source: src/LIN/LINToASM.ma @ 1268

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

1) AST/Identifier.ma no longer used, utilities/IdentifierTools no longer used
2) LIN/LINToAsm porting completed but:

a) a small lemma need to be proved (easy, but boring because of foldl)
b) the code is BUGGED: labels coming from different universes

(for function names and for each function) are merged together.
However, they should be kept clearly separate. We will discuss how
to fix this issue at the next meeting in Paris.
Note: keeping 'em distinct from the very beginning also requires some
work, since some labels are entered directly by the user.

File size: 14.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    [ joint_st_sequential instr' _ ⇒
34      match instr' with
35      [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
36      | joint_instr_cond acc_a_reg lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
37      | _ ⇒ set_empty ?
38      ]
39    | joint_st_return ⇒ set_empty ?
40    | joint_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) ]
41  in
42  match label with
43  [ None ⇒ generated
44  | Some lbl ⇒ set_insert ? (word_of_identifier ? lbl) generated
45  ].
46
47definition function_labels_internal ≝
48  λglobals: list ident.
49  λlabels: BitVectorTrieSet ?.
50  λstatement: lin_statement globals.
51    set_union ? labels (statement_labels globals statement).
52
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 globals).
59  let 〈ignore, fun_def〉 ≝ f in
60  match fun_def return λ_. BitVectorTrieSet ? with
61  [ Internal stmts ⇒
62      foldl ? ? (function_labels_internal globals) (set_empty ?) (pi1 … (joint_if_code ?? stmts))
63  | 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 globals).
71    set_union ? labels (function_labels ? globals funct).
72
73(* CSC: here we are silently throwing away the region information *)
74definition program_labels ≝
75 λprogram: lin_program.
76    foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program)))
77              (set_empty …) (prog_funct … 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
83definition translate_statements ≝
84  λglobals: list (ident × nat).
85  λglobals_old: list ident.
86  λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals).
87  λstatement: pre_lin_statement globals_old.
88  match statement with
89  [ joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
90  | joint_st_return ⇒ Instruction (RET ?)
91  | joint_st_sequential instr _ ⇒
92      match instr with
93      [ joint_instr_extension ext ⇒ ⊥
94      | joint_instr_comment comment ⇒ Comment comment
95      | joint_instr_cost_label lbl ⇒ Cost (word_of_identifier ? 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        | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
104        ]
105      | joint_instr_op1 op1 _ _ ⇒
106        match op1 with
107        [ Cmpl ⇒ Instruction (CPL ? ACC_A)
108        | Inc ⇒ Instruction (INC ? ACC_A)
109        ]
110      | joint_instr_op2 op2 _ _ reg ⇒
111        match op2 with
112        [ Add ⇒
113          let reg' ≝ register_address reg in
114          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
115                                                         direct;
116                                                         registr ]] x) → ? with
117          [ ACC_A ⇒ λacc_a: True.
118            Instruction (ADD ? ACC_A accumulator_address)
119          | DIRECT d ⇒ λdirect1: True.
120            Instruction (ADD ? ACC_A (DIRECT d))
121          | REGISTER r ⇒ λregister1: True.
122            Instruction (ADD ? ACC_A (REGISTER r))
123          | _ ⇒ λother: False. ⊥
124          ] (subaddressing_modein … reg')
125        | Addc ⇒
126          let reg' ≝ register_address reg in
127          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
128                                                         direct;
129                                                         registr ]] x) → ? with
130          [ ACC_A ⇒ λacc_a: True.
131            Instruction (ADDC ? ACC_A accumulator_address)
132          | DIRECT d ⇒ λdirect2: True.
133            Instruction (ADDC ? ACC_A (DIRECT d))
134          | REGISTER r ⇒ λregister2: True.
135            Instruction (ADDC ? ACC_A (REGISTER r))
136          | _ ⇒ λother: False. ⊥
137          ] (subaddressing_modein … reg')
138        | Sub ⇒
139          let reg' ≝ register_address reg in
140          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
141                                                         direct;
142                                                         registr ]] x) → ? with
143          [ ACC_A ⇒ λacc_a: True.
144            Instruction (SUBB ? ACC_A accumulator_address)
145          | DIRECT d ⇒ λdirect3: True.
146            Instruction (SUBB ? ACC_A (DIRECT d))
147          | REGISTER r ⇒ λregister3: True.
148            Instruction (SUBB ? ACC_A (REGISTER r))
149          | _ ⇒ λother: False. ⊥
150          ] (subaddressing_modein … reg')
151        | And ⇒
152          let reg' ≝ register_address reg in
153          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
154                                                         direct;
155                                                         registr ]] x) → ? with
156          [ ACC_A ⇒ λacc_a: True.
157            Instruction (NOP ?)
158          | DIRECT d ⇒ λdirect4: True.
159            Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
160          | REGISTER r ⇒ λregister4: True.
161            Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
162          | _ ⇒ λother: False. ⊥
163          ] (subaddressing_modein … reg')
164        | Or ⇒
165          let reg' ≝ register_address reg in
166          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
167                                                         direct;
168                                                         registr ]] x) → ? with
169          [ ACC_A ⇒ λacc_a: True.
170            Instruction (NOP ?)
171          | DIRECT d ⇒ λdirect5: True.
172            Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
173          | REGISTER r ⇒ λregister5: True.
174            Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
175          | _ ⇒ λother: False. ⊥
176          ] (subaddressing_modein … reg')
177        | Xor ⇒
178          let reg' ≝ register_address reg in
179          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
180                                                         direct;
181                                                         registr ]] x) → ? with
182          [ ACC_A ⇒ λacc_a: True.
183            Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
184          | DIRECT d ⇒ λdirect6: True.
185            Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
186          | REGISTER r ⇒ λregister6: True.
187            Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
188          | _ ⇒ λother: False. ⊥
189          ] (subaddressing_modein … reg')
190        ]
191      | joint_instr_int reg byte ⇒
192        let reg' ≝ register_address reg in
193          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
194                                                         direct;
195                                                         registr ]] x) → ? with
196          [ REGISTER r ⇒ λregister7: True.
197            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉))))))
198          | ACC_A ⇒ λacc: True.
199            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉))))))
200          | DIRECT d ⇒ λdirect7: True.
201            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉)))))
202          | _ ⇒ λother: False. ⊥
203          ] (subaddressing_modein … reg')
204      | joint_instr_move regs ⇒
205         match regs with
206          [ from_acc reg ⇒
207             let reg' ≝ register_address reg in
208               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
209                                                              direct;
210                                                              registr ]] x) → ? with
211               [ REGISTER r ⇒ λregister8: True.
212                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
213               | ACC_A ⇒ λacc: True.
214                 Instruction (NOP ?)
215               | DIRECT d ⇒ λdirect8: True.
216                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
217               | _ ⇒ λother: False. ⊥
218               ] (subaddressing_modein … reg')
219          | to_acc reg ⇒
220             let reg' ≝ register_address reg in
221               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
222                                                              direct;
223                                                              registr ]] x) → ? with
224               [ REGISTER r ⇒ λregister9: True.
225                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
226               | DIRECT d ⇒ λdirect9: True.
227                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
228               | ACC_A ⇒ λacc_a: True.
229                 Instruction (NOP ?)
230               | _ ⇒ λother: False. ⊥
231               ] (subaddressing_modein … reg')]
232      | joint_instr_load _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
233      | joint_instr_store _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
234      | joint_instr_address addr proof _ _ ⇒
235        let look ≝ association addr globals (prf ? proof) in
236          Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
237      | joint_instr_cond _ lbl ⇒
238        (* dpm: this should be handled in translate_code! *)
239        Instruction (JNZ ? (word_of_identifier ? lbl))
240      | joint_instr_set_carry ⇒
241        Instruction (SETB ? CARRY)
242      ]
243    ].
244  try assumption
245  try @ I
246qed.
247
248(*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *)
249definition ident_of_label: label → ident ≝
250 λl. an_identifier … (word_of_identifier … l).
251
252definition build_translated_statement ≝
253  λglobals.
254  λglobals_old.
255  λprf.
256  λstatement: lin_statement globals_old.
257    〈option_map … ident_of_label (\fst statement), translate_statements globals globals_old prf (\snd statement)〉.
258
259definition translate_code ≝
260  λglobals: list (ident × nat).
261  λglobals_old: list ident.
262  λprf.
263  λcode: list (lin_statement globals_old).
264    map ? ? (build_translated_statement globals globals_old prf) code.
265   
266lemma translate_code_preserves_WellFormedP:
267  ∀globals, globals_old, prf, code.
268    well_formed_P ? ? code → well_formed_P ? ? (translate_code globals globals_old prf code).
269  #G #GO #P #C
270  elim C
271  [ normalize
272    //
273  | #G2 #G02 #IH (* CSC: understand here *)
274    whd in ⊢ (% → %) whd in match build_translated_statement normalize nodelta
275    cases (\fst G2) normalize // ]
276qed.
277
278definition translate_fun_def ≝
279  λglobals: list (ident × nat).
280  λglobals_old.
281  λprf.
282  λid_def.
283    let 〈id, def〉 ≝ id_def in
284    match def with
285    [ Internal int ⇒
286      let code_proof ≝ joint_if_code … (lin_params globals_old) int in
287      match translate_code globals globals_old prf (pi1 ?? code_proof) return λtranscode. well_formed_P ? ? transcode → list labelled_instruction with
288      [ nil ⇒ λprf2. ⊥
289      | cons hd tl ⇒ λ_.
290        let rest ≝ 〈Some ? id, \snd hd〉 :: tl in
291          map ? ? (
292            λr.
293            match fst ? ? r with
294            [ Some id' ⇒ 〈Some ? (word_of_identifier ? id'), snd ? ? r〉
295            | None ⇒ 〈None ?, \snd r〉
296            ]) rest
297      ] (translate_code_preserves_WellFormedP globals globals_old prf (pi1 ?? code_proof) (pi2 ?? code_proof))
298    | External _ ⇒ [ ]
299    ].
300@prf2
301qed.
302   
303definition translate_functs ≝
304  λglobals.
305  λglobals_old.
306  λprf.
307  λexit_label.
308  λmain.
309  λfuncts.
310  let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in
311   preamble @
312    (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
313
314(*CSC: region silently thrown away here *)
315definition globals_addr ≝
316 λl.
317  let globals_addr_internal ≝
318   λres_offset.
319   λx_size: ident × region × nat.
320    let 〈res, offset〉 ≝ res_offset in
321    let 〈x, region, size〉 ≝ x_size in
322      〈〈x, offset〉 :: res, offset + size〉
323  in
324    \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).
325
326(* dpm: plays the role of the string "_exit" in the O'caml source *)
327axiom identifier_prefix: Word.
328(*CSC: XXXXXXX wrong anyway since labels from different functions can now
329  clash with each other and with names of functions *)
330axiom fresh_prefix: BitVectorTrieSet 16 → Word → Word.
331
332(* dpm: fresh prefix stuff needs unifying with brian *)
333definition translate : lin_program → pseudo_assembly_program ≝
334  λp.
335  let prog_lbls ≝ program_labels … p in
336  let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
337  let global_addr ≝ globals_addr (prog_vars … p) in
338  let global_addr' ≝ map ?? (λx_off. let 〈x,off〉 ≝ x_off in 〈word_of_identifier ? x,off〉) global_addr in
339    〈global_addr', translate_functs global_addr (prog_var_names … p) ? exit_label (word_of_identifier … (prog_main … p)) (prog_funct … p)〉.
340 #i normalize nodelta -global_addr' global_addr exit_label prog_lbls;
341 normalize in match prog_var_names normalize nodelta
342 elim (prog_vars … p) //
343 #hd #tl #IH whd in ⊢ (% → %)
344 whd in match globals_addr normalize nodelta
345 whd in match (foldl ???? (hd::tl)) normalize nodelta
346 cases hd * #id #reg #size normalize nodelta
347 cases daemon (*CSC: provable using a pair of lemmas over foldl *)
348qed.
Note: See TracBrowser for help on using the repository browser.