Changeset 2808 for src/ERTLptr


Ignore:
Timestamp:
Mar 7, 2013, 6:03:18 PM (8 years ago)
Author:
tranquil
Message:

added local_stacksize to joint internal functions to accomodate for locals in the stack inherited from the front end

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTL.ma

    r2806 r2808  
    4646
    4747definition get_stack:
    48  ∀globals.Register → nat → list (joint_seq LTL globals) ≝
    49  λglobals,r,off.
     48 ∀globals.nat → Register → nat → list (joint_seq LTL globals) ≝
     49 λglobals,localss,r,off.
     50 let off ≝ localss + off in
    5051 set_dp_by_offset ? off @
    5152 [ LOAD … A it it ] @
     
    5354
    5455definition set_stack_not_a :
    55  ∀globals.nat → Register → list (joint_seq LTL globals) ≝
    56  λglobals,off,r.
     56 ∀globals.nat → nat → Register → list (joint_seq LTL globals) ≝
     57 λglobals,localss,off,r.
     58 let off ≝ localss + off in
    5759 set_dp_by_offset ? off @
    5860 [ A ← r
     
    6062
    6163definition set_stack_a :
    62  ∀globals.nat → list (joint_seq LTL globals) ≝
    63  λglobals,off.
     64 ∀globals.nat → nat → list (joint_seq LTL globals) ≝
     65 λglobals,localss,off.
    6466 [ RegisterST1 ← A ] @
    65  set_stack_not_a ? off RegisterST1.
     67 set_stack_not_a ? localss off RegisterST1.
    6668
    6769definition set_stack :
    68  ∀globals.nat → Register → list (joint_seq LTL globals) ≝
    69  λglobals,off,r.
     70 ∀globals.nat → nat → Register → list (joint_seq LTL globals) ≝
     71 λglobals,localss,off,r.
    7072 if eq_Register r RegisterA then
    71    set_stack_a ? off
     73   set_stack_a ? localss off
    7274 else
    73    set_stack_not_a ? off r.
     75   set_stack_not_a ? localss off r.
    7476 
    7577definition set_stack_int :
    76   ∀globals.nat → Byte →  list (joint_seq LTL globals) ≝
    77   λglobals,off,int.
     78  ∀globals.nat → nat → Byte →  list (joint_seq LTL globals) ≝
     79  λglobals,localss,off,int.
     80  let off ≝ localss + off in
    7881  set_dp_by_offset ? off @
    7982  [ A ← int
     
    8184
    8285definition move :
    83   ∀globals.bool → decision → arg_decision → list (joint_seq LTL globals) ≝
    84   λglobals,carry_lives_after,dst,src.
     86  ∀globals.nat → bool → decision → arg_decision → list (joint_seq LTL globals) ≝
     87  λglobals,localss,carry_lives_after,dst,src.
    8588  match dst with
    8689  [ decision_colour dstr ⇒
     
    9396    | arg_decision_spill srco ⇒
    9497      preserve_carry_bit ? carry_lives_after
    95         (get_stack ? dstr srco)
     98        (get_stack ? localss dstr srco)
    9699    | arg_decision_imm int ⇒
    97100      [ A ← int ] @
     
    103106    [ arg_decision_colour srcr ⇒
    104107      preserve_carry_bit ? carry_lives_after
    105         (set_stack ? dsto srcr)
     108        (set_stack ? localss dsto srcr)
    106109    | arg_decision_spill srco ⇒
    107110      if eqb srco dsto then [ ] else
    108111      preserve_carry_bit ? carry_lives_after
    109         (get_stack ? RegisterA srco @
    110          set_stack ? dsto RegisterA)
     112        (get_stack ? localss RegisterA srco @
     113         set_stack ? localss dsto RegisterA)
    111114    | arg_decision_imm int ⇒
    112115      preserve_carry_bit ? carry_lives_after
    113         (set_stack_int ? dsto int)
     116        (set_stack_int ? localss dsto int)
    114117    ]
    115118  ].
     
    169172
    170173definition translate_op2 :
    171   ∀globals.bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    172   λglobals,carry_lives_after,op,dst,arg1,arg2.
     174  ∀globals.nat → bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
     175  λglobals,localss,carry_lives_after,op,dst,arg1,arg2.
    173176  (* this won't preserve the carry bit if op does not set it: left to next function *)
    174177  (* if op uses carry bit (⇒ it sets it too) it must be preserved before the op *)
    175178  (preserve_carry_bit ?
    176179    (uses_carry op ∧ (arg_is_spilled arg1 ∨ arg_is_spilled arg2))
    177     (move ? false RegisterB arg2 @
    178      move ? false RegisterA arg1) @
     180    (move ? localss false RegisterB arg2 @
     181     move ? localss false RegisterA arg1) @
    179182    [ A ← A .op. RegisterB ] @
    180183    (* it op sets the carry bit and it is needed afterwards it must be preserved here *)
    181     move ? (sets_carry op ∧ carry_lives_after) dst RegisterA).
     184    move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA).
    182185
    183186definition translate_op2_smart :
    184   ∀globals.bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    185   λglobals,carry_lives_after,op,dst,arg1,arg2.
     187  ∀globals.nat → bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
     188  λglobals,localss,carry_lives_after,op,dst,arg1,arg2.
    186189  (* if op does not set carry bit (⇒ it does not use it either) then it must be
    187190    preserved *)
     
    191194    (match arg2 with
    192195    [ arg_decision_colour arg2r ⇒
    193       move ? (uses_carry op) RegisterA arg1 @
     196      move ? localss (uses_carry op) RegisterA arg1 @
    194197      [ A ← A .op. arg2r ] @
    195       move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
     198      move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA
    196199    | arg_decision_imm arg2i ⇒
    197       move ? (uses_carry op) RegisterA arg1 @
     200      move ? localss (uses_carry op) RegisterA arg1 @
    198201      [ A ← A .op. arg2i ] @
    199       move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
     202      move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA
    200203    | _ ⇒
    201204      if commutative op then
    202205        match arg1 with
    203206        [ arg_decision_colour arg1r ⇒
    204           move ? (uses_carry op) RegisterA arg2 @
     207          move ? localss (uses_carry op) RegisterA arg2 @
    205208          [ A ← A .op. arg1r ] @
    206           move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
     209          move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA
    207210        | arg_decision_imm arg1i ⇒
    208           move ? (uses_carry op) RegisterA arg2 @
     211          move ? localss (uses_carry op) RegisterA arg2 @
    209212          [ A ← A .op. arg1i ] @
    210           move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
     213          move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA
    211214        | _ ⇒
    212           translate_op2 ? carry_lives_after op dst arg1 arg2
     215          translate_op2 ? localss carry_lives_after op dst arg1 arg2
    213216        ]
    214217      else
    215         translate_op2 ? carry_lives_after op dst arg1 arg2
     218        translate_op2 ? localss carry_lives_after op dst arg1 arg2
    216219    ]).
    217220
     
    225228
    226229definition translate_op1 :
    227   ∀globals.bool → Op1 → decision → decision → list (joint_seq LTL globals) ≝
    228   λglobals,carry_lives_after,op,dst,arg.
     230  ∀globals.nat → bool → Op1 → decision → decision → list (joint_seq LTL globals) ≝
     231  λglobals,localss,carry_lives_after,op,dst,arg.
    229232  let preserve_carry ≝ carry_lives_after ∧ (is_spilled dst ∨ is_spilled arg) in
    230233  preserve_carry_bit ? preserve_carry
    231     (move ? false RegisterA arg @
     234    (move ? localss false RegisterA arg @
    232235     OP1 … op it it ::
    233      move ? false dst RegisterA).
     236     move ? localss false dst RegisterA).
    234237
    235238definition translate_opaccs :
    236   ∀globals.bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    237   λglobals,carry_lives_after,op,dst1,dst2,arg1,arg2.
     239  ∀globals.nat → bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
     240  λglobals,localss,carry_lives_after,op,dst1,dst2,arg1,arg2.
    238241  (* OPACCS always has dead carry bit and sets it to zero *)
    239   move ? false RegisterB arg2 @
    240   move ? false RegisterA arg1 @
     242  move ? localss false RegisterB arg2 @
     243  move ? localss false RegisterA arg1 @
    241244  OPACCS … op it it it it ::
    242   move ? false dst1 RegisterA @
    243   move ? false dst2 RegisterB @
     245  move ? localss false dst1 RegisterA @
     246  move ? localss false dst2 RegisterB @
    244247  if carry_lives_after ∧ (is_spilled dst1 ∨ is_spilled dst2) then
    245248    [CLEAR_CARRY ??]
     
    248251(* does not preserve carry bit *)
    249252definition move_to_dp :
    250   ∀globals.arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    251   λglobals,arg1,arg2.
     253  ∀globals.nat → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
     254  λglobals,localss,arg1,arg2.
    252255  if ¬arg_is_spilled arg1 then
    253     move ? false RegisterDPH arg2 @
     256    move ? localss false RegisterDPH arg2 @
    254257    (* does not change dph because arg1 is not spilled *)
    255     move ? false RegisterDPL arg1
     258    move ? localss false RegisterDPL arg1
    256259  else if ¬arg_is_spilled arg2 then
    257     move ? false RegisterDPL arg1 @
     260    move ? localss false RegisterDPL arg1 @
    258261    (* does not change dpl because arg2 is not spilled *)
    259     move ? false RegisterDPH arg2
     262    move ? localss false RegisterDPH arg2
    260263  else
    261264    (* using B as temporary, as moving spilled registers tampers with DPTR *)
    262     move ? false RegisterB arg1 @
    263     move ? false RegisterDPH arg2 @
    264     move ? false RegisterDPL RegisterB.
     265    move ? localss false RegisterB arg1 @
     266    move ? localss false RegisterDPH arg2 @
     267    move ? localss false RegisterDPL RegisterB.
    265268
    266269definition translate_store : 
    267   ∀globals.bool → arg_decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    268   λglobals,carry_lives_after,addr1,addr2,src.
     270  ∀globals.nat → bool → arg_decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
     271  λglobals,localss,carry_lives_after,addr1,addr2,src.
    269272  (* requires src != RegisterA and RegisterB *)
    270273  preserve_carry_bit ? (carry_lives_after ∧
    271274    (arg_is_spilled addr1 ∨ arg_is_spilled addr1 ∨ arg_is_spilled src))
    272     (let move_to_dptr ≝ move_to_dp ? addr1 addr2 in
     275    (let move_to_dptr ≝ move_to_dp ? localss addr1 addr2 in
    273276     (if arg_is_spilled src then
    274         move ? false RegisterST0 src @
     277        move ? localss false RegisterST0 src @
    275278        move_to_dptr @
    276279        [ A ← RegisterST0]
     
    279282
    280283definition translate_load : 
    281   ∀globals.bool → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    282   λglobals,carry_lives_after,dst,addr1,addr2.
     284  ∀globals.nat → bool → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
     285  λglobals,localss,carry_lives_after,dst,addr1,addr2.
    283286  preserve_carry_bit ? (carry_lives_after ∧
    284287    (is_spilled dst ∨ arg_is_spilled addr1 ∨ arg_is_spilled addr1))
    285     (move_to_dp ? addr1 addr2 @
     288    (move_to_dp ? localss addr1 addr2 @
    286289     [ LOAD … A it it ] @
    287      move ? false dst RegisterA).
     290     move ? localss false dst RegisterA).
    288291
    289292definition translate_address :
    290   ∀globals.bool → ∀i.i ∈ globals → decision → decision →
     293  ∀globals.nat → bool → ∀i.i ∈ globals → decision → decision →
    291294  list (joint_seq LTL globals) ≝
    292   λglobals,carry_lives_after,id,prf,addr1,addr2.
     295  λglobals,localss,carry_lives_after,id,prf,addr1,addr2.
    293296  preserve_carry_bit ? (carry_lives_after ∧ (is_spilled addr1 ∨ is_spilled addr2))
    294297    (ADDRESS LTL ? id prf it it ::
    295      move ? false addr1 RegisterDPL @
    296      move ? false addr2 RegisterDPH).
     298     move ? localss false addr1 RegisterDPL @
     299     move ? localss false addr2 RegisterDPH).
    297300
    298301definition translate_low_address :
    299   ∀globals.bool → decision → label →
     302  ∀globals.nat → bool → decision → label →
    300303  list (joint_seq LTL globals) ≝
    301   λglobals,carry_lives_after,dst,lbl.
     304  λglobals,localss,carry_lives_after,dst,lbl.
    302305  match dst return λ_.list (joint_seq LTL globals) with
    303306  [ decision_colour r ⇒ [LOW_ADDRESS r lbl]
    304307  | _ ⇒
    305     LOW_ADDRESS RegisterA lbl :: move ? carry_lives_after dst RegisterA
     308    LOW_ADDRESS RegisterA lbl :: move ? localss carry_lives_after dst RegisterA
    306309  ].
    307310
    308311definition translate_high_address :
    309   ∀globals.bool → decision → label →
     312  ∀globals.nat → bool → decision → label →
    310313  list (joint_seq LTL globals) ≝
    311   λglobals,carry_lives_after,dst,lbl.
     314  λglobals,localss,carry_lives_after,dst,lbl.
    312315  match dst return λ_.list (joint_seq LTL globals) with
    313316  [ decision_colour r ⇒ [HIGH_ADDRESS r lbl]
    314317  | _ ⇒
    315     HIGH_ADDRESS RegisterA lbl :: move ? carry_lives_after dst RegisterA
     318    HIGH_ADDRESS RegisterA lbl :: move ? localss carry_lives_after dst RegisterA
    316319  ].
    317320
    318321definition translate_step:
    319   ∀globals.∀after : valuation register_lattice.
     322  ∀globals.nat → ∀after : valuation register_lattice.
    320323  coloured_graph after →
    321324  ℕ → label → joint_step ERTLptr globals → bind_step_block LTL globals ≝
    322   λglobals,after,grph,stack_sz,lbl,s.
     325  λglobals,localss,after,grph,stack_sz,lbl,s.
    323326  bret … (
    324327  let lookup ≝ λr.colouring … grph (inl … r) in
     
    328331    ] in
    329332  let carry_lives_after ≝ hlives RegisterCarry (after lbl) in
    330   let move ≝ move globals carry_lives_after in
     333  let move ≝ move globals localss carry_lives_after in
    331334  match s with
    332335  [ step_seq s' ⇒
     
    340343      [ PUSH … A ]
    341344    | STORE addr1 addr2 srcr ⇒
    342       translate_store ? carry_lives_after
     345      translate_store ? localss carry_lives_after
    343346        (lookup_arg addr1)
    344347        (lookup_arg addr2)
    345348        (lookup_arg srcr)
    346349    | LOAD dstr addr1 addr2 ⇒
    347       translate_load ? carry_lives_after
     350      translate_load ? localss carry_lives_after
    348351        (lookup dstr)
    349352        (lookup_arg addr1)
     
    352355    | SET_CARRY ⇒ [CLEAR_CARRY ??]
    353356    | OP2 op dst arg1 arg2 ⇒
    354       translate_op2_smart ? carry_lives_after op
     357      translate_op2_smart ? localss carry_lives_after op
    355358        (lookup dst)
    356359        (lookup_arg arg1)
    357360        (lookup_arg arg2)
    358361    | OP1 op dst arg ⇒
    359       translate_op1 ? carry_lives_after op
     362      translate_op1 ? localss carry_lives_after op
    360363        (lookup dst)
    361364        (lookup arg)
     
    373376      move dst src
    374377    | ADDRESS lbl prf dpl dph ⇒
    375       translate_address ? carry_lives_after
     378      translate_address ? localss carry_lives_after
    376379        lbl prf (lookup dpl) (lookup dph)
    377380    | OPACCS op dst1 dst2 arg1 arg2 ⇒
    378       translate_opaccs ? carry_lives_after op
     381      translate_opaccs ? localss carry_lives_after op
    379382        (lookup dst1) (lookup dst2)
    380383        (lookup_arg arg1) (lookup_arg arg2)
     
    389392          ]
    390393        | LOW_ADDRESS r1 l ⇒
    391            translate_low_address ? carry_lives_after (lookup r1) l
     394           translate_low_address ? localss carry_lives_after (lookup r1) l
    392395        | HIGH_ADDRESS r1 l ⇒
    393            translate_high_address ? carry_lives_after (lookup r1) l       
     396           translate_high_address ? localss carry_lives_after (lookup r1) l       
    394397        ]
    395398    ]
     
    403406      | inr dp ⇒
    404407        let 〈dpl, dph〉 ≝ dp in
    405         〈add_dummy_variance … (move_to_dp (lookup_arg dpl) (lookup_arg dph)),
     408        〈add_dummy_variance … (move_to_dp ? localss (lookup_arg dpl) (lookup_arg dph)),
    406409         λ_.CALL LTL ? (inr … 〈it, it〉) n_args it, [ ]〉
    407410      ]
     
    436439    (* added_prologue ≝ *) [ ]
    437440    (* new_regs ≝ *) [ ]
    438     (* f_step ≝ *) (translate_step … coloured_graph stack_sz)
     441    (* f_step ≝ *) (translate_step ? (joint_if_local_stacksize ?? int_fun) … coloured_graph stack_sz)
    439442    (* f_fin ≝ *) (translate_fin_step globals)
    440443    ????).
Note: See TracChangeset for help on using the changeset viewer.