source: src/RTL/RTLToERTL.ma @ 1516

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

Ported to syntax of Matita 0.99.1.

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.