source: src/LIN/LINToASM.ma @ 1112

Last change on this file since 1112 was 1112, checked in by mulligan, 8 years ago

got lin > asm stuff working

File size: 13.5 KB
Line 
1include "ASM/Util.ma".
2include "utilities/BitVectorTrieSet.ma".
3include "utilities/IdentifierTools.ma".
4include "LIN/LIN.ma".
5 
6let rec association (i: ident) (l: list (ident × nat))
7                    on l: member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat ≝
8  match l return λl. member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat with
9  [ nil ⇒ λabsd. ?
10  | cons hd tl ⇒
11    λprf: member i (eq_identifier ?) (map ? ? (fst ? ?) (cons ? hd tl)).
12      (match eq_identifier ? (\fst hd) i return λb. eq_identifier ? (\fst hd) i = b → nat with
13      [ true ⇒ λeq_prf. \snd hd
14      | false ⇒ λeq_prf. association i tl ?
15      ]) (refl ? (eq_identifier ? (\fst hd) i))
16  ].
17  [ cases absd
18  | cases prf
19    [ > eq_prf
20      # H
21      cases H
22    | # H
23      assumption
24    ]
25  ]
26qed.
27
28definition statement_labels ≝
29  λg: list ident.
30  λs: lin_statement g.
31  let 〈label, instr〉 ≝ s in
32  let generated ≝
33    match instr with
34    [ lin_st_lift l ⇒
35      match l with
36      [ joint_st_sequential instr' _ ⇒
37        match instr' with
38        [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
39        | joint_instr_cond_acc lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
40        | _ ⇒ set_empty ?
41        ]
42      | joint_st_return ⇒ set_empty ?
43      ]
44    | lin_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
45    ]
46  in
47  match label with
48  [ None ⇒ generated
49  | Some lbl ⇒ set_insert ? (word_of_identifier ? lbl) generated
50  ].
51
52definition function_labels_internal ≝
53  λglobals: list ident.
54  λlabels: BitVectorTrieSet ?.
55  λstatement: lin_statement globals.
56    set_union ? labels (statement_labels globals statement).
57
58(* dpm: A = Identifier *)
59definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝
60  λA: Type[0].
61  λglobals: list ident.
62  λf: A × (lin_function_definition globals).
63  let 〈ignore, fun_def〉 ≝ f in
64  match fun_def return λ_. BitVectorTrieSet ? with
65  [ lin_fu_internal stmts proof ⇒
66      foldl ? ? (function_labels_internal globals) (set_empty ?) stmts
67  | lin_fu_external _ ⇒ set_empty ?
68  ].
69 
70definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet ? ≝
71  λA: Type[0].
72  λglobals: list ident.
73  λlabels: BitVectorTrieSet ?.
74  λfunct: A × (lin_function_definition globals).
75    set_union ? labels (function_labels ? globals funct).
76   
77definition program_labels ≝
78  λprogram.
79    foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) (lin_pr_vars program)))
80              (set_empty ?) (lin_pr_funcs program).
81   
82definition data_of_int ≝ λbv. DATA bv.
83definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
84definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
85
86axiom ImplementedInRuntime: False.
87
88definition translate_statements ≝
89  λglobals: list (ident × nat).
90  λglobals_old: list ident.
91  λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals).
92  λstatement: pre_lin_statement globals_old.
93  match statement with
94  [ lin_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
95  | lin_st_lift l ⇒
96    match l with
97    [ joint_st_return ⇒ Instruction (RET ?)
98    | joint_st_sequential instr _ ⇒
99      match instr with
100      [ joint_instr_comment comment ⇒ Comment comment
101      | joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl)
102      | joint_instr_pop ⇒ Instruction (POP ? accumulator_address)
103      | joint_instr_push ⇒ Instruction (PUSH ? accumulator_address)
104      | joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY)
105      | joint_instr_call_id f ⇒ Call (word_of_identifier ? f)
106      | joint_instr_opaccs accs ⇒
107        match accs with
108        [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
109        | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
110        ]
111      | joint_instr_op1 op1 ⇒
112        match op1 with
113        [ Cmpl ⇒ Instruction (CPL ? ACC_A)
114        | Inc ⇒ Instruction (INC ? ACC_A)
115        ]
116      | joint_instr_op2 op2 reg ⇒
117        match op2 with
118        [ Add ⇒
119          let reg' ≝ register_address reg in
120          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
121                                                         direct;
122                                                         registr ]] x) → ? with
123          [ ACC_A ⇒ λacc_a: True.
124            Instruction (ADD ? ACC_A accumulator_address)
125          | DIRECT d ⇒ λdirect1: True.
126            Instruction (ADD ? ACC_A (DIRECT d))
127          | REGISTER r ⇒ λregister1: True.
128            Instruction (ADD ? ACC_A (REGISTER r))
129          | _ ⇒ λother: False. ⊥
130          ] (subaddressing_modein … reg')
131        | Addc ⇒
132          let reg' ≝ register_address reg in
133          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
134                                                         direct;
135                                                         registr ]] x) → ? with
136          [ ACC_A ⇒ λacc_a: True.
137            Instruction (ADDC ? ACC_A accumulator_address)
138          | DIRECT d ⇒ λdirect2: True.
139            Instruction (ADDC ? ACC_A (DIRECT d))
140          | REGISTER r ⇒ λregister2: True.
141            Instruction (ADDC ? ACC_A (REGISTER r))
142          | _ ⇒ λother: False. ⊥
143          ] (subaddressing_modein … reg')
144        | Sub ⇒
145          let reg' ≝ register_address reg in
146          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
147                                                         direct;
148                                                         registr ]] x) → ? with
149          [ ACC_A ⇒ λacc_a: True.
150            Instruction (SUBB ? ACC_A accumulator_address)
151          | DIRECT d ⇒ λdirect3: True.
152            Instruction (SUBB ? ACC_A (DIRECT d))
153          | REGISTER r ⇒ λregister3: True.
154            Instruction (SUBB ? ACC_A (REGISTER r))
155          | _ ⇒ λother: False. ⊥
156          ] (subaddressing_modein … reg')
157        | And ⇒
158          let reg' ≝ register_address reg in
159          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
160                                                         direct;
161                                                         registr ]] x) → ? with
162          [ ACC_A ⇒ λacc_a: True.
163            Instruction (NOP ?)
164          | DIRECT d ⇒ λdirect4: True.
165            Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
166          | REGISTER r ⇒ λregister4: True.
167            Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
168          | _ ⇒ λother: False. ⊥
169          ] (subaddressing_modein … reg')
170        | Or ⇒
171          let reg' ≝ register_address reg in
172          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
173                                                         direct;
174                                                         registr ]] x) → ? with
175          [ ACC_A ⇒ λacc_a: True.
176            Instruction (NOP ?)
177          | DIRECT d ⇒ λdirect5: True.
178            Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
179          | REGISTER r ⇒ λregister5: True.
180            Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
181          | _ ⇒ λother: False. ⊥
182          ] (subaddressing_modein … reg')
183        | Xor ⇒
184          let reg' ≝ register_address reg in
185          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
186                                                         direct;
187                                                         registr ]] x) → ? with
188          [ ACC_A ⇒ λacc_a: True.
189            Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
190          | DIRECT d ⇒ λdirect6: True.
191            Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
192          | REGISTER r ⇒ λregister6: True.
193            Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
194          | _ ⇒ λother: False. ⊥
195          ] (subaddressing_modein … reg')
196        ]
197      | joint_instr_int reg byte ⇒
198        let reg' ≝ register_address reg in
199          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
200                                                         direct;
201                                                         registr ]] x) → ? with
202          [ REGISTER r ⇒ λregister7: True.
203            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉))))))
204          | ACC_A ⇒ λacc: True.
205            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉))))))
206          | DIRECT d ⇒ λdirect7: True.
207            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉)))))
208          | _ ⇒ λother: False. ⊥
209          ] (subaddressing_modein … reg')
210      | joint_instr_from_acc reg ⇒
211        let reg' ≝ register_address reg in
212          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
213                                                         direct;
214                                                         registr ]] x) → ? with
215          [ REGISTER r ⇒ λregister8: True.
216            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
217          | ACC_A ⇒ λacc: True.
218            Instruction (NOP ?)
219          | DIRECT d ⇒ λdirect8: True.
220            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
221          | _ ⇒ λother: False. ⊥
222          ] (subaddressing_modein … reg')
223      | joint_instr_to_acc reg ⇒
224        let reg' ≝ register_address reg in
225          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
226                                                         direct;
227                                                         registr ]] x) → ? with
228          [ REGISTER r ⇒ λregister9: True.
229            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
230          | DIRECT d ⇒ λdirect9: True.
231            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
232          | ACC_A ⇒ λacc_a: True.
233            Instruction (NOP ?)
234          | _ ⇒ λother: False. ⊥
235          ] (subaddressing_modein … reg')
236      | joint_instr_load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
237      | joint_instr_store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
238      | joint_instr_address addr proof ⇒
239        let look ≝ association addr globals (prf ? proof) in
240          Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
241      | joint_instr_cond_acc lbl ⇒
242        (* dpm: this should be handled in translate_code! *)
243        Instruction (JNZ ? (word_of_identifier ? lbl))
244      | joint_instr_set_carry ⇒
245        Instruction (SETB ? CARRY)
246      ]
247    ]
248  ].
249  try assumption
250  try @ I
251  cases ImplementedInRuntime
252qed.
253
254definition build_translated_statement ≝
255  λglobals.
256  λglobals_old.
257  λprf.
258  λstatement: lin_statement globals_old.
259    〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉.
260
261definition translate_code ≝
262  λglobals: list (ident × nat).
263  λglobals_old: list ident.
264  λprf.
265  λcode: list (lin_statement globals_old).
266    map ? ? (build_translated_statement globals globals_old prf) code.
267   
268lemma translate_code_preserves_WellFormedP:
269  ∀globals, globals_old, prf, code.
270    well_formed_P ? ? code → well_formed_P ? ? (translate_code globals globals_old prf code).
271  #G #GO #P #C
272  elim C
273  [ normalize
274    //
275  | #G2 #G02 #IH (* CSC: understand here *)
276    whd in ⊢ (% → %)
277    normalize in ⊢ (% → %)
278    //
279  ]
280qed.
281
282definition translate_fun_def ≝
283  λglobals.
284  λglobals_old.
285  λprf.
286  λid_def.
287    let 〈id, def〉 ≝ id_def in
288    match def with
289    [ lin_fu_internal code proof ⇒
290      match translate_code globals globals_old prf code return λtranscode. well_formed_P ? ? transcode → list labelled_instruction with
291      [ nil ⇒ λprf2. ⊥
292      | cons hd tl ⇒ λ_.
293        let rest ≝ 〈Some ? id, \snd hd〉 :: tl in
294          map ? ? (
295            λr.
296            match fst ? ? r with
297            [ Some id' ⇒ 〈Some ? (word_of_identifier ? id'), snd ? ? r〉
298            | None ⇒ 〈None ?, \snd r〉
299            ]) rest
300      ] (translate_code_preserves_WellFormedP globals globals_old prf code proof)
301    | _ ⇒ [ ]
302    ].
303    @ prf2
304qed.
305   
306definition translate_functs ≝
307  λglobals.
308  λglobals_old.
309  λprf.
310  λexit_label.
311  λmain.
312  λfuncts.
313  let preamble ≝
314    match main with
315    [ None ⇒ [ ]
316    | Some main' ⇒ [ 〈None ?, Call main'〉 ; 〈Some ? exit_label, Jmp exit_label〉 ]
317    ] in
318      preamble @ (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
319
320definition globals_addr_internal ≝
321  λres_offset.
322  λx_size: ident × nat.
323    let 〈res, offset〉 ≝ res_offset in
324    let 〈x, size〉 ≝ x_size in
325      〈〈x, offset〉 :: res, offset + size〉.
326
327definition globals_addr ≝
328  λl.
329    \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).
330     
331(* dpm: plays the role of the string "_exit" in the O'caml source *)
332axiom identifier_prefix: Identifier.
333
334(* dpm: fresh prefix stuff needs unifying with brian *)
335
336(*
337definition translate ≝
338  λp.
339  let prog_lbls ≝ program_labels p in
340  let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
341  let global_addr ≝ globals_addr (LIN_Pr_vars p) in
342    〈global_addr, translate_functs global_addr (map ? ? (fst ? ?) (LIN_Pr_vars p)) ? exit_label (LIN_Pr_main p) (LIN_Pr_funs p)〉.
343*)
Note: See TracBrowser for help on using the repository browser.