source: src/Clight/test/memorymodel.ma @ 717

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

Clean up Clight examples; better temporary definition of multiply.

File size: 3.3 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 "common/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. *)
22definition store0 := empty.
23definition store1block : mem × block ≝ alloc store0 0 4 Any.
24definition store1 : mem ≝ fst ?? store1block.
25definition block := snd ?? store1block.
26
27(* write a value *)
28definition store2 : mem.
29  letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint one));
30
31  lapply (refl ? r); elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
32  | #rr #_ @rr ] qed.
33
34(* overwrite the first byte of the value *)
35definition store3 : mem.
36  letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint one));
37
38  lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
39  | #rr #_ @ rr ] qed.
40 
41(* The size checking rejects the read and gives us Some Vundef. *)
42example vl_undef: load Mint16signed store3 Any block 0 = Some ? Vundef. @refl qed.
43
44(* The read is successful and returns a signed version of the value. *)
45example vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint (zero_ext 8 one)). // qed.
46
47(* NB: Double frees are allowed by the memory model (although not necessarily
48       by the language). *)
49definition store4 := free store3 block.
50definition store5 : mem. letin r ≝ (free store3 block); whd in r @r qed.
51
52(* No ordering is imposed on deallocation (even though alloc and free are only used for
53   stack memory in the semantics. *)
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.
60
61(* Access to the "object representation" (as the C standard puts it) is not specified. *)
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 TracBrowser for help on using the repository browser.