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
RevLine 
[698]1include "ASM/Util.ma".
2include "utilities/BitVectorTrieSet.ma".
3include "LIN/LIN.ma".
[2286]4include "ASM/ASM.ma".
[1264]5
[2286]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
[2443]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 ⇒ Ⓧ
[686]28  | cons hd tl ⇒
[2443]29    λprf.
30    If eq_A a (\fst hd) then \snd hd else with eq_prf do
31      association … eq_A a tl ?
[686]32  ].
[2443]33  elim (orb_Prop_true … prf)
34    [ > eq_prf *
[686]35    | # H
36      assumption
37    ]
[2443]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
[2490]57definition arg_address : hdw_argument →
[2443]58  [[ acc_a ; direct ; registr ; data ]] ≝
[2490]59  λa.
[2443]60  match a
61  with
[2490]62  [ Reg r ⇒ (register_address r : [[ acc_a ; direct ; registr ; data ]])
63  | Imm v ⇒ (DATA v : [[ acc_a ; direct ; registr ; data ]])
[2443]64  ].
[2490]65  [ elim (register_address ?) #rslt @is_in_subvector_is_in_supervector ] @I
[686]66qed.
[491]67
[2286]68definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
[2443]69
[491]70definition statement_labels ≝
[757]71  λg: list ident.
[1264]72  λs: lin_statement g.
[722]73  let 〈label, instr〉 ≝ s in
74  let generated ≝
75    match instr with
[1282]76    [ sequential instr' _ ⇒
[1149]77      match instr' with
[2286]78      [ step_seq instr'' ⇒
79        match instr'' with
80        [ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) }
81        | _ ⇒ ∅
82        ]
[1515]83      | COND acc_a_reg lbl ⇒ { (toASM_ident ? lbl) }
[2286]84      ]
85    | final instr' ⇒
86      match instr' with
87      [ GOTO lbl ⇒ {(toASM_ident ? lbl)}
[1515]88      | _ ⇒ ∅
[1112]89      ]
[2286]90    ]
[1112]91  in
[722]92  match label with
93  [ None ⇒ generated
[1515]94  | Some lbl ⇒ add_set ? generated (toASM_ident ? lbl)
[491]95  ].
96
[683]97definition function_labels_internal ≝
[757]98  λglobals: list ident.
[1515]99  λlabels: identifier_set ?.
[1264]100  λstatement: lin_statement globals.
[1515]101    labels ∪ (statement_labels globals statement).
[491]102
103(* dpm: A = Identifier *)
[1515]104definition function_labels: ∀A. ∀globals. ∀f. identifier_set ? ≝
[491]105  λA: Type[0].
[757]106  λglobals: list ident.
[2286]107  λf: A × (joint_function LIN globals).
[491]108  let 〈ignore, fun_def〉 ≝ f in
[1515]109  match fun_def return λ_. identifier_set ? with
[1245]110  [ Internal stmts ⇒
[1515]111      foldl ? ? (function_labels_internal globals) ∅ (joint_if_code ?? stmts)
112  | External _ ⇒ ∅
[491]113  ].
114 
[1515]115definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. identifier_set ? ≝
[491]116  λA: Type[0].
[757]117  λglobals: list ident.
[1515]118  λlabels: identifier_set ?.
[2286]119  λfunct: A × (joint_function LIN globals).
[1515]120    labels ∪ (function_labels ? globals funct).
[1264]121
122(* CSC: here we are silently throwing away the region information *)
[491]123definition program_labels ≝
[1264]124 λprogram: lin_program.
125    foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program)))
[1515]126              ∅ (prog_funct … program).
[1264]127 
[491]128definition data_of_int ≝ λbv. DATA bv.
[686]129definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
130definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
[491]131
[2286]132(* TODO: check and change to free bit *)
133definition asm_other_bit ≝ BIT_ADDR (zero_byte).
134
[491]135definition translate_statements ≝
[757]136  λglobals: list (ident × nat).
137  λglobals_old: list ident.
[2443]138  λprf: ∀i: ident. member ? (eq_identifier ?) i globals_old → member ? (eq_identifier ?) i (map ? ? (fst ? ?) globals).
[2286]139  λstatement: joint_statement LIN globals_old.
[2490]140  match statement  with
141  [ final instr ⇒
[2286]142    match instr with
143    [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl)
144    | RETURN ⇒ Instruction (RET ?)
[2490]145    | TAILCALL abs _ _ ⇒ Ⓧabs
[2286]146    ]
[1282]147  | sequential instr _ ⇒
[2490]148      match instr with
[2286]149      [ step_seq instr' ⇒
[2490]150        match instr' with
151        [ extension_seq ext ⇒
[2286]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          ]
[2490]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 _ _ _ _ ⇒
[2286]170          match accs with
171          [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
172          | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
173          ]
[2490]174        | OP1 op1 _ _ ⇒
[2286]175          match op1 with
176          [ Cmpl ⇒ Instruction (CPL ? ACC_A)
177          | Inc ⇒ Instruction (INC ? ACC_A)
178          | Rl ⇒ Instruction (RL ? ACC_A)
179          ]
[2490]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 _ _ ⇒
[2443]226          let look ≝ association_ident addr globals (prf ? proof) in
[2286]227            Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
[2490]228        | SET_CARRY ⇒
[2286]229          Instruction (SETB ? CARRY)
230        | MOVE regs ⇒
[2490]231          match regs with
232          [ to_acc _ reg ⇒
233            match register_address reg return λx.is_in … [[ acc_a;
[1245]234                                                              direct;
[2490]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;
[1245]246                                                              direct;
[2490]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〉))))))
[2286]276          ]
277        ]
[2490]278      | COND _ lbl ⇒
[1112]279        (* dpm: this should be handled in translate_code! *)
[1515]280        Instruction (JNZ ? (toASM_ident ? lbl))
[722]281      ]
[1149]282    ].
[2443]283  try @I
[686]284qed.
285
[1268]286(*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *)
[1515]287definition ident_of_label: label → Identifier ≝
288 toASM_ident LabelTag.
[1268]289
[723]290definition build_translated_statement ≝
291  λglobals.
292  λglobals_old.
293  λprf.
[1264]294  λstatement: lin_statement globals_old.
[1268]295    〈option_map … ident_of_label (\fst statement), translate_statements globals globals_old prf (\snd statement)〉.
[723]296
[686]297definition translate_code ≝
[757]298  λglobals: list (ident × nat).
299  λglobals_old: list ident.
[699]300  λprf.
[1264]301  λcode: list (lin_statement globals_old).
[723]302    map ? ? (build_translated_statement globals globals_old prf) code.
303
[696]304definition translate_fun_def ≝
[1268]305  λglobals: list (ident × nat).
[723]306  λglobals_old.
307  λprf.
[2490]308  λid_def : ident × (joint_function LIN globals_old).
[696]309    let 〈id, def〉 ≝ id_def in
310    match def with
[1268]311    [ Internal int ⇒
[2286]312      let code ≝ joint_if_code LIN globals_old int in
[1379]313      match translate_code globals globals_old prf code with
314      [ nil ⇒ ⊥
315      | cons hd tl ⇒
[1515]316        let rest ≝ 〈Some ? (toASM_ident SymbolTag id), \snd hd〉 :: tl in
[757]317          map ? ? (
318            λr.
319            match fst ? ? r with
[1515]320            [ Some id' ⇒ 〈Some ? (toASM_ident ? id'), snd ? ? r〉
[757]321            | None ⇒ 〈None ?, \snd r〉
322            ]) rest
[1379]323      ]
[1264]324    | External _ ⇒ [ ]
[696]325    ].
[1379]326cases daemon (*CSC: XXX will be fixed by an invariant later *)
[723]327qed.
[1515]328
[1522]329include "common/Identifiers.ma".
330
331let rec flatten_fun_defs
332  (globals: list (ident × nat)) (globals_old: list ident) (prf: ?) (initial_pc: nat)
[2490]333    (the_list: list ((identifier SymbolTag) × (joint_function LIN globals_old)))
[1522]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
[696]348definition translate_functs ≝
349  λglobals.
[699]350  λglobals_old.
351  λprf.
[696]352  λexit_label.
353  λmain.
[2490]354  λfuncts : list (ident × (joint_function LIN ?)).
[1264]355  let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in
[1522]356  let 〈flattened, map〉 ≝ flatten_fun_defs globals globals_old prf 6 (* Size of preamble above *) functs in
357   〈preamble @ flattened, map〉.
[696]358
[1264]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.
[696]365    let 〈res, offset〉 ≝ res_offset in
[1264]366    let 〈x, region, size〉 ≝ x_size in
367      〈〈x, offset〉 :: res, offset + size〉
368  in
[699]369    \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).
[1268]370
[699]371(* dpm: plays the role of the string "_exit" in the O'caml source *)
[1515]372axiom identifier_prefix: Identifier.
[1268]373(*CSC: XXXXXXX wrong anyway since labels from different functions can now
374  clash with each other and with names of functions *)
[1515]375axiom fresh_prefix: identifier_set ASMTag → Identifier → Identifier.
[699]376
[723]377(* dpm: fresh prefix stuff needs unifying with brian *)
[1995]378definition lin_to_asm : lin_program → pseudo_assembly_program ≝
[696]379  λp.
[1264]380  let prog_lbls ≝ program_labels … p in
[1268]381  let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
[1264]382  let global_addr ≝ globals_addr (prog_vars … p) in
[1522]383  let global_addr' ≝ map … (λx_off. let 〈x,off〉 ≝ x_off in 〈toASM_ident ? x, bitvector_of_nat 16 off〉) global_addr in
[2490]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
[1522]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
[1268]390 elim (prog_vars … p) //
[1522]391 #hd #tl #IH whd in ⊢ (% → %);
392 whd in match globals_addr; normalize nodelta
393 whd in match (foldl ???? (hd::tl)); normalize nodelta
[1268]394 cases hd * #id #reg #size normalize nodelta
395 cases daemon (*CSC: provable using a pair of lemmas over foldl *)
[1522]396qed.
Note: See TracBrowser for help on using the repository browser.