Changeset 2572
 Timestamp:
 Jan 9, 2013, 1:23:29 PM (7 years ago)
 Location:
 src/Clight
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/frontend_misc.ma
r2565 r2572 326 326 (* Useful facts on blocks. *) 327 327 (*  *) 328 329 lemma eq_block_to_refl : ∀b1,b2. eq_block b1 b2 = true → b1 = b2. 330 #b1 #b2 @(eq_block_elim … b1 b2) 331 [ // 332  #_ #Habsurd destruct ] qed. 328 333 329 334 lemma not_eq_block : ∀b1,b2. b1 ≠ b2 → eq_block b1 b2 = false. 
src/Clight/memoryInjections.ma
r2569 r2572 388 388  3: #Habsurd destruct (Habsurd) 389 389  4: #p1 #p2 #Heq #Heqv #Heqv2 #_ destruct ] 390 qed. 390 qed. 391 392 lemma value_eq_null_inversion : 393 ∀E,v. value_eq E Vnull v → v = Vnull. 394 #E #v #Heq inversion Heq // 395 #p1 #p2 #Htranslate #Habsurd lapply (jmeq_to_eq ??? Habsurd) 396 #Habsurd' destruct 397 qed. 391 398 392 399 (* A cleaner version of inversion for [value_eq] *) … … 443 450 Zltb (block_id b) (nextblock m) = true ∧ 444 451 Zleb (low_bound m b) (Z_of_unsigned_bitvector ? (offv off)) = true ∧ 445 446 452 Zltb (Z_of_unsigned_bitvector ? (offv off)) (high_bound m b) = true. 447 453 #ty #m * #brg #bid #off #v 
src/Clight/toCminor.ma
r2568 r2572 405 405 [ aop_case_ii sz sg ⇒ 406 406 match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with 407 [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omodu …) e1 e2)408  Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (O mod…) e1 e2)407 [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oshru …) e1 e2) 408  Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oshr …) e1 e2) 409 409 ] 410 410 (* no float case *) … … 417 417 [ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I8 Unsigned sz sg) e) 418 418  _ ⇒ Error ? (msg TypeMismatch) 419 ]. 420 419 ]. 420 421 421 definition translate_cmp ≝ 422 422 λc,ty1,ty2,ty'. … … 457 457  Oxor ⇒ translate_misc_aop ty1 ty2 ty Oxor e1 e2 458 458  Oshl ⇒ translate_misc_aop ty1 ty2 ty Oshl e1 e2 459  Oshr ⇒ translate_shr ty1 ty2 ty e1 e2 459 (* Oshr ⇒ translate_misc_aop ty1 ty2 ty Oshr e1 e2 *) 460  Oshr ⇒ translate_shr ty1 ty2 ty e1 e2 (* split on signed/unsigned *) 460 461  Oeq ⇒ translate_cmp Ceq ty1 ty2 ty e1 e2 461 462  One ⇒ translate_cmp Cne ty1 ty2 ty e1 e2 
src/Clight/toCminorCorrectness.ma
r2569 r2572 359 359 qed. 360 360 361 include "Clight/CexecSound.ma".362 363 361 lemma lookup_exec_alloc : 364 362 ∀source_variables, initial_env, env, var_id, clb, m, m'. … … 593 591 qed. 594 592 593 (* 594 lemma classify_cmp_inversion : 595 ∀ty1,ty2. 596 if_type_eq ty1 ty2 (λty1, ty2. classify_cmp_cases ty1 ty2) 597 ((∃sz,sg. ty1 = Tint sz sg ∧ ty2 = ty1 ∧ classify_cmp ty1 ty2 = cmp_case_ii sz sg) ∨ 598 (∃ty'. ty1 = Tpointer ty' ∧ ty2 = ty1 ∧ classify_cmp ty1 ty2 = cmp_case_pp (None ?) ty') ∨ 599 (∃ty',n'. ty1 = Tarray ty' n' ∧ ty2 = ty1 ∧ classify_cmp ty1 ty2 = cmp_case_pp (Some ? n') ty') ∨ 600 (classify_cmp ty1 ty2 = cmp_default …) 601 *) 602 595 603 lemma classify_aop_inversion : 596 604 ∀ty1,ty2. … … 762 770 qed. 763 771 772 lemma sem_mod_inversion_s : 773 ∀sz. 774 ∀v1,v2,res. 775 sem_mod v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res → 776 ∃sz',i1,i2. v1 = Vint sz' i1 ∧ v2 = Vint sz' i2 ∧ 777 match modulus_s ? i1 i2 with 778 [ Some q ⇒ res = (Vint sz' q) 779  None ⇒ False ]. 780 #sz * 781 [  #sz' #i'   #p' ] 782 #v2 #res 783 whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??); 784 >type_eq_dec_true normalize nodelta 785 #H destruct 786 cases v2 in H; normalize nodelta 787 [  #sz2' #i2'   #p2' ] 788 #Heq destruct 789 %{sz'} 790 lapply Heq Heq 791 cases sz' in i'; #i' 792 whd in match (intsize_eq_elim ???????); 793 cases sz2' in i2'; #i2' normalize nodelta 794 whd in match (option_map ????); #Hdiv destruct 795 %{i'} %{i2'} @conj try @conj try @conj try @refl 796 cases (modulus_s ???) in Hdiv; 797 [ 2,4,6: #bv ] normalize #H destruct (H) try @refl 798 qed. 799 800 lemma sem_mod_inversion_u : 801 ∀sz. 802 ∀v1,v2,res. 803 sem_mod v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res → 804 ∃sz',i1,i2. v1 = Vint sz' i1 ∧ v2 = Vint sz' i2 ∧ 805 match modulus_u ? i1 i2 with 806 [ Some q ⇒ res = (Vint sz' q) 807  None ⇒ False ]. 808 #sz * 809 [  #sz' #i'   #p' ] 810 #v2 #res 811 whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??); 812 >type_eq_dec_true normalize nodelta 813 #H destruct 814 cases v2 in H; normalize nodelta 815 [  #sz2' #i2'   #p2' ] 816 #Heq destruct 817 %{sz'} 818 lapply Heq Heq 819 cases sz' in i'; #i' 820 whd in match (intsize_eq_elim ???????); 821 cases sz2' in i2'; #i2' normalize nodelta 822 whd in match (option_map ????); #Hdiv destruct 823 %{i'} %{i2'} @conj try @conj try @conj try @refl 824 cases (modulus_u ???) in Hdiv; 825 [ 2,4,6: #bv ] normalize #H destruct (H) try @refl 826 qed. 827 828 lemma sem_and_inversion : 829 ∀v1,v2,res. 830 sem_and v1 v2 = Some ? res → 831 ∃sz',i1,i2. v1 = Vint sz' i1 ∧ v2 = Vint sz' i2 ∧ 832 res = Vint sz' (conjunction_bv ? i1 i2). 833 * 834 [  #sz' #i'   #p' ] 835 #v2 #res 836 whd in ⊢ ((??%?) → ?); 837 #H destruct 838 cases v2 in H; normalize nodelta 839 [  #sz2' #i2'   #p2' ] 840 #Heq destruct 841 %{sz'} 842 lapply Heq Heq 843 cases sz' in i'; #i' 844 whd in match (intsize_eq_elim ???????); 845 cases sz2' in i2'; #i2' normalize nodelta 846 #H destruct 847 %{i'} %{i2'} @conj try @conj try @conj try @refl 848 qed. 849 850 lemma sem_or_inversion : 851 ∀v1,v2,res. 852 sem_or v1 v2 = Some ? res → 853 ∃sz',i1,i2. v1 = Vint sz' i1 ∧ v2 = Vint sz' i2 ∧ 854 res = Vint sz' (inclusive_disjunction_bv ? i1 i2). 855 * 856 [  #sz' #i'   #p' ] 857 #v2 #res 858 whd in ⊢ ((??%?) → ?); 859 #H destruct 860 cases v2 in H; normalize nodelta 861 [  #sz2' #i2'   #p2' ] 862 #Heq destruct 863 %{sz'} 864 lapply Heq Heq 865 cases sz' in i'; #i' 866 whd in match (intsize_eq_elim ???????); 867 cases sz2' in i2'; #i2' normalize nodelta 868 #H destruct 869 %{i'} %{i2'} @conj try @conj try @conj try @refl 870 qed. 871 872 lemma sem_xor_inversion : 873 ∀v1,v2,res. 874 sem_xor v1 v2 = Some ? res → 875 ∃sz',i1,i2. v1 = Vint sz' i1 ∧ v2 = Vint sz' i2 ∧ 876 res = Vint sz' (exclusive_disjunction_bv ? i1 i2). 877 * 878 [  #sz' #i'   #p' ] 879 #v2 #res 880 whd in ⊢ ((??%?) → ?); 881 #H destruct 882 cases v2 in H; normalize nodelta 883 [  #sz2' #i2'   #p2' ] 884 #Heq destruct 885 %{sz'} 886 lapply Heq Heq 887 cases sz' in i'; #i' 888 whd in match (intsize_eq_elim ???????); 889 cases sz2' in i2'; #i2' normalize nodelta 890 #H destruct 891 %{i'} %{i2'} @conj try @conj try @conj try @refl 892 qed. 893 894 lemma sem_shl_inversion : 895 ∀v1,v2,res. 896 sem_shl v1 v2 = Some ? res → 897 ∃sz1,sz2,i1,i2. 898 v1 = Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧ 899 res = Vint sz1 (shift_left bool (bitsize_of_intsize sz1) 900 (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false) ∧ 901 lt_u (bitsize_of_intsize sz2) i2 902 (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true. 903 * 904 [  #sz' #i'   #p' ] 905 #v2 #res 906 whd in ⊢ ((??%?) → ?); 907 #H destruct 908 cases v2 in H; normalize nodelta 909 [  #sz2' #i2'   #p2' ] 910 #Heq destruct 911 %{sz'} %{sz2'} 912 lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres 913 %{i'} %{i2'} 914 >Hlt_u destruct (Hres) @conj try @conj try @conj try @refl 915 qed. 916 917 lemma sem_shr_inversion : 918 ∀v1,v2,sz,sg,res. 919 sem_shr v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res → 920 ∃sz1,sz2,i1,i2. 921 v1 = Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧ 922 lt_u (bitsize_of_intsize sz2) i2 923 (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true ∧ 924 match sg with 925 [ Signed ⇒ 926 res = 927 (Vint sz1 928 (shift_right bool (7+pred_size_intsize sz1*8) 929 (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 930 (head' bool (7+pred_size_intsize sz1*8) i1))) 931  Unsigned ⇒ 932 res = 933 (Vint sz1 934 (shift_right bool (7+pred_size_intsize sz1*8) 935 (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false)) 936 ]. 937 * 938 [  #sz' #i'   #p' ] 939 #v2 #sz * #res 940 whd in ⊢ ((??%?) → ?); 941 whd in match (classify_aop ??); 942 >type_eq_dec_true normalize nodelta 943 #H destruct 944 cases v2 in H; normalize nodelta 945 [  #sz2' #i2'   #p2' 946   #sz2' #i2'   #p2' ] 947 #Heq destruct 948 %{sz'} %{sz2'} 949 lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres 950 %{i'} %{i2'} 951 >Hlt_u destruct (Hres) @conj try @conj try @conj try @refl 952 qed. 953 954 lemma complete_cmp_inversion : 955 ∀ty:type. 956 ∀e:expr (ASTint I8 Unsigned). 957 ∀r:expr (typ_of_type ty). 958 complete_cmp ty e = return r → 959 ∃sz,sg. ty = Tint sz sg ∧ 960 r ≃ Op1 (ASTint I8 Unsigned) (ASTint sz sg) (Ocastint I8 Unsigned sz sg) e. 961 * 962 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 963  #structname #fieldspec  #unionname #fieldspec  #id ] 964 #e whd in match (typ_of_type ?); 965 #r whd in ⊢ ((??%%) → ?); 966 #H destruct 967 %{sz} %{sg} @conj try @refl @refl_jmeq 968 qed. 969 970 971 lemma sem_cmp_int_inversion : 972 ∀v1,v2,sz,sg,op,m,res. 973 sem_cmp op v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? res → 974 ∃sz,i1,i2. v1 = Vint sz i1 ∧ 975 v2 = Vint sz i2 ∧ 976 match sg with 977 [ Unsigned ⇒ of_bool (cmpu_int ? op i1 i2) = res 978  Signed ⇒ of_bool (cmp_int ? op i1 i2) = res 979 ]. 980 #v1 #v2 #sz0 #sg #op * #contents #next #Hnext #res 981 whd in ⊢ ((??%?) → ?); 982 whd in match (classify_cmp ??); >type_eq_dec_true normalize nodelta 983 cases v1 984 [  #sz #i   #p ] normalize nodelta 985 #H destruct 986 cases v2 in H; 987 [  #sz' #i'   #p' ] normalize nodelta 988 #H destruct lapply H H 989 cases sz in i; #i 990 cases sz' in i'; #i' cases sg normalize nodelta 991 whd in match (intsize_eq_elim ???????); #H destruct 992 [ 1,2: %{I8} 993  3,4: %{I16} 994  5,6: %{I32} ] 995 %{i} %{i'} @conj try @conj try @refl 996 qed. 997 998 lemma typ_of_ptr_type : ∀ty',n. typ_of_type (ptr_type ty' n) = ASTptr. 999 #ty' * // qed. 1000 1001 lemma sem_cmp_ptr_inversion : 1002 ∀v1,v2,ty',n,op,m,res. 1003 sem_cmp op v1 (ptr_type ty' n) v2 (ptr_type ty' n) m = Some ? res → 1004 (∃p1,p2. v1 = Vptr p1 ∧ v2 = Vptr p2 ∧ 1005 valid_pointer m p1 = true ∧ 1006 valid_pointer m p2 = true ∧ 1007 (if eq_block (pblock p1) (pblock p2) 1008 then Some ? (of_bool (cmp_offset op (poff p1) (poff p2))) 1009 else sem_cmp_mismatch op) = Some ? res) ∨ 1010 (∃p1. v1 = Vptr p1 ∧ v2 = Vnull ∧ sem_cmp_mismatch op = Some ? res) ∨ 1011 (∃p2. v1 = Vnull ∧ v2 = Vptr p2 ∧ sem_cmp_mismatch op = Some ? res) ∨ 1012 (v1 = Vnull ∧ v2 = Vnull ∧ sem_cmp_match op = Some ? res). 1013 * [  #sz #i   #p ] normalize nodelta 1014 #v2 #ty' #n #op 1015 * #contents #nextblock #Hnextblock #res whd in ⊢ ((??%?) → ?); 1016 whd in match (classify_cmp ??); cases n normalize nodelta 1017 [ 2,4,6,8: #array_len ] 1018 whd in match (ptr_type ty' ?); 1019 whd in match (if_type_eq ?????); 1020 >type_eq_dec_true normalize nodelta 1021 #H destruct 1022 cases v2 in H; normalize nodelta 1023 [  #sz' #i'   #p' 1024   #sz' #i'   #p' 1025   #sz' #i'   #p' 1026   #sz' #i'   #p' ] 1027 #H destruct 1028 try /6 by or_introl, or_intror, ex_intro, conj/ 1029 [ 1: %1 %1 %2 %{p} @conj try @conj // 1030  3: %1 %1 %2 %{p} @conj try @conj // 1031  *: %1 %1 %1 %{p} %{p'} 1032 cases (valid_pointer (mk_mem ???) p) in H; normalize nodelta 1033 cases (valid_pointer (mk_mem contents nextblock Hnextblock) p') normalize nodelta #H 1034 try @conj try @conj try @conj try @conj try @conj try @refl try @H 1035 destruct 1036 ] qed. 1037 1038 lemma pointer_translation_eq_block : 1039 ∀E,p1,p2,p1',p2'. 1040 pointer_translation p1 E = Some ? p1' → 1041 pointer_translation p2 E = Some ? p2' → 1042 eq_block (pblock p1) (pblock p2) = true → 1043 eq_block (pblock p1') (pblock p2') = true. 1044 #E * #b1 #o1 * #b2 #o2 * #b1' #o1' * #b2' #o2' 1045 #H1 #H2 #Heq_block 1046 lapply (eq_block_to_refl … Heq_block) #H destruct (H) 1047 lapply H1 lapply H2 H1 H2 1048 whd in ⊢ ((??%?) → (??%?) → ?); 1049 cases (E b2) normalize nodelta 1050 [ #Habsurd destruct ] 1051 * #bx #ox normalize nodelta #Heq1 #Heq2 destruct 1052 @eq_block_b_b 1053 qed. 1054 1055 lemma pointer_translation_cmp_offset : 1056 ∀E,p1,p2,p1',p2',op. 1057 pblock p1 = pblock p2 → 1058 pointer_translation p1 E = Some ? p1' → 1059 pointer_translation p2 E = Some ? p2' → 1060 cmp_offset op (poff p1) (poff p2) = cmp_offset op (poff p1') (poff p2'). 1061 #E * #b1 #o1 * #b2 #o2 * #b1' #o1' * #b2' #o2' #op #Heq destruct 1062 whd in ⊢ ((??%?) → (??%?) → ?); 1063 cases (E b2) normalize nodelta 1064 [ #H destruct ] 1065 * #bx #ox normalize nodelta 1066 #Heq1 #Heq2 destruct cases op 1067 [ @sym_eq @eq_offset_translation 1068  @sym_eq @neq_offset_translation 1069  @cthulhu (* !!!! TODO !!!! *) 1070  @cthulhu (* !!!! TODO !!!! *) 1071  @cthulhu (* !!!! TODO !!!! *) 1072  @cthulhu (* !!!! TODO !!!! *) 1073 ] qed. 1074 1075 (* The two following lemmas are just noise. *) 1076 764 1077 lemma expr_vars_fix_ptr_type : 765 1078 ∀ty',optlen. … … 780 1093 qed. 781 1094 782 (* This lemma is just noise. *)783 1095 lemma eval_expr_rewrite_aux : 784 1096 ∀genv. … … 811 1123 a sign extension on i in expressions (ptr + i) whereas Cminor case splits on 812 1124 the sign of i, producing either a sign extension or a zero extension. 1125 3) something similar to 1) happens for binary comparison operators. Clight generates 1126 systematically a 32 bit value for the outcome of the comparison and lives with it, 1127 but toCminor actually generates something 8 bit and casts it back to the context type. 1128 4) we need some proof that we don't blow the stack during the transformation. Otherwise, 1129 a problem appears when we prove semantics preservation for pointer < comparison 1130 (we might wrap up the rhs and end SNAFU). 813 1131 *) 814 1132 lemma eval_expr_sim : … … 1056 1374 >intsize_eq_elim_true #Heq destruct (Heq) 1057 1375 %2 1058  4 : (* div *)1376  4,5: (* div *) 1059 1377 lapply (classify_aop_inversion (typeof e1) (typeof e2)) * 1060 1378 [ 2,4: #Hclassify >Hclassify normalize nodelta … … 1072 1390 whd in match (typ_of_type (Tint ??)); 1073 1391 #lhs #rhs #Htyp_should_eq 1074 [ cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq)1075  cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ]1392 [ 1,3: cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq) 1393  2,4: cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ] 1076 1394 Htyp_should_eq 1077 1395 #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') Heq_e' #Heq_e' … … 1102 1420 whd in match (eval_binop ???????); 1103 1421 whd in Hsem_binary:(??%?); 1104 lapply (div_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) 1105 * #cm_val * #Hsem_binary_translated #Hvalue_eq_res 1106 [ cases (sem_div_inversion_s … Hsem_binary) 1107  cases (sem_div_inversion_u … Hsem_binary) ] 1422 [ 1,3: (* div*) 1423 lapply (div_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) 1424 * #cm_val * #Hsem_binary_translated #Hvalue_eq_res 1425 [ cases (sem_div_inversion_s … Hsem_binary) 1426  cases (sem_div_inversion_u … Hsem_binary) ] 1427  2,4: (* mod *) 1428 lapply (mod_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) 1429 * #cm_val * #Hsem_binary_translated #Hvalue_eq_res 1430 [ cases (sem_mod_inversion_s … Hsem_binary) 1431  cases (sem_mod_inversion_u … Hsem_binary) ] 1432 ] 1108 1433 #cm_vsz * #cm_lhs_v * #cm_rhs_v * * 1109 1434 #Hcm_lhs #Hcm_rhs #Hcm_val … … 1112 1437 >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta 1113 1438 >intsize_eq_elim_true normalize nodelta 1114 [ cases (division_s ???) in Hcm_val; normalize nodelta 1115 [ @False_ind 1116  #i #Hcl_val destruct (Hcl_val) %{(Vint cm_vsz i)} @conj try @refl %2 ] 1117  cases (division_u ???) in Hcm_val; normalize nodelta 1118 [ @False_ind 1119  #i #Hcl_val destruct (Hcl_val) %{(Vint cm_vsz i)} @conj try @refl %2 ] ] 1120  5: (* mod *) @cthulhu 1121  6: (* and *) @cthulhu 1122  7: (* or *) @cthulhu 1123  8: (* xor *) @cthulhu 1124  9: (* shl *) @cthulhu 1125  10: (* shr *) @cthulhu 1126  11: (* eq *) @cthulhu 1127  12: (* ne *) @cthulhu 1128  13: (* lt *) @cthulhu 1129  14: (* gt *) @cthulhu 1130  15: (* le *) @cthulhu 1131  16: (* ge *) @cthulhu ] 1439 [ cases (division_s ???) in Hcm_val; 1440  cases (division_u ???) in Hcm_val; 1441  cases (modulus_s ???) in Hcm_val; 1442  cases (modulus_u ???) in Hcm_val; ] 1443 normalize nodelta 1444 [ 1,3,5,7: @False_ind ] 1445 #i #Hcl_val destruct (Hcl_val) %{(Vint cm_vsz i)} @conj try @refl %2 1446  6,7,8: (* and,or,xor *) 1447 lapply (classify_aop_inversion (typeof e1) (typeof e2)) * 1448 [ 2,4,6: #Hclassify >Hclassify normalize nodelta 1449 #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ] 1450 lapply e' e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 1451 whd in match (typeof ?); #e' 1452 * #sz * #sg * * 1453 whd in match (typeof ?) in ⊢ (% → % → ?); 1454 #Htypeof_e1 #Htypeof_e2 1455 >Htypeof_e1 >Htypeof_e2 1456 whd in match (typeof ?) in ⊢ (% → % → % → ?); 1457 #Hclassify 1458 lapply (jmeq_to_eq ??? Hclassify) Hclassify #Hclassify >Hclassify 1459 normalize nodelta 1460 whd in match (typ_of_type (Tint ??)); 1461 #lhs #rhs #Htyp_should_eq 1462 cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq) 1463 Htyp_should_eq 1464 #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') Heq_e' #Heq_e' 1465 <Heq_e' Heq_e' 1466 #Hexec 1467 #Hexpr_vars_rhs #Hexpr_vars_lhs 1468 #Htranslate_rhs #Htranslate_lhs 1469 * #Hyp_present_lhs #Hyp_present_rhs 1470 #Hind_rhs #Hind_lhs 1471 cases (bind_inversion ????? Hexec) Hexec 1472 * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec 1473 cases (bind_inversion ????? Hexec) Hexec 1474 * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec 1475 cases (bind_inversion ????? Hexec) Hexec 1476 #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 1477 lapply (opt_to_res_inversion ???? Hsem) Hsem 1478 whd in match (typeof ?); whd in match (typeof ?); 1479 #Hsem_binary 1480 lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs) 1481 * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs Hind_rhs 1482 lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs) 1483 * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs Hind_lhs 1484 whd in match (eval_expr ???????); 1485 whd in match (proj1 ???); 1486 >Heval_lhs normalize nodelta 1487 >Heval_rhs normalize nodelta 1488 whd in match (m_bind ?????); 1489 whd in match (eval_binop ???????); 1490 whd in Hsem_binary:(??%?); 1491 [ 1: (* and *) 1492 lapply (and_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) 1493 * #cm_val * #Hsem_binary_translated #Hvalue_eq_res 1494 cases (sem_and_inversion … Hsem_binary) 1495  2: (* or *) 1496 lapply (or_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) 1497 * #cm_val * #Hsem_binary_translated #Hvalue_eq_res 1498 cases (sem_or_inversion … Hsem_binary) 1499  3: (* xor *) 1500 lapply (xor_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) 1501 * #cm_val * #Hsem_binary_translated #Hvalue_eq_res 1502 cases (sem_xor_inversion … Hsem_binary) 1503 ] 1504 #cm_vsz * #cm_lhs_v * #cm_rhs_v * * 1505 #Hcm_lhs #Hcm_rhs #Hcm_val 1506 destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta 1507 >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta 1508 >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta 1509 >intsize_eq_elim_true normalize nodelta 1510 [ 1: %{(Vint cm_vsz (conjunction_bv … cm_lhs_v cm_rhs_v))} 1511  2: %{(Vint cm_vsz (inclusive_disjunction_bv … cm_lhs_v cm_rhs_v))} 1512  3: %{(Vint cm_vsz (exclusive_disjunction_bv … cm_lhs_v cm_rhs_v))} 1513 ] 1514 @conj try @refl >Hcm_val %2 1515  9,10: (* shl, shr *) 1516 lapply (classify_aop_inversion (typeof e1) (typeof e2)) * 1517 [ 2,4: #Hclassify >Hclassify normalize nodelta 1518 #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ] 1519 lapply e' e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 1520 whd in match (typeof ?); #e' 1521 * #sz * * * * 1522 whd in match (typeof ?) in ⊢ (% → % → ?); 1523 #Htypeof_e1 #Htypeof_e2 1524 >Htypeof_e1 >Htypeof_e2 1525 whd in match (typeof ?) in ⊢ (% → % → % → ?); 1526 #Hclassify 1527 lapply (jmeq_to_eq ??? Hclassify) Hclassify #Hclassify >Hclassify 1528 normalize nodelta 1529 whd in match (typ_of_type (Tint ??)); 1530 #lhs #rhs #Htyp_should_eq 1531 [ 1,3: cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq) 1532  2,4: cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ] 1533 Htyp_should_eq 1534 #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') Heq_e' #Heq_e' 1535 <Heq_e' Heq_e' 1536 #Hexec 1537 #Hexpr_vars_rhs #Hexpr_vars_lhs 1538 #Htranslate_rhs #Htranslate_lhs 1539 * #Hyp_present_lhs #Hyp_present_rhs 1540 #Hind_rhs #Hind_lhs 1541 cases (bind_inversion ????? Hexec) Hexec 1542 * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec 1543 cases (bind_inversion ????? Hexec) Hexec 1544 * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec 1545 cases (bind_inversion ????? Hexec) Hexec 1546 #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 1547 lapply (opt_to_res_inversion ???? Hsem) Hsem 1548 whd in match (typeof ?); whd in match (typeof ?); 1549 #Hsem_binary 1550 lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs) 1551 * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs Hind_rhs 1552 lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs) 1553 * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs Hind_lhs 1554 whd in match (eval_expr ???????); 1555 whd in match (proj1 ???); 1556 >Heval_lhs normalize nodelta 1557 >Heval_rhs normalize nodelta 1558 whd in match (m_bind ?????); 1559 whd in match (eval_binop ???????); 1560 whd in Hsem_binary:(??%?); 1561 [ 1,3: (* shl *) 1562 lapply (shl_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) 1563 * #cm_val * #Hsem_binary_translated #Hvalue_eq_res 1564 cases (sem_shl_inversion … Hsem_binary) 1565 #sz1 * #sz2 * #lhs_i * #rhs_i * * * 1566 #Hcl_lhs #Hcl_rhs #Hcl_val #Hshift_ok 1567 destruct (Hcl_lhs Hcl_rhs) 1568 >(value_eq_int_inversion … Hvalue_eq_lhs) 1569 >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta 1570 >Hshift_ok normalize nodelta 1571 %{(Vint sz1 1572 (shift_left bool (bitsize_of_intsize sz1) 1573 (nat_of_bitvector (bitsize_of_intsize sz2) rhs_i) lhs_i false))} 1574 @conj try @refl >Hcl_val %2 1575  *: (* shr, translated to mod /!\ *) 1576 lapply (shr_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) 1577 * #cm_val * #Hsem_binary_translated #Hvalue_eq_res 1578 cases (sem_shr_inversion … Hsem_binary) normalize nodelta 1579 #sz1 * #sz2 * #lhs_i * #rhs_i * * * 1580 #Hcl_lhs #Hcl_rhs #Hshift_ok #Hcl_val 1581 destruct (Hcl_lhs Hcl_rhs) 1582 >(value_eq_int_inversion … Hvalue_eq_lhs) 1583 >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta 1584 >Hshift_ok normalize nodelta >Hcl_val 1585 /3 by ex_intro, conj, vint_eq/ ] 1586  *: (* comparison operators *) 1587 lapply e' e' 1588 cases e1 #ed1 #ety1 1589 cases e2 #ed2 #ety2 1590 whd in match (typeof ?) in ⊢ (% → % → % → %); 1591 #cm_expr whd in match (typeof ?); 1592 inversion (classify_cmp ety1 ety2) 1593 [ 3,6,9,12,15,18: #ety1' #ety2' #Hety1 #Hety2 1594 lapply (jmeq_to_eq ??? Hety1) #Hety1' 1595 lapply (jmeq_to_eq ??? Hety1) #Hety2' 1596 destruct #Hclassify >Hclassify normalize nodelta 1597 #cmexpr1 #cmexpr2 1598 whd in ⊢ ((???%) → ?); 1599 #Heq destruct (Heq) 1600  1,4,7,10,13,16: 1601 #sz #sg #Hety1 #Hety2 #Hclassify 1602 lapply (jmeq_to_eq ??? Hety1) #Hety1' 1603 lapply (jmeq_to_eq ??? Hety1) #Hety2' destruct 1604 >(jmeq_to_eq ??? Hclassify) Hclassify normalize nodelta 1605 whd in match (typeof ?) in ⊢ (% → % → % → %); 1606 whd in match (typ_of_type ?) in ⊢ (% → % → ?); 1607 cases sg #cmexpr1 #cmexpr2 normalize nodelta 1608 #Hcast_to_bool #Hexec_expr 1609 cases (complete_cmp_inversion … Hcast_to_bool) Hcast_to_bool 1610 #tysz * #tysg * #Htyis_int #Hcm_expr_aux 1611 destruct (Htyis_int) 1612 lapply (jmeq_to_eq ??? Hcm_expr_aux) #Hcm_expr Hcm_expr_aux 1613 destruct (Hcm_expr) 1614 cases (bind_inversion ????? Hexec_expr) Hexec_expr 1615 * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec 1616 cases (bind_inversion ????? Hexec) Hexec 1617 * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec 1618 cases (bind_inversion ????? Hexec) Hexec 1619 #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 1620 lapply (opt_to_res_inversion ???? Hsem) Hsem 1621 whd in match (typeof ?); whd in match (sem_binary_operation ??????); 1622 #Hsem_cmp lapply (sem_cmp_int_inversion … Hsem_cmp) Hsem_cmp 1623 * #vsz * #lhs_val * #rhs_val * * #Hcl_lhs #Hcl_rhs normalize nodelta 1624 destruct (Hcl_lhs) destruct (Hcl_rhs) 1625 #Heq_bool whd in match (typ_of_type ?) in ⊢ (% → % → % → %); 1626 #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs 1627 * #Hyp_present_lhs #Hyp_present_rhs 1628 #Hind_rhs #Hind_lhs 1629 lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs) 1630 * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs Hind_rhs 1631 lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs) 1632 * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs Hind_lhs 1633 whd in match (eval_expr ???????); 1634 whd in match (eval_expr ???????); 1635 >Heval_lhs normalize nodelta 1636 >Heval_rhs normalize nodelta 1637 whd in match (m_bind ?????); 1638 whd in match (eval_binop ???????); 1639 >(value_eq_int_inversion … Hvalue_eq_lhs) 1640 >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta 1641 >intsize_eq_elim_true normalize nodelta 1642 destruct (Heq_bool) 1643 whd in match (eval_unop ????); 1644 whd in match (opt_to_res ???); 1645 whd in match (m_bind ?????); 1646 (* finished modulo glitch in integer widths *) 1647 @cthulhu 1648  *: 1649 #n #ty' #Hety1 #Hety2 #Hclassify 1650 lapply (jmeq_to_eq ??? Hety1) #Hety1' 1651 lapply (jmeq_to_eq ??? Hety1) #Hety2' destruct 1652 >(jmeq_to_eq ??? Hclassify) Hclassify normalize nodelta 1653 whd in match (typeof ?) in ⊢ (% → % → % → %); 1654 #cmexpr1 #cmexpr2 1655 #Hcast_to_bool #Hexec_expr 1656 cases (complete_cmp_inversion … Hcast_to_bool) Hcast_to_bool 1657 #tysz * #tysg * #Htyis_int #Hcm_expr_aux 1658 destruct (Htyis_int) 1659 lapply (jmeq_to_eq ??? Hcm_expr_aux) #Hcm_expr Hcm_expr_aux 1660 destruct (Hcm_expr) 1661 cases (bind_inversion ????? Hexec_expr) Hexec_expr 1662 * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec 1663 cases (bind_inversion ????? Hexec) Hexec 1664 * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec 1665 cases (bind_inversion ????? Hexec) Hexec 1666 #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 1667 lapply (opt_to_res_inversion ???? Hsem) Hsem 1668 whd in match (typeof ?); whd in match (sem_binary_operation ??????); 1669 #Hsem_cmp lapply (sem_cmp_ptr_inversion … Hsem_cmp) Hsem_cmp 1670 * 1671 [ 2,4,6,8,10,12: 1672 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct 1673  *: * 1674 [ 2,4,6,8,10,12: 1675 * #p2 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct 1676  *: * 1677 [ 2,4,6,8,10,12: 1678 * #p1 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct 1679  *: * #p1 * #p2 * * * * #Hcl_lhs #Hcl_rhs #Hvalid_p1 #Hvalid_p2 #Heq_block_outcome destruct 1680 ] ] ] 1681 1682 (* #Heq_bool whd in match (typ_of_type ?) in ⊢ (% → % → % → %); *) 1683 #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs 1684 * #Hyp_present_lhs #Hyp_present_rhs 1685 #Hind_rhs #Hind_lhs 1686 lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs) 1687 * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs Hind_rhs 1688 lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs) 1689 * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs Hind_lhs 1690 whd in match (eval_expr ???????); 1691 whd in match (eval_expr ???????); 1692 >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta 1693 >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta 1694 whd in match (m_bind ?????); 1695 Heval_lhs Heval_rhs Hyp_present_rhs Hyp_present_lhs 1696 Hexpr_vars_lhs Hexpr_vars_rhs 1697 whd in match (eval_binop ???????); 1698 [ 1,2,3,4,5,6: 1699 whd in Hsem_cmp:(??%?); destruct (Hsem_cmp) 1700 >(value_eq_null_inversion … Hvalue_eq_lhs) 1701 >(value_eq_null_inversion … Hvalue_eq_rhs) normalize nodelta 1702 whd in match (eval_unop ????); 1703 whd in match (opt_to_res ???); 1704 whd in match (m_bind ?????); 1705 (* same glitch with integer widths *) 1706 @cthulhu 1707  7,8,9,10,11,12: 1708 whd in Hsem_cmp:(??%?); destruct (Hsem_cmp) 1709 >(value_eq_null_inversion … Hvalue_eq_lhs) normalize nodelta 1710 cases (value_eq_ptr_inversion … Hvalue_eq_rhs) #p2' 1711 * #Hcm_rhs_val #Hpointer_translation >Hcm_rhs_val normalize nodelta 1712 whd in match (eval_unop ????); 1713 whd in match (opt_to_res ???); 1714 whd in match (m_bind ?????); 1715 (* same glitch with integer widths *) 1716 @cthulhu 1717  13,14,15,16,17,18: 1718 whd in Hsem_cmp:(??%?); destruct (Hsem_cmp) 1719 >(value_eq_null_inversion … Hvalue_eq_rhs) normalize nodelta 1720 cases (value_eq_ptr_inversion … Hvalue_eq_lhs) #p1' 1721 * #Hcm_lhs_val #Hpointer_translation >Hcm_lhs_val normalize nodelta 1722 whd in match (eval_unop ????); 1723 whd in match (opt_to_res ???); 1724 whd in match (m_bind ?????); 1725 (* same glitch with integer widths *) 1726 @cthulhu 1727  *: 1728 cases (value_eq_ptr_inversion … Hvalue_eq_lhs) #p1' * #Hcm_lhs #Hptr_translation_lhs 1729 cases (value_eq_ptr_inversion … Hvalue_eq_rhs) #p2' * #Hcm_rhs #Hptr_translation_rhs 1730 destruct (Hcm_lhs Hcm_rhs) normalize nodelta 1731 Hvalue_eq_lhs Hvalue_eq_rhs Hexec_lhs Hexec_rhs 1732 >(mi_valid_pointers … Hinj … Hvalid_p1 … Hptr_translation_lhs) 1733 >(mi_valid_pointers … Hinj … Hvalid_p2 … Hptr_translation_rhs) normalize nodelta 1734 lapply Heq_block_outcome Heq_block_outcome 1735 @(match eq_block (pblock p1) (pblock p2) 1736 return λb. (eq_block (pblock p1) (pblock p2)) = b → ? 1737 with 1738 [ true ⇒ λH. ? 1739  false ⇒ λH. ? 1740 ] (refl ? (eq_block (pblock p1) (pblock p2)))) normalize nodelta 1741 [ 1,3,5,7,9,11: 1742 (* block equality in the Clight memory *) 1743 (* entails block equality in the Cminor memory *) 1744 >(pointer_translation_eq_block … Hptr_translation_lhs Hptr_translation_rhs H) normalize nodelta 1745 #Hsem_cmp whd in Hsem_cmp:(??%?); destruct (Hsem_cmp) 1746 whd in match (eval_unop ????); 1747 whd in match (opt_to_res ???); 1748 whd in match (m_bind ?????); 1749 (* TODO !!! In order to finish this, we need an invariant on the fact that we don't blow the stack during 1750 * transformation *) 1751 @cthulhu 1752  *: (* TBF. In the case of block inequality, we will have to use the no_aliasing property of the memory injection. *) 1753 @cthulhu 1754 ] 1755 ] 1756 ] 1757 ] 1132 1758 1133 1759  1: (* Integer constant *)
Note: See TracChangeset
for help on using the changeset viewer.