source: src/LIN/LINToASM.ma @ 2763

Last change on this file since 2763 was 2763, checked in by sacerdot, 7 years ago

All daemons in compiler.ma closed (i.e. proof obligations added
to the sigma type of compiled programs).

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