September 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(pip): Bug fixes.
by François Galea 21 Sep '09

21 Sep '09

Module: ppl/ppl Branch: pip Commit: b5208ce53cc4f481386629a7373a7024263946be URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b5208ce53cc4… Author: François Galea <francois.galea(a)uvsq.fr> Date: Mon Sep 21 15:58:16 2009 +0200 Bug fixes. --- src/PIP_Tree.cc | 30 +++++++++++++++++------------- 1 files changed, 17 insertions(+), 13 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 8ed994e..45d25e1 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -48,7 +48,7 @@ merge_assign(Matrix& x, const Constraint_System& y) { PPL_ASSERT(y_i->is_nonstrict_inequality()); for (dimension_type j=width-1; j-- > 0; ) row[j+1] = y_i->coefficient(Variable(j)); - row[0] = -y_i->inhomogeneous_term(); + row[0] = y_i->inhomogeneous_term(); x.add_row(row); } } @@ -448,7 +448,7 @@ PIP_Solution_Node::compatibility_check(const Matrix &ctx, const Row &cnst) { /* Perform simplex pivots on the context until we find an empty solution * or an optimum */ - for(;;) { + for (;;) { // Look for a negative RHS (=constant term, stored in matrix column 0) i = 0; while (i<num_rows && s[i][0] >= 0) @@ -475,6 +475,8 @@ PIP_Solution_Node::compatibility_check(const Matrix &ctx, const Row &cnst) { continue; const Coefficient &sij_ = p[j_]; for (k=0; k<num_rows; ++k) { + if (k == i) + continue; Coefficient mult = s[k][j] * sij_; if (mult % sij != 0) { // Must scale row to stay in integer case @@ -486,6 +488,7 @@ PIP_Solution_Node::compatibility_check(const Matrix &ctx, const Row &cnst) { } s[k][j_] -= mult / sij; } + s[i][j_] = 0; } for (k=0; k<num_rows; ++k) { Coefficient skj = s[k][j]; @@ -497,7 +500,7 @@ PIP_Solution_Node::compatibility_check(const Matrix &ctx, const Row &cnst) { add_assign(s[k], s[k], scale_factor); skj *= scale_factor; } - s[k][j_] = skj/sij; + s[k][j] = skj/sij; } } @@ -543,7 +546,7 @@ PIP_Solution_Node::update_tableau(PIP_Tree_Node ** /* parent_ref */, int p = 1; Row var(n_vars, tableau.s.capacity(), Row::Flags()); Row param(n_params+1, tableau.t.capacity(), Row::Flags()); - Coefficient cnst_term = -cst->inhomogeneous_term(); + Coefficient cnst_term = cst->inhomogeneous_term(); if (cst->is_strict_inequality()) // convert c > 0 <=> c-1 >= 0 cnst_term -= 1; @@ -643,7 +646,7 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, Either the problem is empty, or a pivoting step is required */ if (i_ != n_a_d) { -#if NOISY_PIP +#ifdef NOISY_PIP std::cout << "Found row with negative parameters: " << i_ << std::endl; #endif @@ -685,7 +688,7 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, /* If no positive S_ij: problem is empty */ if (j_ == n_a_d) { -#if NOISY_PIP +#ifdef NOISY_PIP std::cout << "No positive pivot found: Solution = _|_" << std::endl; #endif @@ -693,7 +696,7 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, delete this; return UNFEASIBLE_PIP_PROBLEM; } -#if NOISY_PIP +#ifdef NOISY_PIP std::cout << "Pivot column: " << j_ << std::endl; #endif @@ -833,12 +836,13 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, context.add_row(r); add_constraint(r); #ifdef NOISY_PIP - Linear_Expression e; - for (j=1; j<num_params; ++j) - e += r[j] * Variable(j-1); - Constraint c(e + r[0] >= 0); - std::cout << "Adding tautology: " << c - << std::endl; + Constraint_System::const_iterator c = constraints_.begin(); + Constraint_System::const_iterator c_end = constraints_.end(); + Constraint_System::const_iterator c1 = c; + while (++c1 != constraints_.end()) + c = c1; + std::cout << "Adding tautology: "; + c->ascii_dump(std::cout); #endif } else { #ifdef NOISY_PIP

1 0

[GIT] ppl/ppl(floating_point): Added a few lines of documentation that were previously forgotten.
by Fabio Bossi 21 Sep '09

21 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 171b89c7ecd9440017606fb6fd8d51659368f322 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=171b89c7ecd9… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Sep 21 15:56:47 2009 +0200 Added a few lines of documentation that were previously forgotten. --- src/Octagonal_Shape.defs.hh | 4 +++- 1 files changed, 3 insertions(+), 1 deletions(-) diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 60f7f58..111d2de 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -1005,7 +1005,9 @@ public: \exception std::invalid_argument Thrown if \p left (or \p right) is dimension-incompatible with \p *this. - + This function is used in abstract interpretation to model a filter + that is generated by a comparison of two expressions that are correctly + approximated by \p left and \p right respectively. */ template <typename Interval_Info> void refine_with_linear_form_inequality(

1 0

[GIT] ppl/ppl(floating_point): Added some more documentation.
by Fabio Bossi 21 Sep '09

21 Sep '09

Module: ppl/ppl Branch: floating_point Commit: e382dfd1d7fa78031d49b05b7bbc0fac51ca3aa9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e382dfd1d7fa… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Sep 21 15:41:16 2009 +0200 Added some more documentation. --- src/Polyhedron.defs.hh | 60 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 files changed, 60 insertions(+), 0 deletions(-) diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index 3c3a9d5..7ecc2cf 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -2628,6 +2628,25 @@ protected: //@} // Exception Throwers #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) + //! Helper function that overapproximates an interval linear form. + /*! + \param lf + The linear form on intervals with floating point boundaries to approximate. + + \param lf_dimension + Must be the space dimension of \p lf. + + \param store + The interval abstract store in which the approximation is performed. + + \param result + Used to store the result. + + This function makes \p result become a linear form that is a correct + approximation of \p lf in \p store. The resulting linear form has the + property that all of its variable coefficients have a non-significative + upper bound and can thus be considered as singletons. + */ template <typename FP_Format, typename Interval_Info> static void overapproximate_linear_form( const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, @@ -2635,12 +2654,53 @@ protected: const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store, Linear_Form<Interval <FP_Format, Interval_Info> >& result); + /*! \brief + Helper function that makes \p result become a Linear_Expression obtained + by normalizing the denominators in \p lf. + + \param lf + The linear form on intervals with floating point boundarie to normalize. + It should be the result of an application of static method + <CODE>overapproximate_linear_form</CODE>. + + \param l_dimension + Must be the space dimension of \p lf. + + \param result + Used to store the result. + + This function ignores the upper bound of intervals in \p lf, + so that in fact the result can be seen as \p lf multiplied by a proper + normalization constant. + */ template <typename FP_Format, typename Interval_Info> static void convert_to_integer_expression( const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, const dimension_type lf_dimension, Linear_Expression& result); + //! Normalization helper function. + /*! + \param lf + The linear form on intervals with floating point boundaries to normalize. + It should be the result of an application of static method + <CODE>overapproximate_linear_form</CODE>. + + \param lf_dimension + Must be the space dimension of \p lf. + + \param res + Stores the normalized linear form, except its inhomogeneous term. + + \param res_low_coeff + Stores the lower boundary of the inhomogeneous term of the result. + + \param res_hi_coeff + Stores the higher boundary of the inhomogeneous term of the result. + + Results are obtained by normalizing denominators in \p lf, ignoring + the upper bounds of variable coefficients in \p lf. + */ template <typename FP_Format, typename Interval_Info> static void convert_to_integer_expressions( const Linear_Form<Interval <FP_Format, Interval_Info> >& lf,

1 0

[GIT] ppl/ppl(floating_point): Fixed a bug in affine_image and implemented three new tests.
by Roberto Amadini 21 Sep '09

21 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 726d6fa6ff5d26301fb02742faf65895242eed08 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=726d6fa6ff5d… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Mon Sep 21 15:26:05 2009 +0200 Fixed a bug in affine_image and implemented three new tests. --- src/BD_Shape.templates.hh | 6 +- tests/Floating_Point_Expression/bdshape1.cc | 91 ++++++++++++++++++++++++++- 2 files changed, 93 insertions(+), 4 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index db11ab5..734f503 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4212,10 +4212,10 @@ void BD_Shape<T> else { // We have to add the constraint `v + w == b', over-approximating it // by computing lower and upper bounds for `w'. - const N& lb_w = dbm[w_id][0]; - if (!is_plus_infinity(lb_w)) { + const N& mlb_w = dbm[w_id][0]; + if (!is_plus_infinity(mlb_w)) { // Add the constraint `v <= ub - lb_w'. - sub_assign_r(dbm[0][var_id], b_ub, lb_w, ROUND_UP); + add_assign_r(dbm[0][var_id], b_ub, mlb_w, ROUND_UP); reset_shortest_path_closed(); } const N& ub_w = dbm[0][w_id]; diff --git a/tests/Floating_Point_Expression/bdshape1.cc b/tests/Floating_Point_Expression/bdshape1.cc index 2c0ab15..a9886b4 100644 --- a/tests/Floating_Point_Expression/bdshape1.cc +++ b/tests/Floating_Point_Expression/bdshape1.cc @@ -61,7 +61,6 @@ test01() { // tests affine_image(A, [-2, 1]) -// FIXME: It's a preliminary version, not sound at the moment. bool test02() { Variable A(0); @@ -168,6 +167,93 @@ bool test05() { return ok; } +// tests affine_image(B, [1, 1]*A + [-3, 1]) +bool test06() { + Variable A(0); + Variable B(1); + + BD_Shape<double> bd1(3); + bd1.add_constraint(A <= 2); + bd1.add_constraint(A - B <= 3); + bd1.add_constraint(B <= 2); + db_r_oc free_term(-3); + free_term.join_assign(1); + Linear_Form<db_r_oc> l(A); + l += free_term; + bd1.affine_image(B, l); + print_constraints(bd1, "*** bd1.affine_image(B, A + [-3, 1]) ***"); + + BD_Shape<double> known_result(3); + known_result.add_constraint(A <= 2); + known_result.add_constraint(B <= 3); + known_result.add_constraint(B - A <= 1); + known_result.add_constraint(A - B <= 3); + print_constraints(known_result, "*** known_result ***"); + + bool ok = (bd1 == known_result); + + return ok; +} + +// tests affine_image(B, [-1, -1]*A + [0, 4]) +bool test07() { + Variable A(0); + Variable B(1); + + BD_Shape<float> bd1(3); + bd1.add_constraint(A <= 2); + bd1.add_constraint(A - B <= 3); + bd1.add_constraint(B <= 2); + fl_r_oc free_term(0); + free_term.join_assign(4); + Linear_Form<fl_r_oc> l(-A); + l += free_term; + bd1.affine_image(B, l); + print_constraints(bd1, "*** bd1.affine_image(B, -A + [0, 4]) ***"); + + BD_Shape<float> known_result(3); + known_result.add_constraint(A <= 2); + known_result.add_constraint(-B <= 2); + known_result.add_constraint(A - B <= 4); + print_constraints(known_result, "*** known_result ***"); + + bool ok = (bd1 == known_result); + + return ok; +} + +// tests affine_image(A, [-1, -1]*B + [0, 2]) +bool test08() { + Variable A(0); + Variable B(1); + + BD_Shape<float> bd1(3); + bd1.add_constraint(A <= 2); + bd1.add_constraint(A - B <= 3); + bd1.add_constraint(B <= 2); + bd1.add_constraint(B >= -10); + fl_r_oc free_term(0); + free_term.join_assign(2); + Linear_Form<fl_r_oc> l(-B); + l += free_term; + bd1.affine_image(A, l); + print_constraints(bd1, "*** bd1.affine_image(A, -B + [0, 2]) ***"); + + BD_Shape<float> known_result(3); + known_result.add_constraint(-A <= 2); + known_result.add_constraint(A <= 12); + known_result.add_constraint(B <= 2); + known_result.add_constraint(B >= -10); + //known_result.add_constraint(-B - A <= 0); + known_result.add_constraint(-A + B <= 4); + known_result.add_constraint(A - B <= 22); + print_constraints(known_result, "*** known_result ***"); + + bool ok = (bd1 == known_result); + + return ok; +} + } // namespace BEGIN_MAIN @@ -176,4 +262,7 @@ BEGIN_MAIN DO_TEST(test03); DO_TEST(test04); DO_TEST(test05); + DO_TEST(test06); + DO_TEST(test07); + DO_TEST(test08); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Added some (and corrected some of the) documentation.
by Fabio Bossi 21 Sep '09

21 Sep '09

Module: ppl/ppl Branch: floating_point Commit: f0f4bf6a9483ec842c9462745db65d3cb4c46e19 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f0f4bf6a9483… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Sep 21 15:00:49 2009 +0200 Added some (and corrected some of the) documentation. --- src/Octagonal_Shape.defs.hh | 18 ++++++++++----- src/Polyhedron.defs.hh | 51 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 63 insertions(+), 6 deletions(-) diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index b5a6055..60f7f58 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -993,17 +993,19 @@ public: the constraint expressed by \p left \f$\leq\f$ \p right. \param left - The linear form on intervals with floating point coefficients that - is on the left of the comparison operator. All of its coefficients + The linear form on intervals with floating point boundaries that + is at the left of the comparison operator. All of its coefficients MUST be bounded. \param right - The linear form on intervals with floating point coefficients that - is on the right of the comparison operator. All of its coefficients + The linear form on intervals with floating point boundaries that + is at the right of the comparison operator. All of its coefficients MUST be bounded. \exception std::invalid_argument Thrown if \p left (or \p right) is dimension-incompatible with \p *this. + + */ template <typename Interval_Info> void refine_with_linear_form_inequality( @@ -1139,12 +1141,16 @@ public: The variable to which the affine expression is assigned. \param lf - The linear form on intervals with floating point coefficients that - defines the affine expression. ALL of its coefficients MUST be boundend. + The linear form on intervals with floating point boundaries that + defines the affine expression(s). ALL of its coefficients MUST be bounded. \exception std::invalid_argument Thrown if \p lf and \p *this are dimension-incompatible or if \p var is not a dimension of \p *this. + + This function is used in abstract interpretation to model an assignment + of a value that is correctly overapproximated by \p lf to the + floating point variable represented by \p var. */ template <typename Interval_Info> void affine_image(const Variable& var, diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index 0ef020c..3c3a9d5 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -979,6 +979,32 @@ public: */ void refine_with_congruences(const Congruence_System& cgs); + /*! + Refines \p *this with the constraint expressed by \p left \f$\leq\f$ + \p right. + + \param left + The linear form on intervals with floating point boundaries that + is on the left of the comparison operator. All of its coefficients + MUST be bounded. + + \param right + The linear form on intervals with floating point boundaries that + is on the right of the comparison operator. All of its coefficients + MUST be bounded. + + \param store + The interval abstract store in which the test defining the filter is + performed. All variables that occur in \p left or \p right MUST have + an associated value in it. + + \exception std::invalid_argument + Thrown if \p left (or \p right) is dimension-incompatible with \p *this. + + This function is used in abstract interpretation to model a filter + that is generated by a comparison of two expressions that are correctly + approximated by \p left and \p right respectively. + */ template <typename FP_Format, typename Interval_Info> void refine_with_linear_form_inequality( const Linear_Form< Interval<FP_Format, Interval_Info> >& left, @@ -1151,6 +1177,31 @@ public: Coefficient_traits::const_reference denominator = Coefficient_one()); + /*! + Assigns to \p *this the + \ref Single_Update_Affine_Functions "affine image" + of \p *this under the function mapping variable \p var into the + affine expression(s) specified by \p lf. + + \param var + The variable to which the affine expression is assigned. + + \param lf + The linear form on intervals with floating point boundaries that + defines the affine expression(s). ALL of its coefficients MUST be bounded. + + \param store + The interval abstract store in which the variable assignment is performed. + All variables that occur in \p lf MUST have an associated value in it. + + \exception std::invalid_argument + Thrown if \p lf and \p *this are dimension-incompatible or if \p var is + not a space dimension of \p *this. + + This function is used in abstract interpretation to model an assignment + of a value that is correctly overapproximated by \p lf to the + floating point variable represented by \p var. + */ template <typename FP_Format, typename Interval_Info> void affine_image(const Variable& var, const Linear_Form<Interval <FP_Format, Interval_Info> >& lf,

1 0

[GIT] ppl/ppl(floating_point): Wrote a first implementation of refine_with_linear_form_inequality.
by Fabio Bossi 21 Sep '09

21 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 4f125f4d90aa912d18bcaf8c110a7ff05616ecd2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4f125f4d90aa… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Sep 21 14:19:43 2009 +0200 Wrote a first implementation of refine_with_linear_form_inequality. --- src/Polyhedron.defs.hh | 6 ++++ src/Polyhedron.templates.hh | 54 ++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 57 insertions(+), 3 deletions(-) diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index d904386..0ef020c 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -979,6 +979,12 @@ public: */ void refine_with_congruences(const Congruence_System& cgs); + template <typename FP_Format, typename Interval_Info> + void refine_with_linear_form_inequality( + const Linear_Form< Interval<FP_Format, Interval_Info> >& left, + const Linear_Form< Interval<FP_Format, Interval_Info> >& right, + const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store); + /*! \brief Computes the \ref Cylindrification "cylindrification" of \p *this with respect to space dimension \p var, assigning the result to \p *this. diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index 9f4f333..a8e2a07 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -298,6 +298,53 @@ Polyhedron::map_space_dimensions(const Partial_Function& pfunc) { template <typename FP_Format, typename Interval_Info> void +Polyhedron::refine_with_linear_form_inequality( + const Linear_Form< Interval<FP_Format, Interval_Info> >& left, + const Linear_Form< Interval<FP_Format, Interval_Info> >& right, + const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) { + + // Check that FP_Format is indeed a floating point type. + PPL_COMPILE_TIME_CHECK(!std::numeric_limits<FP_Format>::is_exact, + "Polyhedron::affine_image:" + " FP_Format not a floating point type."); + + // Dimension compatibility checks. + // The dimensions of left and right should not be greater than the + // dimension of *this. + const dimension_type left_space_dim = left.space_dimension(); + if (space_dim < left_space_dim) + throw_dimension_incompatible( + "refine_with_linear_form_inequality(l1, l2, s)", "l1", left); + + const dimension_type right_space_dim = right.space_dimension(); + if (space_dim < right_space_dim) + throw_dimension_incompatible( + "refine_with_linear_form_inequality(l1, l2, s)", "l2", right); + + // We assume that the analyzer will not refine an unreachable test. + PPL_ASSERT(!marked_empty()); + + typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; + typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; + + // Overapproximate left - right. + FP_Linear_Form left_minus_right(left); + left_minus_right -= right; + dimension_type lf_space_dim = left_minus_right.space_dimension(); + FP_Linear_Form lf_approx; + overapproximate_linear_form(left_minus_right, lf_space_dim, store, lf_approx); + + // Normalize left - right. + Linear_Expression lf_approx_le; + convert_to_integer_expression(lf_approx, lf_space_dim, lf_approx_le); + + // Finally, do the refinement. + refine_with_constraint(lf_approx_le <= 0); + +} + +template <typename FP_Format, typename Interval_Info> +void Polyhedron::affine_image(const Variable& var, const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) { @@ -318,7 +365,7 @@ const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) { if (space_dim < var_id + 1) throw_dimension_incompatible("affine_image(v, l, s)", "v", var); - // We suppose that the analyzer will not filter an unreachable test. + // We assume that the analyzer will not perform an unreachable assignment. PPL_ASSERT(!marked_empty()); typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; @@ -363,6 +410,7 @@ Polyhedron::overapproximate_linear_form( typedef std::map<dimension_type, FP_Interval_Type> Interval_Abstract_Store; result = FP_Linear_Form(lf.inhomogeneous_term()); + // FIXME: this may not be policy-neutral. const FP_Interval_Type aux_divisor1(static_cast<FP_Format>(0.5)); FP_Interval_Type aux_divisor2(aux_divisor1); aux_divisor2.lower() = static_cast<FP_Format>(-0.5); @@ -398,7 +446,7 @@ Polyhedron::convert_to_integer_expression( result = Linear_Expression(); typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; - typedef typename FP_Interval_Type::coefficient_type FP_Coeff_Type; + typedef typename FP_Interval_Type::boundary_type FP_Coeff_Type; std::vector<Coefficient> numerators(lf_dimension+1); std::vector<Coefficient> denominators(lf_dimension+1); @@ -408,7 +456,7 @@ Polyhedron::convert_to_integer_expression( lcm = 1; const FP_Interval_Type& b = lf.inhomogeneous_term(); // FIXME: are these checks numerator[i] != 0 really necessary? - numer_denom(b.upper(), numerators[lf_dimension], + numer_denom(b.lower(), numerators[lf_dimension], denominators[lf_dimension]); if (numerators[lf_dimension] != 0) lcm_assign(lcm, lcm, denominators[lf_dimension]);

1 0

[GIT] ppl/ppl(floating_point): Fixed a bug in BD_Shape<T>:: affine_image and added more tests for
by Roberto Amadini 21 Sep '09

21 Sep '09

Module: ppl/ppl Branch: floating_point Commit: c07b5cfd78cea7c03c90c48697025d595e9cdb2f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c07b5cfd78ce… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Mon Sep 21 13:16:17 2009 +0200 Fixed a bug in BD_Shape<T>::affine_image and added more tests for this method. --- src/BD_Shape.templates.hh | 19 +++--- tests/Floating_Point_Expression/bdshape1.cc | 89 +++++++++++++++++++++++++-- 2 files changed, 93 insertions(+), 15 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index 6d44f5e..db11ab5 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4108,16 +4108,11 @@ BD_Shape<T>::affine_image(const Variable& var, return; } - // General case. - // Either t == 2, so that - // lf == i_1*x_1 + i_2*x_2 + ... + i_n*x_n + b, where n >= 2, - // or t == 1, lf == i*w + b, but i <> [+/-1;+/-1]. - //two_variables_affine_image(var, var_id, lf); PPL_ASSERT(OK()); } -// Case 1: var = [-b, b]. +// Case 1: var = b, where b = [-b_mlb, b_ub] template <typename T> template <typename Interval_Info> void @@ -4139,7 +4134,7 @@ BD_Shape<T>::inhomogeneous_affine_image(const dimension_type& var_id, return; } -// case 2: var = (+/-1) * w + [lb, -mlb], where `w' can be `var' +// case 2: var = (+/-1) * w + [-b_mlb, b_ub], where `w' can be `var' // or another variable. template <typename T> template <typename Interval_Info> @@ -4155,7 +4150,7 @@ void BD_Shape<T> PPL_DIRTY_TEMP(N, b_mlb); neg_assign_r(b_mlb, b.lower(), ROUND_NOT_NEEDED); - // true if b = [b_lb, b_ub] = [-mlb, ub] = [0;0]. + // true if b = [b_lb, b_ub] = [0;0]. bool is_b_zero = (b_mlb == 0 && b_ub == 0); // true if w_coeff = [1;1] bool is_w_coeff_one = (w_coeff == 1); @@ -4193,9 +4188,9 @@ void BD_Shape<T> // Translate the unary constraints on `var' by adding the value // `b_ub' or subtracting the value `b_lb'. N& dbm_v0 = dbm[var_id][0]; - add_assign_r(dbm_v0, dbm_v0, b_ub, ROUND_UP); + add_assign_r(dbm_v0, dbm_v0, b_mlb, ROUND_UP); N& dbm_0v = dbm[0][var_id]; - add_assign_r(dbm_v0, dbm_0v, b_mlb, ROUND_UP); + add_assign_r(dbm_0v, dbm_0v, b_ub, ROUND_UP); } } } @@ -4235,6 +4230,10 @@ void BD_Shape<T> return; } +// General case. +// Either t == 2, so that +// lf == i_1*x_1 + i_2*x_2 + ... + i_n*x_n + b, where n >= 2, +// or t == 1, lf == i*w + b, but i <> [+/-1;+/-1]. template <typename T> template <typename Interval_Info> void BD_Shape<T> diff --git a/tests/Floating_Point_Expression/bdshape1.cc b/tests/Floating_Point_Expression/bdshape1.cc index cd17822..2c0ab15 100644 --- a/tests/Floating_Point_Expression/bdshape1.cc +++ b/tests/Floating_Point_Expression/bdshape1.cc @@ -77,14 +77,90 @@ test02() { bd1.affine_image(A, l); print_constraints(bd1, "*** bd1.affine_image(A, [-2, 1]) ***"); - bd1.ascii_dump(); - // At the moment, affine_image is simply an identity function. - BD_Shape<float> known_result(2); known_result.add_constraint(A <= 1); - known_result.add_constraint(- A <= 2); + known_result.add_constraint(-A <= 2); + known_result.add_constraint(B <= 2); + print_constraints(bd1, "*** known_result ***"); + + bool ok = (bd1 == known_result); + + return ok; +} + +// tests affine_image(A, [-1, -1]*A + [0.5, 2]) +bool test03() { + Variable A(0); + Variable B(1); + + BD_Shape<double> bd1(3); + bd1.add_constraint(A <= 2); + bd1.add_constraint(A - B <= 3); + bd1.add_constraint(B <= 2); + db_r_oc free_term(0.5); + free_term.join_assign(2); + Linear_Form<db_r_oc> l(-A); + l += free_term; + bd1.affine_image(A, l); + print_constraints(bd1, "*** bd1.affine_image(A, -A + [0.5, 2]) ***"); + + BD_Shape<double> known_result(3); + known_result.add_constraint(-2*A <= 3); + known_result.add_constraint(B <= 2); + print_constraints(known_result, "*** known_result ***"); + bool ok = (bd1 == known_result); + + return ok; +} + +// tests affine_image(B, [1, 1]*B + [-1.5, 3.5]) +bool test04() { + Variable A(0); + Variable B(1); + + BD_Shape<float> bd1(3); + bd1.add_constraint(A <= 2); + bd1.add_constraint(A - B <= 3); + bd1.add_constraint(B <= 2); + fl_r_oc free_term(-1.5); + free_term.join_assign(3.5); + Linear_Form<fl_r_oc> l(B); + l += free_term; + bd1.affine_image(B, l); + print_constraints(bd1, "*** bd1.affine_image(B, B + [-1.5, 3.5]) ***"); + + BD_Shape<float> known_result(3); + known_result.add_constraint(A <= 2); + known_result.add_constraint(2*B <= 11); + known_result.add_constraint(-2*B + 2*A <= 9); + print_constraints(known_result, "*** known_result ***"); + + bool ok = (bd1 == known_result); + + return ok; +} + +// tests affine_image(A, [1, 1]*B + [-1, 0.5]) +bool test05() { + Variable A(0); + Variable B(1); + + BD_Shape<double> bd1(3); + bd1.add_constraint(A <= 2); + bd1.add_constraint(A - B <= 3); + bd1.add_constraint(B <= 2); + db_r_oc free_term(-1); + free_term.join_assign(0.5); + Linear_Form<db_r_oc> l(B); + l += free_term; + bd1.affine_image(A, l); + print_constraints(bd1, "*** bd1.affine_image(A, B + [-1, 0.5]) ***"); + + BD_Shape<double> known_result(3); + known_result.add_constraint(2*A <= 5); known_result.add_constraint(B <= 2); - + known_result.add_constraint(B - A <= 1); + known_result.add_constraint(2*A - 2*B <= 1); print_constraints(known_result, "*** known_result ***"); bool ok = (bd1 == known_result); @@ -97,4 +173,7 @@ test02() { BEGIN_MAIN DO_TEST(test01); DO_TEST(test02); + DO_TEST(test03); + DO_TEST(test04); + DO_TEST(test05); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Use the proper exception thrower.
by Fabio Bossi 21 Sep '09

21 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 18e281994a302d502b23daa72e206b3c6772895a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=18e281994a30… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Sep 21 11:37:51 2009 +0200 Use the proper exception thrower. Moved the new exception thrower. --- src/Polyhedron.templates.hh | 10 +++++++++- src/Polyhedron_nonpublic.cc | 8 -------- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index 469672a..9f4f333 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -316,7 +316,7 @@ const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) { // `var' should be one of the dimensions of the polyhedron. const dimension_type var_id = var.id(); if (space_dim < var_id + 1) - throw_dimension_incompatible("affine_image(v, l, s)", var.id()+1); + throw_dimension_incompatible("affine_image(v, l, s)", "v", var); // We suppose that the analyzer will not filter an unreachable test. PPL_ASSERT(!marked_empty()); @@ -498,6 +498,14 @@ Polyhedron::convert_to_integer_expressions( res_hi_coeff = Coefficient(0); } +template <typename C> +void +Polyhedron::throw_dimension_incompatible(const char* method, + const char* lf_name, + const Linear_Form<C>& lf) const { + throw_dimension_incompatible(method, lf_name, lf.space_dimension()); +} + } // namespace Parma_Polyhedra_Library #endif // !defined(PPL_Polyhedron_templates_hh) diff --git a/src/Polyhedron_nonpublic.cc b/src/Polyhedron_nonpublic.cc index 63ceb2a..29d5f7a 100644 --- a/src/Polyhedron_nonpublic.cc +++ b/src/Polyhedron_nonpublic.cc @@ -2232,14 +2232,6 @@ PPL::Polyhedron::throw_dimension_incompatible(const char* method, throw_dimension_incompatible(method, cgs_name, cgs.space_dimension()); } -template <typename C> -void -PPL::Polyhedron::throw_dimension_incompatible(const char* method, - const char* lf_name, - const Linear_Form<C>& lf) const { - throw_dimension_incompatible(method, lf_name, lf.space_dimension()); -} - void PPL::Polyhedron::throw_dimension_incompatible(const char* method, const char* var_name,

1 0

[GIT] ppl/ppl(floating_point): Various corrections.
by Fabio Bossi 21 Sep '09

21 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 4bdd87fc436454719f7d982942fe6615dc00b2e9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4bdd87fc4364… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Sep 21 11:08:33 2009 +0200 Various corrections. --- src/Polyhedron.templates.hh | 28 +++++++++++++++++----------- src/Polyhedron_nonpublic.cc | 2 +- 2 files changed, 18 insertions(+), 12 deletions(-) diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index 8ac2f9d..469672a 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -332,14 +332,16 @@ const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) { Linear_Expression lf_approx_le; PPL_DIRTY_TEMP_COEFFICIENT(lo_coeff); PPL_DIRTY_TEMP_COEFFICIENT(hi_coeff); - convert_to_integer_expressions(lf_approx, lf_space_dim, lo_coeff, hi_coeff); + convert_to_integer_expressions(lf_approx, lf_space_dim, lf_approx_le, + lo_coeff, hi_coeff); // Finally, do the assignment. PPL_DIRTY_TEMP_COEFFICIENT(one_coeff); one_coeff = 1; - generalized_affine_image(var, GREATER_OR_EQUAL, lf_approx + lo_coeff, + generalized_affine_image(var, GREATER_OR_EQUAL, lf_approx_le + lo_coeff, + one_coeff); + generalized_affine_image(var, LESS_OR_EQUAL, lf_approx_le + hi_coeff, one_coeff); - generalized_affine_image(var, LESS_OR_EQUAL, lf_approx + hi_coeff, one_coeff); } @@ -371,23 +373,26 @@ Polyhedron::overapproximate_linear_form( FP_Format curr_lb = curr_coeff.lower(); FP_Format curr_ub = curr_coeff.upper(); if (curr_lb != 0 || curr_ub != 0) { - PPL_ASSERT(store.find(i) != store.end()); + typename Interval_Abstract_Store::const_iterator i_ite = store.find(i); + PPL_ASSERT(i_ite != store.end()); FP_Interval_Type curr_addend(curr_ub - curr_lb); curr_addend *= aux_divisor2; - curr_addend *= store[i]; + curr_addend *= i_ite->second; result += curr_addend; curr_addend = FP_Interval_Type(curr_lb + curr_ub); curr_addend *= aux_divisor1; - curr_addend *= curr_var; - result += curr_addend; + FP_Linear_Form curr_addend_lf(curr_var); + curr_addend_lf *= curr_addend; + result += curr_addend_lf; } } } template <typename FP_Format, typename Interval_Info> -void convert_to_integer_expression( - const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, +void +Polyhedron::convert_to_integer_expression( + const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, const dimension_type lf_dimension, Linear_Expression& result) { result = Linear_Expression(); @@ -432,14 +437,15 @@ void convert_to_integer_expression( } template <typename FP_Format, typename Interval_Info> -void convert_to_integer_expressions( +void +Polyhedron::convert_to_integer_expressions( const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, const dimension_type lf_dimension, Linear_Expression& res, Coefficient& res_low_coeff, Coefficient& res_hi_coeff) { res = Linear_Expression(); typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; - typedef typename FP_Interval_Type::coefficient_type FP_Coeff_Type; + typedef typename FP_Interval_Type::boundary_type FP_Coeff_Type; std::vector<Coefficient> numerators(lf_dimension+2); std::vector<Coefficient> denominators(lf_dimension+2); diff --git a/src/Polyhedron_nonpublic.cc b/src/Polyhedron_nonpublic.cc index 9dce752..63ceb2a 100644 --- a/src/Polyhedron_nonpublic.cc +++ b/src/Polyhedron_nonpublic.cc @@ -25,7 +25,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Polyhedron.defs.hh" #include "Scalar_Products.defs.hh" -#include "Linear_Form.types.hh" +#include "Linear_Form.defs.hh" #include "assert.hh" #include <string> #include <iostream>

1 0

[GIT] ppl/ppl(floating_point): Finished writing a first version of our affine_image variant.
by Fabio Bossi 21 Sep '09

21 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 04edf0b5d66a1dfe43f19050098b4d30969d1b46 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=04edf0b5d66a… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Sep 21 10:11:18 2009 +0200 Finished writing a first version of our affine_image variant. --- src/Polyhedron.templates.hh | 18 ++++++++++++++---- 1 files changed, 14 insertions(+), 4 deletions(-) diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index ab61ee1..8ac2f9d 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -318,18 +318,28 @@ const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) { if (space_dim < var_id + 1) throw_dimension_incompatible("affine_image(v, l, s)", var.id()+1); + // We suppose that the analyzer will not filter an unreachable test. PPL_ASSERT(!marked_empty()); - minimize(); - unconstrain(var); - typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; + // Overapproximate lf. FP_Linear_Form lf_approx; overapproximate_linear_form(lf, lf_space_dim, store, lf_approx); - + // Normalize lf. + Linear_Expression lf_approx_le; + PPL_DIRTY_TEMP_COEFFICIENT(lo_coeff); + PPL_DIRTY_TEMP_COEFFICIENT(hi_coeff); + convert_to_integer_expressions(lf_approx, lf_space_dim, lo_coeff, hi_coeff); + + // Finally, do the assignment. + PPL_DIRTY_TEMP_COEFFICIENT(one_coeff); + one_coeff = 1; + generalized_affine_image(var, GREATER_OR_EQUAL, lf_approx + lo_coeff, + one_coeff); + generalized_affine_image(var, LESS_OR_EQUAL, lf_approx + hi_coeff, one_coeff); }

1 0