source: C-semantics/test/memorymodel.ma @ 12

Last change on this file since 12 was 12, checked in by campbell, 9 years ago

Make memory model tests more readable.
Update README.

File size: 3.4 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "Mem.ma".
16
17
18(* The memory model stores the entire value regardless of whether it fits in
19   the amount of memory used.  Fortunately, it checks the size of the memory
20   access, preventing you reading back more information than the memory can
21   store. *)
22ndefinition store0 := empty.
23ndefinition store1block : mem × block ≝ alloc store0 0 4.
24ndefinition store1 : mem ≝ fst ?? store1block.
25ndefinition block := snd ?? store1block.
26
27(* write a value *)
28ndefinition store2 : mem.
29  nletin r ≝ (store Mint16unsigned store1 block 0 (Vint one));
30
31  nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
32  ##| #rr; #_; napply rr ##] nqed.
33
34(* overwrite the first byte of the value *)
35ndefinition store3 : mem.
36  nletin r ≝ (store Mint8unsigned store1 block 0 (Vint one));
37
38  nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
39  ##| #rr; #_; napply rr ##] nqed.
40 
41(* The size checking rejects the read and gives us Some Vundef. *)
42nremark vl_undef: load Mint16signed store3 block 0 = Some ? Vundef. //; nqed.
43
44(* The read is successful and returns a signed version of the value. *)
45nremark vl_ok': load Mint8unsigned store3 block 0 = Some ? (Vint (zero_ext 8 one)). //; nqed.
46
47(* NB: Double frees are allowed by the memory model (although not necessarily
48       by the language). *)
49ndefinition store4 := free store3 block.
50ndefinition store5 : mem. nletin r ≝ (free store3 block); nwhd in r; napply r; nqed.
51
52(* No ordering is imposed on deallocation (even though alloc and free are only used for
53   stack memory in the semantics. *)
54ndefinition storeA := empty.
55ndefinition storeBblkB := alloc storeA 0 4.
56ndefinition storeCblkC := alloc (fst ?? storeBblkB) 0 8.
57ndefinition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
58ndefinition storeE : mem. nletin r ≝ (free storeD (snd ?? storeCblkC)).
59nwhd in r; napply r; nqed.
60
61(* Access to the "object representation" (as the C standard puts it) is not specified. *)
62ndefinition storeI := empty.
63ndefinition storeIIblk := alloc storeA 0 4.
64ndefinition storeIII : mem.
65 nletin r ≝ (store Mint32 (fst ?? storeIIblk) (snd ?? storeIIblk) 0 (Vint one));
66  nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
67  ##| #rr; #_; napply rr ##] nqed.
68ndefinition byte := load Mint8unsigned storeIII (snd ?? storeIIblk) 0.
69nremark byteundef: byte = Some ? Vundef. //; nqed. (* :( *)
Note: See TracBrowser for help on using the repository browser.