source: src/ASM/I8051.ma @ 2270

Last change on this file since 2270 was 1987, checked in by campbell, 8 years ago

Move BEValues to common to reflect their use in the memory model for
everything.

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