source: src/LIN/LINToASM.ma @ 1052

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

Lots more fixing to get both front and backends using same conventions and types.

File size: 13.3 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_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
41    | joint_st_return ⇒ set_empty ?
42    ] in
43  match label with
44  [ None ⇒ generated
45  | Some lbl ⇒ set_insert ? (word_of_identifier ? lbl) generated
46  ].
47
48definition function_labels_internal ≝
49  λglobals: list ident.
50  λlabels: BitVectorTrieSet ?.
51  λstatement: lin_statement globals.
52    set_union ? labels (statement_labels globals statement).
53
54(* dpm: A = Identifier *)
55definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝
56  λA: Type[0].
57  λglobals: list ident.
58  λf: A × (lin_function_definition globals).
59  let 〈ignore, fun_def〉 ≝ f in
60  match fun_def return λ_. BitVectorTrieSet ? with
61  [ lin_fu_internal stmts proof ⇒
62      foldl ? ? (function_labels_internal globals) (set_empty ?) stmts
63  | lin_fu_external _ ⇒ set_empty ?
64  ].
65 
66definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet ? ≝
67  λA: Type[0].
68  λglobals: list ident.
69  λlabels: BitVectorTrieSet ?.
70  λfunct: A × (lin_function_definition globals).
71    set_union ? labels (function_labels ? globals funct).
72   
73definition program_labels ≝
74  λprogram.
75    foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) (lin_pr_vars program)))
76              (set_empty ?) (lin_pr_funcs 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
82axiom ImplementedInRuntime: False.
83
84definition translate_statements ≝
85  λglobals: list (ident × nat).
86  λglobals_old: list ident.
87  λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals).
88  λstatement: pre_lin_statement globals_old.
89  match statement with
90  [ joint_st_return ⇒ Instruction (RET ?)
91  | joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
92  | joint_st_sequential instr _ ⇒
93    match instr with
94    [ joint_instr_comment comment ⇒ Comment comment
95    | joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl)
96    | joint_instr_pop ⇒ Instruction (POP ? accumulator_address)
97    | joint_instr_push ⇒ Instruction (PUSH ? accumulator_address)
98    | joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY)
99    | joint_instr_call_id f ⇒ Call (word_of_identifier ? f)
100    | joint_instr_opaccs accs ⇒
101      match accs with
102      [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
103      | Divu ⇒ Instruction (DIV ? ACC_A ACC_B)
104      | Modu ⇒ ?
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 (Register_of_register 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 (Register_of_register 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 (Register_of_register 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 (Register_of_register 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 (Register_of_register 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 (Register_of_register 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 (Register_of_register 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 (Register_of_register 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 (Register_of_register 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      WithLabel (JNZ ? (word_of_identifier ? lbl))
239    ]
240  ].
241  try assumption
242  try @ I
243  cases ImplementedInRuntime
244qed.
245
246definition build_translated_statement ≝
247  λglobals.
248  λglobals_old.
249  λprf.
250  λstatement: lin_statement globals_old.
251    〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉.
252
253definition translate_code ≝
254  λglobals: list (ident × nat).
255  λglobals_old: list ident.
256  λprf.
257  λcode: list (lin_statement globals_old).
258    map ? ? (build_translated_statement globals globals_old prf) code.
259   
260lemma translate_code_preserves_WellFormedP:
261  ∀globals, globals_old, prf, code.
262    well_formed_P ? ? code → well_formed_P ? ? (translate_code globals globals_old prf code).
263  #G #GO #P #C
264  elim C
265  [ normalize
266    //
267  | #G2 #G02 #IH (* CSC: understand here *)
268    whd in ⊢ (% → %)
269    normalize in ⊢ (% → %)
270    //
271  ]
272qed.
273
274definition translate_fun_def ≝
275  λglobals.
276  λglobals_old.
277  λprf.
278  λid_def.
279    let 〈id, def〉 ≝ id_def in
280    match def with
281    [ lin_fu_internal code proof ⇒
282      match translate_code globals globals_old prf code return λtranscode. well_formed_P ? ? transcode → list labelled_instruction with
283      [ nil ⇒ λprf2. ⊥
284      | cons hd tl ⇒ λ_.
285        let rest ≝ 〈Some ? id, \snd hd〉 :: tl in
286          map ? ? (
287            λr.
288            match fst ? ? r with
289            [ Some id' ⇒ 〈Some ? (word_of_identifier ? id'), snd ? ? r〉
290            | None ⇒ 〈None ?, \snd r〉
291            ]) rest
292      ] (translate_code_preserves_WellFormedP globals globals_old prf code proof)
293    | _ ⇒ [ ]
294    ].
295    @ prf2
296qed.
297   
298definition translate_functs ≝
299  λglobals.
300  λglobals_old.
301  λprf.
302  λexit_label.
303  λmain.
304  λfuncts.
305  let preamble ≝
306    match main with
307    [ None ⇒ [ ]
308    | Some main' ⇒ [ 〈None ?, Call main'〉 ; 〈Some ? exit_label, Jmp exit_label〉 ]
309    ] in
310      preamble @ (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
311
312definition globals_addr_internal ≝
313  λres_offset.
314  λx_size: Identifier × nat.
315    let 〈res, offset〉 ≝ res_offset in
316    let 〈x, size〉 ≝ x_size in
317      〈〈x, offset〉 :: res, offset + size〉.
318
319definition globals_addr ≝
320  λl.
321    \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).
322     
323(* dpm: plays the role of the string "_exit" in the O'caml source *)
324axiom identifier_prefix: Identifier.
325
326(* dpm: fresh prefix stuff needs unifying with brian *)
327
328(*
329definition translate ≝
330  λp.
331  let prog_lbls ≝ program_labels p in
332  let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
333  let global_addr ≝ globals_addr (LIN_Pr_vars p) in
334    〈global_addr, translate_functs global_addr (map ? ? (fst ? ?) (LIN_Pr_vars p)) ? exit_label (LIN_Pr_main p) (LIN_Pr_funs p)〉.
335*)
Note: See TracBrowser for help on using the repository browser.