Changeset 799 for src/RTLabs/RTLAbstoRTL.ma
 Timestamp:
 May 13, 2011, 5:35:04 PM (9 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.