 Timestamp:
 Jul 19, 2011, 4:30:04 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLtoERTL.ma
r1077 r1079 1 1 include "RTL/RTL.ma". 2 include "RTL/RTLTailcall.ma". 2 3 include "utilities/RegisterSet.ma". 3 4 include "common/Identifiers.ma". … … 528 529 qed. 529 530 531 (* hack with empty graphs used here *) 530 532 definition translate_funct_internal ≝ 531 533 λdef. … … 535 537 let entry' ≝ rtl_if_entry def in 536 538 let exit' ≝ rtl_if_exit def in 539 let graph' ≝ add ? ? (empty_map ? ?) entry' (ertl_st_skip entry') in 540 let graph' ≝ add ? ? graph' exit' (ertl_st_skip exit') in 537 541 let def' ≝ 538 542 mk_ertl_internal_function 539 543 (rtl_if_luniverse def) (rtl_if_runiverse def) 540 544 nb_params new_locals ((rtl_if_stacksize def) + added_stacksize) 541 (empty_map ? ?)? ? in545 graph' ? ? in 542 546 let def' ≝ foldi ? ? ? translate_stmt (rtl_if_graph def) def' in 543 547 let def' ≝ add_pro_and_epilogue (rtl_if_params def) (rtl_if_result def) def' in 544 548 def'. 545 [1: cases entry' 546 #LBL #LBL_PRF 547 % 548 [1: @LBL 549 2: @LBL_PRF 549 [1: % 550 [1: @entry' 551 2: normalize nodelta 552 @graph_add_lookup 553 @graph_add 554 ] 555 2: % 556 [1: @exit' 557 2: normalize nodelta 558 @graph_add 559 ] 560 ] 561 qed. 550 562 551 563 definition translate_funct ≝ … … 567 579 nuniv (ertl_if_runiverse def) (ertl_if_params def) 568 580 (ertl_if_locals def) (ertl_if_stacksize def) graph 569 entry (ertl_if_exit def). 570 571 let generate stmt def = 572 let entry = Label.Gen.fresh def.ERTL.f_luniverse in 573 let def = 574 { def with ERTL.f_graph = Label.Map.add entry stmt def.ERTL.f_graph } in 575 { def with ERTL.f_entry = entry } 576 581 ? ?. 582 [1: % 583 [1: @entry 584 2: normalize nodelta; 585 @graph_add 586 ] 587 2: generalize in match (ertl_if_exit def) 588 #HYP 589 cases HYP 590 #LBL #LBL_PRF 591 % 592 [1: @LBL 593 2: normalize nodelta; 594 @graph_add_lookup 595 @LBL_PRF 596 ] 597 ] 598 qed. 599 600 let rec find_and_remove_first_cost_label_internal 601 (def: ertl_internal_function) (lbl: label) (num_nodes: nat) 602 on num_nodes ≝ 603 match num_nodes with 604 [ O ⇒ 〈None ?, def〉 605  S num_nodes' ⇒ 606 match lookup ? ? (ertl_if_graph def) lbl with 607 [ None ⇒ 〈None ?, def〉 608  Some stmt ⇒ 609 match stmt with 610 [ ertl_st_cost cost_lbl next_lbl ⇒ 611 〈Some ? cost_lbl, add_graph lbl (ertl_st_skip next_lbl) def〉 612  ertl_st_cond _ _ _ ⇒ 〈None ?, def〉 613  ertl_st_return ⇒ 〈None ?, def〉 614  ertl_st_skip lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 615  ertl_st_comment _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 616  ertl_st_get_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 617  ertl_st_set_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 618  ertl_st_hdw_to_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 619  ertl_st_pop _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 620  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' 623  ertl_st_int _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 624  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' 627  ertl_st_op1 _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 628  ertl_st_op2 _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 629  ertl_st_clear_carry lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 630  ertl_st_set_carry lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 631  ertl_st_load _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 632  ertl_st_store _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 633  ertl_st_call_id _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 634  ertl_st_new_frame lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 635  ertl_st_del_frame lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 636  ertl_st_frame_size _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 637 ] 638 ] 639 ]. 640 641 definition find_and_remove_first_cost_label ≝ 642 λdef. 643 find_and_remove_first_cost_label_internal def (ertl_if_entry def) (graph_num_nodes ? (ertl_if_graph def)). 644 645 definition move_first_cost_label_up_internal ≝ 646 λdef. 647 let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label def in 648 match cost_label with 649 [ None ⇒ def 650  Some cost_label ⇒ generate (ertl_st_cost cost_label (ertl_if_entry def)) def 651 ]. 652 653 definition move_first_cost_label_up ≝ 654 λA: Type[0]. 655 λid_def: A × ?. 656 let 〈id, def〉 ≝ id_def in 657 let def' ≝ 658 match def with 659 [ Internal int_fun ⇒ Internal ? (move_first_cost_label_up_internal int_fun) 660  External ext ⇒ def 661 ] 662 in 663 〈id, def'〉. 664 665 definition translate ≝ 666 λp. 667 let p ≝ tailcall_simplify p in (* tailcall simplification here *) 668 let f ≝ λfunct. move_first_cost_label_up ? (translate_funct funct) in 669 let vars ≝ map ? ? f (rtl_pr_functs p) in 670 mk_ertl_program (rtl_pr_vars p) vars (rtl_pr_main p). 671 672 let translate p = 673 (* We simplify tail calls as regular calls for now. *) 674 let p = RTLtailcall.simplify p in 675 (* The tranformation on each RTL function: create an ERTL function and move 676 its first cost label at the very beginning. *) 677 let f funct = move_first_cost_label_up (translate_funct funct) in 678 { ERTL.vars = p.RTL.vars ; 679 ERTL.functs = List.map f p.RTL.functs ; 680 ERTL.main = p.RTL.main } 577 681 578 682 definition save_return_internal ≝
Note: See TracChangeset
for help on using the changeset viewer.