source: src/ASM/I8051.ma @ 2714

Last change on this file since 2714 was 2645, checked in by sacerdot, 7 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 4.6 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 RegisterSST ≝ Register10.
105definition RegisterST0 ≝ Register02.
106definition RegisterST1 ≝ Register03.
107definition RegisterST2 ≝ Register04.
108definition RegisterST3 ≝ Register05.
109definition RegisterSTS ≝ [RegisterST0; RegisterST1; RegisterST2; RegisterST3].
110definition RegisterSPL ≝ Register06.
111definition RegisterSPH ≝ Register07.
112definition RegisterParams: list Register ≝
113  [ Register30; Register31; Register32; Register33;
114    Register34; Register35; Register36; Register37 ].
115definition Registers ≝
116  [Register00; Register01; Register02; Register03; Register04;
117   Register05; Register06; Register07; Register10; Register11;
118   Register12; Register13; Register14; Register15; Register16;
119   Register17; Register20; Register21; Register22; Register23;
120   Register24; Register25; Register26; Register27; Register30;
121   Register31; Register32; Register33; Register34; Register35;
122   Register36; Register37; RegisterA; RegisterB; RegisterDPL;
123   RegisterDPH; RegisterSPL; RegisterSPH; RegisterST0; RegisterST1;
124   RegisterSST].
125definition RegisterRets ≝ [RegisterDPL; RegisterDPH; Register00; Register01].
126definition RegisterCallerSaved ≝
127  [Register00; Register01; Register02; Register03; Register04;
128   Register05; Register06; Register07; Register10; Register11;
129   Register12; Register13; Register14; Register15; Register16;
130   Register17; Register30; Register31; Register32; Register33;
131   Register34; Register35; Register36; Register37].
132definition RegisterCalleeSaved ≝
133  [Register20; Register21; Register22; Register23; Register24;
134   Register25; Register26; Register27].
135definition RegistersForbidden ≝
136  [RegisterA; RegisterB; RegisterDPL; RegisterDPH;
137   RegisterSPL; RegisterSPH; RegisterST0; RegisterST1;
138   RegisterST2; RegisterST3; RegisterSST].
139(* registers minus forbidden *)
140definition 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].
Note: See TracBrowser for help on using the repository browser.