source: src/LIN/LINToASM.ma @ 1515

Last change on this file since 1515 was 1515, checked in by campbell, 10 years ago

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File size: 13.7 KB
Line 
1include "ASM/Util.ma".
2include "utilities/BitVectorTrieSet.ma".
3include "LIN/LIN.ma".
4
5let rec association (i: ident) (l: list (ident × nat))
6                    on l: member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat ≝
7  match l return λl. member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat with
8  [ nil ⇒ λabsd. ?
9  | cons hd tl ⇒
10    λprf: member i (eq_identifier ?) (map ? ? (fst ? ?) (cons ? hd tl)).
11      (match eq_identifier ? (\fst hd) i return λb. eq_identifier ? (\fst hd) i = b → nat with
12      [ true ⇒ λeq_prf. \snd hd
13      | false ⇒ λeq_prf. association i tl ?
14      ]) (refl ? (eq_identifier ? (\fst hd) i))
15  ].
16  [ cases absd
17  | cases prf
18    [ > eq_prf
19      # H
20      cases H
21    | # H
22      assumption
23    ]
24  ]
25qed.
26
27definition statement_labels ≝
28  λg: list ident.
29  λs: lin_statement g.
30  let 〈label, instr〉 ≝ s in
31  let generated ≝
32    match instr with
33    [ sequential instr' _ ⇒
34      match instr' with
35      [ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) }
36      | COND acc_a_reg lbl ⇒ { (toASM_ident ? lbl) }
37      | _ ⇒ ∅
38      ]
39    | RETURN ⇒ ∅
40    | GOTO lbl ⇒ {(toASM_ident ? lbl)} ]
41  in
42  match label with
43  [ None ⇒ generated
44  | Some lbl ⇒ add_set ? generated (toASM_ident ? lbl)
45  ].
46
47definition function_labels_internal ≝
48  λglobals: list ident.
49  λlabels: identifier_set ?.
50  λstatement: lin_statement globals.
51    labels ∪ (statement_labels globals statement).
52
53(* dpm: A = Identifier *)
54definition function_labels: ∀A. ∀globals. ∀f. identifier_set ? ≝
55  λA: Type[0].
56  λglobals: list ident.
57  λf: A × (lin_function globals).
58  let 〈ignore, fun_def〉 ≝ f in
59  match fun_def return λ_. identifier_set ? with
60  [ Internal stmts ⇒
61      foldl ? ? (function_labels_internal globals) ∅ (joint_if_code ?? stmts)
62  | External _ ⇒ ∅
63  ].
64 
65definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. identifier_set ? ≝
66  λA: Type[0].
67  λglobals: list ident.
68  λlabels: identifier_set ?.
69  λfunct: A × (lin_function globals).
70    labels ∪ (function_labels ? globals funct).
71
72(* CSC: here we are silently throwing away the region information *)
73definition program_labels ≝
74 λprogram: lin_program.
75    foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program)))
76              ∅ (prog_funct … program).
77 
78definition data_of_int ≝ λbv. DATA bv.
79definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
80definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
81
82definition translate_statements ≝
83  λglobals: list (ident × nat).
84  λglobals_old: list ident.
85  λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals).
86  λstatement: pre_lin_statement globals_old.
87  match statement with
88  [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl)
89  | RETURN ⇒ Instruction (RET ?)
90  | sequential instr _ ⇒
91      match instr with
92      [ extension ext ⇒ ⊥
93      | COMMENT comment ⇒ Comment comment
94      | COST_LABEL lbl ⇒ Cost (toASM_ident ? lbl)
95      | POP _ ⇒ Instruction (POP ? accumulator_address)
96      | PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
97      | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
98      | CALL_ID f _ _ ⇒ Call (toASM_ident ? f)
99      | OPACCS accs _ _ _ _ ⇒
100        match accs with
101        [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
102        | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
103        ]
104      | OP1 op1 _ _ ⇒
105        match op1 with
106        [ Cmpl ⇒ Instruction (CPL ? ACC_A)
107        | Inc ⇒ Instruction (INC ? ACC_A)
108        ]
109      | OP2 op2 _ _ reg ⇒
110        match op2 with
111        [ Add ⇒
112          let reg' ≝ register_address reg in
113          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
114                                                         direct;
115                                                         registr ]] x) → ? with
116          [ ACC_A ⇒ λacc_a: True.
117            Instruction (ADD ? ACC_A accumulator_address)
118          | DIRECT d ⇒ λdirect1: True.
119            Instruction (ADD ? ACC_A (DIRECT d))
120          | REGISTER r ⇒ λregister1: True.
121            Instruction (ADD ? ACC_A (REGISTER r))
122          | _ ⇒ λother: False. ⊥
123          ] (subaddressing_modein … reg')
124        | Addc ⇒
125          let reg' ≝ register_address reg in
126          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
127                                                         direct;
128                                                         registr ]] x) → ? with
129          [ ACC_A ⇒ λacc_a: True.
130            Instruction (ADDC ? ACC_A accumulator_address)
131          | DIRECT d ⇒ λdirect2: True.
132            Instruction (ADDC ? ACC_A (DIRECT d))
133          | REGISTER r ⇒ λregister2: True.
134            Instruction (ADDC ? ACC_A (REGISTER r))
135          | _ ⇒ λother: False. ⊥
136          ] (subaddressing_modein … reg')
137        | Sub ⇒
138          let reg' ≝ register_address reg in
139          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
140                                                         direct;
141                                                         registr ]] x) → ? with
142          [ ACC_A ⇒ λacc_a: True.
143            Instruction (SUBB ? ACC_A accumulator_address)
144          | DIRECT d ⇒ λdirect3: True.
145            Instruction (SUBB ? ACC_A (DIRECT d))
146          | REGISTER r ⇒ λregister3: True.
147            Instruction (SUBB ? ACC_A (REGISTER r))
148          | _ ⇒ λother: False. ⊥
149          ] (subaddressing_modein … reg')
150        | And ⇒
151          let reg' ≝ register_address reg in
152          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
153                                                         direct;
154                                                         registr ]] x) → ? with
155          [ ACC_A ⇒ λacc_a: True.
156            Instruction (NOP ?)
157          | DIRECT d ⇒ λdirect4: True.
158            Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
159          | REGISTER r ⇒ λregister4: True.
160            Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
161          | _ ⇒ λother: False. ⊥
162          ] (subaddressing_modein … reg')
163        | Or ⇒
164          let reg' ≝ register_address reg in
165          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
166                                                         direct;
167                                                         registr ]] x) → ? with
168          [ ACC_A ⇒ λacc_a: True.
169            Instruction (NOP ?)
170          | DIRECT d ⇒ λdirect5: True.
171            Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
172          | REGISTER r ⇒ λregister5: True.
173            Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
174          | _ ⇒ λother: False. ⊥
175          ] (subaddressing_modein … reg')
176        | Xor ⇒
177          let reg' ≝ register_address reg in
178          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
179                                                         direct;
180                                                         registr ]] x) → ? with
181          [ ACC_A ⇒ λacc_a: True.
182            Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
183          | DIRECT d ⇒ λdirect6: True.
184            Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
185          | REGISTER r ⇒ λregister6: True.
186            Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
187          | _ ⇒ λother: False. ⊥
188          ] (subaddressing_modein … reg')
189        ]
190      | INT reg byte ⇒
191        let reg' ≝ register_address reg in
192          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
193                                                         direct;
194                                                         registr ]] x) → ? with
195          [ REGISTER r ⇒ λregister7: True.
196            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉))))))
197          | ACC_A ⇒ λacc: True.
198            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉))))))
199          | DIRECT d ⇒ λdirect7: True.
200            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉)))))
201          | _ ⇒ λother: False. ⊥
202          ] (subaddressing_modein … reg')
203      | MOVE regs ⇒
204         match regs with
205          [ from_acc reg ⇒
206             let reg' ≝ register_address reg in
207               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
208                                                              direct;
209                                                              registr ]] x) → ? with
210               [ REGISTER r ⇒ λregister8: True.
211                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
212               | ACC_A ⇒ λacc: True.
213                 Instruction (NOP ?)
214               | DIRECT d ⇒ λdirect8: True.
215                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
216               | _ ⇒ λother: False. ⊥
217               ] (subaddressing_modein … reg')
218          | to_acc reg ⇒
219             let reg' ≝ register_address reg in
220               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
221                                                              direct;
222                                                              registr ]] x) → ? with
223               [ REGISTER r ⇒ λregister9: True.
224                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
225               | DIRECT d ⇒ λdirect9: True.
226                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
227               | ACC_A ⇒ λacc_a: True.
228                 Instruction (NOP ?)
229               | _ ⇒ λother: False. ⊥
230               ] (subaddressing_modein … reg')]
231      | LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
232      | STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
233      | ADDRESS addr proof _ _ ⇒
234        let look ≝ association addr globals (prf ? proof) in
235          Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
236      | COND _ lbl ⇒
237        (* dpm: this should be handled in translate_code! *)
238        Instruction (JNZ ? (toASM_ident ? lbl))
239      | SET_CARRY ⇒
240        Instruction (SETB ? CARRY)
241      ]
242    ].
243  try assumption
244  try @ I
245qed.
246
247(*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *)
248definition ident_of_label: label → Identifier ≝
249 toASM_ident LabelTag.
250
251definition build_translated_statement ≝
252  λglobals.
253  λglobals_old.
254  λprf.
255  λstatement: lin_statement globals_old.
256    〈option_map … ident_of_label (\fst statement), translate_statements globals globals_old prf (\snd statement)〉.
257
258definition translate_code ≝
259  λglobals: list (ident × nat).
260  λglobals_old: list ident.
261  λprf.
262  λcode: list (lin_statement globals_old).
263    map ? ? (build_translated_statement globals globals_old prf) code.
264
265definition translate_fun_def ≝
266  λglobals: list (ident × nat).
267  λglobals_old.
268  λprf.
269  λid_def.
270    let 〈id, def〉 ≝ id_def in
271    match def with
272    [ Internal int ⇒
273      let code ≝ joint_if_code … (lin_params globals_old) int in
274      match translate_code globals globals_old prf code with
275      [ nil ⇒ ⊥
276      | cons hd tl ⇒
277        let rest ≝ 〈Some ? (toASM_ident SymbolTag id), \snd hd〉 :: tl in
278          map ? ? (
279            λr.
280            match fst ? ? r with
281            [ Some id' ⇒ 〈Some ? (toASM_ident ? id'), snd ? ? r〉
282            | None ⇒ 〈None ?, \snd r〉
283            ]) rest
284      ]
285    | External _ ⇒ [ ]
286    ].
287cases daemon (*CSC: XXX will be fixed by an invariant later *)
288qed.
289
290definition translate_functs ≝
291  λglobals.
292  λglobals_old.
293  λprf.
294  λexit_label.
295  λmain.
296  λfuncts.
297  let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in
298   preamble @
299    (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
300
301(*CSC: region silently thrown away here *)
302definition globals_addr ≝
303 λl.
304  let globals_addr_internal ≝
305   λres_offset.
306   λx_size: ident × region × nat.
307    let 〈res, offset〉 ≝ res_offset in
308    let 〈x, region, size〉 ≝ x_size in
309      〈〈x, offset〉 :: res, offset + size〉
310  in
311    \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).
312
313(* dpm: plays the role of the string "_exit" in the O'caml source *)
314axiom identifier_prefix: Identifier.
315(*CSC: XXXXXXX wrong anyway since labels from different functions can now
316  clash with each other and with names of functions *)
317axiom fresh_prefix: identifier_set ASMTag → Identifier → Identifier.
318
319(* dpm: fresh prefix stuff needs unifying with brian *)
320definition translate : lin_program → pseudo_assembly_program ≝
321  λp.
322  let prog_lbls ≝ program_labels … p in
323  let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
324  let global_addr ≝ globals_addr (prog_vars … p) in
325  let global_addr' ≝ map ?? (λx_off. let 〈x,off〉 ≝ x_off in 〈toASM_ident ? x,off〉) global_addr in
326    〈global_addr', translate_functs global_addr (prog_var_names … p) ? exit_label (toASM_ident … (prog_main … p)) (prog_funct … p)〉.
327 #i normalize nodelta -global_addr' global_addr exit_label prog_lbls;
328 normalize in match prog_var_names normalize nodelta
329 elim (prog_vars … p) //
330 #hd #tl #IH whd in ⊢ (% → %)
331 whd in match globals_addr normalize nodelta
332 whd in match (foldl ???? (hd::tl)) normalize nodelta
333 cases hd * #id #reg #size normalize nodelta
334 cases daemon (*CSC: provable using a pair of lemmas over foldl *)
335qed.
Note: See TracBrowser for help on using the repository browser.