[PPL-devel] [GIT] ppl/ppl(master): More work on the documentation of approximations for bounded integer arithmetic .

[Roberto Bagnara]

Module: ppl/ppl
Branch: master
Commit: abda7dc37e19d5e24ced391417d8216a2d1aaa10
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=abda7dc37e19d5e24ced391417d8216a2d1aaa10

Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date:   Sat May 16 22:25:18 2009 +0200

More work on the documentation of approximations for bounded integer arithmetic.

---

 doc/definitions.dox  |   30 +++++++++++++++++++++++-------
 src/globals.types.hh |    7 +++++--
 2 files changed, 28 insertions(+), 9 deletions(-)

diff --git a/doc/definitions.dox b/doc/definitions.dox
index bcb5b61..c11b9cc 100644
--- a/doc/definitions.dox
+++ b/doc/definitions.dox
@@ -454,18 +454,18 @@ Supported overflow behaviors are:
     and then wrapped.  For unsigned integers, the wrapping function is
     simply \f$x \bmod 2^w\f$, most conveniently defined as
     \f[
-      \mathrm{wrap}_\mathrm{u}(x)
+      \mathrm{wrap}^\mathrm{u}_w(x)
         \defeq
           x - 2^w \lfloor x/2^w \rfloor.
     \f]
     For signed integers the wrapping function is, instead,
     \f[
-      \mathrm{wrap}_\mathrm{s}(x)
+      \mathrm{wrap}^\mathrm{s}_w(x)
         \defeq
           \begin{cases}
-            \mathrm{wrap}_\mathrm{u}(x),
-              &\text{if $\mathrm{wrap}_\mathrm{u}(x) < 2^{w-1}$;} \\
-            \mathrm{wrap}_\mathrm{u}(x) - 2^w,
+            \mathrm{wrap}^\mathrm{u}_w(x),
+              &\text{if $\mathrm{wrap}^\mathrm{u}_w(x) < 2^{w-1}$;} \\
+            \mathrm{wrap}^\mathrm{u}_w(x) - 2^w,
               &\text{otherwise.}
           \end{cases}
     \f]
@@ -492,12 +492,28 @@ Supported overflow behaviors are:
 </DL>
 
 FIXME(0.11): to be continued.
-\ref SK07 "[SK07]"
 
 
 \subsection Wrapping_Operator Wrapping Operator
 
-FIXME(0.11): to be written.
+One possibility to precisely approximate the semantics of programs that
+operate on bounded integer variables is to follow the approach described
+in \ref SK07 "[SK07]".  The idea is to associate space dimensions to the
+<EM>unwrapped values</EM> of bounded variables.  Suppose <CODE>j</CODE>
+is a \f$w\f$-bit, unsigned program variable associated to a space dimension
+labeled by the variable \f$x\f$.  If \f$x\f$ is constrained by some
+numerical abstraction to take values in a set \f$S \sseq \Rset\f$, then
+the program variable <CODE>j</CODE> can only take values in
+\f$\bigl\{\, \mathrm{wrap}^\mathrm{u}_w(z) \bigm| z \in S \,\bigr\}\f$.
+There are two reasons why this is interesting: firstly, this allows
+to retain relational information by using a single numerical abstraction
+tracking multiple program variables.  Secondly, the integers modulo
+\f$2^w\f$ form a ring of equivalence classes on which addition
+and multiplication are well defined.  This means, e.g., that assignments
+with affine right-hand sides and involving only variables with the same
+bit-width and representation can be safely modeled by affine images.
+
+FIXME(0.11): to be continued.
 
 
 \section convex_polys Convex Polyhedra
diff --git a/src/globals.types.hh b/src/globals.types.hh
index 340e8e7..5ed9e76 100644
--- a/src/globals.types.hh
+++ b/src/globals.types.hh
@@ -101,10 +101,13 @@ enum Bounded_Integer_Type_Width {
   \ref Approximating_Bounded_Arithmetic "approximating bounded arithmetic".
 */
 enum Bounded_Integer_Type_Representation {
-  //! Unsigned integer.
+  //! Unsigned binary.
   UNSIGNED,
 
-  //! Signed integer represented by the two's complement of the absolute value.
+  /*! \brief
+    Signed binary where negative values are represented by the two's
+    complement of the absolute value.
+  */
   SIGNED_2_COMPLEMENT
 };