source: src/LIN/LINToASM.ma @ 1264

Last change on this file since 1264 was 1264, checked in by sacerdot, 8 years ago

Almost ported to new Joint syntax.

File size: 14.2 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_a_reg 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  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
55(* dpm: A = Identifier *)
56definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝
57  λA: Type[0].
58  λglobals: list ident.
59  λf: A × (lin_function globals).
60  let 〈ignore, fun_def〉 ≝ f in
61  match fun_def return λ_. BitVectorTrieSet ? with
62  [ Internal stmts ⇒
63      foldl ? ? (function_labels_internal globals) (set_empty ?) (pi1 … (joint_if_code ?? stmts))
64  | 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 globals).
72    set_union ? labels (function_labels ? globals funct).
73
74(* CSC: here we are silently throwing away the region information *)
75definition program_labels ≝
76 λprogram: lin_program.
77    foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program)))
78              (set_empty …) (prog_funct … program).
79 
80definition data_of_int ≝ λbv. DATA bv.
81definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
82definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
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_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
91  | joint_st_return ⇒ Instruction (RET ?)
92  | joint_st_sequential instr _ ⇒
93      match instr with
94      [ joint_instr_extension ext ⇒ ⊥
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_move regs ⇒
206         match regs with
207          [ from_acc reg ⇒
208             let reg' ≝ register_address reg in
209               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
210                                                              direct;
211                                                              registr ]] x) → ? with
212               [ REGISTER r ⇒ λregister8: True.
213                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
214               | ACC_A ⇒ λacc: True.
215                 Instruction (NOP ?)
216               | DIRECT d ⇒ λdirect8: True.
217                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
218               | _ ⇒ λother: False. ⊥
219               ] (subaddressing_modein … reg')
220          | to_acc reg ⇒
221             let reg' ≝ register_address reg in
222               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
223                                                              direct;
224                                                              registr ]] x) → ? with
225               [ REGISTER r ⇒ λregister9: True.
226                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
227               | DIRECT d ⇒ λdirect9: True.
228                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
229               | ACC_A ⇒ λacc_a: True.
230                 Instruction (NOP ?)
231               | _ ⇒ λother: False. ⊥
232               ] (subaddressing_modein … reg')]
233      | joint_instr_load _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
234      | joint_instr_store _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
235      | joint_instr_address addr proof _ _ ⇒
236        let look ≝ association addr globals (prf ? proof) in
237          Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
238      | joint_instr_cond _ lbl ⇒
239        (* dpm: this should be handled in translate_code! *)
240        Instruction (JNZ ? (word_of_identifier ? lbl))
241      | joint_instr_set_carry ⇒
242        Instruction (SETB ? CARRY)
243      ]
244    ].
245  try assumption
246  try @ I
247qed.
248
249definition build_translated_statement ≝
250  λglobals.
251  λglobals_old.
252  λprf.
253  λstatement: lin_statement globals_old.
254    〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉.
255
256definition translate_code ≝
257  λglobals: list (ident × nat).
258  λglobals_old: list ident.
259  λprf.
260  λcode: list (lin_statement globals_old).
261    map ? ? (build_translated_statement globals globals_old prf) code.
262   
263lemma translate_code_preserves_WellFormedP:
264  ∀globals, globals_old, prf, code.
265    well_formed_P ? ? code → well_formed_P ? ? (translate_code globals globals_old prf code).
266  #G #GO #P #C
267  elim C
268  [ normalize
269    //
270  | #G2 #G02 #IH (* CSC: understand here *)
271    whd in ⊢ (% → %)
272    normalize in ⊢ (% → %)
273    //
274  ]
275qed.
276
277definition translate_fun_def ≝
278  λglobals.
279  λglobals_old.
280  λprf.
281  λid_def: ? × (fundef … (Σcode:list (lin_statement globals_old).?)).
282    let 〈id, def〉 ≝ id_def in
283    match def with
284    [ Internal code_proof ⇒
285      match translate_code globals globals_old prf (pi1 ?? code_proof) return λtranscode. well_formed_P ? ? transcode → list labelled_instruction with
286      [ nil ⇒ λprf2. ⊥
287      | cons hd tl ⇒ λ_.
288        let rest ≝ 〈Some ? id, \snd hd〉 :: tl in
289          map ? ? (
290            λr.
291            match fst ? ? r with
292            [ Some id' ⇒ 〈Some ? (word_of_identifier ? id'), snd ? ? r〉
293            | None ⇒ 〈None ?, \snd r〉
294            ]) rest
295      ] (translate_code_preserves_WellFormedP globals globals_old prf (pi1 ?? code_proof) (pi2 ?? code_proof))
296    | External _ ⇒ [ ]
297    ].
298@prf2
299qed.
300   
301definition translate_functs ≝
302  λglobals.
303  λglobals_old.
304  λprf.
305  λexit_label.
306  λmain.
307  λfuncts.
308  let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in
309   preamble @ (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
310
311(*CSC: region silently thrown away here *)
312definition globals_addr ≝
313 λl.
314  let globals_addr_internal ≝
315   λres_offset.
316   λx_size: ident × region × nat.
317    let 〈res, offset〉 ≝ res_offset in
318    let 〈x, region, size〉 ≝ x_size in
319      〈〈x, offset〉 :: res, offset + size〉
320  in
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 *)
327definition translate : lin_program → pseudo_assembly_program ≝
328  λp.
329  let prog_lbls ≝ program_labels … p in
330  let exit_label ≝ ?(*fresh_prefix … prog_lbls identifier_prefix*) in
331  let global_addr ≝ globals_addr (prog_vars … p) in
332  let global_addr' ≝ map ?? (λx_off. let 〈x,off〉 ≝ x_off in 〈word_of_identifier ? x,off〉) global_addr in
333    〈global_addr', translate_functs global_addr (prog_var_names … p) ? exit_label (word_of_identifier … (prog_main … p)) ?(*(prog_funct ?? p)*)〉.
334[ generalize in match (prog_funct ?? p) #X whd in X:(?(??%)) whd in X:(?(??(?%)))
335| #i normalize nodelta whd in match prog_var_names normalize nodelta elim (prog_vars … p)
336  [ // | #hd #tl #H1 #H2 normalize in ⊢ (???(????%))   
Note: See TracBrowser for help on using the repository browser.