Changeset 2176 for src/Clight/CexecSound.ma
 Timestamp:
 Jul 12, 2012, 1:28:28 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecSound.ma
r2106 r2176 5 5 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r). 6 6 #v #ty #r 7 cases v; [  #sz #i  #f  #r1 #ptr ]8 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 ]7 cases v; [  #sz #i  #f   #ptr ] 8 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 ] 9 9 whd in ⊢ (??%? → ?); 10 10 [ 2: @intsize_eq_elim_elim … … 39 39 @eq_bv_elim 40 40 [ #e >e 41 cases ty; [  #sz' #sg  #fs  #sp #ty  #sp #ty #n  #args #rty  #id #fs  #id #fs  #r#id ]41 cases ty; [  #sz' #sg  #fs  (*#sp*) #ty  (*#sp*) #ty #n  #args #rty  #id #fs  #id #fs  (*#r*) #id ] 42 42 whd in ⊢ (??%? → ?); #H [ 2:  *: destruct ] 43 cases ty' in H ⊢ %; [  #sz'' #sg  #fs  #sp #ty  #sp #ty #n  #args #rty  #id #fs  #id #fs  #r#id ]43 cases ty' in H ⊢ %; [  #sz'' #sg  #fs  (*#sp*) #ty  (*#sp*) #ty #n  #args #rty  #id #fs  #id #fs  (*#r*) #id ] 44 44 try (@eq_intsize_elim #E) whd in ⊢ (??%? → ?); #H destruct @cast_ip_z // 45 45  #_ whd in ⊢ (??%? → ?); #H destruct … … 54 54 [ #H whd in H:(??%?); destruct; 55 55  3: #a #H whd in H:(??%?); destruct; 56  7,8,9: #a #b#H whd in H:(??%?); destruct;56  7,8,9: #a [ 1,2: #b ] #H whd in H:(??%?); destruct; 57 57  #sz1 #si1 cases ty'; 58 58 [ whd in ⊢ (??%? → ?); @intsize_eq_elim_elim … … 64 64  *; whd #H whd in H:(??%?); destruct; @cast_if 65 65 ] 66  2,7,8,9: #a #bwhd in ⊢ (??%? → ?); @intsize_eq_elim_elim66  2,7,8,9: #a [1,2,3: #b] whd in ⊢ (??%? → ?); @intsize_eq_elim_elim 67 67 [ 1,3,5,7: #NE #H destruct 68 68  *: *; whd #H whd in H:(??%?); destruct; // 69 69 ] 70  4,5,6: [ # sp #ty'' letin t ≝ (Tpointer spty'')71  #sp #ty'' #n letin t ≝ (Tarray spty'' n)72 70  4,5,6: [ #ty'' letin t ≝ (Tpointer ty'') 71  #ty'' #n letin t ≝ (Tarray ty'' n) 72  #args #rty letin t ≝ (Tfunction args rty) ] 73 73 whd in ⊢ (??%? → ?); @intsize_eq_elim_elim 74 74 [ 1,3,5: #NE #H destruct … … 81 81 ] 82 82 ] 83  *: [ # sp #ty'' letin t ≝ (Tpointer spty'')84  #sp #ty'' #n letin t ≝ (Tarray spty'' n)85 83  *: [ #ty'' letin t ≝ (Tpointer ty'') 84  #ty'' #n letin t ≝ (Tarray ty'' n) 85  #args #rty letin t ≝ (Tfunction args rty) ] 86 86 whd in ⊢ (??%? → ?); 87 87 lapply (try_cast_null_sound m sz i t ty' v'); … … 91 91 ] 92 92 ] 93  #f cases ty; [ 3 : #x  2,4,6,7,8,9: #x #y  5: #x #y #z]94 [ cases ty'; [ #e  3 : #a #e  2,4,6,7,8,9: #a #b #e  #a #b #c#e ]93  #f cases ty; [ 3,4,9: #x  2,5,6,7,8: #x #y ] 94 [ cases ty'; [ #e  3,4,9: #a #e  2,6,7,8: #a #b #e  #a #b #e ] 95 95 whd in e:(??%?); destruct; //; 96 96  *: #e whd in e:(??%?); destruct 97 97 ] 98  #r cases ty; [ 3: #x  2,4,6,7,8,9: #x #y  5: #x #y #z ] 99 whd in ⊢ (??%? → ?); #H destruct; cases (eq_region_dec r ?) in H; 100 whd in ⊢ (? → ??%? → ?); #H1 #H2 destruct; 101 cases ty' in H2; normalize; try #a try #b try #c try #d destruct; 98  cases ty; [ 3,4,9: #x  2,5,6,7,8: #x #y ] 99 whd in ⊢ (??%? → ?); #H destruct 100 cases ty' in H; normalize; try #a try #b try #c try #d destruct; 102 101 @cast_pp_z //; 102 (* 103 103  #ptr whd in ⊢ (??%? → ?); #e 104 104 elim (bind_inversion ????? e) #s * #es #e' … … 119 119 ] 120 120 ] 121 *) 122  #ptr 123 cases ty; [ 3,4,9: #x  2,5,6,7,8: #x #y ] 124 #E whd in E:(??%?); destruct 125 cases ty' in E ⊢ %; normalize #A try #B try #C try #D destruct /2/ 121 126 ] qed. 122 127 … … 142 147 ] 143 148  #ty #e #He whd in ⊢ (???%); 144 @bind2_OK #v cases v / by / * # r #l #pc#ofs #tr #Hv whd149 @bind2_OK #v cases v / by / * #l #ofs #tr #Hv whd 145 150 >Hv in He; #He 146 @eval_Ederef [ 3: @He  *: skip ]151 @eval_Ederef @He 147 152  #ty #e'' #ty'' #He'' @bind2_OK * #loc #ofs #tr #H 148 cases ty try (try #a try #b try #c @I) * #pty 149 cases loc in H ⊢ %; * #loc' #H 150 whd try @I 153 cases ty try (try #a try #b try #c @I) 154 #ty' whd 151 155 @eval_Eaddrof whd in H:(??%?); >H in He''; #He'' @He'' 152 156  #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1 … … 210 214 ] qed. 211 215 212 lemma addrof_eval_lvalue: ∀ge,en,m,e, r,loc,pc,off,tr,ty.213 eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr (mk_pointer r loc pc off)) tr →216 lemma addrof_eval_lvalue: ∀ge,en,m,e,loc,off,tr,ty. 217 eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr (mk_pointer loc off)) tr → 214 218 eval_lvalue ge en m e loc off tr. 215 #ge #en #m #e # r #loc #pc #off #tr #ty #H inversion H;219 #ge #en #m #e #loc #off #tr #ty #H inversion H; 216 220 [ 1,2,5: #a #b #c #H @False_ind destruct (H); 217 221  #a #b #c #d #e #f #H1 #g #H2 #E1 #E2 #E3 <H2 in H1; #H1 @False_ind … … 219 223 [ #a #b #c #d #bad destruct (bad); 220 224  #a #b #c #d #e #bad destruct (bad); 221  #a #b #c #d #e #f # g #h #bad destruct (bad);225  #a #b #c #d #e #f #bad destruct (bad); 222 226  #a #b #c #d #e #f #g #h #i #j #k #l #bad @False_ind destruct (bad); 223 227  #a #b #c #d #e #f #g #h #i #j #bad destruct (bad); 224 228 ] 225  #e' #ty' # r' #loc' #ofs' #tr' #H' #pc' #e1 #e2 #e3 destruct (e1 e2 e3); #E @H'229  #e' #ty' #loc' #ofs' #tr' #H' #e1 #e2 #e3 destruct (e1 e2 e3); #E @H' 226 230  #a #b #c #d #e #f #g #h #bad destruct (bad); 227 231  #a #b #c #d #e #f #g #h #i #j #k #l #bad destruct (bad); … … 238 242 lemma addrof_exec_lvalue: ∀ge,en,m,e,r,loc,off,tr. 239 243 exec_lvalue ge en m e = OK ? 〈〈mk_block r loc,off〉,tr〉 → 240 exec_expr ge en m (Expr (Eaddrof e) (Tpointer r Tvoid)) = OK ? 〈Vptr (mk_pointer r (mk_block r loc) (same_compat ??) off), tr〉.244 exec_expr ge en m (Expr (Eaddrof e) (Tpointer Tvoid)) = OK ? 〈Vptr (mk_pointer (mk_block r loc) off), tr〉. 241 245 #ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?); 242 246 >H whd in ⊢ (??%?); cases r @refl … … 248 252 cases (exec_lvalue ge en m e) in ⊢ (???% → %); 249 253 [ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ %; #locr #loci #H 250 @(addrof_eval_lvalue … locr … (Tpointer locr Tvoid)) [ @same_compat ]254 @(addrof_eval_lvalue … (Tpointer Tvoid)) 251 255 lapply (addrof_exec_lvalue … H) #H' 252 lapply (exec_expr_sound ge en m (Expr (Eaddrof e) (Tpointer locrTvoid)))256 lapply (exec_expr_sound ge en m (Expr (Eaddrof e) (Tpointer Tvoid))) 253 257 >H' #H'' @H'' 254 258  #msg #_ whd @I … … 284 288 [ #en #m #en' #m' #EXEC whd in EXEC:(??%?); destruct % 285 289  * #id #ty #t #IH #en #m #en' #m' 286 lapply (refl ? (alloc m O (sizeof ty) Any)) whd in ⊢ (? → ??%? → ?);290 lapply (refl ? (alloc m O (sizeof ty) XData)) whd in ⊢ (? → ??%? → ?); 287 291 cases (alloc ????) in ⊢ (???% → %); #m'' #b #ALLOC #EXEC 288 292 @(alloc_variables_cons … ALLOC) … … 314 318 [ // 315 319  #ty #tys whd in ⊢ (???%); 316 cases ty [ #sz #sg  #sz  #r] cases v //320 cases ty [ #sz #sg   #sz ] cases v // 317 321 [ #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?); 318 322 @eq_intsize_elim #E #CHECKev whd in CHECKev:(??%?); destruct
Note: See TracChangeset
for help on using the changeset viewer.