Changeset 3037 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Mar 29, 2013, 5:19:53 PM (7 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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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      ]
Note: See TracChangeset for help on using the changeset viewer.