Changeset 1045 for src/RTLabs
 Timestamp:
 Jun 29, 2011, 10:47:39 AM (9 years ago)
 Location:
 src/RTLabs
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r799 r1045 27 27 match fresh LabelTag (rtl_if_luniverse def) with 28 28 [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ) 29  Error ⇒ None ?29  Error _ ⇒ None ? 30 30 ]. 31 31 … … 917 917 ]. 918 918 919 axiom translate_op2: 920 op2 → list register → list register → list register → label → label → rtl_internal_function → option rtl_internal_function. 921 919 922 definition translate_cond2 ≝ 920 923 λop2. … … 926 929 λdef. 927 930 match op2 with 931 [ op_cmp cmp ⇒ 932 match cmp with 933 [ Compare_Equal ⇒ 934 let srcr1 ≝ extract_singleton ? srcrs1 in 935 match srcr1 with 936 [ None ⇒ None ? 937  Some srcr1 ⇒ 938 let srcr2 ≝ extract_singleton ? srcrs2 in 939 match srcr2 with 940 [ None ⇒ None ? 941  Some srcr2 ⇒ 942 let 〈def, tmpr〉 ≝ fresh_reg def in 943 adds_graph [ 944 rtl_st_clear_carry start_lbl; 945 rtl_st_op2 Sub tmpr srcr1 srcr2 start_lbl; 946 rtl_st_cond_acc tmpr lbl_false lbl_true 947 ] start_lbl start_lbl def 948 ] 949 ] 950  _ ⇒ 951 let n ≝ length ? srcrs1 + length ? srcrs2 in 952 match size_of_op2_ret n op2 with 953 [ None ⇒ None ? 954  Some size ⇒ 955 let 〈def, destrs〉 ≝ fresh_regs def size in 956 let lbl ≝ fresh_label def in 957 match lbl with 958 [ None ⇒ None ? 959  Some lbl ⇒ 960 match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with 961 [ None ⇒ None ? 962  Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def 963 ] 964 ] 965 ] 966 ] 967  _ ⇒ 968 let n ≝ length ? srcrs1 + length ? srcrs2 in 969 match size_of_op2_ret n op2 with 970 [ None ⇒ None ? 971  Some size ⇒ 972 let 〈def, destrs〉 ≝ fresh_regs def size in 973 let lbl ≝ fresh_label def in 974 match lbl with 975 [ None ⇒ None ? 976  Some lbl ⇒ 977 match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with 978 [ None ⇒ None ? 979  Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def 980 ] 981 ] 982 ] 983 ]. 984 985 let rec addressing_pointer (mode: ?) (args: ?) (destr1: ?) 986 (destr2: ?) (start_lbl: label) 987 (dest_lbl: label) (def: rtl_internal_function) ≝ 988 let destrs ≝ [ destr1; destr2 ] in 989 match mode with 990 [ Aindexed off ⇒ 991 let srcr12 ≝ extract_singleton ? args in 992 match srcr12 with 993 [ None ⇒ None ? 994  Some srcr12 ⇒ 995 let srcr12 ≝ extract_pair ? srcr12 in 996 match srcr12 with 997 [ None ⇒ None ? 998  Some srcr12 ⇒ 999 let 〈srcr1, srcr2〉 ≝ srcr12 in 1000 let 〈def, tmpr〉 ≝ fresh_reg def in 1001 add_translates [ 1002 adds_graph [ 1003 rtl_st_int tmpr off start_lbl 1004 ]; 1005 translate_op2 op_addp destrs [ srcr1 ; srcr2 ] [tmpr] 1006 ] start_lbl dest_lbl def 1007 ] 1008 ] 1009  Aindexed2 ⇒ 1010 let args_pair ≝ extract_pair ? args in 1011 match args_pair with 1012 [ None ⇒ None ? 1013  Some args_pair ⇒ 1014 let 〈lft, rgt〉 ≝ args_pair in 1015 let srcr1112 ≝ extract_pair ? lft in 1016 let srcr2 ≝ extract_singleton ? rgt in 1017 match srcr1112 with 1018 [ None ⇒ 1019 let srcr2 ≝ extract_singleton ? rgt in 1020 let srcr1112 ≝ extract_pair ? lft in 1021 match srcr2 with 1022 [ None ⇒ None ? 1023  Some srcr2 ⇒ 1024 match srcr1112 with 1025 [ None ⇒ None ? 1026  Some srcr1112 ⇒ 1027 let 〈srcr11, srcr12〉 ≝ srcr1112 in 1028 translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def 1029 ] 1030 ] 1031  Some srcr1112 ⇒ 1032 let 〈srcr11, srcr12〉 ≝ srcr1112 in 1033 match srcr2 with 1034 [ None ⇒ None ? 1035  Some srcr2 ⇒ 1036 translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def 1037 ] 1038 ] 1039 ] 1040  Aglobal x off ⇒ 1041 let 〈def, tmpr〉 ≝ fresh_reg def in 1042 add_translates [ 1043 adds_graph [ 1044 rtl_st_int tmpr off start_lbl; 1045 rtl_st_addr destr1 destr2 x start_lbl 1046 ]; 1047 translate_op2 op_addp destrs destrs [ tmpr ] 1048 ] start_lbl dest_lbl def 1049  Abased x off ⇒ 1050 let srcrs ≝ extract_singleton ? args in 1051 match srcrs with 1052 [ None ⇒ None ? 1053  Some srcrs ⇒ 1054 let 〈def, tmpr1〉 ≝ fresh_reg def in 1055 let 〈def, tmpr2〉 ≝ fresh_reg def in 1056 (* mode, args, destr1, destr2, start_lbl, dest_lbl, def *) 1057 (* addressing_pointer (Aglobal x off) [ ] tmpr1 tmpr2; *) 1058 let address_unfold ≝ 1059 let 〈def, tmpr〉 ≝ fresh_reg def in 1060 add_translates [ 1061 adds_graph [ 1062 rtl_st_int tmpr off start_lbl; 1063 rtl_st_addr tmpr1 tmpr2 x start_lbl 1064 ]; 1065 translate_op2 op_addp destrs destrs [ tmpr ] 1066 ] 1067 in 1068 add_translates [ 1069 address_unfold; 1070 translate_op2 op_addp destrs [ tmpr1; tmpr2 ] srcrs 1071 ] start_lbl dest_lbl def 1072 ] 1073  Ainstack off ⇒ 1074 let 〈def, tmpr〉 ≝ fresh_reg def in 1075 add_translates [ 1076 adds_graph [ 1077 rtl_st_int tmpr off start_lbl; 1078 rtl_st_stack_addr destr1 destr2 start_lbl 1079 ]; 1080 translate_op2 op_addp destrs destrs [ tmpr ] 1081 ] start_lbl dest_lbl def 1082  _ ⇒ None ? (* wrong number of arguments *) 1083 ]. 1084 1085 definition translate_load ≝ 1086 λq. 1087 λmode. 1088 λargs. 1089 λdestrs. 1090 λstart_lbl: label. 1091 λdest_lbl: label. 1092 λdef. 1093 match q with 928 1094 [ 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] > 1095 ]. 1096 1097 let translate_load q mode args destrs start_lbl dest_lbl def = 1098 match q, destrs with 1099 1100  Memory.QInt 1, [destr] > 1101 let (def, addr1) = fresh_reg def in 1102 let (def, addr2) = fresh_reg def in 1103 add_translates 1104 [addressing_pointer mode args addr1 addr2 ; 1105 adds_graph [RTL.St_load (destr, addr1, addr2, start_lbl)]] 1106 start_lbl dest_lbl def 1107 1108  Memory.QPtr, [destr1 ; destr2] > 1109 let (def, addr1) = fresh_reg def in 1110 let (def, addr2) = fresh_reg def in 1111 let addr = [addr1 ; addr2] in 935 1112 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 1113 add_translates 1114 [addressing_pointer mode args addr1 addr2 ; 1115 adds_graph [RTL.St_load (destr1, addr1, addr2, start_lbl) ; 1116 RTL.St_int (tmpr, 1, start_lbl)] ; 1117 translate_op2 AST.Op_addp addr addr [tmpr] ; 1118 adds_graph [RTL.St_load (destr2, addr1, addr2, start_lbl)]] 1119 start_lbl dest_lbl def 1120 1121  _ > error "Size error in load." 
src/RTLabs/syntax.ma
r888 r1045 10 10 include "common/Graphs.ma". 11 11 12 (* Statements, including the label of successor(s). *) 12 definition immediate : Type[0] ≝ Byte. 13 14 (* Addressing modes *) 15 16 inductive addressing : Type[0] ≝ 17 (* dpm: changed from int to Byte *) 18  Aindexed : immediate → addressing (* r1 + offset *) 19  Aindexed2 : addressing (* r1 + r2 *) 20  Aglobal : ident → immediate → addressing (* global + offset *) 21  Abased : ident → immediate → addressing (* global + offset + r1 *) 22  Ainstack : immediate → addressing (* stack + offset *) 23 . 24 25 definition addr_mode_args : addressing → nat ≝ 26 λa. match a with 27 [ Aindexed _ ⇒ 1 28  Aindexed2 ⇒ 2 29  Aglobal _ _ ⇒ 0 30  Abased _ _ ⇒ 1 31  Ainstack _ ⇒ 0 32 ]. 33 34 definition addr ≝ λm.Vector register (addr_mode_args m). 13 35 14 36 inductive statement : Type[0] ≝
Note: See TracChangeset
for help on using the changeset viewer.