- Timestamp:
- May 13, 2011, 12:29:06 PM (10 years ago)
- Location:
- src
- Files:
-
- 2 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, _, _, _ -
src/common/AST.ma
r793 r795 517 517 inductive Compare: Type[0] ≝ 518 518 Compare_Equal: Compare 519 | Compare_NotEqual: Compare 519 520 | Compare_Less: Compare 520 521 | Compare_Greater: Compare
Note: See TracChangeset
for help on using the changeset viewer.