source: src/ASM/I8051.ma @ 1515

Last change on this file since 1515 was 1515, checked in by campbell, 10 years ago

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
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".
9include "ASM/BitVectorTrie.ma".
10
11definition int_size ≝ bitvector_of_nat 8 1.
12definition ptr_size ≝ bitvector_of_nat 8 2.
13definition alignment ≝ None.
14
15(* dpm: Can these two inductive definitions be merged? In LIN, yes, but perhaps
16        not further back in the translation chain.                            *)
17inductive OpAccs: Type[0] ≝
18  Mul: OpAccs
19| DivuModu: OpAccs.
20
21inductive Op1: Type[0] ≝
22  Cmpl: Op1
23| Inc: Op1.
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 compare_register: Register → Register → compare ≝
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      match eqb r_as_nat s_as_nat with
126      [ true ⇒ compare_equal
127      | false ⇒
128        match ltb r_as_nat s_as_nat with
129        [ true ⇒ compare_less
130        | false ⇒ compare_greater
131        ]
132      ].
133
134definition eq_Register: Register → Register → bool ≝
135  λr, s: Register.
136  let r_as_nat ≝ nat_of_register r in
137  let s_as_nat ≝ nat_of_register s in
138    eqb r_as_nat s_as_nat.
139
140axiom print_register: Register → String.
141
142(* dpm: registers for stack manipulation *)
143definition RegisterSST ≝ Register10.
144definition RegisterST0 ≝ Register02.
145definition RegisterST1 ≝ Register03.
146definition RegisterST2 ≝ Register04.
147definition RegisterST3 ≝ Register05.
148definition RegisterSTS ≝ [RegisterST0; RegisterST1; RegisterST2; RegisterST3].
149definition RegisterSPL ≝ Register06.
150definition RegisterSPH ≝ Register07.
151definition RegisterParams: list Register ≝
152  [ Register30; Register31; Register32; Register33;
153    Register34; Register35; Register36; Register37 ].
154definition Registers ≝
155  [Register00; Register01; Register02; Register03; Register04;
156   Register05; Register06; Register07; Register10; Register11;
157   Register12; Register13; Register14; Register15; Register16;
158   Register17; Register20; Register21; Register22; Register23;
159   Register24; Register25; Register26; Register27; Register30;
160   Register31; Register32; Register33; Register34; Register35;
161   Register36; Register37; RegisterA; RegisterB; RegisterDPL;
162   RegisterDPH; RegisterSPL; RegisterSPH; RegisterST0; RegisterST1;
163   RegisterSST].
164definition RegisterRets ≝ [RegisterDPL; RegisterDPH; Register00; Register01].
165definition RegisterCallerSaved ≝
166  [Register00; Register01; Register02; Register03; Register04;
167   Register05; Register06; Register07; Register10; Register11;
168   Register12; Register13; Register14; Register15; Register16;
169   Register17; Register30; Register31; Register32; Register33;
170   Register34; Register35; Register36; Register37].
171definition RegisterCalleeSaved ≝
172  [Register20; Register21; Register22; Register23; Register24;
173   Register25; Register26; Register27].
174definition RegistersForbidden ≝
175  [RegisterA; RegisterB; RegisterDPL; RegisterDPH;
176   RegisterSPL; RegisterSPH; RegisterST0; RegisterST1;
177   RegisterST2; RegisterST3; RegisterSST].
178(* registers minus forbidden *)
179definition RegistersAllocatable ≝
180  [Register00; Register01; Register02; Register03; Register04;
181   Register05; Register06; Register07; Register10; Register11;
182   Register12; Register13; Register14; Register15; Register16;
183   Register17; Register20; Register21; Register22; Register23;
184   Register24; Register25; Register26; Register27; Register30;
185   Register31; Register32; Register33; Register34; Register35;
186   Register36; Register37].
187
188definition register_address: Register → [[ acc_a; direct; registr ]] ≝
189  λr: Register.
190    match r with
191    [ Register00 ⇒ REGISTER [[ false; false; false ]]
192    | Register01 ⇒ REGISTER [[ false; false; true ]]
193    | Register02 ⇒ REGISTER [[ false; true; false ]]
194    | Register03 ⇒ REGISTER [[ false; true; true ]]
195    | Register04 ⇒ REGISTER [[ true; false; false ]]
196    | Register05 ⇒ REGISTER [[ true; false; true ]]
197    | Register06 ⇒ REGISTER [[ true; true; false ]]
198    | Register07 ⇒ REGISTER [[ true; true; true ]]
199    | RegisterA ⇒ ACC_A
200    | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240)
201    | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82)
202    | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83)
203    | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r))
204    ].
205    [*: normalize
206        @ I
207    ]
208qed.
209
210definition hw_register_env ≝ BitVectorTrie beval 6.
211definition empty_hw_register_env: hw_register_env ≝ Stub ….
212definition hwreg_retrieve: hw_register_env → Register → beval ≝
213 λenv,r. lookup … (bitvector_of_register r) env BVundef.
214definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
215 λr,v,env. insert … (bitvector_of_register r) v env.
216 
217record Eval: Type[0] ≝
218{
219  opaccs: OpAccs → Byte → Byte → Byte × Byte;
220  op1: Op1 → Byte → Byte;
221  op2: Bit → Op2 → Byte → Byte → (Byte × Bit)
222}.
223
224axiom opaccs_implementation: OpAccs → Byte → Byte → Byte × Byte.
225axiom op1_implementation: Op1 → Byte → Byte.
226axiom op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit).
227
228definition eval: Eval ≝
229  mk_Eval opaccs_implementation
230          op1_implementation
231          op2_implementation.
Note: See TracBrowser for help on using the repository browser.