[1079] | 1 | include "RTL/RTLTailcall.ma". |
---|
[1075] | 2 | include "utilities/RegisterSet.ma". |
---|
[1076] | 3 | include "common/Identifiers.ma". |
---|
[759] | 4 | include "ERTL/ERTL.ma". |
---|
[1280] | 5 | include "joint/TranslateUtils.ma". |
---|
[1252] | 6 | |
---|
[763] | 7 | definition save_hdws ≝ |
---|
[1254] | 8 | λglobals,l. |
---|
| 9 | let save_hdws_internal ≝ |
---|
| 10 | λdestr_srcr.λstart_lbl. |
---|
[777] | 11 | let 〈destr, srcr〉 ≝ destr_srcr in |
---|
[1283] | 12 | adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈pseudo destr,hardware srcr〉) ] start_lbl |
---|
[1254] | 13 | in |
---|
| 14 | map ? ? save_hdws_internal l. |
---|
| 15 | |
---|
[777] | 16 | definition restore_hdws ≝ |
---|
[1254] | 17 | λglobals,l. |
---|
| 18 | let restore_hdws_internal ≝ |
---|
| 19 | λsrcr_destr: register × Register. |
---|
| 20 | λstart_lbl: label. |
---|
| 21 | let 〈srcr, destr〉 ≝ srcr_destr in |
---|
[1283] | 22 | adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈hardware destr, pseudo srcr〉) ] start_lbl |
---|
[1254] | 23 | in |
---|
| 24 | map ? ? restore_hdws_internal l. |
---|
[777] | 25 | |
---|
| 26 | definition get_params_hdw ≝ |
---|
[1254] | 27 | λglobals. |
---|
[777] | 28 | λparams: list register. |
---|
[1071] | 29 | match params with |
---|
[1283] | 30 | [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ GOTO … ] start_lbl] |
---|
[777] | 31 | | _ ⇒ |
---|
[1149] | 32 | let l ≝ zip_pottier ? ? params RegisterParams in |
---|
[1254] | 33 | save_hdws globals l ]. |
---|
[777] | 34 | |
---|
| 35 | definition get_param_stack ≝ |
---|
[1254] | 36 | λglobals. |
---|
[777] | 37 | λoff: nat. |
---|
| 38 | λdestr. |
---|
| 39 | λstart_lbl, dest_lbl: label. |
---|
| 40 | λdef. |
---|
[1254] | 41 | let 〈def, addr1〉 ≝ fresh_reg … def in |
---|
| 42 | let 〈def, addr2〉 ≝ fresh_reg … def in |
---|
| 43 | let 〈def, tmpr〉 ≝ fresh_reg … def in |
---|
[1071] | 44 | let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in |
---|
[1280] | 45 | adds_graph ertl_params1 globals [ |
---|
[1283] | 46 | sequential ertl_params_ … (extension … (ertl_st_ext_frame_size addr1)); |
---|
| 47 | sequential ertl_params_ … (INT … tmpr int_offset); |
---|
| 48 | sequential ertl_params_ … (OP2 … Sub addr1 addr1 tmpr); |
---|
| 49 | sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉); |
---|
| 50 | sequential ertl_params_ … (OP2 … Add addr1 addr1 tmpr); |
---|
| 51 | sequential ertl_params_ … (INT … addr2 (bitvector_of_nat 8 0)); |
---|
| 52 | sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉); |
---|
| 53 | sequential ertl_params_ … (OP2 … Addc addr2 addr2 tmpr); |
---|
[1284] | 54 | sequential ertl_params_ … (LOAD … destr addr1 addr2) |
---|
[777] | 55 | ] start_lbl dest_lbl def. |
---|
| 56 | |
---|
| 57 | definition get_params_stack ≝ |
---|
[1257] | 58 | λglobals,params. |
---|
[1071] | 59 | match params with |
---|
[1283] | 60 | [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl ] |
---|
[1257] | 61 | | _ ⇒ mapi ? ? (get_param_stack globals) params ]. |
---|
[777] | 62 | |
---|
| 63 | definition get_params ≝ |
---|
[1257] | 64 | λglobals,params. |
---|
| 65 | let n ≝ min (length … params) (length … RegisterParams) in |
---|
| 66 | let 〈hdw_params, stack_params〉 ≝ list_split … n params in |
---|
| 67 | let hdw_params ≝ get_params_hdw globals hdw_params in |
---|
| 68 | hdw_params @ (get_params_stack … stack_params). |
---|
[1284] | 69 | |
---|
[777] | 70 | definition add_prologue ≝ |
---|
[1257] | 71 | λglobals. |
---|
[1071] | 72 | λparams: list register. |
---|
[777] | 73 | λsral. |
---|
| 74 | λsrah. |
---|
| 75 | λsregs. |
---|
| 76 | λdef. |
---|
[1258] | 77 | let start_lbl ≝ joint_if_entry … (ertl_params globals) def in |
---|
[1284] | 78 | let 〈tmp_lbl, def〉 ≝ fresh_label … def in |
---|
[1280] | 79 | match lookup … (joint_if_code … def) start_lbl |
---|
[1257] | 80 | return λx. x ≠ None ? → ertl_internal_function globals with |
---|
| 81 | [ None ⇒ λnone_absrd. ⊥ |
---|
[1075] | 82 | | Some last_stmt ⇒ λsome_prf. |
---|
[777] | 83 | let def ≝ |
---|
[1257] | 84 | add_translates … |
---|
[1280] | 85 | ((adds_graph ertl_params1 … [ |
---|
[1283] | 86 | sequential ertl_params_ … (extension ertl_params__ globals ertl_st_ext_new_frame) |
---|
[1071] | 87 | ]) :: |
---|
[1283] | 88 | (adds_graph ertl_params1 … [ |
---|
| 89 | sequential ertl_params_ … (POP … sral); |
---|
| 90 | sequential ertl_params_ … (POP … srah) |
---|
[1071] | 91 | ]) :: |
---|
[1257] | 92 | (save_hdws … sregs) @ |
---|
| 93 | (get_params … params)) |
---|
[1071] | 94 | start_lbl tmp_lbl def |
---|
| 95 | in |
---|
[1257] | 96 | add_graph … tmp_lbl last_stmt def |
---|
[1075] | 97 | ] ?. |
---|
[1284] | 98 | [ cases start_lbl #x #H cases daemon (* @H *) (*CSC: XXXX, no Russell *) |
---|
[1257] | 99 | | cases (none_absrd) /2/ ] |
---|
[1071] | 100 | qed. |
---|
| 101 | |
---|
| 102 | definition save_return ≝ |
---|
[1258] | 103 | λglobals. |
---|
[1071] | 104 | λret_regs. |
---|
| 105 | λstart_lbl: label. |
---|
| 106 | λdest_lbl: label. |
---|
[1258] | 107 | λdef: ertl_internal_function globals. |
---|
| 108 | let 〈def, tmpr〉 ≝ fresh_reg … def in |
---|
[1075] | 109 | match reduce_strong ? ? RegisterSTS ret_regs with |
---|
[1071] | 110 | [ dp crl crl_proof ⇒ |
---|
| 111 | let commonl ≝ \fst (\fst crl) in |
---|
| 112 | let commonr ≝ \fst (\snd crl) in |
---|
| 113 | let restl ≝ \snd (\fst crl) in |
---|
| 114 | let restr ≝ \snd (\snd crl) in |
---|
[1283] | 115 | let init_tmpr ≝ sequential ertl_params_ … (INT … tmpr (zero …)) in |
---|
| 116 | let f_save ≝ λst. λr. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo r〉) in |
---|
[1280] | 117 | let saves ≝ map2 … f_save commonl commonr crl_proof in |
---|
[1283] | 118 | let f_default ≝ λst. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo tmpr〉) in |
---|
[1280] | 119 | let defaults ≝ map … f_default restl in |
---|
| 120 | adds_graph ertl_params1 … (init_tmpr :: saves @ defaults) start_lbl dest_lbl def |
---|
[1071] | 121 | ]. |
---|
| 122 | |
---|
[1075] | 123 | definition assign_result ≝ |
---|
[1258] | 124 | λglobals.λstart_lbl: label. |
---|
[1075] | 125 | match reduce_strong ? ? RegisterRets RegisterSTS with |
---|
| 126 | [ dp crl crl_proof ⇒ |
---|
| 127 | let commonl ≝ \fst (\fst crl) in |
---|
| 128 | let commonr ≝ \fst (\snd crl) in |
---|
[1283] | 129 | let f ≝ λret. λst. sequential ertl_params_ globals (MOVE … 〈hardware ret, hardware st〉) in |
---|
[1075] | 130 | let insts ≝ map2 ? ? ? f commonl commonr crl_proof in |
---|
[1280] | 131 | adds_graph ertl_params1 … insts start_lbl |
---|
[1075] | 132 | ]. |
---|
| 133 | |
---|
| 134 | definition add_epilogue ≝ |
---|
[1258] | 135 | λglobals. |
---|
[1075] | 136 | λret_regs. |
---|
| 137 | λsral. |
---|
| 138 | λsrah. |
---|
| 139 | λsregs. |
---|
| 140 | λdef. |
---|
[1258] | 141 | let start_lbl ≝ joint_if_exit … (ertl_params globals) def in |
---|
[1284] | 142 | let 〈tmp_lbl, def〉 ≝ fresh_label … def in |
---|
[1280] | 143 | match lookup … (joint_if_code … def) start_lbl |
---|
[1258] | 144 | return λx. x ≠ None ? → ertl_internal_function globals with |
---|
| 145 | [ None ⇒ λnone_absrd. ⊥ |
---|
[1075] | 146 | | Some last_stmt ⇒ λsome_prf. |
---|
| 147 | let def ≝ |
---|
[1280] | 148 | add_translates ertl_params1 … ( |
---|
[1258] | 149 | [save_return globals ret_regs] @ |
---|
| 150 | restore_hdws … sregs @ |
---|
[1283] | 151 | [adds_graph ertl_params1 … [ |
---|
| 152 | sequential ertl_params_ … (PUSH … srah); |
---|
| 153 | sequential ertl_params_ … (PUSH … sral) |
---|
[1075] | 154 | ]] @ |
---|
[1280] | 155 | [adds_graph ertl_params1 … [ |
---|
[1283] | 156 | sequential ertl_params_ … (extension … ertl_st_ext_del_frame) |
---|
[1075] | 157 | ]] @ |
---|
[1258] | 158 | [assign_result globals] |
---|
[1075] | 159 | ) start_lbl tmp_lbl def |
---|
| 160 | in |
---|
[1258] | 161 | let def' ≝ add_graph … tmp_lbl last_stmt def in |
---|
| 162 | set_joint_if_exit … tmp_lbl def' ? |
---|
[1075] | 163 | ] ?. |
---|
[1284] | 164 | [ cases start_lbl #x #H cases daemon (* @H *) (* CSC: XXXX *) |
---|
[1258] | 165 | | cases (none_absrd) /2/ |
---|
| 166 | | cases daemon (* CSC: XXXXX *) |
---|
| 167 | ] |
---|
[1075] | 168 | qed. |
---|
[777] | 169 | |
---|
[1258] | 170 | |
---|
[777] | 171 | definition allocate_regs ≝ |
---|
[1258] | 172 | λglobals. |
---|
[1075] | 173 | λrs. |
---|
[777] | 174 | λsaved: rs_set rs. |
---|
| 175 | λdef. |
---|
[1258] | 176 | let allocate_regs_internal ≝ |
---|
| 177 | λr: Register. |
---|
| 178 | λdef_sregs. |
---|
| 179 | let 〈def, sregs〉 ≝ def_sregs in |
---|
[1280] | 180 | let 〈def, r'〉 ≝ fresh_reg ertl_params0 globals def in |
---|
[1258] | 181 | 〈def, 〈r', r〉 :: sregs〉 |
---|
| 182 | in |
---|
[777] | 183 | rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉. |
---|
[1075] | 184 | |
---|
| 185 | definition add_pro_and_epilogue ≝ |
---|
[1258] | 186 | λglobals. |
---|
[1075] | 187 | λparams. |
---|
| 188 | λret_regs. |
---|
| 189 | λdef. |
---|
[1280] | 190 | match fresh_regs_strong … globals def 2 with |
---|
[1075] | 191 | [ dp def_sra def_sra_proof ⇒ |
---|
| 192 | let def ≝ \fst def_sra in |
---|
| 193 | let sra ≝ \snd def_sra in |
---|
| 194 | let sral ≝ nth_safe ? 0 sra ? in |
---|
| 195 | let srah ≝ nth_safe ? 1 sra ? in |
---|
[1258] | 196 | let 〈def, sregs〉 ≝ allocate_regs … register_list_set RegisterCalleeSaved def in |
---|
| 197 | let def ≝ add_prologue … params sral srah sregs def in |
---|
| 198 | let def ≝ add_epilogue … ret_regs sral srah sregs def in |
---|
[1075] | 199 | def |
---|
| 200 | ]. |
---|
[1258] | 201 | >def_sra_proof // |
---|
[1075] | 202 | qed. |
---|
| 203 | |
---|
| 204 | definition set_params_hdw ≝ |
---|
[1258] | 205 | λglobals,params. |
---|
[1075] | 206 | match params with |
---|
[1283] | 207 | [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl] |
---|
[1075] | 208 | | _ ⇒ |
---|
[1149] | 209 | let l ≝ zip_pottier ? ? params RegisterParams in |
---|
[1258] | 210 | restore_hdws globals l |
---|
[1075] | 211 | ]. |
---|
| 212 | |
---|
| 213 | definition set_param_stack ≝ |
---|
[1259] | 214 | λglobals. |
---|
[1075] | 215 | λoff. |
---|
| 216 | λsrcr. |
---|
| 217 | λstart_lbl: label. |
---|
| 218 | λdest_lbl: label. |
---|
[1259] | 219 | λdef: ertl_internal_function globals. |
---|
| 220 | let 〈def, addr1〉 ≝ fresh_reg … def in |
---|
| 221 | let 〈def, addr2〉 ≝ fresh_reg … def in |
---|
| 222 | let 〈def, tmpr〉 ≝ fresh_reg … def in |
---|
[1075] | 223 | let 〈ignore, int_off〉 ≝ half_add ? off int_size in |
---|
[1280] | 224 | adds_graph ertl_params1 … [ |
---|
[1283] | 225 | sequential ertl_params_ … (INT … addr1 int_off); |
---|
| 226 | sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉); |
---|
| 227 | sequential ertl_params_ … (CLEAR_CARRY …); |
---|
| 228 | sequential ertl_params_ … (OP2 … Sub addr1 tmpr addr1); |
---|
| 229 | sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉); |
---|
| 230 | sequential ertl_params_ … (INT … addr2 (zero ?)); |
---|
| 231 | sequential ertl_params_ … (OP2 … Sub addr2 tmpr addr2); |
---|
| 232 | sequential ertl_params_ … (STORE … addr1 addr2 srcr) |
---|
[1075] | 233 | ] start_lbl dest_lbl def. |
---|
| 234 | |
---|
| 235 | definition set_params_stack ≝ |
---|
[1259] | 236 | λglobals,params. |
---|
[1075] | 237 | match params with |
---|
[1283] | 238 | [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [GOTO …] start_lbl] |
---|
[1075] | 239 | | _ ⇒ |
---|
[1259] | 240 | let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in |
---|
| 241 | mapi ? ? f params]. |
---|
[1075] | 242 | |
---|
| 243 | definition set_params ≝ |
---|
[1259] | 244 | λglobals,params. |
---|
[1149] | 245 | let n ≝ min (|params|) (|RegisterParams|) in |
---|
[1075] | 246 | let hdw_stack_params ≝ split ? params n ? in |
---|
| 247 | let hdw_params ≝ \fst hdw_stack_params in |
---|
| 248 | let stack_params ≝ \snd hdw_stack_params in |
---|
[1259] | 249 | set_params_hdw globals hdw_params @ set_params_stack globals stack_params. |
---|
| 250 | /2/ |
---|
[1075] | 251 | qed. |
---|
| 252 | |
---|
| 253 | definition fetch_result ≝ |
---|
[1259] | 254 | λglobals. |
---|
[1075] | 255 | λret_regs. |
---|
| 256 | λstart_lbl: label. |
---|
| 257 | match reduce_strong ? ? RegisterSTS RegisterRets with |
---|
| 258 | [ dp crl first_crl_proof ⇒ |
---|
| 259 | let commonl ≝ \fst (\fst crl) in |
---|
| 260 | let commonr ≝ \fst (\snd crl) in |
---|
[1283] | 261 | let f_save ≝ λst. λret. sequential ertl_params_ globals (MOVE … 〈hardware st, hardware ret〉) in |
---|
[1075] | 262 | let saves ≝ map2 ? ? ? f_save commonl commonr ? in |
---|
| 263 | match reduce_strong ? ? ret_regs RegisterSTS with |
---|
| 264 | [ dp crl second_crl_proof ⇒ |
---|
| 265 | let commonl ≝ \fst (\fst crl) in |
---|
| 266 | let commonr ≝ \fst (\snd crl) in |
---|
[1283] | 267 | let f_restore ≝ λr. λst. sequential ertl_params_ … (MOVE … 〈pseudo r, hardware st〉) in |
---|
[1075] | 268 | let restores ≝ map2 ? ? ? f_restore commonl commonr ? in |
---|
[1280] | 269 | adds_graph ertl_params1 … (saves @ restores) start_lbl]]. |
---|
[1259] | 270 | [@second_crl_proof | @first_crl_proof] |
---|
[1075] | 271 | qed. |
---|
| 272 | |
---|
| 273 | definition translate_call_id ≝ |
---|
[1259] | 274 | λglobals,f. |
---|
[1075] | 275 | λargs. |
---|
| 276 | λret_regs. |
---|
| 277 | λstart_lbl. |
---|
| 278 | λdest_lbl. |
---|
| 279 | λdef. |
---|
| 280 | let nb_args ≝ |args| in |
---|
[1280] | 281 | add_translates ertl_params1 globals ( |
---|
[1259] | 282 | set_params … args @ [ |
---|
[1283] | 283 | adds_graph ertl_params1 … [ sequential ertl_params_ … (CALL_ID … f nb_args it) ]; |
---|
[1259] | 284 | fetch_result … ret_regs |
---|
[1075] | 285 | ] |
---|
| 286 | ) start_lbl dest_lbl def. |
---|
| 287 | |
---|
[1275] | 288 | definition translate_stmt : |
---|
[1278] | 289 | ∀globals: list ident. label → rtlntc_statement globals → ertl_internal_function globals → ertl_internal_function globals |
---|
[1262] | 290 | ≝ |
---|
[1259] | 291 | λglobals. |
---|
[1075] | 292 | λlbl. |
---|
| 293 | λstmt. |
---|
| 294 | λdef. |
---|
| 295 | match stmt with |
---|
[1282] | 296 | [ GOTO lbl' ⇒ add_graph … lbl (GOTO … lbl') def |
---|
| 297 | | RETURN ⇒ add_graph … lbl (RETURN …) def |
---|
| 298 | | sequential seq lbl' ⇒ |
---|
[1275] | 299 | match seq with |
---|
[1282] | 300 | [ PUSH _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *) |
---|
| 301 | | POP _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *) |
---|
| 302 | | CALL_ID f args ret_regs ⇒ |
---|
[1275] | 303 | translate_call_id … f args ret_regs lbl lbl' def |
---|
[1282] | 304 | | MOVE rs ⇒ |
---|
[1275] | 305 | let 〈r1,r2〉 ≝ rs in |
---|
| 306 | let rs ≝ 〈pseudo r1, pseudo r2〉 in |
---|
[1282] | 307 | add_graph ertl_params1 ? lbl (sequential … (MOVE … rs) lbl') def |
---|
| 308 | | extension ext ⇒ |
---|
[1275] | 309 | match ext with |
---|
[1278] | 310 | [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *) |
---|
| 311 | | rtlntc_st_ext_address r1 r2 ⇒ |
---|
[1280] | 312 | adds_graph ertl_params1 … [ |
---|
[1283] | 313 | sequential ertl_params_ … (MOVE … 〈pseudo r1, hardware RegisterSPL〉); |
---|
| 314 | sequential ertl_params_ … (MOVE … 〈pseudo r2, hardware RegisterSPH〉) |
---|
[1278] | 315 | ] lbl lbl' def] |
---|
[1275] | 316 | (*CSC: everything is just copied to re-type it from now on; |
---|
| 317 | the problem is call_id that takes different parameters, but that is pattern-matched |
---|
| 318 | above. It could be made nicer at the cost of making all the rest of the code uglier *) |
---|
[1282] | 319 | | COST_LABEL cost_lbl ⇒ add_graph ertl_params1 … lbl (sequential … (COST_LABEL … cost_lbl) lbl') def |
---|
| 320 | | ADDRESS x prf r1 r2 ⇒ add_graph ertl_params1 … lbl (sequential … (ADDRESS … x prf r1 r2) lbl') def |
---|
| 321 | | INT r i ⇒ add_graph ertl_params1 … lbl (sequential … (INT … r i) lbl') def |
---|
| 322 | | OPACCS op destr1 destr2 srcr1 srcr2 ⇒ |
---|
| 323 | add_graph ertl_params1 … lbl (sequential … (OPACCS … op destr1 destr2 srcr1 srcr2) lbl') def |
---|
| 324 | | OP1 op1 destr srcr ⇒ |
---|
| 325 | add_graph ertl_params1 … lbl (sequential … (OP1 … op1 destr srcr) lbl') def |
---|
| 326 | | OP2 op2 destr srcr1 srcr2 ⇒ |
---|
| 327 | add_graph ertl_params1 … lbl (sequential … (OP2 … op2 destr srcr1 srcr2) lbl') def |
---|
| 328 | | CLEAR_CARRY ⇒ |
---|
| 329 | add_graph ertl_params1 … lbl (sequential … (CLEAR_CARRY …) lbl') def |
---|
| 330 | | SET_CARRY ⇒ |
---|
| 331 | add_graph ertl_params1 … lbl (sequential … (SET_CARRY …) lbl') def |
---|
| 332 | | LOAD destr addr1 addr2 ⇒ |
---|
| 333 | add_graph ertl_params1 … lbl (sequential … (LOAD … destr addr1 addr2) lbl') def |
---|
| 334 | | STORE addr1 addr2 srcr ⇒ |
---|
| 335 | add_graph ertl_params1 … lbl (sequential … (STORE … addr1 addr2 srcr) lbl') def |
---|
| 336 | | COND srcr lbl_true ⇒ |
---|
| 337 | add_graph ertl_params1 … lbl (sequential … (COND … srcr lbl_true) lbl') def |
---|
| 338 | | COMMENT msg ⇒ |
---|
| 339 | add_graph ertl_params1 … lbl (sequential … (COMMENT … msg) lbl') def |
---|
[1275] | 340 | ]]. |
---|
[1280] | 341 | @not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *) |
---|
[1275] | 342 | qed. |
---|
[1075] | 343 | |
---|
[1079] | 344 | (* hack with empty graphs used here *) |
---|
[1076] | 345 | definition translate_funct_internal ≝ |
---|
[1278] | 346 | λglobals.λdef:rtlntc_internal_function globals. |
---|
[1270] | 347 | let nb_params ≝ |joint_if_params ?? def| in |
---|
[1149] | 348 | let added_stacksize ≝ max 0 (nb_params - |RegisterParams|) in |
---|
[1270] | 349 | let new_locals ≝ nub_by ? (eq_identifier ?) ((joint_if_locals … def) @ (joint_if_params … def)) in |
---|
| 350 | let entry' ≝ joint_if_entry … def in |
---|
| 351 | let exit' ≝ joint_if_exit … def in |
---|
[1282] | 352 | let graph' ≝ add ? ? (empty_map ? ?) entry' (GOTO … entry') in |
---|
| 353 | let graph' ≝ add ? ? graph' exit' (GOTO … exit') in |
---|
[1076] | 354 | let def' ≝ |
---|
[1262] | 355 | mk_joint_internal_function globals (ertl_params globals) |
---|
[1270] | 356 | (joint_if_luniverse … def) (joint_if_runiverse … def) it |
---|
| 357 | nb_params new_locals ((joint_if_stacksize … def) + added_stacksize) |
---|
[1079] | 358 | graph' ? ? in |
---|
[1270] | 359 | let def' ≝ foldi ? ? ? (translate_stmt globals) (joint_if_code … def) def' in |
---|
[1275] | 360 | add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'. |
---|
[1262] | 361 | whd in match ertl_params (* CSC: Matita's bug here; not enough/too much reduction |
---|
| 362 | makes the next application fail. Why? *) |
---|
| 363 | % |
---|
| 364 | [ @entry' | @graph_add_lookup @graph_add |
---|
| 365 | | @exit' | @graph_add ] |
---|
[1079] | 366 | qed. |
---|
[1077] | 367 | |
---|
| 368 | definition generate ≝ |
---|
[1262] | 369 | λglobals. |
---|
[1077] | 370 | λstmt. |
---|
[1280] | 371 | λdef: joint_internal_function … (ertl_params globals). |
---|
[1284] | 372 | let 〈entry, def〉 ≝ fresh_label … def in |
---|
| 373 | let graph ≝ add … (joint_if_code … def) entry stmt in |
---|
| 374 | set_joint_if_graph … (ertl_params globals) graph def ??. |
---|
| 375 | [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *) |
---|
| 376 | | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF |
---|
| 377 | *) cases daemon (*CSC: XXX *) |
---|
| 378 | ] |
---|
[1079] | 379 | qed. |
---|
[1262] | 380 | |
---|
| 381 | let rec find_and_remove_first_cost_label_internal (globals: list ident) |
---|
| 382 | (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat) |
---|
[1079] | 383 | on num_nodes ≝ |
---|
| 384 | match num_nodes with |
---|
| 385 | [ O ⇒ 〈None ?, def〉 |
---|
| 386 | | S num_nodes' ⇒ |
---|
[1262] | 387 | match lookup … (joint_if_code … def) lbl with |
---|
[1079] | 388 | [ None ⇒ 〈None ?, def〉 |
---|
[1262] | 389 | | Some stmt ⇒ |
---|
[1079] | 390 | match stmt with |
---|
[1282] | 391 | [ sequential inst lbl ⇒ |
---|
[1262] | 392 | match inst with |
---|
[1282] | 393 | [ COST_LABEL cost_lbl ⇒ |
---|
| 394 | 〈Some … cost_lbl, add_graph ertl_params1 globals lbl (GOTO … lbl) def〉 |
---|
[1262] | 395 | | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ] |
---|
[1282] | 396 | | RETURN ⇒ 〈None …, def〉 |
---|
| 397 | | GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' |
---|
[1262] | 398 | ]]]. |
---|
[1079] | 399 | |
---|
| 400 | definition find_and_remove_first_cost_label ≝ |
---|
[1262] | 401 | λglobals,def. |
---|
| 402 | find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)). |
---|
[1077] | 403 | |
---|
[1079] | 404 | definition move_first_cost_label_up_internal ≝ |
---|
[1262] | 405 | λglobals,def. |
---|
| 406 | let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in |
---|
[1079] | 407 | match cost_label with |
---|
| 408 | [ None ⇒ def |
---|
[1282] | 409 | | Some cost_label ⇒ generate … (sequential ertl_params_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def |
---|
[1079] | 410 | ]. |
---|
[1077] | 411 | |
---|
[1262] | 412 | definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)). |
---|
| 413 | |
---|
| 414 | definition translate : rtl_program → ertl_program ≝ |
---|
| 415 | λp. |
---|
| 416 | let p ≝ tailcall_simplify p in (* tailcall simplification here *) |
---|
[1280] | 417 | transform_program ??? p (transf_fundef ?? (translate_funct …)). |
---|