source: src/RTL/RTLtoERTL.ma @ 777

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

Lots of work on RTL to ERTL pass from today.

File size: 10.7 KB
Line 
1include "RTL/RTL.ma".
2include "ERTL/ERTL.ma".
3include "ASM/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_graph' ≝ ertl_if_graph p in
13  let ertl_if_entry' ≝ ertl_if_entry p in
14  let ertl_if_exit' ≝ l in
15    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
16                              ertl_if_params' ertl_if_locals'
17                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
18
19definition change_entry_label ≝
20  λl: label.
21  λp: ertl_internal_function.
22  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
23  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
24  let ertl_if_params' ≝ ertl_if_params p in
25  let ertl_if_locals' ≝ ertl_if_locals p in
26  let ertl_if_graph' ≝ ertl_if_graph p in
27  let ertl_if_entry' ≝ l in
28  let ertl_if_exit' ≝ ertl_if_exit p in
29    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
30                              ertl_if_params' ertl_if_locals'
31                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
32                             
33definition add_graph ≝
34  λl: label.
35  λstmt.
36  λp.
37  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
38  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
39  let ertl_if_params' ≝ ertl_if_params p in
40  let ertl_if_locals' ≝ ertl_if_locals p in
41  let ertl_if_graph' ≝ add ? ? (ertl_if_graph p) l stmt in
42  let ertl_if_entry' ≝ ertl_if_entry p in
43  let ertl_if_exit' ≝ ertl_if_exit p in
44    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
45                              ertl_if_params' ertl_if_locals'
46                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
47                             
48definition fresh_label ≝
49  λdef.
50    match fresh LabelTag (ertl_if_luniverse def) with
51    [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ)
52    | Error ⇒ None ?
53    ].
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 opaccs d s1 s2 _ ⇒ ertl_st_opaccs opaccs d s1 s2 l
75  | ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l
76  | ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l
77  | ertl_st_clear_carry _ ⇒ ertl_st_clear_carry l
78  | ertl_st_load d a1 a2 _ ⇒ ertl_st_load d a1 a2 l
79  | ertl_st_store a1 a2 s _ ⇒ ertl_st_store a1 a2 s l
80  | ertl_st_call_id f args _ ⇒ ertl_st_call_id f args l
81  | ertl_st_cond_acc a i1 i2 ⇒ ertl_st_cond_acc a i1 i2
82  | ertl_st_return a ⇒ ertl_st_return a
83  ].
84 
85let rec adds_graph (stmt_list: list ertl_statement) (start_lbl: label) (dest_lbl: label) (def: ertl_internal_function): option ertl_internal_function ≝
86  match stmt_list with
87  [ nil ⇒ Some ? def
88  | cons hd tl ⇒
89    match tl with
90    [ nil ⇒ Some ? (add_graph start_lbl (change_label dest_lbl hd) def)
91    | _ ⇒
92      let tmp_lbl ≝ fresh_label def in
93      match tmp_lbl with
94      [ Some tmp_lbl ⇒
95        let stmt ≝ change_label tmp_lbl hd in
96        let def ≝ add_graph start_lbl hd def in
97          adds_graph tl tmp_lbl dest_lbl def
98      | None ⇒ None ?
99      ]
100    ]
101  ].
102
103let rec add_translates (translate_list: list (label → label → ertl_internal_function → option ertl_internal_function))
104                       (start_lbl: label) (dest_lbl: label)
105                       (def: ertl_internal_function): option ertl_internal_function ≝
106  match translate_list with
107  [ nil ⇒ Some ? def
108  | cons hd tl ⇒
109    match tl with
110    [ nil ⇒ hd start_lbl dest_lbl def
111    | _ ⇒
112      let tmp_lbl ≝ fresh_label def in
113      match tmp_lbl with
114      [ Some tmp_lbl ⇒
115        match hd start_lbl tmp_lbl def with
116        [ Some def ⇒ add_translates tl tmp_lbl dest_lbl def
117        | None ⇒ None ?
118        ]
119      | None ⇒ None ?
120      ]
121    ]
122  ].
123 
124axiom fresh_reg: ertl_internal_function → ertl_internal_function × register.
125
126let rec fresh_regs (def: ertl_internal_function) (n: nat) on n ≝
127  match n with
128  [ O ⇒ 〈def, [ ]〉
129  | S n' ⇒
130    let 〈def', regs'〉 ≝ fresh_regs def n' in
131    let 〈def', reg〉 ≝ fresh_reg def' in
132      〈def', reg :: regs'〉
133  ].
134 
135definition save_hdws_internal ≝
136  λdestr_srcr: register × hardware_register.
137  λstart_lbl: label.
138    let 〈destr, srcr〉 ≝ destr_srcr in
139      adds_graph [ ertl_st_get_hdw destr srcr start_lbl ] start_lbl.
140 
141definition save_hdws ≝
142  λl.
143    map ? ? save_hdws_internal l.
144   
145definition restore_hdws_internal ≝
146  λdestr_srcr: hardware_register × register.
147  λstart_lbl: label.
148    let 〈destr, srcr〉 ≝ destr_srcr in
149    adds_graph [ ertl_st_set_hdw destr srcr start_lbl ] start_lbl.
150   
151definition swap_components ≝
152  λA, B: Type[0].
153  λp: A × B.
154  let 〈l, r〉 ≝ p in
155  〈r, l〉.
156   
157definition restore_hdws ≝
158  λl.
159    map ? ? restore_hdws_internal (map ? ? (swap_components ? ?) l).
160
161definition get_params_hdw_internal ≝
162  λstart_lbl: label.
163    adds_graph [ ertl_st_skip start_lbl ] start_lbl.
164
165definition get_params_hdw ≝
166  λparams: list register.
167  match length ? params with
168  [ O ⇒ Some ? [ get_params_hdw_internal ]
169  | _ ⇒
170    match zip ? ? params parameters with
171    [ None ⇒ None ?
172    | Some l ⇒ Some ? (save_hdws l)
173    ]
174  ].
175
176definition get_param_stack ≝
177  λoff: nat.
178  λdestr.
179  λstart_lbl, dest_lbl: label.
180  λdef.
181  let 〈def, addr1〉 ≝ fresh_reg def in
182  let 〈def, addr2〉 ≝ fresh_reg def in
183  let 〈def, tmpr〉 ≝ fresh_reg def in
184  let 〈int_offset, ignore〉 ≝ add_8_with_carry (bitvector_of_nat ? off) int_size false in
185  adds_graph [
186    ertl_st_frame_size addr1 start_lbl;
187    ertl_st_int tmpr int_offset start_lbl;
188    ertl_st_op2 Sub addr1 addr1 tmpr start_lbl;
189    ertl_st_get_hdw tmpr RegisterSPL start_lbl;
190    ertl_st_op2 Add addr1 addr1 tmpr start_lbl;
191    ertl_st_int addr2 (bitvector_of_nat 8 0) start_lbl;
192    ertl_st_get_hdw tmpr RegisterSPH start_lbl;
193    ertl_st_op2 Addc addr2 addr2 tmpr start_lbl;
194    ertl_st_load destr addr1 addr2 start_lbl
195  ] start_lbl dest_lbl def.
196 
197definition get_params_stack_internal ≝
198  λi.
199  λr.
200    get_param_stack i r.
201 
202definition get_params_stack ≝
203  λparams.
204  match length ? params with
205  [ O ⇒ [ get_params_hdw_internal ]
206  | _ ⇒ mapi ? ? get_params_stack_internal params
207  ].
208
209definition get_params ≝
210  λparams.
211  let n ≝ min (length ? params) (length ? parameters) in
212  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
213  match get_params_hdw hdw_params with
214  [ None ⇒ None ?
215  | Some hdw_params ⇒ Some ? (hdw_params @ (get_params_stack stack_params))
216  ].
217 
218definition add_prologue ≝
219  λparams.
220  λsral.
221  λsrah.
222  λsregs.
223  λdef.
224  let start_lbl ≝ ertl_if_entry def in
225  let tmp_lbl ≝ fresh_label def in
226  match tmp_lbl with
227  [ None ⇒ None ?
228  | Some tmp_lbl ⇒
229    let last_stmt ≝ lookup ? ? (ertl_if_graph def) start_lbl in
230    let params ≝
231      match get_params params with
232      [ Some params ⇒ params
233      | None ⇒ [ ] (* dpm: is this ok? *)
234      ] in
235    let def ≝
236      add_translates (
237        adds_graph [ ertl_st_new_frame start_lbl ] ::
238        adds_graph [ ertl_st_pop sral start_lbl; ertl_st_pop srah start_lbl ] ::
239        save_hdws sregs @
240        params) start_lbl tmp_lbl def in
241    match def with
242    [ Some def ⇒
243      match last_stmt with
244      [ Some last_stmt ⇒ Some ? (add_graph tmp_lbl last_stmt def)
245      | None ⇒ None ?
246      ]
247    | None ⇒ None ?
248    ]
249  ].
250 
251definition allocate_regs_internal ≝
252  λr: register.
253  λdef_sregs.
254  let 〈def, sregs〉 ≝ def_sregs in
255  let 〈def, r'〉 ≝ fresh_reg def in
256    〈def, 〈r', r〉 :: sregs〉.
257 
258definition allocate_regs ≝
259  λrs: register_set.
260  λsaved: rs_set rs.
261  λdef.
262    rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉.
263   
264definition save_return_internal ≝
265  λr.
266  λstart_lbl.
267  λdest_lbl.
268  λdef.
269  let 〈def, r_tmp〉 ≝ fresh_reg def in
270  adds_graph [
271    ertl_st_int r_tmp (bitvector_of_nat ? 0) start_lbl;
272    ertl_st_set_hdw RegisterST0 r start_lbl;
273    ertl_st_set_hdw RegisterST1 r_tmp start_lbl ] start_lbl dest_lbl def.
274   
275definition save_return_internal' ≝
276  λr1, r2.
277  λstart_lbl.
278  adds_graph [
279    ertl_st_set_hdw RegisterST0 r1 start_lbl;
280    ertl_st_set_hdw RegisterST1 r2 start_lbl
281  ] start_lbl.
282   
283definition save_return ≝
284  λret_regs.
285  match ret_regs with
286  [ nil ⇒ [ get_params_hdw_internal ]
287  | cons hd tl ⇒
288    match tl with
289    [ nil ⇒ [ save_return_internal hd ]
290    | cons hd' tl' ⇒ [ save_return_internal' hd hd' ]
291    ]
292  ].
293   
294definition add_epilogue ≝
295  λret_regs.
296  λsral.
297  λsrah.
298  λsregs.
299  λdef.
300  let start_lbl ≝ ertl_if_exit def in
301  let tmp_lbl ≝ fresh_label def in
302  match tmp_lbl with
303  [ None ⇒ None ?
304  | Some tmp_lbl ⇒
305    let last_stmt ≝ lookup ? ? (ertl_if_graph def) start_lbl in
306    match last_stmt with
307    [ None ⇒ None ?
308    | Some last_stmt ⇒
309      let def ≝
310        add_translates (
311          save_return ret_regs @
312          restore_hdws sregs @
313          [adds_graph [
314            ertl_st_push srah start_lbl;
315            ertl_st_push sral start_lbl
316          ]] @
317          [adds_graph [
318            ertl_st_del_frame start_lbl
319          ]] @
320          [adds_graph [
321            ertl_st_hdw_to_hdw RegisterDPL RegisterST0 start_lbl;
322            ertl_st_hdw_to_hdw RegisterDPH RegisterST1 start_lbl
323          ]]) start_lbl tmp_lbl def in
324      match def with
325      [ None ⇒ None ?
326      | Some def ⇒
327        let def ≝ add_graph tmp_lbl last_stmt def in
328          Some ? (change_exit_label tmp_lbl def)
329      ]
330    ]
331  ].
332   
333definition add_pro_and_epilogue ≝
334  λrs: register_set.
335  λparams.
336  λret_args.
337  λdef.
338  let 〈def, sra〉 ≝ fresh_regs def 2 in
339  let sral ≝ nth ? 0 sra in
340  let srah ≝ nth sra 1 in
341  let 〈def, sregs〉 ≝ allocate_regs callee_saved def in
342  let def ≝ add_prologue params sral srah sregs def in
343  let def ≝ add_epilogue ret_args sral srah sregs def in
344    def.
Note: See TracBrowser for help on using the repository browser.