Changeset 3255 for src/ASM


Ignore:
Timestamp:
May 8, 2013, 4:53:31 PM (6 years ago)
Author:
tranquil
Message:
  • dropped newframe and delframe (to be integrated in calls and returns

in the semantics), as they were too wild for the proof of ERTL to LTL

  • ERTL now has a policy on what hardware registers can be written or

read

  • Rearranged special hardware registers: dropped STS, ST2 and ST3, and

moved DPL and DPH out of RegistersRets?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/I8051.ma

    r2645 r3255  
    102102
    103103(* dpm: registers for stack manipulation *)
    104 definition RegisterSST ≝ Register10.
    105 definition RegisterST0 ≝ Register02.
    106 definition RegisterST1 ≝ Register03.
    107 definition RegisterST2 ≝ Register04.
    108 definition RegisterST3 ≝ Register05.
    109 definition RegisterSTS ≝ [RegisterST0; RegisterST1; RegisterST2; RegisterST3].
     104definition RegisterRets ≝ [Register00; Register01; Register02; Register03 ].
     105definition RegisterST0 ≝ Register04.
     106definition RegisterST1 ≝ Register05.
    110107definition RegisterSPL ≝ Register06.
    111108definition RegisterSPH ≝ Register07.
     
    121118   Register31; Register32; Register33; Register34; Register35;
    122119   Register36; Register37; RegisterA; RegisterB; RegisterDPL;
    123    RegisterDPH; RegisterSPL; RegisterSPH; RegisterST0; RegisterST1;
    124    RegisterSST].
    125 definition RegisterRets ≝ [RegisterDPL; RegisterDPH; Register00; Register01].
     120   RegisterDPH ].
    126121definition RegisterCallerSaved ≝
    127122  [Register00; Register01; Register02; Register03; Register04;
     
    135130definition RegistersForbidden ≝
    136131  [RegisterA; RegisterB; RegisterDPL; RegisterDPH;
    137    RegisterSPL; RegisterSPH; RegisterST0; RegisterST1;
    138    RegisterST2; RegisterST3; RegisterSST].
    139 (* registers minus forbidden *)
    140 definition RegistersAllocatable ≝
    141   [Register00; Register01; Register02; Register03; Register04;
    142    Register05; Register06; Register07; Register10; Register11;
    143    Register12; Register13; Register14; Register15; Register16;
    144    Register17; Register20; Register21; Register22; Register23;
    145    Register24; Register25; Register26; Register27; Register30;
    146    Register31; Register32; Register33; Register34; Register35;
    147    Register36; Register37].
     132   RegisterSPL; RegisterSPH; RegisterST0; RegisterST1 ].
     133(* all registers, as in fact interference with forbidden registers will
     134   disallow use of them for allocation *)
     135definition RegistersAllocatable ≝ Registers.
Note: See TracChangeset for help on using the changeset viewer.