Changeset 1410
- Timestamp:
- Oct 19, 2011, 11:54:13 AM (9 years ago)
- Location:
- src
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/CexecSound.ma
r1350 r1410 1 1 include "Clight/Cexec.ma". 2 2 3 (*include "Plogic/connectives.ma".*)4 5 (* Is rather careful about using destruct because it currently uses excessive6 normalization. *)7 3 lemma exec_bool_of_val_sound: ∀v,ty,r. 8 4 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r). … … 15 11 | *; whd @eq_bv_elim 16 12 [ #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 ]13 | #E1 #E2 destruct @bool_of_val_true @is_true_int_int @E1 18 14 ] 19 15 ] 20 16 | 8: #H cases (eq_dec f Fzero) 21 17 [ #e >e in H ⊢ % >Feq_zero_true #E destruct @bool_of_val_false @is_false_float 22 | #ne >Feq_zero_false in H // #E >(?:r=¬false) [ @bool_of_val_true @is_true_float @ne | destruct @refl ]23 ] 24 | 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 ]18 | #ne >Feq_zero_false in H // #E destruct @bool_of_val_true @is_true_float @ne 19 ] 20 | 14: #H destruct @bool_of_val_false @is_false_pointer 21 | 15: #H destruct @bool_of_val_true @is_true_pointer_pointer 26 22 | *: #H destruct 27 23 ] qed. 28 24 29 25 lemma bool_val_distinct: Vtrue ≠ Vfalse. 30 % #H whd in H:(??%%); (*Wilmer: XXX*) cases daemon (*destruct; @(absurd ? e0 one_not_zero)*)26 % normalize #H destruct 31 27 qed. 32 28 … … 50 46 qed. 51 47 52 axiomexec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'.53 (*Wilmer: XXXX#m #v #ty #ty' #v'48 lemma exec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'. 49 #m #v #ty #ty' #v' 54 50 cases v; 55 51 [ #H whd in H:(??%?); destruct; … … 122 118 ] 123 119 ] 124 ] qed. *)120 ] qed. 125 121 126 122 let rec expr_lvalue_ind … … 194 190 (P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e)). 195 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) 196 (* XXX // fails [ 1,2: #ty #c whd // *)197 192 [ #sz #ty #c whd in ⊢ (???%) cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%) 198 193 @eq_intsize_elim #E try @I <E whd % 199 | #ty #c whd %2194 | #ty #c whd // 200 195 (* expressions that are lvalues *) 201 196 | #e' #ty cases e'; //; [ #i #He' | #e #He' | #e #i #He' ] whd in He' ⊢ %; … … 263 258 [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) ] 264 259 ] 265 | #ty #ty' cases ty try #sz try #sg try #x try @I whd; (* XXX //*) @eval_Esizeof260 | #ty #ty' cases ty try #sz try #sg try #x // 266 261 | #ty #e' #ty' #i cases ty'; //; 267 262 [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H … … 337 332 lemma exec_exprlist_sound: ∀ge,e,m,l. P_res ? (λvltr:list val×trace. eval_exprlist ge e m l (\fst vltr) (\snd vltr)) (exec_exprlist ge e m l). 338 333 #ge #e #m #l elim l; 339 whd ; (* XXX //; *)334 whd 340 335 [ % 341 336 | #e1 #es #IH … … 402 397 //; #H whd; 403 398 @step_skip_call //; 404 | #s' #k' whd; (* XXX //; *) @step_skip_seq399 | #s' #k' whd; // 405 400 | #ex #s' #k' @step_skip_or_continue_while % //; 406 401 | #ex #s' #k' … … 442 437 whd; @(step_call_some … (exec_lvalue_sound' … Hlocofs) Hvf Hvargs efd ety) 443 438 ] 444 | #s1 #s2 whd; (* XXX //; *) @step_seq439 | #s1 #s2 // 445 440 | #ex #s1 #s2 446 441 @res_bindIO2_OK #v #tr #Hv … … 459 454 | @(step_while_false … (exec_expr_sound' … Hv)) @(bool_of … Hb) 460 455 ] 461 | #ex #s' whd; (* XXX //; *) @step_dowhile456 | #ex #s' // 462 457 | #s1 #ex #s2 #s3 whd in ⊢ (?????%); elim (is_Sskip s1); #Hs1 whd in ⊢ (?????%); 463 458 [ >Hs1 … … 495 490 | #ex #ls @res_bindIO2_OK * // #sz #n #tr #Hv 496 491 @step_switch @(exec_expr_sound' … Hv) 497 | #l #s' whd; @step_label (* XXX //; *)492 | #l #s' // 498 493 | #l whd in ⊢ (?????%); lapply (refl ? (find_label l (fn_body f) (call_cont k))); 499 494 cases (find_label l (fn_body f) (call_cont k)) in ⊢ (???% → %); //; 500 495 #sk cases sk; #s' #k' #H 501 496 @(step_goto … H) 502 | #l #s' whd; (* XXX //; *) @step_cost497 | #l #s' // 503 498 ] 504 499 | #f0 #vargs #k #m whd in ⊢ (?????%); cases f0; -
src/Cminor/toRTLabs.ma
r1369 r1410 26 26 generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ? * * #x #y #z 27 27 whd in ⊢ (??%? → ?) elim (fresh RegisterTag z) #r #gen' #E 28 whd in E:(??%?); 29 >(?:e' = add ?? y id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *) 28 whd in E:(??%?); destruct; 30 29 whd >lookup_add_hit % #A destruct 31 30 | #H change in E:(??(match % with [ _ ⇒ ? ])?) with (populate_env e u tl) … … 33 32 cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) (* XXX if I do this directly it rewrites both sides of the equality *) 34 33 * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u1) #r #u'' 35 whd in ⊢ (??%? → ?) #E 36 >(?:e' = add ?? e1 id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *) 34 whd in ⊢ (??%? → ?) #E destruct 37 35 @lookup_add_oblivious 38 36 @(IH … E1 ? H) -
src/common/FrontEndOps.ma
r1369 r1410 145 145 [ #sz' #sg' #H #v #v' #H1 @(elim_val_typ … H1) #i whd in ⊢ (??%? → ?) #E' destruct cases (eq_bv ???) whd in ⊢ (?%?) % 146 146 | #r #H #v #v' #H1 @(elim_val_typ … H1) whd % 147 [ whd in ⊢ (??%? → ?) #E' 148 (* XXX need to normalize or destruct is intractable *) 149 normalize in E'; destruct (E') ; % 147 [ whd in ⊢ (??%? → ?) #E' destruct; % 150 148 | #b #c #o whd in ⊢ (??%? → ?) #E' destruct % 151 149 ]
Note: See TracChangeset
for help on using the changeset viewer.