source: src/LIN/LINToASM.ma @ 2767

Last change on this file since 2767 was 2767, checked in by mckinna, 7 years ago

WARNING: BIG commit, which pushes code_size_opt check into LIN/LINToASM.ma
following CSC's comment on my previous partial commit
plus rolls all the miscellaneous code motion into the rest of the repo.

suggest REBUILD compiler.ma/correctness.ma from scratch.

File size: 15.1 KB
Line 
1include "utilities/BitVectorTrieSet.ma".
2include "utilities/state.ma".
3
4include "ASM/Util.ma".
5include "ASM/ASM.ma".
6
7include "LIN/LIN.ma".
8
9(* utilities to provide Identifier's and addresses  *)
10record ASM_universe (globals : list ident) : Type[0] :=
11{ id_univ : universe ASMTag
12; current_funct : ident
13; ident_map : identifier_map SymbolTag Identifier
14; label_map : identifier_map SymbolTag (identifier_map LabelTag Identifier)
15; address_map : identifier_map SymbolTag Word
16; globals_are_in : ∀i : ident.i ∈ globals → i ∈ address_map
17}.
18
19definition new_ASM_universe :
20∀p : joint_program LIN.ASM_universe (prog_var_names … p) ≝
21λp.
22  let globals_addr_internal ≝
23   λres_offset : identifier_map SymbolTag Word × Z.
24   λx_size: ident × region × nat.
25    let 〈res, offset〉 ≝ res_offset in
26    let 〈x, region, size〉 ≝ x_size in
27      〈add … res x (bitvector_of_Z … offset), offset + Z_of_nat size〉 in
28  let addresses ≝ foldl … globals_addr_internal 〈empty_map …, OZ〉 (prog_vars … p) in
29mk_ASM_universe ? (mk_universe … one)
30  (an_identifier … one (* dummy *))
31  (empty_map …) (empty_map …)
32  (\fst addresses) ?.
33@hide_prf
34normalize nodelta
35cases p -p #vars #functs #main
36#i #H
37letin init_val ≝ (〈empty_map ? Word, OZ〉)
38cut (bool_to_Prop (i ∈ \fst init_val) ∨ bool_to_Prop (i ∈ map … (λx.\fst (\fst x)) vars))
39[ %2{H} ] -H
40lapply i -i lapply init_val -init_val elim vars -vars
41[2: ** #id #r #v #tl #IH ] #init_val #i
42[2: * [2: * ] #H @H ]
43* [2: #H cases (orb_Prop_true … H) -H ] #H
44@IH
45[ %1 cases init_val normalize nodelta #init_map #off
46  >(proj1 ?? (eqb_true ???) H) @mem_set_add_id
47| %2{H}
48| %1 cases init_val in H; normalize nodelta #init_map #off #H
49  >mem_set_add @orb_Prop_r @H
50]
51qed.
52
53definition Identifier_of_label :
54  ∀globals.label → state_monad (ASM_universe globals) Identifier ≝
55λg,l,u.
56let current ≝ current_funct … u in
57let lmap ≝ lookup_def … (label_map … u) current (empty_map …) in
58let 〈id, univ, lmap〉 ≝
59  match lookup … lmap l with
60  [ Some id ⇒ 〈id, id_univ … u, lmap〉
61  | None ⇒
62    let 〈id, univ〉 ≝ fresh … (id_univ … u) in
63    〈id, univ, add … lmap l id〉
64  ] in
65〈mk_ASM_universe … univ current (ident_map … u) (add … (label_map … u) current lmap)
66  (address_map … u) (globals_are_in … u), id〉.
67
68definition Identifier_of_ident :
69  ∀globals.ident → state_monad (ASM_universe globals) Identifier ≝
70λg,i,u.
71let imap ≝ ident_map … u in
72let 〈id, univ, imap〉 ≝
73  match lookup … imap i with
74  [ Some id ⇒ 〈id, id_univ … u, imap〉
75  | None ⇒
76    let 〈id, univ〉 ≝ fresh … (id_univ … u) in
77    〈id, univ, add … imap i id〉
78  ] in
79〈mk_ASM_universe … univ (current_funct … u) imap (label_map … u)
80  (address_map … u) (globals_are_in … u), id〉.
81
82definition start_funct_translation :
83  ∀globals.(ident × (joint_function LIN globals)) →
84    state_monad (ASM_universe globals) unit ≝
85  λg,id_f,u.
86    〈mk_ASM_universe … (id_univ … u) (\fst id_f) (ident_map … u) (label_map … u)
87      (address_map … u) (globals_are_in … u), it〉.
88
89definition address_of_ident :
90  ∀globals,i.i ∈ globals → state_monad (ASM_universe globals) [[ data16 ]] ≝
91λglobals,i,prf,u.
92〈u, DATA16 (lookup_safe … (globals_are_in … u … prf))〉. @I qed.
93
94definition ASM_fresh :
95  ∀globals.state_monad (ASM_universe globals) Identifier ≝
96λg,u.let 〈id, univ〉 ≝ fresh … (id_univ … u) in
97〈mk_ASM_universe … univ (current_funct … u) (ident_map … u) (label_map … u)
98  (address_map … u) (globals_are_in … u), id〉.
99
100definition register_address: Register → [[ acc_a; direct; registr ]] ≝
101  λr: Register.
102    match r with
103    [ Register00 ⇒ REGISTER [[ false; false; false ]]
104    | Register01 ⇒ REGISTER [[ false; false; true ]]
105    | Register02 ⇒ REGISTER [[ false; true; false ]]
106    | Register03 ⇒ REGISTER [[ false; true; true ]]
107    | Register04 ⇒ REGISTER [[ true; false; false ]]
108    | Register05 ⇒ REGISTER [[ true; false; true ]]
109    | Register06 ⇒ REGISTER [[ true; true; false ]]
110    | Register07 ⇒ REGISTER [[ true; true; true ]]
111    | RegisterA ⇒ ACC_A
112    | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240)
113    | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82)
114    | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83)
115    | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r))
116    ]. @I qed.
117
118definition vector_cast :
119∀A,n,m.A → Vector A n → Vector A m ≝
120λA,n,m,dflt,v.
121If leb n m then with prf do
122  replicate … (m - n) dflt @@ v ⌈Vector ?? ↦ ?⌉
123else with prf do
124  \snd (vsplit … (v ⌈Vector ?? ↦ Vector ? (n - m + m)⌉)).
125lapply prf @(leb_elim n)
126[2,3: #_ * #abs elim (abs I) ]
127#H #_ >commutative_plus_faster @eq_f [@sym_eq] @(minus_to_plus … (refl …))
128[ assumption ]
129@(transitive_le … (not_le_to_lt … H)) %2 %1
130qed.
131
132definition arg_address : hdw_argument →
133  [[ acc_a ; direct ; registr ; data ]] ≝
134  λa.
135  match a
136  with
137  [ Reg r ⇒ (register_address r : [[ acc_a ; direct ; registr ; data ]])
138  | Imm v ⇒ (DATA v : [[ acc_a ; direct ; registr ; data ]])
139  ].
140  [ elim (register_address ?) #rslt @is_in_subvector_is_in_supervector ] @I
141qed.
142
143definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
144
145definition data_of_int ≝ λbv. DATA bv.
146definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
147definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
148
149(* TODO: check and change to free bit *)
150definition asm_other_bit ≝ BIT_ADDR (zero_byte).
151
152definition translate_statements :
153  ∀globals.
154  joint_statement LIN globals →
155  state_monad (ASM_universe globals) pseudo_instruction ≝
156  λglobals,statement.
157  match statement with
158  [ final instr ⇒
159    match instr with
160    [ GOTO lbl ⇒
161      ! lbl' ← Identifier_of_label … lbl ;
162      return Jmp (toASM_ident ? lbl)
163    | RETURN ⇒ return Instruction (RET ?)
164    | TAILCALL abs _ _ ⇒ Ⓧabs
165    ]
166  | sequential instr _ ⇒
167      match instr with
168      [ step_seq instr' ⇒
169        match instr' with
170        [ extension_seq ext ⇒
171          match ext with
172          [ SAVE_CARRY ⇒
173            return Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉))
174          | RESTORE_CARRY ⇒
175            return Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉)))
176          | LOW_ADDRESS reg lbl ⇒
177            ! lbl' ← Identifier_of_label … lbl ;
178            return MovSuccessor (register_address reg) LOW lbl'
179          | HIGH_ADDRESS reg lbl ⇒
180            ! lbl' ← Identifier_of_label … lbl ;
181            return MovSuccessor (register_address reg) HIGH lbl'
182          ]
183        | COMMENT comment ⇒ return Comment comment
184        | POP _ ⇒ return Instruction (POP ? accumulator_address)
185        | PUSH _ ⇒ return Instruction (PUSH ? accumulator_address)
186        | CLEAR_CARRY ⇒ return Instruction (CLR ? CARRY)
187        | OPACCS accs _ _ _ _ ⇒
188          return match accs with
189          [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
190          | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
191          ]
192        | OP1 op1 _ _ ⇒
193          return match op1 with
194          [ Cmpl ⇒ Instruction (CPL ? ACC_A)
195          | Inc ⇒ Instruction (INC ? ACC_A)
196          | Rl ⇒ Instruction (RL ? ACC_A)
197          ]
198        | OP2 op2 _ _ reg ⇒
199          return match arg_address … reg
200          return λx.is_in … [[ acc_a;
201                                 direct;
202                                 registr;
203                                 data ]] x → ? with
204          [ ACC_A ⇒ λacc_a: True.
205            match op2 with
206            [ Add ⇒ Instruction (ADD ? ACC_A accumulator_address)
207            | Addc ⇒ Instruction (ADDC ? ACC_A accumulator_address)
208            | Sub ⇒ Instruction (SUBB ? ACC_A accumulator_address)
209            | Xor ⇒ Instruction (CLR ? ACC_A)
210            | _ ⇒ Instruction (NOP ?)
211            ]
212          | DIRECT d ⇒ λdirect1: True.
213            match op2 with
214            [ Add ⇒ Instruction (ADD ? ACC_A (DIRECT d))
215            | Addc ⇒ Instruction (ADDC ? ACC_A (DIRECT d))
216            | Sub ⇒ Instruction (SUBB ? ACC_A (DIRECT d))
217            | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
218            | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
219            | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
220            ]
221          | REGISTER r ⇒ λregister1: True.
222            match op2 with
223            [ Add ⇒ Instruction (ADD ? ACC_A (REGISTER r))
224            | Addc ⇒ Instruction (ADDC ? ACC_A (REGISTER r))
225            | Sub ⇒ Instruction (SUBB ? ACC_A (REGISTER r))
226            | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
227            | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
228            | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
229            ]
230          | DATA b ⇒ λdata : True.
231            match op2 with
232            [ Add ⇒ Instruction (ADD ? ACC_A (DATA b))
233            | Addc ⇒ Instruction (ADDC ? ACC_A (DATA b))
234            | Sub ⇒ Instruction (SUBB ? ACC_A (DATA b))
235            | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
236            | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
237            | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DATA b〉))
238            ]
239          | _ ⇒ Ⓧ
240          ] (subaddressing_modein …)
241        | LOAD _ _ _ ⇒ return Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
242        | STORE _ _ _ ⇒ return Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
243        | ADDRESS addr proof _ _ ⇒
244          ! addr' ← address_of_ident … proof ;
245          return Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, addr'〉)))))
246        | SET_CARRY ⇒
247          return Instruction (SETB ? CARRY)
248        | MOVE regs ⇒
249          return match regs with
250          [ to_acc _ reg ⇒
251            match register_address reg return λx.is_in … [[ acc_a;
252                                                              direct;
253                                                              registr]] x → ? with
254           [ REGISTER r ⇒ λregister9: True.
255             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
256           | DIRECT d ⇒ λdirect9: True.
257             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
258           | ACC_A ⇒ λacc_a: True.
259             Instruction (NOP ?)
260           | _ ⇒ Ⓧ
261           ] (subaddressing_modein …)
262         | from_acc reg _ ⇒
263            match register_address reg return λx.is_in … [[ acc_a;
264                                                              direct;
265                                                              registr ]] x → ? with
266            [ REGISTER r ⇒ λregister8: True.
267             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
268            | ACC_A ⇒ λacc: True.
269             Instruction (NOP ?)
270            | DIRECT d ⇒ λdirect8: True.
271             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
272            | _ ⇒ Ⓧ
273            ] (subaddressing_modein …)
274          | int_to_reg reg b ⇒
275            match register_address reg return λx.is_in … [[ acc_a;
276                                                              direct;
277                                                              registr ]] x → ? with
278            [ REGISTER r ⇒ λregister7: True.
279              Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, DATA b〉))))))
280            | ACC_A ⇒ λacc: True.
281               if eq_bv … (bv_zero …) b then
282                  Instruction (CLR ? ACC_A)
283               else
284                  Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
285            | DIRECT d ⇒ λdirect7: True.
286              Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, DATA b〉)))))
287            | _ ⇒ Ⓧ
288            ] (subaddressing_modein …)
289          | int_to_acc _ b ⇒
290            if eq_bv … (bv_zero …) b then
291              Instruction (CLR ? ACC_A)
292            else
293              Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
294          ]
295        ]
296      | CALL f _ _ ⇒
297        match f with
298        [ inl id ⇒
299          ! id' ← Identifier_of_ident … id ;
300          return Call (toASM_ident ? id')
301        | inr _ ⇒
302          return Instruction (JMP … INDIRECT_DPTR)
303        ]
304      | COST_LABEL lbl ⇒ return Cost lbl
305      | COND _ lbl ⇒
306        ! l ← Identifier_of_label … lbl;
307        return Instruction (JNZ ? l)
308      ]
309    | FCOND _ _ lbl_true lbl_false ⇒
310      ! l1 ← Identifier_of_label … lbl_true;
311      ! l2 ← Identifier_of_label … lbl_false;
312      return Jnz ACC_A l1 l2
313    ].
314  try @I
315qed.
316
317
318definition build_translated_statement ≝
319  λglobals.
320  λstatement: lin_statement globals.
321  ! stmt ← translate_statements globals (\snd statement) ;
322  match \fst statement with
323  [ Some lbl ⇒
324    ! lbl' ← Identifier_of_label globals lbl ;
325    return 〈Some ? lbl', stmt〉
326  | None ⇒
327    return 〈None ?, stmt〉
328  ].
329
330definition translate_code ≝
331  λglobals.
332  λcode: list (lin_statement globals).
333    m_list_map … (build_translated_statement globals) code.
334
335definition translate_fun_def ≝
336  λglobals.
337  λid_def : ident × (joint_function LIN globals).
338  !_ start_funct_translation … id_def ;
339  (* ^ modify current function id ^ *)
340  match \snd id_def with
341    [ Internal int ⇒
342      let code ≝ joint_if_code … int in
343      ! id ← Identifier_of_ident … (\fst id_def) ;
344      ! code' ← translate_code … code ;
345      match code' with
346      [ nil ⇒ return [〈Some ? id, Instruction (RET ?)〉] (* impossible, but whatever *)
347      | cons hd tl ⇒
348        match \fst hd with
349        [ None ⇒ return (〈Some ? id, \snd hd〉 :: tl)
350        | _ ⇒ return (〈Some ? id, Instruction (NOP ?)〉 :: hd :: tl) (* should never happen *)
351        ]
352      ]
353    | External _ ⇒ return [ ]
354    ].
355
356definition get_symboltable :
357  ∀globals.state_monad (ASM_universe globals) (list (Identifier × ident)) ≝
358  λglobals,u.
359  let imap ≝ ident_map … u in
360  let f ≝ λiold,inew.cons ? 〈inew, iold〉 in
361  〈u, foldi ??? f imap [ ]〉.
362
363definition lin_to_asm : lin_program → option pseudo_assembly_program ≝
364  λp.
365  state_run ?? (new_ASM_universe p)
366    (let add_translation ≝
367      λacc,id_def.
368      ! code ← translate_fun_def … id_def ;
369      ! acc ← acc ;
370      return (code @ acc) in
371     ! code ← foldl … add_translation (return [ ]) (prog_funct … p) ;
372     ! exit_label ← ASM_fresh … ;
373     ! main ← Identifier_of_ident … (prog_main … p) ;
374     ! symboltable ← get_symboltable … ;
375     return
376      (let code ≝ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in
377       ! code_ok ← code_size_opt code ; 
378       (* atm no data identifier is used in the code, so preamble must be empty *)
379       return
380        (mk_pseudo_assembly_program [ ] code code_ok symboltable exit_label ? ?))).
381cases daemon
382qed.
Note: See TracBrowser for help on using the repository browser.