Changeset 961 for src/Clight/CexecSound.ma
 Timestamp:
 Jun 15, 2011, 4:15:52 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecSound.ma
r891 r961 8 8 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r). 9 9 #v #ty #r 10 cases v; [  #i  #f  #r1  #r' #b #pc #of ] 11 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 ] 12 #H whd in H:(??%?); 13 [ 2: lapply (eq_spec i zero) cases (eq i zero) in H ⊢ % 14 [ #E1 #E2 destruct @bool_of_val_false @is_false_int 15  #E1 #E2 >(?:r=¬false) [ @bool_of_val_true @is_true_int_int @E2  destruct @refl ] 16 ] 17  8: cases (eq_dec f Fzero) 10 cases v; [  #sz #i  #f  #r1  #r' #b #pc #of ] 11 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 ] 12 whd in ⊢ (??%? → ?) 13 [ 2: @intsize_eq_elim_elim 14 [ #NE #H destruct 15  *; whd @eq_bv_elim 16 [ #E1 #E2 destruct @bool_of_val_false @is_false_int 17  #E1 #E2 >(?:r=¬false) [ @bool_of_val_true @is_true_int_int @E1  destruct @refl ] 18 ] 19 ] 20  8: #H cases (eq_dec f Fzero) 18 21 [ #e >e in H ⊢ % >Feq_zero_true #E destruct @bool_of_val_false @is_false_float 19 22  #ne >Feq_zero_false in H // #E >(?:r=¬false) [ @bool_of_val_true @is_true_float @ne  destruct @refl ] 20 23 ] 21  14: >(?:r=false) [ @bool_of_val_false @is_false_pointer  destruct @refl ]22  15: >(?:r=true) [ @bool_of_val_true @is_true_pointer_pointer  destruct @refl ]23  *: destruct24  14: #H >(?:r=false) [ @bool_of_val_false @is_false_pointer  destruct @refl ] 25  15: #H >(?:r=true) [ @bool_of_val_true @is_true_pointer_pointer  destruct @refl ] 26  *: #H destruct 24 27 ] qed. 25 28 … … 35 38 qed. 36 39 37 lemma try_cast_null_sound: ∀m, i,ty,ty',v'. try_cast_null m i ty ty' = OK ? v' → cast m (Vinti) ty ty' v'.38 #m # i #ty #ty' #v'39 whd in ⊢ (??%? → ?) ;40 lapply (eq_spec i zero); cases (eq i zero); 40 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'. 41 #m #sz #i #ty #ty' #v' 42 whd in ⊢ (??%? → ?) 43 @eq_bv_elim 41 44 [ #e >e 42 cases ty; [  #sz #sg  #fs  #sp #ty  #sp #ty #n  #args #rty  #id #fs  #id #fs  #r #id ]43 whd in ⊢ (??%? → ?); #H destruct;44 cases ty' in H ⊢ %; [  #sz #sg  #fs  #sp #ty  #sp #ty #n  #args #rty  #id #fs  #id #fs  #r #id ]45 whd in ⊢ (??%? → ?); #H destruct (H); @cast_ip_z //;45 cases ty; [  #sz' #sg  #fs  #sp #ty  #sp #ty #n  #args #rty  #id #fs  #id #fs  #r #id ] 46 whd in ⊢ (??%? → ?); #H [ 2:  *: destruct ] 47 cases ty' in H ⊢ %; [  #sz'' #sg  #fs  #sp #ty  #sp #ty #n  #args #rty  #id #fs  #id #fs  #r #id ] 48 try (@eq_intsize_elim #E) whd in ⊢ (??%? → ?); #H destruct @cast_ip_z // 46 49  #_ whd in ⊢ (??%? → ?); #H destruct 47 50 ] … … 52 55 cases v; 53 56 [ #H whd in H:(??%?); destruct; 54  # i cases ty;57  #sz #i cases ty; 55 58 [ #H whd in H:(??%?); destruct; 56 59  3: #a #H whd in H:(??%?); destruct; 57 60  7,8,9: #a #b #H whd in H:(??%?); destruct; 58 61  #sz1 #si1 cases ty'; 59 [ #H whd in H:(??%?); destruct; 60  3: #a #H whd in H:(??%?); destruct; // 61  2,7,8,9: #a #b #H whd in H:(??%?); destruct; // 62 [ whd in ⊢ (??%? → ?) @intsize_eq_elim_elim 63 [ #NE #H destruct 64  *; whd #H whd in H:(??%?); destruct; 65 ] 66  3: #a whd in ⊢ (??%? → ?) @intsize_eq_elim_elim 67 [ #E #H whd in H:(??%?); destruct 68  *; whd #H whd in H:(??%?); destruct; @cast_if 69 ] 70  2,7,8,9: #a #b whd in ⊢ (??%? → ?) @intsize_eq_elim_elim 71 [ 1,3,5,7: #NE #H destruct 72  *: *; whd #H whd in H:(??%?); destruct; // 73 ] 62 74  4,5,6: [ #sp #ty'' letin t ≝ (Tpointer sp ty'') 63 75  #sp #ty'' #n letin t ≝ (Tarray sp ty'' n) 64 76  #args #rty letin t ≝ (Tfunction args rty) ] 65 whd in ⊢ (??%? → ?); 66 lapply (try_cast_null_sound m i (Tint sz1 si1) t v'); 67 cases (try_cast_null m i (Tint sz1 si1) t); 68 [ 1,3,5: #v'' #H' #e @H' @e 69  *: #m #_ whd in ⊢ (??%? → ?); #H destruct (H); 77 whd in ⊢ (??%? → ?) @intsize_eq_elim_elim 78 [ 1,3,5: #NE #H destruct 79  *: *; whd 80 lapply (try_cast_null_sound m sz i (Tint sz si1) t v'); 81 cases (try_cast_null m sz i (Tint sz si1) t); 82 [ 1,3,5: #v'' #H' #e @H' @e 83  *: #m #_ whd in ⊢ (??%? → ?); #H destruct (H); 84 ] 70 85 ] 71 86 ] … … 74 89  #args #rty letin t ≝ (Tfunction args rty) ] 75 90 whd in ⊢ (??%? → ?); 76 lapply (try_cast_null_sound m i t ty' v');77 cases (try_cast_null m i t ty');91 lapply (try_cast_null_sound m sz i t ty' v'); 92 cases (try_cast_null m sz i t ty'); 78 93 [ 1,3,5: #v'' #H' #e @H' @e 79 94  *: #m #_ whd in ⊢ (??%? → ?); #H destruct (H); … … 113 128 (P:expr → Prop) 114 129 (Q:expr_descr → type → Prop) 115 (ci:∀ ty,i.P (Expr (Econst_inti) ty))130 (ci:∀sz,ty,i.P (Expr (Econst_int sz i) ty)) 116 131 (cf:∀ty,f.P (Expr (Econst_float f) ty)) 117 132 (lv:∀e,ty. Q e ty → Plvalue P e ty) … … 133 148 [ Expr e' ty ⇒ 134 149 match e' with 135 [ Econst_int i ⇒ city i150 [ Econst_int sz i ⇒ ci sz ty i 136 151  Econst_float f ⇒ cf ty f 137 152  Evar v ⇒ lv (Evar v) ty (vr v ty) … … 152 167 (P:expr → Prop) 153 168 (Q:expr_descr → type → Prop) 154 (ci:∀ ty,i.P (Expr (Econst_inti) ty))169 (ci:∀sz,ty,i.P (Expr (Econst_int sz i) ty)) 155 170 (cf:∀ty,f.P (Expr (Econst_float f) ty)) 156 171 (lv:∀e,ty. Q e ty → Plvalue P e ty) … … 181 196 #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) 182 197 (* XXX // fails [ 1,2: #ty #c whd // *) 183 [ #ty #c whd % 198 [ #sz #ty #c whd in ⊢ (???%) cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%) 199 @eq_intsize_elim #E try @I <E whd % 184 200  #ty #c whd %2 185 201 (* expressions that are lvalues *) … … 248 264 [ @(bool_of … Hb1)  @(exec_bool_of_val_sound … eb2) ] 249 265 ] 250  #ty #ty' whd; (* XXX //*) @eval_Esizeof266  #ty #ty' cases ty try #sz try #sg try #x try @I whd; (* XXX //*) @eval_Esizeof 251 267  #ty #e' #ty' #i cases ty'; //; 252 268 [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H … … 261 277 (* exec_lvalue fails on nonlvalues. *) 262 278  #e' #ty cases e'; 263 [ 1,2,5,12: #a #H  3,4: #a *  13,14: #a #b * 6,8,10,11: #a #b #H  7,9: #a #b #c #H ]279 [ 2,5,12: #a #H  3,4: #a *  13,14: #a #b *  1,6,8,10,11: #a #b #H  7,9: #a #b #c #H ] 264 280 @I 265 281 ] qed. … … 269 285 eval_lvalue ge en m e loc off tr. 270 286 #ge #en #m #e #r #loc #pc #off #tr #ty #H inversion H; 271 [ 1,2,5: #a #b # H @False_ind destruct (H);287 [ 1,2,5: #a #b #c #H @False_ind destruct (H); 272 288  #a #b #c #d #e #f #H1 #g #H2 <H2 in H1 #H1 @False_ind 273 289 @(eval_lvalue_inv_ind … H1) … … 369 385 [ // 370 386  #ty #tys whd in ⊢ (???%) 371 cases ty cases v // #v' #sz try #sg 372 @bind_OK #evs #CHECK 373 @(evl_match_cons ??????? (P_res_to_P ???? (IH ?) CHECK)) // 387 cases ty [ #sz #sg  #sz  #r ] cases v // 388 [ #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?) 389 @eq_intsize_elim #E #CHECKev whd in CHECKev:(??%?); destruct 390  #v ] @bind_OK #evs #CHECKevs 391 @(evl_match_cons ??????? (P_res_to_P ???? (IH ?) CHECKevs)) 392 // 374 393 ] 375 394 ] qed. … … 483 502 whd; @(step_return_1 … Hnotvoid (exec_expr_sound' … Hv)) 484 503 ] 485  #ex #ls @res_bindIO2_OK #v cases v; //;#n #tr #Hv504  #ex #ls @res_bindIO2_OK * // #sz #n #tr #Hv 486 505 @step_switch @(exec_expr_sound' … Hv) 487 506  #l #s' whd; @step_label (* XXX //; *) … … 542 561 543 562 lemma is_final_sound: ∀s,r. is_final s = Some ? r → final_state s r. 544 * [ 3: #v * [ #m #r cases v [ 2: #r' #E normalize in E; destruct %563 * [ 3: #v * [ #m #r cases v [ 2: * #r' #E normalize in E; destruct % 545 564  *: normalize #x1 try #x2 try #x3 try #x4 try #x5 destruct 546 565 ]
Note: See TracChangeset
for help on using the changeset viewer.