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

Last change on this file since 3 was 3, checked in by campbell, 11 years ago

Import work-in-progress port of the CompCert? C semantics to matita.

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(* write a value *)
27ndefinition store2 : mem.
28  nletin r ≝ (store Mint16unsigned store1 block 0 (Vint one));
29  nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
30  ##| #rr; #_; napply rr ##] nqed.
31(* overwrite the first byte of the value *)
32ndefinition store3 : mem.
33  nletin r ≝ (store Mint8unsigned store1 block 0 (Vint one));
34  nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
35  ##| #rr; #_; napply rr ##] nqed.
36 
37ndefinition vl := load Mint16signed store3 block 0.
38(* The size checking rejects the read and gives us Some Vundef. *)
39nremark vl_undef: vl = Some ? Vundef. //; nqed.
40
41ndefinition vl' := load Mint8unsigned store3 block 0.
42(* The read is successful and returns a signed version of the value. *)
43nremark vl_ok': vl' = Some ? (Vint (zero_ext 8 one)). //; nqed.
44
45ndefinition store4 := free store3 block.
46(* NB: Double frees are allowed by the memory model (although not necessarily
47       by the language). *)
48ndefinition store5 : mem. nletin r ≝ (free store3 block); nwhd in r; napply r; nqed.
49
50(* No ordering is imposed on deallocation (even though alloc and free are only used for
51   stack memory in the semantics. *)
52ndefinition storeA := empty.
53ndefinition storeBblkB := alloc storeA 0 4.
54ndefinition storeCblkC := alloc (fst ?? storeBblkB) 0 8.
55ndefinition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
56ndefinition storeE : mem. nletin r ≝ (free storeD (snd ?? storeCblkC)).
57nwhd in r; napply r; nqed.
58
59(* Access to the "object representation" (as the C standard puts it) is not specified. *)
60ndefinition storeI := empty.
61ndefinition storeIIblk := alloc storeA 0 4.
62ndefinition storeIII : mem.
63 nletin r ≝ (store Mint32 (fst ?? storeIIblk) (snd ?? storeIIblk) 0 (Vint one));
64  nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
65  ##| #rr; #_; napply rr ##] nqed.
66ndefinition byte := load Mint8unsigned storeIII (snd ?? storeIIblk) 0.
67nremark byteundef: byte = Some ? Vundef. //; nqed. (* :( *)
Note: See TracBrowser for help on using the repository browser.