ValueDomain: add some documentation comments.

1 files changed, 32 insertions, 20 deletions

diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index b91d6b98..3d95bdd1 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -64,7 +64,11 @@ Variable bc: block_classification.
 
 (** * Abstracting the result of conditions (type [option bool]) *)
 
-Inductive abool := Bnone | Just (b: bool) | Maybe (b: bool) | Btop.
+Inductive abool :=
+  | Bnone               (**r always [None] (undefined) *)
+  | Just (b: bool)      (**r always [Some b] (defined and known to be [b]) *)
+  | Maybe (b: bool)     (**r either [None] or [Some b] (known to be [b] if defined) *)
+  | Btop.               (**r unknown, all results are possible *)
 
 Inductive cmatch: option bool -> abool -> Prop :=
   | cmatch_none: cmatch None Bnone
@@ -121,14 +125,14 @@ Qed.
 (** * Abstracting pointers *)
 
 Inductive aptr : Type :=
-  | Pbot
-  | Gl (id: ident) (ofs: int)
-  | Glo (id: ident)
-  | Glob
-  | Stk (ofs: int)
-  | Stack
-  | Nonstack
-  | Ptop.
+  | Pbot                        (**r bottom (empty set of pointers) *)
+  | Gl (id: ident) (ofs: int)   (**r pointer into the block for global variable [id] at offset [ofs] *)
+  | Glo (id: ident)             (**r pointer anywhere into the block for global [id] *)
+  | Glob                        (**r pointer into any global variable *)
+  | Stk (ofs: int)              (**r pointer into the current stack frame at offset [ofs] *)
+  | Stack                       (**r pointer anywhere into the current stack frame *)
+  | Nonstack                    (**r pointer anywhere but into the current stack frame *)
+  | Ptop.                       (**r any valid pointer *)
 
 Definition eq_aptr: forall (p1 p2: aptr), {p1=p2} + {p1<>p2}.
 Proof.
@@ -512,15 +516,25 @@ Qed.
 (** * Abstracting values *)
 
 Inductive aval : Type :=
-  | Vbot
-  | I (n: int)
-  | Uns (p: aptr) (n: Z)
-  | Sgn (p: aptr) (n: Z)
-  | L (n: int64)
-  | F (f: float)
-  | FS (f: float32)
-  | Ptr (p: aptr)
-  | Ifptr (p: aptr).
+  | Vbot                     (**r bottom (empty set of values) *)
+  | I (n: int)               (**r exactly [Vint n] *)
+  | Uns (p: aptr) (n: Z)     (**r a [n]-bit unsigned integer, or [Vundef] *)
+  | Sgn (p: aptr) (n: Z)     (**r a [n]-bit signed integer, or [Vundef] *)
+  | L (n: int64)             (**r exactly [Vlong n] *)
+  | F (f: float)             (**r exactly [Vfloat f] *)
+  | FS (f: float32)          (**r exactly [Vsingle f] *)
+  | Ptr (p: aptr)            (**r a pointer from the set [p], or [Vundef] *)
+  | Ifptr (p: aptr).         (**r a pointer from the set [p], or a number, or [Vundef] *)
+
+(** The "top" of the value domain is defined as any pointer, or any
+    number, or [Vundef]. *)
+
+Definition Vtop := Ifptr Ptop.
+
+(** The [p] parameter (an abstract pointer) to [Uns] and [Sgn] helps keeping
+  track of pointers that leak through arithmetic operations such as shifts.
+  See the section "Tracking leakage of pointers" below.
+  In strict analysis mode, [p] is always [Pbot]. *)
 
 Definition eq_aval: forall (v1 v2: aval), {v1=v2} + {v1<>v2}.
 Proof.
@@ -528,8 +542,6 @@ Proof.
   decide equality. 
 Defined.
 
-Definition Vtop := Ifptr Ptop.
-
 Definition is_uns (n: Z) (i: int) : Prop :=
   forall m, 0 <= m < Int.zwordsize -> m >= n -> Int.testbit i m = false.
 Definition is_sgn (n: Z) (i: int) : Prop :=