Ignore:
Timestamp:
Mar 29, 2011, 5:54:36 PM (10 years ago)
Author:
campbell
Message:

Clean up Clight examples; better temporary definition of multiply.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/memorymodel.ma

    r409 r717  
    1313(**************************************************************************)
    1414
    15 include "Mem.ma".
     15include "common/Mem.ma".
    1616
    1717
     
    2020   access, preventing you reading back more information than the memory can
    2121   store. *)
    22 ndefinition store0 := empty.
    23 ndefinition store1block : mem × block ≝ alloc store0 0 4 Any.
    24 ndefinition store1 : mem ≝ fst ?? store1block.
    25 ndefinition block := snd ?? store1block.
     22definition store0 := empty.
     23definition store1block : mem × block ≝ alloc store0 0 4 Any.
     24definition store1 : mem ≝ fst ?? store1block.
     25definition block := snd ?? store1block.
    2626
    2727(* write a value *)
    28 ndefinition store2 : mem.
    29   nletin r ≝ (store Mint16unsigned store1 Any block 0 (Vint one));
     28definition store2 : mem.
     29  letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint one));
    3030
    31   nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
    32   ##| #rr; #_; napply rr ##] nqed.
     31  lapply (refl ? r); elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
     32  | #rr #_ @rr ] qed.
    3333
    3434(* overwrite the first byte of the value *)
    35 ndefinition store3 : mem.
    36   nletin r ≝ (store Mint8unsigned store1 Any block 0 (Vint one));
     35definition store3 : mem.
     36  letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint one));
    3737
    38   nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
    39   ##| #rr; #_; napply rr ##] nqed.
     38  lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
     39  | #rr #_ @ rr ] qed.
    4040 
    4141(* The size checking rejects the read and gives us Some Vundef. *)
    42 nremark vl_undef: load Mint16signed store3 Any block 0 = Some ? Vundef. //; nqed.
     42example vl_undef: load Mint16signed store3 Any block 0 = Some ? Vundef. @refl qed.
    4343
    4444(* The read is successful and returns a signed version of the value. *)
    45 nremark vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint (zero_ext 8 one)). //; nqed.
     45example vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint (zero_ext 8 one)). // qed.
    4646
    4747(* NB: Double frees are allowed by the memory model (although not necessarily
    4848       by the language). *)
    49 ndefinition store4 := free store3 block.
    50 ndefinition store5 : mem. nletin r ≝ (free store3 block); nwhd in r; napply r; nqed.
     49definition store4 := free store3 block.
     50definition store5 : mem. letin r ≝ (free store3 block); whd in r @r qed.
    5151
    5252(* No ordering is imposed on deallocation (even though alloc and free are only used for
    5353   stack memory in the semantics. *)
    54 ndefinition storeA := empty.
    55 ndefinition storeBblkB := alloc storeA 0 4 Any.
    56 ndefinition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any.
    57 ndefinition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
    58 ndefinition storeE : mem. nletin r ≝ (free storeD (snd ?? storeCblkC)).
    59 nwhd in r; napply r; nqed.
     54definition storeA := empty.
     55definition storeBblkB := alloc storeA 0 4 Any.
     56definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any.
     57definition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
     58definition storeE : mem. letin r ≝ (free storeD (snd ?? storeCblkC)).
     59whd in r @r qed.
    6060
    6161(* Access to the "object representation" (as the C standard puts it) is not specified. *)
    62 ndefinition storeI := empty.
    63 ndefinition storeIIblk := alloc storeA 0 4 Any.
    64 ndefinition storeIII : mem.
    65  nletin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint one));
    66   nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
    67   ##| #rr; #_; napply rr ##] nqed.
    68 ndefinition byte := load Mint8unsigned storeIII Any (snd ?? storeIIblk) 0.
    69 nremark byteundef: byte = Some ? Vundef. //; nqed. (* :( *)
     62definition storeI := empty.
     63definition storeIIblk := alloc storeA 0 4 Any.
     64definition storeIII : mem.
     65 letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint one));
     66  lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
     67  | #rr #_ @rr ] qed.
     68definition byte := load Mint8unsigned storeIII Any (snd ?? storeIIblk) 0.
     69example byteundef: byte = Some ? Vundef. // qed. (* :( *)
Note: See TracChangeset for help on using the changeset viewer.