Changeset 1153 for Deliverables/D3.3/idlookupbranch/RTL/RTLtoERTL.ma
 Timestamp:
 Aug 30, 2011, 6:55:12 PM (9 years ago)
 Location:
 Deliverables/D3.3/idlookupbranch
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch
 Property svn:mergeinfo changed
/src merged: 11101132,11361150
 Property svn:mergeinfo changed

Deliverables/D3.3/idlookupbranch/RTL/RTLtoERTL.ma
r1109 r1153 97 97  ertl_st_pop r _ ⇒ ertl_st_pop r l 98 98  ertl_st_push r _ ⇒ ertl_st_push r l 99  ertl_st_addr_h r id _ ⇒ ertl_st_addr_h r id l 100  ertl_st_addr_l r id _ ⇒ ertl_st_addr_l r id l 99  ertl_st_addr r1 r2 x _ ⇒ ertl_st_addr r1 r2 x l 101 100  ertl_st_int r i _ ⇒ ertl_st_int r i l 102 101  ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l 103  ertl_st_opaccs_a opaccs d s1 s2 _ ⇒ ertl_st_opaccs_a opaccs d s1 s2 l 104  ertl_st_opaccs_b opaccs d s1 s2 _ ⇒ ertl_st_opaccs_b opaccs d s1 s2 l 102  ertl_st_opaccs opaccs d1 d2 s1 s2 _ ⇒ ertl_st_opaccs opaccs d1 s1 s1 s2 l 105 103  ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l 106 104  ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l … … 224 222 [ nil ⇒ [get_params_hdw_internal] 225 223  _ ⇒ 226 let l ≝ zip_pottier ? ? params parameters in224 let l ≝ zip_pottier ? ? params RegisterParams in 227 225 save_hdws l 228 226 ]. … … 260 258 definition get_params ≝ 261 259 λparams. 262 let n ≝ min (length ? params) (length ? parameters) in260 let n ≝ min (length ? params) (length ? RegisterParams) in 263 261 let 〈hdw_params, stack_params〉 ≝ list_split ? n params in 264 262 let hdw_params ≝ get_params_hdw hdw_params in … … 396 394 [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl] 397 395  _ ⇒ 398 let l ≝ zip_pottier ? ? params parameters in396 let l ≝ zip_pottier ? ? params RegisterParams in 399 397 restore_hdws l 400 398 ]. … … 436 434 definition set_params ≝ 437 435 λparams. 438 let n ≝ min (params) ( parameters) in436 let n ≝ min (params) (RegisterParams) in 439 437 let hdw_stack_params ≝ split ? params n ? in 440 438 let hdw_params ≝ \fst hdw_stack_params in … … 477 475 add_translates ( 478 476 set_params args @ [ 479 adds_graph [ ertl_st_call_id f (bitvector_of_nat ? nb_args)start_lbl ];477 adds_graph [ ertl_st_call_id f nb_args start_lbl ]; 480 478 fetch_result ret_regs 481 479 ] … … 489 487 [ rtl_st_skip lbl' ⇒ add_graph lbl (ertl_st_skip lbl') def 490 488  rtl_st_cost cost_lbl lbl' ⇒ add_graph lbl (ertl_st_cost cost_lbl lbl') def 491  rtl_st_addr r1 r2 x lbl' ⇒ 492 adds_graph [ 493 ertl_st_addr_l r1 x lbl; 494 ertl_st_addr_h r2 x lbl 495 ] lbl lbl' def 489  rtl_st_addr r1 r2 x lbl' ⇒ add_graph lbl (ertl_st_addr r1 r2 x lbl') def 496 490  rtl_st_stack_addr r1 r2 lbl' ⇒ 497 491 adds_graph [ … … 502 496  rtl_st_move r1 r2 lbl' ⇒ add_graph lbl (ertl_st_move r1 r2 lbl') def 503 497  rtl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl' ⇒ 498 add_graph lbl (ertl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl) def 499 (* XXX: change from o'caml 504 500 adds_graph [ 505 501 ertl_st_opaccs_a op destr1 srcr1 srcr2 lbl; 506 502 ertl_st_opaccs_b op destr2 srcr1 srcr2 lbl 507 503 ] lbl lbl' def 504 *) 508 505  rtl_st_op1 op1 destr srcr lbl' ⇒ 509 506 add_graph lbl (ertl_st_op1 op1 destr srcr lbl') def … … 533 530 λdef. 534 531 let nb_params ≝ rtl_if_params def in 535 let added_stacksize ≝ max 0 (nb_params   parameters) in532 let added_stacksize ≝ max 0 (nb_params  RegisterParams) in 536 533 let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in 537 534 let entry' ≝ rtl_if_entry def in … … 619 616  ertl_st_pop _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 620 617  ertl_st_push _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 621  ertl_st_addr_h _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 622  ertl_st_addr_l _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 618  ertl_st_addr _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 623 619  ertl_st_int _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 624 620  ertl_st_move _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 625  ertl_st_opaccs_a _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 626  ertl_st_opaccs_b _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 621  ertl_st_opaccs _ _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 627 622  ertl_st_op1 _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 628 623  ertl_st_op2 _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
Note: See TracChangeset
for help on using the changeset viewer.