Ignore:
Timestamp:
Jul 18, 2012, 1:26:43 PM (8 years ago)
Author:
tranquil
Message:
  • moving some code around
  • changed immediates to hold beval in general, not only bytes
  • fixed RTLabsToRTL after redefinitions in front end
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL_paolo.ma

    r2175 r2208  
    1414  | arg_decision_colour : Register → arg_decision
    1515  | arg_decision_spill : ℕ → arg_decision
    16   | arg_decision_imm : Byte → arg_decision.
     16  | arg_decision_imm : beval → arg_decision.
    1717
    1818coercion Reg_to_arg_dec : ∀r:Register.arg_decision ≝ arg_decision_colour on _r : Register to arg_decision.
     
    3535  if do_it then SAVE_CARRY :: steps @ [RESTORE_CARRY] else steps.
    3636
     37(* for notation *)
     38definition A ≝ it.
     39
     40coercion beval_of_byte : ∀b : Byte.beval ≝ BVByte on _b : Byte to beval.
     41
     42(* spill should be byte-based from the start *)
    3743definition set_dp_by_offset :
    38   ∀globals.Byte → list (joint_seq ltl_params globals) ≝
     44  ∀globals.nat → list (joint_seq ltl_params globals) ≝
    3945  λglobals,off.
    40   [ 𝐀 ← off
    41   ; 𝐀 ← 𝐀 .Add. RegisterSPL
    42   ; RegisterDPL ← 𝐀
    43   ; 𝐀 ← 0
    44   ; 𝐀 ← 𝐀 .Addc. RegisterSPH
    45   ; RegisterDPH ← 𝐀
     46  [ A ← byte_of_nat off
     47  ; A ← A .Add. RegisterSPL
     48  ; RegisterDPL ← A
     49  ; A ← zero_byte
     50  ; A ← A .Addc. RegisterSPH
     51  ; RegisterDPH ← A
    4652  ].
    4753
    4854definition get_stack:
    49  ∀globals.Register → Byte → list (joint_seq ltl_params globals) ≝
     55 ∀globals.Register → nat → list (joint_seq ltl_params globals) ≝
    5056 λglobals,r,off.
    5157 set_dp_by_offset ? off @
    52  [ LOAD … it it it ] @
    53  if eq_Register r RegisterA then [ ] else [ r ← 𝐀 ].
     58 [ LOAD … A it it ] @
     59 if eq_Register r RegisterA then [ ] else [ r ← A ].
    5460
    5561definition set_stack_not_a :
    56  ∀globals.Byte → Register → list (joint_seq ltl_params globals) ≝
     62 ∀globals.nat → Register → list (joint_seq ltl_params globals) ≝
    5763 λglobals,off,r.
    5864 set_dp_by_offset ? off @
    59  [ 𝐀 ← r
    60  ; STORE … it it it ].
     65 [ A ← r
     66 ; STORE … it it A ].
    6167
    6268definition set_stack_a :
    63  ∀globals.Byte → list (joint_seq ltl_params globals) ≝
     69 ∀globals.nat → list (joint_seq ltl_params globals) ≝
    6470 λglobals,off.
    65  [ RegisterST1 ← 𝐀 ] @
     71 [ RegisterST1 ← A ] @
    6672 set_stack_not_a ? off RegisterST1.
    6773
    6874definition set_stack :
    69  ∀globals.Byte → Register → list (joint_seq ltl_params globals) ≝
     75 ∀globals.nat → Register → list (joint_seq ltl_params globals) ≝
    7076 λglobals,off,r.
    7177 if eq_Register r RegisterA then
     
    7581 
    7682definition set_stack_int :
    77   ∀globals.Byte → Byte →  list (joint_seq ltl_params globals) ≝
     83  ∀globals.nat → beval →  list (joint_seq ltl_params globals) ≝
    7884  λglobals,off,int.
    7985  set_dp_by_offset ? off @
    80   [ 𝐀 ← int
    81   ; STORE … it it it ].
     86  [ A ← int
     87  ; STORE … it it A ].
    8288
    8389definition move :
     
    8995    [ arg_decision_colour srcr ⇒
    9096      if eq_Register dstr srcr then [ ] else
    91       if eq_Register dstr RegisterA then [ 𝐀 ← srcr ] else
    92       if eq_Register srcr RegisterA then [ dstr ← 𝐀 ] else
    93       [ 𝐀 ← srcr ; dstr ← 𝐀]
     97      if eq_Register dstr RegisterA then [ A ← srcr ] else
     98      if eq_Register srcr RegisterA then [ dstr ← A ] else
     99      [ A ← srcr ; dstr ← A]
    94100    | arg_decision_spill srco ⇒
    95101      preserve_carry_bit ? carry_lives_after
    96102        (get_stack ? dstr srco)
    97103    | arg_decision_imm int ⇒
    98       [ 𝐀 ← int ] @
     104      [ A ← int ] @
    99105      if eq_Register dstr RegisterA then [ ] else
    100       [ dstr ← 𝐀 ]
     106      [ dstr ← A ]
    101107    ]
    102108  | decision_spill dsto ⇒
     
    125131  λglobals,stack_sz.
    126132  [ CLEAR_CARRY …
    127   ; 𝐀 ← RegisterSPL
    128   ; 𝐀 ← 𝐀 .Sub. stack_sz
    129   ; RegisterSPL ← 𝐀
    130   ; 𝐀 ← RegisterSPH
    131   ; 𝐀 ← 𝐀 .Sub. 0
    132   ; RegisterSPL ← 𝐀
     133  ; A ← RegisterSPL
     134  ; A ← A .Sub. byte_of_nat stack_sz
     135  ; RegisterSPL ← A
     136  ; A ← RegisterSPH
     137  ; A ← A .Sub. zero_byte
     138  ; RegisterSPL ← A
    133139  ].
    134140
     
    136142  ∀globals.ℕ → list (joint_seq ltl_params globals) ≝
    137143  λglobals,stack_sz.
    138   [ 𝐀 ← RegisterSPL
    139   ; 𝐀 ← 𝐀 .Add. stack_sz
    140   ; RegisterSPL ← 𝐀
    141   ; 𝐀 ← RegisterSPH
    142   ; 𝐀 ← 𝐀 .Addc. 0
    143   ; RegisterSPL ← 𝐀
     144  [ A ← RegisterSPL
     145  ; A ← A .Add. byte_of_nat stack_sz
     146  ; RegisterSPL ← A
     147  ; A ← RegisterSPH
     148  ; A ← A .Addc. zero_byte
     149  ; RegisterSPL ← A
    144150  ].
    145151
     
    178184    (move ? false RegisterB arg2 @
    179185     move ? false RegisterA arg1) @
    180     [ 𝐀 ← 𝐀 .op. RegisterB ] @
     186    [ A ← A .op. RegisterB ] @
    181187    (* it op sets the carry bit and it is needed afterwards it must be preserved here *)
    182188    move ? (sets_carry op ∧ carry_lives_after) dst RegisterA).
     
    193199    [ arg_decision_colour arg2r ⇒
    194200      move ? (uses_carry op) RegisterA arg1 @
    195       [ 𝐀 ← 𝐀 .op. arg2r ] @
     201      [ A ← A .op. arg2r ] @
    196202      move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
    197203    | arg_decision_imm arg2i ⇒
    198204      move ? (uses_carry op) RegisterA arg1 @
    199       [ 𝐀 ← 𝐀 .op. arg2i ] @
     205      [ A ← A .op. arg2i ] @
    200206      move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
    201207    | _ ⇒
     
    204210        [ arg_decision_colour arg1r ⇒
    205211          move ? (uses_carry op) RegisterA arg2 @
    206           [ 𝐀 ← 𝐀 .op. arg1r ] @
     212          [ A ← A .op. arg1r ] @
    207213          move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
    208214        | arg_decision_imm arg1i ⇒
    209215          move ? (uses_carry op) RegisterA arg2 @
    210           [ 𝐀 ← 𝐀 .op. arg1i ] @
     216          [ A ← A .op. arg1i ] @
    211217          move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
    212218        | _ ⇒
     
    275281        move ? false RegisterST0 src @
    276282        move_to_dptr @
    277         [ 𝐀 ← RegisterST0]
     283        [ A ← RegisterST0]
    278284      else move_to_dptr) @
    279      [STORE … it it it]).
     285     [STORE … it it A]).
    280286
    281287definition translate_load : 
     
    285291    (is_spilled dst ∨ arg_is_spilled addr1 ∨ arg_is_spilled addr1))
    286292    (move_to_dp ? addr1 addr2 @
    287      [ LOAD … it it it ] @
     293     [ LOAD … A it it ] @
    288294     move ? false dst RegisterA).
    289295
     
    315321    | COST_LABEL cost_lbl ⇒ COST_LABEL … cost_lbl
    316322    | POP r ⇒
    317       POP … it ::
     323      POP … A ::
    318324      move (lookup r) RegisterA
    319325    | PUSH a ⇒
    320326      move RegisterA (lookup_arg a) @
    321       [ PUSH … it ]
     327      [ PUSH … A ]
    322328    | STORE addr1 addr2 srcr ⇒
    323329      translate_store ? carry_lives_after
     
    349355      let src ≝
    350356        match \snd pair_regs return λ_.arg_decision with
    351         [ REG r ⇒ lookup_move_dst r
    352         | INT b ⇒ arg_decision_imm b
     357        [ Reg r ⇒ lookup_move_dst r
     358        | Imm b ⇒ arg_decision_imm b
    353359        ] in
    354360      move dst src
     
    365371      | ertl_del_frame ⇒ delframe ? stack_sz
    366372      | ertl_frame_size r ⇒
    367         move (lookup r) (arg_decision_imm stack_sz)
     373        move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
    368374      ]
    369375    | CALL_ID f n_args _ ⇒ CALL_ID ltl_params ? f n_args it
     
    384390
    385391definition translate_internal: ∀globals: list ident.
    386   ertl_internal_function globals → joint_internal_function globals ltl_params ≝
     392  joint_internal_function globals ertl_params →
     393  joint_internal_function globals ltl_params ≝
    387394  λglobals: list ident.
    388   λint_fun: ertl_internal_function globals.
     395  λint_fun: joint_internal_function globals ertl_params.
    389396  (* initialize graph *)
    390397  let entry ≝ pi1 … (joint_if_entry … int_fun) in
Note: See TracChangeset for help on using the changeset viewer.