Changeset 3037 for src/ERTL


Ignore:
Timestamp:
Mar 29, 2013, 5:19:53 PM (8 years ago)
Author:
tranquil
Message:
  • ADDRESS joint instruction now has also an offset
  • corrected call to pointer (needed to clear the accumulator)
  • now we make sure globals contain also function names

LINToASM will be fixed in an upcoming commit

Location:
src/ERTL
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r2952 r3037  
    125125  on _s : ertl_seq to joint_seq ERTL ?.
    126126
    127 definition ERTL_premain : ∀p : ertl_program.joint_closed_internal_function ERTL (prog_var_names ?? p) ≝
     127definition ERTL_premain : ∀p : ertl_program.
     128  joint_closed_internal_function ERTL (prog_names … p) ≝
    128129λp.
    129130let l1 : label ≝ an_identifier … one in
     
    131132let l3 : label ≝ an_identifier … (p1 one) in
    132133let res ≝
    133   mk_joint_internal_function ERTL (prog_var_names … p)
     134  mk_joint_internal_function ERTL (prog_names … p)
    134135  (mk_universe … (p0 (p0 one)))
    135136  (mk_universe … one)
  • src/ERTL/ERTLToLTL.ma

    r3014 r3037  
    291291
    292292definition translate_address :
    293   ∀globals.nat → bool → ∀i.i ∈ globals → decision → decision →
     293  ∀globals.nat → bool → ∀i.i ∈ globals → Word → decision → decision →
    294294  list (joint_seq LTL globals) ≝
    295   λglobals,localss,carry_lives_after,id,prf,addr1,addr2.
     295  λglobals,localss,carry_lives_after,id,prf,off,addr1,addr2.
    296296  preserve_carry_bit ? (carry_lives_after ∧ (is_spilled addr1 ∨ is_spilled addr2))
    297     (ADDRESS LTL ? id prf it it ::
     297    (ADDRESS LTL ? id prf off it it ::
    298298     move ? localss false addr1 RegisterDPL @
    299299     move ? localss false addr2 RegisterDPH).
     
    356356        ] in
    357357      move dst src
    358     | ADDRESS lbl prf dpl dph ⇒
     358    | ADDRESS lbl prf off dpl dph ⇒
    359359      translate_address ? localss carry_lives_after
    360         lbl prf (lookup dpl) (lookup dph)
     360        lbl prf off (lookup dpl) (lookup dph)
    361361    | OPACCS op dst1 dst2 arg1 arg2 ⇒
    362362      translate_opaccs ? localss carry_lives_after op
     
    384384          λ_.PUSH LTL ? it;
    385385          λl.HIGH_ADDRESS l;
    386           λ_.PUSH LTL ? it],
     386          λ_.PUSH LTL ? it ;
     387          (* necessary as ptr CALL will be JMP A+DPTR *)
     388          λ_.A ← zero_byte ],
    387389         λ_.CALL LTL ? (inr … 〈it, it〉) n_args it, [ ]〉
    388390      ]
  • src/ERTL/liveness.ma

    r3014 r3037  
    6161      | OP1 op1 r1 r2 ⇒ rl_psingleton r1
    6262      | POP r ⇒ rl_psingleton r
    63       | ADDRESS _ _ r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
     63      | ADDRESS _ _ _ r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
    6464      | LOAD r _ _ ⇒ rl_psingleton r
    6565      | COMMENT c ⇒ rl_bottom
     
    176176  | OP1 op1 r1 r2 ⇒
    177177    ¬set_member … (eq_identifier …) r1 pliveafter
    178   | ADDRESS _ _ r1 r2 ⇒
     178  | ADDRESS _ _ _ r1 r2 ⇒
    179179    ¬(set_member … (eq_identifier …) r1 pliveafter ∨
    180180      set_member … (eq_identifier …) r2 pliveafter)
  • src/ERTL/uses.ma

    r3014 r3037  
    4747         match s with
    4848         [ COMMENT _ ⇒ map
    49          | ADDRESS _ _ _ _ ⇒ map
     49         | ADDRESS _ _ _ _ _ ⇒ map
    5050         | CLEAR_CARRY ⇒ map
    5151         | SET_CARRY ⇒ map
Note: See TracChangeset for help on using the changeset viewer.