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

Last change on this file since 1875 was 1875, checked in by campbell, 6 years ago

Update brief memory model test.

File size: 4.1 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 becontentT.
23definition store1block : mem × Σb:block.? ≝ alloc ? store0 0 4 Any.
24definition store1 : mem ≝ fst ?? store1block.
25definition block :block := pi1 … (snd ?? store1block).
26
27(* write a value *)
28definition store2 : mem.
29  letin r ≝ (store (ASTint I16 Unsigned) store1 (mk_pointer Any block (same_compat …) zero_offset) (Vint I16 (repr ? 1)));
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 (ASTint I8 Unsigned) store2 (mk_pointer Any block (same_compat …) zero_offset) (Vint I8 (repr ? 1)));
37
38  lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
39  | #rr #_ @ rr ] qed.
40 
41(* This is what happened under the original CompCert 1.6 ported memory model:
42   The size checking rejects the read and gives us Some Vundef.
43example vl_undef: load (ASTint I16 Signed) store3 (mk_pointer Any block (same_compat …) zero_offset) = Some ? Vundef. @refl qed.
44*)
45(* Now we do byte-wise values and get to see the altered integer. *)
46example vl_changed: load (ASTint I16 Signed) store3 (mk_pointer Any block (same_compat …) zero_offset) = Some ? (Vint I16 (repr ? 257)). @refl qed.
47
48(* The read is successful and returns the value. *)
49example vl_ok': load (ASTint I8 Unsigned) store3 (mk_pointer Any block (same_compat …) zero_offset) = Some ? (Vint I8 (repr ? 1)). // qed.
50
51(* NB: Double frees are allowed by the memory model (although not necessarily
52       by the language). *)
53definition store4 := free ? store3 block.
54definition store5 : mem. letin r ≝ (free ? store3 block); whd in r; @r qed.
55
56(* No ordering is imposed on deallocation (even though alloc and free are only used for
57   stack memory in the semantics. *)
58definition storeA := empty becontentT.
59definition storeBblkB := alloc ? storeA 0 4 Any.
60definition storeCblkC := alloc ? (fst ?? storeBblkB) 0 8 Any.
61definition storeD := free ? (fst ?? storeCblkC) (snd ?? storeBblkB).
62definition storeE : mem. letin r ≝ (free ? storeD (snd ?? storeCblkC)).
63whd in r; @r qed.
64
65(* Access to the "object representation" (as the C standard puts it) was not specified,
66   but can now split up integer values into bytes.  The front-end interface
67   doesn't currently expose parts of pointers. *)
68definition storeI := empty becontentT.
69definition storeIIblk := alloc ? storeA 0 4 Any.
70definition storeIII : mem.
71 letin r ≝ (store (ASTint I32 Unsigned) (fst ?? storeIIblk) (mk_pointer Any (snd ?? storeIIblk) (same_compat …) zero_offset) (Vint I32 (repr ? 1)));
72  lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
73  | #rr #_ @rr ] qed.
74definition byte := load (ASTint I8 Unsigned) storeIII (mk_pointer Any (snd ?? storeIIblk) (same_compat …) zero_offset).
75example byteundef: byte = Some ? (Vint I8 (repr ? 0)). // qed. (* :) *)
Note: See TracBrowser for help on using the repository browser.