source: src/LIN/LINToASM.ma @ 2490

Last change on this file since 2490 was 2490, checked in by tranquil, 7 years ago

switched back to Byte immediate (instead of beval ones)
propagated pending changes to all passes

File size: 15.5 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
24let rec association A B (eq_A : A → A → bool) (a : A) (l: list (A × B))
25                    on l: member A eq_A a (map ? ? (fst ? ?) l) → B ≝
26  match l return λl. member A eq_A a (map ? ? (fst ? ?) l) → B with
27  [ nil ⇒ Ⓧ
28  | cons hd tl ⇒
29    λprf.
30    If eq_A a (\fst hd) then \snd hd else with eq_prf do
31      association … eq_A a tl ?
32  ].
33  elim (orb_Prop_true … prf)
34    [ > eq_prf *
35    | # H
36      assumption
37    ]
38qed.
39
40definition association_ident ≝ association ident nat (eq_identifier ?).
41definition association_block ≝ association block Word eq_block.
42
43definition vector_cast :
44∀A,n,m.A → Vector A n → Vector A m ≝
45λA,n,m,dflt,v.
46If leb n m then with prf do
47  replicate … (m - n) dflt @@ v ⌈Vector ?? ↦ ?⌉
48else with prf do
49  \snd (vsplit … (v ⌈Vector ?? ↦ Vector ? (n - m + m)⌉)).
50lapply prf @(leb_elim n)
51[2,3: #_ * #abs elim (abs I) ]
52#H #_ >commutative_plus_faster @eq_f [@sym_eq] @(minus_to_plus … (refl …))
53[ assumption ]
54@(transitive_le … (not_le_to_lt … H)) %2 %1
55qed.
56
57definition arg_address : hdw_argument →
58  [[ acc_a ; direct ; registr ; data ]] ≝
59  λa.
60  match a
61  with
62  [ Reg r ⇒ (register_address r : [[ acc_a ; direct ; registr ; data ]])
63  | Imm v ⇒ (DATA v : [[ acc_a ; direct ; registr ; data ]])
64  ].
65  [ elim (register_address ?) #rslt @is_in_subvector_is_in_supervector ] @I
66qed.
67
68definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
69
70definition statement_labels ≝
71  λg: list ident.
72  λs: lin_statement g.
73  let 〈label, instr〉 ≝ s in
74  let generated ≝
75    match instr with
76    [ sequential instr' _ ⇒
77      match instr' with
78      [ step_seq instr'' ⇒
79        match instr'' with
80        [ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) }
81        | _ ⇒ ∅
82        ]
83      | COND acc_a_reg lbl ⇒ { (toASM_ident ? lbl) }
84      ]
85    | final instr' ⇒
86      match instr' with
87      [ GOTO lbl ⇒ {(toASM_ident ? lbl)}
88      | _ ⇒ ∅
89      ]
90    ]
91  in
92  match label with
93  [ None ⇒ generated
94  | Some lbl ⇒ add_set ? generated (toASM_ident ? lbl)
95  ].
96
97definition function_labels_internal ≝
98  λglobals: list ident.
99  λlabels: identifier_set ?.
100  λstatement: lin_statement globals.
101    labels ∪ (statement_labels globals statement).
102
103(* dpm: A = Identifier *)
104definition function_labels: ∀A. ∀globals. ∀f. identifier_set ? ≝
105  λA: Type[0].
106  λglobals: list ident.
107  λf: A × (joint_function LIN globals).
108  let 〈ignore, fun_def〉 ≝ f in
109  match fun_def return λ_. identifier_set ? with
110  [ Internal stmts ⇒
111      foldl ? ? (function_labels_internal globals) ∅ (joint_if_code ?? stmts)
112  | External _ ⇒ ∅
113  ].
114 
115definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. identifier_set ? ≝
116  λA: Type[0].
117  λglobals: list ident.
118  λlabels: identifier_set ?.
119  λfunct: A × (joint_function LIN globals).
120    labels ∪ (function_labels ? globals funct).
121
122(* CSC: here we are silently throwing away the region information *)
123definition program_labels ≝
124 λprogram: lin_program.
125    foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program)))
126              ∅ (prog_funct … program).
127 
128definition data_of_int ≝ λbv. DATA bv.
129definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
130definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
131
132(* TODO: check and change to free bit *)
133definition asm_other_bit ≝ BIT_ADDR (zero_byte).
134
135definition translate_statements ≝
136  λglobals: list (ident × nat).
137  λglobals_old: list ident.
138  λprf: ∀i: ident. member ? (eq_identifier ?) i globals_old → member ? (eq_identifier ?) i (map ? ? (fst ? ?) globals).
139  λstatement: joint_statement LIN globals_old.
140  match statement  with
141  [ final instr ⇒
142    match instr with
143    [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl)
144    | RETURN ⇒ Instruction (RET ?)
145    | TAILCALL abs _ _ ⇒ Ⓧabs
146    ]
147  | sequential instr _ ⇒
148      match instr with
149      [ step_seq instr' ⇒
150        match instr' with
151        [ extension_seq ext ⇒
152          match ext with
153          [ SAVE_CARRY ⇒
154            Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉))
155          | RESTORE_CARRY ⇒
156            Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉)))
157          ]
158        | COMMENT comment ⇒ Comment comment
159        | COST_LABEL lbl ⇒ Cost lbl
160        | POP _ ⇒ Instruction (POP ? accumulator_address)
161        | PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
162        | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
163        | CALL f _ _ ⇒
164          match f with
165          [ inl f_id ⇒ Call (toASM_ident ? f_id)
166          | inr _ ⇒ (* TODO call from ptr in DPTR *)
167            match not_implemented in False with [ ]
168          ]
169        | OPACCS accs _ _ _ _ ⇒
170          match accs with
171          [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
172          | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
173          ]
174        | OP1 op1 _ _ ⇒
175          match op1 with
176          [ Cmpl ⇒ Instruction (CPL ? ACC_A)
177          | Inc ⇒ Instruction (INC ? ACC_A)
178          | Rl ⇒ Instruction (RL ? ACC_A)
179          ]
180        | OP2 op2 _ _ reg ⇒
181          match arg_address … reg
182          return λx.is_in … [[ acc_a;
183                                 direct;
184                                 registr;
185                                 data ]] x → ? with
186          [ ACC_A ⇒ λacc_a: True.
187            match op2 with
188            [ Add ⇒ Instruction (ADD ? ACC_A accumulator_address)
189            | Addc ⇒ Instruction (ADDC ? ACC_A accumulator_address)
190            | Sub ⇒ Instruction (SUBB ? ACC_A accumulator_address)
191            | Xor ⇒ Instruction (CLR ? ACC_A)
192            | _ ⇒ Instruction (NOP ?)
193            ]
194          | DIRECT d ⇒ λdirect1: True.
195            match op2 with
196            [ Add ⇒ Instruction (ADD ? ACC_A (DIRECT d))
197            | Addc ⇒ Instruction (ADDC ? ACC_A (DIRECT d))
198            | Sub ⇒ Instruction (SUBB ? ACC_A (DIRECT d))
199            | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
200            | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
201            | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
202            ]
203          | REGISTER r ⇒ λregister1: True.
204            match op2 with
205            [ Add ⇒ Instruction (ADD ? ACC_A (REGISTER r))
206            | Addc ⇒ Instruction (ADDC ? ACC_A (REGISTER r))
207            | Sub ⇒ Instruction (SUBB ? ACC_A (REGISTER r))
208            | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
209            | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
210            | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
211            ]
212          | DATA b ⇒ λdata : True.
213            match op2 with
214            [ Add ⇒ Instruction (ADD ? ACC_A (DATA b))
215            | Addc ⇒ Instruction (ADDC ? ACC_A (DATA b))
216            | Sub ⇒ Instruction (SUBB ? ACC_A (DATA b))
217            | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
218            | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
219            | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DATA b〉))
220            ]
221          | _ ⇒ Ⓧ
222          ] (subaddressing_modein …)
223        | LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
224        | STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
225        | ADDRESS addr proof _ _ ⇒
226          let look ≝ association_ident addr globals (prf ? proof) in
227            Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
228        | SET_CARRY ⇒
229          Instruction (SETB ? CARRY)
230        | MOVE regs ⇒
231          match regs with
232          [ to_acc _ reg ⇒
233            match register_address reg return λx.is_in … [[ acc_a;
234                                                              direct;
235                                                              registr]] x → ? with
236           [ REGISTER r ⇒ λregister9: True.
237             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
238           | DIRECT d ⇒ λdirect9: True.
239             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
240           | ACC_A ⇒ λacc_a: True.
241             Instruction (NOP ?)
242           | _ ⇒ Ⓧ
243           ] (subaddressing_modein …)
244         | from_acc reg _ ⇒
245            match register_address reg return λx.is_in … [[ acc_a;
246                                                              direct;
247                                                              registr ]] x → ? with
248            [ REGISTER r ⇒ λregister8: True.
249             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
250            | ACC_A ⇒ λacc: True.
251             Instruction (NOP ?)
252            | DIRECT d ⇒ λdirect8: True.
253             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
254            | _ ⇒ Ⓧ
255            ] (subaddressing_modein …)
256          | int_to_reg reg b ⇒
257            match register_address reg return λx.is_in … [[ acc_a;
258                                                              direct;
259                                                              registr ]] x → ? with
260            [ REGISTER r ⇒ λregister7: True.
261              Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, DATA b〉))))))
262            | ACC_A ⇒ λacc: True.
263               if eq_bv … (bv_zero …) b then
264                  Instruction (CLR ? ACC_A)
265               else
266                  Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
267            | DIRECT d ⇒ λdirect7: True.
268              Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, DATA b〉)))))
269            | _ ⇒ Ⓧ
270            ] (subaddressing_modein …)
271          | int_to_acc _ b ⇒
272            if eq_bv … (bv_zero …) b then
273              Instruction (CLR ? ACC_A)
274            else
275              Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
276          ]
277        ]
278      | COND _ lbl ⇒
279        (* dpm: this should be handled in translate_code! *)
280        Instruction (JNZ ? (toASM_ident ? lbl))
281      ]
282    ].
283  try @I
284qed.
285
286(*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *)
287definition ident_of_label: label → Identifier ≝
288 toASM_ident LabelTag.
289
290definition build_translated_statement ≝
291  λglobals.
292  λglobals_old.
293  λprf.
294  λstatement: lin_statement globals_old.
295    〈option_map … ident_of_label (\fst statement), translate_statements globals globals_old prf (\snd statement)〉.
296
297definition translate_code ≝
298  λglobals: list (ident × nat).
299  λglobals_old: list ident.
300  λprf.
301  λcode: list (lin_statement globals_old).
302    map ? ? (build_translated_statement globals globals_old prf) code.
303
304definition translate_fun_def ≝
305  λglobals: list (ident × nat).
306  λglobals_old.
307  λprf.
308  λid_def : ident × (joint_function LIN globals_old).
309    let 〈id, def〉 ≝ id_def in
310    match def with
311    [ Internal int ⇒
312      let code ≝ joint_if_code LIN globals_old int in
313      match translate_code globals globals_old prf code with
314      [ nil ⇒ ⊥
315      | cons hd tl ⇒
316        let rest ≝ 〈Some ? (toASM_ident SymbolTag id), \snd hd〉 :: tl in
317          map ? ? (
318            λr.
319            match fst ? ? r with
320            [ Some id' ⇒ 〈Some ? (toASM_ident ? id'), snd ? ? r〉
321            | None ⇒ 〈None ?, \snd r〉
322            ]) rest
323      ]
324    | External _ ⇒ [ ]
325    ].
326cases daemon (*CSC: XXX will be fixed by an invariant later *)
327qed.
328
329include "common/Identifiers.ma".
330
331let rec flatten_fun_defs
332  (globals: list (ident × nat)) (globals_old: list ident) (prf: ?) (initial_pc: nat)
333    (the_list: list ((identifier SymbolTag) × (joint_function LIN globals_old)))
334      on the_list: ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) ≝
335  match the_list return λx. ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) with
336  [ cons hd tl ⇒
337    let fun_def ≝ \snd hd in
338    let fun_id ≝ \fst hd in
339    let translated ≝ translate_fun_def globals globals_old prf hd in
340    let size_translated ≝ | translated | in
341    let 〈tail_trans, tail_map〉 ≝ flatten_fun_defs globals globals_old prf (initial_pc + size_translated) tl in
342    let new_hd ≝ translated @ tail_trans in
343    let new_map ≝ add ? ? tail_map fun_id initial_pc in
344      〈new_hd, new_map〉
345  | nil ⇒ 〈[ ], empty_map …〉
346  ].
347
348definition translate_functs ≝
349  λglobals.
350  λglobals_old.
351  λprf.
352  λexit_label.
353  λmain.
354  λfuncts : list (ident × (joint_function LIN ?)).
355  let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in
356  let 〈flattened, map〉 ≝ flatten_fun_defs globals globals_old prf 6 (* Size of preamble above *) functs in
357   〈preamble @ flattened, map〉.
358
359(*CSC: region silently thrown away here *)
360definition globals_addr ≝
361 λl.
362  let globals_addr_internal ≝
363   λres_offset.
364   λx_size: ident × region × nat.
365    let 〈res, offset〉 ≝ res_offset in
366    let 〈x, region, size〉 ≝ x_size in
367      〈〈x, offset〉 :: res, offset + size〉
368  in
369    \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).
370
371(* dpm: plays the role of the string "_exit" in the O'caml source *)
372axiom identifier_prefix: Identifier.
373(*CSC: XXXXXXX wrong anyway since labels from different functions can now
374  clash with each other and with names of functions *)
375axiom fresh_prefix: identifier_set ASMTag → Identifier → Identifier.
376
377(* dpm: fresh prefix stuff needs unifying with brian *)
378definition lin_to_asm : lin_program → pseudo_assembly_program ≝
379  λp.
380  let prog_lbls ≝ program_labels … p in
381  let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
382  let global_addr ≝ globals_addr (prog_vars … p) in
383  let global_addr' ≝ map … (λx_off. let 〈x,off〉 ≝ x_off in 〈toASM_ident ? x, bitvector_of_nat 16 off〉) global_addr in
384  let 〈translated, funct_map〉 ≝
385    translate_functs global_addr (prog_var_names … p) ? exit_label
386    (toASM_ident … (prog_main … p)) (prog_funct ?? p) in
387    〈〈funct_map, global_addr'〉, translated〉.
388 #i normalize nodelta -global_addr' -global_addr -exit_label -prog_lbls;
389 normalize in match prog_var_names; normalize nodelta
390 elim (prog_vars … p) //
391 #hd #tl #IH whd in ⊢ (% → %);
392 whd in match globals_addr; normalize nodelta
393 whd in match (foldl ???? (hd::tl)); normalize nodelta
394 cases hd * #id #reg #size normalize nodelta
395 cases daemon (*CSC: provable using a pair of lemmas over foldl *)
396qed.
Note: See TracBrowser for help on using the repository browser.