Changeset 2030 for src/Clight/SimplifyCasts.ma
- Timestamp:
- Jun 8, 2012, 1:44:31 PM (9 years ago)
- File:
-
- 1 edited
-
src/Clight/SimplifyCasts.ma (modified) (22 diffs)
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/SimplifyCasts.ma
r2019 r2030 5 5 include "Clight/Cexec.ma". 6 6 include "Clight/casts.ma". 7 include "Clight/CexecSound.ma". 8 7 9 8 10 (* include "ASM/AssemblyProof.ma". *) (* I had to manually copy some of the lemmas in this file, including an axiom ... *) … … 139 141 ]. 140 142 143 lemma size_lt_to_le : ∀sz1,sz2. size_lt sz1 sz2 → size_le sz1 sz2. 144 #sz1 #sz2 elim sz1 elim sz2 normalize // qed. 145 141 146 lemma size_lt_dec : ∀sz1,sz2. size_lt sz1 sz2 + (¬ (size_lt sz1 sz2)). 142 147 * * normalize /2/ /3/ … … 186 191 | 2: #Hsg_neq #_ %2 destruct /2/ ] 187 192 ] 188 ] qed. 189 193 ] qed. 190 194 191 195 (* Compare the results [r1,r2] of the evaluation of two expressions. If [r1] is an 192 196 * integer value smaller but containing the same stuff than [r2] then all is well. 193 197 * If the first evaluation is erroneous, we don't care about anything else. *) 194 definition smaller_integer_val ≝ λsrc_sz,dst_sz,sg. λr1,r2:res 198 definition smaller_integer_val ≝ λsrc_sz,dst_sz,sg. λr1,r2:res(val×trace). 195 199 match r1 with 196 200 [ OK res1 ⇒ 201 let 〈val1, tr1〉 ≝ res1 in 202 ∀v1. val1 = Vint src_sz v1 → 197 203 match r2 with 198 [ OK res2 ⇒ 199 let 〈v1, tr1〉 ≝ res1 in 200 let 〈v2, tr2〉 ≝ res2 in 201 match v1 with 202 [ Vint sz1 v1 ⇒ 203 match v2 with 204 [ Vint sz2 v2 ⇒ 205 match sz_eq_dec sz1 src_sz with 206 [ inl Hsrc_eq ⇒ 207 match sz_eq_dec sz2 dst_sz with 208 [ inl Hdst_eq ⇒ 209 v2 = cast_int_int sz1 sg sz2 v1 210 ∧ tr1 = tr2 211 ∧ size_le dst_sz src_sz 212 | inr _ ⇒ False ] 213 | inr _ ⇒ False ] 214 | _ ⇒ False ] 215 | _ ⇒ False ] 204 [ OK res2 ⇒ 205 let 〈val2, tr2〉 ≝ res2 in 206 ∃v2. (val2 = Vint dst_sz v2 ∧ 207 v2 = cast_int_int src_sz sg dst_sz v1 ∧ tr1 = tr2 ∧ size_le dst_sz src_sz) 216 208 | _ ⇒ False ] 217 | Error errmsg1 ⇒ True (* Simulation ... *) 218 (* match r2 with 219 [ OK _ ⇒ False 220 | Error errmsg2 ⇒ True (* Note that the two expressions may fail for different reasons ... Too lax maybe ? *) 221 ] *) 209 | Error errmsg1 ⇒ True 222 210 ]. 223 224 (* Inversion on smaller_integer_val *)225 lemma smaller_integer_val_spec : ∀src_sz,dst_sz,sg,val1,val2,tr1,tr2.226 smaller_integer_val src_sz dst_sz sg (OK ? 〈val1, tr1〉) (OK ? 〈val2, tr2〉) →227 ∃v1,v2. val1 = Vint src_sz v1 ∧ val2 = Vint dst_sz v2 ∧228 v2 = cast_int_int src_sz sg dst_sz v1 ∧ tr1 = tr2 ∧ size_le dst_sz src_sz.229 #src_sz #dst_sz #sg #val1 #val2 #tr1 #tr2230 whd in ⊢ (% → ?);231 elim val1 normalize nodelta232 [ 1: #Hcontr @(False_ind … Hcontr) | 3,4,5: #foo #Hcontr @(False_ind … Hcontr)233 | 2: #size1 #int1 cases val2234 [ 1: #Hcontr @(False_ind … Hcontr) | 3,4,5: #foo #Hcontr @(False_ind … Hcontr)235 | 2: #size2 #int2 normalize nodelta236 cases (sz_eq_dec size1 src_sz)237 cases (sz_eq_dec size2 dst_sz)238 [ 2,3,4: #Hneq #Heq #Hcontr @(False_ind … Hcontr)239 | 1: #Heq1 #Heq2 * * #Hcast #Htrace #H destruct240 @(ex_intro … int1) @(ex_intro … (cast_int_int src_sz sg dst_sz int1))241 try @conj try @conj try @conj try @conj try @conj try @conj //242 ]243 ]244 ] qed.245 211 246 212 (* Simulation relation used for expression evaluation. *) … … 265 231 simplify_inv ge en m e1 e2 target_sz target_sg true. 266 232 233 (* Invariant of simplify_inside *) 267 234 definition conservation ≝ λe,result:expr. 268 235 ∀ge,en,m. simulate ? (exec_expr ge en m e) (exec_expr ge en m result) … … 731 698 lapply (Hind ? tl) #H 732 699 whd in match (two_complement_negation ??) in H; 733 (* trying to reduce add_with_carries *)700 (* trying to reduce add_with_carries *) 734 701 normalize in match (S m'+n); 735 702 whd in match (zero ?) in ⊢ (???%); … … 737 704 whd in match (negation_bv ??) in ⊢ (???%); 738 705 >add_with_carries_unfold in ⊢ (???%); 739 (* >truncate_tail *)740 706 normalize in ⊢ (???%); 741 707 cases hd normalize nodelta … … 803 769 ] 804 770 ] qed. 805 771 772 lemma simplify_int_success_lt : ∀sz,sg,sz',sg',i,i'. (simplify_int sz sz' sg sg' i=Some (bvint sz') i') → size_le sz' sz. 773 * #sg * #sg' #i #i' #H whd in H:(??%?); try destruct normalize // qed. 774 775 lemma smaller_integer_val_identity : ∀sz,sg,x. 776 smaller_integer_val sz sz sg x x. 777 #sz #sg * 778 [ 2: #error // 779 | 1: * #val #trace whd in match (smaller_integer_val ?????); 780 #v1 #Hval %{v1} @conj try @conj try @conj // 781 elim sz // 782 ] qed. 783 784 (* Inversion on exec_cast *) 785 lemma exec_cast_inv : ∀castee_val,src_sz,src_sg,cast_sz,cast_sg,m,result. 786 exec_cast m castee_val (Tint src_sz src_sg) (Tint cast_sz cast_sg) = OK ? result → 787 ∃i. castee_val = Vint src_sz i ∧ result = Vint cast_sz (cast_int_int src_sz src_sg cast_sz i). 788 #castee_val #src_sz #src_sg #cast_sz #cast_sg #m #result 789 elim castee_val 790 [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ] 791 [ 2: | *: whd in ⊢ ((??%?) → ?); #Habsurd destruct ] 792 whd in ⊢ ((??%?) → ?); 793 cases (sz_eq_dec sz' src_sz) 794 [ 1: #Heq destruct >intsize_eq_elim_true normalize nodelta #Heq destruct 795 %{i} /2/ 796 | 2: #Hneq >intsize_eq_elim_false; try assumption #H destruct ] 797 qed. 798 799 800 (* Lemmas related to the Ebinop case *) 801 806 802 lemma classify_add_int : ∀sz,sg. classify_add (Tint sz sg) (Tint sz sg) = add_case_ii sz sg. 807 803 * * // qed. … … 812 808 lemma bool_conj_inv : ∀a,b : bool. (a ∧ b) = true → a = true ∧ b = true. 813 809 * * normalize #H @conj // qed. 814 815 lemma simplify_int_success_lt : ∀sz,sg,sz',sg',i,i'. (simplify_int sz sz' sg sg' i=Some (bvint sz') i') → size_le sz' sz.816 * #sg * #sg' #i #i' #H whd in H:(??%?); try destruct normalize // qed.817 810 818 811 (* Operations where it is safe to use a smaller integer type on the assumption … … 820 813 definition binop_simplifiable ≝ 821 814 λop. match op with [ Oadd ⇒ true | Osub ⇒ true | _ ⇒ false ]. 815 816 (* Inversion principle for integer addition *) 817 lemma iadd_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r → 818 ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (addition_n (bitsize_of_intsize dsz) i1 i2)). 819 #sz #sg #v1 #v2 #m #r 820 elim v1 821 [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ] 822 whd in ⊢ ((??%?) → ?); normalize nodelta 823 >classify_add_int normalize nodelta #H destruct 824 elim v2 in H; 825 [ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ] 826 whd in ⊢ ((??%?) → ?); #H destruct 827 elim (sz_eq_dec sz' sz'') 828 [ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/ 829 | 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct 830 ] qed. 831 832 (* Inversion principle for integer subtraction. *) 833 lemma isub_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r → 834 ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (subtraction ? i1 i2)). 835 #sz #sg #v1 #v2 #m #r 836 elim v1 837 [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ] 838 whd in ⊢ ((??%?) → ?); normalize nodelta 839 >classify_sub_int normalize nodelta #H destruct 840 elim v2 in H; 841 [ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ] 842 whd in ⊢ ((??%?) → ?); #H destruct 843 elim (sz_eq_dec sz' sz'') 844 [ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/ 845 | 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct 846 ] qed. 847 848 definition is_int : val → Prop ≝ 849 λv. 850 match v with 851 [ Vint _ _ ⇒ True 852 | _ ⇒ False ]. 853 854 (* "negative" (in the sense of ¬ Some) inversion principle for integer addition *) 855 lemma neg_iadd_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = None ? → 856 ¬ (is_int v1) ∨ ¬ (is_int v2) ∨ 857 ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2. 858 #sz #sg #v1 #v2 #m 859 elim v1 860 [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ] 861 [ 2: | *: #_ %1 %1 % #H @H ] 862 elim v2 863 [ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ] 864 [ 2: | *: #_ %1 %2 % #H @H ] 865 whd in ⊢ ((??%?) → ?); normalize nodelta 866 >classify_add_int normalize nodelta 867 elim (sz_eq_dec sz' sz'') 868 [ 1: #Heq destruct >intsize_eq_elim_true #Habsurd destruct (Habsurd) 869 | 2: #Hneq >intsize_eq_elim_false try assumption #_ 870 %2 %{sz'} %{sz''} %{i} %{i'} try @conj try @conj // 871 ] qed. 872 873 (* "negative" inversion principle for integer subtraction *) 874 lemma neg_isub_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = None ? → 875 ¬ (is_int v1) ∨ ¬ (is_int v2) ∨ 876 ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2. 877 #sz #sg #v1 #v2 #m 878 elim v1 879 [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ] 880 [ 2: | *: #_ %1 %1 % #H @H ] 881 elim v2 882 [ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ] 883 [ 2: | *: #_ %1 %2 % #H @H ] 884 whd in ⊢ ((??%?) → ?); normalize nodelta 885 >classify_sub_int normalize nodelta 886 elim (sz_eq_dec sz' sz'') 887 [ 1: #Heq destruct >intsize_eq_elim_true #Habsurd destruct (Habsurd) 888 | 2: #Hneq >intsize_eq_elim_false try assumption #_ 889 %2 %{sz'} %{sz''} %{i} %{i'} try @conj try @conj // 890 ] qed. 891 892 893 lemma simplifiable_op_inconsistent : ∀op,sz,sg,v1,v2,m. 894 ¬ (is_int v1) → binop_simplifiable op = true → sem_binary_operation op v1 (Tint sz sg) v2 (Tint sz sg) m = None ?. 895 #op #sz #sg #v1 #v2 #m #H 896 elim op normalize in match (binop_simplifiable ?); #H destruct 897 elim v1 in H; 898 [ 1,6: | 2,7: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I)) | 3,8: #f | 4,9: #r | 5,10: #ptr ] 899 #_ 900 whd in match (sem_binary_operation ??????); normalize nodelta 901 >classify_add_int normalize nodelta // 902 >classify_sub_int normalize nodelta // 903 qed. 822 904 823 905 notation > "hvbox('let' «ident x,ident y» 'as' ident E ≝ t 'in' s)" … … 833 915 ] (refl ? $t) 834 916 }. 835 836 917 837 918 (* This function will make your eyes bleed. You've been warned. 838 919 * Implements a correct-by-construction version of Brian's original cast-removal code. Does so by … … 1016 1097 ] 1017 1098 | Econst_float f ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» 1018 | Evar id ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» 1099 (* | Evar id ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» *) 1100 (* In order for the simplification function to be less dymp, we would have to use this line, which would in fact 1101 require to alter the semantics of [load_value_of_type]. *) 1102 | Evar id ⇒ λHdesc_eq. «〈type_eq ty (Tint target_sz target_sg), Expr ed ty〉, ?» 1019 1103 | Esizeof t ⇒ λHdesc_eq. «〈type_eq ty (Tint target_sz target_sg), Expr ed ty〉, ?» 1020 1104 ] (refl ? ed) … … 1085 1169 cases (exec_expr ge en m e) #res 1086 1170 try (@(SimOk ???) //) 1087 | 13,14: %1 // >Hexpr_eq cases (exec_expr ge en m e) #res1088 try (@(SimOk ???) //)1089 1171 | 2: @(Inv_coerce_ok ge en m … target_sz target_sg target_sz target_sg) destruct /by refl/ 1172 (* 1090 1173 whd in match (exec_expr ????); >eq_intsize_identity whd 1091 1174 >sz_eq_identity normalize % [ 1: @conj // | 2: elim target_sz in i; normalize #i @I ] 1175 *) 1092 1176 | 4: destruct @(Inv_coerce_ok ge en m ???? ty_sz sg) / by refl/ 1093 1177 whd in match (exec_expr ????); 1094 1178 whd in match (exec_expr ????); 1095 1179 >eq_intsize_identity >eq_intsize_identity whd 1096 >sz_eq_identity >sz_eq_identity whd @conj try @conj try @refl1180 #v1 #Heq destruct (Heq) %{i'} try @conj try @conj try @conj // 1097 1181 [ 1: @(simplify_int_implements_cast … Hsimpl_eq) 1098 1182 | 2: @(simplify_int_success_lt … Hsimpl_eq) ] 1183 | 13: %1 // >Hexpr_eq cases (exec_expr ge en m e) #res 1184 try (@(SimOk ???) //) 1185 | 14: elim (type_eq_dec ty (Tint target_sz target_sg)) 1186 [ 1: #Heq >Heq >type_eq_identity @(Inv_coerce_ok ??????? target_sz target_sg) 1187 destruct 1188 [ 1,2: // 1189 | 3: @smaller_integer_val_identity ] 1190 | 2: #Hneq >(type_neq_not_identity … Hneq) %1 // destruct 1191 @(SimOk ???) // 1192 ] 1099 1193 | 15: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq 1100 1194 [ 1: (* Proving preservation of the semantics for expressions. *) … … 1214 1308 | 3: whd in match (exec_expr ??? (Expr ??)); 1215 1309 whd in match (exec_expr ??? (Expr ??)); 1310 (* Tidy up the type equations *) 1311 >Htype_lhs in Htylhs_eq_tyrhs; >Htype_rhs #Heq destruct 1312 lapply Hsmaller_rhs lapply Hsmaller_lhs 1313 generalize in match rhs_src_sz; #src_sz 1314 generalize in match rhs_src_sg; #src_sg 1315 -Hsmaller_lhs -Hsmaller_rhs -Htype_lhs -Htype_rhs -Hinv_lhs -Hinv_rhs 1316 >Htype_lhs1 >Htype_rhs1 -Htype_lhs1 -Htype_rhs1 1216 1317 (* Enumerate all the cases for the evaluation of the source expressions ... *) 1217 cases (exec_expr ge en m lhs) in Hsmaller_lhs; 1218 [ 2: #error // 1219 | 1: * #val_lhs #trace_lhs normalize nodelta cases (exec_expr ge en m lhs1) 1220 [ 2: #error #H @(False_ind … H) 1221 | 1: * #val_lhs1 #trace_lhs1 #Hsmaller_lhs 1222 elim (smaller_integer_val_spec … Hsmaller_lhs) 1223 #lhs_int * #lhs1_int * * * * #Hval_lhs #Hval_lhs1 #Hlhs_cast #Hlhs_trace #Hlhs_size 1224 cases (exec_expr ge en m rhs) in Hsmaller_rhs; 1225 [ 2: #error // 1226 | 1: * #val_rhs #trace_rhs normalize nodelta cases (exec_expr ge en m rhs1) 1227 [ 2: #error #H @(False_ind … H) 1228 | 1: * #val_rhs1 #trace_rhs1 #Hsmaller_rhs 1229 elim (smaller_integer_val_spec … Hsmaller_rhs) 1230 #rhs_int * #rhs1_int * * * * #Hval_rhs #Hval_rhs1 #Hrhs_cast #Hrhs_trace #Hrhs_size 1231 whd in match (m_bind ?????); 1232 whd in match (m_bind ?????); 1233 <Htylhs_eq_tyrhs >Htype_lhs 1234 >Htype_lhs1 >Htype_rhs1 1235 cut (lhs_src_sz = rhs_src_sz ∧ lhs_src_sg = rhs_src_sg) 1236 [ 1: >Htype_lhs in Htylhs_eq_tyrhs; >Htype_rhs #Hty_eq destruct (Hty_eq) 1237 @conj // ] 1238 * #Hsrc_sz_eq #Hsrc_sg_eq 1239 cases op in Hop_simplifiable_eq; 1240 normalize in match (binop_simplifiable ?); 1241 [ 3,4,5,6,7,8,9,10,11,12,13,14,15,16: #H destruct (H) 1242 | 1: #_ (* addition case *) 1243 >Hval_lhs >Hval_rhs destruct 1244 whd in match (sem_binary_operation Oadd ?????); 1245 whd in match (sem_binary_operation Oadd ?????); normalize nodelta 1246 >classify_add_int >classify_add_int normalize nodelta 1247 >intsize_eq_elim_true >intsize_eq_elim_true 1248 whd in match (opt_to_res ???); whd in match (opt_to_res ???); 1249 whd in match (smaller_integer_val ?????); normalize nodelta 1250 >sz_eq_identity >sz_eq_identity normalize nodelta 1251 try @conj try @conj try // 1252 >integer_add_cast_le // 1253 | 2: #_ (* subtraction case *) 1254 >Hval_lhs >Hval_rhs destruct 1255 whd in match (sem_binary_operation Osub ?????); 1256 whd in match (sem_binary_operation Osub ?????); normalize nodelta 1257 >classify_sub_int >classify_sub_int normalize nodelta 1258 >intsize_eq_elim_true >intsize_eq_elim_true 1259 whd in match (opt_to_res ???); whd in match (opt_to_res ???); 1260 whd in match (smaller_integer_val ?????); normalize nodelta 1261 >sz_eq_identity >sz_eq_identity normalize nodelta 1262 try @conj try @conj try // 1263 >integer_sub_cast_le // 1264 ] 1265 ] 1266 ] 1267 ] 1268 ] 1269 ] 1270 ] 1271 ] 1318 cases (exec_expr ge en m lhs); 1319 try // * #val_lhs #trace_lhs normalize nodelta 1320 cases (exec_expr ge en m rhs); 1321 try // * #val_rhs #trace_rhs normalize nodelta 1322 whd in match (m_bind ?????); 1323 (* specialize to the actual simplifiable operations. *) 1324 cases op in Hop_simplifiable_eq; 1325 [ 1,2: | *: normalize in ⊢ (% → ?); #H destruct (H) ] #_ 1326 [ 1: lapply (iadd_inv src_sz src_sg val_lhs val_rhs m) 1327 | 2: lapply (isub_inv src_sz src_sg val_lhs val_rhs m) ] 1328 cases (sem_binary_operation ? val_lhs (Tint src_sz src_sg) val_rhs (Tint src_sz src_sg) m) 1329 [ 1,3: #_ #_ #_ normalize @I ] 1330 #src_result #Hinversion_src elim (Hinversion_src src_result (refl ? (Some ? src_result))) 1331 #src_result_sz * #i1 * #i2 * * #Hval_lhs_eq #Hval_rhs_eq #Hsrc_result_eq 1332 whd in match (opt_to_res ???); whd in match (m_bind ?????); normalize nodelta 1333 >Hval_lhs_eq >Hval_rhs_eq #Hsmaller_rhs #Hsmaller_lhs 1334 whd 1335 #result_int #Hsrc_result >Hsrc_result in Hsrc_result_eq; #Hsrc_result_eq 1336 lapply (sym_eq ??? Hsrc_result_eq) -Hsrc_result_eq #Hsrc_result_eq 1337 cut (src_result_sz = src_sz) [ 1,3: destruct // ] #Hsz_eq 1338 lapply Hsmaller_lhs lapply Hsmaller_rhs 1339 cases (exec_expr ge en m lhs1) normalize nodelta 1340 [ 2,4: destruct #error normalize in ⊢ (% → ?); #H @(False_ind … (H i1 (refl ? (Vint src_sz i1)))) ] 1341 * #val_lhs1 #trace_lhs1 1342 cases (exec_expr ge en m rhs1) 1343 [ 2,4: destruct #error #_ normalize in ⊢ (% → ?); #H @(False_ind … (H i2 (refl ? (Vint src_sz i2)))) ] 1344 * #val_rhs1 #trace_rhs1 1345 whd in match (m_bind ?????); normalize nodelta 1346 [ 1: lapply (neg_iadd_inv target_sz target_sg val_lhs1 val_rhs1 m) 1347 lapply (iadd_inv target_sz target_sg val_lhs1 val_rhs1 m) 1348 | 2: lapply (neg_isub_inv target_sz target_sg val_lhs1 val_rhs1 m) 1349 lapply (isub_inv target_sz target_sg val_lhs1 val_rhs1 m) ] 1350 cases (sem_binary_operation ? val_lhs1 (Tint target_sz target_sg) val_rhs1 (Tint target_sz target_sg) m) 1351 [ 1,3: destruct #_ #Hneg_inversion elim (Hneg_inversion (refl ? (None ?))) 1352 (* Proceed by case analysis on Hneg_inversion to prove the absurdity of this branch *) 1353 * 1354 [ 1,4: whd in ⊢ (? → % → ?); normalize nodelta 1355 #Habsurd #Hcounterexample elim (Hcounterexample i1 (refl ? (Vint src_sz i1))) 1356 #i * * * #Hlhs1_is_int >Hlhs1_is_int in Habsurd; * #Habsurd 1357 @(False_ind … (Habsurd I)) 1358 | 2,5: whd in ⊢ (? → ? → % → ?); normalize nodelta 1359 #Habsurd #_ #Hcounterexample elim (Hcounterexample i2 (refl ? (Vint src_sz i2))) 1360 #i * * * #Hlhs1_is_int >Hlhs1_is_int in Habsurd; * #Habsurd 1361 @(False_ind … (Habsurd I)) 1362 | 3,6: #dsz1 * #dsz2 * #j1 * #j2 * * #Hval_lhs1 #Hval_rhs1 #Hsz_neq 1363 whd in ⊢ (% → % → ?); normalize nodelta 1364 #Hsmaller_lhs #Hsmaller_rhs 1365 elim (Hsmaller_lhs … i1 (refl ? (Vint src_sz i1))) 1366 #li * * * #Hval_lhs1_alt #H_lhs_cast_eq #Htrace_eq_lhs #Hsize_le 1367 elim (Hsmaller_rhs … i2 (refl ? (Vint src_sz i2))) 1368 #ri * * * #Hval_rhs1_alt #H_rhs_cast_eq #Htrace_eq_rhs #_ 1369 destruct elim Hsz_neq #Habsurd @(Habsurd (refl ? target_sz)) 1370 ] 1371 | 2,4: destruct #result #Hinversion #_ #Hsmaller_lhs #Hsmaller_rhs normalize nodelta 1372 elim (Hinversion result (refl ? (Some ? result))) 1373 #result_sz * #lhs_int * #rhs_int * * #Hlhs1_eq #Hrhs1_eq #Hop_eq 1374 elim (Hsmaller_lhs … i1 (refl ? (Vint src_sz i1))) 1375 #li * * * #Hval_lhs1_alt #H_lhs_cast_eq #Htrace_eq_lhs #Hsize_le 1376 elim (Hsmaller_rhs … i2 (refl ? (Vint src_sz i2))) 1377 #ri * * * #Hval_rhs1_alt #H_rhs_cast_eq #Htrace_eq_rhs #_ 1378 destruct 1379 [ 1: %{(addition_n (bitsize_of_intsize target_sz) 1380 (cast_int_int src_sz src_sg target_sz i1) 1381 (cast_int_int src_sz src_sg target_sz i2))} 1382 try @conj try @conj try @conj // 1383 >integer_add_cast_le try // 1384 | 2: %{(subtraction (bitsize_of_intsize target_sz) 1385 (cast_int_int src_sz src_sg target_sz i1) 1386 (cast_int_int src_sz src_sg target_sz i2))} 1387 try @conj try @conj try @conj // 1388 >integer_sub_cast_le try // 1389 ] 1390 ] ] ] ] 1272 1391 | 19,20,21,22: destruct %1 try @refl 1273 1392 elim (Hequiv_lhs ge en m) * #Hexpr_sim_lhs #Hlvalue_sim_lhs #Htype_eq_lhs … … 1335 1454 [ 1: // | 2: <Htype_castee1 // 1336 1455 | 3: whd in match (exec_expr ??? (Expr ??)); 1337 >Htype_castee 1456 >Htype_castee 1338 1457 (* Simplify the goal by culling impossible cases, using Hsmaller_val *) 1339 1458 cases (exec_expr ge en m castee) in Hsmaller_eval; 1340 1459 [ 2: #error // 1341 | 1: * #castee_val #castee_trace cases (exec_expr ge en m castee1)1342 [ 2: #error #Hcontr @(False_ind … Hcontr)1343 | 1: * #castee1_val #castee1_trace #Hsmaller1344 elim (smaller_integer_val_spec … Hsmaller)1345 #int1 * #int2 * * * * #Hint1 #Hint2 #Hcast #Htrace #Hle1346 normalize nodelta destruct whd in match (exec_cast ????);1347 normalize nodelta >intsize_eq_elim_true whd1348 >sz_eq_identity >sz_eq_identity whd try @conj try @conj1349 [ 3: elim (necessary_conditions_spec … (sym_eq … Hconditions))1350 [ 1: elim target_sz elim cast_sz normalize #Hlt try @I @(False_ind … Hlt)1351 | 2: * #Hcast_eq #_ >Hcast_eq elim target_sz // ]1352 | 2: @refl1353 | 1: @cast_composition //1354 elim (necessary_conditions_spec … (sym_eq … Hconditions)) (* Clearly suboptimal stuff in this mess *)1355 [ 1: elim target_sz elim cast_sz normalize #Hlt try @I @(False_ind … Hlt)1356 | 2: * #Hcast_eq #_ >Hcast_eq elim target_sz // ]1357 ]1358 ]1359 ]1360 ]1361 ]1460 | 1: * #castee_val #castee_trace #Hsmaller normalize nodelta 1461 lapply (exec_cast_inv castee_val src_sz src_sg cast_sz cast_sg m) 1462 cases (exec_cast m castee_val (Tint src_sz src_sg) (Tint cast_sz cast_sg)) 1463 [ 2: #error #_ @I 1464 | 1: #result #Hinversion elim (Hinversion result (refl ? (OK ? result))) 1465 #castee_int * #Hcastee_val_eq #Hresult_eq 1466 whd in match (m_bind ?????); 1467 #result_int #Hresult_eq2 1468 cases (exec_expr ge en m castee1) in Hsmaller; 1469 [ 2: #error normalize in ⊢ (% → ?); #Habsurd 1470 @(False_ind … (Habsurd castee_int Hcastee_val_eq)) 1471 | 1: * #val1 #trace1 whd in ⊢ (% → ?); normalize nodelta 1472 #Hsmaller elim (Hsmaller castee_int Hcastee_val_eq) 1473 #val1_int * * * #Hval1_eq #Hval1_int_eq #Hcastee_trace_eq 1474 destruct #Hle %{(cast_int_int src_sz src_sg target_sz castee_int)} 1475 try @conj try @conj try @conj try // 1476 [ 1: @cast_composition ] try assumption 1477 elim (necessary_conditions_spec … (sym_eq … Hconditions)) 1478 [ 2,4: * #Heq >Heq #_ elim target_sz // 1479 | 1,3: #Hlt @(size_lt_to_le ?? Hlt) ] 1480 ] ] ] ] ] 1362 1481 | 25,27: destruct 1363 1482 inversion (Hcast2 ge en m) … … 1365 1484 #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hresult_contr <Hresult_contr in Hresult; 1366 1485 #Hcontr destruct 1367 | 2,4: (* We successfuly cast the expression to the desired type. We can thus get rid of the "cast" itself. 1486 | 2,4: (* We successfuly cast the expression to the desired type. We can thus get rid of the "cast" itself. 1368 1487 We did not successfuly cast the subexpression to target_sz, though. *) 1369 1488 #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #_ #Hinv_eq … … 1375 1494 [ 2,4: (* erroneous evaluation of the original expression *) 1376 1495 #error #Hsmaller_eval @SimFail @(ex_intro … error) // 1377 | 1,3: * #val #trace 1378 cases (exec_expr ge en m castee2) 1379 [ 2,4: #error #Hsmaller_eval normalize in Hsmaller_eval; @(False_ind … Hsmaller_eval) 1380 | 1,3: * #val1 #trace1 #Hsmaller_eval elim (smaller_integer_val_spec … Hsmaller_eval) 1381 #int1 * #int2 * * * * #Hint1 #Hint2 #Hcast #Htrace #Hle 1382 @SimOk * #val2 #trace2 normalize nodelta >Htype_castee 1383 whd in match (exec_cast ????); 1384 cases val in Hint1; normalize nodelta 1385 [ 1,6: #Hint1 destruct | 3,4,5,8,9,10: #foo #Hint1 destruct 1386 | 2,7: destruct cases src_sz in int1; #int1 * #int2 #Hint1 1387 whd in match (intsize_eq_elim ???????); 1388 whd in match (m_bind ?????); 1389 [ 1,5,9,10,14,18: (* correct cases *) destruct #H @H 1390 | 2,3,4,6,7,8,11,12,13,15,16,17: #Habsurd destruct ] 1391 ] 1392 ] 1393 ] 1394 | 3,6: @SimFail /2 by refl, ex_intro/ 1395 ] 1396 ] 1496 | 1,3: * #val #trace normalize nodelta >Htype_castee 1497 lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m) 1498 cases (exec_cast m val (Tint src_sz src_sg) (Tint cast_sz cast_sg)) 1499 [ 2,4: #error #_ #_ @SimFail /2 by ex_intro/ 1500 | 1,3: #result #Hinversion elim (Hinversion result (refl ??)) 1501 #val_int * #Hval_eq #Hresult_eq 1502 cases (exec_expr ge en m castee2) 1503 [ 2,4: #error #Hsmaller_eval normalize in Hsmaller_eval; @(False_ind … (Hsmaller_eval val_int Hval_eq)) 1504 | 1,3: * #val1 #trace1 #Hsmaller elim (Hsmaller val_int Hval_eq) 1505 #val1_int * * * #Hval1_eq #Hcast_eq #Htrace_eq #Hle 1506 destruct @SimOk normalize #a #H @H ] 1507 ] ] 1508 | 3,6: @SimFail /2 by refl, ex_intro/ 1509 ] ] 1397 1510 | 26,28: destruct 1398 1511 inversion (Hcast2 ge en m) … … 1468 1581 cases (exec_expr ge en m iftrue) in Hsmaller_true; 1469 1582 [ 2: #error #_ @I 1470 | 1: * #val_true_branch #trace_true_branch 1583 | 1: * #val_true_branch #trace_true_branch #Hsmaller 1584 #val_true_branch #Hval_true_branch lapply Hsmaller -Hsmaller 1471 1585 cases (exec_expr ge en m iftrue1) 1472 [ 2: #error normalize in ⊢ (% → ?); #H @(False_ind … H)1473 | 1: * #val_true1_branch #trace_true1_branch #Hsmaller1474 elim (smaller_integer_val_spec … Hsmaller)1475 #true_val * #true1_val * * * * #Htrue_val #Htrue1_val #Hcast1476 # Htrace_eq #Hsize_le normalize nodelta destruct1477 whd in match (smaller_integer_val ?????);1478 >sz_eq_identity normalize nodelta1479 >sz_eq_identity normalize nodelta1480 try @conj try @conj // ]1481 ]1482 | 2: (* false branch taken. Same proof as above, different arguments ... *)1586 [ 2: #error normalize in ⊢ (% → ?); #Hsmaller 1587 @(False_ind … (Hsmaller val_true_branch Hval_true_branch)) 1588 | 1: * #val_true1_branch #trace_true1_branch #Hsmaller normalize nodelta 1589 elim (Hsmaller val_true_branch Hval_true_branch) 1590 #val_true1_int * * * #val_true1_branch #Hval_cast_eq #Htrace_eq #Hle 1591 %{val_true1_int} try @conj try @conj try @conj // 1592 ] ] 1593 | 2: (* false branch taken. Same proof as above, different arguments ... *) 1594 cut (false_src_sz = true_src_sz ∧ false_src_sg = true_src_sg) 1595 [ 1: >Htype_eq_true in Hiftrue_eq_iffalse; >Htype_eq_false #Htype_eq 1596 destruct (Htype_eq) @conj @refl ] * #Hsz_eq #Hsg_eq destruct 1483 1597 cases (exec_expr ge en m iffalse) in Hsmaller_false; 1484 1598 [ 2: #error #_ @I 1485 | 1: * #val_false_branch #trace_false_branch 1599 | 1: destruct * #val_false_branch #trace_false_branch #Hsmaller 1600 #val_false_branch #Hval_false_branch lapply Hsmaller -Hsmaller 1486 1601 cases (exec_expr ge en m iffalse1) 1487 [ 2: #error normalize in ⊢ (% → ?); #H @(False_ind … H) 1488 | 1: * #val_false1_branch #trace_false1_branch #Hsmaller 1489 elim (smaller_integer_val_spec … Hsmaller) 1490 #false_val * #false1_val * * * * #Hfalse_val #Hfalse1_val #Hcast 1491 #Htrace_eq #Hsize_le normalize nodelta destruct 1492 whd in match (smaller_integer_val ?????); 1493 cut (false_src_sz = true_src_sz ∧ false_src_sg = true_src_sg) 1494 [ 1: >Htype_eq_true in Hiftrue_eq_iffalse; >Htype_eq_false #Htype_eq 1495 destruct (Htype_eq) @conj @refl 1496 | 2: * #Hsize_eq #Hsg_eq destruct 1497 >sz_eq_identity normalize nodelta 1498 >sz_eq_identity normalize nodelta 1499 try @conj try @conj try @refl assumption 1500 ] 1501 ] 1502 ] 1503 ] 1504 ] 1505 ] 1506 ] 1507 ] 1508 ] 1509 ] 1602 [ 2: #error normalize in ⊢ (% → ?); #Hsmaller 1603 @(False_ind … (Hsmaller val_false_branch Hval_false_branch)) 1604 | 1: * #val_false1_branch #trace_false1_branch #Hsmaller normalize nodelta 1605 elim (Hsmaller val_false_branch Hval_false_branch) 1606 #val_false1_int * * * #val_false1_branch #Hval_cast_eq #Htrace_eq #Hle 1607 %{val_false1_int} try @conj try @conj try @conj // 1608 ] ] 1609 ] ] ] ] ] ] ] 1510 1610 | 38,39,40: destruct 1511 1611 elim (Hcond_equiv ge en m) * #Hsim_expr_cond #Hsim_vlalue_cond #Htype_cond_eq … … 1601 1701 @(Inv_coerce_ok ??????? target_sz target_sg) 1602 1702 [ 1,2: // 1603 | 3: cases target_sz cases target_sg normalize try @conj try @conj try @refl try @I]1703 | 3: @smaller_integer_val_identity ] 1604 1704 | 2: #Hneq >(type_neq_not_identity … Hneq) 1605 1705 %1 // @SimOk #a #H @H … … 1651 1751 cases (exec_expr ge en m e1) in Hsmaller; 1652 1752 [ 2: #error normalize // 1653 | 1: * #val1 #trace1 cases (exec_expr ge en m e2) 1654 [ 2: #error normalize in ⊢ (% → ?); #Habsurd @(False_ind … Habsurd) 1655 | 1: * #val2 #trace #Hsmaller 1656 elim (smaller_integer_val_spec … Hsmaller) 1657 #i1 * #i2 * * * * #Hval1 #Hval2 #Hcast #Htrace_eq #Hsize_le 1658 normalize nodelta destruct whd in match (smaller_integer_val ?????); 1659 >sz_eq_identity >sz_eq_identity normalize nodelta 1660 try @conj try @conj try @conj try @refl assumption 1753 | 1: * #val1 #trace1 #Hsmaller #val1_int #Hval1_eq 1754 cases (exec_expr ge en m e2) in Hsmaller; 1755 [ 2: #error normalize in ⊢ (% → ?); #Habsurd @(False_ind … (Habsurd val1_int Hval1_eq)) 1756 | 1: * #val2 #trace #Hsmaller elim (Hsmaller val1_int Hval1_eq) 1757 #val2_int * * * #Hval2_eq #Hcast #Htrace #Hle normalize nodelta 1758 %{val2_int} try @conj try @conj try @conj // 1661 1759 ] 1662 1760 ] … … 1780 1878 cases (exec_expr ge en m castee) in Hsmaller; 1781 1879 [ 2: #error #_ @SimFail /2 by ex_intro/ 1782 | 1: * #val #trace cases (exec_expr ge en m castee1) 1783 [ 2: #error #Habsurd @(False_ind … Habsurd) 1784 | 1: * #val1 #trace1 #Hsmaller elim (smaller_integer_val_spec … Hsmaller) 1785 #v1 * #v2 * * * * #Hval1 #Hval2 #Hcast #Htrace #Hle 1786 >Hsrc_type_eq normalize nodelta cases val in Hval1; 1787 [ 1: #Hval1 | 2: #sz #i #Hval1 | 3,4,5: #irrelevant #Hval1 ] 1788 [ 1,3,4,5: normalize @SimFail /2 by ex_intro/ ] 1789 whd in match (exec_cast ????); 1790 cases (sz_eq_dec sz src_sz) 1791 [ 2: #Hneq normalize nodelta 1792 >(intsize_eq_elim_false (res ?) sz src_sz ???? Hneq) 1793 @SimFail /2 by ex_intro/ 1794 | 1: #Heq <Heq normalize nodelta >intsize_eq_elim_true 1795 destruct normalize 1796 @SimOk #a #H @H 1880 | 1: * #val #trace normalize nodelta >Hsrc_type_eq 1881 lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m) 1882 cases (exec_cast m val ??) 1883 [ 2: #error #_ #_ @SimFail /2 by ex_intro/ 1884 | 1: #result #Hinversion elim (Hinversion result (refl ??)) 1885 #val_int * #Hval_eq #Hcast 1886 cases (exec_expr ge en m castee1) 1887 [ 2: #error #Habsurd normalize in Habsurd; @(False_ind … (Habsurd val_int Hval_eq)) 1888 | 1: * #val1 #trace1 #Hsmaller elim (Hsmaller val_int Hval_eq) 1889 #val1_int * * * #Hval1_int #Hval18int #Htrace #Hle 1890 @SimOk destruct normalize // ] 1797 1891 ] 1798 ] 1799 ] 1892 ] 1800 1893 | 2: @SimFail /2 by ex_intro/ 1801 1894 | 3: >Htarget_type_eq // … … 2046 2139 // qed. 2047 2140 2048 include "Clight/CexecInd.ma". 2141 2142 definition expr_lvalue_ind_combined ≝ 2143 λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx. 2144 conj ?? 2145 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx) 2146 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx). 2049 2147 2050 2148 lemma simulation_transitive : ∀A,r0,r1,r2. simulate A r0 r1 → simulate A r1 r2 → simulate A r0 r2. … … 3012 3110 whd in match (exec_step ??) in ⊢ (% → %); 3013 3111 #Habsurd destruct (Habsurd) 3014 ] qed. 3015 3112 ]
Note: See TracChangeset
for help on using the changeset viewer.
