source: src/LIN/LINToASM.ma @ 2182

Last change on this file since 2182 was 1995, checked in by campbell, 8 years ago

Overall compiler definition; bits and pieces to
make everything happy(ish).

File size: 14.8 KB
Line 
1include "ASM/Util.ma".
2include "utilities/BitVectorTrieSet.ma".
3include "LIN/LIN.ma".
4
5let 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  ]
25qed.
26
27definition 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
47definition 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 *)
54definition 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 
65definition 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 *)
73definition program_labels ≝
74 λprogram: lin_program.
75    foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program)))
76              ∅ (prog_funct … program).
77 
78definition data_of_int ≝ λbv. DATA bv.
79definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
80definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
81
82definition 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
246qed.
247
248(*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *)
249definition ident_of_label: label → Identifier ≝
250 toASM_ident LabelTag.
251
252definition 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
259definition 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
266definition 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    ].
288cases daemon (*CSC: XXX will be fixed by an invariant later *)
289qed.
290
291include "common/Identifiers.ma".
292
293let 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
310definition 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 *)
322definition 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 *)
334axiom 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 *)
337axiom fresh_prefix: identifier_set ASMTag → Identifier → Identifier.
338
339(* dpm: fresh prefix stuff needs unifying with brian *)
340definition 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 *)
356qed.
Note: See TracBrowser for help on using the repository browser.