Changeset 1066 for src/RTLabs
- Timestamp:
- Jul 13, 2011, 5:12:10 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLAbstoRTL.ma
r1064 r1066 204 204 λA. 205 205 λlst: list A. 206 λprf: length A lst = 2. (* do not use on arguments other than those of length 2 *)207 match lst return λx. length A x = 2→ A × A with206 λprf: 2 ≤ length A lst. 207 match lst return λx. 2 ≤ |x| → A × A with 208 208 [ nil ⇒ λlst_nil_prf. ? 209 209 | cons hd tl ⇒ λprf. 210 match tl return λx. length A x = 1→ A × A with210 match tl return λx. 1 ≤ |x| → A × A with 211 211 [ nil ⇒ λtl_nil_prf. ? 212 212 | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉 … … 214 214 ] prf. 215 215 [1: normalize in lst_nil_prf; 216 destruct(lst_nil_prf); 216 cases(not_le_Sn_O 1); 217 #HYP cases(HYP lst_nil_prf) 217 218 |2: normalize in prf; 218 destruct(prf)219 @e0219 @le_S_S_to_le 220 assumption 220 221 |3: normalize in tl_nil_prf; 221 destruct(tl_nil_prf); 222 cases(not_le_Sn_O 0) 223 #HYP cases(HYP tl_nil_prf) 222 224 ] 223 225 qed. … … 253 255 | rtl_st_tailcall_id f a ⇒ rtl_st_tailcall_id f a 254 256 | rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a 255 | rtl_st_cond _acc r l1 l2 ⇒ rtl_st_cond_accr l1 l2257 | rtl_st_cond r l1 l2 ⇒ rtl_st_cond r l1 l2 256 258 | rtl_st_clear_carry l ⇒ rtl_st_clear_carry lbl 257 259 | rtl_st_set_carry l ⇒ rtl_st_set_carry lbl … … 394 396 λdestrs. 395 397 λsrcrs. 396 match | srcrs | return λx. | srcrs| = x → ? with398 match |srcrs| return λx. |srcrs| = x → ? with 397 399 [ O ⇒ λzero_prf. adds_graph [ ] 398 400 | S n' ⇒ λsucc_prf. … … 466 468 ]. 467 469 470 (* TODO: examine this properly. This is a change from the O'caml code due 471 to us dropping the explicit use of a cast destination size field. We 472 instead infer the size of the cast's destination from the context. Is 473 this correct? 474 *) 468 475 definition translate_op1 ≝ 469 λop1: op1.476 λop1: unary_operation. 470 477 λdestrs: list register. 471 478 λsrcrs: list register. … … 475 482 λdef: rtl_internal_function. 476 483 match op1 with 477 [ op_cast src_size src_sign dest_size ⇒ 484 [ Ocastint src_sign src_size ⇒ 485 let dest_size ≝ |destrs| * 8 in 486 let src_size ≝ bitsize_of_intsize src_size in 478 487 translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def 479 | op_neg_int ⇒488 | Onegint ⇒ 480 489 translate_negint destrs srcrs start_lbl dest_lbl def prf 481 | op_not_bool ⇒490 | Onotbool ⇒ 482 491 translate_notbool destrs srcrs start_lbl dest_lbl def 483 | op_not_int ⇒492 | Onotint ⇒ 484 493 let f ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in 485 494 let l ≝ map2 … f destrs srcrs prf in 486 495 adds_graph l start_lbl dest_lbl def 487 | op_ptr_of_int⇒496 | Optrofint r ⇒ 488 497 translate_move destrs srcrs start_lbl dest_lbl def 489 | op_int_of_ptr ⇒498 | Ointofptr r ⇒ 490 499 translate_move destrs srcrs start_lbl dest_lbl def 491 | op_id ⇒500 | Oid ⇒ 492 501 translate_move destrs srcrs start_lbl dest_lbl def 493 ]. 502 | _ ⇒ ? (* float operations implemented in runtime *) 503 ]. 504 cases not_implemented 505 qed. 494 506 495 507 definition translate_op ≝ … … 498 510 λsrcrs1. 499 511 λsrcrs2. 500 λprf: |srcrs1| = |srcrs2|.501 512 λstart_lbl. 502 513 λdest_lbl. … … 533 544 ] 534 545 ]. 535 cases not_implemented (* problem here with lengths of lists: possible bug? *) 546 [1: @third_reduced_proof 547 |3: @first_reduced_proof 548 |*: cases daemon (* TODO *) 549 ] 536 550 qed. 537 551 … … 597 611 λdestrs: list register. 598 612 λtmp_destrs: list register. 599 λdestrs_prf: |destrs| = |tmp_destrs|.600 613 λsrcrs1: list register. 601 614 λdummy_lbl: label. … … 618 631 rtl_st_clear_carry dummy_lbl 619 632 ]; 620 translate_op Addc destrs destrs tmp_destrs destrs_prf633 translate_op Addc destrs destrs tmp_destrs 621 634 ] 622 635 ] … … 822 835 λsrcrs1: list register. 823 836 λsrcrs2: list register. 824 λprf_srcrs: |srcrs1| = |srcrs2|.825 837 λstart_lbl: label. 826 838 λdest_lbl: label. … … 889 901 λsrcrs1: list register. 890 902 λsrcrs2: list register. 891 λsrcrs_prf: |srcrs1| = |srcrs2|.892 903 λsrcrs1_lt_prf: 0 < |srcrs1|. 904 λsrcrs2_lt_prf: 0 < |srcrs2|. 893 905 λstart_lbl: label. 894 906 λdest_lbl: label. … … 911 923 add_128_to_last tmp_128 tmp_srcrs1 ?; 912 924 add_128_to_last tmp_128 tmp_srcrs2 ?; 913 translate_lt destrs destrs_prf tmp_srcrs1 tmp_srcrs2 ?925 translate_lt destrs destrs_prf tmp_srcrs1 tmp_srcrs2 914 926 ] start_lbl dest_lbl def 915 927 ] 916 928 ]. 917 [2: >srcrs2_prf >srcrs1_prf @srcrs_prf 918 |3: >srcrs2_prf <srcrs_prf @srcrs1_lt_prf 919 |1: >srcrs1_prf @srcrs1_lt_prf 929 [1: >srcrs1_prf @srcrs1_lt_prf 930 |2: >srcrs2_prf @srcrs2_lt_prf 920 931 ] 921 932 qed. … … 927 938 λsrcrs1: list register. 928 939 λsrcrs2: list register. 929 λsrcrs_prf: |srcrs1| = |srcrs2|. 940 λsrcrs1_prf: lt 0 (|srcrs1|). (* can this be relaxed? i think it can 941 but we need more dep. typ. in modu/divu 942 cases *) 943 λsrcrs2_prf: lt 0 (|srcrs2|). 930 944 λstart_lbl: label. 931 945 λdest_lbl: label. 932 946 λdef: rtl_internal_function. 933 947 match op2 with 934 [ op_add ⇒ 935 translate_op Addc destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def 936 | op_addp ⇒ 937 translate_op Addc destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def 938 | op_sub ⇒ 939 translate_op Sub destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def 940 | op_subp ⇒ 941 translate_op Sub destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def 942 | op_subpp ⇒ 943 translate_op Sub destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def 944 | op_mul ⇒ 945 translate_op Mul destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def 946 | op_divu ⇒ ? 947 | op_modu ⇒ ? 948 | op_and ⇒ 949 translate_op And destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def 950 | op_or ⇒ 951 translate_op Or destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def 952 | op_xor ⇒ 953 translate_op Xor destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def 954 | op_cmp c ⇒ 948 [ Oadd ⇒ 949 translate_op Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def 950 | Oaddp ⇒ 951 translate_op Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def 952 | Osub ⇒ 953 translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def 954 | Osubpi ⇒ 955 translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def 956 | Osubpp sz ⇒ 957 translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def 958 | Omul ⇒ 959 translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def 960 | Odivu ⇒ 961 match srcrs1 return λx. 0 < |x| → rtl_internal_function with 962 [ cons hd tl ⇒ λcons_prf. 963 match tl with 964 [ nil ⇒ translate_divumodu8 true destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def 965 | _ ⇒ ? (* not implemented *) 966 ] 967 | nil ⇒ λnil_absrd. ? 968 ] srcrs1_prf 969 | Omodu ⇒ 970 match srcrs1 return λx. 0 < |x| → rtl_internal_function with 971 [ cons hd tl ⇒ λcons_prf. 972 match tl with 973 [ nil ⇒ translate_divumodu8 false destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def 974 | _ ⇒ ? (* not implemented *) 975 ] 976 | nil ⇒ λnil_absrd. ? 977 ] srcrs1_prf 978 | Oand ⇒ 979 translate_op And destrs srcrs1 srcrs2 start_lbl dest_lbl def 980 | Oor ⇒ 981 translate_op Or destrs srcrs1 srcrs2 start_lbl dest_lbl def 982 | Oxor ⇒ 983 translate_op Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def 984 | Ocmp c ⇒ 955 985 match c with 956 [ C ompare_Equal⇒986 [ Ceq ⇒ 957 987 add_translates [ 958 translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def;959 translate_op1 op_not_bool destrs destrs (refl ? (|destrs|))988 translate_ne destrs srcrs1 srcrs2; 989 translate_op1 Onotbool destrs destrs (refl ? (|destrs|)) 960 990 ] start_lbl dest_lbl def 961 | C ompare_NotEqual⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def962 | C ompare_Less ⇒ translate_lts destrs destrs_prf srcrs1 srcrs2 srcrs_prf? start_lbl dest_lbl def963 | C ompare_Greater ⇒ translate_lts destrs destrs_prf srcrs2 srcrs1 srcrs_prf? start_lbl dest_lbl def964 | C ompare_LessEqual⇒991 | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def 992 | Clt ⇒ translate_lts destrs destrs_prf srcrs1 srcrs2 ? ? start_lbl dest_lbl def 993 | Cgt ⇒ translate_lts destrs destrs_prf srcrs2 srcrs1 ? ? start_lbl dest_lbl def 994 | Cle ⇒ 965 995 add_translates [ 966 translate_lts destrs destrs_prf srcrs2 srcrs1 srcrs_prf ? start_lbl dest_lbl def;967 translate_op1 op_not_bool destrs destrs (refl ? (|destrs|))996 translate_lts destrs destrs_prf srcrs2 srcrs1 ? ?; 997 translate_op1 Onotbool destrs destrs (refl ? (|destrs|)) 968 998 ] start_lbl dest_lbl def 969 | C ompare_GreaterEqual⇒999 | Cge ⇒ 970 1000 add_translates [ 971 translate_lts destrs destrs_prf srcrs1 srcrs2 srcrs_prf ? start_lbl dest_lbl def;972 translate_op1 op_not_bool destrs destrs (refl ? (|destrs|))1001 translate_lts destrs destrs_prf srcrs1 srcrs2 ? ?; 1002 translate_op1 Onotbool destrs destrs (refl ? (|destrs|)) 973 1003 ] start_lbl dest_lbl def 974 1004 ] 1005 | Ocmpu c ⇒ 1006 match c with 1007 [ Ceq ⇒ 1008 add_translates [ 1009 translate_ne destrs srcrs1 srcrs2; 1010 translate_op1 Onotbool destrs destrs (refl ? (|destrs|)) 1011 ] start_lbl dest_lbl def 1012 | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def 1013 | Clt ⇒ translate_lt destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def 1014 | Cgt ⇒ translate_lt destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def 1015 | Cle ⇒ 1016 add_translates [ 1017 translate_lt destrs destrs_prf srcrs2 srcrs1; 1018 translate_op1 Onotbool destrs destrs (refl ? (|destrs|)) 1019 ] start_lbl dest_lbl def 1020 | Cge ⇒ 1021 add_translates [ 1022 translate_lt destrs destrs_prf srcrs1 srcrs2; 1023 translate_op1 Onotbool destrs destrs (refl ? (|destrs|)) 1024 ] start_lbl dest_lbl def 1025 ] 1026 | Ocmpp c ⇒ 1027 match c with 1028 [ Ceq ⇒ 1029 add_translates [ 1030 translate_ne destrs srcrs1 srcrs2; 1031 translate_op1 Onotbool destrs destrs (refl ? (|destrs|)) 1032 ] start_lbl dest_lbl def 1033 | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def 1034 | Clt ⇒ translate_lt destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def 1035 | Cgt ⇒ translate_lt destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def 1036 | Cle ⇒ 1037 add_translates [ 1038 translate_lt destrs destrs_prf srcrs2 srcrs1; 1039 translate_op1 Onotbool destrs destrs (refl ? (|destrs|)) 1040 ] start_lbl dest_lbl def 1041 | Cge ⇒ 1042 add_translates [ 1043 translate_lt destrs destrs_prf srcrs1 srcrs2; 1044 translate_op1 Onotbool destrs destrs (refl ? (|destrs|)) 1045 ] start_lbl dest_lbl def 1046 ] 1047 | _ ⇒ ? (* assert false, implemented in run time or float op *) 1048 ]. 1049 [ 2,6: normalize in nil_absrd; 1050 cases(not_le_Sn_O 0) 1051 #HYP cases(HYP nil_absrd) 1052 | 3,7,12,17,13,15,18,19,20,21,14,16: 1053 assumption 1054 | *: cases not_implemented (* yes, really *) 1055 ] 1056 qed. 1057 1058 definition translate_cond ≝ 1059 λsrcrs: list register. 1060 λstart_lbl: label. 1061 λlbl_true: label. 1062 λlbl_false: label. 1063 λdef: rtl_internal_function. 1064 let 〈def, tmpr〉 ≝ fresh_reg def in 1065 let 〈def, tmp_lbl〉 ≝ fresh_label def in 1066 let init ≝ rtl_st_int tmpr (zero ?) start_lbl in 1067 let f ≝ λsrcr. rtl_st_op2 Or tmpr tmpr srcr start_lbl in 1068 let def ≝ adds_graph (init :: (map … f srcrs)) start_lbl tmp_lbl def in 1069 add_graph tmp_lbl (rtl_st_cond tmpr lbl_true lbl_false) def. 1070 1071 definition translate_load ≝ 1072 λaddr. 1073 λaddr_prf: 2 ≤ |addr|. 1074 λdestrs: list register. 1075 λstart_lbl: label. 1076 λdest_lbl: label. 1077 λdef: rtl_internal_function. 1078 match fresh_regs_strong def (|addr|) with 1079 [ dp def_save_addr save_addr_prf ⇒ 1080 let def ≝ \fst def_save_addr in 1081 let save_addr ≝ \snd def_save_addr in 1082 match fresh_regs_strong def (|addr|) with 1083 [ dp def_tmp_addr tmp_addr_prf ⇒ 1084 let def ≝ \fst def_tmp_addr in 1085 let tmp_addr ≝ \snd def_tmp_addr in 1086 let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr ? tmp_addr ? in 1087 let 〈def, tmpr〉 ≝ fresh_reg def in 1088 let insts_save_addr ≝ translate_move save_addr addr in 1089 let f ≝ λtranslates_off. λr. 1090 let 〈translates, off〉 ≝ translates_off in 1091 let translates ≝ translates @ [ 1092 adds_graph [ 1093 rtl_st_int tmpr off start_lbl 1094 ]; 1095 translate_op2 Oaddp tmp_addr ? save_addr [tmpr] ? ?; 1096 adds_graph [ 1097 rtl_st_load r tmp_addr1 tmp_addr2 dest_lbl 1098 ] 1099 ] 1100 in 1101 let 〈carry, result〉 ≝ half_add ? off int_size in 1102 〈translates, result〉 1103 in 1104 let 〈translates, ignore〉 ≝ foldl ? ? f 〈[ ], (zero ?)〉 destrs in 1105 add_translates (insts_save_addr :: translates) start_lbl dest_lbl def 1106 ] 1107 ]. 1108 [1: normalize // 1109 |2: >save_addr_prf normalize 1110 @(transitive_le 1 2 (|addr|)) // 1111 |3: >tmp_addr_prf normalize 1112 @(transitive_le 1 2 (|addr|)) // 1113 |*: >tmp_addr_prf assumption 1114 ] 1115 qed. 1116 1117 definition translate_store ≝ 1118 λaddr. 1119 λaddr_prf: 2 ≤ |addr|. 1120 λsrcrs: list register. 1121 λstart_lbl: label. 1122 λdest_lbl: label. 1123 λdef: rtl_internal_function. 1124 match fresh_regs_strong def (|addr|) with 1125 [ dp def_tmp_addr tmp_addr_prf ⇒ 1126 let def ≝ \fst def_tmp_addr in 1127 let tmp_addr ≝ \snd def_tmp_addr in 1128 let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr ? tmp_addr ? in 1129 let 〈def, tmpr〉 ≝ fresh_reg def in 1130 let f ≝ λtranslate_off. λsrcr. 1131 let 〈translates, off〉 ≝ translate_off in 1132 let translates ≝ translates @ [ 1133 adds_graph [ 1134 rtl_st_int tmpr off start_lbl 1135 ]; 1136 translate_op2 Oaddp tmp_addr ? addr [tmpr] ? ?; 1137 adds_graph [ 1138 rtl_st_store tmp_addr1 tmp_addr2 srcr dest_lbl 1139 ] 1140 ] 1141 in 1142 let 〈carry, result〉 ≝ half_add ? off int_size in 1143 〈translates, result〉 1144 in 1145 let 〈translates, ignore〉 ≝ foldl ? ? f 〈[ ], zero ?〉 srcrs in 1146 add_translates translates start_lbl dest_lbl def 1147 ]. 1148 [1: normalize // 1149 |2: >tmp_addr_prf normalize 1150 @(transitive_le 1 2 (|addr|)) // 1151 |3: >tmp_addr_prf normalize 1152 @(transitive_le 1 2 (|addr|)) // 1153 |*: >tmp_addr_prf assumption 1154 ] 1155 qed. 1156 1157 definition translate_stmt ≝ 1158 λlenv. 1159 λlbl: label. 1160 λstmt. 1161 λdef: rtl_internal_function. 1162 match stmt with 1163 [ St_skip lbl' ⇒ add_graph lbl (rtl_st_skip lbl') def 1164 | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def 1165 | St_const destr cst lbl' ⇒ 1166 translate_cst cst (find_local_env destr lenv) lbl lbl' def 1167 | St_op1 op1 destr srcr lbl' ⇒ 1168 translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) ? lbl lbl' def 1169 | St_op2 op2 destr srcr1 srcr2 lbl' ⇒ 1170 translate_op2 op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def 1171 | St_load ignore addr destr lbl' ⇒ 1172 translate_load (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def 1173 | St_store ignore addr srcr lbl' ⇒ 1174 translate_store (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def 1175 | St_call_id f args retr lbl' ⇒ 1176 match retr with 1177 [ Some retr ⇒ 1178 add_graph lbl (rtl_st_call_id f (rtl_args args lenv) (find_local_env retr lenv) lbl') def 1179 | None ⇒ add_graph lbl (rtl_st_call_id f (rtl_args args lenv) [ ] lbl') def 1180 ] 1181 | St_call_ptr f args retr lbl' ⇒ 1182 match retr with 1183 [ None ⇒ 1184 let 〈f1, f2〉 ≝ find_and_addr f lenv ? in 1185 add_graph lbl (rtl_st_call_ptr f1 f2 (rtl_args args lenv) [ ] lbl') def 1186 | Some retr ⇒ 1187 let 〈f1, f2〉 ≝ find_and_addr f lenv ? in 1188 add_graph lbl (rtl_st_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv) lbl') def 1189 ] 1190 | St_tailcall_id f args ⇒ 1191 add_graph lbl (rtl_st_tailcall_id f (rtl_args args lenv)) def 1192 | St_tailcall_ptr f args ⇒ 1193 let 〈f1, f2〉 ≝ find_and_addr f lenv ? in 1194 add_graph lbl (rtl_st_tailcall_ptr f1 f2 (rtl_args args lenv)) def 1195 | St_cond r lbl_true lbl_false ⇒ 1196 translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def 1197 | St_jumptable r l ⇒ ? (* assert false: not implemented yet *) 1198 | St_return r ⇒ 1199 match r with 1200 [ None ⇒ add_graph lbl (rtl_st_return [ ]) def 1201 | Some r ⇒ add_graph lbl (rtl_st_return (find_local_env r lenv)) def 1202 ] 975 1203 | _ ⇒ ? 976 1204 ]. 977 1205 978 let rec translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def = 979 match op2 with 980 981 | AST.Op_divu when List.length srcrs1 = 1 && List.length srcrs2 = 1 -> 982 translate_divumodu8 true destrs (List.hd srcrs1) (List.hd srcrs2) 983 start_lbl dest_lbl def 984 985 | AST.Op_modu when List.length srcrs1 = 1 && List.length srcrs2 = 1 -> 986 translate_divumodu8 false destrs (List.hd srcrs1) (List.hd srcrs2) 987 start_lbl dest_lbl def 988 989 | AST.Op_cmp AST.Cmp_eq 990 | AST.Op_cmpu AST.Cmp_eq 991 | AST.Op_cmpp AST.Cmp_eq -> 992 add_translates 993 [translate_op2 (AST.Op_cmpu AST.Cmp_ne) destrs srcrs1 srcrs2 ; 994 translate_op1 AST.Op_notbool destrs destrs] 995 start_lbl dest_lbl def 996 997 | AST.Op_cmp AST.Cmp_ne 998 | AST.Op_cmpu AST.Cmp_ne 999 | AST.Op_cmpp AST.Cmp_ne -> 1000 translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def 1001 1002 | AST.Op_cmp AST.Cmp_lt -> 1003 translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def 1004 1005 | AST.Op_cmpu AST.Cmp_lt | AST.Op_cmpp AST.Cmp_lt -> 1006 translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def 1007 1008 | AST.Op_cmp AST.Cmp_le -> 1009 add_translates 1010 [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs2 srcrs1 ; 1011 translate_op1 AST.Op_notbool destrs destrs] 1012 start_lbl dest_lbl def 1013 1014 | AST.Op_cmpu AST.Cmp_le -> 1015 add_translates 1016 [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs2 srcrs1 ; 1017 translate_op1 AST.Op_notbool destrs destrs] 1018 start_lbl dest_lbl def 1019 1020 | AST.Op_cmpp AST.Cmp_le -> 1021 add_translates 1022 [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs2 srcrs1 ; 1023 translate_op1 AST.Op_notbool destrs destrs] 1024 start_lbl dest_lbl def 1025 1026 | AST.Op_cmp AST.Cmp_gt -> 1027 translate_op2 (AST.Op_cmp AST.Cmp_lt) 1028 destrs srcrs2 srcrs1 start_lbl dest_lbl def 1029 1030 | AST.Op_cmpu AST.Cmp_gt -> 1031 translate_op2 (AST.Op_cmpu AST.Cmp_lt) 1032 destrs srcrs2 srcrs1 start_lbl dest_lbl def 1033 1034 | AST.Op_cmpp AST.Cmp_gt -> 1035 translate_op2 (AST.Op_cmpp AST.Cmp_lt) 1036 destrs srcrs2 srcrs1 start_lbl dest_lbl def 1037 1038 | AST.Op_cmp AST.Cmp_ge -> 1039 add_translates 1040 [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs1 srcrs2 ; 1041 translate_op1 AST.Op_notbool destrs destrs] 1042 start_lbl dest_lbl def 1043 1044 | AST.Op_cmpu AST.Cmp_ge -> 1045 add_translates 1046 [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ; 1047 translate_op1 AST.Op_notbool destrs destrs] 1048 start_lbl dest_lbl def 1049 1050 | AST.Op_cmpp AST.Cmp_ge -> 1051 add_translates 1052 [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ; 1053 translate_op1 AST.Op_notbool destrs destrs] 1054 start_lbl dest_lbl def 1055 1056 | AST.Op_div | AST.Op_divu | AST.Op_modu | AST.Op_mod | AST.Op_shl 1057 | AST.Op_shr | AST.Op_shru -> 1058 (* Unsupported, should have been replaced by a runtime function. *) 1059 assert false 1060 1206 let translate_stmt lenv lbl stmt def = match stmt with 1207 1208 | RTLabs.St_skip lbl' -> 1209 add_graph lbl (RTL.St_skip lbl') def 1210 1211 | RTLabs.St_cost (cost_lbl, lbl') -> 1212 add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def 1213 1214 | RTLabs.St_cst (destr, cst, lbl') -> 1215 translate_cst cst (find_local_env destr lenv) lbl lbl' def 1216 1217 | RTLabs.St_op1 (op1, destr, srcr, lbl') -> 1218 translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) 1219 lbl lbl' def 1220 1221 | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') -> 1222 translate_op2 op2 (find_local_env destr lenv) 1223 (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def 1224 1225 | RTLabs.St_load (_, addr, destr, lbl') -> 1226 translate_load (find_local_env addr lenv) (find_local_env destr lenv) 1227 lbl lbl' def 1228 1229 | RTLabs.St_store (_, addr, srcr, lbl') -> 1230 translate_store (find_local_env addr lenv) (find_local_env srcr lenv) 1231 lbl lbl' def 1232 1233 | RTLabs.St_call_id (f, args, None, _, lbl') -> 1234 add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def 1235 1236 | RTLabs.St_call_id (f, args, Some retr, _, lbl') -> 1237 add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, 1238 find_local_env retr lenv, lbl')) def 1239 1240 | RTLabs.St_call_ptr (f, args, None, _, lbl') -> 1241 let (f1, f2) = find_and_addr f lenv in 1242 add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def 1243 1244 | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') -> 1245 let (f1, f2) = find_and_addr f lenv in 1246 add_graph lbl 1247 (RTL.St_call_ptr 1248 (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def 1249 1250 | RTLabs.St_tailcall_id (f, args, _) -> 1251 add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def 1252 1253 | RTLabs.St_tailcall_ptr (f, args, _) -> 1254 let (f1, f2) = find_and_addr f lenv in 1255 add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def 1256 1257 | RTLabs.St_cond (r, lbl_true, lbl_false) -> 1258 translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def 1259 1260 | RTLabs.St_jumptable _ -> 1261 error "Jump tables not supported yet." 1262 1263 | RTLabs.St_return None -> 1264 add_graph lbl (RTL.St_return []) def 1265 1266 | RTLabs.St_return (Some r) -> 1267 add_graph lbl (RTL.St_return (find_local_env r lenv)) def 1061 1268 1062 1269 definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset
for help on using the changeset viewer.