source: src/RTL/RTLtoERTL.ma @ 1076

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

small changes

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