Changeset 1516 for src/Clight/CexecSound.ma
- Timestamp:
- Nov 19, 2011, 12:38:20 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/CexecSound.ma
r1510 r1516 6 6 cases v; [ | #sz #i | #f | #r1 | #r' #b #pc #of ] 7 7 cases ty; [ 2,11,20,29,38: #sz' #sg | 3,12,21,30,39: #sz' | 4,13,22,31,40: #rg #ty | 5,14,23,32,41: #r #ty #n | 6,15,24,33,42: #args #rty | 7,8,16,17,25,26,34,35,43,44: #id #fs | 9,18,27,36,45: #r #id ] 8 whd in ⊢ (??%? → ?) 8 whd in ⊢ (??%? → ?); 9 9 [ 2: @intsize_eq_elim_elim 10 10 [ #NE #H destruct … … 15 15 ] 16 16 | 8: #H cases (eq_dec f Fzero) 17 [ #e >e in H ⊢ % >Feq_zero_true #E destruct @bool_of_val_false @is_false_float18 | #ne >Feq_zero_false in H // #E destruct @bool_of_val_true @is_true_float @ne17 [ #e >e in H ⊢ %; >Feq_zero_true #E destruct @bool_of_val_false @is_false_float 18 | #ne >Feq_zero_false in H; // #E destruct @bool_of_val_true @is_true_float @ne 19 19 ] 20 20 | 14: #H destruct @bool_of_val_false @is_false_pointer … … 35 35 lemma try_cast_null_sound: ∀m,sz,i,ty,ty',v'. try_cast_null m sz i ty ty' = OK ? v' → cast m (Vint sz i) ty ty' v'. 36 36 #m #sz #i #ty #ty' #v' 37 whd in ⊢ (??%? → ?) 37 whd in ⊢ (??%? → ?); 38 38 @eq_bv_elim 39 39 [ #e >e … … 55 55 | 7,8,9: #a #b #H whd in H:(??%?); destruct; 56 56 | #sz1 #si1 cases ty'; 57 [ whd in ⊢ (??%? → ?) @intsize_eq_elim_elim57 [ whd in ⊢ (??%? → ?); @intsize_eq_elim_elim 58 58 [ #NE #H destruct 59 59 | *; whd #H whd in H:(??%?); destruct; 60 60 ] 61 | 3: #a whd in ⊢ (??%? → ?) @intsize_eq_elim_elim61 | 3: #a whd in ⊢ (??%? → ?); @intsize_eq_elim_elim 62 62 [ #E #H whd in H:(??%?); destruct 63 63 | *; whd #H whd in H:(??%?); destruct; @cast_if 64 64 ] 65 | 2,7,8,9: #a #b whd in ⊢ (??%? → ?) @intsize_eq_elim_elim65 | 2,7,8,9: #a #b whd in ⊢ (??%? → ?); @intsize_eq_elim_elim 66 66 [ 1,3,5,7: #NE #H destruct 67 67 | *: *; whd #H whd in H:(??%?); destruct; // … … 70 70 | #sp #ty'' #n letin t ≝ (Tarray sp ty'' n) 71 71 | #args #rty letin t ≝ (Tfunction args rty) ] 72 whd in ⊢ (??%? → ?) @intsize_eq_elim_elim72 whd in ⊢ (??%? → ?); @intsize_eq_elim_elim 73 73 [ 1,3,5: #NE #H destruct 74 74 | *: *; whd … … 100 100 cases ty' in H2; normalize; try #a try #b try #c try #d destruct; 101 101 @cast_pp_z //; 102 | #r #b #pc #of whd in ⊢ (??%? → ?) #e102 | #r #b #pc #of whd in ⊢ (??%? → ?); #e 103 103 elim (bind_inversion ????? e) #s * #es #e' 104 104 elim (bind_inversion ????? e') #u * #eu #e'' -e'; … … 113 113 | #Hty' 114 114 cut (s = r). elim (eq_region_dec r s) in eu; //; normalize; #_ #e destruct. 115 #e >e in Hty #Hty116 cases (pointer_compat_dec b s') in e''' 115 #e >e in Hty; #Hty 116 cases (pointer_compat_dec b s') in e'''; 117 117 #Hcompat #e''' whd in e''':(??%?); destruct (e'''); /2/ 118 118 ] … … 190 190 (P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e)). 191 191 #ge #en #m #e @(expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e) 192 [ #sz #ty #c whd in ⊢ (???%) cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%)192 [ #sz #ty #c whd in ⊢ (???%); cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%); 193 193 @eq_intsize_elim #E try @I <E whd % 194 194 | #ty #c whd // … … 197 197 @bind2_OK #x cases x; #y cases y; #sp #loc #ofs #tr #H 198 198 @opt_bind_OK #vl #evl whd in evl:(??%?); @(eval_Elvalue … evl) 199 >H in He' #He' @He'199 >H in He'; #He' @He' 200 200 | #v #ty 201 201 whd in ⊢ (???%); 202 202 lapply (refl ? (lookup SymbolTag block en v)) 203 cases (lookup SymbolTag block en v) in ⊢ (???% → %) 203 cases (lookup SymbolTag block en v) in ⊢ (???% → %); 204 204 [ #eget @opt_bind_OK #sploc cases sploc; #sp #loc #efind 205 205 whd; @(eval_Evar_global … eget efind) 206 206 | #loc #eget @(eval_Evar_local … eget) 207 207 ] 208 | #ty #e #He whd in ⊢ (???%) 208 | #ty #e #He whd in ⊢ (???%); 209 209 @bind2_OK #v cases v // #r #l #pc #ofs #tr #Hv whd 210 >Hv in He #He210 >Hv in He; #He 211 211 @eval_Ederef [ 3: @He | *: skip ] 212 212 | #ty #e'' #ty'' #He'' @bind2_OK * #loc #ofs #tr #H 213 213 cases ty // * #pty 214 cases loc in H ⊢ % * #loc' #H214 cases loc in H ⊢ %; * #loc' #H 215 215 whd try @I 216 @eval_Eaddrof whd in H:(??%?) >H in He''#He'' @He''216 @eval_Eaddrof whd in H:(??%?); >H in He''; #He'' @He'' 217 217 | #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1 218 218 @opt_bind_OK #v #ev 219 219 @(eval_Eunop … ev) 220 >Hv1 in He1 #He1 @He1220 >Hv1 in He1; #He1 @He1 221 221 | #ty #op #e1 #e2 #He1 #He2 222 @bind2_OK #v1 #tr1 #ev1 >ev1 in He1 #He1223 @bind2_OK #v2 #tr2 #ev2 >ev2 in He2 #He2222 @bind2_OK #v1 #tr1 #ev1 >ev1 in He1; #He1 223 @bind2_OK #v2 #tr2 #ev2 >ev2 in He2; #He2 224 224 @opt_bind_OK #v #ev whd in He1 He2; whd; 225 225 @(eval_Ebinop … He1 He2 ev) 226 226 | #ty #ty' #e' #He' 227 @bind2_OK #v #tr #Hv >Hv in He' #He'227 @bind2_OK #v #tr #Hv >Hv in He'; #He' 228 228 @bind_OK #v' #ev' 229 229 @(eval_Ecast … He' ?) … … 231 231 @(exec_cast_sound … ev') 232 232 | #ty #e1 #e2 #e3 #He1 #He2 #He3 233 @bind2_OK #vb #tr1 #Hvb >Hvb in He1 #He1233 @bind2_OK #vb #tr1 #Hvb >Hvb in He1; #He1 234 234 @bind_OK #b 235 235 cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb 236 @bind2_OK #v #tr #Hv whd in Hv:(??%?) 237 [ >Hv in He2 #He2 whd in He2 Hv:(??%?) ⊢%;236 @bind2_OK #v #tr #Hv whd in Hv:(??%?); 237 [ >Hv in He2; #He2 whd in He2 Hv:(??%?) ⊢%; 238 238 @(eval_Econdition_true … He1 ? He2) @(bool_of ??? Hb) 239 | >Hv in He3 #He3 whd in He3 Hv:(??%?) ⊢%;239 | >Hv in He3; #He3 whd in He3 Hv:(??%?) ⊢%; 240 240 @(eval_Econdition_false … He1 ? He3) @(bool_of ??? Hb) 241 241 ] 242 242 | #ty #e1 #e2 #He1 #He2 243 @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1 #He1243 @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1 244 244 @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1 245 [ @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2 #He2245 [ @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2 246 246 @bind_OK #b2 #eb2 247 247 @(eval_Eandbool_2 … He1 … He2) … … 250 250 ] 251 251 | #ty #e1 #e2 #He1 #He2 252 @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1 #He1252 @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1 253 253 @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1 254 254 [ @(eval_Eorbool_1 … He1) @(bool_of … Hb1) 255 | @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2 #He2255 | @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2 256 256 @bind_OK #b2 #eb2 257 257 @(eval_Eorbool_2 … He1 … He2) … … 261 261 | #ty #e' #ty' #i cases ty'; //; 262 262 [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H 263 @bind_OK #delta #Hdelta whd in H:(??%?) >H in He'#He'263 @bind_OK #delta #Hdelta whd in H:(??%?); >H in He'; #He' 264 264 @(eval_Efield_struct … He' (refl ??) Hdelta) 265 | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H whd in H:(??%?) 266 >H in He' #He'265 | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H whd in H:(??%?); 266 >H in He'; #He' 267 267 @(eval_Efield_union … He' (refl ??)) 268 268 ] 269 | #ty #l #e' #He' @bind2_OK #v #tr1 #H >H in He' #He'269 | #ty #l #e' #He' @bind2_OK #v #tr1 #H >H in He'; #He' 270 270 @(eval_Ecost … He') 271 271 (* exec_lvalue fails on non-lvalues. *) … … 280 280 #ge #en #m #e #r #loc #pc #off #tr #ty #H inversion H; 281 281 [ 1,2,5: #a #b #c #H @False_ind destruct (H); 282 | #a #b #c #d #e #f #H1 #g #H2 #E1 #E2 #E3 <H2 in H1 #H1 @False_ind282 | #a #b #c #d #e #f #H1 #g #H2 #E1 #E2 #E3 <H2 in H1; #H1 @False_ind 283 283 @(eval_lvalue_inv_ind … H1) 284 284 [ #a #b #c #d #bad destruct (bad); … … 304 304 exec_lvalue ge en m e = OK ? 〈〈mk_block r loc,off〉,tr〉 → 305 305 exec_expr ge en m (Expr (Eaddrof e) (Tpointer r Tvoid)) = OK ? 〈Vptr r (mk_block r loc) (same_compat ??) off, tr〉. 306 #ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?) 307 >H whd in ⊢ (??%?) cases r @refl306 #ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?); 307 >H whd in ⊢ (??%?); cases r @refl 308 308 qed. 309 309 … … 312 312 #ge #en #m #e lapply (refl ? (exec_lvalue ge en m e)); 313 313 cases (exec_lvalue ge en m e) in ⊢ (???% → %); 314 [ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ % #locr #loci #H314 [ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ %; #locr #loci #H 315 315 @(addrof_eval_lvalue … locr … (Tpointer locr Tvoid)) [ @same_compat ] 316 316 lapply (addrof_exec_lvalue … H) #H' … … 350 350 | * #id #ty #t #IH #en #m #en' #m' 351 351 lapply (refl ? (alloc m O (sizeof ty) Any)) #ALLOC #EXEC 352 whd in EXEC:(??%?) ALLOC:(???%) 352 whd in EXEC:(??%?) ALLOC:(???%); 353 353 @(alloc_variables_cons … ALLOC) 354 354 @IH @EXEC … … 365 365 @opt_bind_OK #m' #STORE 366 366 lapply (refl ? (exec_bind_parameters en m' ps' vs)) 367 cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %) [2: #msg #_ %]367 cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %); [2: #msg #_ %] 368 368 #m'' #BIND 369 369 @(bind_parameters_cons … GET STORE) 370 lapply (IH vs en m') whd in ⊢ (% → ?) >BIND //370 lapply (IH vs en m') whd in ⊢ (% → ?); >BIND // 371 371 ] 372 372 ] qed. … … 378 378 | #v #vs #IH * 379 379 [ // 380 | #ty #tys whd in ⊢ (???%) 380 | #ty #tys whd in ⊢ (???%); 381 381 cases ty [ #sz #sg | #sz | #r ] cases v // 382 [ #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?) 382 [ #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?); 383 383 @eq_intsize_elim #E #CHECKev whd in CHECKev:(??%?); destruct 384 384 | #v ] @bind_OK #evs #CHECKevs … … 498 498 ] 499 499 | #f0 #vargs #k #m whd in ⊢ (?????%); cases f0; 500 [ #fn whd in ⊢ (?????%) 500 [ #fn whd in ⊢ (?????%); 501 501 lapply (refl ? (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn))) 502 cases (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)) in ⊢ (???% → %) 503 #en' #m' #ALLOC whd in ⊢ (?????%) 502 cases (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)) in ⊢ (???% → %); 503 #en' #m' #ALLOC whd in ⊢ (?????%); 504 504 @res_bindIO_OK #m2 #BIND 505 505 whd; @(step_internal_function … (exec_alloc_variables_sound … ALLOC))
Note: See TracChangeset
for help on using the changeset viewer.