Changeset 1516 for src/Clight/CexecSound.ma
 Timestamp:
 Nov 19, 2011, 12:38:20 AM (9 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 nonlvalues. *) … … 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.