Changeset 2271
 Timestamp:
 Jul 26, 2012, 5:02:52 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/switchRemoval.ma
r2263 r2271 2980 2980 ] qed. 2981 2981 2982 lemma cast_value_eq : 2983 ∀E,m1,m2,v1,v2. (* memory_inj E m1 m2 → *) value_eq E v1 v2 → 2984 ∀ty,cast_ty,res. exec_cast m1 v1 ty cast_ty = OK ? res → 2985 ∃res'. exec_cast m2 v2 ty cast_ty = OK ? res' ∧ value_eq E res res'. 2986 #E #m1 #m2 #v1 #v2 (* #Hmemory_inj *) #Hvalue_eq #ty #cast_ty #res 2987 @(value_eq_inversion … Hvalue_eq) 2988 [ 1: #v normalize #Habsurd destruct (Habsurd) 2989  2: #vsz #vi whd in match (exec_cast ????); 2990 cases ty 2991 [ 1:  2: #sz #sg  3: #fl  4: #ptrty  5: #arrayty #n  6: #tl #retty  7: #id #fl  8: #id #fl  9: #comptrty ] 2992 normalize nodelta 2993 [ 1,3,7,8,9: #Habsurd destruct (Habsurd) 2994  2: @intsize_eq_elim_elim 2995 [ 1: #Hneq #Habsurd destruct (Habsurd) 2996  2: #Heq destruct (Heq) normalize nodelta 2997 cases cast_ty 2998 [ 1:  2: #csz #csg  3: #cfl  4: #cptrty  5: #carrayty #cn 2999  6: #ctl #cretty  7: #cid #cfl  8: #cid #cfl  9: #ccomptrty ] 3000 normalize nodelta 3001 [ 1,7,8,9: #Habsurd destruct (Habsurd) 3002  2: #Heq destruct (Heq) /3 by ex_intro, conj, vint_eq/ 3003  3: #Heq destruct (Heq) /3 by ex_intro, conj, vfloat_eq/ 3004  4,5,6: whd in match (try_cast_null ?????); normalize nodelta 3005 @eq_bv_elim 3006 [ 1,3,5: #Heq destruct (Heq) >eq_intsize_identity normalize nodelta 3007 whd in match (m_bind ?????); 3008 #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ 3009  2,4,6: #Hneq >eq_intsize_identity normalize nodelta 3010 whd in match (m_bind ?????); 3011 #Habsurd destruct (Habsurd) ] ] 3012 ] 3013  4,5,6: whd in match (try_cast_null ?????); normalize nodelta 3014 @eq_bv_elim 3015 [ 1,3,5: #Heq destruct (Heq) normalize nodelta 3016 whd in match (m_bind ?????); #Habsurd destruct (Habsurd) 3017  2,4,6: #Hneq normalize nodelta 3018 whd in match (m_bind ?????); #Habsurd destruct (Habsurd) ] 3019 ] 3020  3: #f whd in match (exec_cast ????); 3021 cases ty 3022 [ 1:  2: #sz #sg  3: #fl  4: #ptrty  5: #arrayty #n 3023  6: #tl #retty  7: #id #fl  8: #id #fl  9: #comptrty ] 3024 normalize nodelta 3025 [ 1,2,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ] 3026 cases cast_ty 3027 [ 1:  2: #csz #csg  3: #cfl  4: #cptrty  5: #carrayty #cn 3028  6: #ctl #cretty  7: #cid #cfl  8: #cid #cfl  9: #ccomptrty ] 3029 normalize nodelta 3030 [ 1,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ] 3031 #Heq destruct (Heq) 3032 [ 1: /3 by ex_intro, conj, vint_eq/ 3033  2: /3 by ex_intro, conj, vfloat_eq/ ] 3034  4: whd in match (exec_cast ????); 3035 cases ty 3036 [ 1:  2: #sz #sg  3: #fl  4: #ptrty  5: #arrayty #n 3037  6: #tl #retty  7: #id #fl  8: #id #fl  9: #comptrty ] 3038 normalize 3039 [ 1,2,3,7,8,9: #Habsurd destruct (Habsurd) ] 3040 cases cast_ty normalize nodelta 3041 [ 1,10,19: #Habsurd destruct (Habsurd) 3042  2,11,20: #csz #csg #Habsurd destruct (Habsurd) 3043  3,12,21: #cfl #Habsurd destruct (Habsurd) 3044  4,13,22: #cptrty #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ 3045  5,14,23: #carrayty #cn #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ 3046  6,15,24: #ctl #cretty #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ 3047  7,16,25: #cid #cfl #Habsurd destruct (Habsurd) 3048  8,17,26: #cid #cfl #Habsurd destruct (Habsurd) 3049  9,18,27: #ccomptrty #Habsurd destruct (Habsurd) ] 3050  5: #p1 #p2 #Hembed whd in match (exec_cast ????); 3051 cases ty 3052 [ 1:  2: #sz #sg  3: #fl  4: #ptrty  5: #arrayty #n 3053  6: #tl #retty  7: #id #fl  8: #id #fl  9: #comptrty ] 3054 normalize 3055 [ 1,2,3,7,8,9: #Habsurd destruct (Habsurd) ] 3056 cases cast_ty normalize nodelta 3057 [ 1,10,19: #Habsurd destruct (Habsurd) 3058  2,11,20: #csz #csg #Habsurd destruct (Habsurd) 3059  3,12,21: #cfl #Habsurd destruct (Habsurd) 3060  4,13,22: #cptrty #Heq destruct (Heq) %{(Vptr p2)} @conj try @refl @vptr_eq assumption 3061  5,14,23: #carrayty #cn #Heq destruct (Heq) 3062 %{(Vptr p2)} @conj try @refl @vptr_eq assumption 3063  6,15,24: #ctl #cretty #Heq destruct (Heq) 3064 %{(Vptr p2)} @conj try @refl @vptr_eq assumption 3065  7,16,25: #cid #cfl #Habsurd destruct (Habsurd) 3066  8,17,26: #cid #cfl #Habsurd destruct (Habsurd) 3067  9,18,27: #ccomptrty #Habsurd destruct (Habsurd) ] 3068 qed. 3069 3070 lemma bool_of_val_value_eq : 3071 ∀E,v1,v2. value_eq E v1 v2 → 3072 ∀ty,b.exec_bool_of_val v1 ty = OK ? b → exec_bool_of_val v2 ty = OK ? b. 3073 #E #v1 #v2 #Hvalue_eq #ty #b 3074 @(value_eq_inversion … Hvalue_eq) // 3075 [ 1: #v #H normalize in H; destruct (H) 3076  2: #p1 #p2 #Hembed #H @H ] qed. 2982 3077 2983 3078 (* Simulation relation on expressions *) … … 3097 3192 >Hopval_eq normalize destruct /2 by conj/ 3098 3193  9: #ty #cast_ty #e #Hsim @(exec_expr_expr_elim … Hsim) 3099 #v1 #v2 #trace #Hvalue_eq (* TODO ... *) @cthulhu 3100  *: @cthulhu ] qed. 3101 3102 (* TODO: Old cases, to be ported to memory injection. 3103  8: #ty #op #e1 #e2 #Hind1 #Hind2 3104 whd in match (exec_expr ge ???); 3105 whd in match (exec_expr ge' ???); 3106 @(exec_expr_expr_elim … Hind1) 3107 cases (exec_expr ge en1 m1 e2) in Hind2; 3108 [ 2: #error normalize // 3109  1: * #v1 #tr1 normalize in ⊢ (% → ?); #Hind2 elim (Hind2 〈v1,tr1〉 (refl ??)) * #v2 #tr2 * 3110 #Hexec_eq * #Hvalue_eq #Htrace_eq #v1' #v2' #trace #Hvalue_eq' 3111 >Hexec_eq whd in match (m_bind ?????); whd in match (m_bind ?????); 3112 3113 3114  9: #ty #castty #e #Hind 3115 whd in match (exec_expr ge ???); 3116 whd in match (exec_expr ge' ???); 3117 cases Hind 3118 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 3119  1: cases (exec_expr ge en m e) 3120 [ 2: #error #_ @SimFail /2 by ex_intro/ 3121  1: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk // 3122 ] 3123 ] 3124  10: #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3 3125 whd in match (exec_expr ge ???); 3126 whd in match (exec_expr ge' ???); 3127 cases Hind1 3128 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 3129  1: cases (exec_expr ge en m e1) 3130 [ 2: #error #_ @SimFail /2 by ex_intro/ 3131  1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1))) 3132 normalize nodelta 3133 cases (exec_bool_of_val ??) 3134 [ 2: #error @SimFail /2 by ex_intro/ 3135  1: * whd in match (m_bind ?????); normalize nodelta 3136 [ 1: cases Hind2 3137 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 3138  1: cases (exec_expr ge en m e2) 3139 [ 2: #error #_ @SimFail /2 by ex_intro/ 3140  1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2))) 3141 @SimOk normalize nodelta #a2 3142 whd in match (m_bind ?????); // ] 3143 ] 3144  2: cases Hind3 3145 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 3146  1: cases (exec_expr ge en m e3) 3147 [ 2: #error #_ @SimFail /2 by ex_intro/ 3148  1: #a3 #Hind3 >(Hind3 a3 (refl ? (OK ? a3))) 3149 @SimOk normalize nodelta #a3 3150 whd in match (m_bind ?????); // ] 3151 ] 3152 ] ] ] ] 3153  11: #ty #e1 #e2 #Hind1 #Hind2 3154 whd in match (exec_expr ge ???); 3155 whd in match (exec_expr ge' ???); 3156 cases Hind1 3157 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 3158  1: cases (exec_expr ge en m e1) 3159 [ 2: #error #_ @SimFail /2 by ex_intro/ 3160  1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1))) 3161 normalize nodelta 3162 cases (exec_bool_of_val ??) 3163 [ 2: #error @SimFail /2 by ex_intro/ 3164  1: * whd in match (m_bind ?????); 3165 [ 2: @SimOk // ] 3166 cases Hind2 3167 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 3168  1: cases (exec_expr ge en m e2) 3169 [ 2: #error #_ @SimFail /2 by ex_intro/ 3170  1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2))) 3171 @SimOk #a2 3172 whd in match (m_bind ?????); // 3173 ] ] ] ] ] 3174  12: #ty #e1 #e2 #Hind1 #Hind2 3175 whd in match (exec_expr ge ???); 3176 whd in match (exec_expr ge' ???); 3177 cases Hind1 3178 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 3179  1: cases (exec_expr ge en m e1) 3180 [ 2: #error #_ @SimFail /2 by ex_intro/ 3181  1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1))) 3182 normalize nodelta 3183 cases (exec_bool_of_val ??) 3184 [ 2: #error @SimFail /2 by ex_intro/ 3185  1: * whd in match (m_bind ?????); 3186 [ 1: @SimOk // ] 3187 cases Hind2 3188 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 3189  1: cases (exec_expr ge en m e2) 3190 [ 2: #error #_ @SimFail /2 by ex_intro/ 3191  1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2))) 3192 @SimOk #a2 3193 whd in match (m_bind ?????); // 3194 ] ] ] ] ] 3195  13: #ty #sizeof_ty 3196 whd in match (exec_expr ge ???); 3197 whd in match (exec_expr ge' ???); 3198 @SimOk // 3199  14: #ty #e #ty' #fld #Hind 3200 whd in match (exec_lvalue' ge ????); 3201 whd in match (exec_lvalue' ge' ????); 3202 whd in match (typeof ?); 3203 cases ty' in Hind; 3204 [ 1:  2: #sz #sg  3: #fsz  4: #rg #ptr_ty  5: #rg #array_ty #array_sz  6: #domain #codomain 3205  7: #structname #fieldspec  8: #unionname #fieldspec  9: #rg #id ] 3206 normalize nodelta #Hind 3207 try (@SimFail /2 by ex_intro/) 3208 whd in match (exec_lvalue ????); 3209 whd in match (exec_lvalue ????); 3210 cases Hind 3211 [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 3212  1,3: cases (exec_lvalue' ge en m e ?) 3213 [ 2,4: #error #_ @SimFail /2 by ex_intro/ 3214  1,3: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk // 3215 ] ] 3216  15: #ty #l #e #Hind 3217 whd in match (exec_expr ge ???); 3218 whd in match (exec_expr ge' ???); 3219 cases Hind 3220 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ 3221  1: cases (exec_expr ge en m e) 3222 [ 2: #error #_ @SimFail /2 by ex_intro/ 3223  1: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk // 3224 ] ] 3194 #v1 #v2 #trace #Hvalue_eq lapply (cast_value_eq E m1 m2 … Hvalue_eq (typeof e) cast_ty) 3195 cases (exec_cast m1 v1 (typeof e) cast_ty) 3196 [ 2: #error #_ normalize @I 3197  1: #res #H lapply (H res (refl ??)) whd in match (m_bind ?????); 3198 * #res' * #Hexec_cast >Hexec_cast #Hvalue_eq normalize nodelta 3199 @conj // ] 3200  10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 3201 @(exec_expr_expr_elim … Hsim1) #v1 #v2 #trace #Hvalue_eq 3202 lapply (bool_of_val_value_eq E v1 v2 Hvalue_eq (typeof e1)) 3203 cases (exec_bool_of_val ? (typeof e1)) #b 3204 [ 2: #_ normalize @I ] 3205 #H lapply (H ? (refl ??)) #Hexec >Hexec normalize 3206 cases b normalize nodelta 3207 [ 1: (* true branch *) 3208 cases (exec_expr ge en1 m1 e2) in Hsim2; 3209 [ 2: #error normalize #_ @I 3210  1: * #e2v #e2tr normalize #H elim (H ? (refl ??)) 3211 * #e2v' #e2tr' * #Hexec2 >Hexec2 * #Hvalue_eq2 #Htrace_eq2 normalize 3212 destruct @conj try // ] 3213  2: (* false branch *) 3214 cases (exec_expr ge en1 m1 e3) in Hsim3; 3215 [ 2: #error normalize #_ @I 3216  1: * #e3v #e3tr normalize #H elim (H ? (refl ??)) 3217 * #e3v' #e3tr' * #Hexec3 >Hexec3 * #Hvalue_eq3 #Htrace_eq3 normalize 3218 destruct @conj // ] ] 3219  11,12: #ty #e1 #e2 #Hsim1 #Hsim2 3220 @(exec_expr_expr_elim … Hsim1) #v1 #v1' #trace #Hvalue_eq 3221 lapply (bool_of_val_value_eq E v1 v1' Hvalue_eq (typeof e1)) 3222 cases (exec_bool_of_val v1 (typeof e1)) 3223 [ 2,4: #error #_ normalize @I ] 3224 #b cases b #H lapply (H ? (refl ??)) #Heq >Heq 3225 whd in match (m_bind ?????); 3226 whd in match (m_bind ?????); 3227 [ 2,3: normalize @conj try @refl try @vint_eq ] 3228 cases (exec_expr ge en1 m1 e2) in Hsim2; 3229 [ 2,4: #error #_ normalize @I ] 3230 * #v2 #tr2 whd in ⊢ (% → %); #H2 normalize nodelta elim (H2 ? (refl ??)) 3231 * #v2' #tr2' * #Heq2 * #Hvalue_eq2 #Htrace2 >Heq2 normalize nodelta 3232 lapply (bool_of_val_value_eq E v2 v2' Hvalue_eq2 (typeof e2)) 3233 cases (exec_bool_of_val v2 (typeof e2)) 3234 [ 2,4: #error #_ normalize @I ] 3235 #b2 #H3 lapply (H3 ? (refl ??)) #Heq3 >Heq3 normalize nodelta 3236 destruct @conj try @conj // 3237 cases b2 whd in match (of_bool ?); @vint_eq 3238  13: #ty #ty' cases ty 3239 [ 1:  2: #sz #sg  3: #fl  4: #ty  5: #ty #n 3240  6: #tl #ty  7: #id #fl  8: #id #fl  9: #ty ] 3241 whd in match (exec_expr ????); whd 3242 * #v #trace #Heq destruct %{〈Vint sz (repr sz (sizeof ty')), E0〉} 3243 @conj try @refl @conj // 3244  14: #ty #ed #aggregty #i #Hsim whd * * #b #o #tr normalize nodelta 3245 whd in match (exec_lvalue' ?????); 3246 whd in match (exec_lvalue' ge' en2 m2 (Efield (Expr ed aggregty) i) ty); 3247 whd in match (typeof ?); 3248 cases aggregty in Hsim; 3249 [ 1:  2: #sz' #sg'  3: #fl'  4: #ty'  5: #ty' #n' 3250  6: #tl' #ty'  7: #id' #fl'  8: #id' #fl'  9: #ty' ] 3251 normalize nodelta #Hsim 3252 [ 1,2,3,4,5,6,9: #Habsurd destruct (Habsurd) ] 3253 whd in match (m_bind ?????); 3254 whd in match (m_bind ?????); 3255 whd in match (exec_lvalue ge en1 m1 (Expr ed ?)); 3256 cases (exec_lvalue' ge en1 m1 ed ?) in Hsim; 3257 [ 2,4: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] 3258 * * #b1 #o1 #tr1 whd in ⊢ (% → ?); #H elim (H ? (refl ??)) 3259 * * #b1' #o1' #tr1' * #Hexec normalize nodelta * #Hvalue_eq #Htrace_eq 3260 whd in match (exec_lvalue ????); >Hexec normalize nodelta 3261 [ 2: #Heq destruct (Heq) %{〈 b1',o1',tr1'〉} @conj // 3262 normalize @conj // ] 3263 cases (field_offset i fl') 3264 [ 2: #error normalize #Habsurd destruct (Habsurd) ] 3265 #offset whd in match (m_bind ?????); #Heq destruct (Heq) 3266 whd in match (m_bind ?????); 3267 %{〈b1',shift_offset (bitsize_of_intsize I32) o1' (repr I32 offset),tr1'〉} @conj 3268 destruct // normalize nodelta @conj try @refl @vptr_eq 3269 H lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hptr_eq 3270 whd in match (pointer_translation ??); 3271 whd in match (pointer_translation ??); 3272 cases (E b) 3273 [ 1: normalize nodelta #Habsurd destruct (Habsurd) ] 3274 * #b' #o' normalize nodelta #Heq destruct (Heq) destruct (Hptr_eq) 3275 cut (offset_plus (mk_offset (offv o1+Z_of_signed_bitvector (bitsize_of_intsize I32) (repr I32 offset))) o' 3276 = (shift_offset (bitsize_of_intsize I32) (offset_plus o1 o') (repr I32 offset))) 3277 [ normalize >associative_Zplus >(sym_Zplus ? (offv o')) in ⊢ (??%?); <associative_Zplus @refl ] 3278 #Heq >Heq @refl 3279  15: #ty #l #e #Hsim 3280 @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq normalize nodelta @conj // 3225 3281  16: * 3226 3282 [ 1: #sz #i  2: #fl  3: #var_id  4: #e1  5: #e1  6: #op #e1  7: #op #e1 #e2  8: #cast_ty #e1 3227 3283  9: #cond #iftrue #iffalse  10: #e1 #e2  11: #e1 #e2  12: #sizeofty  13: #e1 #field  14: #cost #e1 ] 3228 3284 #ty normalize in ⊢ (% → ?); 3229 [ 1,2: #_ @SimOk #a normalize // 3230  3,4,13: #H @(False_ind … H) 3231  *: #_ @SimFail /2 by ex_intro/ 3232 ] 3233 ] qed. *) 3285 [ 3,4,13: @False_ind 3286  *: #_ normalize #a1 #Habsurd destruct (Habsurd) ] 3287 ] qed. 3288 3234 3289 3235 3290 (*
Note: See TracChangeset
for help on using the changeset viewer.