source: src/LIN/LINToASM.ma @ 1379

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

Invariant on LIN code removed. In Paris it was decided that a simpler invariant
(to be added later) holds: every function in graph format starts with a
label that is equal to the name of the funciton.

File size: 13.9 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    [ sequential instr' _ ⇒
34      match instr' with
35      [ COST_LABEL lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
36      | COND acc_a_reg lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
37      | _ ⇒ set_empty ?
38      ]
39    | RETURN ⇒ set_empty ?
40    | 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(* dpm: A = Identifier *)
54definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝
55  λA: Type[0].
56  λglobals: list ident.
57  λf: A × (lin_function globals).
58  let 〈ignore, fun_def〉 ≝ f in
59  match fun_def return λ_. BitVectorTrieSet ? with
60  [ Internal stmts ⇒
61      foldl ? ? (function_labels_internal globals) (set_empty ?) (joint_if_code ?? stmts)
62  | External _ ⇒ set_empty ?
63  ].
64 
65definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet ? ≝
66  λA: Type[0].
67  λglobals: list ident.
68  λlabels: BitVectorTrieSet ?.
69  λfunct: A × (lin_function globals).
70    set_union ? labels (function_labels ? globals funct).
71
72(* CSC: here we are silently throwing away the region information *)
73definition program_labels ≝
74 λprogram: lin_program.
75    foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program)))
76              (set_empty …) (prog_funct … 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
82definition translate_statements ≝
83  λglobals: list (ident × nat).
84  λglobals_old: list ident.
85  λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals).
86  λstatement: pre_lin_statement globals_old.
87  match statement with
88  [ GOTO lbl ⇒ Jmp (word_of_identifier ? lbl)
89  | RETURN ⇒ Instruction (RET ?)
90  | sequential instr _ ⇒
91      match instr with
92      [ extension ext ⇒ ⊥
93      | COMMENT comment ⇒ Comment comment
94      | COST_LABEL lbl ⇒ Cost (word_of_identifier ? lbl)
95      | POP _ ⇒ Instruction (POP ? accumulator_address)
96      | PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
97      | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
98      | CALL_ID f _ _ ⇒ Call (word_of_identifier ? f)
99      | OPACCS accs _ _ _ _ ⇒
100        match accs with
101        [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
102        | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
103        ]
104      | OP1 op1 _ _ ⇒
105        match op1 with
106        [ Cmpl ⇒ Instruction (CPL ? ACC_A)
107        | Inc ⇒ Instruction (INC ? ACC_A)
108        ]
109      | OP2 op2 _ _ reg ⇒
110        match op2 with
111        [ Add ⇒
112          let reg' ≝ register_address reg in
113          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
114                                                         direct;
115                                                         registr ]] x) → ? with
116          [ ACC_A ⇒ λacc_a: True.
117            Instruction (ADD ? ACC_A accumulator_address)
118          | DIRECT d ⇒ λdirect1: True.
119            Instruction (ADD ? ACC_A (DIRECT d))
120          | REGISTER r ⇒ λregister1: True.
121            Instruction (ADD ? ACC_A (REGISTER r))
122          | _ ⇒ λother: False. ⊥
123          ] (subaddressing_modein … reg')
124        | Addc ⇒
125          let reg' ≝ register_address reg in
126          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
127                                                         direct;
128                                                         registr ]] x) → ? with
129          [ ACC_A ⇒ λacc_a: True.
130            Instruction (ADDC ? ACC_A accumulator_address)
131          | DIRECT d ⇒ λdirect2: True.
132            Instruction (ADDC ? ACC_A (DIRECT d))
133          | REGISTER r ⇒ λregister2: True.
134            Instruction (ADDC ? ACC_A (REGISTER r))
135          | _ ⇒ λother: False. ⊥
136          ] (subaddressing_modein … reg')
137        | Sub ⇒
138          let reg' ≝ register_address reg in
139          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
140                                                         direct;
141                                                         registr ]] x) → ? with
142          [ ACC_A ⇒ λacc_a: True.
143            Instruction (SUBB ? ACC_A accumulator_address)
144          | DIRECT d ⇒ λdirect3: True.
145            Instruction (SUBB ? ACC_A (DIRECT d))
146          | REGISTER r ⇒ λregister3: True.
147            Instruction (SUBB ? ACC_A (REGISTER r))
148          | _ ⇒ λother: False. ⊥
149          ] (subaddressing_modein … reg')
150        | And ⇒
151          let reg' ≝ register_address reg in
152          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
153                                                         direct;
154                                                         registr ]] x) → ? with
155          [ ACC_A ⇒ λacc_a: True.
156            Instruction (NOP ?)
157          | DIRECT d ⇒ λdirect4: True.
158            Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
159          | REGISTER r ⇒ λregister4: True.
160            Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
161          | _ ⇒ λother: False. ⊥
162          ] (subaddressing_modein … reg')
163        | Or ⇒
164          let reg' ≝ register_address reg in
165          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
166                                                         direct;
167                                                         registr ]] x) → ? with
168          [ ACC_A ⇒ λacc_a: True.
169            Instruction (NOP ?)
170          | DIRECT d ⇒ λdirect5: True.
171            Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
172          | REGISTER r ⇒ λregister5: True.
173            Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
174          | _ ⇒ λother: False. ⊥
175          ] (subaddressing_modein … reg')
176        | Xor ⇒
177          let reg' ≝ register_address reg in
178          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
179                                                         direct;
180                                                         registr ]] x) → ? with
181          [ ACC_A ⇒ λacc_a: True.
182            Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
183          | DIRECT d ⇒ λdirect6: True.
184            Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
185          | REGISTER r ⇒ λregister6: True.
186            Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
187          | _ ⇒ λother: False. ⊥
188          ] (subaddressing_modein … reg')
189        ]
190      | INT reg byte ⇒
191        let reg' ≝ register_address reg in
192          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
193                                                         direct;
194                                                         registr ]] x) → ? with
195          [ REGISTER r ⇒ λregister7: True.
196            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉))))))
197          | ACC_A ⇒ λacc: True.
198            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉))))))
199          | DIRECT d ⇒ λdirect7: True.
200            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉)))))
201          | _ ⇒ λother: False. ⊥
202          ] (subaddressing_modein … reg')
203      | MOVE regs ⇒
204         match regs with
205          [ 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          | 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      | LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
232      | STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
233      | ADDRESS addr proof _ _ ⇒
234        let look ≝ association addr globals (prf ? proof) in
235          Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
236      | COND _ lbl ⇒
237        (* dpm: this should be handled in translate_code! *)
238        Instruction (JNZ ? (word_of_identifier ? lbl))
239      | SET_CARRY ⇒
240        Instruction (SETB ? CARRY)
241      ]
242    ].
243  try assumption
244  try @ I
245qed.
246
247(*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *)
248definition ident_of_label: label → ident ≝
249 λl. an_identifier … (word_of_identifier … l).
250
251definition build_translated_statement ≝
252  λglobals.
253  λglobals_old.
254  λprf.
255  λstatement: lin_statement globals_old.
256    〈option_map … ident_of_label (\fst statement), translate_statements globals globals_old prf (\snd statement)〉.
257
258definition translate_code ≝
259  λglobals: list (ident × nat).
260  λglobals_old: list ident.
261  λprf.
262  λcode: list (lin_statement globals_old).
263    map ? ? (build_translated_statement globals globals_old prf) code.
264
265definition translate_fun_def ≝
266  λglobals: list (ident × nat).
267  λglobals_old.
268  λprf.
269  λid_def.
270    let 〈id, def〉 ≝ id_def in
271    match def with
272    [ Internal int ⇒
273      let code ≝ joint_if_code … (lin_params globals_old) int in
274      match translate_code globals globals_old prf code with
275      [ nil ⇒ ⊥
276      | cons hd tl ⇒
277        let rest ≝ 〈Some ? id, \snd hd〉 :: tl in
278          map ? ? (
279            λr.
280            match fst ? ? r with
281            [ Some id' ⇒ 〈Some ? (word_of_identifier ? id'), snd ? ? r〉
282            | None ⇒ 〈None ?, \snd r〉
283            ]) rest
284      ]
285    | External _ ⇒ [ ]
286    ].
287cases daemon (*CSC: XXX will be fixed by an invariant later *)
288qed.
289   
290definition translate_functs ≝
291  λglobals.
292  λglobals_old.
293  λprf.
294  λexit_label.
295  λmain.
296  λfuncts.
297  let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in
298   preamble @
299    (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
300
301(*CSC: region silently thrown away here *)
302definition globals_addr ≝
303 λl.
304  let globals_addr_internal ≝
305   λres_offset.
306   λx_size: ident × region × nat.
307    let 〈res, offset〉 ≝ res_offset in
308    let 〈x, region, size〉 ≝ x_size in
309      〈〈x, offset〉 :: res, offset + size〉
310  in
311    \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).
312
313(* dpm: plays the role of the string "_exit" in the O'caml source *)
314axiom identifier_prefix: Word.
315(*CSC: XXXXXXX wrong anyway since labels from different functions can now
316  clash with each other and with names of functions *)
317axiom fresh_prefix: BitVectorTrieSet 16 → Word → Word.
318
319(* dpm: fresh prefix stuff needs unifying with brian *)
320definition translate : lin_program → pseudo_assembly_program ≝
321  λp.
322  let prog_lbls ≝ program_labels … p in
323  let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
324  let global_addr ≝ globals_addr (prog_vars … p) in
325  let global_addr' ≝ map ?? (λx_off. let 〈x,off〉 ≝ x_off in 〈word_of_identifier ? x,off〉) global_addr in
326    〈global_addr', translate_functs global_addr (prog_var_names … p) ? exit_label (word_of_identifier … (prog_main … p)) (prog_funct … p)〉.
327 #i normalize nodelta -global_addr' global_addr exit_label prog_lbls;
328 normalize in match prog_var_names normalize nodelta
329 elim (prog_vars … p) //
330 #hd #tl #IH whd in ⊢ (% → %)
331 whd in match globals_addr normalize nodelta
332 whd in match (foldl ???? (hd::tl)) normalize nodelta
333 cases hd * #id #reg #size normalize nodelta
334 cases daemon (*CSC: provable using a pair of lemmas over foldl *)
335qed.
Note: See TracBrowser for help on using the repository browser.