Changeset 14 for C-semantics/Mem.ma


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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Mem.ma

    r10 r14  
    17011701##| #ineq; @1; @1; napply ineq;
    17021702##] 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. *)
    17041705ndefinition meminj_no_overlap ≝ λmi: meminj. λm: mem.
    17051706  ∀b1,b1',delta1,b2,b2',delta2.
     
    17071708  mi b1 = Some ? 〈b1', delta1〉 →
    17081709  mi b2 = Some ? 〈b2', delta2〉 →
    1709   b1' ≠ b2'
    1710   ∨ low_bound m b1 ≥ high_bound m b1
    1711   ∨ low_bound m b2 ≥ high_bound m b2
    1712   ∨ (high_bound m b1 + delta1 ≤ low_bound m b2 + delta2
    1713   ∨ 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)).
    17141715
    17151716(* FIXME *)
     
    22202221##| ##3: nwhd in ⊢ (??%?); //
    22212222##| ##4,5: //;
    2222 ##| ##6: nwhd; #chunk;#_; nwhd; @ O; //;
     2223##| ##6: nwhd; #chunk;#_; ncases chunk;//;
    22232224##] nqed.
    22242225
     
    23532354    nrewrite > (?:repr O = zero); ##[ ##2: // ##]
    23542355    nrewrite > (add_zero ?);
     2356    nrewrite > (Zplus_z_OZ …);
    23552357    //;
    23562358##| (* delta ≠ 0 *)
     
    23872389##] nqed.
    23882390
     2391(* XXX: should use ndestruct, but reduces large definitions *)
     2392nremark 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
    23892395nlemma valid_pointer_inject:
    23902396  ∀f,m1,m2,b,ofs,b',ofs'.
     
    23972403##[ ##1,2,4: #x;#H;ndestruct; ##]
    23982404#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; // ##]
     2405nrewrite < (proj1 … (vptr_eq ???? eptr)) in Hb; nrewrite < (proj1 … (vptr_eq ???? eptr'));
     2406nrewrite < (proj2 … (vptr_eq ???? eptr)) in Hi'; nrewrite < (proj2 … (vptr_eq ???? eptr'));
    24042407  #Hofs; #Hbinj;
    24052408nrewrite > Hofs;
     
    25102513  ##| ncases chunk'; #v;#_;#_; @4;
    25112514  ##]
    2512 (* FIXME: the next two cases are the same *)
     2515(* FIXME: the next two cases are very similar *)
    25132516##| #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;
    25172529        ##[ ##1,3: napply I ##| ##2,4: napply leb_true_to_le; @; ##]
     2530        *)
    25182531    ##]
    25192532
    25202533##| #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        ##]
    25252546    ##]
    25262547
     
    29202941#Hminj;#ALLOC1;#ALLOC2;#Hlo;#Hhi;
    29212942napply (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);
    29242944##| nrewrite > (low_bound_alloc_same … ALLOC2); //
    29252945##| nrewrite > (high_bound_alloc_same … ALLOC2); //
     
    31353155ncut (f b = Some ? delta);
    31363156##[ nwhd in INJb':(??%?); ncases (f b) in INJb' ⊢ %;
    3137   ##[ #H; ndestruct; ##| #delta'; #H; nelim (grumpydestruct2 ?????? H); // ##]
     3157  ##[ #H; napply (False_ind … (grumpydestruct … H)); ##| #delta'; #H; nelim (grumpydestruct2 ?????? H); // ##]
    31383158##] #INJb;
    31393159nlapply (valid_pointer_shift_no_overflow … VALID INJb); //; #NOOV;
     
    31713191nlapply INJb1; nwhd in ⊢ (??%? → ?);
    31723192nlapply (refl ? (f b1)); ncases (f b1) in ⊢ (???% → %);
    3173 ##[ #_; nwhd in ⊢ (??%? → ?); #H; napply False_ind; ndestruct;
     3193##[ #_; nwhd in ⊢ (??%? → ?); #H; napply False_ind; napply (False_ind … (grumpydestruct … H));
    31743194##| #delta'; #DELTA; nwhd in ⊢ (??%? → ?); #H; nelim (grumpydestruct2 ?????? H);
    31753195    #eb;#edelta;
     
    34353455##]
    34363456nqed.
    3437 *)
     3457
    34383458(* ** Relation between signed and unsigned loads and stores *)
    34393459
     
    34863506nelim (in_bounds m Mint8unsigned b (signed ofs)); /2/;
    34873507#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.
     3508nelim (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##]
     3517nqed.
Note: See TracChangeset for help on using the changeset viewer.