source: src/ASM/I8051.ma @ 1489

Last change on this file since 1489 was 1416, checked in by sacerdot, 9 years ago

Maps from hardware registers to beval now implemented in ASM/I8051 (in place
of the old huge implementation to Bytes).

File size: 7.2 KB
Line 
1include "arithmetics/nat.ma".
2include "basics/jmeq.ma".
3
4include "ASM/String.ma".
5include "ASM/ASM.ma".
6include "ASM/Arithmetic.ma".
7include "utilities/Compare.ma".
8include "joint/BEValues.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 compare_register: Register → Register → compare ≝
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      match eqb r_as_nat s_as_nat with
125      [ true ⇒ compare_equal
126      | false ⇒
127        match ltb r_as_nat s_as_nat with
128        [ true ⇒ compare_less
129        | false ⇒ compare_greater
130        ]
131      ].
132
133definition eq_Register: Register → Register → bool ≝
134  λr, s: Register.
135  let r_as_nat ≝ nat_of_register r in
136  let s_as_nat ≝ nat_of_register s in
137    eqb r_as_nat s_as_nat.
138
139axiom print_register: Register → String.
140
141(* dpm: registers for stack manipulation *)
142definition RegisterSST ≝ Register10.
143definition RegisterST0 ≝ Register02.
144definition RegisterST1 ≝ Register03.
145definition RegisterST2 ≝ Register04.
146definition RegisterST3 ≝ Register05.
147definition RegisterSTS ≝ [RegisterST0; RegisterST1; RegisterST2; RegisterST3].
148definition RegisterSPL ≝ Register06.
149definition RegisterSPH ≝ Register07.
150definition RegisterParams: list Register ≝
151  [ Register30; Register31; Register32; Register33;
152    Register34; Register35; Register36; Register37 ].
153definition Registers ≝
154  [Register00; Register01; Register02; Register03; Register04;
155   Register05; Register06; Register07; Register10; Register11;
156   Register12; Register13; Register14; Register15; Register16;
157   Register17; Register20; Register21; Register22; Register23;
158   Register24; Register25; Register26; Register27; Register30;
159   Register31; Register32; Register33; Register34; Register35;
160   Register36; Register37; RegisterA; RegisterB; RegisterDPL;
161   RegisterDPH; RegisterSPL; RegisterSPH; RegisterST0; RegisterST1;
162   RegisterSST].
163definition RegisterRets ≝ [RegisterDPL; RegisterDPH; Register00; Register01].
164definition RegisterCallerSaved ≝
165  [Register00; Register01; Register02; Register03; Register04;
166   Register05; Register06; Register07; Register10; Register11;
167   Register12; Register13; Register14; Register15; Register16;
168   Register17; Register30; Register31; Register32; Register33;
169   Register34; Register35; Register36; Register37].
170definition RegisterCalleeSaved ≝
171  [Register20; Register21; Register22; Register23; Register24;
172   Register25; Register26; Register27].
173definition RegistersForbidden ≝
174  [RegisterA; RegisterB; RegisterDPL; RegisterDPH;
175   RegisterSPL; RegisterSPH; RegisterST0; RegisterST1;
176   RegisterST2; RegisterST3; RegisterSST].
177(* registers minus forbidden *)
178definition RegistersAllocatable ≝
179  [Register00; Register01; Register02; Register03; Register04;
180   Register05; Register06; Register07; Register10; Register11;
181   Register12; Register13; Register14; Register15; Register16;
182   Register17; Register20; Register21; Register22; Register23;
183   Register24; Register25; Register26; Register27; Register30;
184   Register31; Register32; Register33; Register34; Register35;
185   Register36; Register37].
186
187definition register_address: Register → [[ acc_a; direct; registr ]] ≝
188  λr: Register.
189    match r with
190    [ Register00 ⇒ REGISTER [[ false; false; false ]]
191    | Register01 ⇒ REGISTER [[ false; false; true ]]
192    | Register02 ⇒ REGISTER [[ false; true; false ]]
193    | Register03 ⇒ REGISTER [[ false; true; true ]]
194    | Register04 ⇒ REGISTER [[ true; false; false ]]
195    | Register05 ⇒ REGISTER [[ true; false; true ]]
196    | Register06 ⇒ REGISTER [[ true; true; false ]]
197    | Register07 ⇒ REGISTER [[ true; true; true ]]
198    | RegisterA ⇒ ACC_A
199    | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240)
200    | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82)
201    | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83)
202    | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r))
203    ].
204    [*: normalize
205        @ I
206    ]
207qed.
208
209definition hw_register_env ≝ BitVectorTrie beval 6.
210definition empty_hw_register_env: hw_register_env ≝ Stub ….
211definition hwreg_retrieve: hw_register_env → Register → beval ≝
212 λenv,r. lookup … (bitvector_of_register r) env BVundef.
213definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
214 λr,v,env. insert … (bitvector_of_register r) v env.
215 
216record Eval: Type[0] ≝
217{
218  opaccs: OpAccs → Byte → Byte → Byte × Byte;
219  op1: Op1 → Byte → Byte;
220  op2: Bit → Op2 → Byte → Byte → (Byte × Bit)
221}.
222
223axiom opaccs_implementation: OpAccs → Byte → Byte → Byte × Byte.
224axiom op1_implementation: Op1 → Byte → Byte.
225axiom op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit).
226
227definition eval: Eval ≝
228  mk_Eval opaccs_implementation
229          op1_implementation
230          op2_implementation.
Note: See TracBrowser for help on using the repository browser.