source: src/RTL/RTLtoERTL.ma @ 1077

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

ack, dependent types are scary

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