source: src/LIN/LINToASM.ma @ 1149

Last change on this file since 1149 was 1149, checked in by mulligan, 10 years ago

changes to get everything type checking again after changing names of registers in i8051

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