source: src/ASM/I8051.ma @ 1515

Last change on this file since 1515 was 1515, checked in by campbell, 8 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.