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/StatusSimulationUtils.ma

    r3262 r3371  
    256256  return 〈f,t_fn〉 →
    257257  bind_new_P' ??
    258      (λregs1.λdata.bind_new_P' ??
     258     (λregs1.λdata.
     259     init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
    259260      (λregs2.λblp.
    260261       ∃l : list (joint_seq P_out (globals ? (mk_prog_params P_out trans_prog stack_sizes))).
     
    292293     return 〈f,t_fn〉 →
    293294    bind_new_P' ??
    294      (λregs1.λdata.bind_new_P' ??
     295     (λregs1.λdata.
     296      init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
    295297     (λregs2.λblp.(\snd blp) = [ ] ∧
    296298        ∀mid.
     
    342344  bind_new_P' ??
    343345     (λregs1.λdata.
    344       bind_new_P' ??
     346      init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
    345347      (λregs2.λblp.
    346348       \snd blp = (RETURN …) ∧
     
    426428  bind_new_P' ??
    427429    (λregs1.λdata.
    428      bind_new_P' ??
     430     init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
    429431      (λregs2.λblp.
    430432        ∀pc',t_fn,id',arg',dest',nxt1.
     
    448450       bind_new_P' ??
    449451         (λregs11.λdata1.
    450           ∃st2'.
     452          init_regs bl = new_regs … data1 → ∃st2'.
    451453           repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1
    452454           (added_prologue … data1) (increment_stack_usage P_out n st2_after_call) =
     
    481483  bind_new_P' ??
    482484     (λregs1.λdata.
    483       bind_new_P' ??
     485      init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
    484486      (λregs2.λblp.
    485487        ∃st_fin. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
     
    523525   bind_new_P' ??
    524526    (λregs1.λdata.
    525      bind_new_P' ??
     527     init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
    526528      (λregs2.λblp.
    527529       ∃ has_tail',id',arg'.
     
    537539       bind_new_P' ??
    538540         (λregs11.λdata1.
    539           ∃st2'.
     541          init_regs bl = new_regs … data1 → ∃st2'.
    540542           repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1
    541543           (added_prologue … data1) (increment_stack_usage P_out ssize_f1 st2_after) =
     
    782784lapply(b_graph_transform_program_fetch_internal_function … good … bl id fn)
    783785@eqZb_elim [ #EQ >EQ in Hbl; #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) -H
    784 #data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #pp_labs #_ #fresh_lab #_ #_ #_ #H
     786#data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #_ #_ #pp_labs #_ #fresh_lab #_ #_ #_ #H
    785787lapply(H … EQstmt) -H normalize nodelta cases stmt in EQstmt; -stmt
    786788[ #j_step #nxt | #fin | * ] #EQstmt normalize nodelta **
     
    984986lapply(b_graph_transform_program_fetch_internal_function … good … (pc_block pc) f fn)
    985987@eqZb_elim [ #EQ >EQ in Hbl; * #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) -H
    986 #data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #pp_labs #_ #fresh_labs #_ #_ #_ #H
     988#data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #_ #_ #pp_labs #_ #fresh_labs #_ #_ #_ #H
    987989lapply(H … EQstmt) -H normalize nodelta #H #_ %{data} >Hinit %{(refl …)}
    988990-EQfetch cases stmt in EQstmt H;
Note: See TracChangeset for help on using the changeset viewer.