source: src/ASM/I8051.ma

Last change on this file was 3255, checked in by tranquil, 7 years ago
  • 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 size: 4.0 KB
Line 
1include "arithmetics/nat.ma".
2include "basics/jmeq.ma".
3include "ASM/Arithmetic.ma". 
4
5definition int_size ≝ bitvector_of_nat 8 1.
6definition ptr_size ≝ bitvector_of_nat 8 2.
7definition alignment ≝ None.
8
9(* dpm: maybe useless? *)
10inductive Register: Type[0] ≝
11  Register00: Register
12| Register01: Register
13| Register02: Register
14| Register03: Register
15| Register04: Register
16| Register05: Register
17| Register06: Register
18| Register07: Register
19| Register10: Register
20| Register11: Register
21| Register12: Register
22| Register13: Register
23| Register14: Register
24| Register15: Register
25| Register16: Register
26| Register17: Register
27| Register20: Register
28| Register21: Register
29| Register22: Register
30| Register23: Register
31| Register24: Register
32| Register25: Register
33| Register26: Register
34| Register27: Register
35| Register30: Register
36| Register31: Register
37| Register32: Register
38| Register33: Register
39| Register34: Register
40| Register35: Register
41| Register36: Register
42| Register37: Register
43| RegisterA: Register
44| RegisterB: Register
45| RegisterDPL: Register
46| RegisterDPH: Register
47| RegisterCarry: Register.
48
49definition nat_of_register: Register → nat ≝
50  λr: Register.
51  match r with
52  [ Register00 ⇒ 0
53  | Register01 ⇒ 1
54  | Register02 ⇒ 2
55  | Register03 ⇒ 3
56  | Register04 ⇒ 4
57  | Register05 ⇒ 5
58  | Register06 ⇒ 6
59  | Register07 ⇒ 7
60  | Register10 ⇒ 8
61  | Register11 ⇒ 9
62  | Register12 ⇒ 10
63  | Register13 ⇒ 11
64  | Register14 ⇒ 12
65  | Register15 ⇒ 13
66  | Register16 ⇒ 14
67  | Register17 ⇒ 15
68  | Register20 ⇒ 16
69  | Register21 ⇒ 17
70  | Register22 ⇒ 18
71  | Register23 ⇒ 19
72  | Register24 ⇒ 20
73  | Register25 ⇒ 21
74  | Register26 ⇒ 22
75  | Register27 ⇒ 23
76  | Register30 ⇒ 24
77  | Register31 ⇒ 25
78  | Register32 ⇒ 26
79  | Register33 ⇒ 27
80  | Register34 ⇒ 28
81  | Register35 ⇒ 29
82  | Register36 ⇒ 30
83  | Register37 ⇒ 31
84  | RegisterA ⇒ 32
85  | RegisterB ⇒ 33
86  | RegisterDPL ⇒ 34
87  | RegisterDPH ⇒ 35
88  | RegisterCarry ⇒ 36 (* was -1, increment as needed *)
89  ].
90 
91definition physical_register_count ≝ 36.
92
93definition bitvector_of_register: Register → BitVector 6 ≝
94  λregister.
95    bitvector_of_nat ? (nat_of_register register).
96
97definition eq_Register: Register → Register → bool ≝
98  λr, s: Register.
99  let r_as_nat ≝ nat_of_register r in
100  let s_as_nat ≝ nat_of_register s in
101    eqb r_as_nat s_as_nat.
102
103(* dpm: registers for stack manipulation *)
104definition RegisterRets ≝ [Register00; Register01; Register02; Register03 ].
105definition RegisterST0 ≝ Register04.
106definition RegisterST1 ≝ Register05.
107definition RegisterSPL ≝ Register06.
108definition RegisterSPH ≝ Register07.
109definition RegisterParams: list Register ≝
110  [ Register30; Register31; Register32; Register33;
111    Register34; Register35; Register36; Register37 ].
112definition Registers ≝
113  [Register00; Register01; Register02; Register03; Register04;
114   Register05; Register06; Register07; Register10; Register11;
115   Register12; Register13; Register14; Register15; Register16;
116   Register17; Register20; Register21; Register22; Register23;
117   Register24; Register25; Register26; Register27; Register30;
118   Register31; Register32; Register33; Register34; Register35;
119   Register36; Register37; RegisterA; RegisterB; RegisterDPL;
120   RegisterDPH ].
121definition RegisterCallerSaved ≝
122  [Register00; Register01; Register02; Register03; Register04;
123   Register05; Register06; Register07; Register10; Register11;
124   Register12; Register13; Register14; Register15; Register16;
125   Register17; Register30; Register31; Register32; Register33;
126   Register34; Register35; Register36; Register37].
127definition RegisterCalleeSaved ≝
128  [Register20; Register21; Register22; Register23; Register24;
129   Register25; Register26; Register27].
130definition RegistersForbidden ≝
131  [RegisterA; RegisterB; RegisterDPL; RegisterDPH;
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 TracBrowser for help on using the repository browser.