Changeset 795 for src/RTLabs/RTLAbstoRTL.ma
 Timestamp:
 May 13, 2011, 12:29:06 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r793 r795 177 177 ]. 178 178 179 (* dpm: had to lift this into option *) 179 180 let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label) 180 181 (def: ?) on translate_list ≝ … … 183 184  cons hd tl ⇒ 184 185 match tl with 185 [ nil ⇒ Some ? (hd start_lbl dest_lbl def)186 [ nil ⇒ hd start_lbl dest_lbl def 186 187  cons hd' tl' ⇒ 187 188 let tmp_lbl ≝ fresh_label def in … … 189 190 [ None ⇒ None ? 190 191  Some tmp_lbl ⇒ 191 let def ≝ hd start_lbl tmp_lbl def in 192 add_translates tl tmp_lbl dest_lbl def 192 match hd start_lbl tmp_lbl def with 193 [ None ⇒ None ? 194  Some def ⇒ add_translates tl tmp_lbl dest_lbl def 195 ] 193 196 ] 194 197 ] … … 580 583  op_divf ⇒ None ? 581 584  op_cmpf _ ⇒ None ? 582  op_addp ⇒ ? 585  op_addp ⇒ 586 let destr12 ≝ extract_pair ? destrs in 587 match destr12 with 588 [ None ⇒ None ? 589  Some destr12 ⇒ 590 let 〈destr1, destr2〉 ≝ destr12 in 591 let srcr12 ≝ extract_pair ? srcrs1 in 592 match srcr12 with 593 [ None ⇒ 594 let srcr2 ≝ extract_singleton ? srcrs1 in 595 match srcr2 with 596 [ None ⇒ None ? 597  Some srcr2 ⇒ 598 let srcr12 ≝ extract_pair ? srcrs2 in 599 match srcr12 with 600 [ None ⇒ None ? 601  Some srcr12 ⇒ 602 let 〈srcr11, srcr12〉 ≝ srcr12 in 603 let 〈def, tmpr1〉 ≝ fresh_reg def in 604 let 〈def, tmpr2〉 ≝ fresh_reg def in 605 adds_graph [ 606 rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl; 607 rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl; 608 rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl; 609 rtl_st_move destr1 tmpr1 start_lbl 610 ] start_lbl dest_lbl def 611 ] 612 ] 613  Some srcr12 ⇒ 614 let 〈srcr11, srcr12〉 ≝ srcr12 in 615 let srcr2 ≝ extract_singleton ? srcrs2 in 616 match srcr2 with 617 [ None ⇒ None ? 618  Some srcr2 ⇒ 619 let 〈def, tmpr1〉 ≝ fresh_reg def in 620 let 〈def, tmpr2〉 ≝ fresh_reg def in 621 adds_graph [ 622 rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl; 623 rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl; 624 rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl; 625 rtl_st_move destr1 tmpr1 start_lbl 626 ] start_lbl dest_lbl def 627 ] 628 ] 629 ] 630  op_subp ⇒ 631 let destr ≝ extract_singleton ? destrs in 632 match destr with 633 [ None ⇒ 634 let destr12 ≝ extract_pair ? destrs in 635 match destr12 with 636 [ None ⇒ None ? 637  Some destr12 ⇒ 638 let 〈destr1, destr2〉 ≝ destr12 in 639 let srcr12 ≝ extract_pair ? srcrs1 in 640 match srcr12 with 641 [ None ⇒ None ? 642  Some srcr12 ⇒ 643 let 〈srcr11, srcr12〉 ≝ srcr12 in 644 let srcr2 ≝ extract_singleton ? srcrs2 in 645 match srcr2 with 646 [ None ⇒ None ? 647  Some srcr2 ⇒ 648 adds_graph [ 649 rtl_st_clear_carry start_lbl; 650 rtl_st_op2 Sub destr1 srcr11 srcr2 start_lbl; 651 rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl; 652 rtl_st_op2 Sub destr2 srcr12 destr2 start_lbl 653 ] start_lbl dest_lbl def 654 ] 655 ] 656 ] 657  Some destr ⇒ 658 match srcrs1 with 659 [ nil ⇒ None ? 660  cons srcr1 tl ⇒ 661 match srcrs2 with 662 [ nil ⇒ None ? 663  cons srcr2 tl' ⇒ 664 let 〈def, tmpr1〉 ≝ fresh_reg def in 665 let 〈def, tmpr2〉 ≝ fresh_reg def in 666 adds_graph [ 667 rtl_st_op1 Cmpl tmpr1 srcr2 start_lbl; 668 rtl_st_int tmpr2 (bitvector_of_nat ? 1) start_lbl; 669 rtl_st_op2 Add tmpr1 tmpr1 tmpr2 start_lbl; 670 rtl_st_op2 Add destr srcr1 tmpr1 start_lbl 671 ] start_lbl dest_lbl def 672 ] 673 ] 674 ] 675  op_cmp cmp ⇒ 676 match cmp with 677 [ Compare_Equal ⇒ 678 add_translates [ 679 translate_op2 op_sub destrs srcrs1 srcrs2; 680 translate_op1 op_not_bool destrs destrs 681 ] start_lbl dest_lbl def 682  Compare_NotEqual ⇒ 683 translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def 684  _ ⇒ None ? 685 ] 686  op_cmpu cmp ⇒ 687 match cmp with 688 [ Compare_Equal ⇒ 689 add_translates [ 690 translate_op2 op_sub destrs srcrs1 srcrs2; 691 translate_op1 op_not_bool destrs destrs 692 ] start_lbl dest_lbl def 693  Compare_NotEqual ⇒ 694 translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def 695  _ ⇒ None ? 696 ] 583 697  _ ⇒ ? 584 698 ]. 585 586  AST.Op_addp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2]587  AST.Op_addp, [destr1 ; destr2], [srcr2], [srcr11 ; srcr12] >588 let (def, tmpr1) = fresh_reg def in589 let (def, tmpr2) = fresh_reg def in590 adds_graph591 [RTL.St_op2 (I8051.Add, tmpr1, srcr11, srcr2, start_lbl) ;592 RTL.St_int (tmpr2, 0, start_lbl) ;593 RTL.St_op2 (I8051.Addc, destr2, tmpr2, srcr12, start_lbl) ;594 RTL.St_move (destr1, tmpr1, start_lbl)]595 start_lbl dest_lbl def596 597  AST.Op_subp, [destr], [srcr1 ; _], [srcr2 ; _] >598 let (def, tmpr1) = fresh_reg def in599 let (def, tmpr2) = fresh_reg def in600 adds_graph601 [RTL.St_op1 (I8051.Cmpl, tmpr1, srcr2, start_lbl) ;602 RTL.St_int (tmpr2, 1, start_lbl) ;603 RTL.St_op2 (I8051.Add, tmpr1, tmpr1, tmpr2, start_lbl) ;604 RTL.St_op2 (I8051.Add, destr, srcr1, tmpr1, start_lbl)]605 start_lbl dest_lbl def606 607  AST.Op_subp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2] >608 adds_graph609 [RTL.St_clear_carry start_lbl ;610 RTL.St_op2 (I8051.Sub, destr1, srcr11, srcr2, start_lbl) ;611 RTL.St_int (destr2, 0, start_lbl) ;612 RTL.St_op2 (I8051.Sub, destr2, srcr12, destr2, start_lbl)]613 start_lbl dest_lbl def614 615  AST.Op_cmp AST.Cmp_eq, _, _, _616  AST.Op_cmpu AST.Cmp_eq, _, _, _ >617 add_translates618 [translate_op2 AST.Op_sub destrs srcrs1 srcrs2 ;619 translate_op1 AST.Op_notbool destrs destrs]620 start_lbl dest_lbl def621 699 622 700  AST.Op_cmp AST.Cmp_ne, _, _, _
Note: See TracChangeset
for help on using the changeset viewer.