source: src/ASM/I8051.ma @ 2327

Last change on this file since 2327 was 2286, checked in by tranquil, 7 years ago

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

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