source: src/RTL/RTLToERTL.ma @ 2160

Last change on this file since 2160 was 2103, checked in by campbell, 9 years ago

Make transform_*program take a more general transformation to make
properties easier to state.
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
7include alias "basics/lists/list.ma".
8
9definition save_hdws ≝
10 λglobals,l.
11  let save_hdws_internal ≝
12   λdestr_srcr.λstart_lbl.
13    let 〈destr, srcr〉 ≝ destr_srcr in
14     adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈pseudo destr,hardware srcr〉) ] start_lbl
15  in
16   map ? ? save_hdws_internal l.
17
18definition restore_hdws ≝
19  λglobals,l.
20   let restore_hdws_internal ≝
21    λsrcr_destr: register × Register.
22    λstart_lbl: label.
23     let 〈srcr, destr〉 ≝ srcr_destr in
24     adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈hardware destr, pseudo srcr〉) ] start_lbl
25   in
26    map ? ? restore_hdws_internal l.
27
28definition get_params_hdw ≝
29  λglobals.
30  λparams: list register.
31  match params with
32  [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ GOTO … ] start_lbl]
33  | _ ⇒
34    let l ≝ zip_pottier ? ? params RegisterParams in
35      save_hdws globals l ].
36
37definition get_param_stack ≝
38  λglobals.
39  λoff: nat.
40  λdestr.
41  λstart_lbl, dest_lbl: label.
42  λdef.
43  let 〈def, addr1〉 ≝ fresh_reg … def in
44  let 〈def, addr2〉 ≝ fresh_reg … def in
45  let 〈def, tmpr〉 ≝ fresh_reg … def in
46  let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in
47  adds_graph ertl_params1 globals [
48    sequential ertl_params_ … (extension … (ertl_st_ext_frame_size addr1));
49    sequential ertl_params_ … (INT … tmpr int_offset);
50    sequential ertl_params_ … (OP2 … Sub addr1 addr1 tmpr);
51    sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉);
52    sequential ertl_params_ … (OP2 … Add addr1 addr1 tmpr);
53    sequential ertl_params_ … (INT … addr2 (bitvector_of_nat 8 0));
54    sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉);
55    sequential ertl_params_ … (OP2 … Addc addr2 addr2 tmpr);
56    sequential ertl_params_ … (LOAD … destr addr1 addr2)
57  ] start_lbl dest_lbl def.
58 
59definition get_params_stack ≝
60  λglobals,params.
61  match params with
62  [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl ]
63  | _ ⇒ mapi ? ? (get_param_stack globals) params ].
64
65definition get_params ≝
66  λglobals,params.
67  let n ≝ min (length … params) (length … RegisterParams) in
68  let 〈hdw_params, stack_params〉 ≝ list_split … n params in
69  let hdw_params ≝ get_params_hdw globals hdw_params in
70    hdw_params @ (get_params_stack … stack_params).
71
72definition add_prologue ≝
73  λglobals.
74  λparams: list register.
75  λsral.
76  λsrah.
77  λsregs.
78  λdef.
79  let start_lbl ≝ joint_if_entry … (ertl_params globals) def in
80  let 〈tmp_lbl, def〉 ≝ fresh_label … def in
81  match lookup … (joint_if_code … def) start_lbl
82    return λx. x ≠ None ? → ertl_internal_function globals with
83  [ None ⇒ λnone_absrd. ⊥
84  | Some last_stmt ⇒ λsome_prf.
85    let def ≝
86      add_translates …
87         ((adds_graph ertl_params1 … [
88                     sequential ertl_params_ … (extension ertl_params__ globals ertl_st_ext_new_frame)
89                   ]) ::
90         (adds_graph ertl_params1 … [
91                      sequential ertl_params_ … (POP … sral);
92                      sequential ertl_params_ … (POP … srah)
93                   ]) ::
94         (save_hdws … sregs) @
95         (get_params … params))
96        start_lbl tmp_lbl def
97    in
98      add_graph … tmp_lbl last_stmt def
99  ] ?.
100[ cases start_lbl #x #H cases daemon (* @H *) (*CSC: XXXX, no Russell *)
101| cases (none_absrd) /2/ ]
102qed.
103
104definition save_return ≝
105  λglobals.
106  λret_regs.
107  λstart_lbl: label.
108  λdest_lbl: label.
109  λdef: ertl_internal_function globals.
110  let 〈def, tmpr〉 ≝ fresh_reg … def in
111  match reduce_strong ? ? RegisterSTS ret_regs with
112  [ mk_Sig crl crl_proof ⇒
113    let commonl ≝ \fst (\fst crl) in
114    let commonr ≝ \fst (\snd crl) in
115    let restl ≝ \snd (\fst crl) in
116    let restr ≝ \snd (\snd crl) in
117    let init_tmpr ≝ sequential ertl_params_ … (INT … tmpr (zero …)) in
118    let f_save ≝ λst. λr. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo r〉) in
119    let saves ≝ map2 … f_save commonl commonr crl_proof in
120    let f_default ≝ λst. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo tmpr〉) in
121    let defaults ≝ map … f_default restl in
122      adds_graph ertl_params1 ? (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
123  ].
124
125definition assign_result ≝
126  λglobals.λstart_lbl: label.
127  match reduce_strong ? ? RegisterRets RegisterSTS with
128  [ mk_Sig crl crl_proof ⇒
129    let commonl ≝ \fst (\fst crl) in
130    let commonr ≝ \fst (\snd crl) in
131    let f ≝ λret. λst. sequential ertl_params_ globals (MOVE … 〈hardware ret, hardware st〉) in
132    let insts ≝ map2 ? ? ? f commonl commonr crl_proof in
133      adds_graph ertl_params1 … insts start_lbl
134  ].
135
136definition add_epilogue ≝
137  λglobals.
138  λret_regs.
139  λsral.
140  λsrah.
141  λsregs.
142  λdef.
143  let start_lbl ≝ joint_if_exit … (ertl_params globals) def in
144  let 〈tmp_lbl, def〉 ≝ fresh_label … def in
145  match lookup … (joint_if_code … def) start_lbl
146    return λx. x ≠ None ? → ertl_internal_function globals with
147  [ None ⇒ λnone_absrd. ⊥
148  | Some last_stmt ⇒ λsome_prf.
149    let def ≝
150      add_translates ertl_params1 … (
151        [save_return globals ret_regs] @
152        restore_hdws … sregs @
153        [adds_graph ertl_params1 … [
154          sequential ertl_params_ … (PUSH … srah);
155          sequential ertl_params_ … (PUSH … sral)
156        ]] @
157        [adds_graph ertl_params1 … [
158          sequential ertl_params_ … (extension … ertl_st_ext_del_frame)
159        ]] @
160        [assign_result globals]
161      ) start_lbl tmp_lbl def
162    in
163    let def' ≝ add_graph … tmp_lbl last_stmt def in
164      set_joint_if_exit … tmp_lbl def' ?
165  ] ?.
166[ cases start_lbl #x #H cases daemon (* @H *) (* CSC: XXXX *)
167| cases (none_absrd) /2/
168| cases daemon (* CSC: XXXXX *)
169]
170qed.
171 
172
173definition allocate_regs ≝
174  λglobals.
175  λrs.
176  λsaved: rs_set rs.
177  λdef.
178   let allocate_regs_internal ≝
179    λr: Register.
180    λdef_sregs.
181    let 〈def, sregs〉 ≝ def_sregs in
182    let 〈def, r'〉 ≝ fresh_reg ertl_params0 globals def in
183      〈def, 〈r', r〉 :: sregs〉
184   in
185    rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉.
186   
187definition add_pro_and_epilogue ≝
188  λglobals.
189  λparams.
190  λret_regs.
191  λdef.
192  match fresh_regs_strong … globals def 2 with
193  [ mk_Sig def_sra def_sra_proof ⇒
194    let def ≝ \fst def_sra in
195    let sra ≝ \snd def_sra in
196    let sral ≝ nth_safe ? 0 sra ? in
197    let srah ≝ nth_safe ? 1 sra ? in
198    let 〈def, sregs〉 ≝ allocate_regs … register_list_set RegisterCalleeSaved def in
199    let def ≝ add_prologue … params sral srah sregs def in
200    let def ≝ add_epilogue … ret_regs sral srah sregs def in
201      def
202  ].
203>def_sra_proof //
204qed.
205
206definition set_params_hdw ≝
207  λglobals,params.
208  match params with
209  [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl]
210  | _ ⇒
211    let l ≝ zip_pottier ? ? params RegisterParams in
212      restore_hdws globals l
213  ].
214
215definition set_param_stack ≝
216  λglobals.
217  λoff.
218  λsrcr.
219  λstart_lbl: label.
220  λdest_lbl: label.
221  λdef: ertl_internal_function globals.
222  let 〈def, addr1〉 ≝ fresh_reg … def in
223  let 〈def, addr2〉 ≝ fresh_reg … def in
224  let 〈def, tmpr〉 ≝ fresh_reg … def in
225  let 〈ignore, int_off〉 ≝ half_add ? off int_size in
226    adds_graph ertl_params1 … [
227      sequential ertl_params_ … (INT … addr1 int_off);
228      sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉);
229      sequential ertl_params_ … (CLEAR_CARRY …);
230      sequential ertl_params_ … (OP2 … Sub addr1 tmpr addr1);
231      sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉);
232      sequential ertl_params_ … (INT … addr2 (zero ?));
233      sequential ertl_params_ … (OP2 … Sub addr2 tmpr addr2);
234      sequential ertl_params_ … (STORE … addr1 addr2 srcr)
235    ] start_lbl dest_lbl def.   
236
237definition set_params_stack ≝
238  λglobals,params.
239  match params with
240  [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [GOTO …] start_lbl]
241  | _ ⇒
242    let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in
243      mapi ? ? f params].
244
245definition set_params ≝
246  λglobals,params.
247  let n ≝ min (|params|) (|RegisterParams|) in
248  let hdw_stack_params ≝ split ? params n in
249  let hdw_params ≝ \fst hdw_stack_params in
250  let stack_params ≝ \snd hdw_stack_params in
251    set_params_hdw globals hdw_params @ set_params_stack globals stack_params.
252
253definition fetch_result ≝
254  λglobals.
255  λret_regs.
256  λstart_lbl: label.
257  match reduce_strong ? ? RegisterSTS RegisterRets with
258  [ mk_Sig 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    [ mk_Sig 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 rtl_to_ertl : rtl_program → ertl_program ≝
415 λp.
416  let p ≝ tailcall_simplify p in (* tailcall simplification here *)
417    transform_program ??? p (λvarnames. transf_fundef ?? (translate_funct varnames)).
Note: See TracBrowser for help on using the repository browser.