source: src/ASM/I8051.ma @ 2276

Last change on this file since 2276 was 2275, checked in by tranquil, 7 years ago
  • moved around some code (I8051.ma does not depend on ByteValues?.ma anymore, rather the other way around)
  • proposed reimplementation of beval with pointer arithmetics and stuff
File size: 6.4 KB
Line 
1include "arithmetics/nat.ma".
2include "basics/jmeq.ma".
3
4include "ASM/String.ma".
5include "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: Can these two inductive definitions be merged? In LIN, yes, but perhaps
13        not further back in the translation chain.                            *)
14inductive OpAccs: Type[0] ≝
15  Mul: OpAccs
16| DivuModu: OpAccs.
17
18inductive Op1: Type[0] ≝
19  Cmpl: Op1
20| Inc: Op1
21| Rl: Op1. (* TODO: implement left rotation *)
22
23inductive Op2: Type[0] ≝
24  Add: Op2
25| Addc: Op2
26| Sub: Op2
27| And: Op2
28| Or: Op2
29| Xor: Op2.
30
31(* dpm: maybe useless? *)
32inductive Register: Type[0] ≝
33  Register00: Register
34| Register01: Register
35| Register02: Register
36| Register03: Register
37| Register04: Register
38| Register05: Register
39| Register06: Register
40| Register07: Register
41| Register10: Register
42| Register11: Register
43| Register12: Register
44| Register13: Register
45| Register14: Register
46| Register15: Register
47| Register16: Register
48| Register17: Register
49| Register20: Register
50| Register21: Register
51| Register22: Register
52| Register23: Register
53| Register24: Register
54| Register25: Register
55| Register26: Register
56| Register27: Register
57| Register30: Register
58| Register31: Register
59| Register32: Register
60| Register33: Register
61| Register34: Register
62| Register35: Register
63| Register36: Register
64| Register37: Register
65| RegisterA: Register
66| RegisterB: Register
67| RegisterDPL: Register
68| RegisterDPH: Register
69| RegisterCarry: Register.
70
71definition nat_of_register: Register → nat ≝
72  λr: Register.
73  match r with
74  [ Register00 ⇒ 0
75  | Register01 ⇒ 1
76  | Register02 ⇒ 2
77  | Register03 ⇒ 3
78  | Register04 ⇒ 4
79  | Register05 ⇒ 5
80  | Register06 ⇒ 6
81  | Register07 ⇒ 7
82  | Register10 ⇒ 8
83  | Register11 ⇒ 9
84  | Register12 ⇒ 10
85  | Register13 ⇒ 11
86  | Register14 ⇒ 12
87  | Register15 ⇒ 13
88  | Register16 ⇒ 14
89  | Register17 ⇒ 15
90  | Register20 ⇒ 16
91  | Register21 ⇒ 17
92  | Register22 ⇒ 18
93  | Register23 ⇒ 19
94  | Register24 ⇒ 20
95  | Register25 ⇒ 21
96  | Register26 ⇒ 22
97  | Register27 ⇒ 23
98  | Register30 ⇒ 24
99  | Register31 ⇒ 25
100  | Register32 ⇒ 26
101  | Register33 ⇒ 27
102  | Register34 ⇒ 28
103  | Register35 ⇒ 29
104  | Register36 ⇒ 30
105  | Register37 ⇒ 31
106  | RegisterA ⇒ 32
107  | RegisterB ⇒ 33
108  | RegisterDPL ⇒ 34
109  | RegisterDPH ⇒ 35
110  | RegisterCarry ⇒ 36 (* was -1, increment as needed *)
111  ].
112 
113definition physical_register_count ≝ 36.
114
115definition bitvector_of_register: Register → BitVector 6 ≝
116  λregister.
117    bitvector_of_nat ? (nat_of_register register).
118
119definition eq_Register: Register → Register → bool ≝
120  λr, s: Register.
121  let r_as_nat ≝ nat_of_register r in
122  let s_as_nat ≝ nat_of_register s in
123    eqb r_as_nat s_as_nat.
124
125axiom print_register: Register → String.
126
127(* dpm: registers for stack manipulation *)
128definition RegisterSST ≝ Register10.
129definition RegisterST0 ≝ Register02.
130definition RegisterST1 ≝ Register03.
131definition RegisterST2 ≝ Register04.
132definition RegisterST3 ≝ Register05.
133definition RegisterSTS ≝ [RegisterST0; RegisterST1; RegisterST2; RegisterST3].
134definition RegisterSPL ≝ Register06.
135definition RegisterSPH ≝ Register07.
136definition RegisterParams: list Register ≝
137  [ Register30; Register31; Register32; Register33;
138    Register34; Register35; Register36; Register37 ].
139definition Registers ≝
140  [Register00; Register01; Register02; Register03; Register04;
141   Register05; Register06; Register07; Register10; Register11;
142   Register12; Register13; Register14; Register15; Register16;
143   Register17; Register20; Register21; Register22; Register23;
144   Register24; Register25; Register26; Register27; Register30;
145   Register31; Register32; Register33; Register34; Register35;
146   Register36; Register37; RegisterA; RegisterB; RegisterDPL;
147   RegisterDPH; RegisterSPL; RegisterSPH; RegisterST0; RegisterST1;
148   RegisterSST].
149definition RegisterRets ≝ [RegisterDPL; RegisterDPH; Register00; Register01].
150definition RegisterCallerSaved ≝
151  [Register00; Register01; Register02; Register03; Register04;
152   Register05; Register06; Register07; Register10; Register11;
153   Register12; Register13; Register14; Register15; Register16;
154   Register17; Register30; Register31; Register32; Register33;
155   Register34; Register35; Register36; Register37].
156definition RegisterCalleeSaved ≝
157  [Register20; Register21; Register22; Register23; Register24;
158   Register25; Register26; Register27].
159definition RegistersForbidden ≝
160  [RegisterA; RegisterB; RegisterDPL; RegisterDPH;
161   RegisterSPL; RegisterSPH; RegisterST0; RegisterST1;
162   RegisterST2; RegisterST3; RegisterSST].
163(* registers minus forbidden *)
164definition RegistersAllocatable ≝
165  [Register00; Register01; Register02; Register03; Register04;
166   Register05; Register06; Register07; Register10; Register11;
167   Register12; Register13; Register14; Register15; Register16;
168   Register17; Register20; Register21; Register22; Register23;
169   Register24; Register25; Register26; Register27; Register30;
170   Register31; Register32; Register33; Register34; Register35;
171   Register36; Register37].
172
173definition register_address: Register → [[ acc_a; direct; registr ]] ≝
174  λr: Register.
175    match r with
176    [ Register00 ⇒ REGISTER [[ false; false; false ]]
177    | Register01 ⇒ REGISTER [[ false; false; true ]]
178    | Register02 ⇒ REGISTER [[ false; true; false ]]
179    | Register03 ⇒ REGISTER [[ false; true; true ]]
180    | Register04 ⇒ REGISTER [[ true; false; false ]]
181    | Register05 ⇒ REGISTER [[ true; false; true ]]
182    | Register06 ⇒ REGISTER [[ true; true; false ]]
183    | Register07 ⇒ REGISTER [[ true; true; true ]]
184    | RegisterA ⇒ ACC_A
185    | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240)
186    | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82)
187    | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83)
188    | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r))
189    ].
190    [*: normalize
191        @ I
192    ]
193qed.
194
195record Eval: Type[0] ≝
196{
197  opaccs: OpAccs → Byte → Byte → Byte × Byte;
198  op1: Op1 → Byte → Byte;
199  op2: Bit → Op2 → Byte → Byte → (Byte × Bit)
200}.
201
202axiom opaccs_implementation: OpAccs → Byte → Byte → Byte × Byte.
203axiom op1_implementation: Op1 → Byte → Byte.
204axiom op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit).
205
206definition eval: Eval ≝
207  mk_Eval opaccs_implementation
208          op1_implementation
209          op2_implementation.
Note: See TracBrowser for help on using the repository browser.