Ignore:
Timestamp:
Jun 26, 2013, 2:22:28 PM (6 years ago)
Author:
piccolo
Message:

Modified RTLsemantics and ERTLsemantics. Now the pop frame will set
to undef the carry bit and all RegisterCallerSaved? exept those used to
pass the return value of a function.

Added an overflow check in ERTL_semantics

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/StatusSimulationHelper.ma

    r3154 r3371  
    181181* #l1 * #mid ** #EQmid #EQl1 whd in ⊢ (% → ?); #EQfin
    182182cases(bind_new_bind_new_instantiates' … Hregs
    183   (bind_new_bind_new_instantiates' … Hdata (goto_commutation … good …
    184        EQfetch Rst1st2 …)))
    185 [2: % assumption
    186 |4: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (??%?); assumption
    187 |3:
     183  ((bind_new_bind_new_instantiates' … Hdata (goto_commutation … good …
     184       EQfetch Rst1st2 …) ? )))
     185[3: % assumption
     186|5: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (??%?); assumption
     187|4:
     188|2: @sym_eq @(bind_new_bind_new_instantiates' … Hdata (pi2 ?? (init ? fn)))
    188189]
    189190#st2_fin ** #EQst2_fin #EQ destruct(EQ) #Hfin_rel
     
    332333    #H cases(H EQint_fn1) -H #data1 * #t_fn1 ** #EQt_fn1 #Hregs1 #good1
    333334    cases(bind_new_bind_new_instantiates' … Hregs
    334     (bind_new_bind_new_instantiates' ?????? Hdata
     335    ((bind_new_bind_new_instantiates' ?????? Hdata
    335336     (tailcall_commutation ?????????? good ???????? EQfetch ? EQbl … EQint_fn1 …
    336        EQssize_f … EQssize_f1 … EQst1_setup … Rst1st2 … EQt_fn1))) [2: % assumption]
     337       EQssize_f … EQssize_f1 … EQst1_setup … Rst1st2 … EQt_fn1)) ?))
     338    [3: % assumption
     339    |2: @sym_eq @(bind_new_bind_new_instantiates' … Hdata (pi2 ?? (init ? fn)))
     340    ]
    337341    #has_tail' * #id' * #arg' * #EQ destruct(EQ) * #st2_pre ** #EQst2_pre #EQt_bl
    338342    * #st2_after * #EQst2_after #H cases(bind_new_bind_new_instantiates' … Hregs1 H)
    339     -H #st2' * #EQst2' #fin_sem_rel
     343    -H [2: @sym_eq
     344           @(bind_new_bind_new_instantiates' … Hregs1 (pi2 ?? (init ? fn1)))]
     345    #st2' * #EQst2' #fin_sem_rel
    340346|2: whd in match fetch_internal_function; normalize nodelta >EQfn1 %
    341347|
     
    366372  whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
    367373  >point_of_pc_of_point >EQmid % ]
    368 cases good1 -good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1))
     374cases good1 -good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1))
    369375#nxt1 * #c #EQin #H lapply(H … EQin) -H normalize nodelta >(f_step_on_cost … data1)
    370376* #st_bl @eq_identifier_elim [2: * #H @⊥ @H % #_ ] #_
     
    582588]
    583589#EQ destruct(EQ) #n_costed
    584 lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
    585 [2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
    586       #H cases(H EQfetch) -H |*:]
     590lapply(b_graph_transform_program_fetch_internal_function … goodR (pc_block (pc … st1)) f fn)
     591@eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta #H
     592cases(H (proj1 … (fetch_statement_inv … EQfetch))) -H
    587593#init_data * #t_fn1 **  >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
    588 #EQt_fn1 whd in ⊢ (% → ?); #Hinit normalize nodelta
    589 *** #blp #blm #bls * whd in ⊢ (% → ?); @if_elim
     594#EQt_fn1 #Hinit * #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ #H
     595lapply(H ?? (proj2 … (fetch_statement_inv … EQfetch))) -H normalize nodelta
     596 whd in ⊢ (% → ?);
     597*** #blp #blm #bls * @if_elim
    590598[1,3: @eq_identifier_elim [2,4: #_ cases(not_emptyb ??) *]
    591       whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??);
    592       #ABS #_ lapply(fetch_statement_inv … EQfetch) * #_
    593       >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
    594       whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??);
    595       <ABS cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
     599      #ABS #_ lapply(fetch_statement_inv … EQfetch) * #_ <ABS
     600      cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
    596601]
    597602#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); *
    598603#l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1
    599604* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    600 cases(bind_new_bind_new_instantiates' … EQbl (bind_new_bind_new_instantiates' … Hinit
    601                (cond_commutation … goodR … EQfetch EQbv EQbool Rst1st2 t_fn1 EQt_fn1)))
    602 [2,4: % assumption]
     605cases(bind_new_bind_new_instantiates' … EQbl ((bind_new_bind_new_instantiates' … Hinit
     606               (cond_commutation … goodR … EQfetch EQbv EQbool Rst1st2 t_fn1 EQt_fn1)) ?))
     607[2,5: @sym_eq >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
     608      @(bind_new_bind_new_instantiates' … Hinit (pi2 ?? (init ? fn)))
     609|3,6: % assumption
     610]
    603611#EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
    604612cases(APP … EQmid) -APP #st_pre_mid_no_pc * #EQst_pre_mid_no_pc *
    605613normalize nodelta
    606 #Hsem * #a' * #EQt_cond * #bv' * #EQbv' #rel_v_v'
     614#Hsem * #a' * #EQt_cond * #bv' * #EQbv' #rel_v_v' #_
    607615[ %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) ltrue)
    608616     (last_pop … st2))}
     
    775783#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl
    776784>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #SBiC
    777 cases(bind_new_bind_new_instantiates' … EQbl (bind_new_bind_new_instantiates' … Hinit
    778                (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
    779                [2: % assumption]
     785cases(bind_new_bind_new_instantiates' … EQbl ((bind_new_bind_new_instantiates' … Hinit
     786               (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)) ? ))
     787[2: @sym_eq >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) 
     788    @(bind_new_bind_new_instantiates' … Hinit (pi2 ?? (init ? fn)))
     789|3: % assumption
     790]
    780791#l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem
    781792%{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
     
    10641075cases(next_of_call_pc_inv … EQnext_of_call) #f1 * #fn1 * #id * #args * #dest #EQcall
    10651076<(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in Hregs; #Hregs
    1066 cases(bind_new_bind_new_instantiates' … Hregs (bind_new_bind_new_instantiates' … Hinit
     1077cases(bind_new_bind_new_instantiates' … Hregs ((bind_new_bind_new_instantiates' … Hinit
    10671078 (return_commutation ?????????? good … Hbl EQfetch … EQssize … EQpop … EQcall …
    1068    Rst1st2 t_fn EQt_fn))) #EQ destruct(EQ) * #st_fin * #EQst_fin * #t_st_pop * #t_pc_pop
     1079   Rst1st2 t_fn EQt_fn)) ? ))
     1080[2: @sym_eq >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch)
     1081    @(bind_new_bind_new_instantiates' … Hinit (pi2 ?? (init ? fn))) ] 
     1082#EQ destruct(EQ) * #st_fin * #EQst_fin * #t_st_pop * #t_pc_pop
    10691083** #EQt_pop #EQt_pc_pop @eqZb_elim #Hbl_pcpop normalize nodelta
    10701084[ * #sem_rel #EQt_next
     
    13471361#id' * #args' * #dest' #EQinstr
    13481362cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs)
    1349   (bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … EQdata)
     1363  ((bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … EQdata)
    13501364 (call_commutation … good … Hbl EQfetch bl EQbl … EQint_fn … EQst1_save … EQssize …
    1351    EQst1_no_pc'' … Rst1st2 … EQt_fn1)) … EQpc' EQt_call EQinstr)
     1365   EQst1_no_pc'' … Rst1st2 … EQt_fn1)) ?) … EQpc' EQt_call EQinstr)
     1366[2: @sym_eq
     1367    @(bind_new_bind_new_instantiates' …
     1368        (bind_instantiates_to_instantiate … EQdata) (pi2 ?? (init ? fn))) ]
    13521369#st2_pre ** #EQst2_pre #EQt_bl * #st2_save * #EQst2_save * #st2_after * #EQst2_after
    13531370#Hprologue
     
    13631380%{(mk_state_pc ? (increment_stack_usage p_out ssize st2_after)
    13641381   (pc_of_point p_out bl (joint_if_entry … t_fn1)) (last_pop … st2))}
    1365 cases(bind_new_bind_new_instantiates' … Hdata1 Hprologue) -Hprologue #st2' * #EQst2'
    1366 #fin_sem_rel cases good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1))
     1382cases(bind_new_bind_new_instantiates' … Hdata1 Hprologue)
     1383[2: @sym_eq @(bind_new_bind_new_instantiates' … Hdata1 (pi2 ?? (init ? fn1)))] 
     1384-Hprologue #st2' * #EQst2'
     1385#fin_sem_rel cases good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1))
    13671386#nxt1 * #c #EQcost #H lapply(H … EQcost) -H -good1 normalize nodelta
    13681387>(f_step_on_cost … data1) *** #pre1 #instr1 #post1 @eq_identifier_elim [2: * #H @⊥ @H %]
Note: See TracChangeset for help on using the changeset viewer.