Changeset 1066
 Timestamp:
 Jul 13, 2011, 5:12:10 PM (9 years ago)
 Location:
 src
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/I8051.ma
r1060 r1066 115 115 bitvector_of_nat ? (nat_of_register register). 116 116 117 definition compare_register: Register → Register → Compare ≝117 definition compare_register: Register → Register → compare ≝ 118 118 λr, s: Register. 119 119 let r_as_nat ≝ nat_of_register r in 120 120 let s_as_nat ≝ nat_of_register s in 121 121 match eqb r_as_nat s_as_nat with 122 [ true ⇒ Compare_Equal122 [ true ⇒ compare_equal 123 123  false ⇒ 124 124 match ltb r_as_nat s_as_nat with 125 [ true ⇒ Compare_Less126  false ⇒ Compare_Greater125 [ true ⇒ compare_less 126  false ⇒ compare_greater 127 127 ] 128 128 ]. 
src/RTL/RTL.ma
r1064 r1066 24 24  rtl_st_tailcall_id: ident → registers → rtl_statement 25 25  rtl_st_tailcall_ptr: register → register → registers → rtl_statement 26  rtl_st_cond _acc: register → label → label → rtl_statement26  rtl_st_cond: register → label → label → rtl_statement 27 27  rtl_st_set_carry: label → rtl_statement 28 28  rtl_st_return: registers → rtl_statement. 
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 ≝ 
src/utilities/Compare.ma
r491 r1066 1 1 include "basics/logic.ma". 2 2 3 inductive Compare: Type[0] ≝4 Compare_Equal: Compare5  Compare_Less: Compare6  Compare_Greater: Compare7  Compare_LessEqual: Compare8  Compare_GreaterEqual: Compare.3 inductive compare: Type[0] ≝ 4 compare_equal: compare 5  compare_less: compare 6  compare_greater: compare 7  compare_less_equal: compare 8  compare_greater_equal: compare. 9 9
Note: See TracChangeset
for help on using the changeset viewer.