Context Navigation

LINToASM.ma @ 1132

Last change on this file since 1132 was 1112, checked in by mulligan, 9 years ago
got lin > asm stuff working
File size: 13.5 KB

Line
1	include "ASM/Util.ma".
2	include "utilities/BitVectorTrieSet.ma".
3	include "utilities/IdentifierTools.ma".
4	include "LIN/LIN.ma".
5
6	let rec association (i: ident) (l: list (ident × nat))
7	on l: member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat ≝
8	match l return λl. member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat with
9	[ nil ⇒ λabsd. ?
10	\| cons hd tl ⇒
11	λprf: member i (eq_identifier ?) (map ? ? (fst ? ?) (cons ? hd tl)).
12	(match eq_identifier ? (\fst hd) i return λb. eq_identifier ? (\fst hd) i = b → nat with
13	[ true ⇒ λeq_prf. \snd hd
14	\| false ⇒ λeq_prf. association i tl ?
15	]) (refl ? (eq_identifier ? (\fst hd) i))
16	].
17	[ cases absd
18	\| cases prf
19	[ > eq_prf
20	# H
21	cases H
22	\| # H
23	assumption
24	]
25	]
26	qed.
27
28	definition statement_labels ≝
29	λg: list ident.
30	λs: lin_statement g.
31	let 〈label, instr〉 ≝ s in
32	let generated ≝
33	match instr with
34	[ lin_st_lift l ⇒
35	match l with
36	[ joint_st_sequential instr' _ ⇒
37	match instr' with
38	[ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
39	\| joint_instr_cond_acc lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
40	\| _ ⇒ set_empty ?
41	]
42	\| joint_st_return ⇒ set_empty ?
43	]
44	\| lin_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
45	]
46	in
47	match label with
48	[ None ⇒ generated
49	\| Some lbl ⇒ set_insert ? (word_of_identifier ? lbl) generated
50	].
51
52	definition function_labels_internal ≝
53	λglobals: list ident.
54	λlabels: BitVectorTrieSet ?.
55	λstatement: lin_statement globals.
56	set_union ? labels (statement_labels globals statement).
57
58	(* dpm: A = Identifier *)
59	definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝
60	λA: Type[0].
61	λglobals: list ident.
62	λf: A × (lin_function_definition globals).
63	let 〈ignore, fun_def〉 ≝ f in
64	match fun_def return λ_. BitVectorTrieSet ? with
65	[ lin_fu_internal stmts proof ⇒
66	foldl ? ? (function_labels_internal globals) (set_empty ?) stmts
67	\| lin_fu_external _ ⇒ set_empty ?
68	].
69
70	definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet ? ≝
71	λA: Type[0].
72	λglobals: list ident.
73	λlabels: BitVectorTrieSet ?.
74	λfunct: A × (lin_function_definition globals).
75	set_union ? labels (function_labels ? globals funct).
76
77	definition program_labels ≝
78	λprogram.
79	foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) (lin_pr_vars program)))
80	(set_empty ?) (lin_pr_funcs program).
81
82	definition data_of_int ≝ λbv. DATA bv.
83	definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
84	definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
85
86	axiom ImplementedInRuntime: False.
87
88	definition translate_statements ≝
89	λglobals: list (ident × nat).
90	λglobals_old: list ident.
91	λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals).
92	λstatement: pre_lin_statement globals_old.
93	match statement with
94	[ lin_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
95	\| lin_st_lift l ⇒
96	match l with
97	[ joint_st_return ⇒ Instruction (RET ?)
98	\| joint_st_sequential instr _ ⇒
99	match instr with
100	[ joint_instr_comment comment ⇒ Comment comment
101	\| joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl)
102	\| joint_instr_pop ⇒ Instruction (POP ? accumulator_address)
103	\| joint_instr_push ⇒ Instruction (PUSH ? accumulator_address)
104	\| joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY)
105	\| joint_instr_call_id f ⇒ Call (word_of_identifier ? f)
106	\| joint_instr_opaccs accs ⇒
107	match accs with
108	[ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
109	\| DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
110	]
111	\| joint_instr_op1 op1 ⇒
112	match op1 with
113	[ Cmpl ⇒ Instruction (CPL ? ACC_A)
114	\| Inc ⇒ Instruction (INC ? ACC_A)
115	]
116	\| joint_instr_op2 op2 reg ⇒
117	match op2 with
118	[ Add ⇒
119	let reg' ≝ register_address reg in
120	match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
121	direct;
122	registr ]] x) → ? with
123	[ ACC_A ⇒ λacc_a: True.
124	Instruction (ADD ? ACC_A accumulator_address)
125	\| DIRECT d ⇒ λdirect1: True.
126	Instruction (ADD ? ACC_A (DIRECT d))
127	\| REGISTER r ⇒ λregister1: True.
128	Instruction (ADD ? ACC_A (REGISTER r))
129	\| _ ⇒ λother: False. ⊥
130	] (subaddressing_modein … reg')
131	\| Addc ⇒
132	let reg' ≝ register_address reg in
133	match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
134	direct;
135	registr ]] x) → ? with
136	[ ACC_A ⇒ λacc_a: True.
137	Instruction (ADDC ? ACC_A accumulator_address)
138	\| DIRECT d ⇒ λdirect2: True.
139	Instruction (ADDC ? ACC_A (DIRECT d))
140	\| REGISTER r ⇒ λregister2: True.
141	Instruction (ADDC ? ACC_A (REGISTER r))
142	\| _ ⇒ λother: False. ⊥
143	] (subaddressing_modein … reg')
144	\| Sub ⇒
145	let reg' ≝ register_address reg in
146	match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
147	direct;
148	registr ]] x) → ? with
149	[ ACC_A ⇒ λacc_a: True.
150	Instruction (SUBB ? ACC_A accumulator_address)
151	\| DIRECT d ⇒ λdirect3: True.
152	Instruction (SUBB ? ACC_A (DIRECT d))
153	\| REGISTER r ⇒ λregister3: True.
154	Instruction (SUBB ? ACC_A (REGISTER r))
155	\| _ ⇒ λother: False. ⊥
156	] (subaddressing_modein … reg')
157	\| And ⇒
158	let reg' ≝ register_address reg in
159	match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
160	direct;
161	registr ]] x) → ? with
162	[ ACC_A ⇒ λacc_a: True.
163	Instruction (NOP ?)
164	\| DIRECT d ⇒ λdirect4: True.
165	Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
166	\| REGISTER r ⇒ λregister4: True.
167	Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
168	\| _ ⇒ λother: False. ⊥
169	] (subaddressing_modein … reg')
170	\| Or ⇒
171	let reg' ≝ register_address reg in
172	match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
173	direct;
174	registr ]] x) → ? with
175	[ ACC_A ⇒ λacc_a: True.
176	Instruction (NOP ?)
177	\| DIRECT d ⇒ λdirect5: True.
178	Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
179	\| REGISTER r ⇒ λregister5: True.
180	Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
181	\| _ ⇒ λother: False. ⊥
182	] (subaddressing_modein … reg')
183	\| Xor ⇒
184	let reg' ≝ register_address reg in
185	match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
186	direct;
187	registr ]] x) → ? with
188	[ ACC_A ⇒ λacc_a: True.
189	Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
190	\| DIRECT d ⇒ λdirect6: True.
191	Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
192	\| REGISTER r ⇒ λregister6: True.
193	Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
194	\| _ ⇒ λother: False. ⊥
195	] (subaddressing_modein … reg')
196	]
197	\| joint_instr_int reg byte ⇒
198	let reg' ≝ register_address reg in
199	match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
200	direct;
201	registr ]] x) → ? with
202	[ REGISTER r ⇒ λregister7: True.
203	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉))))))
204	\| ACC_A ⇒ λacc: True.
205	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉))))))
206	\| DIRECT d ⇒ λdirect7: True.
207	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉)))))
208	\| _ ⇒ λother: False. ⊥
209	] (subaddressing_modein … reg')
210	\| joint_instr_from_acc reg ⇒
211	let reg' ≝ register_address reg in
212	match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
213	direct;
214	registr ]] x) → ? with
215	[ REGISTER r ⇒ λregister8: True.
216	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
217	\| ACC_A ⇒ λacc: True.
218	Instruction (NOP ?)
219	\| DIRECT d ⇒ λdirect8: True.
220	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
221	\| _ ⇒ λother: False. ⊥
222	] (subaddressing_modein … reg')
223	\| joint_instr_to_acc reg ⇒
224	let reg' ≝ register_address reg in
225	match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
226	direct;
227	registr ]] x) → ? with
228	[ REGISTER r ⇒ λregister9: True.
229	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
230	\| DIRECT d ⇒ λdirect9: True.
231	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
232	\| ACC_A ⇒ λacc_a: True.
233	Instruction (NOP ?)
234	\| _ ⇒ λother: False. ⊥
235	] (subaddressing_modein … reg')
236	\| joint_instr_load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
237	\| joint_instr_store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
238	\| joint_instr_address addr proof ⇒
239	let look ≝ association addr globals (prf ? proof) in
240	Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
241	\| joint_instr_cond_acc lbl ⇒
242	(* dpm: this should be handled in translate_code! *)
243	Instruction (JNZ ? (word_of_identifier ? lbl))
244	\| joint_instr_set_carry ⇒
245	Instruction (SETB ? CARRY)
246	]
247	]
248	].
249	try assumption
250	try @ I
251	cases ImplementedInRuntime
252	qed.
253
254	definition build_translated_statement ≝
255	λglobals.
256	λglobals_old.
257	λprf.
258	λstatement: lin_statement globals_old.
259	〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉.
260
261	definition translate_code ≝
262	λglobals: list (ident × nat).
263	λglobals_old: list ident.
264	λprf.
265	λcode: list (lin_statement globals_old).
266	map ? ? (build_translated_statement globals globals_old prf) code.
267
268	lemma translate_code_preserves_WellFormedP:
269	∀globals, globals_old, prf, code.
270	well_formed_P ? ? code → well_formed_P ? ? (translate_code globals globals_old prf code).
271	#G #GO #P #C
272	elim C
273	[ normalize
274	//
275	\| #G2 #G02 #IH (* CSC: understand here *)
276	whd in ⊢ (% → %)
277	normalize in ⊢ (% → %)
278	//
279	]
280	qed.
281
282	definition translate_fun_def ≝
283	λglobals.
284	λglobals_old.
285	λprf.
286	λid_def.
287	let 〈id, def〉 ≝ id_def in
288	match def with
289	[ lin_fu_internal code proof ⇒
290	match translate_code globals globals_old prf code return λtranscode. well_formed_P ? ? transcode → list labelled_instruction with
291	[ nil ⇒ λprf2. ⊥
292	\| cons hd tl ⇒ λ_.
293	let rest ≝ 〈Some ? id, \snd hd〉 :: tl in
294	map ? ? (
295	λr.
296	match fst ? ? r with
297	[ Some id' ⇒ 〈Some ? (word_of_identifier ? id'), snd ? ? r〉
298	\| None ⇒ 〈None ?, \snd r〉
299	]) rest
300	] (translate_code_preserves_WellFormedP globals globals_old prf code proof)
301	\| _ ⇒ [ ]
302	].
303	@ prf2
304	qed.
305
306	definition translate_functs ≝
307	λglobals.
308	λglobals_old.
309	λprf.
310	λexit_label.
311	λmain.
312	λfuncts.
313	let preamble ≝
314	match main with
315	[ None ⇒ [ ]
316	\| Some main' ⇒ [ 〈None ?, Call main'〉 ; 〈Some ? exit_label, Jmp exit_label〉 ]
317	] in
318	preamble @ (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
319
320	definition globals_addr_internal ≝
321	λres_offset.
322	λx_size: ident × nat.
323	let 〈res, offset〉 ≝ res_offset in
324	let 〈x, size〉 ≝ x_size in
325	〈〈x, offset〉 :: res, offset + size〉.
326
327	definition globals_addr ≝
328	λl.
329	\fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).
330
331	(* dpm: plays the role of the string "_exit" in the O'caml source *)
332	axiom identifier_prefix: Identifier.
333
334	(* dpm: fresh prefix stuff needs unifying with brian *)
335
336	(*
337	definition translate ≝
338	λp.
339	let prog_lbls ≝ program_labels p in
340	let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
341	let global_addr ≝ globals_addr (LIN_Pr_vars p) in
342	〈global_addr, translate_functs global_addr (map ? ? (fst ? ?) (LIN_Pr_vars p)) ? exit_label (LIN_Pr_main p) (LIN_Pr_funs p)〉.
343	*)

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

Download in other formats:

Original Format