Changeset 3371 for src/ERTL/ERTLToLTL.ma


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/ERTL/ERTLToLTL.ma

    r3263 r3371  
    3838  ∀globals.nat → list (joint_seq LTL globals) ≝
    3939  λglobals,off.
    40   [ A ← byte_of_nat off
     40  let 〈off_h, off_l〉 ≝ (vsplit … 8 8 (bitvector_of_nat 16 off) : Byte × Byte) in
     41  [ A ← off_l
    4142  ; A ← A .Add. RegisterSPL
    4243  ; RegisterDPL ← A
    43   ; A ← zero_byte
     44  ; A ← off_h
    4445  ; A ← A .Addc. RegisterSPH
    4546  ; RegisterDPH ← A
     
    127128  ∀globals.ℕ → list (joint_seq LTL globals) ≝
    128129  λglobals,stack_sz.
    129   [ CLEAR_CARRY …
     130  let 〈off_h, off_l〉 ≝ (vsplit … 8 8 (bitvector_of_nat 16 stack_sz) : Byte × Byte) in
     131  [ CLEAR_CARRY ??
    130132  ; A ← RegisterSPL
    131   ; A ← A .Sub. byte_of_nat stack_sz
     133  ; A ← A .Sub. off_l
    132134  ; RegisterSPL ← A
    133135  ; A ← RegisterSPH
    134   ; A ← A .Sub. zero_byte
     136  ; A ← A .Sub. off_h
    135137  ; RegisterSPH ← A
    136138  ].
     
    139141  ∀globals.ℕ → list (joint_seq LTL globals) ≝
    140142  λglobals,stack_sz.
     143  let 〈off_h, off_l〉 ≝ (vsplit … 8 8 (bitvector_of_nat 16 stack_sz) : Byte × Byte) in
    141144  [ A ← RegisterSPL
    142   ; A ← A .Add. byte_of_nat stack_sz
     145  ; A ← A .Add. off_l
    143146  ; RegisterSPL ← A
    144147  ; A ← RegisterSPH
    145   ; A ← A .Addc. zero_byte
     148  ; A ← A .Addc. off_h
    146149  ; RegisterSPH ← A
    147150  ].
     
    406409 ∀globals.
    407410  joint_closed_internal_function ERTL globals →
    408   bind_new register (b_graph_translate_data ERTL LTL globals)
     411  bound_b_graph_translate_data ERTL LTL globals
    409412λthe_fixpoint,build,globals,int_fun.
    410413νν |RegisterCalleeSaved| as callee_saved_store in
     
    436439    ????).
    437440@hide_prf
    438 [3: #l #c % ]
     441[3: #l #c %
     442|5: #r0 #r1 #r2 #r3 #r4 #r5 #r6 #r7 %
     443]
    439444cases daemon (* TODO *)
    440445qed.
     
    449454   let ltlprog ≝ b_graph_transform_program … (translate_data the_fixpoint build) pr in
    450455   〈ltlprog, stack_cost … ltlprog, 2^16 - globals_stacksize … ltlprog〉.
    451 #r0 #r1 #r2 #r3 #r4 #r5 #r6 #r7 %
    452 qed.
    453456
    454457lemma ERTLToLTL_monotone_stacksizes :
Note: See TracChangeset for help on using the changeset viewer.