Module: ppl/ppl Branch: master Commit: abda7dc37e19d5e24ced391417d8216a2d1aaa10 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=abda7dc37e19d... Author: Roberto Bagnara <bagnara@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 };