source: src/RTL/RTLtoERTL.ma @ 1075

Last change on this file since 1075 was 1075, checked in by mulligan, 9 years ago

nearly completed rtl -> ertl pass removing all option types with dep. types

File size: 28.8 KB
Line 
1include "RTL/RTL.ma".
2include "utilities/RegisterSet.ma".
3include "ERTL/ERTL.ma".
4
5definition change_exit_label ≝
6  λl: label.
7  λp: ertl_internal_function.
8  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
9  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
10  let ertl_if_params' ≝ ertl_if_params p in
11  let ertl_if_locals' ≝ ertl_if_locals p in
12  let ertl_if_stacksize' ≝ ertl_if_stacksize p in
13  let ertl_if_graph' ≝ ertl_if_graph p in
14  let ertl_if_entry' ≝ ertl_if_entry p in
15  let ertl_if_exit' ≝ l in
16    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
17                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
18                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
19
20definition change_entry_label ≝
21  λl: label.
22  λp: ertl_internal_function.
23  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
24  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
25  let ertl_if_params' ≝ ertl_if_params p in
26  let ertl_if_locals' ≝ ertl_if_locals p in
27  let ertl_if_stacksize' ≝ ertl_if_stacksize p in
28  let ertl_if_graph' ≝ ertl_if_graph p in
29  let ertl_if_entry' ≝ l in
30  let ertl_if_exit' ≝ ertl_if_exit p in
31    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
32                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
33                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
34                             
35definition add_graph ≝
36  λl: label.
37  λstmt.
38  λp.
39  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
40  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
41  let ertl_if_params' ≝ ertl_if_params p in
42  let ertl_if_locals' ≝ ertl_if_locals p in
43  let ertl_if_stacksize' ≝ ertl_if_stacksize p in
44  let ertl_if_graph' ≝ add ? ? (ertl_if_graph p) l stmt in
45  let ertl_if_entry' ≝ ertl_if_entry p in
46  let ertl_if_exit' ≝ ertl_if_exit p in
47    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
48                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
49                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
50                             
51definition fresh_label ≝
52  λdef.
53    fresh LabelTag (ertl_if_luniverse def).
54   
55definition change_label ≝
56  λl.
57  λe: ertl_statement.
58  match e with
59  [ ertl_st_skip _ ⇒ ertl_st_skip l
60  | ertl_st_comment s _ ⇒ ertl_st_comment s l
61  | ertl_st_cost c _ ⇒ ertl_st_cost c l
62  | ertl_st_get_hdw r1 r2 _ ⇒ ertl_st_get_hdw r1 r2 l
63  | ertl_st_set_hdw r1 r2 _ ⇒ ertl_st_set_hdw r1 r2 l
64  | ertl_st_hdw_to_hdw r1 r2 _ ⇒ ertl_st_hdw_to_hdw r1 r2 l
65  | ertl_st_new_frame _ ⇒ ertl_st_new_frame l
66  | ertl_st_del_frame _ ⇒ ertl_st_del_frame l
67  | ertl_st_frame_size r _ ⇒ ertl_st_frame_size r l
68  | ertl_st_pop r _ ⇒ ertl_st_pop r l
69  | ertl_st_push r _ ⇒ ertl_st_push r l
70  | ertl_st_addr_h r id _ ⇒ ertl_st_addr_h r id l
71  | ertl_st_addr_l r id _ ⇒ ertl_st_addr_l r id l
72  | ertl_st_int r i _ ⇒ ertl_st_int r i l
73  | ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l
74  | ertl_st_opaccs_a opaccs d s1 s2 _ ⇒ ertl_st_opaccs_a opaccs d s1 s2 l
75  | ertl_st_opaccs_b opaccs d s1 s2 _ ⇒ ertl_st_opaccs_b opaccs d s1 s2 l
76  | ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l
77  | ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l
78  | ertl_st_clear_carry _ ⇒ ertl_st_clear_carry l
79  | ertl_st_set_carry _ ⇒ ertl_st_set_carry l
80  | ertl_st_load d a1 a2 _ ⇒ ertl_st_load d a1 a2 l
81  | ertl_st_store a1 a2 s _ ⇒ ertl_st_store a1 a2 s l
82  | ertl_st_call_id f args _ ⇒ ertl_st_call_id f args l
83  | ertl_st_cond a i1 i2 ⇒ ertl_st_cond a i1 i2
84  | ertl_st_return ⇒ ertl_st_return
85  ].
86 
87let rec adds_graph
88  (stmt_list: list ertl_statement) (start_lbl: label)
89  (dest_lbl: label) (def: ertl_internal_function)
90    on stmt_list ≝
91  match stmt_list with
92  [ nil ⇒ add_graph start_lbl (ertl_st_skip dest_lbl) def
93  | cons stmt stmt_list ⇒
94    match stmt_list with
95    [ nil ⇒ add_graph start_lbl (change_label dest_lbl stmt) def
96    | _ ⇒
97      let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
98      let stmt ≝ change_label tmp_lbl stmt in
99      let def ≝ add_graph start_lbl stmt def in
100        adds_graph stmt_list tmp_lbl dest_lbl def
101    ]
102  ].
103
104let rec add_translates
105  (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
106  (def: ertl_internal_function)
107    on translate_list ≝
108  match translate_list with
109  [ nil ⇒ add_graph start_lbl (ertl_st_skip dest_lbl) def
110  | cons trans translate_list ⇒
111    match translate_list with
112    [ nil ⇒ trans start_lbl dest_lbl def
113    | _ ⇒
114      let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
115      let def ≝ trans start_lbl tmp_lbl def in
116        add_translates translate_list tmp_lbl dest_lbl def
117    ]
118  ].
119
120axiom register_fresh: universe RegisterTag → register.
121
122definition fresh_reg: ertl_internal_function → ertl_internal_function × register ≝
123  λdef.
124    let r ≝ register_fresh (ertl_if_runiverse def) in
125    let locals ≝ r :: ertl_if_locals def in
126    let ertl_if_luniverse' ≝ ertl_if_luniverse def in
127    let ertl_if_runiverse' ≝ ertl_if_runiverse def in
128    let ertl_if_params' ≝ ertl_if_params def in
129    let ertl_if_locals' ≝ locals in
130    let ertl_if_stacksize' ≝ ertl_if_stacksize def in
131    let ertl_if_graph' ≝ ertl_if_graph def in
132    let ertl_if_entry' ≝ ertl_if_entry def in
133    let ertl_if_exit' ≝ ertl_if_exit def in
134      〈mk_ertl_internal_function
135        ertl_if_luniverse' ertl_if_runiverse' ertl_if_params'
136        ertl_if_locals' ertl_if_stacksize' ertl_if_graph'
137        ertl_if_entry' ertl_if_exit', r〉.
138
139let rec fresh_regs
140  (def: ertl_internal_function) (n: nat)
141    on n ≝
142  match n with
143  [ O ⇒ 〈def, [ ]〉
144  | S n' ⇒
145    let 〈def', regs'〉 ≝ fresh_regs def n' in
146    let 〈def', reg〉 ≝ fresh_reg def' in
147      〈def', reg :: regs'〉
148  ].
149 
150axiom fresh_regs_length:
151  ∀def: ertl_internal_function.
152  ∀n: nat.
153    |(\snd (fresh_regs def n))| = n.
154
155definition fresh_regs_strong: ? → ∀n: nat. Σregs: ertl_internal_function × (list register). |\snd regs| = n ≝
156  λdef: ertl_internal_function.
157  λn: nat.
158    fresh_regs def n.
159  @fresh_regs_length
160qed.
161 
162definition save_hdws_internal ≝
163  λdestr_srcr: register × hardware_register.
164  λstart_lbl: label.
165    let 〈destr, srcr〉 ≝ destr_srcr in
166      adds_graph [ ertl_st_get_hdw destr srcr start_lbl ] start_lbl.
167 
168definition save_hdws ≝
169  λl.
170    map ? ? save_hdws_internal l.
171   
172definition restore_hdws_internal ≝
173  λdestr_srcr: hardware_register × register.
174  λstart_lbl: label.
175    let 〈destr, srcr〉 ≝ destr_srcr in
176    adds_graph [ ertl_st_set_hdw destr srcr start_lbl ] start_lbl.
177   
178definition swap_components ≝
179  λA, B: Type[0].
180  λp: A × B.
181  let 〈l, r〉 ≝ p in
182  〈r, l〉.
183   
184definition restore_hdws ≝
185  λl.
186    map ? ? restore_hdws_internal (map ? ? (swap_components ? ?) l).
187
188definition get_params_hdw_internal ≝
189  λstart_lbl: label.
190    adds_graph [ ertl_st_skip start_lbl ] start_lbl.
191
192definition get_params_hdw ≝
193  λparams: list register.
194  match params with
195  [ nil ⇒ [get_params_hdw_internal]
196  | _ ⇒
197    let l ≝ zip_pottier ? ? params parameters in
198      save_hdws l
199  ].
200
201definition get_param_stack ≝
202  λoff: nat.
203  λdestr.
204  λstart_lbl, dest_lbl: label.
205  λdef.
206  let 〈def, addr1〉 ≝ fresh_reg def in
207  let 〈def, addr2〉 ≝ fresh_reg def in
208  let 〈def, tmpr〉 ≝ fresh_reg def in
209  let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in
210  adds_graph [
211    ertl_st_frame_size addr1 start_lbl;
212    ertl_st_int tmpr int_offset start_lbl;
213    ertl_st_op2 Sub addr1 addr1 tmpr start_lbl;
214    ertl_st_get_hdw tmpr RegisterSPL start_lbl;
215    ertl_st_op2 Add addr1 addr1 tmpr start_lbl;
216    ertl_st_int addr2 (bitvector_of_nat 8 0) start_lbl;
217    ertl_st_get_hdw tmpr RegisterSPH start_lbl;
218    ertl_st_op2 Addc addr2 addr2 tmpr start_lbl;
219    ertl_st_load destr addr1 addr2 start_lbl
220  ] start_lbl dest_lbl def.
221 
222definition get_params_stack ≝
223  λparams.
224  match params with
225  [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl ]
226  | _ ⇒
227    let f ≝ λi. λr. get_param_stack i r in
228      mapi ? ? f params
229  ].
230
231definition get_params ≝
232  λparams.
233  let n ≝ min (length ? params) (length ? parameters) in
234  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
235  let hdw_params ≝ get_params_hdw hdw_params in
236    hdw_params @ (get_params_stack stack_params).
237 
238definition add_prologue ≝
239  λparams: list register.
240  λsral.
241  λsrah.
242  λsregs.
243  λdef.
244  let start_lbl ≝ ertl_if_entry def in
245  let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
246  match lookup ? ? (ertl_if_graph def) start_lbl
247    return λx. lookup ? ? (ertl_if_graph def) start_lbl ≠ None ? → ertl_internal_function with
248  [ None ⇒ λnone_absrd. ?
249  | Some last_stmt ⇒ λsome_prf.
250    let def ≝
251      add_translates
252         ((adds_graph [
253                     ertl_st_new_frame start_lbl
254                   ]) ::
255         (adds_graph [
256                      ertl_st_pop sral start_lbl;
257                      ertl_st_pop srah start_lbl
258                   ]) ::
259         (save_hdws sregs) @
260         (get_params params))
261        start_lbl tmp_lbl def
262    in
263      add_graph tmp_lbl last_stmt def
264  ] ?.
265  cases not_implemented (* dep. types here *)
266qed.
267
268definition save_return ≝
269  λret_regs.
270  λstart_lbl: label.
271  λdest_lbl: label.
272  λdef: ertl_internal_function.
273  let 〈def, tmpr〉 ≝ fresh_reg def in
274  match reduce_strong ? ? RegisterSTS ret_regs with
275  [ dp crl crl_proof ⇒
276    let commonl ≝ \fst (\fst crl) in
277    let commonr ≝ \fst (\snd crl) in
278    let restl ≝ \snd (\fst crl) in
279    let restr ≝ \snd (\snd crl) in
280    let init_tmpr ≝ ertl_st_int tmpr (zero ?) start_lbl in
281    let f_save ≝ λst. λr. ertl_st_set_hdw st r start_lbl in
282    let saves ≝ map2 ? ? ? f_save commonl commonr crl_proof in
283    let f_default ≝ λst. ertl_st_set_hdw st tmpr start_lbl in
284    let defaults ≝ map ? ? f_default restl in
285      adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
286  ].
287
288definition assign_result ≝
289  λstart_lbl: label.
290  match reduce_strong ? ? RegisterRets RegisterSTS with
291  [ dp crl crl_proof ⇒
292    let commonl ≝ \fst (\fst crl) in
293    let commonr ≝ \fst (\snd crl) in
294    let f ≝ λret. λst. ertl_st_hdw_to_hdw ret st start_lbl in
295    let insts ≝ map2 ? ? ? f commonl commonr crl_proof in
296      adds_graph insts start_lbl
297  ].
298
299definition add_epilogue ≝
300  λret_regs.
301  λsral.
302  λsrah.
303  λsregs.
304  λdef.
305  let start_lbl ≝ ertl_if_exit def in
306  let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
307  match lookup ? ? (ertl_if_graph def) start_lbl
308    return λx. lookup ? ? (ertl_if_graph def) start_lbl ≠ None ? → ? with
309  [ None ⇒ λnone_absd. ?
310  | Some last_stmt ⇒ λsome_prf.
311    let def ≝
312      add_translates (
313        [save_return ret_regs] @
314        restore_hdws sregs @
315        [adds_graph [
316          ertl_st_push srah start_lbl;
317          ertl_st_push sral start_lbl
318        ]] @
319        [adds_graph [
320          ertl_st_del_frame start_lbl
321        ]] @
322        [assign_result]
323      ) start_lbl tmp_lbl def
324    in
325    let def ≝ add_graph tmp_lbl last_stmt def in
326      change_exit_label tmp_lbl def
327  ] ?.
328  cases not_implemented (* dep types here *)
329qed.
330 
331definition allocate_regs_internal ≝
332  λr: Register.
333  λdef_sregs.
334  let 〈def, sregs〉 ≝ def_sregs in
335  let 〈def, r'〉 ≝ fresh_reg def in
336    〈def, 〈r', r〉 :: sregs〉.
337 
338definition allocate_regs ≝
339  λrs.
340  λsaved: rs_set rs.
341  λdef.
342    rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉.
343   
344definition add_pro_and_epilogue ≝
345  λparams.
346  λret_regs.
347  λdef.
348  match fresh_regs_strong def 2 with
349  [ dp def_sra def_sra_proof ⇒
350    let def ≝ \fst def_sra in
351    let sra ≝ \snd def_sra in
352    let sral ≝ nth_safe ? 0 sra ? in
353    let srah ≝ nth_safe ? 1 sra ? in
354    let 〈def, sregs〉 ≝ allocate_regs register_list_set RegisterCalleeSaved def in
355    let def ≝ add_prologue params sral srah sregs def in
356    let def ≝ add_epilogue ret_regs sral srah sregs def in
357      def
358  ].
359  [1: >def_sra_proof //
360  |2: >def_sra_proof //
361  ]
362qed.
363
364definition set_params_hdw ≝
365  λparams.
366  match params with
367  [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl]
368  | _ ⇒
369    let l ≝ zip_pottier ? ? params parameters in
370      restore_hdws l
371  ].
372
373definition set_param_stack ≝
374  λoff.
375  λsrcr.
376  λstart_lbl: label.
377  λdest_lbl: label.
378  λdef: ertl_internal_function.
379  let 〈def, addr1〉 ≝ fresh_reg def in
380  let 〈def, addr2〉 ≝ fresh_reg def in
381  let 〈def, tmpr〉 ≝ fresh_reg def in
382  let 〈ignore, int_off〉 ≝ half_add ? off int_size in
383    adds_graph [
384      ertl_st_int addr1 int_off start_lbl;
385      ertl_st_get_hdw tmpr RegisterSPL start_lbl;
386      ertl_st_clear_carry start_lbl;
387      ertl_st_op2 Sub addr1 tmpr addr1 start_lbl;
388      ertl_st_get_hdw tmpr RegisterSPH start_lbl;
389      ertl_st_int addr2 (zero ?) start_lbl;
390      ertl_st_op2 Sub addr2 tmpr addr2 start_lbl;
391      ertl_st_store addr1 addr2 srcr start_lbl
392    ] start_lbl dest_lbl def.   
393
394definition set_params_stack ≝
395  λparams.
396  match params with
397  [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl]
398  | _ ⇒
399    let f ≝ λi. λr. set_param_stack (bitvector_of_nat ? i) r in
400      mapi ? ? f params
401  ].
402
403axiom min_fst:
404  ∀m, n: nat.
405    min m n ≤ m.
406
407definition set_params ≝
408  λparams.
409  let n ≝ min (|params|) (|parameters|) in
410  let hdw_stack_params ≝ split ? params n ? in
411  let hdw_params ≝ \fst hdw_stack_params in
412  let stack_params ≝ \snd hdw_stack_params in
413    set_params_hdw hdw_params @ set_params_stack stack_params.
414  @min_fst
415qed.
416
417definition fetch_result ≝
418  λret_regs.
419  λstart_lbl: label.
420  match reduce_strong ? ? RegisterSTS RegisterRets with
421  [ dp crl first_crl_proof ⇒
422    let commonl ≝ \fst (\fst crl) in
423    let commonr ≝ \fst (\snd crl) in
424    let f_save ≝ λst. λret. ertl_st_hdw_to_hdw st ret start_lbl in
425    let saves ≝ map2 ? ? ? f_save commonl commonr ? in
426    match reduce_strong ? ? ret_regs RegisterSTS with
427    [ dp crl second_crl_proof ⇒
428      let commonl ≝ \fst (\fst crl) in
429      let commonr ≝ \fst (\snd crl) in
430      let f_restore ≝ λr. λst. ertl_st_get_hdw r st start_lbl in
431      let restores ≝ map2 ? ? ? f_restore commonl commonr ? in
432        adds_graph (saves @ restores) start_lbl
433    ]
434  ].
435  [ normalize nodelta; @second_crl_proof
436  | @first_crl_proof
437  ]
438qed.
439
440definition translate_call_id ≝
441  λf.
442  λargs.
443  λret_regs.
444  λstart_lbl.
445  λdest_lbl.
446  λdef.
447  let nb_args ≝ |args| in
448    add_translates (
449      set_params args @ [
450      adds_graph [ ertl_st_call_id f (bitvector_of_nat ? nb_args) start_lbl ];
451      fetch_result ret_regs
452      ]
453    ) start_lbl dest_lbl def.
454
455definition translate_stmt ≝
456  λlbl.
457  λstmt.
458  λdef.
459  match stmt with
460  [ rtl_st_skip lbl' ⇒ add_graph lbl (ertl_st_skip lbl') def
461  | rtl_st_cost cost_lbl lbl' ⇒ add_graph lbl (ertl_st_cost cost_lbl lbl') def
462  | rtl_st_addr r1 r2 x lbl' ⇒
463    adds_graph [
464      ertl_st_addr_l r1 x lbl;
465      ertl_st_addr_h r2 x lbl
466    ] lbl lbl' def
467  | rtl_st_stack_addr r1 r2 lbl' ⇒
468    adds_graph [
469      ertl_st_get_hdw r1 RegisterSPL lbl;
470      ertl_st_get_hdw r2 RegisterSPH lbl
471    ] lbl lbl' def
472  | rtl_st_int r i lbl' ⇒ add_graph lbl (ertl_st_int r i lbl') def
473  | rtl_st_move r1 r2 lbl' ⇒ add_graph lbl (ertl_st_move r1 r2 lbl') def
474  | rtl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl' ⇒
475    adds_graph [
476      ertl_st_opaccs_a op destr1 srcr1 srcr2 lbl;
477      ertl_st_opaccs_b op destr2 srcr1 srcr2 lbl
478      ] lbl lbl' def
479  | rtl_st_op1 op1 destr srcr lbl' ⇒
480    add_graph lbl (ertl_st_op1 op1 destr srcr lbl') def
481  | rtl_st_op2 op2 destr srcr1 srcr2 lbl' ⇒
482    add_graph lbl (ertl_st_op2 op2 destr srcr1 srcr2 lbl') def
483  | rtl_st_clear_carry lbl' ⇒
484    add_graph lbl (ertl_st_clear_carry lbl') def
485  | rtl_st_set_carry lbl' ⇒
486    add_graph lbl (ertl_st_set_carry lbl') def
487  | rtl_st_load destr addr1 addr2 lbl' ⇒
488    add_graph lbl (ertl_st_load destr addr1 addr2 lbl') def
489  | rtl_st_store addr1 addr2 srcr lbl' ⇒
490    add_graph lbl (ertl_st_store addr1 addr2 srcr lbl') def
491  | rtl_st_call_id f args ret_regs lbl' ⇒
492    translate_call_id f args ret_regs lbl lbl' def
493  | rtl_st_cond srcr lbl_true lbl_false ⇒
494    add_graph lbl (ertl_st_cond srcr lbl_true lbl_false) def
495  | rtl_st_return ⇒
496    add_graph lbl ertl_st_return def
497  | _ ⇒ ? (* assert false: not implemented or should not happen *)
498  ].
499  cases not_implemented
500qed.   
501
502   
503   
504definition save_return_internal ≝
505  λr.
506  λstart_lbl.
507  λdest_lbl.
508  λdef.
509  let 〈def, r_tmp〉 ≝ fresh_reg def in
510  adds_graph [
511    ertl_st_int r_tmp (bitvector_of_nat ? 0) start_lbl;
512    ertl_st_set_hdw RegisterST0 r start_lbl;
513    ertl_st_set_hdw RegisterST1 r_tmp start_lbl ] start_lbl dest_lbl def.
514   
515definition save_return_internal' ≝
516  λr1, r2.
517  λstart_lbl.
518  adds_graph [
519    ertl_st_set_hdw RegisterST0 r1 start_lbl;
520    ertl_st_set_hdw RegisterST1 r2 start_lbl
521  ] start_lbl.
522   
523definition save_return ≝
524  λret_regs.
525  match ret_regs with
526  [ nil ⇒ [ get_params_hdw_internal ]
527  | cons hd tl ⇒
528    match tl with
529    [ nil ⇒ [ save_return_internal hd ]
530    | cons hd' tl' ⇒ [ save_return_internal' hd hd' ]
531    ]
532  ].
533   
534definition add_epilogue ≝
535  λret_regs.
536  λsral.
537  λsrah.
538  λsregs.
539  λdef.
540  let start_lbl ≝ ertl_if_exit def in
541  let tmp_lbl ≝ fresh_label def in
542  match tmp_lbl with
543  [ None ⇒ None ?
544  | Some tmp_lbl ⇒
545    let last_stmt ≝ lookup ? ? (ertl_if_graph def) start_lbl in
546    match last_stmt with
547    [ None ⇒ None ?
548    | Some last_stmt ⇒
549      let def ≝
550        add_translates (
551          save_return ret_regs @
552          restore_hdws sregs @
553          [adds_graph [
554            ertl_st_push srah start_lbl;
555            ertl_st_push sral start_lbl
556          ]] @
557          [adds_graph [
558            ertl_st_del_frame start_lbl
559          ]] @
560          [adds_graph [
561            ertl_st_hdw_to_hdw RegisterDPL RegisterST0 start_lbl;
562            ertl_st_hdw_to_hdw RegisterDPH RegisterST1 start_lbl
563          ]]) start_lbl tmp_lbl def in
564      match def with
565      [ None ⇒ None ?
566      | Some def ⇒
567        let def ≝ add_graph tmp_lbl last_stmt def in
568          Some ? (change_exit_label tmp_lbl def)
569      ]
570    ]
571  ].
572 
573axiom add_pro_and_epilogue:
574  ∀rs: register_set.
575  ∀params: list register.
576  ∀ret_args: list register.
577  ∀def: ertl_internal_function.
578    option ertl_internal_function.
579   
580(*
581  dpm: address callee_saved problem   
582definition add_pro_and_epilogue ≝
583  λrs: register_set.
584  λparams.
585  λret_args.
586  λdef.
587  let 〈def, sra〉 ≝ fresh_regs def 2 in
588  let sral ≝ safe_nth ? 0 sra ? in
589  let srah ≝ safe_nth ? 1 sra ? in
590  let 〈def, sregs〉 ≝ allocate_regs callee_saved def in
591  let def ≝ add_prologue params sral srah sregs def in
592  let def ≝ add_epilogue ret_args sral srah sregs def in
593    def. 
594*)
595
596definition set_params_hdw ≝
597  λparams.
598  match length ? params with
599  [ O ⇒ Some ? [ get_params_hdw_internal ]
600  | _ ⇒
601    match zip ? ? params parameters with
602    [ None ⇒ None ?
603    | Some zipped_params ⇒ Some ? (restore_hdws zipped_params)
604    ]
605  ].
606 
607definition set_param_stack ≝
608  λoff: nat.
609  λsrcr.
610  λstart_lbl, dest_lbl: label.
611  λdef.
612  let 〈def, addr1〉 ≝ fresh_reg def in
613  let 〈def, addr2〉 ≝ fresh_reg def in
614  let 〈def, tmpr〉 ≝ fresh_reg def in
615  let 〈int_offset, ignore〉 ≝ add_8_with_carry (bitvector_of_nat ? off) int_size false in
616    adds_graph [
617      ertl_st_int addr2 int_offset start_lbl;
618      ertl_st_get_hdw tmpr RegisterSPL start_lbl;
619      ertl_st_clear_carry start_lbl;
620      ertl_st_op2 Sub addr1 tmpr addr1 start_lbl;
621      ertl_st_get_hdw tmpr RegisterSPH start_lbl;
622      ertl_st_int addr2 (bitvector_of_nat ? 0) start_lbl;
623      ertl_st_op2 Sub addr2 tmpr addr2 start_lbl;
624      ertl_st_store addr1 addr2 srcr start_lbl
625    ] start_lbl dest_lbl def.
626
627definition set_params_stack ≝
628  λparams.
629  match length ? params with
630  [ O ⇒ [ get_params_hdw_internal ]
631  | _ ⇒ mapi ? ? set_param_stack params
632 
633  ].
634 
635definition set_params ≝
636  λparams.
637  let n ≝ min (length ? params) (length ? parameters) in
638  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
639    match set_params_hdw hdw_params with
640    [ None ⇒ None ?
641    | Some hdw_params' ⇒ Some ? (hdw_params' @ (set_params_stack stack_params))
642    ].
643   
644definition fetch_result ≝
645  λret_regs.
646  λstart_lbl.
647  match ret_regs with
648  [ nil ⇒ adds_graph [ertl_st_skip start_lbl] start_lbl
649  | cons hd tl ⇒
650    match tl with
651    [ nil ⇒
652      adds_graph [
653        ertl_st_hdw_to_hdw RegisterST0 RegisterDPL start_lbl;
654        ertl_st_get_hdw hd RegisterST0 start_lbl
655      ] start_lbl
656    | cons hd' tl' ⇒
657      adds_graph [
658        ertl_st_hdw_to_hdw RegisterST0 RegisterDPL start_lbl;
659        ertl_st_hdw_to_hdw RegisterST1 RegisterDPH start_lbl;
660        ertl_st_get_hdw hd RegisterST0 start_lbl;
661        ertl_st_get_hdw hd' RegisterST1 start_lbl
662      ] start_lbl
663    ]
664  ].
665 
666definition translate_call_id ≝
667  λf.
668  λargs.
669  λret_regs.
670  λstart_lbl, dest_lbl: label.
671  λdef.
672  let nb_args ≝ bitvector_of_nat ? (length ? args) in
673  match set_params args with
674  [ None ⇒ None ?
675  | Some params_args ⇒
676    add_translates (
677      params_args @ [
678        adds_graph [ ertl_st_call_id f nb_args start_lbl ] ;
679        fetch_result ret_regs
680      ]) start_lbl dest_lbl def
681  ].
682 
683definition translate_stmt ≝
684  λlbl: label.
685  λstmt: rtl_statement.
686  λdef: ertl_internal_function.
687  match stmt with
688  [ rtl_st_skip lbl' ⇒
689    Some ? (add_graph lbl (ertl_st_skip lbl') def)
690  | rtl_st_cost cost_lbl lbl' ⇒
691    Some ? (add_graph lbl (ertl_st_cost cost_lbl lbl') def)
692  | rtl_st_addr r1 r2 x lbl' ⇒
693    adds_graph [
694      ertl_st_addr_l r1 x lbl;
695      ertl_st_addr_h r2 x lbl
696    ] lbl lbl' def
697  | rtl_st_stack_addr r1 r2 lbl' ⇒
698    adds_graph [
699      ertl_st_get_hdw r1 RegisterSPL lbl;
700      ertl_st_get_hdw r2 RegisterSPH lbl
701    ] lbl lbl' def
702  | rtl_st_int r i lbl' ⇒
703    Some ? (add_graph lbl (ertl_st_int r i lbl') def)
704  | rtl_st_move r1 r2 lbl' ⇒
705    Some ? (add_graph lbl (ertl_st_move r1 r2 lbl') def)
706  | rtl_st_opaccs opaccs d s1 s2 lbl' ⇒
707    Some ? (add_graph lbl (ertl_st_opaccs opaccs d s1 s2 lbl') def)
708  | rtl_st_op1 op1 d s lbl' ⇒
709    Some ? (add_graph lbl (ertl_st_op1 op1 d s lbl') def)
710  | rtl_st_op2 op2 d s1 s2 lbl' ⇒
711    Some ? (add_graph lbl (ertl_st_op2 op2 d s1 s2 lbl') def)
712  | rtl_st_clear_carry lbl' ⇒
713    Some ? (add_graph lbl (ertl_st_clear_carry lbl') def)
714  | rtl_st_load d a1 a2 lbl' ⇒
715    Some ? (add_graph lbl (ertl_st_load d a1 a2 lbl') def)
716  | rtl_st_store a1 a2 s lbl' ⇒
717    Some ? (add_graph lbl (ertl_st_store a1 a2 s lbl') def)
718  | rtl_st_call_id f args ret_regs lbl' ⇒
719    translate_call_id f args ret_regs lbl lbl' def
720  | rtl_st_call_ptr r1 r2 regs1 regs2 lbl ⇒ None ? (* dpm: todo *)
721  | rtl_st_cond_acc src lbl_true lbl_false ⇒
722    Some ? (add_graph lbl (ertl_st_cond_acc src lbl_true lbl_false) def)
723  | rtl_st_return ret_regs ⇒
724    Some ? (add_graph lbl (ertl_st_return ret_regs) def)
725  | rtl_st_tailcall_id ident regs ⇒ None ? (* dpm: impossible *)
726  | rtl_st_tailcall_ptr r1 r2 regs ⇒ None ? (* dpm: impossible *)
727  ].
728   
729definition translate_funct_internal ≝
730  λdef.
731  let nb_params ≝ length ? (rtl_if_params def) in
732  let added_stacksize ≝ max 0 (nb_params - (length ? parameters)) in
733  let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in
734  let def' ≝
735    mk_ertl_internal_function
736      (rtl_if_luniverse def) (rtl_if_runiverse def)
737      nb_params new_locals ((rtl_if_stacksize def) + added_stacksize)
738      (empty_map ? ?) (rtl_if_entry def) (rtl_if_exit def) in
739  let def' ≝ map_fold ? ? translate_stmt (rtl_if_graph def) def' in
740  let def' ≝ add_pro_and_epilogue register_list_set (rtl_if_params def) (rtl_if_result def) def' in
741    def'.
742   
743definition translate_funct ≝
744  λid_def: ident × ?.
745  let 〈id, def〉 ≝ id_def in
746  let def' ≝
747    match def with
748    [ rtl_f_internal def ⇒
749      match translate_funct_internal def with
750      [ None ⇒ None ?
751      | Some internal_def ⇒ Some ? (ertl_f_internal internal_def)
752      ]
753    | rtl_f_external def ⇒ Some ? (ertl_f_external def)
754    ] in
755  〈id, def'〉.
756
757definition generate ≝
758  λstmt.
759  λdef.
760  let entry ≝ fresh_label def in
761  match entry with
762  [ None ⇒ None ?
763  | Some entry ⇒
764    let def ≝ add_graph entry stmt def in
765      Some ? (change_entry_label entry def)
766  ].
767 
768let rec find_and_remove_first_cost_label_internal (def: ertl_internal_function)
769                                                  (lbl: label) (n: nat) on n ≝
770  match n with
771  [ O ⇒ None ?
772  | S n' ⇒
773    let statement_at_label ≝ lookup ? ? (ertl_if_graph def) lbl in
774    match statement_at_label with
775    [ None ⇒ None ?
776    | Some statement ⇒
777      match statement with
778      [ ertl_st_cost cost_lbl next_lbl ⇒
779        let def' ≝ add_graph lbl (ertl_st_skip next_lbl) def in
780          Some ? 〈Some ? cost_lbl, def'〉
781      | ertl_st_cond_acc _ _ _ ⇒ Some ? 〈None ?, def〉
782      | ertl_st_return _⇒ Some ? 〈None ?, def〉
783      | ertl_st_skip lbl' ⇒ find_and_remove_first_cost_label_internal def lbl' n'
784      | ertl_st_comment _ lbl' ⇒
785        find_and_remove_first_cost_label_internal def lbl' n'
786      | ertl_st_get_hdw _ _ lbl' ⇒
787        find_and_remove_first_cost_label_internal def lbl' n'
788      | ertl_st_set_hdw _ _ lbl' ⇒
789        find_and_remove_first_cost_label_internal def lbl' n'
790      | ertl_st_hdw_to_hdw _ _ lbl' ⇒
791        find_and_remove_first_cost_label_internal def lbl' n'
792      | ertl_st_pop _ lbl' ⇒
793        find_and_remove_first_cost_label_internal def lbl' n'
794      | ertl_st_push _ lbl' ⇒
795        find_and_remove_first_cost_label_internal def lbl' n'
796      | ertl_st_addr_h _ _ lbl' ⇒
797        find_and_remove_first_cost_label_internal def lbl' n'
798      | ertl_st_addr_l _ _ lbl' ⇒
799        find_and_remove_first_cost_label_internal def lbl' n'
800      | ertl_st_int _ _ lbl' ⇒
801        find_and_remove_first_cost_label_internal def lbl' n'
802      | ertl_st_move _ _ lbl' ⇒
803        find_and_remove_first_cost_label_internal def lbl' n'
804      | ertl_st_opaccs _ _ _ _ lbl' ⇒
805        find_and_remove_first_cost_label_internal def lbl' n'
806      | ertl_st_op2 _ _ _ _ lbl' ⇒
807        find_and_remove_first_cost_label_internal def lbl' n'
808      | ertl_st_op1 _ _ _ lbl' ⇒
809        find_and_remove_first_cost_label_internal def lbl' n'
810      | ertl_st_clear_carry lbl' ⇒
811        find_and_remove_first_cost_label_internal def lbl' n'
812      | ertl_st_load _ _ _ lbl' ⇒
813        find_and_remove_first_cost_label_internal def lbl' n'
814      | ertl_st_store _ _ _ lbl' ⇒
815        find_and_remove_first_cost_label_internal def lbl' n'
816      | ertl_st_call_id _ _ lbl' ⇒
817        find_and_remove_first_cost_label_internal def lbl' n'
818      | ertl_st_new_frame lbl' ⇒
819        find_and_remove_first_cost_label_internal def lbl' n'
820      | ertl_st_del_frame lbl' ⇒
821        find_and_remove_first_cost_label_internal def lbl' n'
822      | ertl_st_frame_size _ lbl' ⇒
823        find_and_remove_first_cost_label_internal def lbl' n'
824      ]
825    ]
826  ].
827 
828axiom num_entries:
829  ∀A: Type[0].
830  ∀g: graph A.
831    nat.
832 
833definition find_and_remove_first_cost_label ≝
834  λdef.
835    find_and_remove_first_cost_label_internal def (ertl_if_entry def) (num_entries ? (ertl_if_graph def)).
836
837definition move_first_cost_label_up_internal ≝
838  λdef.
839  let cost_label_def ≝ find_and_remove_first_cost_label def in
840  match cost_label_def with
841  [ None ⇒ None ?
842  | Some cost_label_def ⇒
843    let 〈cost_label, def〉 ≝ cost_label_def in
844    match cost_label with
845    [ None ⇒ Some ? def
846    | Some cost_label ⇒ generate (ertl_st_cost cost_label (ertl_if_entry def)) def
847    ]
848  ].
849 
850definition move_first_cost_label_up ≝
851  λid_def: ident × ?.
852  let 〈id, def〉 ≝ id_def in
853  let def' ≝
854    match def with 
855    [ ertl_f_internal int_fun ⇒
856      let cost_label_def ≝ move_first_cost_label_up_internal int_fun in
857      match cost_label_def with
858      [ None ⇒ None ?
859      | Some cost_label_def ⇒
860          Some ? (ertl_f_internal cost_label_def)
861      ]
862    | ertl_f_external _ ⇒ Some ? def
863    ] in
864  match def' with
865  [ None ⇒ None ?
866  | Some def' ⇒ Some ? 〈id, def'〉
867  ].
868 
869definition translate_internal ≝
870  λfunct.
871    let 〈id, funct〉 ≝ translate_funct funct in
872    match funct with
873    [ None ⇒ None ?
874    | Some funct ⇒ move_first_cost_label_up 〈id, funct〉
875    ].
876
877let rec strip_none (A: Type[0]) (l: list (option A)) on l: list A ≝
878  match l with
879  [ nil ⇒ nil ?
880  | cons hd tl ⇒
881    match hd with
882    [ None ⇒ strip_none A tl
883    | Some hd ⇒ hd :: strip_none A tl
884    ]
885  ].
886 
887definition translate: rtl_program → ertl_program ≝
888  λp.
889  let p ≝ tailcall_simplify p in
890  let rtl_pr_vars' ≝ rtl_pr_vars p in
891  let rtl_pr_functs' ≝ map … translate_internal (rtl_pr_functs p) in
892  let rtl_pr_functs_filtered ≝ strip_none ? rtl_pr_functs' in
893  let rtl_pr_main' ≝ rtl_pr_main p in
894    mk_ertl_program rtl_pr_vars' rtl_pr_functs_filtered rtl_pr_main'.
Note: See TracBrowser for help on using the repository browser.