September 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): Removed unnecessary temporaries from affine_image.
by Fabio Bossi 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 453985a4ec00db64b013edc7965bd193809da9fe URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=453985a4ec00… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Sep 17 11:32:08 2009 +0200 Removed unnecessary temporaries from affine_image. --- src/Octagonal_Shape.templates.hh | 11 ++++------- 1 files changed, 4 insertions(+), 7 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 67148c2..3eac070 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -5103,26 +5103,23 @@ Octagonal_Shape<T>::affine_image(Variable var, PPL_DIRTY_TEMP(N, b_ub); assign_r(b_ub, b.upper(), ROUND_NOT_NEEDED); - PPL_DIRTY_TEMP(N, b_lb); - assign_r(b_lb, b.lower(), ROUND_NOT_NEEDED); PPL_DIRTY_TEMP(N, b_mlb); - neg_assign_r(b_mlb, b_lb, ROUND_NOT_NEEDED); + neg_assign_r(b_mlb, b.lower(), ROUND_NOT_NEEDED); if (t == 0) { // Case 1: lf = [lb;ub]; forget_all_octagonal_constraints(var_id); mul_2exp_assign_r(b_mlb, b_mlb, 1, ROUND_UP); - PPL_DIRTY_TEMP(N, two_ub); - mul_2exp_assign_r(two_ub, b_ub, 1, ROUND_UP); + mul_2exp_assign_r(b_ub, b_ub, 1, ROUND_UP); // Add the constraint `var >= lb && var <= ub'. - add_octagonal_constraint(n_var+1, n_var, two_ub); + add_octagonal_constraint(n_var+1, n_var, b_ub); add_octagonal_constraint(n_var, n_var+1, b_mlb); PPL_ASSERT(OK()); return; } // true if b = [0;0]. - bool is_b_zero = (b_lb == 0 && b_ub == 0); + bool is_b_zero = (b_mlb == 0 && b_ub == 0); if (t == 1) { // The one and only non-zero homogeneous coefficient in `lf'.

1 0

[GIT] ppl/ppl(floating_point): Optimized linear_form_upper_bound: got rid of two unnecessary
by Fabio Bossi 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 4fa3f4c26c6d3c7adada8cd08d659f67a6e5ef94 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4fa3f4c26c6d… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Sep 17 11:17:11 2009 +0200 Optimized linear_form_upper_bound: got rid of two unnecessary temporaries. --- src/Octagonal_Shape.templates.hh | 20 +++++++++----------- 1 files changed, 9 insertions(+), 11 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 99c9d5b..67148c2 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -5323,8 +5323,6 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, PPL_DIRTY_TEMP(N, first_comparison_term); PPL_DIRTY_TEMP(N, second_comparison_term); - PPL_DIRTY_TEMP(N, third_comparison_term); - PPL_DIRTY_TEMP(N, fourth_comparison_term); PPL_DIRTY_TEMP(N, negator); @@ -5354,24 +5352,24 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, // Next addend will be the maximum of four quantities. assign_r(first_comparison_term, 0, ROUND_NOT_NEEDED); assign_r(second_comparison_term, 0, ROUND_NOT_NEEDED); - assign_r(third_comparison_term, 0, ROUND_NOT_NEEDED); - assign_r(fourth_comparison_term, 0, ROUND_NOT_NEEDED); add_mul_assign_r(first_comparison_term, curr_var_ub, curr_ub, ROUND_UP); - add_mul_assign_r(third_comparison_term, curr_var_ub, curr_lb, - ROUND_UP); - add_mul_assign_r(second_comparison_term, curr_minus_var_ub, curr_ub, - ROUND_UP); - add_mul_assign_r(fourth_comparison_term, curr_minus_var_ub, curr_lb, + add_mul_assign_r(second_comparison_term, curr_var_ub, curr_lb, ROUND_UP); assign_r(first_comparison_term, std::max(first_comparison_term, second_comparison_term), ROUND_NOT_NEEDED); + assign_r(second_comparison_term, 0, ROUND_NOT_NEEDED); + add_mul_assign_r(second_comparison_term, curr_minus_var_ub, curr_ub, + ROUND_UP); assign_r(first_comparison_term, std::max(first_comparison_term, - third_comparison_term), + second_comparison_term), ROUND_NOT_NEEDED); + assign_r(second_comparison_term, 0, ROUND_NOT_NEEDED); + add_mul_assign_r(second_comparison_term, curr_minus_var_ub, curr_lb, + ROUND_UP); assign_r(first_comparison_term, std::max(first_comparison_term, - fourth_comparison_term), + second_comparison_term), ROUND_NOT_NEEDED); add_assign_r(result, result, first_comparison_term, ROUND_UP);

1 0

[GIT] ppl/ppl(floating_point): Definitively removed counterproductive checks in
by Fabio Bossi 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 5d2ee886c0013061fb43b16e45de1c042ff29361 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5d2ee886c001… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Sep 17 10:57:25 2009 +0200 Definitively removed counterproductive checks in linear_form_upper_bound, since we have confirmed that comparing with -infinity is legitimate. --- src/Octagonal_Shape.templates.hh | 30 ++++++++---------------------- 1 files changed, 8 insertions(+), 22 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 0c6efd2..99c9d5b 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -5356,28 +5356,14 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, assign_r(second_comparison_term, 0, ROUND_NOT_NEEDED); assign_r(third_comparison_term, 0, ROUND_NOT_NEEDED); assign_r(fourth_comparison_term, 0, ROUND_NOT_NEEDED); - /*if (is_plus_infinity(curr_var_ub)) { - assign_r(first_comparison_term, PLUS_INFINITY, ROUND_NOT_NEEDED); - assign_r(third_comparison_term, PLUS_INFINITY, ROUND_NOT_NEEDED); - } - else {*/ - add_mul_assign_r(first_comparison_term, curr_var_ub, curr_ub, - ROUND_UP); - add_mul_assign_r(third_comparison_term, curr_var_ub, curr_lb, - ROUND_UP); - /*} - - if (is_minus_infinity(curr_minus_var_ub)) { - assign_r(second_comparison_term, PLUS_INFINITY, ROUND_NOT_NEEDED); - assign_r(fourth_comparison_term, PLUS_INFINITY, ROUND_NOT_NEEDED); - } - else { */ - add_mul_assign_r(second_comparison_term, curr_minus_var_ub, curr_ub, - ROUND_UP); - add_mul_assign_r(fourth_comparison_term, curr_minus_var_ub, curr_lb, - ROUND_UP); - //} - + add_mul_assign_r(first_comparison_term, curr_var_ub, curr_ub, + ROUND_UP); + add_mul_assign_r(third_comparison_term, curr_var_ub, curr_lb, + ROUND_UP); + add_mul_assign_r(second_comparison_term, curr_minus_var_ub, curr_ub, + ROUND_UP); + add_mul_assign_r(fourth_comparison_term, curr_minus_var_ub, curr_lb, + ROUND_UP); assign_r(first_comparison_term, std::max(first_comparison_term, second_comparison_term), ROUND_NOT_NEEDED);

1 0

[GIT] ppl/ppl(floating_point): Use ROUND_DOWN instead of ROUND_UP to compute the negation of the upper
by Fabio Bossi 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: b9f5aee8d9e95cda8126480538154b2b929bb163 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b9f5aee8d9e9… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Sep 17 10:52:37 2009 +0200 Use ROUND_DOWN instead of ROUND_UP to compute the negation of the upper bound of -var. --- src/Octagonal_Shape.templates.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 1d93abf..0c6efd2 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -5339,7 +5339,7 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, assign_r(curr_var_ub, matrix[n_var+1][n_var], ROUND_NOT_NEEDED); div_2exp_assign_r(curr_var_ub, curr_var_ub, 1, ROUND_UP); neg_assign_r(curr_minus_var_ub, matrix[n_var][n_var+1], ROUND_NOT_NEEDED); - div_2exp_assign_r(curr_minus_var_ub, curr_minus_var_ub, 1, ROUND_UP); + div_2exp_assign_r(curr_minus_var_ub, curr_minus_var_ub, 1, ROUND_DOWN); // Optimize the most common case: curr = +/-[1;1] if (curr_lb == 1 && curr_ub == 1) { add_assign_r(result, result, std::max(curr_var_ub, curr_minus_var_ub),

1 0

[GIT] ppl/ppl(floating_point): Use ROUND_UP (or, in one case where intervals are involved, ROUND_DOWN)
by Fabio Bossi 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 41e8ca0bea15517ef175ca7b0b2fd44300497442 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=41e8ca0bea15… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Sep 17 10:30:57 2009 +0200 Use ROUND_UP (or, in one case where intervals are involved, ROUND_DOWN) whenever appropriate. --- src/Octagonal_Shape.templates.hh | 39 ++++++++++++++++++------------------- 1 files changed, 19 insertions(+), 20 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 0cd06f5..1d93abf 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -32,6 +32,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "meta_programming.hh" #include "assert.hh" #include <vector> +#include <map> #include <deque> #include <string> #include <iostream> @@ -563,7 +564,7 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( sub_assign_r(b_plus_minus_a_minus, right_b.upper(), left_a.lower(), ROUND_UP); mul_2exp_assign_r(b_plus_minus_a_minus, b_plus_minus_a_minus, 1, - ROUND_IGNORE); + ROUND_UP); add_octagonal_constraint(n_right, n_right+1, b_plus_minus_a_minus); return; } @@ -576,7 +577,7 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( sub_assign_r(b_plus_minus_a_minus, right_b.upper(), left_a.lower(), ROUND_UP); mul_2exp_assign_r(b_plus_minus_a_minus, b_plus_minus_a_minus, 1, - ROUND_IGNORE); + ROUND_UP); add_octagonal_constraint(n_right+1, n_right, b_plus_minus_a_minus); return; } @@ -596,7 +597,7 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(), ROUND_UP); mul_2exp_assign_r(a_plus_minus_b_minus, a_plus_minus_b_minus, 1, - ROUND_IGNORE); + ROUND_UP); add_octagonal_constraint(n_left+1, n_left, a_plus_minus_b_minus); return; } @@ -609,7 +610,7 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(), ROUND_UP); mul_2exp_assign_r(a_plus_minus_b_minus, a_plus_minus_b_minus, 1, - ROUND_IGNORE); + ROUND_UP); add_octagonal_constraint(n_left, n_left+1, a_plus_minus_b_minus); return; } @@ -668,7 +669,7 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(), ROUND_UP); mul_2exp_assign_r(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, - ROUND_IGNORE); + ROUND_UP); if (left_w_id < right_w_id) add_octagonal_constraint(n_right, n_left, c_plus_minus_a_minus); else @@ -684,7 +685,7 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(), ROUND_UP); mul_2exp_assign_r(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, - ROUND_IGNORE); + ROUND_UP); if (left_w_id < right_w_id) add_octagonal_constraint(n_right+1, n_left, c_plus_minus_a_minus); else @@ -700,7 +701,7 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(), ROUND_UP); mul_2exp_assign_r(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, - ROUND_IGNORE); + ROUND_UP); if (left_w_id < right_w_id) add_octagonal_constraint(n_right, n_left+1, c_plus_minus_a_minus); else @@ -716,7 +717,7 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(), ROUND_UP); mul_2exp_assign_r(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, - ROUND_IGNORE); + ROUND_UP); if (left_w_id < right_w_id) add_octagonal_constraint(n_right+1, n_left+1, c_plus_minus_a_minus); else @@ -5163,10 +5164,10 @@ Octagonal_Shape<T>::affine_image(Variable var, add_assign_r(m_i_cv, m_i_cv, b_mlb, ROUND_UP); } // Now update unary constraints on var. - mul_2exp_assign_r(b_ub, b_ub, 1, ROUND_IGNORE); + mul_2exp_assign_r(b_ub, b_ub, 1, ROUND_UP); N& m_cv_v = m_cv[n_var]; add_assign_r(m_cv_v, m_cv_v, b_ub, ROUND_UP); - mul_2exp_assign_r(b_mlb, b_mlb, 1, ROUND_IGNORE); + mul_2exp_assign_r(b_mlb, b_mlb, 1, ROUND_UP); N& m_v_cv = m_v[n_var+1]; add_assign_r(m_v_cv, m_v_cv, b_mlb, ROUND_UP); reset_strongly_closed(); @@ -5188,8 +5189,8 @@ Octagonal_Shape<T>::affine_image(Variable var, if (b != 0) { // Translate the unary constraints on `var' by adding the value // `b_ub' or subtracting the value `b_lb'. - mul_2exp_assign_r(b_ub, b_ub, 1, ROUND_IGNORE); - mul_2exp_assign_r(b_mlb, b_mlb, 1, ROUND_IGNORE); + mul_2exp_assign_r(b_ub, b_ub, 1, ROUND_UP); + mul_2exp_assign_r(b_mlb, b_mlb, 1, ROUND_UP); add_assign_r(m_cv_v, m_cv_v, b_ub, ROUND_UP); add_assign_r(m_v_cv, m_v_cv, b_mlb, ROUND_UP); } @@ -5288,9 +5289,9 @@ Octagonal_Shape<T>::affine_image(Variable var, linear_form_upper_bound(lf, lf_ub); PPL_DIRTY_TEMP(N, minus_lf_ub); linear_form_upper_bound(minus_lf, minus_lf_ub); - mul_2exp_assign_r(lf_ub, lf_ub, 1, ROUND_IGNORE); + mul_2exp_assign_r(lf_ub, lf_ub, 1, ROUND_UP); assign_r(matrix[n_var+1][n_var], lf_ub, ROUND_NOT_NEEDED); - mul_2exp_assign_r(minus_lf_ub, minus_lf_ub, 1, ROUND_IGNORE); + mul_2exp_assign_r(minus_lf_ub, minus_lf_ub, 1, ROUND_UP); assign_r(matrix[n_var][n_var+1], minus_lf_ub, ROUND_NOT_NEEDED); PPL_ASSERT(OK()); @@ -5335,11 +5336,10 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, assign_r(curr_lb, curr_coefficient->lower(), ROUND_NOT_NEEDED); assign_r(curr_ub, curr_coefficient->upper(), ROUND_NOT_NEEDED); if (curr_lb != 0 || curr_ub != 0) { - // FIXME: ensure that ROUND_IGNORE works fine with divisions by 2. assign_r(curr_var_ub, matrix[n_var+1][n_var], ROUND_NOT_NEEDED); - div_2exp_assign_r(curr_var_ub, curr_var_ub, 1, ROUND_IGNORE); + div_2exp_assign_r(curr_var_ub, curr_var_ub, 1, ROUND_UP); neg_assign_r(curr_minus_var_ub, matrix[n_var][n_var+1], ROUND_NOT_NEEDED); - div_2exp_assign_r(curr_minus_var_ub, curr_minus_var_ub, 1, ROUND_IGNORE); + div_2exp_assign_r(curr_minus_var_ub, curr_minus_var_ub, 1, ROUND_UP); // Optimize the most common case: curr = +/-[1;1] if (curr_lb == 1 && curr_ub == 1) { add_assign_r(result, result, std::max(curr_var_ub, curr_minus_var_ub), @@ -5456,10 +5456,9 @@ refine_fp_interval_abstract_store( FP_Interval_Type& curr_int = ite->second; T& lb = curr_int.lower(); T& ub = curr_int.upper(); - // FIXME: are we sure that ROUND_IGNORE is good? // Now get the upper bound for curr_var in the octagon. assign_r(upper_bound, matrix[n_curr_var+1][n_curr_var], ROUND_NOT_NEEDED); - div_2exp_assign_r(upper_bound, upper_bound, 1, ROUND_IGNORE); + div_2exp_assign_r(upper_bound, upper_bound, 1, ROUND_UP); if (upper_bound < ub) ub = upper_bound.raw_value(); @@ -5467,7 +5466,7 @@ refine_fp_interval_abstract_store( // Now get the lower bound for curr_var in the octagon. neg_assign_r(upper_bound, matrix[n_curr_var][n_curr_var+1], ROUND_NOT_NEEDED); - div_2exp_assign_r(upper_bound, upper_bound, 1, ROUND_IGNORE); + div_2exp_assign_r(upper_bound, upper_bound, 1, ROUND_DOWN); if (upper_bound > lb) lb = upper_bound.raw_value();

1 0

[GIT] ppl/ppl(floating_point): Added another test. Coverage of 100% reached for affine_image and
by Roberto Amadini 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: fae817ce8120f46f89a3f254c00cd80725db09e1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fae817ce8120… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Wed Sep 16 20:13:44 2009 +0200 Added another test. Coverage of 100% reached for affine_image and linear_form_upper_bound methods. Temporarily(?) removed some checks in linear_form_upper_bound. --- src/Octagonal_Shape.templates.hh | 12 +++--- tests/Floating_Point_Expression/affineimage3.cc | 39 ++++++++++++++++++---- 2 files changed, 38 insertions(+), 13 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index da27f9d..0cd06f5 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -5356,27 +5356,27 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, assign_r(second_comparison_term, 0, ROUND_NOT_NEEDED); assign_r(third_comparison_term, 0, ROUND_NOT_NEEDED); assign_r(fourth_comparison_term, 0, ROUND_NOT_NEEDED); - if (is_plus_infinity(curr_var_ub)) { + /*if (is_plus_infinity(curr_var_ub)) { assign_r(first_comparison_term, PLUS_INFINITY, ROUND_NOT_NEEDED); assign_r(third_comparison_term, PLUS_INFINITY, ROUND_NOT_NEEDED); } - else { + else {*/ add_mul_assign_r(first_comparison_term, curr_var_ub, curr_ub, ROUND_UP); add_mul_assign_r(third_comparison_term, curr_var_ub, curr_lb, ROUND_UP); - } + /*} if (is_minus_infinity(curr_minus_var_ub)) { assign_r(second_comparison_term, PLUS_INFINITY, ROUND_NOT_NEEDED); assign_r(fourth_comparison_term, PLUS_INFINITY, ROUND_NOT_NEEDED); } - else { + else { */ add_mul_assign_r(second_comparison_term, curr_minus_var_ub, curr_ub, ROUND_UP); add_mul_assign_r(fourth_comparison_term, curr_minus_var_ub, curr_lb, ROUND_UP); - } + //} assign_r(first_comparison_term, std::max(first_comparison_term, second_comparison_term), @@ -5392,7 +5392,7 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, } } - n_var += 2; + n_var += 2; } } diff --git a/tests/Floating_Point_Expression/affineimage3.cc b/tests/Floating_Point_Expression/affineimage3.cc index 8438ea3..5736f8d 100644 --- a/tests/Floating_Point_Expression/affineimage3.cc +++ b/tests/Floating_Point_Expression/affineimage3.cc @@ -259,8 +259,36 @@ bool test08() { return ok; } -// tests affine_image(A, i1*A + i2*B + i3) +// tests affine_image(B, [-0.5, 0.5]*A) bool test09() { + Variable A(0); + Variable B(1); + + Octagonal_Shape<double> oc1(3); + oc1.add_constraint(A <= 2); + oc1.add_constraint(A - B <= 3); + oc1.add_constraint(B <= 2); + db_r_oc coeff(-0.5); + coeff.join_assign(0.5); + Linear_Form<db_r_oc> l(A); + l *= coeff; + oc1.affine_image(B, l); + print_constraints(oc1, "*** oc1.affine_image(B, [-0.5, 0.5]*A) ***"); + + Octagonal_Shape<double> known_result(3); + known_result.add_constraint(A <= 2); + known_result.add_constraint(-B + A <= 3); + known_result.add_constraint(A + B <= 3); + print_constraints(known_result, "*** known_result ***"); + + bool ok = (oc1 == known_result); + + return ok; +} + + +// tests affine_image(A, i + i0*A + i1*B) +bool test10() { Variable A(0); Variable B(1); @@ -271,22 +299,17 @@ bool test09() { oc1.add_constraint(B >= 0); oc1.add_constraint(B <= 2); oc1.add_constraint(A - B >= 0); - - print_constraints(oc1, "*** oc1 ***"); - db_r_oc i3(0); i3.join_assign(2); db_r_oc i2(1); i2.join_assign(2); db_r_oc i1(1); i1.join_assign(1); - Linear_Form<db_r_oc> l(i3); - l += i1*Linear_Form<db_r_oc>(A); l += i2*Linear_Form<db_r_oc>(B);; - print_constraints(oc1, "*** oc1.affine_image(A,i1*A+i2*B+i3) ***"); oc1.affine_image(A,l); + print_constraints(oc1, "*** oc1.affine_image(A, i + i0*A + i1*B) ***"); Octagonal_Shape<double> know_result(2); know_result.add_constraint(A >= 0); @@ -297,6 +320,7 @@ bool test09() { know_result.add_constraint(A + B <= 10); know_result.add_constraint(-A + B <= 0); know_result.add_constraint(-A - B <= 0); + print_constraints(know_result, "*** know_result ***"); bool ok = (oc1 == know_result); @@ -315,4 +339,5 @@ BEGIN_MAIN DO_TEST(test07); DO_TEST(test08); DO_TEST(test09); + DO_TEST(test10); END_MAIN

1 0

[GIT] ppl/ppl(pip): Fixes to avoid some useless Coefficient duplicates.
by François Galea 16 Sep '09

16 Sep '09

Module: ppl/ppl Branch: pip Commit: ec92733bc0d255c59bb78d80c813ea2fc32704c7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ec92733bc0d2… Author: François Galea <francois.galea(a)uvsq.fr> Date: Wed Sep 16 19:53:33 2009 +0200 Fixes to avoid some useless Coefficient duplicates. --- src/PIP_Tree.cc | 13 ++++++------- 1 files changed, 6 insertions(+), 7 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 8578048..604683c 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -388,9 +388,8 @@ PIP_Solution_Node::ascii_load(std::istream& s) { PIP_Solution_Node::Row_Sign PIP_Solution_Node::row_sign(const Row &x) { PIP_Solution_Node::Row_Sign sign = ZERO; - Coefficient c; for (int i = x.size(); i-- > 0; ) { - c = x[i]; + const Coefficient &c = x[i]; switch (sign) { case UNKNOWN: // cannot happen @@ -449,11 +448,11 @@ PIP_Solution_Node::compatibility_check(const Matrix &ctx, const Row &cnst) { break; } // Perform a pivot operation on the matrix - Coefficient sij = p[j]; + const Coefficient &sij = p[j]; for (j_=0; j_<num_cols; ++j_) { if (j_ == j) continue; - Coefficient sij_ = p[j_]; + const Coefficient &sij_ = p[j_]; for (k=0; k<num_rows; ++k) { Coefficient mult = s[k][j] * sij_; if (mult % sij != 0) { @@ -514,8 +513,8 @@ PIP_Solution_Node::update_tableau(PIP_Tree_Node ** /* parent_ref */, } internal_space_dim = external_space_dim; - Coefficient denom_s = tableau.s.get_denominator(); - Coefficient denom_t = tableau.t.get_denominator(); + const Coefficient &denom_s = tableau.s.get_denominator(); + const Coefficient &denom_t = tableau.t.get_denominator(); for (cst = input_cs.begin() + first_pending_constraint; cst < input_cs.end(); ++cst) { @@ -532,7 +531,7 @@ PIP_Solution_Node::update_tableau(PIP_Tree_Node ** /* parent_ref */, if (parameters.count(i) == 1) { param[p++] = cst->coefficient(Variable(i)) * denom_t; } else { - Coefficient c = cst->coefficient(Variable(i)); + const Coefficient &c = cst->coefficient(Variable(i)); dimension_type idx = mapping[v]; if (basis[v]) // Basic variable : add c * x_i

1 0

[GIT] ppl/ppl(pip): Implemented the Rational_Matrix normalize method.
by François Galea 16 Sep '09

16 Sep '09

Module: ppl/ppl Branch: pip Commit: 1024999dddcc6d7646b0f7bf26f0255652babad4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1024999dddcc… Author: François Galea <francois.galea(a)uvsq.fr> Date: Wed Sep 16 18:21:41 2009 +0200 Implemented the Rational_Matrix normalize method. --- src/PIP_Tree.cc | 30 +++++++++++++++++++++++++++++- 1 files changed, 29 insertions(+), 1 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index d528d37..8578048 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -298,7 +298,35 @@ PIP_Decision_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& context) { void PIP_Solution_Node::Rational_Matrix::normalize() { - //FIXME + if (denominator == 1) + return; + dimension_type i_max = num_rows(); + dimension_type j_max = num_columns(); + dimension_type i, j; + PPL_DIRTY_TEMP_COEFFICIENT(gcd); + gcd = denominator; + + for (i=0; i<i_max; ++i) { + const Row &row = rows[i]; + for (j=0; j<j_max; ++j) { + const Coefficient &x = row[j]; + if (x != 0) { + gcd_assign(gcd, x, gcd); + if (gcd == 1) + return; + } + } + } + + // Divide the coefficients by the GCD. + for (i=0; i<i_max; ++i) { + Row &row = rows[i]; + for (j=0; j<j_max; ++j) { + Coefficient &x = row[j]; + exact_div_assign(x, x, gcd); + } + } + exact_div_assign(denominator, denominator, gcd); } void

1 0

[GIT] ppl/ppl(floating_point): Small documentation improvements.
by Fabio Bossi 16 Sep '09

16 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 6685edf5c48bbdf791bdd392b9027f425b05928c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6685edf5c48b… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 16 17:56:29 2009 +0200 Small documentation improvements. --- doc/definitions.dox | 12 ++++++++++++ src/Octagonal_Shape.defs.hh | 2 +- 2 files changed, 13 insertions(+), 1 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index 7dee776..dd68fd4 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2731,6 +2731,18 @@ be denoted by \f$\linexpr{e} \left \langle \rho^{\#}, \rho^{\#}_l \right and - when we try to divide by an interval that contains \f$0\f$. +\subsection fp_abstract_domains Use of other abstract domains for floating point analysis + +Three of the other abstract domains of the PPL ( +\link Parma_Polyhedra_Library::BD_Shape \c BD_Shape \endlink, +\link Parma_Polyhedra_Library::Octagonal_Shape \c Octagonal_Shape \endlink, +and \link Parma_Polyhedra_Library::Polyhedron \c Polyhedron \endlink) +provide a few optimized methods to be used in the analysis of floating point +computations. They are recognized by the fact that they take interval +linear forms and/or an interval abstract stores as their parameters. + +Please see the methods' documentation for more information. + \section use_of_library Using the Library \subsection A_Note_on_the_Implementation_of_the_Operators A Note on the Implementation of the Operators diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 6ebd381..5377ca3 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -990,7 +990,7 @@ public: /*! \brief Refines the system of octagonal constraints defining \p *this using - the constraint expressed by \p left \f$\f$ \p right. + the constraint expressed by \p left \f$\leq\f$ \p right. \param left The linear form on intervals with floating point coefficients that

1 0

[GIT] ppl/ppl(floating_point): Added some comments.
by Fabio Bossi 16 Sep '09

16 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 164b9ef702d0b9d73a978f8acd6c639885ce9b81 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=164b9ef702d0… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 16 17:26:27 2009 +0200 Added some comments. --- src/Octagonal_Shape.defs.hh | 48 +++++++++++++++++++++++++++++++++++++++++++ 1 files changed, 48 insertions(+), 0 deletions(-) diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 5ac7536..6ebd381 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -988,6 +988,23 @@ public: */ void refine_with_congruences(const Congruence_System& cgs); + /*! \brief + Refines the system of octagonal constraints defining \p *this using + the constraint expressed by \p left \f$\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 + 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 + 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( const Linear_Form< Interval<T, Interval_Info> >& left, @@ -1113,6 +1130,22 @@ public: Coefficient_traits::const_reference denominator = Coefficient_one()); + /*! \brief + Assigns to \p *this the \ref affine_relation "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 coefficients that + defines the affine expression. ALL of its coefficients MUST be boundend. + + \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. + */ template <typename Interval_Info> void affine_image(Variable var, const Linear_Form< Interval<T, Interval_Info> >& lf); @@ -1698,6 +1731,11 @@ public: */ void fold_space_dimensions(const Variables_Set& vars, Variable dest); + //! Refines \p store with the constraints defining \p *this. + /*! + \param store + The interval floating point abstract store to refine. + */ template <typename Interval_Info> void refine_fp_interval_abstract_store( std::map< dimension_type, Interval<T, Interval_Info> >& store); @@ -1803,6 +1841,16 @@ private: N& matrix_at(dimension_type i, dimension_type j); const N& matrix_at(dimension_type i, dimension_type j) const; + /*! \brief + Returns an upper bound for \p lf according to the constraints + embedded in \p *this. + + \p lf must be a linear form on intervals with floating point coefficients. + If all coefficients in \p lf are bounded, then \p result will become a + correct overapproximation of the value of \p lf when variables in + \p lf satisfy the constraints expressed by \p *this. Otherwise the + behavior of the method is undefined. + */ template <typename Interval_Info> void linear_form_upper_bound( const Linear_Form< Interval<T, Interval_Info> >& lf,

1 0