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

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

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File size: 3.9 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/FrontEndMem.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 × Σb:block.? ≝ alloc store0 0 4 XData.
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 block 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 block 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 block 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 block 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 block 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.
59definition storeBblkB := alloc storeA 0 4 XData.
60definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 XData.
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.
69definition storeIIblk := alloc storeI 0 4 XData.
70definition storeIII : mem.
71 letin r ≝ (store (ASTint I32 Unsigned) (fst ?? storeIIblk) (mk_pointer (snd ?? storeIIblk) 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 (snd ?? storeIIblk) zero_offset).
75example byteundef: byte = Some ? (Vint I8 (repr ? 0)). // qed. (* :) *)
76
Note: See TracBrowser for help on using the repository browser.