Context Navigation

LINToASM.ma @ 2202

Last change on this file since 2202 was 1995, checked in by campbell, 9 years ago
Overall compiler definition; bits and pieces to make everything happy(ish).
File size: 14.8 KB

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

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

Download in other formats:

Original Format