Changeset 2208 for src/ERTL


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
Location:
src/ERTL
Files:
1 added
3 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
  • src/ERTL/ERTL_paolo.ma

    r2174 r2208  
    66  | HDW: Register → move_dst.
    77
    8 inductive move_src: Type[0] ≝
    9   | INT: Byte → move_src
    10   | REG: move_dst → move_src.
     8definition move_src ≝ argument move_dst.
    119
    12 coercion move_dst_to_src : ∀r : move_dst.move_src ≝ REG on _r : move_dst to move_src.
     10definition move_src_from_dst : move_dst → move_src ≝ Reg move_dst.
     11coercion move_dst_to_src : ∀r : move_dst.move_src ≝ move_src_from_dst on _r : move_dst to move_src.
    1312
    14 definition rtl_argument_move_src : rtl_argument → move_src ≝
     13definition psd_argument_move_src : psd_argument → move_src ≝
    1514  λarg.match arg with
    16   [ Imm b ⇒ INT b
    17   | Reg r ⇒ REG (PSD r)
     15  [ Imm b ⇒ Imm ? b
     16  | Reg r ⇒ Reg ? (PSD r)
    1817  ].
    19 
    20 coercion rtl_argument_to_move_src : ∀a:rtl_argument.move_src ≝
    21   rtl_argument_move_src on _a : rtl_argument to move_src.
     18coercion psd_argument_to_move_src : ∀a:psd_argument.move_src ≝
     19  psd_argument_move_src on _a : psd_argument to move_src.
    2220
    2321inductive ertl_seq : Type[0] ≝
     
    3028    (* acc_a_reg ≝ *) register
    3129    (* acc_b_reg ≝ *) register
    32     (* acc_a_arg ≝ *) rtl_argument
    33     (* acc_b_arg ≝ *) rtl_argument
     30    (* acc_a_arg ≝ *) psd_argument
     31    (* acc_b_arg ≝ *) psd_argument
    3432    (* dpl_reg   ≝ *) register
    3533    (* dph_reg   ≝ *) register
    36     (* dpl_arg   ≝ *) rtl_argument
    37     (* dph_arg   ≝ *) rtl_argument
    38     (* snd_arg   ≝ *) rtl_argument
     34    (* dpl_arg   ≝ *) psd_argument
     35    (* dph_arg   ≝ *) psd_argument
     36    (* snd_arg   ≝ *) psd_argument
    3937    (* pair_move ≝ *) (move_dst × move_src)
    4038    (* call_args ≝ *) ℕ
     
    5048      (* localsT ≝ *) register).
    5149
    52   definition ertl_params ≝ mk_graph_params ertl_uns_params.
    53   definition ertl_internal_function ≝
    54   λglobals. joint_internal_function globals ertl_params.
     50definition ertl_params ≝ mk_graph_params ertl_uns_params.
    5551definition ertl_program ≝ joint_program ertl_params.
    5652
     
    6965unification hint 0 ≔
    7066(*---------------*) ⊢
    71 acc_a_arg ertl_params ≡ rtl_argument.
     67acc_a_arg ertl_params ≡ psd_argument.
    7268unification hint 0 ≔
    7369(*---------------*) ⊢
    74 acc_b_arg ertl_params ≡ rtl_argument.
     70acc_b_arg ertl_params ≡ psd_argument.
    7571unification hint 0 ≔
    7672(*---------------*) ⊢
     
    8177unification hint 0 ≔
    8278(*---------------*) ⊢
    83 dpl_arg ertl_params ≡ rtl_argument.
     79dpl_arg ertl_params ≡ psd_argument.
    8480unification hint 0 ≔
    8581(*---------------*) ⊢
    86 dph_arg ertl_params ≡ rtl_argument.
     82dph_arg ertl_params ≡ psd_argument.
    8783unification hint 0 ≔
    8884(*---------------*) ⊢
    89 snd_arg ertl_params ≡ rtl_argument.
     85snd_arg ertl_params ≡ psd_argument.
    9086unification hint 0 ≔
    9187(*---------------*) ⊢
     
    105101ext_tailcall ertl_params ≡ void.
    106102
    107 coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ertl_params ≝ Reg
     103coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ertl_params ≝
     104  psd_argument_from_reg
    108105  on _r : register to snd_arg ertl_params.
    109 coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ertl_params ≝ Imm
     106coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ertl_params ≝
     107  psd_argument_from_byte
    110108  on _b : Byte to snd_arg ertl_params.
    111109 
  • src/ERTL/liveness_paolo.ma

    r2182 r2208  
    9292definition ret_regs ≝ set_from_list … RegisterRets.
    9393
    94 definition rl_arg : rtl_argument → register_lattice ≝
     94definition rl_arg : psd_argument → register_lattice ≝
    9595  λarg.match arg with
    9696  [ Imm _ ⇒ rl_bottom
     
    124124        let r2 ≝ \snd pair_reg in
    125125        match r2 with
    126         [ REG p ⇒
     126        [ Reg p ⇒
    127127          match p with
    128128          [ PSD r ⇒ rl_psingleton r
    129129          | HDW r ⇒ rl_hsingleton r
    130130          ]
    131         | INT _ ⇒ rl_bottom
     131        | Imm _ ⇒ rl_bottom
    132132        ]
    133133      | extension_seq ext ⇒
     
    236236definition livebefore ≝
    237237  λglobals: list ident.
    238   λint_fun: ertl_internal_function globals.
     238  λint_fun: joint_internal_function globals ertl_params.
    239239  λlabel.
    240240  λliveafter: valuation register_lattice.
     
    246246definition liveafter ≝
    247247   λglobals: list ident.
    248   λint_fun: ertl_internal_function globals.
     248  λint_fun: joint_internal_function globals ertl_params.
    249249  λlabel.
    250250  λliveafter: valuation register_lattice.
Note: See TracChangeset for help on using the changeset viewer.