Context Navigation

Interpret.ma @ 1522

Last change on this file since 1522 was 1522, checked in by mulligan, 8 years ago
changes to preamble and lin to asm pass, resolved conflict in interpret
File size: 30.9 KB

Line
1	include "ASM/Status.ma".
2	include "ASM/Fetch.ma".
3
4	definition sign_extension: Byte → Word ≝
5	λc.
6	let b ≝ get_index_v ? 8 c 1 ? in
7	[[ b; b; b; b; b; b; b; b ]] @@ c.
8	normalize;
9	repeat (@ (le_S_S ?));
10	@ (le_O_n);
11	qed.
12
13	lemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b.
14	# a
15	# b
16	cases a
17	cases b
18	normalize
19	//
20	# K
21	cases (eq_true_false K)
22	qed.
23
24	lemma is_a_to_mem_to_is_in:
25	∀he,a,m,q. is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
26	# he
27	# a
28	# m
29	# q
30	elim q
31	[ normalize
32	# _
33	# K
34	assumption
35	\| # m'
36	# t
37	# q'
38	# II
39	# H1
40	# H2
41	normalize
42	change with (orb ??) in H2: (??%?);
43	cases (inclusive_disjunction_true … H2)
44	[ # K
45	< (eq_a_to_eq … K)
46	> H1
47	%
48	\| # K
49	> II
50	try assumption
51	cases (is_a t a)
52	normalize
53	%
54	]
55	]
56	qed.
57
58	lemma execute_1_technical:
59	∀n, m: nat.
60	∀v: Vector addressing_mode_tag (S n).
61	∀q: Vector addressing_mode_tag (S m).
62	∀a: addressing_mode.
63	bool_to_Prop (is_in ? v a) →
64	bool_to_Prop (subvector_with ? ? ? eq_a v q) →
65	bool_to_Prop (is_in ? q a).
66	# n
67	# m
68	# v
69	# q
70	# a
71	elim v
72	[ normalize
73	# K
74	cases K
75	\| # n'
76	# he
77	# tl
78	# II
79	whd in ⊢ (% → ? → ?);
80	lapply (refl … (is_in … (he:::tl) a))
81	cases (is_in … (he:::tl) a) in ⊢ (???% → %);
82	[ # K
83	# _
84	normalize in K;
85	whd in ⊢ (% → ?);
86	lapply (refl … (subvector_with … eq_a (he:::tl) q));
87	cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %);
88	[ # K1
89	# _
90	change with ((andb ? (subvector_with …)) = true) in K1;
91	cases (conjunction_true … K1)
92	# K3
93	# K4
94	cases (inclusive_disjunction_true … K)
95	# K2
96	[ > (is_a_to_mem_to_is_in … K2 K3)
97	%
98	\| @ II
99	[ > K2
100	%
101	\| > K4
102	%
103	]
104	]
105	\| # K1
106	# K2
107	normalize in K2;
108	cases K2;
109	]
110	\| # K1
111	# K2
112	normalize in K2;
113	cases K2
114	]
115	]
116	qed.
117
118	include alias "arithmetics/nat.ma".
119	include alias "ASM/BitVectorTrie.ma".
120
121	definition execute_1_preinstruction:
122	∀ticks: nat × nat.
123	∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → PreStatus M → PreStatus M ≝
124	λticks.
125	λA, M: Type[0].
126	λaddr_of: A → (PreStatus M) → Word.
127	λinstr: preinstruction A.
128	λs: PreStatus M.
129	let add_ticks1 ≝ λs: PreStatus M.set_clock … s (\fst ticks + clock … s) in
130	let add_ticks2 ≝ λs: PreStatus M.set_clock … s (\snd ticks + clock … s) in
131	match instr with
132	[ ADD addr1 addr2 ⇒
133	let s ≝ add_ticks1 s in
134	let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
135	(get_arg_8 ? s false addr2) false in
136	let cy_flag ≝ get_index' ? O ? flags in
137	let ac_flag ≝ get_index' ? 1 ? flags in
138	let ov_flag ≝ get_index' ? 2 ? flags in
139	let s ≝ set_arg_8 ? s ACC_A result in
140	set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
141	\| ADDC addr1 addr2 ⇒
142	let s ≝ add_ticks1 s in
143	let old_cy_flag ≝ get_cy_flag ? s in
144	let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
145	(get_arg_8 ? s false addr2) old_cy_flag in
146	let cy_flag ≝ get_index' ? O ? flags in
147	let ac_flag ≝ get_index' ? 1 ? flags in
148	let ov_flag ≝ get_index' ? 2 ? flags in
149	let s ≝ set_arg_8 ? s ACC_A result in
150	set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
151	\| SUBB addr1 addr2 ⇒
152	let s ≝ add_ticks1 s in
153	let old_cy_flag ≝ get_cy_flag ? s in
154	let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s false addr1)
155	(get_arg_8 ? s false addr2) old_cy_flag in
156	let cy_flag ≝ get_index' ? O ? flags in
157	let ac_flag ≝ get_index' ? 1 ? flags in
158	let ov_flag ≝ get_index' ? 2 ? flags in
159	let s ≝ set_arg_8 ? s ACC_A result in
160	set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
161	\| ANL addr ⇒
162	let s ≝ add_ticks1 s in
163	match addr with
164	[ inl l ⇒
165	match l with
166	[ inl l' ⇒
167	let 〈addr1, addr2〉 ≝ l' in
168	let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
169	set_arg_8 ? s addr1 and_val
170	\| inr r ⇒
171	let 〈addr1, addr2〉 ≝ r in
172	let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
173	set_arg_8 ? s addr1 and_val
174	]
175	\| inr r ⇒
176	let 〈addr1, addr2〉 ≝ r in
177	let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ? s addr2 true) in
178	set_flags ? s and_val (None ?) (get_ov_flag ? s)
179	]
180	\| ORL addr ⇒
181	let s ≝ add_ticks1 s in
182	match addr with
183	[ inl l ⇒
184	match l with
185	[ inl l' ⇒
186	let 〈addr1, addr2〉 ≝ l' in
187	let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
188	set_arg_8 ? s addr1 or_val
189	\| inr r ⇒
190	let 〈addr1, addr2〉 ≝ r in
191	let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
192	set_arg_8 ? s addr1 or_val
193	]
194	\| inr r ⇒
195	let 〈addr1, addr2〉 ≝ r in
196	let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ? s addr2 true) in
197	set_flags ? s or_val (None ?) (get_ov_flag ? s)
198	]
199	\| XRL addr ⇒
200	let s ≝ add_ticks1 s in
201	match addr with
202	[ inl l' ⇒
203	let 〈addr1, addr2〉 ≝ l' in
204	let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
205	set_arg_8 ? s addr1 xor_val
206	\| inr r ⇒
207	let 〈addr1, addr2〉 ≝ r in
208	let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
209	set_arg_8 ? s addr1 xor_val
210	]
211	\| INC addr ⇒
212	let s ≝ add_ticks1 s in
213	match addr return λx. bool_to_Prop (is_in … [[ acc_a;
214	registr;
215	direct;
216	indirect;
217	dptr ]] x) → ? with
218	[ ACC_A ⇒ λacc_a: True.
219	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true ACC_A) (bitvector_of_nat 8 1) in
220	set_arg_8 ? s ACC_A result
221	\| REGISTER r ⇒ λregister: True.
222	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (REGISTER r)) (bitvector_of_nat 8 1) in
223	set_arg_8 ? s (REGISTER r) result
224	\| DIRECT d ⇒ λdirect: True.
225	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (DIRECT d)) (bitvector_of_nat 8 1) in
226	set_arg_8 ? s (DIRECT d) result
227	\| INDIRECT i ⇒ λindirect: True.
228	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (INDIRECT i)) (bitvector_of_nat 8 1) in
229	set_arg_8 ? s (INDIRECT i) result
230	\| DPTR ⇒ λdptr: True.
231	let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ? s SFR_DPL) (bitvector_of_nat 8 1) in
232	let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s SFR_DPH) (zero 8) carry in
233	let s ≝ set_8051_sfr ? s SFR_DPL bl in
234	set_8051_sfr ? s SFR_DPH bu
235	\| _ ⇒ λother: False. ⊥
236	] (subaddressing_modein … addr)
237	\| DEC addr ⇒
238	let s ≝ add_ticks1 s in
239	let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in
240	set_arg_8 ? s addr result
241	\| MUL addr1 addr2 ⇒
242	let s ≝ add_ticks1 s in
243	let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
244	let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
245	let product ≝ acc_a_nat * acc_b_nat in
246	let ov_flag ≝ product ≥ 256 in
247	let low ≝ bitvector_of_nat 8 (product mod 256) in
248	let high ≝ bitvector_of_nat 8 (product ÷ 256) in
249	let s ≝ set_8051_sfr ? s SFR_ACC_A low in
250	set_8051_sfr ? s SFR_ACC_B high
251	\| DIV addr1 addr2 ⇒
252	let s ≝ add_ticks1 s in
253	let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
254	let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
255	match acc_b_nat with
256	[ O ⇒ set_flags ? s false (None Bit) true
257	\| S o ⇒
258	let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
259	let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
260	let s ≝ set_8051_sfr ? s SFR_ACC_A q in
261	let s ≝ set_8051_sfr ? s SFR_ACC_B r in
262	set_flags ? s false (None Bit) false
263	]
264	\| DA addr ⇒
265	let s ≝ add_ticks1 s in
266	let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in
267	if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ? s) then
268	let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr ? s SFR_ACC_A) (bitvector_of_nat 8 6) false in
269	let cy_flag ≝ get_index' ? O ? flags in
270	let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
271	if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
272	let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
273	let new_acc ≝ nu @@ acc_nl' in
274	let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
275	set_flags ? s cy_flag (Some ? (get_ac_flag ? s)) (get_ov_flag ? s)
276	else
277	s
278	else
279	s
280	\| CLR addr ⇒
281	let s ≝ add_ticks1 s in
282	match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
283	[ ACC_A ⇒ λacc_a: True. set_arg_8 ? s ACC_A (zero 8)
284	\| CARRY ⇒ λcarry: True. set_arg_1 ? s CARRY false
285	\| BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 ? s (BIT_ADDR b) false
286	\| _ ⇒ λother: False. ⊥
287	] (subaddressing_modein … addr)
288	\| CPL addr ⇒
289	let s ≝ add_ticks1 s in
290	match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
291	[ ACC_A ⇒ λacc_a: True.
292	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
293	let new_acc ≝ negation_bv ? old_acc in
294	set_8051_sfr ? s SFR_ACC_A new_acc
295	\| CARRY ⇒ λcarry: True.
296	let old_cy_flag ≝ get_arg_1 ? s CARRY true in
297	let new_cy_flag ≝ ¬old_cy_flag in
298	set_arg_1 ? s CARRY new_cy_flag
299	\| BIT_ADDR b ⇒ λbit_addr: True.
300	let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in
301	let new_bit ≝ ¬old_bit in
302	set_arg_1 ? s (BIT_ADDR b) new_bit
303	\| _ ⇒ λother: False. ?
304	] (subaddressing_modein … addr)
305	\| SETB b ⇒
306	let s ≝ add_ticks1 s in
307	set_arg_1 ? s b false
308	\| RL _ ⇒ (* DPM: always ACC_A *)
309	let s ≝ add_ticks1 s in
310	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
311	let new_acc ≝ rotate_left … 1 old_acc in
312	set_8051_sfr ? s SFR_ACC_A new_acc
313	\| RR _ ⇒ (* DPM: always ACC_A *)
314	let s ≝ add_ticks1 s in
315	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
316	let new_acc ≝ rotate_right … 1 old_acc in
317	set_8051_sfr ? s SFR_ACC_A new_acc
318	\| RLC _ ⇒ (* DPM: always ACC_A *)
319	let s ≝ add_ticks1 s in
320	let old_cy_flag ≝ get_cy_flag ? s in
321	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
322	let new_cy_flag ≝ get_index' ? O ? old_acc in
323	let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
324	let s ≝ set_arg_1 ? s CARRY new_cy_flag in
325	set_8051_sfr ? s SFR_ACC_A new_acc
326	\| RRC _ ⇒ (* DPM: always ACC_A *)
327	let s ≝ add_ticks1 s in
328	let old_cy_flag ≝ get_cy_flag ? s in
329	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
330	let new_cy_flag ≝ get_index' ? 7 ? old_acc in
331	let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
332	let s ≝ set_arg_1 ? s CARRY new_cy_flag in
333	set_8051_sfr ? s SFR_ACC_A new_acc
334	\| SWAP _ ⇒ (* DPM: always ACC_A *)
335	let s ≝ add_ticks1 s in
336	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
337	let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
338	let new_acc ≝ nl @@ nu in
339	set_8051_sfr ? s SFR_ACC_A new_acc
340	\| PUSH addr ⇒
341	let s ≝ add_ticks1 s in
342	match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
343	[ DIRECT d ⇒ λdirect: True.
344	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
345	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
346	write_at_stack_pointer ? s d
347	\| _ ⇒ λother: False. ⊥
348	] (subaddressing_modein … addr)
349	\| POP addr ⇒
350	let s ≝ add_ticks1 s in
351	let contents ≝ read_at_stack_pointer ? s in
352	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
353	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
354	set_arg_8 ? s addr contents
355	\| XCH addr1 addr2 ⇒
356	let s ≝ add_ticks1 s in
357	let old_addr ≝ get_arg_8 ? s false addr2 in
358	let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
359	let s ≝ set_8051_sfr ? s SFR_ACC_A old_addr in
360	set_arg_8 ? s addr2 old_acc
361	\| XCHD addr1 addr2 ⇒
362	let s ≝ add_ticks1 s in
363	let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_ACC_A) in
364	let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 ? s false addr2) in
365	let new_acc ≝ acc_nu @@ arg_nl in
366	let new_arg ≝ arg_nu @@ acc_nl in
367	let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
368	set_arg_8 ? s addr2 new_arg
369	\| RET ⇒
370	let s ≝ add_ticks1 s in
371	let high_bits ≝ read_at_stack_pointer ? s in
372	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
373	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
374	let low_bits ≝ read_at_stack_pointer ? s in
375	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
376	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
377	let new_pc ≝ high_bits @@ low_bits in
378	set_program_counter ? s new_pc
379	\| RETI ⇒
380	let s ≝ add_ticks1 s in
381	let high_bits ≝ read_at_stack_pointer ? s in
382	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
383	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
384	let low_bits ≝ read_at_stack_pointer ? s in
385	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
386	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
387	let new_pc ≝ high_bits @@ low_bits in
388	set_program_counter ? s new_pc
389	\| MOVX addr ⇒
390	let s ≝ add_ticks1 s in
391	(* DPM: only copies --- doesn't affect I/O *)
392	match addr with
393	[ inl l ⇒
394	let 〈addr1, addr2〉 ≝ l in
395	set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
396	\| inr r ⇒
397	let 〈addr1, addr2〉 ≝ r in
398	set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
399	]
400	\| MOV addr ⇒
401	let s ≝ add_ticks1 s in
402	match addr with
403	[ inl l ⇒
404	match l with
405	[ inl l' ⇒
406	match l' with
407	[ inl l'' ⇒
408	match l'' with
409	[ inl l''' ⇒
410	match l''' with
411	[ inl l'''' ⇒
412	let 〈addr1, addr2〉 ≝ l'''' in
413	set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
414	\| inr r'''' ⇒
415	let 〈addr1, addr2〉 ≝ r'''' in
416	set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
417	]
418	\| inr r''' ⇒
419	let 〈addr1, addr2〉 ≝ r''' in
420	set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
421	]
422	\| inr r'' ⇒
423	let 〈addr1, addr2〉 ≝ r'' in
424	set_arg_16 ? s (get_arg_16 ? s addr2) addr1
425	]
426	\| inr r ⇒
427	let 〈addr1, addr2〉 ≝ r in
428	set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
429	]
430	\| inr r ⇒
431	let 〈addr1, addr2〉 ≝ r in
432	set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
433	]
434	\| JC addr ⇒
435	if get_cy_flag ? s then
436	let s ≝ add_ticks1 s in
437	set_program_counter ? s (addr_of addr s)
438	else
439	let s ≝ add_ticks2 s in
440	s
441	\| JNC addr ⇒
442	if ¬(get_cy_flag ? s) then
443	let s ≝ add_ticks1 s in
444	set_program_counter ? s (addr_of addr s)
445	else
446	let s ≝ add_ticks2 s in
447	s
448	\| JB addr1 addr2 ⇒
449	if get_arg_1 ? s addr1 false then
450	let s ≝ add_ticks1 s in
451	set_program_counter ? s (addr_of addr2 s)
452	else
453	let s ≝ add_ticks2 s in
454	s
455	\| JNB addr1 addr2 ⇒
456	if ¬(get_arg_1 ? s addr1 false) then
457	let s ≝ add_ticks1 s in
458	set_program_counter ? s (addr_of addr2 s)
459	else
460	let s ≝ add_ticks2 s in
461	s
462	\| JBC addr1 addr2 ⇒
463	let s ≝ set_arg_1 ? s addr1 false in
464	if get_arg_1 ? s addr1 false then
465	let s ≝ add_ticks1 s in
466	set_program_counter ? s (addr_of addr2 s)
467	else
468	let s ≝ add_ticks2 s in
469	s
470	\| JZ addr ⇒
471	if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then
472	let s ≝ add_ticks1 s in
473	set_program_counter ? s (addr_of addr s)
474	else
475	let s ≝ add_ticks2 s in
476	s
477	\| JNZ addr ⇒
478	if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then
479	let s ≝ add_ticks1 s in
480	set_program_counter ? s (addr_of addr s)
481	else
482	let s ≝ add_ticks2 s in
483	s
484	\| CJNE addr1 addr2 ⇒
485	match addr1 with
486	[ inl l ⇒
487	let 〈addr1, addr2'〉 ≝ l in
488	let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
489	(nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
490	if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
491	let s ≝ add_ticks1 s in
492	let s ≝ set_program_counter ? s (addr_of addr2 s) in
493	set_flags ? s new_cy (None ?) (get_ov_flag ? s)
494	else
495	let s ≝ add_ticks2 s in
496	(set_flags ? s new_cy (None ?) (get_ov_flag ? s))
497	\| inr r' ⇒
498	let 〈addr1, addr2'〉 ≝ r' in
499	let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
500	(nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
501	if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
502	let s ≝ add_ticks1 s in
503	let s ≝ set_program_counter ? s (addr_of addr2 s) in
504	set_flags ? s new_cy (None ?) (get_ov_flag ? s)
505	else
506	let s ≝ add_ticks2 s in
507	(set_flags ? s new_cy (None ?) (get_ov_flag ? s))
508	]
509	\| DJNZ addr1 addr2 ⇒
510	let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr1) (bitvector_of_nat 8 1) false in
511	let s ≝ set_arg_8 ? s addr1 result in
512	if ¬(eq_bv ? result (zero 8)) then
513	let s ≝ add_ticks1 s in
514	set_program_counter ? s (addr_of addr2 s)
515	else
516	let s ≝ add_ticks2 s in
517	s
518	\| NOP ⇒
519	let s ≝ add_ticks2 s in
520	s
521	].
522	try assumption
523	try @I
524	try (
525	@ (execute_1_technical … (subaddressing_modein …))
526	@ I
527	)
528	qed.
529
530	include "ASM/JMCoercions.ma".
531
532	definition execute_1_0: ∀s: Status. instruction × Word × nat → Σs': Status. clock … s ≤ clock … s' ≝
533	λs,instr_pc_ticks.
534	let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
535	let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
536	let s ≝ set_program_counter ? s pc in
537	let s ≝
538	match instr with
539	[ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks,ticks〉 [[ relative ]] ?
540	(λx. λs.
541	match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
542	[ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
543	\| _ ⇒ λabsd. ⊥
544	] (subaddressing_modein … x)) instr s
545	\| _ ⇒ ?
546	] in s.
547	\| ACALL addr ⇒
548	let s ≝ set_clock ? s (ticks + clock ? s) in
549	match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
550	[ ADDR11 a ⇒ λaddr11: True.
551	let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
552	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
553	let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
554	let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
555	let s ≝ write_at_stack_pointer ? s pc_bl in
556	let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
557	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
558	let s ≝ write_at_stack_pointer ? s pc_bu in
559	let thr ≝ \fst (split ? 3 8 a) in
560	let eig ≝ \snd (split ? 3 8 a) in
561	let fiv ≝ \fst (split ? 5 3 pc_bu) in
562	let thr' ≝ \snd (split ? 5 3 pc_bu) in
563	let new_addr ≝ (fiv @@ thr) @@ pc_bl in
564	set_program_counter ? s new_addr
565	\| _ ⇒ λother: False. ⊥
566	] (subaddressing_modein … addr)
567	\| LCALL addr ⇒
568	let s ≝ set_clock ? s (ticks + clock ? s) in
569	match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
570	[ ADDR16 a ⇒ λaddr16: True.
571	let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
572	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
573	let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
574	let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
575	let s ≝ write_at_stack_pointer ? s pc_bl in
576	let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
577	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
578	let s ≝ write_at_stack_pointer ? s pc_bu in
579	set_program_counter ? s a
580	\| _ ⇒ λother: False. ⊥
581	] (subaddressing_modein … addr)
582	\| MOVC addr1 addr2 ⇒
583	let s ≝ set_clock ? s (ticks + clock ? s) in
584	match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
585	[ ACC_DPTR ⇒ λacc_dptr: True.
586	let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
587	let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
588	let new_addr ≝ \snd (half_add ? dptr big_acc) in
589	let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
590	set_8051_sfr ? s SFR_ACC_A result
591	\| ACC_PC ⇒ λacc_pc: True.
592	let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
593	let inc_pc ≝ \snd (half_add ? (program_counter ? s) (bitvector_of_nat 16 1)) in
594	(* DPM: Under specified: does the carry from PC incrementation affect the *)
595	(* addition of the PC with the DPTR? At the moment, no. *)
596	let s ≝ set_program_counter ? s inc_pc in
597	let new_addr ≝ \snd (half_add ? inc_pc big_acc) in
598	let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
599	set_8051_sfr ? s SFR_ACC_A result
600	\| _ ⇒ λother: False. ⊥
601	] (subaddressing_modein … addr2)
602	\| JMP _ ⇒ (* DPM: always indirect_dptr *)
603	let s ≝ set_clock ? s (ticks + clock ? s) in
604	let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
605	let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
606	let jmp_addr ≝ \snd (half_add ? big_acc dptr) in
607	let new_pc ≝ \snd (half_add ? (program_counter ? s) jmp_addr) in
608	set_program_counter ? s new_pc
609	\| LJMP addr ⇒
610	let s ≝ set_clock ? s (ticks + clock ? s) in
611	match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
612	[ ADDR16 a ⇒ λaddr16: True.
613	set_program_counter ? s a
614	\| _ ⇒ λother: False. ⊥
615	] (subaddressing_modein … addr)
616	\| SJMP addr ⇒
617	let s ≝ set_clock ? s (ticks + clock ? s) in
618	match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
619	[ RELATIVE r ⇒ λrelative: True.
620	let new_pc ≝ \snd (half_add ? (program_counter ? s) (sign_extension r)) in
621	set_program_counter ? s new_pc
622	\| _ ⇒ λother: False. ⊥
623	] (subaddressing_modein … addr)
624	\| AJMP addr ⇒
625	let s ≝ set_clock ? s (ticks + clock ? s) in
626	match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
627	[ ADDR11 a ⇒ λaddr11: True.
628	let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
629	let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
630	let nu ≝ \fst (split ? 4 4 pc_bu) in
631	let nl ≝ \snd (split ? 4 4 pc_bu) in
632	let bit ≝ get_index' ? O ? nl in
633	let relevant1 ≝ \fst (split ? 3 8 a) in
634	let relevant2 ≝ \snd (split ? 3 8 a) in
635	let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
636	let new_pc ≝ \snd (half_add ? (program_counter ? s) new_addr) in
637	set_program_counter ? s new_pc
638	\| _ ⇒ λother: False. ⊥
639	] (subaddressing_modein … addr)
640	]
641	in
642	s.
643	try assumption
644	try (
645	normalize
646	repeat (@ (le_S_S))
647	@ (le_O_n)
648	)
649	try (
650	@ (execute_1_technical … (subaddressing_modein …))
651	@ I
652	)
653	try (
654	normalize
655	@ I
656	)
657	qed.
658
659	definition execute_1: Status → Status ≝
660	λs: Status.
661	let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
662	execute_1_0 s instr_pc_ticks.
663
664	definition execute_1_pseudo_instruction0: (nat × nat) → PseudoStatus → ? → ? → PseudoStatus ≝
665	λticks,s,instr,pc.
666	let s ≝ set_program_counter ? s pc in
667	let s ≝
668	match instr with
669	[ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels y x) instr s
670	\| Comment cmt ⇒
671	let s ≝ set_clock ? s (\fst ticks + clock ? s) in
672	s
673	\| Cost cst ⇒ s
674	\| Jmp jmp ⇒
675	let s ≝ set_clock ? s (\fst ticks + clock ? s) in
676	set_program_counter ? s (address_of_word_labels s jmp)
677	\| Call call ⇒
678	let s ≝ set_clock ? s (\fst ticks + clock ? s) in
679	let a ≝ address_of_word_labels s call in
680	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
681	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
682	let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
683	let s ≝ write_at_stack_pointer ? s pc_bl in
684	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
685	let s ≝ set_8051_sfr ? s SFR_SP new_sp in
686	let s ≝ write_at_stack_pointer ? s pc_bu in
687	set_program_counter ? s a
688	\| Mov dptr ident ⇒
689	let s ≝ set_clock ? s (\fst ticks + clock ? s) in
690	let preamble ≝ \fst (code_memory ? s) in
691	let data_labels ≝ construct_datalabels (map … (fst …) preamble) in
692	set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
693	]
694	in
695	s.
696	normalize
697	@ I
698	qed.
699
700	definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝
701	λticks_of,s.
702	let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
703	let ticks ≝ ticks_of (program_counter ? s) in
704	execute_1_pseudo_instruction0 ticks s instr pc.
705
706	let rec execute (n: nat) (s: Status) on n: Status ≝
707	match n with
708	[ O ⇒ s
709	\| S o ⇒ execute o (execute_1 s)
710	].
711
712	let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (s: PseudoStatus) on n: PseudoStatus ≝
713	match n with
714	[ O ⇒ s
715	\| S o ⇒ execute_pseudo_instruction o ticks_of (execute_1_pseudo_instruction ticks_of s)
716	].

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format