- Timestamp:
- May 13, 2011, 5:35:04 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLAbstoRTL.ma
r795 r799 417 417 ] start_lbl start_lbl def. 418 418 419 (* 419 420 let rec translate_op2 (op2: ?) (destrs: ?) (srcrs1: ?) (srcrs2: ?) 420 421 (start_lbl: label) (dest_lbl: label) (def: ?) on op2 ≝ … … 693 694 | Compare_NotEqual ⇒ 694 695 translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def 696 | Compare 695 697 | _ ⇒ None ? 696 698 ] 697 699 | _ ⇒ ? 698 700 ]. 699 700 | AST.Op_cmp AST.Cmp_ne, _, _, _701 | AST.Op_cmpu AST.Cmp_ne, _, _, _ ->702 translate_op2 AST.Op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def703 701 704 702 | AST.Op_cmpu AST.Cmp_lt, [destr], [srcr1], [srcr2] -> … … 776 774 777 775 | _ -> assert false (* wrong number of arguments *) 776 *) 777 778 definition translate_condcst ≝ 779 λcst. 780 λstart_lbl: label. 781 λlbl_true: label. 782 λlbl_false: label. 783 λdef. 784 match cst with 785 [ cast_int i ⇒ 786 let 〈def, tmpr〉 ≝ fresh_reg def in 787 adds_graph [ 788 rtl_st_int tmpr i start_lbl; 789 rtl_st_cond_acc tmpr lbl_true lbl_false 790 ] start_lbl start_lbl def 791 | cast_addr_symbol x ⇒ 792 let 〈def, r1〉 ≝ fresh_reg def in 793 let 〈def, r2〉 ≝ fresh_reg def in 794 let lbl ≝ fresh_label def in 795 match lbl with 796 [ None ⇒ None ? 797 | Some lbl ⇒ 798 let def ≝ add_graph start_lbl (rtl_st_addr r1 r2 x lbl) def in 799 translate_condptr r1 r2 lbl lbl_true lbl_false def 800 ] 801 | cast_stack_offset off ⇒ 802 let 〈def, r1〉 ≝ fresh_reg def in 803 let 〈def, r2〉 ≝ fresh_reg def in 804 let tmp_lbl ≝ fresh_label def in 805 match tmp_lbl with 806 [ None ⇒ None ? 807 | Some tmp_lbl ⇒ 808 let def ≝ translate_cst (cast_stack_offset off) [r1; r2] start_lbl tmp_lbl def in 809 match def with 810 [ None ⇒ None ? 811 | Some def ⇒ translate_condptr r1 r2 tmp_lbl lbl_true lbl_false def 812 ] 813 ] 814 | cast_float f ⇒ None ? (* error_float *) 815 ]. 816 817 definition size_of_op1_ret ≝ 818 λop. 819 match op with 820 [ op_cast8_unsigned ⇒ Some ? 1 821 | op_cast8_signed ⇒ Some ? 1 822 | op_cast16_unsigned ⇒ Some ? 1 823 | op_cast16_signed ⇒ Some ? 1 824 | op_neg_int ⇒ Some ? 1 825 | op_not_int ⇒ Some ? 1 826 | op_int_of_ptr ⇒ Some ? 1 827 | op_ptr_of_int ⇒ Some ? 2 828 | op_id ⇒ None ? (* invalid_argument *) 829 | _ ⇒ None ? (* error_float *) 830 ]. 831 832 definition translate_cond1 ≝ 833 λop1. 834 λsrcrs: list register. 835 λstart_lbl: label. 836 λlbl_true: label. 837 λlbl_false: label. 838 λdef. 839 match op1 with 840 [ op_id ⇒ 841 let srcr ≝ extract_singleton ? srcrs in 842 match srcr with 843 [ None ⇒ 844 let srcr12 ≝ extract_pair ? srcrs in 845 match srcr12 with 846 [ None ⇒ None ? 847 | Some srcr12 ⇒ 848 let 〈srcr1, srcr2〉 ≝ srcr12 in 849 translate_condptr srcr1 srcr2 start_lbl lbl_true lbl_false def 850 ] 851 | Some srcr ⇒ 852 adds_graph [ 853 rtl_st_cond_acc srcr lbl_true lbl_false 854 ] start_lbl start_lbl def 855 ] 856 | _ ⇒ 857 let size ≝ size_of_op1_ret op1 in 858 match size with 859 [ None ⇒ None ? 860 | Some size ⇒ 861 let 〈def, destrs〉 ≝ fresh_regs def size in 862 let lbl ≝ fresh_label def in 863 match lbl with 864 [ None ⇒ None ? 865 | Some lbl ⇒ 866 let def ≝ translate_op1 op1 destrs srcrs start_lbl lbl def in 867 match def with 868 [ None ⇒ None ? 869 | Some def ⇒ 870 let destr ≝ extract_singleton ? destrs in 871 match destr with 872 [ None ⇒ 873 let destr12 ≝ extract_pair ? destrs in 874 match destr12 with 875 [ None ⇒ None ? 876 | Some destr12 ⇒ 877 let 〈destr1, destr2〉 ≝ destr12 in 878 translate_condptr destr1 destr2 start_lbl lbl_true lbl_false def 879 ] 880 | Some destr ⇒ 881 adds_graph [ 882 rtl_st_cond_acc destr lbl_true lbl_false 883 ] start_lbl start_lbl def 884 ] 885 ] 886 ] 887 ] 888 ]. 889 890 definition size_of_op2_ret ≝ 891 λn: nat. 892 λop2. 893 match op2 with 894 [ op_add ⇒ Some ? 1 895 | op_sub ⇒ Some ? 1 896 | op_mul ⇒ Some ? 1 897 | op_div ⇒ Some ? 1 898 | op_divu ⇒ Some ? 1 899 | op_mod ⇒ Some ? 1 900 | op_modu ⇒ Some ? 1 901 | op_and ⇒ Some ? 1 902 | op_or ⇒ Some ? 1 903 | op_xor ⇒ Some ? 1 904 | op_shl ⇒ Some ? 1 905 | op_shr ⇒ Some ? 1 906 | op_shru ⇒ Some ? 1 907 | op_cmp _ ⇒ Some ? 1 908 | op_cmpu _ ⇒ Some ? 1 909 | op_cmpp _ ⇒ Some ? 1 910 | op_addp ⇒ Some ? 2 911 | op_subp ⇒ 912 if eq_nat n 4 then 913 Some ? 1 914 else 915 Some ? 2 916 | _ ⇒ None ? (* error_float *) 917 ]. 918 919 definition translate_cond2 ≝ 920 λop2. 921 λsrcrs1: list register. 922 λsrcrs2: list register. 923 λstart_lbl: label. 924 λlbl_true: label. 925 λlbl_false: label. 926 λdef. 927 match op2 with 928 [ 929 ] 930 931 let translate_cond2 op2 srcrs1 srcrs2 start_lbl lbl_true lbl_false def = 932 match op2, srcrs1, srcrs2 with 933 934 | AST.Op_cmp AST.Cmp_eq, [srcr1], [srcr2] -> 935 let (def, tmpr) = fresh_reg def in 936 adds_graph 937 [RTL.St_clear_carry start_lbl ; 938 RTL.St_op2 (I8051.Sub, tmpr, srcr1, srcr2, start_lbl) ; 939 RTL.St_condacc (tmpr, lbl_false, lbl_true)] 940 start_lbl start_lbl def 941 942 | _, _, _ -> 943 let n = (List.length srcrs1) + (List.length srcrs2) in 944 let (def, destrs) = fresh_regs def (size_of_op2_ret n op2) in 945 let lbl = fresh_label def in 946 let def = translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def in 947 translate_cond1 AST.Op_id destrs lbl lbl_true lbl_false def
Note: See TracChangeset
for help on using the changeset viewer.