1 | include "RTL/RTLTailcall_paolo.ma". |
---|
2 | include "utilities/RegisterSet.ma". |
---|
3 | include "common/Identifiers.ma". |
---|
4 | include "ERTL/ERTL_paolo.ma". |
---|
5 | include "joint/TranslateUtils_paolo.ma". |
---|
6 | |
---|
7 | include alias "basics/lists/list.ma". |
---|
8 | |
---|
9 | definition save_hdws : |
---|
10 | ∀globals.list (register×Register) → list (joint_seq ertl_params globals) ≝ |
---|
11 | λglobals. |
---|
12 | let save_hdws_internal ≝ |
---|
13 | λdestr_srcr.PSD (\fst destr_srcr) ← HDW (\snd destr_srcr) in |
---|
14 | map ?? save_hdws_internal. |
---|
15 | |
---|
16 | definition restore_hdws : |
---|
17 | ∀globals.list (rtl_argument×Register) → list (joint_seq ertl_params globals) ≝ |
---|
18 | λglobals. |
---|
19 | let restore_hdws_internal ≝ |
---|
20 | λdestr_srcr:rtl_argument×?.HDW (\snd destr_srcr) ← \fst destr_srcr in |
---|
21 | map ? ? restore_hdws_internal. |
---|
22 | |
---|
23 | definition get_params_hdw : |
---|
24 | ∀globals.list register → list (joint_seq ertl_params globals) ≝ |
---|
25 | λglobals,params. |
---|
26 | save_hdws … (zip_pottier … params RegisterParams). |
---|
27 | |
---|
28 | (* Paolo: The following can probably be done way more efficiently with INC DPTR *) |
---|
29 | |
---|
30 | definition get_param_stack : |
---|
31 | ∀globals.register → register → nat → register → |
---|
32 | list (joint_seq ertl_params globals) ≝ |
---|
33 | λglobals,addr1,addr2,off,destr. |
---|
34 | let int_offset : Byte ≝ \snd (half_add ? (bitvector_of_nat ? off) int_size) in |
---|
35 | [ (ertl_frame_size addr1 : joint_seq ??) ; |
---|
36 | CLEAR_CARRY … ; |
---|
37 | addr1 ← addr1 .Sub. int_offset ; (* are we sure carry bit is unimportant? *) |
---|
38 | PSD destr ← HDW RegisterSPL ; |
---|
39 | addr1 ← addr1 .Add. destr ; |
---|
40 | PSD addr2 ← HDW RegisterSPH ; |
---|
41 | addr2 ← addr2 .Addc. 0 ; |
---|
42 | LOAD … destr addr1 addr2 |
---|
43 | ]. |
---|
44 | |
---|
45 | definition get_params_stack : |
---|
46 | ∀globals.list register → |
---|
47 | bind_new (localsT ertl_params) (list (joint_seq ertl_params globals)) ≝ |
---|
48 | λglobals,params. |
---|
49 | νaddr1,addr2 in |
---|
50 | flatten … (mapi ?? (get_param_stack globals addr1 addr2) params). |
---|
51 | |
---|
52 | definition get_params ≝ |
---|
53 | λglobals,params. |
---|
54 | let n ≝ min (length … params) (length … RegisterParams) in |
---|
55 | let 〈hdw_params, stack_params〉 ≝ list_split … n params in |
---|
56 | get_params_hdw globals hdw_params @@ get_params_stack … stack_params. |
---|
57 | |
---|
58 | definition prologue : |
---|
59 | ∀globals.list register → register → register → list (register×Register) → |
---|
60 | bind_new (localsT ertl_params) (list (joint_seq ertl_params globals)) ≝ |
---|
61 | λglobals,params,sral,srah,sregs. |
---|
62 | [ (ertl_new_frame : joint_seq ??) ; |
---|
63 | POP … sral ; |
---|
64 | POP … srah |
---|
65 | ] @@ save_hdws … sregs @@ get_params … params. |
---|
66 | |
---|
67 | definition save_return : |
---|
68 | ∀globals.list rtl_argument → list (joint_seq ertl_params globals) ≝ |
---|
69 | λglobals,ret_regs. |
---|
70 | match reduce_strong ? ? RegisterSTS ret_regs with |
---|
71 | [ mk_Sig crl crl_proof ⇒ |
---|
72 | let commonl ≝ \fst (\fst crl) in |
---|
73 | let commonr ≝ \fst (\snd crl) in |
---|
74 | let restl ≝ \snd (\fst crl) in |
---|
75 | (* let restr ≝ \snd (\snd crl) in *) |
---|
76 | map2 … (λst.λr : rtl_argument.HDW st ← r) commonl commonr crl_proof @ |
---|
77 | map … (λst.HDW st ← 0) restl |
---|
78 | ]. |
---|
79 | |
---|
80 | definition assign_result : ∀globals.list (joint_seq ertl_params globals) ≝ |
---|
81 | λglobals. |
---|
82 | match reduce_strong ?? RegisterRets RegisterSTS with |
---|
83 | [ mk_Sig crl crl_proof ⇒ |
---|
84 | let commonl ≝ \fst (\fst crl) in |
---|
85 | let commonr ≝ \fst (\snd crl) in |
---|
86 | map2 … (λret,st.HDW ret ← HDW st) commonl commonr crl_proof |
---|
87 | ]. |
---|
88 | |
---|
89 | definition epilogue : |
---|
90 | ∀globals.list register → register → register → list (register × Register) → |
---|
91 | list (joint_seq ertl_params globals) ≝ |
---|
92 | λglobals,ret_regs,sral,srah,sregs. |
---|
93 | save_return … (map … Reg ret_regs) @ |
---|
94 | restore_hdws … (map … (λpr.〈Reg (\fst pr),\snd pr〉) sregs) @ |
---|
95 | [ PUSH ertl_params ? srah ; |
---|
96 | PUSH … sral ; |
---|
97 | ertl_del_frame ] @ |
---|
98 | assign_result globals. |
---|
99 | |
---|
100 | definition allocate_regs : |
---|
101 | ∀globals,rs.rs_set rs → |
---|
102 | state_monad (joint_internal_function globals ertl_params) (list (register×Register)) ≝ |
---|
103 | λglobals,rs,saved,def. |
---|
104 | let allocate_regs_internal ≝ |
---|
105 | λr: Register. |
---|
106 | λdef_sregs. |
---|
107 | let 〈def, r'〉 ≝ rtl_ertl_fresh_reg … (\fst def_sregs) in |
---|
108 | 〈def, 〈r', r〉::\snd def_sregs〉 in |
---|
109 | rs_fold ?? allocate_regs_internal saved 〈def, [ ]〉. |
---|
110 | |
---|
111 | definition add_pro_and_epilogue : |
---|
112 | ∀globals.list register → list register → |
---|
113 | joint_internal_function globals ertl_params → |
---|
114 | joint_internal_function globals ertl_params ≝ |
---|
115 | λglobals,params,ret_regs,def. |
---|
116 | let start_lbl ≝ joint_if_entry … def in |
---|
117 | let end_lbl ≝ joint_if_exit … def in |
---|
118 | state_run … def ( |
---|
119 | ! sral ← rtl_ertl_fresh_reg … ; |
---|
120 | ! srah ← rtl_ertl_fresh_reg … ; |
---|
121 | ! sregs ← allocate_regs … register_list_set RegisterCalleeSaved ; |
---|
122 | ! prologue' ← bcompile … (rtl_ertl_fresh_reg …) (prologue … params sral srah sregs) ; |
---|
123 | let epilogue' ≝ epilogue … ret_regs sral srah sregs in |
---|
124 | ! def' ← state_get … ; |
---|
125 | let def'' ≝ insert_prologue … prologue' def' in |
---|
126 | return insert_epilogue … epilogue' def'' |
---|
127 | ). |
---|
128 | |
---|
129 | definition set_params_hdw : |
---|
130 | ∀globals.list rtl_argument → list (joint_seq ertl_params globals) ≝ |
---|
131 | λglobals,params. |
---|
132 | restore_hdws globals (zip_pottier ? ? params RegisterParams). |
---|
133 | |
---|
134 | (* Paolo: The following can probably be done way more efficiently with INC DPTR *) |
---|
135 | |
---|
136 | definition set_param_stack : |
---|
137 | ∀globals.register → register → nat → rtl_argument → |
---|
138 | list (joint_seq ertl_params globals) ≝ |
---|
139 | λglobals,addr1,addr2,off,arg. |
---|
140 | let int_off : Byte ≝ \snd (half_add ? (bitvector_of_nat ? off) int_size) in |
---|
141 | [ PSD addr1 ← HDW RegisterSPL ; |
---|
142 | CLEAR_CARRY … ; |
---|
143 | addr1 ← addr1 .Sub. int_off ; |
---|
144 | PSD addr2 ← HDW RegisterSPH ; |
---|
145 | addr2 ← addr2 .Sub. 0 ; |
---|
146 | STORE … addr1 addr2 arg |
---|
147 | ]. |
---|
148 | |
---|
149 | definition set_params_stack : |
---|
150 | ∀globals.list rtl_argument → bind_new (localsT ertl_params) ? ≝ |
---|
151 | λglobals,params. |
---|
152 | νaddr1,addr2 in |
---|
153 | flatten … (mapi … (set_param_stack globals addr1 addr2) params). |
---|
154 | |
---|
155 | definition set_params ≝ |
---|
156 | λglobals,params. |
---|
157 | let n ≝ min (|params|) (|RegisterParams|) in |
---|
158 | let hdw_stack_params ≝ split ? params n in |
---|
159 | let hdw_params ≝ \fst hdw_stack_params in |
---|
160 | let stack_params ≝ \snd hdw_stack_params in |
---|
161 | set_params_hdw globals hdw_params @@ set_params_stack globals stack_params. |
---|
162 | |
---|
163 | definition fetch_result : |
---|
164 | ∀globals.list register → list (joint_seq ertl_params globals) ≝ |
---|
165 | λglobals,ret_regs. |
---|
166 | match reduce_strong ?? RegisterSTS RegisterRets with |
---|
167 | [ mk_Sig crl crl_proof ⇒ |
---|
168 | let commonl ≝ \fst (\fst crl) in |
---|
169 | let commonr ≝ \fst (\snd crl) in |
---|
170 | map2 … (λst,r.HDW st ← HDW r) commonl commonr crl_proof @ |
---|
171 | match reduce_strong ?? ret_regs RegisterSTS with |
---|
172 | [ mk_Sig crl crl_proof ⇒ |
---|
173 | let commonl ≝ \fst (\fst crl) in |
---|
174 | let commonr ≝ \fst (\snd crl) in |
---|
175 | map2 … (λret,st.PSD ret ← HDW st) commonl commonr crl_proof |
---|
176 | ] |
---|
177 | ]. |
---|
178 | |
---|
179 | definition translate_step : |
---|
180 | ∀globals.label → joint_step rtlntc_params globals → |
---|
181 | bind_seq_block ertl_params globals (joint_step ertl_params globals) ≝ |
---|
182 | λglobals.λ_.λs. |
---|
183 | match s return λ_.bind_seq_block ?? (joint_step ??) with |
---|
184 | [ step_seq s ⇒ |
---|
185 | match s return λ_.bind_seq_block ?? (joint_step ??) with |
---|
186 | [ PUSH _ ⇒ NOOP … (*CSC: XXXX should not be in the syntax *) |
---|
187 | | POP _ ⇒ NOOP … (*CSC: XXXX should not be in the syntax *) |
---|
188 | | MOVE rs ⇒ PSD (\fst rs) ← |
---|
189 | match \snd rs with |
---|
190 | [ Reg src ⇒ PSD src |
---|
191 | | Imm b ⇒ INT b |
---|
192 | ] |
---|
193 | | COST_LABEL lbl ⇒ |
---|
194 | COST_LABEL … lbl |
---|
195 | | ADDRESS x prf r1 r2 ⇒ |
---|
196 | ADDRESS ertl_params ? x prf r1 r2 |
---|
197 | | OPACCS op destr1 destr2 srcr1 srcr2 ⇒ |
---|
198 | OPACCS ertl_params ? op destr1 destr2 srcr1 srcr2 |
---|
199 | | OP1 op1 destr srcr ⇒ |
---|
200 | OP1 ertl_params ? op1 destr srcr |
---|
201 | | OP2 op2 destr srcr1 srcr2 ⇒ |
---|
202 | OP2 ertl_params ? op2 destr srcr1 srcr2 |
---|
203 | | CLEAR_CARRY ⇒ |
---|
204 | CLEAR_CARRY … |
---|
205 | | SET_CARRY ⇒ |
---|
206 | SET_CARRY … |
---|
207 | | LOAD destr addr1 addr2 ⇒ |
---|
208 | LOAD ertl_params ? destr addr1 addr2 |
---|
209 | | STORE addr1 addr2 srcr ⇒ |
---|
210 | STORE ertl_params ? addr1 addr2 srcr |
---|
211 | | COMMENT msg ⇒ |
---|
212 | COMMENT … msg |
---|
213 | | extension_seq ext ⇒ |
---|
214 | match ext with |
---|
215 | [ rtl_stack_address addr1 addr2 ⇒ |
---|
216 | [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ] |
---|
217 | ] |
---|
218 | | CALL_ID f args ret_regs ⇒ |
---|
219 | set_params ? args @@ |
---|
220 | CALL_ID ertl_params ? f (|args|) it ::: |
---|
221 | fetch_result ? ret_regs |
---|
222 | | extension_call c ⇒ |
---|
223 | match c with |
---|
224 | [ rtl_call_ptr f1 f2 args dest ⇒ |
---|
225 | ? |
---|
226 | ] |
---|
227 | ] |
---|
228 | | COND r ltrue ⇒ |
---|
229 | COND ertl_params ? r ltrue |
---|
230 | ]. cases daemon (* pointer call to be ported yet *) qed. |
---|
231 | |
---|
232 | definition translate_fin_step : |
---|
233 | ∀globals.label → joint_fin_step rtlntc_params → |
---|
234 | bind_seq_block ertl_params globals (joint_fin_step ertl_params) ≝ |
---|
235 | λglobals.λ_.λs. |
---|
236 | match s with |
---|
237 | [ GOTO lbl' ⇒ GOTO … lbl' |
---|
238 | | RETURN ⇒ RETURN ? |
---|
239 | | tailcall abs ⇒ match abs in void with [ ] |
---|
240 | ]. |
---|
241 | |
---|
242 | (* hack with empty graphs used here *) |
---|
243 | definition translate_funct : |
---|
244 | ∀globals.joint_internal_function globals rtlntc_params → |
---|
245 | joint_internal_function globals ertl_params ≝ |
---|
246 | λglobals,def. |
---|
247 | let nb_params ≝ |joint_if_params ?? def| in |
---|
248 | let added_stacksize ≝ max 0 (minus nb_params (|RegisterParams|)) in |
---|
249 | let new_locals ≝ nub_by ? (eq_identifier ?) ((joint_if_locals … def) @ (joint_if_params … def)) in |
---|
250 | let entry' ≝ pi1 … (joint_if_entry … def) in |
---|
251 | let exit' ≝ pi1 … (joint_if_exit … def) in |
---|
252 | let graph' ≝ add ? ? (empty_map ? (joint_statement ??)) entry' (GOTO … exit') in |
---|
253 | let graph' ≝ add ? ? graph' exit' (RETURN …) in |
---|
254 | let def' ≝ |
---|
255 | mk_joint_internal_function globals ertl_params |
---|
256 | (joint_if_luniverse … def) (joint_if_runiverse … def) (joint_if_result … def) (*CSC: different from OCaml code where joint_if_result is unit*) |
---|
257 | nb_params new_locals ((joint_if_stacksize … def) + added_stacksize) |
---|
258 | graph' entry' exit' in |
---|
259 | let def'' ≝ b_graph_translate … |
---|
260 | (rtl_ertl_fresh_reg …) |
---|
261 | def' |
---|
262 | (translate_step globals) |
---|
263 | (translate_fin_step globals) |
---|
264 | def in |
---|
265 | add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'. |
---|
266 | >graph_code_has_point @map_mem_prop |
---|
267 | [@graph_add_lookup] @graph_add |
---|
268 | qed. |
---|
269 | |
---|
270 | (* removing this because of how insert_prologue is now defined |
---|
271 | definition generate ≝ |
---|
272 | λglobals. |
---|
273 | λstmt. |
---|
274 | λdef: joint_internal_function globals ertl_params. |
---|
275 | let 〈entry, def〉 ≝ fresh_label … def in |
---|
276 | let graph ≝ add … (joint_if_code … def) entry stmt in |
---|
277 | set_joint_if_graph … (ertl_params globals) graph def ??. |
---|
278 | [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *) |
---|
279 | | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF |
---|
280 | *) cases daemon (*CSC: XXX *) |
---|
281 | ] |
---|
282 | qed. |
---|
283 | |
---|
284 | let rec find_and_remove_first_cost_label_internal (globals: list ident) |
---|
285 | (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat) |
---|
286 | on num_nodes ≝ |
---|
287 | match num_nodes with |
---|
288 | [ O ⇒ 〈None ?, def〉 |
---|
289 | | S num_nodes' ⇒ |
---|
290 | match lookup … (joint_if_code … def) lbl with |
---|
291 | [ None ⇒ 〈None ?, def〉 |
---|
292 | | Some stmt ⇒ |
---|
293 | match stmt with |
---|
294 | [ sequential inst lbl ⇒ |
---|
295 | match inst with |
---|
296 | [ COST_LABEL cost_lbl ⇒ |
---|
297 | 〈Some … cost_lbl, add_graph ertl_params1 globals lbl (GOTO … lbl) def〉 |
---|
298 | | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ] |
---|
299 | | RETURN ⇒ 〈None …, def〉 |
---|
300 | | GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' |
---|
301 | ]]]. |
---|
302 | |
---|
303 | definition find_and_remove_first_cost_label ≝ |
---|
304 | λglobals,def. |
---|
305 | find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)). |
---|
306 | |
---|
307 | definition move_first_cost_label_up_internal ≝ |
---|
308 | λglobals,def. |
---|
309 | let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in |
---|
310 | match cost_label with |
---|
311 | [ None ⇒ def |
---|
312 | | Some cost_label ⇒ generate … (sequential ertl_params_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def |
---|
313 | ]. |
---|
314 | |
---|
315 | definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)). |
---|
316 | *) |
---|
317 | |
---|
318 | definition rtl_to_ertl : rtl_program → ertl_program ≝ |
---|
319 | λp. |
---|
320 | let p ≝ tailcall_simplify p in (* tailcall simplification here *) |
---|
321 | transform_program ??? p (λvarnames. transf_fundef ?? (translate_funct varnames)). |
---|