Changeset 1280 for src/RTL/RTLtoERTL.ma
 Timestamp:
 Sep 28, 2011, 2:43:37 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLtoERTL.ma
r1278 r1280 3 3 include "common/Identifiers.ma". 4 4 include "ERTL/ERTL.ma". 5 6 definition fresh_label ≝ 7 λglobals.λdef: joint_internal_function … (ertl_params globals). 8 fresh LabelTag (joint_if_luniverse … def). 9 10 definition change_label ≝ 11 λglobals.λe: joint_statement ertl_params_ globals.λl. 12 match e with 13 [ joint_st_goto _ ⇒ joint_st_goto … l 14  joint_st_return ⇒ joint_st_return ?? 15  joint_st_sequential instr _ ⇒ joint_st_sequential … instr l]. 16 17 (*CSC: bad programming habit: the code below puts everywhere a fake 18 label and then adds_graph fixes them *) 19 (*CSC: the code is artificially fixed to work on ertl_statements, but 20 it works on every graph_params *) 21 (*CSC: this is just an instance of add_translates below! *) 22 let rec adds_graph 23 (globals: list ident) 24 (stmt_list: list (ertl_statement globals)) (start_lbl: label) 25 (dest_lbl: label) (def: ertl_internal_function globals) 26 on stmt_list ≝ 27 match stmt_list with 28 [ nil ⇒ add_graph … start_lbl (joint_st_goto … dest_lbl) def 29  cons stmt stmt_list ⇒ 30 match stmt_list with 31 [ nil ⇒ add_graph … start_lbl (change_label … stmt dest_lbl) def 32  _ ⇒ 33 let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in 34 let stmt ≝ change_label … stmt tmp_lbl in 35 let def ≝ add_graph … start_lbl stmt def in 36 adds_graph globals stmt_list tmp_lbl dest_lbl def]]. 37 38 (*CSC: bad programming habit: the code below puts everywhere a fake 39 label and then adds_graph fixes them *) 40 (*CSC: the code is artificially fixed to work on ertl_statements, but 41 it works on every graph_params *) 42 let rec add_translates 43 (globals: list ident) (translate_list: list ?) (start_lbl: label) (dest_lbl: label) 44 (def: ertl_internal_function globals) 45 on translate_list ≝ 46 match translate_list with 47 [ nil ⇒ add_graph … start_lbl (joint_st_goto … dest_lbl) def 48  cons trans translate_list ⇒ 49 match translate_list with 50 [ nil ⇒ trans start_lbl dest_lbl def 51  _ ⇒ 52 let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in 53 let def ≝ trans start_lbl tmp_lbl def in 54 add_translates globals translate_list tmp_lbl dest_lbl def]]. 55 56 definition fresh_reg: 57 ∀globals. ertl_internal_function globals → (ertl_internal_function globals) × register ≝ 58 λglobals,def. 59 let 〈r,runiverse〉 ≝ fresh … (joint_if_runiverse … def) in 60 〈set_locals … (set_runiverse … def runiverse) (r::joint_if_locals … def), r〉. 61 62 let rec fresh_regs (globals: list ident) (def: ertl_internal_function globals) (n: nat) on n ≝ 63 match n with 64 [ O ⇒ 〈def, [ ]〉 65  S n' ⇒ 66 let 〈def', regs'〉 ≝ fresh_regs globals def n' in 67 let 〈def', reg〉 ≝ fresh_reg … def' in 68 〈def', reg :: regs'〉 69 ]. 70 71 lemma fresh_regs_length: 72 ∀globals.∀def: ertl_internal_function globals. ∀n: nat. 73 (\snd (fresh_regs … def n)) = n. 74 #globals #def #n elim n 75 [ % 76  #m whd in ⊢ (? → ??(??%)?) whd in ⊢ (? → ??(??match % with [ _ ⇒ ?])?) 77 cases (fresh_regs globals def m) normalize nodelta 78 #def' #regs #EQ change in EQ with (regs = m) <EQ 79 change with 80 (let 〈a,b〉 ≝ let 〈x,y〉 ≝ let 〈r,runiverse〉 ≝ ? in ? in ? in ? = ?) 81 cases (fresh … (joint_if_runiverse … def')) normalize // ] 82 qed. 83 84 definition fresh_regs_strong: 85 ∀globals. ertl_internal_function globals → 86 ∀n: nat. Σregs: (ertl_internal_function globals) × (list register). \snd regs = n ≝ 87 λdef,n.fresh_regs def n. // 88 qed. 5 include "joint/TranslateUtils.ma". 89 6 90 7 definition save_hdws ≝ … … 93 10 λdestr_srcr.λstart_lbl. 94 11 let 〈destr, srcr〉 ≝ destr_srcr in 95 adds_graph globals [ joint_st_sequential … (joint_instr_move … 〈pseudo destr,hardware srcr〉) start_lbl ] start_lbl12 adds_graph ertl_params1 globals [ joint_st_sequential … (joint_instr_move … 〈pseudo destr,hardware srcr〉) start_lbl ] start_lbl 96 13 in 97 14 map ? ? save_hdws_internal l. … … 103 20 λstart_lbl: label. 104 21 let 〈srcr, destr〉 ≝ srcr_destr in 105 adds_graph globals [ joint_st_sequential … (joint_instr_move … 〈hardware destr, pseudo srcr〉) start_lbl ] start_lbl22 adds_graph ertl_params1 globals [ joint_st_sequential … (joint_instr_move … 〈hardware destr, pseudo srcr〉) start_lbl ] start_lbl 106 23 in 107 24 map ? ? restore_hdws_internal l. … … 111 28 λparams: list register. 112 29 match params with 113 [ nil ⇒ [λstart_lbl: label. adds_graph globals [ joint_st_goto … start_lbl ] start_lbl]30 [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ joint_st_goto … start_lbl ] start_lbl] 114 31  _ ⇒ 115 32 let l ≝ zip_pottier ? ? params RegisterParams in … … 126 43 let 〈def, tmpr〉 ≝ fresh_reg … def in 127 44 let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in 128 adds_graph globals [45 adds_graph ertl_params1 globals [ 129 46 joint_st_sequential … (joint_instr_extension … (ertl_st_ext_frame_size addr1)) start_lbl; 130 47 joint_st_sequential … (joint_instr_int … tmpr int_offset) start_lbl; … … 160 77 let start_lbl ≝ joint_if_entry … (ertl_params globals) def in 161 78 let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in 162 match lookup … (joint_if_code … (ertl_params globals)def) start_lbl79 match lookup … (joint_if_code … def) start_lbl 163 80 return λx. x ≠ None ? → ertl_internal_function globals with 164 81 [ None ⇒ λnone_absrd. ⊥ … … 166 83 let def ≝ 167 84 add_translates … 168 ((adds_graph … [169 joint_st_sequential … (joint_instr_extension ertl_params_ globals ertl_st_ext_new_frame) start_lbl85 ((adds_graph ertl_params1 … [ 86 joint_st_sequential ertl_params_ … (joint_instr_extension ertl_params__ globals ertl_st_ext_new_frame) start_lbl 170 87 ]) :: 171 88 (adds_graph … [ … … 196 113 let restl ≝ \snd (\fst crl) in 197 114 let restr ≝ \snd (\snd crl) in 198 let init_tmpr ≝ joint_st_sequential ertl_params_ … (joint_instr_int … tmpr (zero ?)) start_lbl in115 let init_tmpr ≝ joint_st_sequential ertl_params_ … (joint_instr_int … tmpr (zero …)) start_lbl in 199 116 let f_save ≝ λst. λr. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo r〉) start_lbl in 200 let saves ≝ map2 ? ? ?f_save commonl commonr crl_proof in117 let saves ≝ map2 … f_save commonl commonr crl_proof in 201 118 let f_default ≝ λst. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo tmpr〉) start_lbl in 202 let defaults ≝ map ? ?f_default restl in203 adds_graph … (init_tmpr :: saves @ defaults) start_lbl dest_lbl def119 let defaults ≝ map … f_default restl in 120 adds_graph ertl_params1 … (init_tmpr :: saves @ defaults) start_lbl dest_lbl def 204 121 ]. 205 122 … … 212 129 let f ≝ λret. λst. joint_st_sequential ertl_params_ globals (joint_instr_move … 〈hardware ret, hardware st〉) start_lbl in 213 130 let insts ≝ map2 ? ? ? f commonl commonr crl_proof in 214 adds_graph … insts start_lbl131 adds_graph ertl_params1 … insts start_lbl 215 132 ]. 216 133 … … 224 141 let start_lbl ≝ joint_if_exit … (ertl_params globals) def in 225 142 let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in 226 match lookup … (joint_if_code … (ertl_params globals)def) start_lbl143 match lookup … (joint_if_code … def) start_lbl 227 144 return λx. x ≠ None ? → ertl_internal_function globals with 228 145 [ None ⇒ λnone_absrd. ⊥ 229 146  Some last_stmt ⇒ λsome_prf. 230 147 let def ≝ 231 add_translates … (148 add_translates ertl_params1 … ( 232 149 [save_return globals ret_regs] @ 233 150 restore_hdws … sregs @ … … 236 153 joint_st_sequential … (joint_instr_push … sral) start_lbl 237 154 ]] @ 238 [adds_graph … [155 [adds_graph ertl_params1 … [ 239 156 joint_st_sequential … (joint_instr_extension … ertl_st_ext_del_frame) start_lbl 240 157 ]] @ … … 261 178 λdef_sregs. 262 179 let 〈def, sregs〉 ≝ def_sregs in 263 let 〈def, r'〉 ≝ fresh_reg globals def in180 let 〈def, r'〉 ≝ fresh_reg ertl_params0 globals def in 264 181 〈def, 〈r', r〉 :: sregs〉 265 182 in … … 271 188 λret_regs. 272 189 λdef. 273 match fresh_regs_strong globals def 2 with190 match fresh_regs_strong … globals def 2 with 274 191 [ dp def_sra def_sra_proof ⇒ 275 192 let def ≝ \fst def_sra in … … 305 222 let 〈def, tmpr〉 ≝ fresh_reg … def in 306 223 let 〈ignore, int_off〉 ≝ half_add ? off int_size in 307 adds_graph ?[224 adds_graph ertl_params1 … [ 308 225 joint_st_sequential … (joint_instr_int … addr1 int_off) start_lbl; 309 226 joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl; … … 319 236 λglobals,params. 320 237 match params with 321 [ nil ⇒ [ λstart_lbl. adds_graph globals [joint_st_goto … start_lbl] start_lbl]238 [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [joint_st_goto … start_lbl] start_lbl] 322 239  _ ⇒ 323 240 let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in … … 350 267 let f_restore ≝ λr. λst. joint_st_sequential ertl_params_ … (joint_instr_move … 〈pseudo r, hardware st〉) start_lbl in 351 268 let restores ≝ map2 ? ? ? f_restore commonl commonr ? in 352 adds_graph … (saves @ restores) start_lbl]].269 adds_graph ertl_params1 … (saves @ restores) start_lbl]]. 353 270 [@second_crl_proof  @first_crl_proof] 354 271 qed. … … 362 279 λdef. 363 280 let nb_args ≝ args in 364 add_translates globals (281 add_translates ertl_params1 globals ( 365 282 set_params … args @ [ 366 adds_graph … [ joint_st_sequential … (joint_instr_call_id … f nb_args it) start_lbl ];283 adds_graph ertl_params1 … [ joint_st_sequential … (joint_instr_call_id … f nb_args it) start_lbl ]; 367 284 fetch_result … ret_regs 368 285 ] … … 388 305 let 〈r1,r2〉 ≝ rs in 389 306 let rs ≝ 〈pseudo r1, pseudo r2〉 in 390 add_graph … lbl (joint_st_sequential ertl_params_… (joint_instr_move … rs) lbl') def307 add_graph ertl_params1 ? lbl (joint_st_sequential … (joint_instr_move … rs) lbl') def 391 308  joint_instr_extension ext ⇒ 392 309 match ext with 393 310 [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *) 394 311  rtlntc_st_ext_address r1 r2 ⇒ 395 adds_graph … [312 adds_graph ertl_params1 … [ 396 313 joint_st_sequential … (joint_instr_move … 〈pseudo r1, hardware RegisterSPL〉) lbl; 397 314 joint_st_sequential … (joint_instr_move … 〈pseudo r2, hardware RegisterSPH〉) lbl … … 400 317 the problem is call_id that takes different parameters, but that is patternmatched 401 318 above. It could be made nicer at the cost of making all the rest of the code uglier *) 402  joint_instr_cost_label cost_lbl ⇒ add_graph … lbl (joint_st_sequential ertl_params_… (joint_instr_cost_label … cost_lbl) lbl') def403  joint_instr_address x prf r1 r2 ⇒ add_graph … lbl (joint_st_sequential ertl_params_… (joint_instr_address … x prf r1 r2) lbl') def404  joint_instr_int r i ⇒ add_graph … lbl (joint_st_sequential ertl_params_ globals(joint_instr_int … r i) lbl') def319  joint_instr_cost_label cost_lbl ⇒ add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_cost_label … cost_lbl) lbl') def 320  joint_instr_address x prf r1 r2 ⇒ add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_address … x prf r1 r2) lbl') def 321  joint_instr_int r i ⇒ add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_int … r i) lbl') def 405 322  joint_instr_opaccs op destr1 destr2 srcr1 srcr2 ⇒ 406 add_graph … lbl (joint_st_sequential ertl_params_… (joint_instr_opaccs … op destr1 destr2 srcr1 srcr2) lbl') def323 add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_opaccs … op destr1 destr2 srcr1 srcr2) lbl') def 407 324  joint_instr_op1 op1 destr srcr ⇒ 408 add_graph … lbl (joint_st_sequential ertl_params_… (joint_instr_op1 … op1 destr srcr) lbl') def325 add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_op1 … op1 destr srcr) lbl') def 409 326  joint_instr_op2 op2 destr srcr1 srcr2 ⇒ 410 add_graph … lbl (joint_st_sequential ertl_params_… (joint_instr_op2 … op2 destr srcr1 srcr2) lbl') def327 add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_op2 … op2 destr srcr1 srcr2) lbl') def 411 328  joint_instr_clear_carry ⇒ 412 add_graph … lbl (joint_st_sequential ertl_params_… (joint_instr_clear_carry …) lbl') def329 add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_clear_carry …) lbl') def 413 330  joint_instr_set_carry ⇒ 414 add_graph … lbl (joint_st_sequential ertl_params_… (joint_instr_set_carry …) lbl') def331 add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_set_carry …) lbl') def 415 332  joint_instr_load destr addr1 addr2 ⇒ 416 add_graph … lbl (joint_st_sequential ertl_params_… (joint_instr_load … destr addr1 addr2) lbl') def333 add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_load … destr addr1 addr2) lbl') def 417 334  joint_instr_store addr1 addr2 srcr ⇒ 418 add_graph … lbl (joint_st_sequential ertl_params_… (joint_instr_store … addr1 addr2 srcr) lbl') def335 add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_store … addr1 addr2 srcr) lbl') def 419 336  joint_instr_cond srcr lbl_true ⇒ 420 add_graph … lbl (joint_st_sequential ertl_params_… (joint_instr_cond … srcr lbl_true) lbl') def337 add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_cond … srcr lbl_true) lbl') def 421 338  joint_instr_comment msg ⇒ 422 add_graph … lbl (joint_st_sequential ertl_params_… (joint_instr_comment … msg) lbl') def339 add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_comment … msg) lbl') def 423 340 ]]. 424 casesnot_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *)341 @not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *) 425 342 qed. 426 343 … … 452 369 λglobals. 453 370 λstmt. 454 λdef .371 λdef: joint_internal_function … (ertl_params globals). 455 372 let 〈entry, nuniv〉 ≝ fresh_label … def in 456 373 let graph ≝ add ? ? (joint_if_code … def) entry stmt in … … 476 393 match inst with 477 394 [ joint_instr_cost_label cost_lbl ⇒ 478 〈Some … cost_lbl, add_graph ertl_params _globals lbl (joint_st_goto … lbl) def〉395 〈Some … cost_lbl, add_graph ertl_params1 globals lbl (joint_st_goto … lbl) def〉 479 396  _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ] 480 397  joint_st_return ⇒ 〈None …, def〉
Note: See TracChangeset
for help on using the changeset viewer.