source: src/RTL/RTLtoERTL.ma @ 782

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

More work on rtl-ertl pass from today, plus resolved conflict.

File size: 16.8 KB
Line 
1include "RTL/RTL.ma".
2include "ERTL/ERTL.ma".
3include "utilities/RegisterSet.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    match fresh LabelTag (ertl_if_luniverse def) with
54    [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ)
55    | Error ⇒ None ?
56    ].
57   
58definition change_label ≝
59  λl.
60  λe: ertl_statement.
61  match e with
62  [ ertl_st_skip _ ⇒ ertl_st_skip l
63  | ertl_st_comment s _ ⇒ ertl_st_comment s l
64  | ertl_st_cost c _ ⇒ ertl_st_cost c l
65  | ertl_st_get_hdw r1 r2 _ ⇒ ertl_st_get_hdw r1 r2 l
66  | ertl_st_set_hdw r1 r2 _ ⇒ ertl_st_set_hdw r1 r2 l
67  | ertl_st_hdw_to_hdw r1 r2 _ ⇒ ertl_st_hdw_to_hdw r1 r2 l
68  | ertl_st_new_frame _ ⇒ ertl_st_new_frame l
69  | ertl_st_del_frame _ ⇒ ertl_st_del_frame l
70  | ertl_st_frame_size r _ ⇒ ertl_st_frame_size r l
71  | ertl_st_pop r _ ⇒ ertl_st_pop r l
72  | ertl_st_push r _ ⇒ ertl_st_push r l
73  | ertl_st_addr_h r id _ ⇒ ertl_st_addr_h r id l
74  | ertl_st_addr_l r id _ ⇒ ertl_st_addr_l r id l
75  | ertl_st_int r i _ ⇒ ertl_st_int r i l
76  | ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l
77  | ertl_st_opaccs opaccs d s1 s2 _ ⇒ ertl_st_opaccs opaccs d s1 s2 l
78  | ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l
79  | ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l
80  | ertl_st_clear_carry _ ⇒ ertl_st_clear_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_acc a i1 i2 ⇒ ertl_st_cond_acc a i1 i2
85  | ertl_st_return a ⇒ ertl_st_return a
86  ].
87 
88let rec adds_graph (stmt_list: list ertl_statement) (start_lbl: label) (dest_lbl: label) (def: ertl_internal_function): option ertl_internal_function ≝
89  match stmt_list with
90  [ nil ⇒ Some ? def
91  | cons hd tl ⇒
92    match tl with
93    [ nil ⇒ Some ? (add_graph start_lbl (change_label dest_lbl hd) def)
94    | _ ⇒
95      let tmp_lbl ≝ fresh_label def in
96      match tmp_lbl with
97      [ Some tmp_lbl ⇒
98        let stmt ≝ change_label tmp_lbl hd in
99        let def ≝ add_graph start_lbl hd def in
100          adds_graph tl tmp_lbl dest_lbl def
101      | None ⇒ None ?
102      ]
103    ]
104  ].
105
106let rec add_translates (translate_list: list (label → label → ertl_internal_function → option ertl_internal_function))
107                       (start_lbl: label) (dest_lbl: label)
108                       (def: ertl_internal_function): option ertl_internal_function ≝
109  match translate_list with
110  [ nil ⇒ Some ? def
111  | cons hd tl ⇒
112    match tl with
113    [ nil ⇒ hd start_lbl dest_lbl def
114    | _ ⇒
115      let tmp_lbl ≝ fresh_label def in
116      match tmp_lbl with
117      [ Some tmp_lbl ⇒
118        match hd start_lbl tmp_lbl def with
119        [ Some def ⇒ add_translates tl tmp_lbl dest_lbl def
120        | None ⇒ None ?
121        ]
122      | None ⇒ None ?
123      ]
124    ]
125  ].
126 
127axiom fresh_reg: ertl_internal_function → ertl_internal_function × register.
128
129let rec fresh_regs (def: ertl_internal_function) (n: nat) on n ≝
130  match n with
131  [ O ⇒ 〈def, [ ]〉
132  | S n' ⇒
133    let 〈def', regs'〉 ≝ fresh_regs def n' in
134    let 〈def', reg〉 ≝ fresh_reg def' in
135      〈def', reg :: regs'〉
136  ].
137 
138definition save_hdws_internal ≝
139  λdestr_srcr: register × hardware_register.
140  λstart_lbl: label.
141    let 〈destr, srcr〉 ≝ destr_srcr in
142      adds_graph [ ertl_st_get_hdw destr srcr start_lbl ] start_lbl.
143 
144definition save_hdws ≝
145  λl.
146    map ? ? save_hdws_internal l.
147   
148definition restore_hdws_internal ≝
149  λdestr_srcr: hardware_register × register.
150  λstart_lbl: label.
151    let 〈destr, srcr〉 ≝ destr_srcr in
152    adds_graph [ ertl_st_set_hdw destr srcr start_lbl ] start_lbl.
153   
154definition swap_components ≝
155  λA, B: Type[0].
156  λp: A × B.
157  let 〈l, r〉 ≝ p in
158  〈r, l〉.
159   
160definition restore_hdws ≝
161  λl.
162    map ? ? restore_hdws_internal (map ? ? (swap_components ? ?) l).
163
164definition get_params_hdw_internal ≝
165  λstart_lbl: label.
166    adds_graph [ ertl_st_skip start_lbl ] start_lbl.
167
168definition get_params_hdw ≝
169  λparams: list register.
170  match length ? params with
171  [ O ⇒ Some ? [ get_params_hdw_internal ]
172  | _ ⇒
173    match zip ? ? params parameters with
174    [ None ⇒ None ?
175    | Some l ⇒ Some ? (save_hdws l)
176    ]
177  ].
178
179definition get_param_stack ≝
180  λoff: nat.
181  λdestr.
182  λstart_lbl, dest_lbl: label.
183  λdef.
184  let 〈def, addr1〉 ≝ fresh_reg def in
185  let 〈def, addr2〉 ≝ fresh_reg def in
186  let 〈def, tmpr〉 ≝ fresh_reg def in
187  let 〈int_offset, ignore〉 ≝ add_8_with_carry (bitvector_of_nat ? off) int_size false in
188  adds_graph [
189    ertl_st_frame_size addr1 start_lbl;
190    ertl_st_int tmpr int_offset start_lbl;
191    ertl_st_op2 Sub addr1 addr1 tmpr start_lbl;
192    ertl_st_get_hdw tmpr RegisterSPL start_lbl;
193    ertl_st_op2 Add addr1 addr1 tmpr start_lbl;
194    ertl_st_int addr2 (bitvector_of_nat 8 0) start_lbl;
195    ertl_st_get_hdw tmpr RegisterSPH start_lbl;
196    ertl_st_op2 Addc addr2 addr2 tmpr start_lbl;
197    ertl_st_load destr addr1 addr2 start_lbl
198  ] start_lbl dest_lbl def.
199 
200definition get_params_stack_internal ≝
201  λi.
202  λr.
203    get_param_stack i r.
204 
205definition get_params_stack ≝
206  λparams.
207  match length ? params with
208  [ O ⇒ [ get_params_hdw_internal ]
209  | _ ⇒ mapi ? ? get_params_stack_internal params
210  ].
211
212definition get_params ≝
213  λparams.
214  let n ≝ min (length ? params) (length ? parameters) in
215  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
216  match get_params_hdw hdw_params with
217  [ None ⇒ None ?
218  | Some hdw_params ⇒ Some ? (hdw_params @ (get_params_stack stack_params))
219  ].
220 
221definition add_prologue ≝
222  λparams.
223  λsral.
224  λsrah.
225  λsregs.
226  λdef.
227  let start_lbl ≝ ertl_if_entry def in
228  let tmp_lbl ≝ fresh_label def in
229  match tmp_lbl with
230  [ None ⇒ None ?
231  | Some tmp_lbl ⇒
232    let last_stmt ≝ lookup ? ? (ertl_if_graph def) start_lbl in
233    let params ≝
234      match get_params params with
235      [ Some params ⇒ params
236      | None ⇒ [ ] (* dpm: is this ok? *)
237      ] in
238    let def ≝
239      add_translates (
240        adds_graph [ ertl_st_new_frame start_lbl ] ::
241        adds_graph [ ertl_st_pop sral start_lbl; ertl_st_pop srah start_lbl ] ::
242        save_hdws sregs @
243        params) start_lbl tmp_lbl def in
244    match def with
245    [ Some def ⇒
246      match last_stmt with
247      [ Some last_stmt ⇒ Some ? (add_graph tmp_lbl last_stmt def)
248      | None ⇒ None ?
249      ]
250    | None ⇒ None ?
251    ]
252  ].
253 
254definition allocate_regs_internal ≝
255  λr: register.
256  λdef_sregs.
257  let 〈def, sregs〉 ≝ def_sregs in
258  let 〈def, r'〉 ≝ fresh_reg def in
259    〈def, 〈r', r〉 :: sregs〉.
260 
261definition allocate_regs ≝
262  λrs: register_set.
263  λsaved: rs_set rs.
264  λdef.
265    rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉.
266   
267definition save_return_internal ≝
268  λr.
269  λstart_lbl.
270  λdest_lbl.
271  λdef.
272  let 〈def, r_tmp〉 ≝ fresh_reg def in
273  adds_graph [
274    ertl_st_int r_tmp (bitvector_of_nat ? 0) start_lbl;
275    ertl_st_set_hdw RegisterST0 r start_lbl;
276    ertl_st_set_hdw RegisterST1 r_tmp start_lbl ] start_lbl dest_lbl def.
277   
278definition save_return_internal' ≝
279  λr1, r2.
280  λstart_lbl.
281  adds_graph [
282    ertl_st_set_hdw RegisterST0 r1 start_lbl;
283    ertl_st_set_hdw RegisterST1 r2 start_lbl
284  ] start_lbl.
285   
286definition save_return ≝
287  λret_regs.
288  match ret_regs with
289  [ nil ⇒ [ get_params_hdw_internal ]
290  | cons hd tl ⇒
291    match tl with
292    [ nil ⇒ [ save_return_internal hd ]
293    | cons hd' tl' ⇒ [ save_return_internal' hd hd' ]
294    ]
295  ].
296   
297definition add_epilogue ≝
298  λret_regs.
299  λsral.
300  λsrah.
301  λsregs.
302  λdef.
303  let start_lbl ≝ ertl_if_exit def in
304  let tmp_lbl ≝ fresh_label def in
305  match tmp_lbl with
306  [ None ⇒ None ?
307  | Some tmp_lbl ⇒
308    let last_stmt ≝ lookup ? ? (ertl_if_graph def) start_lbl in
309    match last_stmt with
310    [ None ⇒ None ?
311    | Some last_stmt ⇒
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          [adds_graph [
324            ertl_st_hdw_to_hdw RegisterDPL RegisterST0 start_lbl;
325            ertl_st_hdw_to_hdw RegisterDPH RegisterST1 start_lbl
326          ]]) start_lbl tmp_lbl def in
327      match def with
328      [ None ⇒ None ?
329      | Some def ⇒
330        let def ≝ add_graph tmp_lbl last_stmt def in
331          Some ? (change_exit_label tmp_lbl def)
332      ]
333    ]
334  ].
335 
336axiom add_pro_and_epilogue:
337  ∀rs: register_set.
338  ∀params: list register.
339  ∀ret_args: list register.
340  ∀def: ertl_internal_function.
341    option ertl_internal_function.
342   
343(*
344  dpm: address callee_saved problem   
345definition add_pro_and_epilogue ≝
346  λrs: register_set.
347  λparams.
348  λret_args.
349  λdef.
350  let 〈def, sra〉 ≝ fresh_regs def 2 in
351  let sral ≝ safe_nth ? 0 sra ? in
352  let srah ≝ safe_nth ? 1 sra ? in
353  let 〈def, sregs〉 ≝ allocate_regs callee_saved def in
354  let def ≝ add_prologue params sral srah sregs def in
355  let def ≝ add_epilogue ret_args sral srah sregs def in
356    def. 
357*)
358
359definition set_params_hdw ≝
360  λparams.
361  match length ? params with
362  [ O ⇒ Some ? [ get_params_hdw_internal ]
363  | _ ⇒
364    match zip ? ? params parameters with
365    [ None ⇒ None ?
366    | Some zipped_params ⇒ Some ? (restore_hdws zipped_params)
367    ]
368  ].
369 
370definition set_param_stack ≝
371  λoff: nat.
372  λsrcr.
373  λstart_lbl, dest_lbl: label.
374  λdef.
375  let 〈def, addr1〉 ≝ fresh_reg def in
376  let 〈def, addr2〉 ≝ fresh_reg def in
377  let 〈def, tmpr〉 ≝ fresh_reg def in
378  let 〈int_offset, ignore〉 ≝ add_8_with_carry (bitvector_of_nat ? off) int_size false in
379    adds_graph [
380      ertl_st_int addr2 int_offset start_lbl;
381      ertl_st_get_hdw tmpr RegisterSPL start_lbl;
382      ertl_st_clear_carry start_lbl;
383      ertl_st_op2 Sub addr1 tmpr addr1 start_lbl;
384      ertl_st_get_hdw tmpr RegisterSPH start_lbl;
385      ertl_st_int addr2 (bitvector_of_nat ? 0) start_lbl;
386      ertl_st_op2 Sub addr2 tmpr addr2 start_lbl;
387      ertl_st_store addr1 addr2 srcr start_lbl
388    ] start_lbl dest_lbl def.
389
390definition set_params_stack ≝
391  λparams.
392  match length ? params with
393  [ O ⇒ [ get_params_hdw_internal ]
394  | _ ⇒ mapi ? ? set_param_stack params
395 
396  ].
397 
398definition set_params ≝
399  λparams.
400  let n ≝ min (length ? params) (length ? parameters) in
401  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
402    match set_params_hdw hdw_params with
403    [ None ⇒ None ?
404    | Some hdw_params' ⇒ Some ? (hdw_params' @ (set_params_stack stack_params))
405    ].
406   
407definition fetch_result ≝
408  λret_regs.
409  λstart_lbl.
410  match ret_regs with
411  [ nil ⇒ adds_graph [ertl_st_skip start_lbl] start_lbl
412  | cons hd tl ⇒
413    match tl with
414    [ nil ⇒
415      adds_graph [
416        ertl_st_hdw_to_hdw RegisterST0 RegisterDPL start_lbl;
417        ertl_st_get_hdw hd RegisterST0 start_lbl
418      ] start_lbl
419    | cons hd' tl' ⇒
420      adds_graph [
421        ertl_st_hdw_to_hdw RegisterST0 RegisterDPL start_lbl;
422        ertl_st_hdw_to_hdw RegisterST1 RegisterDPH start_lbl;
423        ertl_st_get_hdw hd RegisterST0 start_lbl;
424        ertl_st_get_hdw hd' RegisterST1 start_lbl
425      ] start_lbl
426    ]
427  ].
428 
429definition translate_call_id ≝
430  λf.
431  λargs.
432  λret_regs.
433  λstart_lbl, dest_lbl: label.
434  λdef.
435  let nb_args ≝ bitvector_of_nat ? (length ? args) in
436  match set_params args with
437  [ None ⇒ None ?
438  | Some params_args ⇒
439    add_translates (
440      params_args @ [
441        adds_graph [ ertl_st_call_id f nb_args start_lbl ] ;
442        fetch_result ret_regs
443      ]) start_lbl dest_lbl def
444  ].
445 
446definition translate_stmt ≝
447  λlbl: label.
448  λstmt: rtl_statement.
449  λdef: ertl_internal_function.
450  match stmt with
451  [ rtl_st_skip lbl' ⇒
452    Some ? (add_graph lbl (ertl_st_skip lbl') def)
453  | rtl_st_cost cost_lbl lbl' ⇒
454    Some ? (add_graph lbl (ertl_st_cost cost_lbl lbl') def)
455  | rtl_st_addr r1 r2 x lbl' ⇒
456    adds_graph [
457      ertl_st_addr_l r1 x lbl;
458      ertl_st_addr_h r2 x lbl
459    ] lbl lbl' def
460  | rtl_st_stack_addr r1 r2 lbl' ⇒
461    adds_graph [
462      ertl_st_get_hdw r1 RegisterSPL lbl;
463      ertl_st_get_hdw r2 RegisterSPH lbl
464    ] lbl lbl' def
465  | rtl_st_int r i lbl' ⇒
466    Some ? (add_graph lbl (ertl_st_int r i lbl') def)
467  | rtl_st_move r1 r2 lbl' ⇒
468    Some ? (add_graph lbl (ertl_st_move r1 r2 lbl') def)
469  | rtl_st_opaccs opaccs d s1 s2 lbl' ⇒
470    Some ? (add_graph lbl (ertl_st_opaccs opaccs d s1 s2 lbl') def)
471  | rtl_st_op1 op1 d s lbl' ⇒
472    Some ? (add_graph lbl (ertl_st_op1 op1 d s lbl') def)
473  | rtl_st_op2 op2 d s1 s2 lbl' ⇒
474    Some ? (add_graph lbl (ertl_st_op2 op2 d s1 s2 lbl') def)
475  | rtl_st_clear_carry lbl' ⇒
476    Some ? (add_graph lbl (ertl_st_clear_carry lbl') def)
477  | rtl_st_load d a1 a2 lbl' ⇒
478    Some ? (add_graph lbl (ertl_st_load d a1 a2 lbl') def)
479  | rtl_st_store a1 a2 s lbl' ⇒
480    Some ? (add_graph lbl (ertl_st_store a1 a2 s lbl') def)
481  | rtl_st_call_id f args ret_regs lbl' ⇒
482    translate_call_id f args ret_regs lbl lbl' def
483  | rtl_st_call_ptr r1 r2 regs1 regs2 lbl ⇒ None ? (* dpm: todo *)
484  | rtl_st_cond_acc src lbl_true lbl_false ⇒
485    Some ? (add_graph lbl (ertl_st_cond_acc src lbl_true lbl_false) def)
486  | rtl_st_return ret_regs ⇒
487    Some ? (add_graph lbl (ertl_st_return ret_regs) def)
488  | rtl_st_tailcall_id ident regs ⇒ None ? (* dpm: impossible *)
489  | rtl_st_tailcall_ptr r1 r2 regs ⇒ None ? (* dpm: impossible *)
490  ].
491
492(* dpm: this should not be option, fix *)
493axiom map_fold:
494  ∀A, B: Type[0].
495  ∀f: label → A → B → option B.
496  ∀m: rtl_statement_graph.
497  ∀b: B.
498    B.
499   
500definition translate_internal ≝
501  λdef.
502  let nb_params ≝ length ? (rtl_if_params def) in
503  let added_stacksize ≝ max 0 (nb_params - (length ? parameters)) in
504  let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in
505  let def' ≝
506    mk_ertl_internal_function
507      (rtl_if_luniverse def) (rtl_if_runiverse def)
508      nb_params new_locals ((rtl_if_stacksize def) + added_stacksize)
509      (empty_map ? ?) (rtl_if_entry def) (rtl_if_exit def) in
510  let def' ≝ map_fold ? ? translate_stmt (rtl_if_graph def) def' in
511  let def' ≝ add_pro_and_epilogue register_list_set (rtl_if_params def) (rtl_if_result def) def' in
512    def'.
513   
514definition translate_funct ≝
515  λid_def: ident × ?.
516  let 〈id, def〉 ≝ id_def in
517  let def' ≝
518    match def with
519    [ rtl_f_internal def ⇒
520      match translate_internal def with
521      [ None ⇒ None ?
522      | Some internal_def ⇒ Some ? (ertl_f_internal internal_def)
523      ]
524    | rtl_f_external def ⇒ Some ? (ertl_f_external def)
525    ] in
526  〈id, def'〉.
527
528definition generate ≝
529  λstmt.
530  λdef.
531  let entry ≝ fresh_label def in
532  match entry with
533  [ None ⇒ None ?
534  | Some entry ⇒
535    let def ≝ add_graph entry stmt def in
536      Some ? (change_entry_label entry def)
537  ].
538 
Note: See TracBrowser for help on using the repository browser.