# Changeset 14

Ignore:
Timestamp:
Jul 21, 2010, 3:08:58 PM (10 years ago)
Message:

Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.

Location:
C-semantics
Files:
5 edited

Unmodified
Removed
• ## C-semantics/Integers.ma

 r10 integer (type [Z]) plus a proof that it is in the range 0 (included) to [modulus] (excluded. *) nrecord int: Type ≝ { intval: Z ; intrange: True (*(0 ≤ intval) ∧ intval < modulus*) }. (* XXX: hack to prevent normalization of huge proof term. *) ninductive inrange : Z → Prop ≝ | inrg_mod : ∀i:Z. inrange (i \mod modulus) | inrg_pf : ∀i:Z. (0 ≤ i) ∧ i < modulus → inrange i. ninductive int: Type ≝ | mk_int: ∀i:Z. inrange i → int. (* nrecord int: Type ≝ { intval: Z ; intrange: (0 ≤ intval) ∧ intval < modulus }. *) ndefinition intval: int → Z ≝ λi.match i with [ mk_int x _ ⇒ x ]. ndefinition intrange: ∀i:int. 0 ≤ (intval i) ∧ (intval i) < modulus. #i;ncases i; #x H; ncases H; ##[ #x'; napply modZ_lt_mod; //; ##| //; ##] nqed. (* The [unsigned] and [signed] functions return the Coq integer corresponding (* Conversely, [repr] takes a Coq integer and returns the corresponding machine integer.  The argument is treated modulo [modulus]. *) (* TODO: prove *) (*naxiom repr : Z → int.*) (*naxiom repr_ax : ∀x. 0 ≤ x \mod modulus ∧ x \mod modulus < modulus.*) (* ndefinition repr : Z → int := λx. mk_int x I (*x \mod modulus) ?*) (*Z_mod_lt x modulus modulus_pos*). (*napply repr_ax. nqed.*) mk_int (x \mod modulus) (modZ_lt_mod x modulus modulus_pos). *) ndefinition repr : Z → int ≝ λx. mk_int (x \mod modulus) (inrg_mod x). ndefinition zero := repr 0. ndefinition neg : int → int ≝ λx. repr (- unsigned x). naxiom zero_ext : Z → int → int. naxiom sign_ext : Z → int → int. (* Definition zero_ext (n: Z) (x: int) : int := repr (Zmod (unsigned x) (two_p n)). Definition sign_ext (n: Z) (x: int) : int := repr (let p := two_p n in let y := Zmod (unsigned x) p in if zlt y (two_p (n-1)) then y else y - p). *) ndefinition zero_ext : Z → int → int ≝ λn,x. repr (modZ (unsigned x) (two_p n)). ndefinition sign_ext : Z → int → int ≝ λn,x. repr (let p ≝ two_p n in let y ≝ modZ (unsigned x) p in if Zltb y (two_p (n-1)) then y else y - p). ndefinition add ≝ λx,y: int. repr (unsigned x + unsigned y). (standard behaviour for arithmetic right shift) and [shrx] rounds towards zero. *) naxiom two_p : Z → Z. ndefinition shr : int → int → int ≝ λx,y. repr (signed x / two_p (unsigned y)).
• ## C-semantics/Mem.ma

 r10 ##| #ineq; @1; @1; napply ineq; ##] nqed. (*  XXX: reenable once I've sorted out performance a bit (* XXX: use Or rather than ∨ to bring resource usage under control. *) ndefinition meminj_no_overlap ≝ λmi: meminj. λm: mem. ∀b1,b1',delta1,b2,b2',delta2. mi b1 = Some ? 〈b1', delta1〉 → mi b2 = Some ? 〈b2', delta2〉 → b1' ≠ b2' ∨ low_bound m b1 ≥ high_bound m b1 ∨ low_bound m b2 ≥ high_bound m b2 ∨ (high_bound m b1 + delta1 ≤ low_bound m b2 + delta2 ∨ high_bound m b2 + delta2 ≤ low_bound m b1 + delta1). Or (Or (Or (b1' ≠ b2') (low_bound m b1 ≥ high_bound m b1)) (low_bound m b2 ≥ high_bound m b2)) (Or (high_bound m b1 + delta1 ≤ low_bound m b2 + delta2) (high_bound m b2 + delta2 ≤ low_bound m b1 + delta1)). (* FIXME *) ##| ##3: nwhd in ⊢ (??%?); // ##| ##4,5: //; ##| ##6: nwhd; #chunk;#_; nwhd; @ O; //; ##| ##6: nwhd; #chunk;#_; ncases chunk;//; ##] nqed. nrewrite > (?:repr O = zero); ##[ ##2: // ##] nrewrite > (add_zero ?); nrewrite > (Zplus_z_OZ …); //; ##| (* delta ≠ 0 *) ##] nqed. (* XXX: should use ndestruct, but reduces large definitions *) nremark vptr_eq: ∀b,b',i,i'. Vptr b i = Vptr b' i' → b = b' ∧ i = i'. #b b' i i' e; ndestruct; /2/; nqed. nlemma valid_pointer_inject: ∀f,m1,m2,b,ofs,b',ofs'. ##[ ##1,2,4: #x;#H;ndestruct; ##] #b0;#i;#b0';#i';#delta;#Hb;#Hi';#eptr;#eptr'; (* FIXME want ndestruct to sort this out, but get assertion failure *) nrewrite > (?:b0 = b) in Hb; ##[ ##2: ndestruct; // ##] nrewrite > (?:b0' = b'); ##[ ##2: ndestruct; // ##] nrewrite > (?:i = ofs) in Hi'; ##[ ##2: ndestruct; // ##] nrewrite > (?:i' = ofs'); ##[ ##2: ndestruct; // ##] nrewrite < (proj1 … (vptr_eq ???? eptr)) in Hb; nrewrite < (proj1 … (vptr_eq ???? eptr')); nrewrite < (proj2 … (vptr_eq ???? eptr)) in Hi'; nrewrite < (proj2 … (vptr_eq ???? eptr')); #Hofs; #Hbinj; nrewrite > Hofs; ##| ncases chunk'; #v;#_;#_; @4; ##] (* FIXME: the next two cases are the same *) (* FIXME: the next two cases are very similar *) ##| #chunk'';#i;#i';*;#echunk;nrewrite > echunk;#Hz;#_;#_;#_; nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ndestruct; ##[ ##2,4: nrewrite > Hz; @ ##| ##1,3: nrewrite > (sign_ext_equal_if_zero_equal … Hz); @; nnormalize; nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ##[ ##3,4,5,6,7,10,11,12,13,14: napply False_ind; ndestruct; ##| ##2,9: nwhd in ⊢ (??%%); nrewrite > Hz; @ ##| ##1,8: nwhd in ⊢ (??%%); (* XXX: applying the rewrite directly fails with a unification error, but establishing the equality then using napplyS works! *) nlapply (sign_ext_equal_if_zero_equal … Hz); ##[ ##1,3: @; ##[ ##1,3: napply I; ##| ##2,4: napply leb_true_to_le; @; ##] ##| ##2,4: #H; napplyS val_inject_int; ##] (* original version: nrewrite > (sign_ext_equal_if_zero_equal … Hz); @; nnormalize; ##[ ##1,3: napply I ##| ##2,4: napply leb_true_to_le; @; ##] *) ##] ##| #chunk'';#i;#i';*;#echunk;nrewrite > echunk;#Hz;#_;#_;#_; nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ndestruct; ##[ ##2,4: nrewrite > Hz; @ ##| ##1,3: nrewrite > (sign_ext_equal_if_zero_equal … Hz); @; nnormalize; ##[ ##1,3: napply I ##| ##2,4: napply leb_true_to_le; @; ##] nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ##[ ##1,2,5,6,7,8,9,12,13,14: napply False_ind; ndestruct; ##| ##4,11: nwhd in ⊢ (??%%); nrewrite > Hz; @ ##| ##3,10: nwhd in ⊢ (??%%); (* XXX: actually, napplyS doesn't complete in a reasonable time here; but rewriting on one goal at a time giving the exact position does! *) ##[ nrewrite > (sign_ext_equal_if_zero_equal … Hz) in ⊢ (??(?%)?); @; ##[ ##1,3: napply I; ##| ##2,4: napply leb_true_to_le; @; ##] ##|  nrewrite > (sign_ext_equal_if_zero_equal … Hz) in ⊢ (??(?%)?); @; ##[ ##1,3: napply I; ##| ##2,4: napply leb_true_to_le; @; ##] ##] ##] #Hminj;#ALLOC1;#ALLOC2;#Hlo;#Hhi; napply (alloc_mapped_inject … ALLOC1); /2/; ##[ nlapply (alloc_right_inject … Hminj ALLOC2); //; ##| (* TODO: add to integers *) napply daemon ##[ napply (alloc_right_inject … Hminj ALLOC2); ##| nrewrite > (low_bound_alloc_same … ALLOC2); // ##| nrewrite > (high_bound_alloc_same … ALLOC2); // ncut (f b = Some ? delta); ##[ nwhd in INJb':(??%?); ncases (f b) in INJb' ⊢ %; ##[ #H; ndestruct; ##| #delta'; #H; nelim (grumpydestruct2 ?????? H); // ##] ##[ #H; napply (False_ind … (grumpydestruct … H)); ##| #delta'; #H; nelim (grumpydestruct2 ?????? H); // ##] ##] #INJb; nlapply (valid_pointer_shift_no_overflow … VALID INJb); //; #NOOV; nlapply INJb1; nwhd in ⊢ (??%? → ?); nlapply (refl ? (f b1)); ncases (f b1) in ⊢ (???% → %); ##[ #_; nwhd in ⊢ (??%? → ?); #H; napply False_ind; ndestruct; ##[ #_; nwhd in ⊢ (??%? → ?); #H; napply False_ind; napply (False_ind … (grumpydestruct … H)); ##| #delta'; #DELTA; nwhd in ⊢ (??%? → ?); #H; nelim (grumpydestruct2 ?????? H); #eb;#edelta; ##] nqed. *) (* ** Relation between signed and unsigned loads and stores *) nelim (in_bounds m Mint8unsigned b (signed ofs)); /2/; #H; nwhd in ⊢ (??%%); nelim (getN 0 (signed ofs) (contents (blocks m b))); //; #i; nwhd in ⊢ (??(??%)(??%)); nrewrite > (sign_ext_zero_ext …); //; (* arith *) napply daemon; nqed. nelim (getN 0 (signed ofs) (contents (blocks m b))); ##[ ##1,3,4: //; ##| #i; nwhd in ⊢ (??(??%)(??%)); (* XXX: need to specify which side of the equality to rewrite on to avoid a unification assertion. *) nrewrite > (sign_ext_zero_ext ?? i) in ⊢ (???%); ##[ napply refl; (* XXX: // ? *) ##| (* arith *) napply daemon; ##] ##] nqed.