May 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Get rid of a comparison warning.
by Abramo Bagnara 17 May '09

17 May '09

Module: ppl/ppl Branch: master Commit: 0a171dbe14eed7901117a045b7a3e24783c4178b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0a171dbe14ee… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Sun May 17 14:55:14 2009 +0200 Get rid of a comparison warning. --- src/checked.inlines.hh | 6 +++--- src/checked_float.inlines.hh | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/checked.inlines.hh b/src/checked.inlines.hh index 34d7ce6..9f40671 100644 --- a/src/checked.inlines.hh +++ b/src/checked.inlines.hh @@ -404,9 +404,9 @@ inline Result_Relation sgn_generic(const Type& x) { if (x > 0) return VR_GT; - if (x < 0) - return VR_LT; - return VR_EQ; + if (x == 0) + return VR_EQ; + return VR_LT; } template <typename T1, typename T2, typename Enable = void> diff --git a/src/checked_float.inlines.hh b/src/checked_float.inlines.hh index 4dd7fda..92455b9 100644 --- a/src/checked_float.inlines.hh +++ b/src/checked_float.inlines.hh @@ -722,7 +722,7 @@ sgn_float(const Type x) { return VR_LT; if (x == 0) return VR_EQ; - return VR_EMPTY; + return VR_EMPTY; } template <typename Policy1, typename Policy2, typename Type>

1 0

[GIT] ppl/ppl(master): Simplified code.
by Abramo Bagnara 17 May '09

17 May '09

Module: ppl/ppl Branch: master Commit: a30eaca4651ed3dd7977b028e0a9c4c642b0e340 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a30eaca4651e… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Sun May 17 11:41:21 2009 +0200 Simplified code. --- src/wrap_assign.hh | 25 ++++++++----------------- 1 files changed, 8 insertions(+), 17 deletions(-) diff --git a/src/wrap_assign.hh b/src/wrap_assign.hh index 01c3135..5b1498e 100644 --- a/src/wrap_assign.hh +++ b/src/wrap_assign.hh @@ -309,29 +309,20 @@ wrap_assign(PSET& pointset, if (o == OVERFLOW_UNDEFINED || collective_wrap_too_complex) goto set_full_range; - Coefficient& diff = ud; - diff = last_quadrant - first_quadrant; - - // Please note that the `>=' is intentional here. - if (diff >= UINT_MAX) - goto set_full_range; + Coefficient& quadrants = ud; + quadrants = last_quadrant - first_quadrant + 1; unsigned extension; - assign_r(extension, diff, ROUND_NOT_NEEDED); - ++extension; - assert(extension > 0); - - if (extension > complexity_threshold) + Result r = assign_r(extension, quadrants, ROUND_DIRECT); + if (result_overflow(r) || extension > complexity_threshold) goto set_full_range; if (!wrap_individually && !collective_wrap_too_complex) { - if (collective_wrap_complexity > UINT_MAX / extension) - collective_wrap_too_complex = true; - else { - collective_wrap_complexity *= extension; - if (collective_wrap_complexity > complexity_threshold) + r = mul_assign_r(collective_wrap_complexity, + collective_wrap_complexity, extension, ROUND_DIRECT); + if (result_overflow(r) || + collective_wrap_complexity > complexity_threshold) collective_wrap_too_complex = true; - } if (collective_wrap_too_complex) { // Set all the dimensions in `translations' to full range. for (Wrap_Translations::const_iterator i = translations.begin(),

1 0

[GIT] ppl/ppl(products): After the affine (pre)image operations, unset the reduced flag.
by Patricia Hill 17 May '09

17 May '09

Module: ppl/ppl Branch: products Commit: 7d94d1213ad812f7d2a1cec93763247bdab22d34 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7d94d1213ad8… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Sun May 17 09:04:08 2009 +0100 After the affine (pre)image operations, unset the reduced flag. --- src/Partially_Reduced_Product.inlines.hh | 6 ++++++ .../constraintsproduct1.cc | 12 +++++++++--- 2 files changed, 15 insertions(+), 3 deletions(-) diff --git a/src/Partially_Reduced_Product.inlines.hh b/src/Partially_Reduced_Product.inlines.hh index 534f6ef..cf33f46 100644 --- a/src/Partially_Reduced_Product.inlines.hh +++ b/src/Partially_Reduced_Product.inlines.hh @@ -264,6 +264,7 @@ Partially_Reduced_Product<D1, D2, R> Coefficient_traits::const_reference denominator) { d1.affine_image(var, expr, denominator); d2.affine_image(var, expr, denominator); + clear_reduced_flag(); } template <typename D1, typename D2, typename R> @@ -274,6 +275,7 @@ Partially_Reduced_Product<D1, D2, R> Coefficient_traits::const_reference denominator) { d1.affine_preimage(var, expr, denominator); d2.affine_preimage(var, expr, denominator); + clear_reduced_flag(); } template <typename D1, typename D2, typename R> @@ -285,6 +287,7 @@ Partially_Reduced_Product<D1, D2, R> Coefficient_traits::const_reference denominator) { d1.generalized_affine_image(var, relsym, expr, denominator); d2.generalized_affine_image(var, relsym, expr, denominator); + clear_reduced_flag(); } template <typename D1, typename D2, typename R> @@ -296,6 +299,7 @@ Partially_Reduced_Product<D1, D2, R> Coefficient_traits::const_reference denominator) { d1.generalized_affine_preimage(var, relsym, expr, denominator); d2.generalized_affine_preimage(var, relsym, expr, denominator); + clear_reduced_flag(); } template <typename D1, typename D2, typename R> @@ -306,6 +310,7 @@ Partially_Reduced_Product<D1, D2, R> const Linear_Expression& rhs) { d1.generalized_affine_image(lhs, relsym, rhs); d2.generalized_affine_image(lhs, relsym, rhs); + clear_reduced_flag(); } template <typename D1, typename D2, typename R> @@ -316,6 +321,7 @@ Partially_Reduced_Product<D1, D2, R> const Linear_Expression& rhs) { d1.generalized_affine_preimage(lhs, relsym, rhs); d2.generalized_affine_preimage(lhs, relsym, rhs); + clear_reduced_flag(); } diff --git a/tests/Partially_Reduced_Product/constraintsproduct1.cc b/tests/Partially_Reduced_Product/constraintsproduct1.cc index 444e1f7..0a7f716 100644 --- a/tests/Partially_Reduced_Product/constraintsproduct1.cc +++ b/tests/Partially_Reduced_Product/constraintsproduct1.cc @@ -344,7 +344,7 @@ test10() { cs.insert(D <= 9); Congruence_System cgs; cgs.insert(A %= 0); - cgs.insert((B %= 0) / 15); + cgs.insert((B %= 5) / 15); cgs.insert(C %= 0); cgs.insert(D %= 0); @@ -364,6 +364,8 @@ test10() { gb1.refine_with_constraints(cs); gb1.refine_with_congruences(cgs); gb1.affine_image(A, 2*B + D); + print_constraints(ab1, + "*** (Affine_Space x TBox) ab1 constraints ***"); AffBox ab2(ab1); TBox box2(box1); @@ -406,9 +408,11 @@ test10() { GridBox known_gb(4); known_gb.refine_with_constraints(known_cs); known_gb.refine_with_congruences(cgs); - known_gb.refine_with_congruence((A + 2*B - D %= 0) / 90); + known_gb.refine_with_congruence((A - D %= 20) / 30); + known_gb.refine_with_congruence((B %= 5) / 15); - bool ok = (ab1 == known_ab && box1 == known_box + bool ok = (ab1 == known_ab + && box1 == known_box && affs1 == known_affs && gb1 == known_gb); print_constraints(ab1, @@ -416,6 +420,8 @@ test10() { print_constraints(box1, "*** (TBox) box1 constraints ***"); print_constraints(affs1, "*** (Affine_Space) affs1 constraints ***"); + print_constraints(gb1, + "*** (Grid x TBox) gb1 constraints ***"); print_congruences(gb1, "*** (Grid x TBox) gb1 congruences ***");

1 0

[GIT] ppl/ppl(master): Added more in the section about the wrapping operator.
by Roberto Bagnara 17 May '09

17 May '09

Module: ppl/ppl Branch: master Commit: c3dd71f3d2a0c91b1bb493757c9bcaf7d3e2e3c4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c3dd71f3d2a0… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun May 17 08:44:42 2009 +0200 Added more in the section about the wrapping operator. --- doc/definitions.dox | 11 +++++++++++ 1 files changed, 11 insertions(+), 0 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index c11b9cc..c651cdf 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -512,6 +512,17 @@ tracking multiple program variables. Secondly, the integers modulo 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. +While upper bounds and widening can be used without any precaution, +anything that can be reconducted to intersection requires a preliminary +wrapping phase, where the dimensions corresponding to bounded +integer types are brought back to their natural domain. +This necessity arise naturally for the analysis of conditionals +and conversion operators, as well as in the realization of domain +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.

1 0

[51065] ppl Lint Report
by noreply＠macports.org 17 May '09

17 May '09

Change: http://trac.macports.org/changeset/51065 Portfile: ppl Warning: Line 22 seems to hardcode the version number, consider using ${version} instead Error: Missing required variable: platforms

1 0

[GIT] ppl/ppl(master): More work on the documentation of approximations for bounded integer arithmetic .
by Roberto Bagnara 16 May '09

16 May '09

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

1 0

[GIT] ppl/ppl(master): Bounded_Integer_Type_Signedness renamed Bounded_Integer_Type_Representation .
by Roberto Bagnara 16 May '09

16 May '09

Module: ppl/ppl Branch: master Commit: ead00b0ac972c863e5960555ef868585ec61226f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ead00b0ac972… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat May 16 21:08:08 2009 +0200 Bounded_Integer_Type_Signedness renamed Bounded_Integer_Type_Representation. --- src/BD_Shape.defs.hh | 6 +++--- src/BD_Shape.templates.hh | 4 ++-- src/Box.defs.hh | 6 +++--- src/Box.templates.hh | 4 ++-- src/Grid.defs.hh | 6 +++--- src/Grid_public.cc | 10 +++++----- src/Interval.defs.hh | 10 +++++----- src/Octagonal_Shape.defs.hh | 6 +++--- src/Octagonal_Shape.templates.hh | 4 ++-- src/Polyhedron.defs.hh | 6 +++--- src/Polyhedron_public.cc | 6 +++--- src/globals.types.hh | 2 +- src/wrap_assign.hh | 6 +++--- 13 files changed, 38 insertions(+), 38 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=ead00b0a…

1 0

[GIT] ppl/ppl(master): Comments improved.
by Roberto Bagnara 16 May '09

16 May '09

Module: ppl/ppl Branch: master Commit: 64ad90df3806c6332e62393ddbeded5763f29996 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=64ad90df3806… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat May 16 14:11:38 2009 +0200 Comments improved. --- src/globals.types.hh | 27 ++++++++++++++++++++------- 1 files changed, 20 insertions(+), 7 deletions(-) diff --git a/src/globals.types.hh b/src/globals.types.hh index c1a6f40..35658a9 100644 --- a/src/globals.types.hh +++ b/src/globals.types.hh @@ -71,8 +71,12 @@ enum Optimization_Mode { MAXIMIZATION }; -//! Widths of bounded integer types. -/*! \ingroup PPL_CXX_interface */ +/*! \brief \ingroup PPL_CXX_interface + Widths of bounded integer types. + + See the section on + \ref Approximating_Bounded_Arithmetic "approximating bounded arithmetic". +*/ enum Bounded_Integer_Type_Width { //! \hideinitializer 8 bits. BITS_8 = 8, @@ -90,8 +94,12 @@ enum Bounded_Integer_Type_Width { BITS_128 = 128, }; -//! Signedness of bounded integer types. -/*! \ingroup PPL_CXX_interface */ +/*! \brief \ingroup PPL_CXX_interface + Representation of bounded integer types. + + See the section on + \ref Approximating_Bounded_Arithmetic "approximating bounded arithmetic". +*/ enum Bounded_Integer_Type_Signedness { //! Unsigned integer. UNSIGNED, @@ -100,13 +108,18 @@ enum Bounded_Integer_Type_Signedness { SIGNED_2_COMPLEMENT }; -//! Overflow behavior of bounded integer types. -/*! \ingroup PPL_CXX_interface */ +/*! \brief \ingroup PPL_CXX_interface + Overflow behavior of bounded integer types. + + See the section on + \ref Approximating_Bounded_Arithmetic "approximating bounded arithmetic". +*/ enum Bounded_Integer_Type_Overflow { /*! \brief On overflow, wrapping takes place. - FIXME: formally specify what "wrapping takes place" means. + This means that, for a \f$w\f$-bit bounded integer, the computation + happens modulo \f$2^w\f$. */ OVERFLOW_WRAPS,

1 0

[GIT] ppl/ppl(master): Started writing the section on approximating bounded arithmetic.
by Roberto Bagnara 16 May '09

16 May '09

Module: ppl/ppl Branch: master Commit: f04ae2cea940368690787bf9a370526d497219e7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f04ae2cea940… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat May 16 12:05:35 2009 +0200 Started writing the section on approximating bounded arithmetic. --- doc/definitions.dox | 56 +++++++++++++++++++++++++++++++++++++++++++++++++- 1 files changed, 54 insertions(+), 2 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index 83cd6a7..bcb5b61 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -439,13 +439,65 @@ that are consistent with respect to the desired results. \section Approximating_Bounded_Arithmetic Approximating Bounded Arithmetic -FIXME(0.11): to be written. +The Parma Polyhedra Library provides services that allow to compute +correct approximations of bounded arithmetic as available in widespread +programming languages. Supported bit-widths are 8, 16, 32 and 64 bits, +with some limited support for 128 bits. +Supported representations are binary unsigned and two's complement signed. +Supported overflow behaviors are: +<DL> + <DT>Wrapping:</DT> + <DD> + this means that, for a \f$w\f$-bit bounded integer, the computation + happens modulo \f$2^w\f$. In turn, this signifies that the computation + happens as if the unbounded arithmetic result was computed + 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) + \defeq + x - 2^w \lfloor x/2^w \rfloor. + \f] + For signed integers the wrapping function is, instead, + \f[ + \mathrm{wrap}_\mathrm{s}(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, + &\text{otherwise.} + \end{cases} + \f] + </DD> + <DT>Undefined:</DT> + <DD> + this means that the result of the operation resulting in an + overflow can take any value. This is useful to partially + model systems where overflow has unspecified effects on + the computed result. + Even though something more serious can happen in the system + being analyzed ---due to, e.g., C's undefined behavior---, here we + are only concerned with the results of arithmetic operations. + It is the responsibility of the analyzer to ensure that other + manifestations of undefined behavior are conservatively approximated. + </DD> + <DT>Impossible:</DT> + <DD> + this is for the analysis of languages where overflow is trapped + before it affects the state, for which, thus, any indication that + an overflow may have affected the state is necessarily due to + the imprecision of the analysis. + </DD> +</DL> + +FIXME(0.11): to be continued. +\ref SK07 "[SK07]" \subsection Wrapping_Operator Wrapping Operator FIXME(0.11): to be written. -\ref SK07 "[SK07]" \section convex_polys Convex Polyhedra

1 0

[GIT] ppl/ppl(master): Further cleaning of relation_with(Congruence) implementations.
by Enea Zaffanella 16 May '09

16 May '09

Module: ppl/ppl Branch: master Commit: f28c8bf97087a04310fb24a1bed44163c371ee33 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f28c8bf97087… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat May 16 12:04:14 2009 +0200 Further cleaning of relation_with(Congruence) implementations. --- src/BD_Shape.templates.hh | 45 +++++++++++++------------------------ src/Octagonal_Shape.templates.hh | 31 ++++++++++---------------- src/Polyhedron_public.cc | 37 ++++++++++++++++--------------- 3 files changed, 47 insertions(+), 66 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index f00a885..c57d575 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -1204,24 +1204,17 @@ BD_Shape<T>::max_min(const Linear_Expression& expr, template <typename T> Poly_Con_Relation BD_Shape<T>::relation_with(const Congruence& cg) const { - const dimension_type cg_space_dim = cg.space_dimension(); const dimension_type space_dim = space_dimension(); // Dimension-compatibility check. - if (cg_space_dim > space_dim) + if (cg.space_dimension() > space_dim) throw_dimension_incompatible("relation_with(cg)", cg); // If the congruence is a bounded difference equality, // find the relation with the equivalent equality constraint. if (cg.is_equality()) { Constraint c(cg); - dimension_type num_vars = 0; - dimension_type i = 0; - dimension_type j = 0; - PPL_DIRTY_TEMP_COEFFICIENT(coeff); - if (extract_bounded_difference(c, cg_space_dim, num_vars, - i, j, coeff)) - return relation_with(c); + return relation_with(c); } shortest_path_closure_assign(); @@ -1234,36 +1227,30 @@ BD_Shape<T>::relation_with(const Congruence& cg) const { if (space_dim == 0) { if (cg.is_inconsistent()) return Poly_Con_Relation::is_disjoint(); - else if (cg.inhomogeneous_term() % cg.modulus() == 0) + else return Poly_Con_Relation::saturates() && Poly_Con_Relation::is_included(); } - PPL_DIRTY_TEMP(Coefficient, min_num); - PPL_DIRTY_TEMP(Coefficient, min_den); + // FIXME: add proper comments to the following. + Linear_Expression le = Linear_Expression(cg); + PPL_DIRTY_TEMP_COEFFICIENT(min_num); + PPL_DIRTY_TEMP_COEFFICIENT(min_den); bool min_included; - PPL_DIRTY_TEMP_COEFFICIENT(mod); - mod = cg.modulus(); - Linear_Expression le; - for (dimension_type i = cg_space_dim; i-- > 0; ) - le += cg.coefficient(Variable(i)) * Variable(i); bool bounded_below = minimize(le, min_num, min_den, min_included); if (!bounded_below) return Poly_Con_Relation::strictly_intersects(); - PPL_DIRTY_TEMP_COEFFICIENT(v); - PPL_DIRTY_TEMP_COEFFICIENT(lower_num); - PPL_DIRTY_TEMP_COEFFICIENT(lower_den); - PPL_DIRTY_TEMP_COEFFICIENT(lower); - assign_r(lower_num, min_num, ROUND_NOT_NEEDED); - assign_r(lower_den, min_den, ROUND_NOT_NEEDED); - neg_assign(v, cg.inhomogeneous_term()); - lower = lower_num / lower_den; - v += ((lower / mod) * mod); - if (v * lower_den < lower_num) - v += mod; - const Constraint& c(le == v); + PPL_DIRTY_TEMP_COEFFICIENT(value); + value = min_num / min_den; + const Coefficient& modulus = cg.modulus(); + PPL_DIRTY_TEMP_COEFFICIENT(signed_distance); + signed_distance = value % modulus; + value -= signed_distance; + if (value * min_den < min_num) + value += modulus; + Constraint c(le == value); return relation_with(c); } diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index df6de2d..8f4973b 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -1190,9 +1190,8 @@ Octagonal_Shape<T>::relation_with(const Congruence& cg) const { dimension_type cg_space_dim = cg.space_dimension(); // Dimension-compatibility check. - if (cg_space_dim > space_dim) { + if (cg_space_dim > space_dim) throw_dimension_incompatible("relation_with(cg)", cg); - } // If the congruence is an equality, // find the relation with the equivalent equality constraint. @@ -1211,18 +1210,14 @@ Octagonal_Shape<T>::relation_with(const Congruence& cg) const { if (space_dim == 0) { if (cg.is_inconsistent()) return Poly_Con_Relation::is_disjoint(); - else { - assert(cg.is_tautological()); + else return Poly_Con_Relation::saturates() && Poly_Con_Relation::is_included(); - } } // FIXME: the following code has to be checked and improved. // Add comment to explain what we are doing and why. - const Coefficient& inhomo = cg.inhomogeneous_term(); Linear_Expression le = Linear_Expression(cg); - le -= inhomo; PPL_DIRTY_TEMP_COEFFICIENT(min_num); PPL_DIRTY_TEMP_COEFFICIENT(min_den); bool min_included; @@ -1231,19 +1226,17 @@ Octagonal_Shape<T>::relation_with(const Congruence& cg) const { if (!bounded_below) return Poly_Con_Relation::strictly_intersects(); - PPL_DIRTY_TEMP_COEFFICIENT(val); - neg_assign(val, inhomo); - - PPL_DIRTY_TEMP_COEFFICIENT(lower); - // FIXME: specify rounding mode. - lower = min_num / min_den; - - const Coefficient& mod = cg.modulus(); // FIXME: specify rounding mode. - val += ((lower / mod) * mod); - if (val * min_den < min_num) - val += mod; - Constraint c(le == val); + PPL_DIRTY_TEMP_COEFFICIENT(value); + value = min_num / min_den; + + const Coefficient& modulus = cg.modulus(); + PPL_DIRTY_TEMP_COEFFICIENT(signed_distance); + signed_distance = value % modulus; + value -= signed_distance; + if (value * min_den < min_num) + value += modulus; + Constraint c(le == value); return relation_with(c); } diff --git a/src/Polyhedron_public.cc b/src/Polyhedron_public.cc index a805773..94393b1 100644 --- a/src/Polyhedron_public.cc +++ b/src/Polyhedron_public.cc @@ -310,34 +310,35 @@ PPL::Polyhedron::relation_with(const Congruence& cg) const { // The polyhedron is non-empty so that there exists a point. // For an arbitrary generator point, compute the scalar product with // the equality. - PPL_DIRTY_TEMP_COEFFICIENT(point_val); - + PPL_DIRTY_TEMP_COEFFICIENT(sp_point); for (Generator_System::const_iterator gs_i = gen_sys.begin(), gs_end = gen_sys.end(); gs_i != gs_end; ++gs_i) { if (gs_i->is_point()) { - Scalar_Products::assign(point_val, c, *gs_i); + Scalar_Products::assign(sp_point, c, *gs_i); + expr -= sp_point; break; } } - // Find 2 hyperplanes that satisfy the congruence and are near to + // Find two hyperplanes that satisfy the congruence and are near to // the generating point (so that the point lies on or between these - // hyperplanes). - // Then use the relations between the polyhedron and the corresponding - // halfspaces to determine its relation with the congruence. - const Coefficient& modulus = cg.modulus(); - - // FIXME: specify rounding mode. - PPL_DIRTY_TEMP_COEFFICIENT(nearest); - nearest = (point_val / modulus) * modulus; + // two hyperplanes). + // Then use the relations between the polyhedron and the halfspaces + // corresponding to the hyperplanes to determine the result. - point_val -= nearest; - expr -= nearest; - if (point_val == 0) - return relation_with(expr == 0); + // Compute the distance from the point to an hyperplane. + const Coefficient& modulus = cg.modulus(); + PPL_DIRTY_TEMP_COEFFICIENT(signed_distance); + signed_distance = sp_point % modulus; + if (signed_distance == 0) + // The point is lying on the hyperplane. + return relation_with(expr == 0); + else + // The point is not lying on the hyperplane. + expr += signed_distance; - // Build first halfspace. - const bool positive = (point_val > 0); + // Build first halfspace constraint. + const bool positive = (signed_distance > 0); Constraint first_halfspace = positive ? (expr >= 0) : (expr <= 0); Poly_Con_Relation first_rels = relation_with(first_halfspace);

1 0