 Timestamp:
 Oct 3, 2011, 4:55:17 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1286 r1287 509 509 (* 510 510 definition translate_mul ≝ 511 λglobals: list ident. 511 512 λdestrs: list register. 512 513 λsrcrs1: list register. … … 514 515 λstart_lbl: label. 515 516 λdest_lbl: label. 516 λdef: rtl_internal_function .517 let 〈def, dummy〉 ≝ fresh_reg def in518 let 〈def, tmpr〉 ≝ fresh_reg def in519 let 〈def, tmp_destrs〉 ≝ fresh_regs def (destrs) in520 let 〈def, fresh_srcrs1〉 ≝ fresh_regs def (srcrs1) in521 let 〈def, fresh_srcrs2〉 ≝ fresh_regs def (srcrs2) in517 λdef: rtl_internal_function globals. 518 let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in 519 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 520 let 〈def, tmp_destrs〉 ≝ fresh_regs rtl_params0 globals def (destrs) in 521 let 〈def, fresh_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (srcrs1) in 522 let 〈def, fresh_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (srcrs2) in 522 523 let insts_init ≝ [ 523 translate_move fresh_srcrs1 srcrs1;524 translate_move fresh_srcrs2 srcrs2;525 translate_cst (Ointconst I8 (zero ?)) destrs524 translate_move globals fresh_srcrs1 srcrs1; 525 translate_move globals fresh_srcrs2 srcrs2; 526 translate_cst globals (Ointconst I8 (zero …)) destrs 526 527 ] 527 528 in 528 let f ≝ λi. translate_muli dummy tmpr destrs tmp_destrs ? fresh_srcrs1 start_lbl i ? in529 let insts_mul ≝ foldi ? ?[ ] srcrs2 in ?. [5: check insts_init.529 let f ≝ λi. translate_muli globals dummy tmpr destrs tmp_destrs ? fresh_srcrs1 start_lbl i ? in 530 let insts_mul ≝ foldi … [ ] srcrs2 in ?. [5: check insts_init. 530 531 add_translates (insts_init @ insts_mul) start_lbl dest_lbl def. 531 532 *) 532 533 533 534 definition translate_divumodu8 ≝ 535 λglobals: list ident. 534 536 λorder: bool. 535 537 λdestrs: list register. … … 538 540 λstart_lbl: label. 539 541 λdest_lbl: label. 540 λdef: rtl_internal_function .542 λdef: rtl_internal_function globals. 541 543 match destrs with 542 [ nil ⇒ add_graph start_lbl (rtl_st_skipdest_lbl) def544 [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def 543 545  cons destr destrs ⇒ 544 let 〈def, dummy〉 ≝ fresh_reg def in546 let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in 545 547 let 〈destr1, destr2〉 ≝ match order with [ true ⇒ 〈destr, dummy〉  _ ⇒ 〈dummy, destr〉 ] in 546 let inst_div ≝ adds_graph [547 rtl_st_opaccs DivuModu destr1 destr2 srcr1 srcr2 start_lbl548 let inst_div ≝ adds_graph rtl_params1 globals [ 549 sequential rtl_params_ globals (OPACCS … DivuModu destr1 destr2 srcr1 srcr2) 548 550 ] 549 551 in 550 let insts_rest ≝ translate_cst (Ointconst I8 (zero ?)) destrs in 551 add_translates [ inst_div; insts_rest ] start_lbl dest_lbl def 552 ]. 553 554 definition translate_ne: ? → ? → ? → ? → ? → ? → rtl_internal_function ≝ 552 let insts_rest ≝ translate_cst globals (Ointconst I8 (zero ?)) destrs in 553 add_translates rtl_params1 globals [ inst_div; insts_rest ] start_lbl dest_lbl def 554 ]. 555 556 definition translate_ne: ∀globals: list ident. ? → ? → ? → ? → ? → ? → rtl_internal_function globals ≝ 557 λglobals: list ident. 555 558 λdestrs: list register. 556 559 λsrcrs1: list register. … … 558 561 λstart_lbl: label. 559 562 λdest_lbl: label. 560 λdef: rtl_internal_function .563 λdef: rtl_internal_function globals. 561 564 match destrs with 562 [ nil ⇒ add_graph start_lbl (rtl_st_skipdest_lbl) def565 [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def 563 566  cons destr destrs ⇒ 564 let 〈def, tmpr〉 ≝ fresh_reg def in565 let 〈def, tmp_zero〉 ≝ fresh_reg def in566 let 〈def, tmp_srcrs1〉 ≝ fresh_regs def (srcrs1) in567 let save_srcrs1 ≝ translate_move tmp_srcrs1 srcrs1 in568 let 〈def, tmp_srcrs2〉 ≝ fresh_regs def (srcrs2) in569 let save_srcrs2 ≝ translate_move tmp_srcrs2 srcrs2 in567 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 568 let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params0 globals def in 569 let 〈def, tmp_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (srcrs1) in 570 let save_srcrs1 ≝ translate_move globals tmp_srcrs1 srcrs1 in 571 let 〈def, tmp_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (srcrs2) in 572 let save_srcrs2 ≝ translate_move globals tmp_srcrs2 srcrs2 in 570 573 match reduce_strong register register tmp_srcrs1 tmp_srcrs2 with 571 574 [ dp crl their_proof ⇒ … … 576 579 let rest ≝ choose_rest ? restl restr ? ? in 577 580 let inits ≝ [ 578 rtl_st_int destr (zero ?) start_lbl;579 rtl_st_int tmp_zero (zero ?) start_lbl581 sequential … (INT rtl_params_ globals destr (zero …)); 582 sequential … (INT rtl_params_ globals tmp_zero (zero …)) 580 583 ] 581 584 in 582 585 let f_common ≝ λtmp_srcr1. λtmp_srcr2. [ 583 rtl_st_clear_carry start_lbl;584 rtl_st_op2 Sub tmpr tmp_srcr1 tmp_srcr2 start_lbl;585 rtl_st_op2 Or destr destr tmpr start_lbl586 sequential … (CLEAR_CARRY …); 587 sequential … (OP2 rtl_params_ globals Sub tmpr tmp_srcr1 tmp_srcr2); 588 sequential … (OP2 rtl_params_ globals Or destr destr tmpr) 586 589 ] 587 590 in 588 let insts_common ≝ flatten ?(map2 … f_common commonl commonr ?) in591 let insts_common ≝ flatten … (map2 … f_common commonl commonr ?) in 589 592 let f_rest ≝ λtmp_srcr. [ 590 rtl_st_clear_carry start_lbl;591 rtl_st_op2 Sub tmpr tmp_zero tmp_srcr start_lbl;592 rtl_st_op2 Or destr destr tmpr start_lbl593 sequential … (CLEAR_CARRY …); 594 sequential … (OP2 rtl_params_ globals Sub tmpr tmp_zero tmp_srcr); 595 sequential … (OP2 rtl_params_ globals Or destr destr tmpr) 593 596 ] 594 597 in 595 let insts_rest ≝ flatten ? (map ? ?f_rest rest) in598 let insts_rest ≝ flatten … (map … f_rest rest) in 596 599 let insts ≝ inits @ insts_common @ insts_rest in 597 let epilogue ≝ translate_cst (Ointconst I8 (zero ?)) destrs in598 add_translates [599 save_srcrs1; save_srcrs2; adds_graph insts; epilogue600 let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in 601 add_translates rtl_params1 globals [ 602 save_srcrs1; save_srcrs2; adds_graph rtl_params1 globals insts; epilogue 600 603 ] start_lbl dest_lbl def 601 604 ] … … 609 612 610 613 definition translate_eq_reg ≝ 614 λglobals: list ident. 611 615 λtmp_zero: register. 612 616 λtmp_one: register. … … 617 621 λsrcr12: register × register. 618 622 let 〈srcr1, srcr2〉 ≝ srcr12 in 619 [ rtl_st_clear_carry dummy_lbl;620 rtl_st_op2 Sub tmpr1 srcr1 srcr2 dummy_lbl;621 rtl_st_op2 Addc tmpr1 tmp_zero tmp_zero dummy_lbl;622 rtl_st_op2 Sub tmpr2 srcr2 srcr1 dummy_lbl;623 rtl_st_op2 Addc tmpr2 tmp_zero tmp_zero dummy_lbl;624 rtl_st_op2 Or tmpr1 tmpr1 tmpr2 dummy_lbl;625 rtl_st_op2 Xor tmpr1 tmpr1 tmp_one dummy_lbl;626 rtl_st_op2 And destr destr tmpr1 dummy_lbl].623 [ sequential … (CLEAR_CARRY …); 624 sequential rtl_params_ globals (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2); 625 sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero); 626 sequential … (OP2 rtl_params_ globals Sub tmpr2 srcr2 srcr1); 627 sequential … (OP2 rtl_params_ globals Addc tmpr2 tmp_zero tmp_zero); 628 sequential … (OP2 rtl_params_ globals Or tmpr1 tmpr1 tmpr2); 629 sequential … (OP2 rtl_params_ globals Xor tmpr1 tmpr1 tmp_one); 630 sequential … (OP2 rtl_params_ globals And destr destr tmpr1) ]. 627 631 628 632 definition translate_eq_list ≝ 633 λglobals: list ident. 629 634 λtmp_zero: register. 630 635 λtmp_one: register. … … 634 639 λleq: list (register × register). 635 640 λdummy_lbl: label. 636 let f ≝ translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in637 ( rtl_st_int destr (bitvector_of_nat ? 1) dummy_lbl) ::638 flatten ? (map ? ?f leq).641 let f ≝ translate_eq_reg globals tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in 642 (sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1))) :: 643 flatten … (map … f leq). 639 644 640 645 definition translate_atom ≝ 646 λglobals: list ident. 641 647 λtmp_zero: register. 642 648 λtmp_one: register. … … 649 655 λsrcr1: register. 650 656 λsrcr2: register. 651 translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl @652 [ rtl_st_clear_carry dummy_lbl;653 rtl_st_op2 Sub tmpr1 srcr1 srcr2 dummy_lbl;654 rtl_st_op2 Addc tmpr1 tmp_zero tmp_zero dummy_lbl;655 rtl_st_op2 And tmpr3 tmpr3 tmpr1 dummy_lbl;656 rtl_st_op2 Or destr destr tmpr3 dummy_lbl].657 translate_eq_list globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl @ 658 [ sequential … (CLEAR_CARRY …); 659 sequential … (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2); 660 sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero); 661 sequential … (OP2 rtl_params_ globals And tmpr3 tmpr3 tmpr1); 662 sequential … (OP2 rtl_params_ globals Or destr destr tmpr3) ]. 657 663 658 664 definition translate_lt_main ≝ 665 λglobals: list ident. 659 666 λtmp_zero: register. 660 667 λtmp_one: register. … … 669 676 let f ≝ λinsts_leq. λsrcr1. λsrcr2. 670 677 let 〈insts, leq〉 ≝ insts_leq in 671 let added_insts ≝ translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 in678 let added_insts ≝ translate_atom globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 in 672 679 〈insts @ added_insts, leq @ [〈srcr1, srcr2〉]〉 673 680 in 674 \fst (fold_left2 ? ? ?f 〈[ ], [ ]〉 srcrs1 srcrs2 proof).681 \fst (fold_left2 … f 〈[ ], [ ]〉 srcrs1 srcrs2 proof). 675 682 676 683 definition fresh_regs_strong: 677 rtl_internal_function → ∀n: nat. Σfresh: rtl_internal_function × (list register). \snd fresh = n ≝ 684 ∀globals. rtl_internal_function globals → ∀n: nat. Σfresh: (rtl_internal_function globals) × (list register). \snd fresh = n ≝ 685 λglobals: list ident. 678 686 λdef. 679 687 λn. 680 fresh_regs def n.688 fresh_regs rtl_params0 globals def n. 681 689 @fresh_regs_length 682 690 qed. 683 691 684 692 definition complete_regs_strong: 685 rtl_internal_function → list register → list register → Σcomplete: (list register) × (list register) × (list register). \fst (\fst complete) = \snd (\fst complete) ≝ 693 ∀globals: list ident. rtl_internal_function globals → list register → list register → Σcomplete: (list register) × (list register) × (list register). \fst (\fst complete) = \snd (\fst complete) ≝ 694 λglobals: list ident. 686 695 λdef. 687 696 λleft. 688 697 λright. 689 complete_regs def left right.698 complete_regs globals def left right. 690 699 @complete_regs_length 691 700 qed. 692 701 693 702 definition translate_lt ≝ 703 λglobals: list ident. 694 704 λdestrs: list register. 695 705 λprf_destrs: lt 0 (destrs). … … 698 708 λstart_lbl: label. 699 709 λdest_lbl: label. 700 λdef: rtl_internal_function .710 λdef: rtl_internal_function globals. 701 711 match destrs with 702 [ nil ⇒ add_graph start_lbl (rtl_st_skipdest_lbl) def712 [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def 703 713  _ ⇒ 704 match fresh_regs_strong def (destrs) with714 match fresh_regs_strong globals def (destrs) with 705 715 [ dp def_tmp_destrs tmp_destrs_proof ⇒ 706 716 let def ≝ \fst def_tmp_destrs in 707 717 let tmp_destrs ≝ \snd def_tmp_destrs in 708 718 let tmp_destr ≝ hd_safe ? tmp_destrs ? in 709 let 〈def, tmp_zero〉 ≝ fresh_reg def in710 let 〈def, tmp_one〉 ≝ fresh_reg def in711 let 〈def, tmpr1〉 ≝ fresh_reg def in712 let 〈def, tmpr2〉 ≝ fresh_reg def in713 let 〈def, tmpr3〉 ≝ fresh_reg def in714 match complete_regs_strong def srcrs1 srcrs2 with719 let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params1 globals def in 720 let 〈def, tmp_one〉 ≝ fresh_reg rtl_params1 globals def in 721 let 〈def, tmpr1〉 ≝ fresh_reg rtl_params1 globals def in 722 let 〈def, tmpr2〉 ≝ fresh_reg rtl_params1 globals def in 723 let 〈def, tmpr3〉 ≝ fresh_reg rtl_params1 globals def in 724 match complete_regs_strong globals def srcrs1 srcrs2 with 715 725 [ dp srcrs12_added srcrs12_proof ⇒ 716 726 let srcrs1 ≝ \fst (\fst srcrs12_added) in 717 727 let srcrs2 ≝ \snd (\fst srcrs12_added) in 718 728 let added ≝ \snd srcrs12_added in 719 let srcrs1' ≝ rev ?srcrs1 in720 let srcrs2' ≝ rev ?srcrs2 in729 let srcrs1' ≝ rev … srcrs1 in 730 let srcrs2' ≝ rev … srcrs2 in 721 731 let insts_init ≝ [ 722 translate_cst (Ointconst I8 (zero ?)) tmp_destrs;723 translate_cst (Ointconst I8 (zero ?)) added;724 adds_graph [725 rtl_st_int tmp_zero (zero ?) start_lbl;726 rtl_st_int tmp_one (bitvector_of_nat ? 1) start_lbl732 translate_cst globals (Ointconst I8 (zero ?)) tmp_destrs; 733 translate_cst globals (Ointconst I8 (zero ?)) added; 734 adds_graph rtl_params1 globals [ 735 sequential rtl_params_ globals (INT rtl_params_ globals tmp_zero (zero …)); 736 sequential rtl_params_ globals (INT rtl_params_ globals tmp_one (bitvector_of_nat … 1)) 727 737 ] 728 738 ] 729 739 in 730 740 let insts_main ≝ 731 translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl srcrs1' srcrs2' ? in732 let insts_main ≝ [ adds_graph insts_main ] in733 let insts_exit ≝ [ translate_move destrs tmp_destrs ] in734 add_translates (insts_init @ insts_main @ insts_exit) start_lbl dest_lbl def741 translate_lt_main globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl srcrs1' srcrs2' ? in 742 let insts_main ≝ [ adds_graph rtl_params1 globals insts_main ] in 743 let insts_exit ≝ [ translate_move globals destrs tmp_destrs ] in 744 add_translates rtl_params1 globals (insts_init @ insts_main @ insts_exit) start_lbl dest_lbl def 735 745 ] 736 746 ] … … 744 754 745 755 definition add_128_to_last ≝ 756 λglobals: list ident. 746 757 λtmp_128: register. 747 758 λrs. … … 749 760 λstart_lbl: label. 750 761 match rs with 751 [ nil ⇒ adds_graph [ ] start_lbl762 [ nil ⇒ adds_graph rtl_params1 globals [ ] start_lbl 752 763  _ ⇒ 753 let r ≝ last_safe ?rs prf in754 adds_graph [755 rtl_st_op2 Add r r tmp_128 start_lbl764 let r ≝ last_safe … rs prf in 765 adds_graph rtl_params1 globals [ 766 sequential rtl_params_ globals (OP2 rtl_params_ globals Add r r tmp_128) 756 767 ] start_lbl 757 768 ]. 758 769 759 770 definition translate_lts ≝ 771 λglobals: list ident. 760 772 λdestrs: list register. 761 773 λdestrs_prf: lt 0 (destrs). … … 766 778 λstart_lbl: label. 767 779 λdest_lbl: label. 768 λdef: rtl_internal_function .769 match fresh_regs_strong def (srcrs1) with780 λdef: rtl_internal_function globals. 781 match fresh_regs_strong globals def (srcrs1) with 770 782 [ dp def_tmp_srcrs1 srcrs1_prf ⇒ 771 783 let def ≝ \fst def_tmp_srcrs1 in 772 784 let tmp_srcrs1 ≝ \snd def_tmp_srcrs1 in 773 match fresh_regs_strong def (srcrs2) with785 match fresh_regs_strong globals def (srcrs2) with 774 786 [ dp def_tmp_srcrs2 srcrs2_prf ⇒ 775 787 let def ≝ \fst def_tmp_srcrs2 in 776 788 let tmp_srcrs2 ≝ \snd def_tmp_srcrs2 in 777 let 〈def, tmp_128〉 ≝ fresh_reg def in778 add_translates [779 translate_move tmp_srcrs1 srcrs1;780 translate_move tmp_srcrs2 srcrs2;781 adds_graph [782 rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl789 let 〈def, tmp_128〉 ≝ fresh_reg rtl_params0 globals def in 790 add_translates rtl_params1 globals [ 791 translate_move globals tmp_srcrs1 srcrs1; 792 translate_move globals tmp_srcrs2 srcrs2; 793 adds_graph rtl_params1 globals [ 794 sequential rtl_params_ globals (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128)) 783 795 ]; 784 add_128_to_last tmp_128 tmp_srcrs1 ?;785 add_128_to_last tmp_128 tmp_srcrs2 ?;786 translate_lt destrs destrs_prf tmp_srcrs1 tmp_srcrs2796 add_128_to_last globals tmp_128 tmp_srcrs1 ?; 797 add_128_to_last globals tmp_128 tmp_srcrs2 ?; 798 translate_lt globals destrs destrs_prf tmp_srcrs1 tmp_srcrs2 787 799 ] start_lbl dest_lbl def 788 800 ]
Note: See TracChangeset
for help on using the changeset viewer.