From f774d5f2d604f747e72e2d3bb56cc3f90090e2dd Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 15 Feb 2013 16:24:13 +0000
Subject: Pointers one past

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 common/Memtype.v | 53 +++++++++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 47 insertions(+), 6 deletions(-)

(limited to 'common/Memtype.v')

diff --git a/common/Memtype.v b/common/Memtype.v
index a39daf41..59dc7a3b 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -259,6 +259,22 @@ Axiom valid_pointer_valid_access:
   forall m b ofs,
   valid_pointer m b ofs = true <-> valid_access m Mint8unsigned b ofs Nonempty.
 
+(** C allows pointers one past the last element of an array.  These are not
+  valid according to the previously defined [valid_pointer]. The property
+  [weak_valid_pointer m b ofs] holds if address [b, ofs] is a valid pointer
+  in [m], or a pointer one past a valid block in [m].  *)
+
+Definition weak_valid_pointer (m: mem) (b: block) (ofs: Z) :=
+  valid_pointer m b ofs || valid_pointer m b (ofs - 1).
+
+Axiom weak_valid_pointer_spec:
+  forall m b ofs,
+  weak_valid_pointer m b ofs = true <->
+    valid_pointer m b ofs = true \/ valid_pointer m b (ofs - 1) = true.
+Axiom valid_pointer_implies:
+  forall m b ofs,
+  valid_pointer m b ofs = true -> weak_valid_pointer m b ofs = true.
+
 (** * Properties of the memory operations *)
 
 (** ** Properties of the initial memory state. *)
@@ -899,6 +915,10 @@ Axiom valid_access_extends:
 Axiom valid_pointer_extends:
   forall m1 m2 b ofs,
   extends m1 m2 -> valid_pointer m1 b ofs = true -> valid_pointer m2 b ofs = true.
+Axiom weak_valid_pointer_extends:
+  forall m1 m2 b ofs,
+  extends m1 m2 ->
+  weak_valid_pointer m1 b ofs = true -> weak_valid_pointer m2 b ofs = true.
 
 (** * Memory injections *)
 
@@ -950,19 +970,33 @@ Axiom valid_pointer_inject:
   valid_pointer m1 b1 ofs = true ->
   valid_pointer m2 b2 (ofs + delta) = true.
 
+Axiom weak_valid_pointer_inject:
+  forall f m1 m2 b1 ofs b2 delta,
+  f b1 = Some(b2, delta) ->
+  inject f m1 m2 ->
+  weak_valid_pointer m1 b1 ofs = true ->
+  weak_valid_pointer m2 b2 (ofs + delta) = true.
+
 Axiom address_inject:
-  forall f m1 m2 b1 ofs1 b2 delta,
+  forall f m1 m2 b1 ofs1 b2 delta p,
   inject f m1 m2 ->
-  perm m1 b1 (Int.unsigned ofs1) Max Nonempty ->
+  perm m1 b1 (Int.unsigned ofs1) Cur p ->
   f b1 = Some (b2, delta) ->
   Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta.
 
 Axiom valid_pointer_inject_no_overflow:
-  forall f m1 m2 b ofs b' x,
+  forall f m1 m2 b ofs b' delta,
   inject f m1 m2 ->
   valid_pointer m1 b (Int.unsigned ofs) = true ->
-  f b = Some(b', x) ->
-  0 <= Int.unsigned ofs + Int.unsigned (Int.repr x) <= Int.max_unsigned.
+  f b = Some(b', delta) ->
+  0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
+
+Axiom weak_valid_pointer_inject_no_overflow:
+  forall f m1 m2 b ofs b' delta,
+  inject f m1 m2 ->
+  weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
+  f b = Some(b', delta) ->
+  0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
 
 Axiom valid_pointer_inject_val:
   forall f m1 m2 b ofs b' ofs',
@@ -971,6 +1005,13 @@ Axiom valid_pointer_inject_val:
   val_inject f (Vptr b ofs) (Vptr b' ofs') ->
   valid_pointer m2 b' (Int.unsigned ofs') = true.
 
+Axiom weak_valid_pointer_inject_val:
+  forall f m1 m2 b ofs b' ofs',
+  inject f m1 m2 ->
+  weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
+  val_inject f (Vptr b ofs) (Vptr b' ofs') ->
+  weak_valid_pointer m2 b' (Int.unsigned ofs') = true.
+
 Axiom inject_no_overlap:
   forall f m1 m2 b1 b2 b1' b2' delta1 delta2 ofs1 ofs2,
   inject f m1 m2 ->
@@ -1103,7 +1144,7 @@ Axiom alloc_left_mapped_inject:
   alloc m1 lo hi = (m1', b1) ->
   valid_block m2 b2 ->
   0 <= delta <= Int.max_unsigned ->
-  (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs <= Int.max_unsigned) ->
+  (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs < Int.max_unsigned) ->
   (forall ofs k p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) k p) ->
   inj_offset_aligned delta (hi-lo) ->
   (forall b delta' ofs k p,
-- 
cgit