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