source: src/LIN/LINToASM.ma @ 2286

Last change on this file since 2286 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 
1include "ASM/Util.ma".
2include "utilities/BitVectorTrieSet.ma".
3include "LIN/LIN.ma".
4include "ASM/ASM.ma".
5
6definition 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. *)
29definition 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
39definition 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
46qed.
47
48let 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  ]
68qed.
69
70definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
71 
72definition 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
99definition 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 *)
106definition 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 
117definition 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 *)
125definition program_labels ≝
126 λprogram: lin_program.
127    foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program)))
128              ∅ (prog_funct … program).
129 
130definition data_of_int ≝ λbv. DATA bv.
131definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
132definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
133
134(* TODO: check and change to free bit *)
135definition asm_other_bit ≝ BIT_ADDR (zero_byte).
136
137definition 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
336qed.
337
338(*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *)
339definition ident_of_label: label → Identifier ≝
340 toASM_ident LabelTag.
341
342definition 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
349definition 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
356definition 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    ].
378cases daemon (*CSC: XXX will be fixed by an invariant later *)
379qed.
380
381include "common/Identifiers.ma".
382
383let 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
400definition 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 *)
412definition 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 *)
424axiom 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 *)
427axiom fresh_prefix: identifier_set ASMTag → Identifier → Identifier.
428
429(* dpm: fresh prefix stuff needs unifying with brian *)
430definition 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 *)
446qed.
Note: See TracBrowser for help on using the repository browser.