Changeset 14 for Csemantics/Mem.ma
 Timestamp:
 Jul 21, 2010, 3:08:58 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Mem.ma
r10 r14 1701 1701 ## #ineq; @1; @1; napply ineq; 1702 1702 ##] nqed. 1703 (* XXX: reenable once I've sorted out performance a bit 1703 1704 (* XXX: use Or rather than ∨ to bring resource usage under control. *) 1704 1705 ndefinition meminj_no_overlap ≝ λmi: meminj. λm: mem. 1705 1706 ∀b1,b1',delta1,b2,b2',delta2. … … 1707 1708 mi b1 = Some ? 〈b1', delta1〉 → 1708 1709 mi b2 = Some ? 〈b2', delta2〉 → 1709 b1' ≠ b2'1710 ∨ low_bound m b1 ≥ high_bound m b11711 ∨ low_bound m b2 ≥ high_bound m b21712 ∨ (high_bound m b1 + delta1 ≤ low_bound m b2 + delta21713 ∨ high_bound m b2 + delta2 ≤ low_bound m b1 + delta1).1710 Or (Or (Or (b1' ≠ b2') 1711 (low_bound m b1 ≥ high_bound m b1)) 1712 (low_bound m b2 ≥ high_bound m b2)) 1713 (Or (high_bound m b1 + delta1 ≤ low_bound m b2 + delta2) 1714 (high_bound m b2 + delta2 ≤ low_bound m b1 + delta1)). 1714 1715 1715 1716 (* FIXME *) … … 2220 2221 ## ##3: nwhd in ⊢ (??%?); // 2221 2222 ## ##4,5: //; 2222 ## ##6: nwhd; #chunk;#_; n whd; @ O;//;2223 ## ##6: nwhd; #chunk;#_; ncases chunk;//; 2223 2224 ##] nqed. 2224 2225 … … 2353 2354 nrewrite > (?:repr O = zero); ##[ ##2: // ##] 2354 2355 nrewrite > (add_zero ?); 2356 nrewrite > (Zplus_z_OZ …); 2355 2357 //; 2356 2358 ## (* delta ≠ 0 *) … … 2387 2389 ##] nqed. 2388 2390 2391 (* XXX: should use ndestruct, but reduces large definitions *) 2392 nremark vptr_eq: ∀b,b',i,i'. Vptr b i = Vptr b' i' → b = b' ∧ i = i'. 2393 #b b' i i' e; ndestruct; /2/; nqed. 2394 2389 2395 nlemma valid_pointer_inject: 2390 2396 ∀f,m1,m2,b,ofs,b',ofs'. … … 2397 2403 ##[ ##1,2,4: #x;#H;ndestruct; ##] 2398 2404 #b0;#i;#b0';#i';#delta;#Hb;#Hi';#eptr;#eptr'; 2399 (* FIXME want ndestruct to sort this out, but get assertion failure *) 2400 nrewrite > (?:b0 = b) in Hb; ##[ ##2: ndestruct; // ##] 2401 nrewrite > (?:b0' = b'); ##[ ##2: ndestruct; // ##] 2402 nrewrite > (?:i = ofs) in Hi'; ##[ ##2: ndestruct; // ##] 2403 nrewrite > (?:i' = ofs'); ##[ ##2: ndestruct; // ##] 2405 nrewrite < (proj1 … (vptr_eq ???? eptr)) in Hb; nrewrite < (proj1 … (vptr_eq ???? eptr')); 2406 nrewrite < (proj2 … (vptr_eq ???? eptr)) in Hi'; nrewrite < (proj2 … (vptr_eq ???? eptr')); 2404 2407 #Hofs; #Hbinj; 2405 2408 nrewrite > Hofs; … … 2510 2513 ## ncases chunk'; #v;#_;#_; @4; 2511 2514 ##] 2512 (* FIXME: the next two cases are the same*)2515 (* FIXME: the next two cases are very similar *) 2513 2516 ## #chunk'';#i;#i';*;#echunk;nrewrite > echunk;#Hz;#_;#_;#_; 2514 nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ndestruct; 2515 ##[ ##2,4: nrewrite > Hz; @ 2516 ## ##1,3: nrewrite > (sign_ext_equal_if_zero_equal … Hz); @; nnormalize; 2517 nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; 2518 ##[ ##3,4,5,6,7,10,11,12,13,14: napply False_ind; ndestruct; 2519 ## ##2,9: nwhd in ⊢ (??%%); nrewrite > Hz; @ 2520 ## ##1,8: nwhd in ⊢ (??%%); 2521 (* XXX: applying the rewrite directly fails with a unification error, 2522 but establishing the equality then using napplyS works! *) 2523 nlapply (sign_ext_equal_if_zero_equal … Hz); 2524 ##[ ##1,3: @; ##[ ##1,3: napply I; ## ##2,4: napply leb_true_to_le; @; ##] 2525 ## ##2,4: #H; napplyS val_inject_int; 2526 ##] 2527 (* original version: 2528 nrewrite > (sign_ext_equal_if_zero_equal … Hz); @; nnormalize; 2517 2529 ##[ ##1,3: napply I ## ##2,4: napply leb_true_to_le; @; ##] 2530 *) 2518 2531 ##] 2519 2532 2520 2533 ## #chunk'';#i;#i';*;#echunk;nrewrite > echunk;#Hz;#_;#_;#_; 2521 nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ndestruct; 2522 ##[ ##2,4: nrewrite > Hz; @ 2523 ## ##1,3: nrewrite > (sign_ext_equal_if_zero_equal … Hz); @; nnormalize; 2524 ##[ ##1,3: napply I ## ##2,4: napply leb_true_to_le; @; ##] 2534 nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; 2535 ##[ ##1,2,5,6,7,8,9,12,13,14: napply False_ind; ndestruct; 2536 ## ##4,11: nwhd in ⊢ (??%%); nrewrite > Hz; @ 2537 ## ##3,10: nwhd in ⊢ (??%%); 2538 (* XXX: actually, napplyS doesn't complete in a reasonable time here; 2539 but rewriting on one goal at a time giving the exact position 2540 does! *) 2541 ##[ nrewrite > (sign_ext_equal_if_zero_equal … Hz) in ⊢ (??(?%)?); @; 2542 ##[ ##1,3: napply I; ## ##2,4: napply leb_true_to_le; @; ##] 2543 ## nrewrite > (sign_ext_equal_if_zero_equal … Hz) in ⊢ (??(?%)?); @; 2544 ##[ ##1,3: napply I; ## ##2,4: napply leb_true_to_le; @; ##] 2545 ##] 2525 2546 ##] 2526 2547 … … 2920 2941 #Hminj;#ALLOC1;#ALLOC2;#Hlo;#Hhi; 2921 2942 napply (alloc_mapped_inject … ALLOC1); /2/; 2922 ##[ nlapply (alloc_right_inject … Hminj ALLOC2); //; 2923 ## (* TODO: add to integers *) napply daemon 2943 ##[ napply (alloc_right_inject … Hminj ALLOC2); 2924 2944 ## nrewrite > (low_bound_alloc_same … ALLOC2); // 2925 2945 ## nrewrite > (high_bound_alloc_same … ALLOC2); // … … 3135 3155 ncut (f b = Some ? delta); 3136 3156 ##[ nwhd in INJb':(??%?); ncases (f b) in INJb' ⊢ %; 3137 ##[ #H; n destruct; ## #delta'; #H; nelim (grumpydestruct2 ?????? H); // ##]3157 ##[ #H; napply (False_ind … (grumpydestruct … H)); ## #delta'; #H; nelim (grumpydestruct2 ?????? H); // ##] 3138 3158 ##] #INJb; 3139 3159 nlapply (valid_pointer_shift_no_overflow … VALID INJb); //; #NOOV; … … 3171 3191 nlapply INJb1; nwhd in ⊢ (??%? → ?); 3172 3192 nlapply (refl ? (f b1)); ncases (f b1) in ⊢ (???% → %); 3173 ##[ #_; nwhd in ⊢ (??%? → ?); #H; napply False_ind; n destruct;3193 ##[ #_; nwhd in ⊢ (??%? → ?); #H; napply False_ind; napply (False_ind … (grumpydestruct … H)); 3174 3194 ## #delta'; #DELTA; nwhd in ⊢ (??%? → ?); #H; nelim (grumpydestruct2 ?????? H); 3175 3195 #eb;#edelta; … … 3435 3455 ##] 3436 3456 nqed. 3437 *) 3457 3438 3458 (* ** Relation between signed and unsigned loads and stores *) 3439 3459 … … 3486 3506 nelim (in_bounds m Mint8unsigned b (signed ofs)); /2/; 3487 3507 #H; nwhd in ⊢ (??%%); 3488 nelim (getN 0 (signed ofs) (contents (blocks m b))); //; 3489 #i; nwhd in ⊢ (??(??%)(??%)); nrewrite > (sign_ext_zero_ext …); //; 3490 (* arith *) napply daemon; 3491 nqed. 3508 nelim (getN 0 (signed ofs) (contents (blocks m b))); 3509 ##[ ##1,3,4: //; 3510 ## #i; nwhd in ⊢ (??(??%)(??%)); 3511 (* XXX: need to specify which side of the equality to rewrite on to avoid 3512 a unification assertion. *) 3513 nrewrite > (sign_ext_zero_ext ?? i) in ⊢ (???%); ##[ napply refl; (* XXX: // ? *) 3514 ## (* arith *) napply daemon; 3515 ##] 3516 ##] 3517 nqed.
Note: See TracChangeset
for help on using the changeset viewer.