source: src/ASM/I8051.ma @ 1600

Last change on this file since 1600 was 1600, checked in by sacerdot, 8 years ago

utilities and ASM ported to the new standard library

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