Context Navigation

LINToASM.ma @ 1238

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

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

Download in other formats:

Original Format