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