Context Navigation

LINToASM.ma @ 2497

Last change on this file since 2497 was 2490, checked in by tranquil, 8 years ago
switched back to Byte immediate (instead of beval ones) propagated pending changes to all passes
File size: 15.5 KB

Line
1	include "ASM/Util.ma".
2	include "utilities/BitVectorTrieSet.ma".
3	include "LIN/LIN.ma".
4	include "ASM/ASM.ma".
5
6	definition register_address: Register → [[ acc_a; direct; registr ]] ≝
7	λr: Register.
8	match r with
9	[ Register00 ⇒ REGISTER [[ false; false; false ]]
10	\| Register01 ⇒ REGISTER [[ false; false; true ]]
11	\| Register02 ⇒ REGISTER [[ false; true; false ]]
12	\| Register03 ⇒ REGISTER [[ false; true; true ]]
13	\| Register04 ⇒ REGISTER [[ true; false; false ]]
14	\| Register05 ⇒ REGISTER [[ true; false; true ]]
15	\| Register06 ⇒ REGISTER [[ true; true; false ]]
16	\| Register07 ⇒ REGISTER [[ true; true; true ]]
17	\| RegisterA ⇒ ACC_A
18	\| RegisterB ⇒ DIRECT (bitvector_of_nat 8 240)
19	\| RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82)
20	\| RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83)
21	\| _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r))
22	]. @I qed.
23
24	let rec association A B (eq_A : A → A → bool) (a : A) (l: list (A × B))
25	on l: member A eq_A a (map ? ? (fst ? ?) l) → B ≝
26	match l return λl. member A eq_A a (map ? ? (fst ? ?) l) → B with
27	[ nil ⇒ Ⓧ
28	\| cons hd tl ⇒
29	λprf.
30	If eq_A a (\fst hd) then \snd hd else with eq_prf do
31	association … eq_A a tl ?
32	].
33	elim (orb_Prop_true … prf)
34	[ > eq_prf *
35	\| # H
36	assumption
37	]
38	qed.
39
40	definition association_ident ≝ association ident nat (eq_identifier ?).
41	definition association_block ≝ association block Word eq_block.
42
43	definition vector_cast :
44	∀A,n,m.A → Vector A n → Vector A m ≝
45	λA,n,m,dflt,v.
46	If leb n m then with prf do
47	replicate … (m - n) dflt @@ v ⌈Vector ?? ↦ ?⌉
48	else with prf do
49	\snd (vsplit … (v ⌈Vector ?? ↦ Vector ? (n - m + m)⌉)).
50	lapply prf @(leb_elim n)
51	[2,3: #_ * #abs elim (abs I) ]
52	#H #_ >commutative_plus_faster @eq_f [@sym_eq] @(minus_to_plus … (refl …))
53	[ assumption ]
54	@(transitive_le … (not_le_to_lt … H)) %2 %1
55	qed.
56
57	definition arg_address : hdw_argument →
58	[[ acc_a ; direct ; registr ; data ]] ≝
59	λa.
60	match a
61	with
62	[ Reg r ⇒ (register_address r : [[ acc_a ; direct ; registr ; data ]])
63	\| Imm v ⇒ (DATA v : [[ acc_a ; direct ; registr ; data ]])
64	].
65	[ elim (register_address ?) #rslt @is_in_subvector_is_in_supervector ] @I
66	qed.
67
68	definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
69
70	definition statement_labels ≝
71	λg: list ident.
72	λs: lin_statement g.
73	let 〈label, instr〉 ≝ s in
74	let generated ≝
75	match instr with
76	[ sequential instr' _ ⇒
77	match instr' with
78	[ step_seq instr'' ⇒
79	match instr'' with
80	[ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) }
81	\| _ ⇒ ∅
82	]
83	\| COND acc_a_reg lbl ⇒ { (toASM_ident ? lbl) }
84	]
85	\| final instr' ⇒
86	match instr' with
87	[ GOTO lbl ⇒ {(toASM_ident ? lbl)}
88	\| _ ⇒ ∅
89	]
90	]
91	in
92	match label with
93	[ None ⇒ generated
94	\| Some lbl ⇒ add_set ? generated (toASM_ident ? lbl)
95	].
96
97	definition function_labels_internal ≝
98	λglobals: list ident.
99	λlabels: identifier_set ?.
100	λstatement: lin_statement globals.
101	labels ∪ (statement_labels globals statement).
102
103	(* dpm: A = Identifier *)
104	definition function_labels: ∀A. ∀globals. ∀f. identifier_set ? ≝
105	λA: Type[0].
106	λglobals: list ident.
107	λf: A × (joint_function LIN globals).
108	let 〈ignore, fun_def〉 ≝ f in
109	match fun_def return λ_. identifier_set ? with
110	[ Internal stmts ⇒
111	foldl ? ? (function_labels_internal globals) ∅ (joint_if_code ?? stmts)
112	\| External _ ⇒ ∅
113	].
114
115	definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. identifier_set ? ≝
116	λA: Type[0].
117	λglobals: list ident.
118	λlabels: identifier_set ?.
119	λfunct: A × (joint_function LIN globals).
120	labels ∪ (function_labels ? globals funct).
121
122	(* CSC: here we are silently throwing away the region information *)
123	definition program_labels ≝
124	λprogram: lin_program.
125	foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program)))
126	∅ (prog_funct … program).
127
128	definition data_of_int ≝ λbv. DATA bv.
129	definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
130	definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
131
132	(* TODO: check and change to free bit *)
133	definition asm_other_bit ≝ BIT_ADDR (zero_byte).
134
135	definition translate_statements ≝
136	λglobals: list (ident × nat).
137	λglobals_old: list ident.
138	λprf: ∀i: ident. member ? (eq_identifier ?) i globals_old → member ? (eq_identifier ?) i (map ? ? (fst ? ?) globals).
139	λstatement: joint_statement LIN globals_old.
140	match statement with
141	[ final instr ⇒
142	match instr with
143	[ GOTO lbl ⇒ Jmp (toASM_ident ? lbl)
144	\| RETURN ⇒ Instruction (RET ?)
145	\| TAILCALL abs _ _ ⇒ Ⓧabs
146	]
147	\| sequential instr _ ⇒
148	match instr with
149	[ step_seq instr' ⇒
150	match instr' with
151	[ extension_seq ext ⇒
152	match ext with
153	[ SAVE_CARRY ⇒
154	Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉))
155	\| RESTORE_CARRY ⇒
156	Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉)))
157	]
158	\| COMMENT comment ⇒ Comment comment
159	\| COST_LABEL lbl ⇒ Cost lbl
160	\| POP _ ⇒ Instruction (POP ? accumulator_address)
161	\| PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
162	\| CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
163	\| CALL f _ _ ⇒
164	match f with
165	[ inl f_id ⇒ Call (toASM_ident ? f_id)
166	\| inr _ ⇒ (* TODO call from ptr in DPTR *)
167	match not_implemented in False with [ ]
168	]
169	\| OPACCS accs _ _ _ _ ⇒
170	match accs with
171	[ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
172	\| DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
173	]
174	\| OP1 op1 _ _ ⇒
175	match op1 with
176	[ Cmpl ⇒ Instruction (CPL ? ACC_A)
177	\| Inc ⇒ Instruction (INC ? ACC_A)
178	\| Rl ⇒ Instruction (RL ? ACC_A)
179	]
180	\| OP2 op2 _ _ reg ⇒
181	match arg_address … reg
182	return λx.is_in … [[ acc_a;
183	direct;
184	registr;
185	data ]] x → ? with
186	[ ACC_A ⇒ λacc_a: True.
187	match op2 with
188	[ Add ⇒ Instruction (ADD ? ACC_A accumulator_address)
189	\| Addc ⇒ Instruction (ADDC ? ACC_A accumulator_address)
190	\| Sub ⇒ Instruction (SUBB ? ACC_A accumulator_address)
191	\| Xor ⇒ Instruction (CLR ? ACC_A)
192	\| _ ⇒ Instruction (NOP ?)
193	]
194	\| DIRECT d ⇒ λdirect1: True.
195	match op2 with
196	[ Add ⇒ Instruction (ADD ? ACC_A (DIRECT d))
197	\| Addc ⇒ Instruction (ADDC ? ACC_A (DIRECT d))
198	\| Sub ⇒ Instruction (SUBB ? ACC_A (DIRECT d))
199	\| And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
200	\| Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
201	\| Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
202	]
203	\| REGISTER r ⇒ λregister1: True.
204	match op2 with
205	[ Add ⇒ Instruction (ADD ? ACC_A (REGISTER r))
206	\| Addc ⇒ Instruction (ADDC ? ACC_A (REGISTER r))
207	\| Sub ⇒ Instruction (SUBB ? ACC_A (REGISTER r))
208	\| And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
209	\| Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
210	\| Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
211	]
212	\| DATA b ⇒ λdata : True.
213	match op2 with
214	[ Add ⇒ Instruction (ADD ? ACC_A (DATA b))
215	\| Addc ⇒ Instruction (ADDC ? ACC_A (DATA b))
216	\| Sub ⇒ Instruction (SUBB ? ACC_A (DATA b))
217	\| And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
218	\| Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
219	\| Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DATA b〉))
220	]
221	\| _ ⇒ Ⓧ
222	] (subaddressing_modein …)
223	\| LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
224	\| STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
225	\| ADDRESS addr proof _ _ ⇒
226	let look ≝ association_ident addr globals (prf ? proof) in
227	Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
228	\| SET_CARRY ⇒
229	Instruction (SETB ? CARRY)
230	\| MOVE regs ⇒
231	match regs with
232	[ to_acc _ reg ⇒
233	match register_address reg return λx.is_in … [[ acc_a;
234	direct;
235	registr]] x → ? with
236	[ REGISTER r ⇒ λregister9: True.
237	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
238	\| DIRECT d ⇒ λdirect9: True.
239	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
240	\| ACC_A ⇒ λacc_a: True.
241	Instruction (NOP ?)
242	\| _ ⇒ Ⓧ
243	] (subaddressing_modein …)
244	\| from_acc reg _ ⇒
245	match register_address reg return λx.is_in … [[ acc_a;
246	direct;
247	registr ]] x → ? with
248	[ REGISTER r ⇒ λregister8: True.
249	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
250	\| ACC_A ⇒ λacc: True.
251	Instruction (NOP ?)
252	\| DIRECT d ⇒ λdirect8: True.
253	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
254	\| _ ⇒ Ⓧ
255	] (subaddressing_modein …)
256	\| int_to_reg reg b ⇒
257	match register_address reg return λx.is_in … [[ acc_a;
258	direct;
259	registr ]] x → ? with
260	[ REGISTER r ⇒ λregister7: True.
261	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, DATA b〉))))))
262	\| ACC_A ⇒ λacc: True.
263	if eq_bv … (bv_zero …) b then
264	Instruction (CLR ? ACC_A)
265	else
266	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
267	\| DIRECT d ⇒ λdirect7: True.
268	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, DATA b〉)))))
269	\| _ ⇒ Ⓧ
270	] (subaddressing_modein …)
271	\| int_to_acc _ b ⇒
272	if eq_bv … (bv_zero …) b then
273	Instruction (CLR ? ACC_A)
274	else
275	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
276	]
277	]
278	\| COND _ lbl ⇒
279	(* dpm: this should be handled in translate_code! *)
280	Instruction (JNZ ? (toASM_ident ? lbl))
281	]
282	].
283	try @I
284	qed.
285
286	(CSC: XXXXXXXXXXX looks bad: what invariant is needed here? )
287	definition ident_of_label: label → Identifier ≝
288	toASM_ident LabelTag.
289
290	definition build_translated_statement ≝
291	λglobals.
292	λglobals_old.
293	λprf.
294	λstatement: lin_statement globals_old.
295	〈option_map … ident_of_label (\fst statement), translate_statements globals globals_old prf (\snd statement)〉.
296
297	definition translate_code ≝
298	λglobals: list (ident × nat).
299	λglobals_old: list ident.
300	λprf.
301	λcode: list (lin_statement globals_old).
302	map ? ? (build_translated_statement globals globals_old prf) code.
303
304	definition translate_fun_def ≝
305	λglobals: list (ident × nat).
306	λglobals_old.
307	λprf.
308	λid_def : ident × (joint_function LIN globals_old).
309	let 〈id, def〉 ≝ id_def in
310	match def with
311	[ Internal int ⇒
312	let code ≝ joint_if_code LIN globals_old int in
313	match translate_code globals globals_old prf code with
314	[ nil ⇒ ⊥
315	\| cons hd tl ⇒
316	let rest ≝ 〈Some ? (toASM_ident SymbolTag id), \snd hd〉 :: tl in
317	map ? ? (
318	λr.
319	match fst ? ? r with
320	[ Some id' ⇒ 〈Some ? (toASM_ident ? id'), snd ? ? r〉
321	\| None ⇒ 〈None ?, \snd r〉
322	]) rest
323	]
324	\| External _ ⇒ [ ]
325	].
326	cases daemon (CSC: XXX will be fixed by an invariant later )
327	qed.
328
329	include "common/Identifiers.ma".
330
331	let rec flatten_fun_defs
332	(globals: list (ident × nat)) (globals_old: list ident) (prf: ?) (initial_pc: nat)
333	(the_list: list ((identifier SymbolTag) × (joint_function LIN globals_old)))
334	on the_list: ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) ≝
335	match the_list return λx. ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) with
336	[ cons hd tl ⇒
337	let fun_def ≝ \snd hd in
338	let fun_id ≝ \fst hd in
339	let translated ≝ translate_fun_def globals globals_old prf hd in
340	let size_translated ≝ \| translated \| in
341	let 〈tail_trans, tail_map〉 ≝ flatten_fun_defs globals globals_old prf (initial_pc + size_translated) tl in
342	let new_hd ≝ translated @ tail_trans in
343	let new_map ≝ add ? ? tail_map fun_id initial_pc in
344	〈new_hd, new_map〉
345	\| nil ⇒ 〈[ ], empty_map …〉
346	].
347
348	definition translate_functs ≝
349	λglobals.
350	λglobals_old.
351	λprf.
352	λexit_label.
353	λmain.
354	λfuncts : list (ident × (joint_function LIN ?)).
355	let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in
356	let 〈flattened, map〉 ≝ flatten_fun_defs globals globals_old prf 6 (* Size of preamble above *) functs in
357	〈preamble @ flattened, map〉.
358
359	(CSC: region silently thrown away here )
360	definition globals_addr ≝
361	λl.
362	let globals_addr_internal ≝
363	λres_offset.
364	λx_size: ident × region × nat.
365	let 〈res, offset〉 ≝ res_offset in
366	let 〈x, region, size〉 ≝ x_size in
367	〈〈x, offset〉 :: res, offset + size〉
368	in
369	\fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).
370
371	(* dpm: plays the role of the string "_exit" in the O'caml source *)
372	axiom identifier_prefix: Identifier.
373	(*CSC: XXXXXXX wrong anyway since labels from different functions can now
374	clash with each other and with names of functions *)
375	axiom fresh_prefix: identifier_set ASMTag → Identifier → Identifier.
376
377	(* dpm: fresh prefix stuff needs unifying with brian *)
378	definition lin_to_asm : lin_program → pseudo_assembly_program ≝
379	λp.
380	let prog_lbls ≝ program_labels … p in
381	let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
382	let global_addr ≝ globals_addr (prog_vars … p) in
383	let global_addr' ≝ map … (λx_off. let 〈x,off〉 ≝ x_off in 〈toASM_ident ? x, bitvector_of_nat 16 off〉) global_addr in
384	let 〈translated, funct_map〉 ≝
385	translate_functs global_addr (prog_var_names … p) ? exit_label
386	(toASM_ident … (prog_main … p)) (prog_funct ?? p) in
387	〈〈funct_map, global_addr'〉, translated〉.
388	#i normalize nodelta -global_addr' -global_addr -exit_label -prog_lbls;
389	normalize in match prog_var_names; normalize nodelta
390	elim (prog_vars … p) //
391	#hd #tl #IH whd in ⊢ (% → %);
392	whd in match globals_addr; normalize nodelta
393	whd in match (foldl ???? (hd::tl)); normalize nodelta
394	cases hd * #id #reg #size normalize nodelta
395	cases daemon (CSC: provable using a pair of lemmas over foldl )
396	qed.

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

Download in other formats:

Original Format