source: src/RTL/RTLToERTL.ma @ 2032

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

!! BEWARE: major commit !!

1) [affects everybody]

split for vectors renamed to vsplit to reduce ambiguity since split is
now also a function in the standard library.
Note: I have not been able to propagate the changes everywhere in
the front-end/back-end because some files do not compile

2) [affects everybody]

functions on Vectors copied both in the front and back-ends moved to
Vectors.ma

3) [affects only the back-end]

subaddressing_mode_elim redesigned from scratch and now also applied to
Policy.ma. Moreover, all daemons about that have been closed.
The new one is much simpler to apply since it behaves like a standard
elimination principle: @(subaddressing_mode_elim \ldots x) where x is
the thing to eliminate.

File size: 16.2 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 ≝ vsplit ? 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.
252normalize nodelta /2/
253qed.
254
255definition fetch_result ≝
256  λglobals.
257  λret_regs.
258  λstart_lbl: label.
259  match reduce_strong ? ? RegisterSTS RegisterRets with
260  [ mk_Sig crl first_crl_proof ⇒
261    let commonl ≝ \fst (\fst crl) in
262    let commonr ≝ \fst (\snd crl) in
263    let f_save ≝ λst. λret. sequential ertl_params_ globals (MOVE … 〈hardware st, hardware ret〉) in
264    let saves ≝ map2 ? ? ? f_save commonl commonr ? in
265    match reduce_strong ? ? ret_regs RegisterSTS with
266    [ mk_Sig crl second_crl_proof ⇒
267      let commonl ≝ \fst (\fst crl) in
268      let commonr ≝ \fst (\snd crl) in
269      let f_restore ≝ λr. λst. sequential ertl_params_ … (MOVE … 〈pseudo r, hardware st〉) in
270      let restores ≝ map2 ? ? ? f_restore commonl commonr ? in
271        adds_graph ertl_params1 … (saves @ restores) start_lbl]].
272[@second_crl_proof | @first_crl_proof]
273qed.
274
275definition translate_call_id ≝
276  λglobals,f.
277  λargs.
278  λret_regs.
279  λstart_lbl.
280  λdest_lbl.
281  λdef.
282  let nb_args ≝ |args| in
283    add_translates ertl_params1 globals (
284      set_params … args @ [
285      adds_graph ertl_params1 … [ sequential ertl_params_ … (CALL_ID … f nb_args it) ];
286      fetch_result … ret_regs
287      ]
288    ) start_lbl dest_lbl def.
289
290definition translate_stmt :
291 ∀globals: list ident. label → rtlntc_statement globals → ertl_internal_function globals → ertl_internal_function globals
292 ≝
293  λglobals.
294  λlbl.
295  λstmt.
296  λdef.
297  match stmt with
298  [ GOTO lbl' ⇒ add_graph … lbl (GOTO … lbl') def
299  | RETURN ⇒ add_graph … lbl (RETURN …) def
300  | sequential seq lbl' ⇒
301     match seq with
302      [ PUSH _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
303      | POP _  ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
304      | CALL_ID f args ret_regs ⇒
305         translate_call_id … f args ret_regs lbl lbl' def
306      | MOVE rs ⇒
307         let 〈r1,r2〉 ≝ rs in
308         let rs ≝ 〈pseudo r1, pseudo r2〉 in
309          add_graph ertl_params1 ? lbl (sequential … (MOVE … rs) lbl') def
310      | extension ext ⇒
311         match ext with
312          [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *)
313          | rtlntc_st_ext_stack_address r1 r2 ⇒
314             adds_graph ertl_params1 … [
315              sequential ertl_params_ … (MOVE … 〈pseudo r1, hardware RegisterSPL〉);
316              sequential ertl_params_ … (MOVE … 〈pseudo r2, hardware RegisterSPH〉)
317             ] lbl lbl' def]
318      (*CSC: everything is just copied to re-type it from now on;
319        the problem is call_id that takes different parameters, but that is pattern-matched
320        above. It could be made nicer at the cost of making all the rest of the code uglier *)
321      | COST_LABEL cost_lbl ⇒ add_graph ertl_params1 … lbl (sequential … (COST_LABEL … cost_lbl) lbl') def
322      | ADDRESS x prf r1 r2 ⇒ add_graph ertl_params1 … lbl (sequential … (ADDRESS … x prf r1 r2) lbl') def
323      | INT r i ⇒  add_graph ertl_params1 … lbl (sequential … (INT … r i) lbl') def
324      | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
325          add_graph ertl_params1 … lbl (sequential … (OPACCS … op destr1 destr2 srcr1 srcr2) lbl') def
326      | OP1 op1 destr srcr ⇒
327        add_graph ertl_params1 … lbl (sequential … (OP1 … op1 destr srcr) lbl') def
328      | OP2 op2 destr srcr1 srcr2 ⇒
329        add_graph ertl_params1 … lbl (sequential … (OP2 … op2 destr srcr1 srcr2) lbl') def
330      | CLEAR_CARRY ⇒
331        add_graph ertl_params1 … lbl (sequential … (CLEAR_CARRY …) lbl') def
332      | SET_CARRY ⇒
333        add_graph ertl_params1 … lbl (sequential … (SET_CARRY …) lbl') def
334      | LOAD destr addr1 addr2 ⇒
335        add_graph ertl_params1 … lbl (sequential … (LOAD … destr addr1 addr2) lbl') def
336      | STORE addr1 addr2 srcr ⇒
337        add_graph ertl_params1 … lbl (sequential … (STORE … addr1 addr2 srcr) lbl') def
338      | COND srcr lbl_true ⇒
339        add_graph ertl_params1 … lbl (sequential … (COND … srcr lbl_true) lbl') def
340      | COMMENT msg ⇒
341        add_graph ertl_params1 … lbl (sequential … (COMMENT … msg) lbl') def
342      ]].
343  @not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *)
344qed.
345
346(* hack with empty graphs used here *)
347definition translate_funct_internal ≝
348  λglobals.λdef:rtlntc_internal_function globals.
349  let nb_params ≝ |joint_if_params ?? def| in
350  let added_stacksize ≝ max 0 (minus nb_params (|RegisterParams|)) in
351  let new_locals ≝ nub_by ? (eq_identifier ?) ((joint_if_locals … def) @ (joint_if_params … def)) in
352  let entry' ≝ joint_if_entry … def in
353  let exit' ≝ joint_if_exit … def in
354  let graph' ≝ add ? ? (empty_map ? ?) entry' (GOTO … entry') in
355  let graph' ≝ add ? ? graph' exit' (GOTO … exit') in
356  let def' ≝
357    mk_joint_internal_function globals (ertl_params globals)
358      (joint_if_luniverse … def) (joint_if_runiverse … def) (joint_if_result … def) (*CSC: different from OCaml code where joint_if_result is unit*)
359      nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
360      graph' ? ? in
361  let def' ≝ foldi ? ? ? (translate_stmt globals) (joint_if_code … def) def' in
362   add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
363whd in match ertl_params; (* CSC: Matita's bug here; not enough/too much reduction
364                                 makes the next application fail. Why? *)   
365%
366 [ @entry' | @graph_add_lookup @graph_add
367 | @exit'  | @graph_add ]
368qed.
369
370definition generate ≝
371  λglobals.
372  λstmt.
373  λdef: joint_internal_function … (ertl_params globals).
374  let 〈entry, def〉 ≝ fresh_label … def in
375  let graph ≝ add … (joint_if_code … def) entry stmt in
376   set_joint_if_graph … (ertl_params globals) graph def ??.
377  [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *)
378  | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF
379    *) cases daemon (*CSC: XXX *)
380  ]
381qed.
382
383let rec find_and_remove_first_cost_label_internal (globals: list ident)
384  (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat)
385    on num_nodes ≝
386  match num_nodes with
387  [ O ⇒ 〈None ?, def〉
388  | S num_nodes' ⇒
389    match lookup … (joint_if_code … def) lbl with
390    [ None ⇒ 〈None ?, def〉
391    | Some stmt ⇒
392      match stmt with
393      [ sequential inst lbl ⇒
394         match inst with
395          [ COST_LABEL cost_lbl ⇒
396             〈Some … cost_lbl, add_graph ertl_params1 globals lbl (GOTO … lbl) def〉
397          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
398      | RETURN ⇒ 〈None …, def〉
399      | GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'
400      ]]].
401   
402definition find_and_remove_first_cost_label ≝
403  λglobals,def. 
404    find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)).
405
406definition move_first_cost_label_up_internal ≝
407  λglobals,def.
408  let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in
409  match cost_label with
410  [ None ⇒ def
411  | Some cost_label ⇒ generate … (sequential ertl_params_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
412  ].
413
414definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
415
416definition rtl_to_ertl : rtl_program → ertl_program ≝
417 λp.
418  let p ≝ tailcall_simplify p in (* tailcall simplification here *)
419    transform_program ??? p (transf_fundef ?? (translate_funct …)).
Note: See TracBrowser for help on using the repository browser.