Context Navigation

LINToASM.ma @ 2407

Last change on this file since 2407 was 2286, checked in by tranquil, 8 years ago

Big update!

merge of all _paolo variants
reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

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

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

Download in other formats:

Original Format