Module: ppl/ppl Branch: master Commit: 5a29f32dbb8b1543d8738da6eae2eb318162c22d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5a29f32dbb8b1... Author: Roberto Bagnara <bagnara@cs.unipr.it> Date: Sun May 17 17:42:14 2009 +0200 Finished the documentation about the wrapping operator. --- doc/definitions.dox | 49 ++++++++++++++++++++++++++++++++++++++++++++----- src/globals.types.hh | 6 +++--- 2 files changed, 47 insertions(+), 8 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index c651cdf..ff19299 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -437,7 +437,17 @@ library user to provide the PPL's method with approximations of reality that are consistent with respect to the desired results. -\section Approximating_Bounded_Arithmetic Approximating Bounded Arithmetic +\section Approximating_Integers Approximating Integers + +FIXME(0.11): to be written. + + +\subsection Dropping_Non_Integer_Points Dropping Non-Integer Points + +FIXME(0.11): to be written. + + +\subsection Approximating_Bounded_Integers Approximating Bounded Integers The Parma Polyhedra Library provides services that allow to compute correct approximations of bounded arithmetic as available in widespread @@ -494,7 +504,7 @@ Supported overflow behaviors are: FIXME(0.11): to be continued. -\subsection Wrapping_Operator Wrapping Operator +\subsubsection Wrapping_Operator Wrapping Operator One possibility to precisely approximate the semantics of programs that operate on bounded integer variables is to follow the approach described @@ -522,9 +532,38 @@ combinations. The PPL provides a general wrapping operator that is parametric with respect to the set of space dimensions (variables) to be wrapped, -the width, representation and overflow behavior of all these variables, - -FIXME(0.11): to be continued. +the width, representation and overflow behavior of all these variables. +An optional constraint system allows, when given, to increase the +precision. This constraint system, which must only depend on variables +with respect to which wrapping is performed, is assumed to represent +the conditional or looping construct guard with respect to which +wrapping is performed. Since wrapping requires the computation of +upper bounds and due to non-distributivity of constraint refinement +over upper bounds, passing a constraint system in this way can be more +precise than refining the result of the wrapping operation afterwards. +The general wrapping operator offered by the PPL also allows to control +the complexity/precision ratio by means of two additional parameters: +an unsigned integer encoding a complexity threshold, with higher values +resulting in possibly improved precision; and a Boolean controlling +whether space dimensions should be wrapped individually, something that +results in much greater efficiency to the detriment of precision, +or collectively. + +Note that the PPL assumes that any space dimension subject to wrapping +is being used to capture the value of bounded integer values. As a +consequence the library is free to drop, from the involved numerical +abstraction, any point having a non-integer coordinate in correspondence +of a space dimension subject to wrapping. It must be stressed that +freedom to drop such points does not constitute an obligation to remove +all of them (especially because this would be extraordinarily expensive +on some numerical abstractions). +The PPL provides operators for the more systematic +\ref Dropping_Non_Integer_Points +"removal of points with non-integral coordinates". + +The wrapping operator will only remove some of these points +as a byproduct of its main task and only when this comes at a negligible +extra cost. \section convex_polys Convex Polyhedra diff --git a/src/globals.types.hh b/src/globals.types.hh index 5ed9e76..546445d 100644 --- a/src/globals.types.hh +++ b/src/globals.types.hh @@ -75,7 +75,7 @@ enum Optimization_Mode { Widths of bounded integer types. See the section on - \ref Approximating_Bounded_Arithmetic "approximating bounded arithmetic". + \ref Approximating_Bounded_Integers "approximating bounded integers". */ enum Bounded_Integer_Type_Width { //! \hideinitializer 8 bits. @@ -98,7 +98,7 @@ enum Bounded_Integer_Type_Width { Representation of bounded integer types. See the section on - \ref Approximating_Bounded_Arithmetic "approximating bounded arithmetic". + \ref Approximating_Bounded_Integers "approximating bounded integers". */ enum Bounded_Integer_Type_Representation { //! Unsigned binary. @@ -115,7 +115,7 @@ enum Bounded_Integer_Type_Representation { Overflow behavior of bounded integer types. See the section on - \ref Approximating_Bounded_Arithmetic "approximating bounded arithmetic". + \ref Approximating_Bounded_Integers "approximating bounded integers". */ enum Bounded_Integer_Type_Overflow { /*! \brief