Changeset 717 for src/Clight/test/memorymodel.ma
 Timestamp:
 Mar 29, 2011, 5:54:36 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/test/memorymodel.ma
r409 r717 13 13 (**************************************************************************) 14 14 15 include " Mem.ma".15 include "common/Mem.ma". 16 16 17 17 … … 20 20 access, preventing you reading back more information than the memory can 21 21 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.22 definition store0 := empty. 23 definition store1block : mem × block ≝ alloc store0 0 4 Any. 24 definition store1 : mem ≝ fst ?? store1block. 25 definition block := snd ?? store1block. 26 26 27 27 (* write a value *) 28 ndefinition store2 : mem.29 nletin r ≝ (store Mint16unsigned store1 Any block 0 (Vint one));28 definition store2 : mem. 29 letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint one)); 30 30 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. 33 33 34 34 (* overwrite the first byte of the value *) 35 ndefinition store3 : mem.36 nletin r ≝ (store Mint8unsigned store1 Any block 0 (Vint one));35 definition store3 : mem. 36 letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint one)); 37 37 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. 40 40 41 41 (* The size checking rejects the read and gives us Some Vundef. *) 42 nremark vl_undef: load Mint16signed store3 Any block 0 = Some ? Vundef. //; nqed.42 example vl_undef: load Mint16signed store3 Any block 0 = Some ? Vundef. @refl qed. 43 43 44 44 (* 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.45 example vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint (zero_ext 8 one)). // qed. 46 46 47 47 (* NB: Double frees are allowed by the memory model (although not necessarily 48 48 by the language). *) 49 ndefinition store4 := free store3 block.50 ndefinition store5 : mem. nletin r ≝ (free store3 block); nwhd in r; napply r; nqed.49 definition store4 := free store3 block. 50 definition store5 : mem. letin r ≝ (free store3 block); whd in r @r qed. 51 51 52 52 (* No ordering is imposed on deallocation (even though alloc and free are only used for 53 53 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.54 definition storeA := empty. 55 definition storeBblkB := alloc storeA 0 4 Any. 56 definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any. 57 definition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB). 58 definition storeE : mem. letin r ≝ (free storeD (snd ?? storeCblkC)). 59 whd in r @r qed. 60 60 61 61 (* 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. (* :( *)62 definition storeI := empty. 63 definition storeIIblk := alloc storeA 0 4 Any. 64 definition 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. 68 definition byte := load Mint8unsigned storeIII Any (snd ?? storeIIblk) 0. 69 example byteundef: byte = Some ? Vundef. // qed. (* :( *)
Note: See TracChangeset
for help on using the changeset viewer.