source: src/LIN/LINToASM.ma @ 1245

Last change on this file since 1245 was 1245, checked in by sacerdot, 9 years ago

RTLtoERTL and LINToASM: porting to new Joint data type in progress.
However, it seems better to go back to a Joint representation where
the "mapping" from label to internal functions is more concrete.
To be done.

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