source: src/RTL/RTLToERTL.ma @ 1481

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

Proof fixed. The new standard library does not index any longer the lemma
previously used. However, automation should be equally successfull. The reason
it is not is because it does not handle let-ins correctly.

File size: 16.1 KB
Line 
1include "RTL/RTLTailcall.ma".
2include "utilities/RegisterSet.ma".
3include "common/Identifiers.ma".
4include "ERTL/ERTL.ma".
5include "joint/TranslateUtils.ma".
6
7definition save_hdws ≝
8 λglobals,l.
9  let save_hdws_internal ≝
10   λdestr_srcr.λstart_lbl.
11    let 〈destr, srcr〉 ≝ destr_srcr in
12     adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈pseudo destr,hardware srcr〉) ] start_lbl
13  in
14   map ? ? save_hdws_internal l.
15
16definition restore_hdws ≝
17  λglobals,l.
18   let restore_hdws_internal ≝
19    λsrcr_destr: register × Register.
20    λstart_lbl: label.
21     let 〈srcr, destr〉 ≝ srcr_destr in
22     adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈hardware destr, pseudo srcr〉) ] start_lbl
23   in
24    map ? ? restore_hdws_internal l.
25
26definition get_params_hdw ≝
27  λglobals.
28  λparams: list register.
29  match params with
30  [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ GOTO … ] start_lbl]
31  | _ ⇒
32    let l ≝ zip_pottier ? ? params RegisterParams in
33      save_hdws globals l ].
34
35definition get_param_stack ≝
36  λglobals.
37  λoff: nat.
38  λdestr.
39  λstart_lbl, dest_lbl: label.
40  λdef.
41  let 〈def, addr1〉 ≝ fresh_reg … def in
42  let 〈def, addr2〉 ≝ fresh_reg … def in
43  let 〈def, tmpr〉 ≝ fresh_reg … def in
44  let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in
45  adds_graph ertl_params1 globals [
46    sequential ertl_params_ … (extension … (ertl_st_ext_frame_size addr1));
47    sequential ertl_params_ … (INT … tmpr int_offset);
48    sequential ertl_params_ … (OP2 … Sub addr1 addr1 tmpr);
49    sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉);
50    sequential ertl_params_ … (OP2 … Add addr1 addr1 tmpr);
51    sequential ertl_params_ … (INT … addr2 (bitvector_of_nat 8 0));
52    sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉);
53    sequential ertl_params_ … (OP2 … Addc addr2 addr2 tmpr);
54    sequential ertl_params_ … (LOAD … destr addr1 addr2)
55  ] start_lbl dest_lbl def.
56 
57definition get_params_stack ≝
58  λglobals,params.
59  match params with
60  [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl ]
61  | _ ⇒ mapi ? ? (get_param_stack globals) params ].
62
63definition get_params ≝
64  λglobals,params.
65  let n ≝ min (length … params) (length … RegisterParams) in
66  let 〈hdw_params, stack_params〉 ≝ list_split … n params in
67  let hdw_params ≝ get_params_hdw globals hdw_params in
68    hdw_params @ (get_params_stack … stack_params).
69
70definition add_prologue ≝
71  λglobals.
72  λparams: list register.
73  λsral.
74  λsrah.
75  λsregs.
76  λdef.
77  let start_lbl ≝ joint_if_entry … (ertl_params globals) def in
78  let 〈tmp_lbl, def〉 ≝ fresh_label … def in
79  match lookup … (joint_if_code … def) start_lbl
80    return λx. x ≠ None ? → ertl_internal_function globals with
81  [ None ⇒ λnone_absrd. ⊥
82  | Some last_stmt ⇒ λsome_prf.
83    let def ≝
84      add_translates …
85         ((adds_graph ertl_params1 … [
86                     sequential ertl_params_ … (extension ertl_params__ globals ertl_st_ext_new_frame)
87                   ]) ::
88         (adds_graph ertl_params1 … [
89                      sequential ertl_params_ … (POP … sral);
90                      sequential ertl_params_ … (POP … srah)
91                   ]) ::
92         (save_hdws … sregs) @
93         (get_params … params))
94        start_lbl tmp_lbl def
95    in
96      add_graph … tmp_lbl last_stmt def
97  ] ?.
98[ cases start_lbl #x #H cases daemon (* @H *) (*CSC: XXXX, no Russell *)
99| cases (none_absrd) /2/ ]
100qed.
101
102definition save_return ≝
103  λglobals.
104  λret_regs.
105  λstart_lbl: label.
106  λdest_lbl: label.
107  λdef: ertl_internal_function globals.
108  let 〈def, tmpr〉 ≝ fresh_reg … def in
109  match reduce_strong ? ? RegisterSTS ret_regs with
110  [ dp crl crl_proof ⇒
111    let commonl ≝ \fst (\fst crl) in
112    let commonr ≝ \fst (\snd crl) in
113    let restl ≝ \snd (\fst crl) in
114    let restr ≝ \snd (\snd crl) in
115    let init_tmpr ≝ sequential ertl_params_ … (INT … tmpr (zero …)) in
116    let f_save ≝ λst. λr. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo r〉) in
117    let saves ≝ map2 … f_save commonl commonr crl_proof in
118    let f_default ≝ λst. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo tmpr〉) in
119    let defaults ≝ map … f_default restl in
120      adds_graph ertl_params1 ? (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
121  ].
122
123definition assign_result ≝
124  λglobals.λstart_lbl: label.
125  match reduce_strong ? ? RegisterRets RegisterSTS with
126  [ dp crl crl_proof ⇒
127    let commonl ≝ \fst (\fst crl) in
128    let commonr ≝ \fst (\snd crl) in
129    let f ≝ λret. λst. sequential ertl_params_ globals (MOVE … 〈hardware ret, hardware st〉) in
130    let insts ≝ map2 ? ? ? f commonl commonr crl_proof in
131      adds_graph ertl_params1 … insts start_lbl
132  ].
133
134definition add_epilogue ≝
135  λglobals.
136  λret_regs.
137  λsral.
138  λsrah.
139  λsregs.
140  λdef.
141  let start_lbl ≝ joint_if_exit … (ertl_params globals) def in
142  let 〈tmp_lbl, def〉 ≝ fresh_label … def in
143  match lookup … (joint_if_code … def) start_lbl
144    return λx. x ≠ None ? → ertl_internal_function globals with
145  [ None ⇒ λnone_absrd. ⊥
146  | Some last_stmt ⇒ λsome_prf.
147    let def ≝
148      add_translates ertl_params1 … (
149        [save_return globals ret_regs] @
150        restore_hdws … sregs @
151        [adds_graph ertl_params1 … [
152          sequential ertl_params_ … (PUSH … srah);
153          sequential ertl_params_ … (PUSH … sral)
154        ]] @
155        [adds_graph ertl_params1 … [
156          sequential ertl_params_ … (extension … ertl_st_ext_del_frame)
157        ]] @
158        [assign_result globals]
159      ) start_lbl tmp_lbl def
160    in
161    let def' ≝ add_graph … tmp_lbl last_stmt def in
162      set_joint_if_exit … tmp_lbl def' ?
163  ] ?.
164[ cases start_lbl #x #H cases daemon (* @H *) (* CSC: XXXX *)
165| cases (none_absrd) /2/
166| cases daemon (* CSC: XXXXX *)
167]
168qed.
169 
170
171definition allocate_regs ≝
172  λglobals.
173  λrs.
174  λsaved: rs_set rs.
175  λdef.
176   let allocate_regs_internal ≝
177    λr: Register.
178    λdef_sregs.
179    let 〈def, sregs〉 ≝ def_sregs in
180    let 〈def, r'〉 ≝ fresh_reg ertl_params0 globals def in
181      〈def, 〈r', r〉 :: sregs〉
182   in
183    rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉.
184   
185definition add_pro_and_epilogue ≝
186  λglobals.
187  λparams.
188  λret_regs.
189  λdef.
190  match fresh_regs_strong … globals def 2 with
191  [ dp def_sra def_sra_proof ⇒
192    let def ≝ \fst def_sra in
193    let sra ≝ \snd def_sra in
194    let sral ≝ nth_safe ? 0 sra ? in
195    let srah ≝ nth_safe ? 1 sra ? in
196    let 〈def, sregs〉 ≝ allocate_regs … register_list_set RegisterCalleeSaved def in
197    let def ≝ add_prologue … params sral srah sregs def in
198    let def ≝ add_epilogue … ret_regs sral srah sregs def in
199      def
200  ].
201>def_sra_proof //
202qed.
203
204definition set_params_hdw ≝
205  λglobals,params.
206  match params with
207  [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl]
208  | _ ⇒
209    let l ≝ zip_pottier ? ? params RegisterParams in
210      restore_hdws globals l
211  ].
212
213definition set_param_stack ≝
214  λglobals.
215  λoff.
216  λsrcr.
217  λstart_lbl: label.
218  λdest_lbl: label.
219  λdef: ertl_internal_function globals.
220  let 〈def, addr1〉 ≝ fresh_reg … def in
221  let 〈def, addr2〉 ≝ fresh_reg … def in
222  let 〈def, tmpr〉 ≝ fresh_reg … def in
223  let 〈ignore, int_off〉 ≝ half_add ? off int_size in
224    adds_graph ertl_params1 … [
225      sequential ertl_params_ … (INT … addr1 int_off);
226      sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉);
227      sequential ertl_params_ … (CLEAR_CARRY …);
228      sequential ertl_params_ … (OP2 … Sub addr1 tmpr addr1);
229      sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉);
230      sequential ertl_params_ … (INT … addr2 (zero ?));
231      sequential ertl_params_ … (OP2 … Sub addr2 tmpr addr2);
232      sequential ertl_params_ … (STORE … addr1 addr2 srcr)
233    ] start_lbl dest_lbl def.   
234
235definition set_params_stack ≝
236  λglobals,params.
237  match params with
238  [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [GOTO …] start_lbl]
239  | _ ⇒
240    let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in
241      mapi ? ? f params].
242
243definition set_params ≝
244  λglobals,params.
245  let n ≝ min (|params|) (|RegisterParams|) in
246  let hdw_stack_params ≝ split ? params n ? in
247  let hdw_params ≝ \fst hdw_stack_params in
248  let stack_params ≝ \snd hdw_stack_params in
249    set_params_hdw globals hdw_params @ set_params_stack globals stack_params.
250normalize nodelta /2/
251qed.
252
253definition fetch_result ≝
254  λglobals.
255  λret_regs.
256  λstart_lbl: label.
257  match reduce_strong ? ? RegisterSTS RegisterRets with
258  [ dp crl first_crl_proof ⇒
259    let commonl ≝ \fst (\fst crl) in
260    let commonr ≝ \fst (\snd crl) in
261    let f_save ≝ λst. λret. sequential ertl_params_ globals (MOVE … 〈hardware st, hardware ret〉) in
262    let saves ≝ map2 ? ? ? f_save commonl commonr ? in
263    match reduce_strong ? ? ret_regs RegisterSTS with
264    [ dp crl second_crl_proof ⇒
265      let commonl ≝ \fst (\fst crl) in
266      let commonr ≝ \fst (\snd crl) in
267      let f_restore ≝ λr. λst. sequential ertl_params_ … (MOVE … 〈pseudo r, hardware st〉) in
268      let restores ≝ map2 ? ? ? f_restore commonl commonr ? in
269        adds_graph ertl_params1 … (saves @ restores) start_lbl]].
270[@second_crl_proof | @first_crl_proof]
271qed.
272
273definition translate_call_id ≝
274  λglobals,f.
275  λargs.
276  λret_regs.
277  λstart_lbl.
278  λdest_lbl.
279  λdef.
280  let nb_args ≝ |args| in
281    add_translates ertl_params1 globals (
282      set_params … args @ [
283      adds_graph ertl_params1 … [ sequential ertl_params_ … (CALL_ID … f nb_args it) ];
284      fetch_result … ret_regs
285      ]
286    ) start_lbl dest_lbl def.
287
288definition translate_stmt :
289 ∀globals: list ident. label → rtlntc_statement globals → ertl_internal_function globals → ertl_internal_function globals
290 ≝
291  λglobals.
292  λlbl.
293  λstmt.
294  λdef.
295  match stmt with
296  [ GOTO lbl' ⇒ add_graph … lbl (GOTO … lbl') def
297  | RETURN ⇒ add_graph … lbl (RETURN …) def
298  | sequential seq lbl' ⇒
299     match seq with
300      [ PUSH _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
301      | POP _  ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
302      | CALL_ID f args ret_regs ⇒
303         translate_call_id … f args ret_regs lbl lbl' def
304      | MOVE rs ⇒
305         let 〈r1,r2〉 ≝ rs in
306         let rs ≝ 〈pseudo r1, pseudo r2〉 in
307          add_graph ertl_params1 ? lbl (sequential … (MOVE … rs) lbl') def
308      | extension ext ⇒
309         match ext with
310          [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *)
311          | rtlntc_st_ext_stack_address r1 r2 ⇒
312             adds_graph ertl_params1 … [
313              sequential ertl_params_ … (MOVE … 〈pseudo r1, hardware RegisterSPL〉);
314              sequential ertl_params_ … (MOVE … 〈pseudo r2, hardware RegisterSPH〉)
315             ] lbl lbl' def]
316      (*CSC: everything is just copied to re-type it from now on;
317        the problem is call_id that takes different parameters, but that is pattern-matched
318        above. It could be made nicer at the cost of making all the rest of the code uglier *)
319      | COST_LABEL cost_lbl ⇒ add_graph ertl_params1 … lbl (sequential … (COST_LABEL … cost_lbl) lbl') def
320      | ADDRESS x prf r1 r2 ⇒ add_graph ertl_params1 … lbl (sequential … (ADDRESS … x prf r1 r2) lbl') def
321      | INT r i ⇒  add_graph ertl_params1 … lbl (sequential … (INT … r i) lbl') def
322      | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
323          add_graph ertl_params1 … lbl (sequential … (OPACCS … op destr1 destr2 srcr1 srcr2) lbl') def
324      | OP1 op1 destr srcr ⇒
325        add_graph ertl_params1 … lbl (sequential … (OP1 … op1 destr srcr) lbl') def
326      | OP2 op2 destr srcr1 srcr2 ⇒
327        add_graph ertl_params1 … lbl (sequential … (OP2 … op2 destr srcr1 srcr2) lbl') def
328      | CLEAR_CARRY ⇒
329        add_graph ertl_params1 … lbl (sequential … (CLEAR_CARRY …) lbl') def
330      | SET_CARRY ⇒
331        add_graph ertl_params1 … lbl (sequential … (SET_CARRY …) lbl') def
332      | LOAD destr addr1 addr2 ⇒
333        add_graph ertl_params1 … lbl (sequential … (LOAD … destr addr1 addr2) lbl') def
334      | STORE addr1 addr2 srcr ⇒
335        add_graph ertl_params1 … lbl (sequential … (STORE … addr1 addr2 srcr) lbl') def
336      | COND srcr lbl_true ⇒
337        add_graph ertl_params1 … lbl (sequential … (COND … srcr lbl_true) lbl') def
338      | COMMENT msg ⇒
339        add_graph ertl_params1 … lbl (sequential … (COMMENT … msg) lbl') def
340      ]].
341  @not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *)
342qed.
343
344(* hack with empty graphs used here *)
345definition translate_funct_internal ≝
346  λglobals.λdef:rtlntc_internal_function globals.
347  let nb_params ≝ |joint_if_params ?? def| in
348  let added_stacksize ≝ max 0 (minus nb_params (|RegisterParams|)) in
349  let new_locals ≝ nub_by ? (eq_identifier ?) ((joint_if_locals … def) @ (joint_if_params … def)) in
350  let entry' ≝ joint_if_entry … def in
351  let exit' ≝ joint_if_exit … def in
352  let graph' ≝ add ? ? (empty_map ? ?) entry' (GOTO … entry') in
353  let graph' ≝ add ? ? graph' exit' (GOTO … exit') in
354  let def' ≝
355    mk_joint_internal_function globals (ertl_params globals)
356      (joint_if_luniverse … def) (joint_if_runiverse … def) (joint_if_result … def) (*CSC: different from OCaml code where joint_if_result is unit*)
357      nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
358      graph' ? ? in
359  let def' ≝ foldi ? ? ? (translate_stmt globals) (joint_if_code … def) def' in
360   add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
361whd in match ertl_params (* CSC: Matita's bug here; not enough/too much reduction
362                                 makes the next application fail. Why? *)   
363%
364 [ @entry' | @graph_add_lookup @graph_add
365 | @exit'  | @graph_add ]
366qed.
367
368definition generate ≝
369  λglobals.
370  λstmt.
371  λdef: joint_internal_function … (ertl_params globals).
372  let 〈entry, def〉 ≝ fresh_label … def in
373  let graph ≝ add … (joint_if_code … def) entry stmt in
374   set_joint_if_graph … (ertl_params globals) graph def ??.
375  [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *)
376  | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF
377    *) cases daemon (*CSC: XXX *)
378  ]
379qed.
380
381let rec find_and_remove_first_cost_label_internal (globals: list ident)
382  (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat)
383    on num_nodes ≝
384  match num_nodes with
385  [ O ⇒ 〈None ?, def〉
386  | S num_nodes' ⇒
387    match lookup … (joint_if_code … def) lbl with
388    [ None ⇒ 〈None ?, def〉
389    | Some stmt ⇒
390      match stmt with
391      [ sequential inst lbl ⇒
392         match inst with
393          [ COST_LABEL cost_lbl ⇒
394             〈Some … cost_lbl, add_graph ertl_params1 globals lbl (GOTO … lbl) def〉
395          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
396      | RETURN ⇒ 〈None …, def〉
397      | GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'
398      ]]].
399   
400definition find_and_remove_first_cost_label ≝
401  λglobals,def. 
402    find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)).
403
404definition move_first_cost_label_up_internal ≝
405  λglobals,def.
406  let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in
407  match cost_label with
408  [ None ⇒ def
409  | Some cost_label ⇒ generate … (sequential ertl_params_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
410  ].
411
412definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
413
414definition translate : rtl_program → ertl_program ≝
415 λp.
416  let p ≝ tailcall_simplify p in (* tailcall simplification here *)
417    transform_program ??? p (transf_fundef ?? (translate_funct …)).
Note: See TracBrowser for help on using the repository browser.