 Timestamp:
 Sep 28, 2011, 11:50:32 PM (9 years ago)
 Location:
 src/RTL
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLTailcall.ma
r1275 r1282 8 8 λgraph: codeT … (rtlntc_params globals). 9 9 match stmt with 10 [ joint_st_sequential seq DUMMY ⇒10 [ sequential seq DUMMY ⇒ 11 11 match seq with 12 [ joint_instr_extension ext ⇒12 [ extension ext ⇒ 13 13 match ext with 14 14 [ rtl_st_ext_tailcall_id f args ⇒ 15 add ? ? graph lbl ( joint_st_sequential … (joint_instr_call_id… f args [ ]) exit)15 add ? ? graph lbl (sequential … (CALL_ID … f args [ ]) exit) 16 16  rtl_st_ext_tailcall_ptr f1 f2 args ⇒ 17 add ? ? graph lbl ( joint_st_sequential … (joint_instr_extension … (rtlntc_st_ext_call_ptr f1 f2 args [ ])) exit)17 add ? ? graph lbl (sequential … (extension … (rtlntc_st_ext_call_ptr f1 f2 args [ ])) exit) 18 18  _ ⇒ graph ] 19 19  _ ⇒ graph ] 
src/RTL/RTLtoERTL.ma
r1280 r1282 10 10 λdestr_srcr.λstart_lbl. 11 11 let 〈destr, srcr〉 ≝ destr_srcr in 12 adds_graph ertl_params1 globals [ joint_st_sequential … (joint_instr_move… 〈pseudo destr,hardware srcr〉) start_lbl ] start_lbl12 adds_graph ertl_params1 globals [ sequential … (MOVE … 〈pseudo destr,hardware srcr〉) start_lbl ] start_lbl 13 13 in 14 14 map ? ? save_hdws_internal l. … … 20 20 λstart_lbl: label. 21 21 let 〈srcr, destr〉 ≝ srcr_destr in 22 adds_graph ertl_params1 globals [ joint_st_sequential … (joint_instr_move… 〈hardware destr, pseudo srcr〉) start_lbl ] start_lbl22 adds_graph ertl_params1 globals [ sequential … (MOVE … 〈hardware destr, pseudo srcr〉) start_lbl ] start_lbl 23 23 in 24 24 map ? ? restore_hdws_internal l. … … 28 28 λparams: list register. 29 29 match params with 30 [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ joint_st_goto… start_lbl ] start_lbl]30 [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ GOTO … start_lbl ] start_lbl] 31 31  _ ⇒ 32 32 let l ≝ zip_pottier ? ? params RegisterParams in … … 44 44 let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in 45 45 adds_graph ertl_params1 globals [ 46 joint_st_sequential … (joint_instr_extension … (ertl_st_ext_frame_size addr1)) start_lbl;47 joint_st_sequential … (joint_instr_int… tmpr int_offset) start_lbl;48 joint_st_sequential … (joint_instr_op2 … Sub addr1 addr1 tmpr) start_lbl;49 joint_st_sequential … (joint_instr_move… 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl;50 joint_st_sequential … (joint_instr_op2 … Add addr1 addr1 tmpr) start_lbl;51 joint_st_sequential … (joint_instr_int… addr2 (bitvector_of_nat 8 0)) start_lbl;52 joint_st_sequential … (joint_instr_move… 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl;53 joint_st_sequential … (joint_instr_op2 … Addc addr2 addr2 tmpr) start_lbl;54 joint_st_sequential … (joint_instr_load… destr addr1 addr2) start_lbl46 sequential … (extension … (ertl_st_ext_frame_size addr1)) start_lbl; 47 sequential … (INT … tmpr int_offset) start_lbl; 48 sequential … (OP2 … Sub addr1 addr1 tmpr) start_lbl; 49 sequential … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl; 50 sequential … (OP2 … Add addr1 addr1 tmpr) start_lbl; 51 sequential … (INT … addr2 (bitvector_of_nat 8 0)) start_lbl; 52 sequential … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl; 53 sequential … (OP2 … Addc addr2 addr2 tmpr) start_lbl; 54 sequential … (LOAD … destr addr1 addr2) start_lbl 55 55 ] start_lbl dest_lbl def. 56 56 … … 58 58 λglobals,params. 59 59 match params with 60 [ nil ⇒ [ λstart_lbl. adds_graph … [ joint_st_goto… start_lbl] start_lbl ]60 [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO … start_lbl] start_lbl ] 61 61  _ ⇒ mapi ? ? (get_param_stack globals) params ]. 62 62 … … 84 84 add_translates … 85 85 ((adds_graph ertl_params1 … [ 86 joint_st_sequential ertl_params_ … (joint_instr_extension ertl_params__ globals ertl_st_ext_new_frame) start_lbl86 sequential ertl_params_ … (extension ertl_params__ globals ertl_st_ext_new_frame) start_lbl 87 87 ]) :: 88 88 (adds_graph … [ 89 joint_st_sequential … (joint_instr_pop… sral) start_lbl;90 joint_st_sequential … (joint_instr_pop… srah) start_lbl89 sequential … (POP … sral) start_lbl; 90 sequential … (POP … srah) start_lbl 91 91 ]) :: 92 92 (save_hdws … sregs) @ … … 113 113 let restl ≝ \snd (\fst crl) in 114 114 let restr ≝ \snd (\snd crl) in 115 let init_tmpr ≝ joint_st_sequential ertl_params_ … (joint_instr_int… tmpr (zero …)) start_lbl in116 let f_save ≝ λst. λr. joint_st_sequential ertl_params_ … (joint_instr_move… 〈hardware st, pseudo r〉) start_lbl in115 let init_tmpr ≝ sequential ertl_params_ … (INT … tmpr (zero …)) start_lbl in 116 let f_save ≝ λst. λr. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo r〉) start_lbl in 117 117 let saves ≝ map2 … f_save commonl commonr crl_proof in 118 let f_default ≝ λst. joint_st_sequential ertl_params_ … (joint_instr_move… 〈hardware st, pseudo tmpr〉) start_lbl in118 let f_default ≝ λst. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo tmpr〉) start_lbl in 119 119 let defaults ≝ map … f_default restl in 120 120 adds_graph ertl_params1 … (init_tmpr :: saves @ defaults) start_lbl dest_lbl def … … 127 127 let commonl ≝ \fst (\fst crl) in 128 128 let commonr ≝ \fst (\snd crl) in 129 let f ≝ λret. λst. joint_st_sequential ertl_params_ globals (joint_instr_move… 〈hardware ret, hardware st〉) start_lbl in129 let f ≝ λret. λst. sequential ertl_params_ globals (MOVE … 〈hardware ret, hardware st〉) start_lbl in 130 130 let insts ≝ map2 ? ? ? f commonl commonr crl_proof in 131 131 adds_graph ertl_params1 … insts start_lbl … … 150 150 restore_hdws … sregs @ 151 151 [adds_graph … [ 152 joint_st_sequential … (joint_instr_push… srah) start_lbl;153 joint_st_sequential … (joint_instr_push… sral) start_lbl152 sequential … (PUSH … srah) start_lbl; 153 sequential … (PUSH … sral) start_lbl 154 154 ]] @ 155 155 [adds_graph ertl_params1 … [ 156 joint_st_sequential … (joint_instr_extension … ertl_st_ext_del_frame) start_lbl156 sequential … (extension … ertl_st_ext_del_frame) start_lbl 157 157 ]] @ 158 158 [assign_result globals] … … 205 205 λglobals,params. 206 206 match params with 207 [ nil ⇒ [ λstart_lbl. adds_graph … [ joint_st_goto… start_lbl] start_lbl]207 [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO … start_lbl] start_lbl] 208 208  _ ⇒ 209 209 let l ≝ zip_pottier ? ? params RegisterParams in … … 223 223 let 〈ignore, int_off〉 ≝ half_add ? off int_size in 224 224 adds_graph ertl_params1 … [ 225 joint_st_sequential … (joint_instr_int… addr1 int_off) start_lbl;226 joint_st_sequential … (joint_instr_move… 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl;227 joint_st_sequential … (joint_instr_clear_carry…) start_lbl;228 joint_st_sequential … (joint_instr_op2 … Sub addr1 tmpr addr1) start_lbl;229 joint_st_sequential … (joint_instr_move… 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl;230 joint_st_sequential … (joint_instr_int… addr2 (zero ?)) start_lbl;231 joint_st_sequential … (joint_instr_op2 … Sub addr2 tmpr addr2) start_lbl;232 joint_st_sequential … (joint_instr_store… addr1 addr2 srcr) start_lbl225 sequential … (INT … addr1 int_off) start_lbl; 226 sequential … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl; 227 sequential … (CLEAR_CARRY …) start_lbl; 228 sequential … (OP2 … Sub addr1 tmpr addr1) start_lbl; 229 sequential … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl; 230 sequential … (INT … addr2 (zero ?)) start_lbl; 231 sequential … (OP2 … Sub addr2 tmpr addr2) start_lbl; 232 sequential … (STORE … addr1 addr2 srcr) start_lbl 233 233 ] start_lbl dest_lbl def. 234 234 … … 236 236 λglobals,params. 237 237 match params with 238 [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [ joint_st_goto… start_lbl] start_lbl]238 [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [GOTO … start_lbl] start_lbl] 239 239  _ ⇒ 240 240 let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in … … 259 259 let commonl ≝ \fst (\fst crl) in 260 260 let commonr ≝ \fst (\snd crl) in 261 let f_save ≝ λst. λret. joint_st_sequential ertl_params_ globals (joint_instr_move… 〈hardware st, hardware ret〉) start_lbl in261 let f_save ≝ λst. λret. sequential ertl_params_ globals (MOVE … 〈hardware st, hardware ret〉) start_lbl in 262 262 let saves ≝ map2 ? ? ? f_save commonl commonr ? in 263 263 match reduce_strong ? ? ret_regs RegisterSTS with … … 265 265 let commonl ≝ \fst (\fst crl) in 266 266 let commonr ≝ \fst (\snd crl) in 267 let f_restore ≝ λr. λst. joint_st_sequential ertl_params_ … (joint_instr_move… 〈pseudo r, hardware st〉) start_lbl in267 let f_restore ≝ λr. λst. sequential ertl_params_ … (MOVE … 〈pseudo r, hardware st〉) start_lbl in 268 268 let restores ≝ map2 ? ? ? f_restore commonl commonr ? in 269 269 adds_graph ertl_params1 … (saves @ restores) start_lbl]]. … … 281 281 add_translates ertl_params1 globals ( 282 282 set_params … args @ [ 283 adds_graph ertl_params1 … [ joint_st_sequential … (joint_instr_call_id… f nb_args it) start_lbl ];283 adds_graph ertl_params1 … [ sequential … (CALL_ID … f nb_args it) start_lbl ]; 284 284 fetch_result … ret_regs 285 285 ] … … 294 294 λdef. 295 295 match stmt with 296 [ joint_st_goto lbl' ⇒ add_graph … lbl (joint_st_goto… lbl') def297  joint_st_return ⇒ add_graph … lbl (joint_st_return…) def298  joint_st_sequential seq lbl' ⇒296 [ GOTO lbl' ⇒ add_graph … lbl (GOTO … lbl') def 297  RETURN ⇒ add_graph … lbl (RETURN …) def 298  sequential seq lbl' ⇒ 299 299 match seq with 300 [ joint_instr_push_ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)301  joint_instr_pop_ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)302  joint_instr_call_idf args ret_regs ⇒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 ⇒ 303 303 translate_call_id … f args ret_regs lbl lbl' def 304  joint_instr_movers ⇒304  MOVE rs ⇒ 305 305 let 〈r1,r2〉 ≝ rs in 306 306 let rs ≝ 〈pseudo r1, pseudo r2〉 in 307 add_graph ertl_params1 ? lbl ( joint_st_sequential … (joint_instr_move… rs) lbl') def308  joint_instr_extension ext ⇒307 add_graph ertl_params1 ? lbl (sequential … (MOVE … rs) lbl') def 308  extension ext ⇒ 309 309 match ext with 310 310 [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *) 311 311  rtlntc_st_ext_address r1 r2 ⇒ 312 312 adds_graph ertl_params1 … [ 313 joint_st_sequential … (joint_instr_move… 〈pseudo r1, hardware RegisterSPL〉) lbl;314 joint_st_sequential … (joint_instr_move… 〈pseudo r2, hardware RegisterSPH〉) lbl313 sequential … (MOVE … 〈pseudo r1, hardware RegisterSPL〉) lbl; 314 sequential … (MOVE … 〈pseudo r2, hardware RegisterSPH〉) lbl 315 315 ] lbl lbl' def] 316 316 (*CSC: everything is just copied to retype it from now on; 317 317 the problem is call_id that takes different parameters, but that is patternmatched 318 318 above. It could be made nicer at the cost of making all the rest of the code uglier *) 319  joint_instr_cost_label cost_lbl ⇒ add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_cost_label… cost_lbl) lbl') def320  joint_instr_address x prf r1 r2 ⇒ add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_address… x prf r1 r2) lbl') def321  joint_instr_int r i ⇒ add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_int… r i) lbl') def322  joint_instr_opaccsop destr1 destr2 srcr1 srcr2 ⇒323 add_graph ertl_params1 … lbl ( joint_st_sequential … (joint_instr_opaccs… op destr1 destr2 srcr1 srcr2) lbl') def324  joint_instr_op1 op1 destr srcr ⇒325 add_graph ertl_params1 … lbl ( joint_st_sequential … (joint_instr_op1 … op1 destr srcr) lbl') def326  joint_instr_op2 op2 destr srcr1 srcr2 ⇒327 add_graph ertl_params1 … lbl ( joint_st_sequential … (joint_instr_op2 … op2 destr srcr1 srcr2) lbl') def328  joint_instr_clear_carry⇒329 add_graph ertl_params1 … lbl ( joint_st_sequential … (joint_instr_clear_carry…) lbl') def330  joint_instr_set_carry⇒331 add_graph ertl_params1 … lbl ( joint_st_sequential … (joint_instr_set_carry…) lbl') def332  joint_instr_loaddestr addr1 addr2 ⇒333 add_graph ertl_params1 … lbl ( joint_st_sequential … (joint_instr_load… destr addr1 addr2) lbl') def334  joint_instr_storeaddr1 addr2 srcr ⇒335 add_graph ertl_params1 … lbl ( joint_st_sequential … (joint_instr_store… addr1 addr2 srcr) lbl') def336  joint_instr_condsrcr lbl_true ⇒337 add_graph ertl_params1 … lbl ( joint_st_sequential … (joint_instr_cond… srcr lbl_true) lbl') def338  joint_instr_commentmsg ⇒339 add_graph ertl_params1 … lbl ( joint_st_sequential … (joint_instr_comment… msg) lbl') def319  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 340 340 ]]. 341 341 @not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *) … … 350 350 let entry' ≝ joint_if_entry … def in 351 351 let exit' ≝ joint_if_exit … def in 352 let graph' ≝ add ? ? (empty_map ? ?) entry' ( joint_st_goto… entry') in353 let graph' ≝ add ? ? graph' exit' ( joint_st_goto… exit') in352 let graph' ≝ add ? ? (empty_map ? ?) entry' (GOTO … entry') in 353 let graph' ≝ add ? ? graph' exit' (GOTO … exit') in 354 354 let def' ≝ 355 355 mk_joint_internal_function globals (ertl_params globals) … … 390 390  Some stmt ⇒ 391 391 match stmt with 392 [ joint_st_sequential inst lbl ⇒392 [ sequential inst lbl ⇒ 393 393 match inst with 394 [ joint_instr_cost_labelcost_lbl ⇒395 〈Some … cost_lbl, add_graph ertl_params1 globals lbl ( joint_st_goto… lbl) def〉394 [ COST_LABEL cost_lbl ⇒ 395 〈Some … cost_lbl, add_graph ertl_params1 globals lbl (GOTO … lbl) def〉 396 396  _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ] 397  joint_st_return⇒ 〈None …, def〉398  joint_st_gotolbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'397  RETURN ⇒ 〈None …, def〉 398  GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' 399 399 ]]]. 400 400 … … 408 408 match cost_label with 409 409 [ None ⇒ def 410  Some cost_label ⇒ generate … ( joint_st_sequential ertl_params_ globals (joint_instr_cost_label… cost_label) (joint_if_entry … def)) def410  Some cost_label ⇒ generate … (sequential ertl_params_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def 411 411 ]. 412 412
Note: See TracChangeset
for help on using the changeset viewer.