October 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(pip): Unified the common denominator between both matrices of the tableau.
by François Galea 02 Oct '09

02 Oct '09

Module: ppl/ppl Branch: pip Commit: 039d147fe8112c460b66c6fb8b5e76109909ecf0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=039d147fe811… Author: François Galea <francois.galea(a)uvsq.fr> Date: Fri Oct 2 10:57:20 2009 +0200 Unified the common denominator between both matrices of the tableau. --- src/PIP_Tree.cc | 110 ++++++++++++++++++++++++++++------------------ src/PIP_Tree.defs.hh | 65 +++++++++------------------- src/PIP_Tree.inlines.hh | 31 +++++++------ 3 files changed, 105 insertions(+), 101 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=039d147f…

1 0

[GIT] ppl/ppl(floating_point): Implemented a test on rate limiter which uses octagons abstract
by Roberto Amadini 02 Oct '09

02 Oct '09

Module: ppl/ppl Branch: floating_point Commit: eb9cef62704bb38eb71996631dfcd25c8c341dcb URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=eb9cef62704b… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Fri Oct 2 14:49:25 2009 +0200 Implemented a test on rate limiter which uses octagons abstract domain and linearization of floating point expressions. --- tests/Floating_Point_Expression/digitalfilters1.cc | 107 ++++++++++++++++++-- 1 files changed, 100 insertions(+), 7 deletions(-) diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index b94b5f9..bc77d19 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -201,11 +201,11 @@ test03() { //if (R <= -D) Y = S - D; FP_Octagonal_Shape oc_then(oc); oc_then.refine_with_linear_form_inequality(FP_Linear_Form(R), - -FP_Linear_Form(D)); + -FP_Linear_Form(D)); oc_then.affine_image(Y, FP_Linear_Form(S - D)); oc.refine_with_linear_form_inequality(-FP_Linear_Form(D), - FP_Linear_Form(R)); + FP_Linear_Form(R)); oc.upper_bound_assign(oc_then); print_constraints(Box<FP_Interval>(oc) , "*** if (R <= -D) Y = S - D; ***"); @@ -213,11 +213,11 @@ test03() { //if (R >= D) Y = S + D; oc_then = oc; oc_then.refine_with_linear_form_inequality(FP_Linear_Form(D), - FP_Linear_Form(R)); + FP_Linear_Form(R)); oc_then.affine_image(Y, FP_Linear_Form(S + D)); oc.refine_with_linear_form_inequality(FP_Linear_Form(R), - FP_Linear_Form(D)); + FP_Linear_Form(D)); oc.upper_bound_assign(oc_then); print_constraints(Box<FP_Interval>(oc) , @@ -303,12 +303,105 @@ test04() { return tmp.is_bounded(); } +// tests rate limiter using octagons abstract domain and +// linearization of floating point expressions. +bool +test05() { + Variable X(0); //input + Variable D(1); //input + Variable Y(2); //output + Variable S(3); //last output + Variable R(4); //actual rate + FP_Interval_Abstract_Store abstract_store(5); + FP_Linear_Form_Abstract_Store lf_abstract_store; + FP_Octagonal_Shape oc(abstract_store); + FP_Interval tmp(0); + FP_Octagonal_Shape oc_begin; + Con_FP_Expression con_y(0, 0); + FP_Linear_Form lx; + FP_Linear_Form ly; + FP_Linear_Form lr; + FP_Linear_Form lk; + + // Y = 0; + con_y.linearize(abstract_store, lf_abstract_store, lk); + oc.affine_image(Y, lk); + FP_Interval threesold(-144); + threesold.join_assign(144); + + for(unsigned int n = 0; !tmp.contains(threesold); ++n) { + + nout << "*** n = " << n << " ***" << endl; + oc_begin = oc; + + Con_FP_Expression con_x(-128, 128); + con_x.linearize(abstract_store, lf_abstract_store, lk); + oc.affine_image(X, lk); + + Con_FP_Expression con_d(0, 16); + con_d.linearize(abstract_store, lf_abstract_store, lk); + oc.affine_image(D, lk); + + Var_FP_Expression var_y(2); + var_y.linearize(abstract_store, lf_abstract_store, ly); + oc.affine_image(S, ly); + + Var_FP_Expression* px = new Var_FP_Expression(0); + Var_FP_Expression* ps = new Var_FP_Expression(3); + Dif_FP_Expression x_dif_s(px, ps); + x_dif_s.linearize(abstract_store, lf_abstract_store, lr); + oc.affine_image(R, lr); + + Var_FP_Expression var_x(0); + var_x.linearize(abstract_store, lf_abstract_store, lx); + oc.affine_image(Y, lx); + + //if (R <= -D) Y = S - D; + FP_Octagonal_Shape oc_then(oc); + oc_then.refine_with_linear_form_inequality(lr, -lk); + + Var_FP_Expression* pd = new Var_FP_Expression(1); + Var_FP_Expression* ps2 = new Var_FP_Expression(3); + Dif_FP_Expression s_dif_d(ps2, pd); + s_dif_d.linearize(abstract_store, lf_abstract_store, ly); + oc_then.affine_image(Y, ly); + + oc.refine_with_linear_form_inequality(-lk, lr); + + oc.upper_bound_assign(oc_then); + print_constraints(Box<FP_Interval>(oc) , + "*** if (R <= -D) Y = S - D; ***"); + + //if (R >= D) Y = S + D; + oc_then = oc; + oc_then.refine_with_linear_form_inequality(lk, lr); + + Var_FP_Expression* pd1 = new Var_FP_Expression(1); + Var_FP_Expression* ps3 = new Var_FP_Expression(3); + Sum_FP_Expression s_sum_d(ps3, pd1); + s_sum_d.linearize(abstract_store, lf_abstract_store, ly); + oc_then.affine_image(Y, ly); + + oc.refine_with_linear_form_inequality(lr, lk); + + oc.upper_bound_assign(oc_then); + Box<FP_Interval> box(oc); + print_constraints(box, "*** if (R >= D) Y = S + D; ***"); + tmp = box.get_interval(Y); + } + + oc.refine_fp_interval_abstract_store(abstract_store); + tmp = abstract_store.get_interval(Y); + nout << "*** Y in " << tmp << " ***" << endl; + return tmp.is_bounded(); +} } // namespace BEGIN_MAIN - //DO_TEST(test01); + DO_TEST(test01); DO_TEST(test02); - //DO_TEST(test03); - //DO_TEST(test04); + DO_TEST(test03); + DO_TEST(test04); + DO_TEST(test05); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Improved BD_Shape<T>:: refine_with_linear_form_inequality.
by Roberto Amadini 01 Oct '09

01 Oct '09

Module: ppl/ppl Branch: floating_point Commit: fcb9568396f2be664cd096a1d0b49e7605a5da1d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fcb9568396f2… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Thu Oct 1 22:38:57 2009 +0200 Improved BD_Shape<T>::refine_with_linear_form_inequality. Corrected BD_Shape<T>::affine_image. Adapted tests in bshape2.cc and finished test02 in digitalfilters1.cc --- src/BD_Shape.templates.hh | 63 ++++++++++++++----- tests/Floating_Point_Expression/Makefile.am | 6 +- tests/Floating_Point_Expression/bdshape2.cc | 34 ++++++---- tests/Floating_Point_Expression/digitalfilters1.cc | 15 ++--- 4 files changed, 75 insertions(+), 43 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index 47e74af..70be7c8 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4238,7 +4238,8 @@ void BD_Shape<T> const dimension_type& space_dim) { // Remove all constraints on 'var'. - forget_all_dbm_constraints(var_id); + //forget_all_dbm_constraints(var_id); + // Shortest-path closure is maintained, but not reduction. if (marked_shortest_path_reduced()) reset_shortest_path_reduced(); @@ -4480,7 +4481,7 @@ BD_Shape<T> ROUND_UP); div_2exp_assign_r(a_plus_minus_b_minus, a_plus_minus_b_minus, 1, ROUND_UP); - add_dbm_constraint(0, left_w_id+1, a_plus_minus_b_minus); + add_dbm_constraint(0, left_w_id + 1, a_plus_minus_b_minus); return; } if (is_left_coeff_minus_one && is_right_coeff_one) { @@ -4493,26 +4494,55 @@ BD_Shape<T> ROUND_UP); div_2exp_assign_r(a_plus_minus_b_minus, a_plus_minus_b_minus, 1, ROUND_UP); - add_dbm_constraint(right_w_id+1, 0, a_plus_minus_b_minus); + add_dbm_constraint(right_w_id + 1, 0, a_plus_minus_b_minus); return; } } else if (is_left_coeff_minus_one && is_right_coeff_one) { - // if right and left coefficents are negative the constraint - // - x - y <= b - // is ignored; - - // FIXME: manage this case adding a costraint - x <= k - // where k is an overaproximation of b + y - return; + // over-approximate (if is it possible) the inequality + // -B + [b1, b2] <= A + [a1, a2] by adding the constraints + // -B <= upper_bound(A) + (a2 - b1) and + // -A <= upper_bound(B) + (a2 - b1) + PPL_DIRTY_TEMP(N, a_plus_minus_b_minus); + const FP_Interval_Type& left_b = left.inhomogeneous_term(); + const FP_Interval_Type& right_a = right.inhomogeneous_term(); + sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(), + ROUND_UP); + PPL_DIRTY_TEMP(N, ub); + ub = dbm[0][right_w_id + 1]; + if (!is_plus_infinity(ub)) { + add_assign_r(ub, ub, a_plus_minus_b_minus, ROUND_UP); + add_dbm_constraint(left_w_id + 1, 0, ub); + } + ub = dbm[0][left_w_id + 1]; + if (!is_plus_infinity(ub)) { + add_assign_r(ub, ub, a_plus_minus_b_minus, ROUND_UP); + add_dbm_constraint(right_w_id + 1, 0, ub); + } + return; } if (is_left_coeff_one && is_right_coeff_minus_one) { - // if right coefficent is negative the constraint x + y <= b - // is ignored; - - // FIXME: manage this case adding a costraint x <= k - // where k is an overaproximation of b - y - return; + // over-approximate (if is it possible) the inequality + // B + [b1, b2] <= -A + [a1, a2] by adding the constraints + // B <= upper_bound(-A) + (a2 - b1) and + // A <= upper_bound(-B) + (a2 - b1) + PPL_DIRTY_TEMP(N, a_plus_minus_b_minus); + const FP_Interval_Type& left_b = left.inhomogeneous_term(); + const FP_Interval_Type& right_a = right.inhomogeneous_term(); + sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(), + ROUND_UP); + PPL_DIRTY_TEMP(N, ub); + ub = dbm[right_w_id + 1][0]; + if (!is_plus_infinity(ub)) { + add_assign_r(ub, ub, a_plus_minus_b_minus, ROUND_UP); + add_dbm_constraint(0, left_w_id + 1, ub); + } + ub = dbm[left_w_id + 1][0]; + if (!is_plus_infinity(ub)) { + add_assign_r(ub, ub, a_plus_minus_b_minus, ROUND_UP); + add_dbm_constraint(0, right_w_id + 1, ub); + } + return; } if (is_left_coeff_one && is_right_coeff_one) { PPL_DIRTY_TEMP(N, c_plus_minus_a_minus); @@ -4545,7 +4575,6 @@ BD_Shape<T> const Linear_Form< Interval<T, Interval_Info> >& right) { typedef Interval<T, Interval_Info> FP_Interval_Type; - Linear_Form<FP_Interval_Type> right_minus_left(right); right_minus_left -= left; diff --git a/tests/Floating_Point_Expression/Makefile.am b/tests/Floating_Point_Expression/Makefile.am index b6d2a0c..9755e4b 100644 --- a/tests/Floating_Point_Expression/Makefile.am +++ b/tests/Floating_Point_Expression/Makefile.am @@ -53,6 +53,8 @@ $(top_builddir)/src/libppl.la \ ORIGINAL_TESTS = \ digitalfilters1 +#digitalfilters1 +#bdshape2 \ #bdshape1 \ #floatingpointexpr1 \ #linearform1 \ @@ -62,8 +64,6 @@ digitalfilters1 #polyhedron2 - - DERIVED_TESTS = ALL_TESTS = $(ORIGINAL_TESTS) $(DERIVED_TESTS) @@ -134,7 +134,7 @@ print_INSTANCES: digitalfilters1_SOURCES = digitalfilters1.cc -#bdshape2_SOURCE = bdshape2.cc +#bdshape2_SOURCES = bdshape2.cc #polyhedron2_SOURCES = polyhedron2.cc diff --git a/tests/Floating_Point_Expression/bdshape2.cc b/tests/Floating_Point_Expression/bdshape2.cc index 5a70ad3..f0f30a7 100644 --- a/tests/Floating_Point_Expression/bdshape2.cc +++ b/tests/Floating_Point_Expression/bdshape2.cc @@ -32,7 +32,7 @@ test01() { bool ok1 = false; FP_Linear_Form l1(A); FP_Linear_Form l2; - + try{ bd1.refine_with_linear_form_inequality(l1,l2); std::cout <<"no eccezione" <<std::endl; @@ -40,8 +40,8 @@ test01() { catch(std::invalid_argument e) { ok1 = true; } - - + + bool ok2 = false; try{ bd1.refine_with_linear_form_inequality(l2,l1); @@ -59,7 +59,7 @@ test01() { bd2.refine_with_linear_form_inequality(l1, l2); ok2 = true; } - + return ok1 && ok2; } @@ -198,14 +198,16 @@ test05() { l1 += tmp; bd1.refine_with_linear_form_inequality(l1, l2); print_constraints(bd1, "*** [1, 3] + A <= [4, 4] - B ***"); - + print_constraints(known_result, "*** known_result ***"); - + bool ok1 = (bd1 == known_result); bd1.refine_with_linear_form_inequality(l2, l1); print_constraints(bd1, "*** [4, 4] - B <= [1, 3] + A ***"); + known_result.add_constraint(-A <= 1); + known_result.add_constraint(-B <= 1); print_constraints(known_result, "*** known_result2 ***"); bool ok2 = (bd1 == known_result); @@ -235,12 +237,14 @@ test06() { bd1.refine_with_linear_form_inequality(l1, l2); print_constraints(bd1, "*** [1, 4] - A <= [-2, -2] + B ***"); + known_result.add_constraint(-A <= -1); + known_result.add_constraint(-B <= -1); print_constraints(known_result, "*** known_result ***"); bool ok1 = (bd1 == known_result); bd1.refine_with_linear_form_inequality(l2, l1); - print_constraints(bd1, "*** [4, 4] - B <= [1, 3] + A ***"); + print_constraints(bd1, "*** [-2, -2] + B <= [1, 4] - A ***"); print_constraints(known_result, "*** known_result2 ***"); @@ -457,7 +461,7 @@ test12() { tmp.join_assign(-1); FP_Linear_Form l2(tmp); FP_Linear_Form l1(-A); - + bd1.refine_with_linear_form_inequality(l1, l2); print_constraints(bd1, "*** - A <= [-1, 0] ***"); @@ -476,7 +480,7 @@ test12() { return ok1 && ok2; } -// tests A <= - B + [-1, 0] and - B + [0, 1] <= A +// tests A <= - B + [-1, 0] and - B + [-1, 0] <= A bool test13() { Variable A(0); @@ -492,7 +496,7 @@ test13() { FP_Linear_Form l2(-B); FP_Linear_Form l1(A); l2 += tmp; - + bd1.refine_with_linear_form_inequality(l1, l2); print_constraints(bd1, "*** A <= - B + [-1, 0] ***"); @@ -501,8 +505,10 @@ test13() { bool ok1 = (bd1 == known_result); bd1.refine_with_linear_form_inequality(l2, l1); - print_constraints(bd1, "*** - B + [0, 1] <= A ***"); - + print_constraints(bd1, "*** - B + [-1, 0] <= A ***"); + known_result.add_constraint(-A <= 3); + known_result.add_constraint(-B <= 3); + print_constraints(known_result, "*** known_result ***"); bool ok2 = (bd1 == known_result); @@ -526,7 +532,7 @@ test14() { FP_Linear_Form l2(-A); FP_Linear_Form l1(A); l2 += tmp; - + bd1.refine_with_linear_form_inequality(l1, l2); print_constraints(bd1, "*** A <= - A + [-1, 0] ***"); @@ -537,7 +543,7 @@ test14() { bd1.refine_with_linear_form_inequality(l2, l1); print_constraints(bd1, "*** - A + [0, 1] <= A ***"); - + known_result.add_constraint(2*(-A) <= 1); print_constraints(known_result, "*** known_result ***"); diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index 4f444cd..b94b5f9 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -100,7 +100,6 @@ test01() { print_constraints(abstract_store ,"*** if (R >= D) Y = S + D; ***"); } - tmp = abstract_store.get_interval(Y); nout << "*** Y in [-128 - 16n, 128 + 16n] ***" << endl; return tmp.is_bounded(); } @@ -121,7 +120,7 @@ test02() { // Y = 0; bd.affine_image(Y, FP_Linear_Form(tmp)); - for(unsigned int n = 0; bd_begin != bd; ++n) { + for(unsigned int n = 0; n < 5; ++n) { nout << "*** n = " << n << " ***" << endl; bd_begin = bd; @@ -163,9 +162,7 @@ test02() { "*** if (R >= D) Y = S + D; ***"); } - bd.refine_fp_interval_abstract_store(abstract_store); - tmp = abstract_store.get_interval(Y); - nout << "*** Y in " << tmp << " ***" << endl; + nout << "*** Y in [-16 - 16n, 128 + 16n] ***" << endl; return tmp.is_bounded(); } @@ -310,8 +307,8 @@ test04() { } // namespace BEGIN_MAIN - DO_TEST(test01); - //DO_TEST(test02); - DO_TEST(test03); - DO_TEST(test04); + //DO_TEST(test01); + DO_TEST(test02); + //DO_TEST(test03); + //DO_TEST(test04); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Fixed bug in BD_Shape<T>:: two_variables_affine_image.
by Roberto Amadini 01 Oct '09

01 Oct '09

Module: ppl/ppl Branch: floating_point Commit: 0ca73838e132e6f1f80de75ece6312aba89fa878 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0ca73838e132… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Thu Oct 1 18:17:27 2009 +0200 Fixed bug in BD_Shape<T>::two_variables_affine_image. Added a first implementation of test02. --- src/BD_Shape.templates.hh | 33 ++++++----- tests/Floating_Point_Expression/digitalfilters1.cc | 59 +++++++++++++++++++- 2 files changed, 76 insertions(+), 16 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index a1f5694..47e74af 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4237,10 +4237,13 @@ void BD_Shape<T> const Linear_Form< Interval<T, Interval_Info> >& lf, const dimension_type& space_dim) { - // Shortest-path closure is preserved, but not reduction. + // Remove all constraints on 'var'. + forget_all_dbm_constraints(var_id); + // Shortest-path closure is maintained, but not reduction. if (marked_shortest_path_reduced()) reset_shortest_path_reduced(); + reset_shortest_path_closed(); Linear_Form< Interval<T, Interval_Info> > minus_lf(lf); minus_lf.negate(); @@ -4332,9 +4335,9 @@ void BD_Shape<T>::refine_with_linear_form_inequality( right_w_id = i; } - const FP_Interval_Type& left_w_coeff = + const FP_Interval_Type& left_w_coeff = left.coefficient(Variable(left_w_id)); - const FP_Interval_Type& right_w_coeff = + const FP_Interval_Type& right_w_coeff = right.coefficient(Variable(right_w_id)); // FIXME: there is plenty of duplicate code in the following lines. We could @@ -4378,7 +4381,7 @@ BD_Shape<T>::left_inhomogeneous_refine(const dimension_type& right_t, const Linear_Form< Interval<T, Interval_Info> >& right) { typedef Interval<T, Interval_Info> FP_Interval_Type; - + if (right_t == 1) { // The constraint has the form [a-;a+] <= [b-;b+] + [c-;c+] * x. // Reduce it to the constraint +/-x <= b+ - a- if [c-;c+] = +/-[1;1]. @@ -4418,7 +4421,7 @@ BD_Shape<T> const Linear_Form< Interval<T, Interval_Info> >& right) { typedef Interval<T, Interval_Info> FP_Interval_Type; - + if (right_t == 0) { // The constraint has the form [b-;b+] + [c-;c+] * x <= [a-;a+] // Reduce it to the constraint +/-x <= a+ - b- if [c-;c+] = +/-[1;1]. @@ -4445,7 +4448,7 @@ BD_Shape<T> return; } } // fi right_t == 0 - + if(right_t == 1) { // The constraint has the form: // [a-;a+] + [b-;b+] * x <= [c-;c+] + [d-;d+] * y. @@ -4475,8 +4478,8 @@ BD_Shape<T> const FP_Interval_Type& right_a = right.inhomogeneous_term(); sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(), ROUND_UP); - div_2exp_assign_r(a_plus_minus_b_minus, a_plus_minus_b_minus, 1, - ROUND_UP); + div_2exp_assign_r(a_plus_minus_b_minus, a_plus_minus_b_minus, 1, + ROUND_UP); add_dbm_constraint(0, left_w_id+1, a_plus_minus_b_minus); return; } @@ -4488,14 +4491,14 @@ BD_Shape<T> const FP_Interval_Type& right_a = right.inhomogeneous_term(); sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(), ROUND_UP); - div_2exp_assign_r(a_plus_minus_b_minus, a_plus_minus_b_minus, 1, + div_2exp_assign_r(a_plus_minus_b_minus, a_plus_minus_b_minus, 1, ROUND_UP); add_dbm_constraint(right_w_id+1, 0, a_plus_minus_b_minus); return; } } else if (is_left_coeff_minus_one && is_right_coeff_one) { - // if right and left coefficents are negative the constraint + // if right and left coefficents are negative the constraint // - x - y <= b // is ignored; @@ -4511,7 +4514,7 @@ BD_Shape<T> // where k is an overaproximation of b - y return; } - if (is_left_coeff_one && is_right_coeff_one) { + if (is_left_coeff_one && is_right_coeff_one) { PPL_DIRTY_TEMP(N, c_plus_minus_a_minus); const FP_Interval_Type& left_a = left.inhomogeneous_term(); const FP_Interval_Type& right_c = right.inhomogeneous_term(); @@ -4550,9 +4553,9 @@ BD_Shape<T> PPL_DIRTY_TEMP(N, low_coeff); PPL_DIRTY_TEMP(N, high_coeff); PPL_DIRTY_TEMP(N, upper_bound); - + dimension_type max_w_id = std::max(left_w_id, right_w_id); - + for (dimension_type first_v = 0; first_v < max_w_id; ++first_v) { for (dimension_type second_v = first_v+1; second_v <= max_w_id; ++second_v) { @@ -4597,7 +4600,7 @@ BD_Shape<T> } } } - + if (do_update) { Variable first(first_v); Variable second(second_v); @@ -4642,7 +4645,7 @@ BD_Shape<T> add_dbm_constraint(n_var, 0, upper_bound); } } - + } template <typename T> diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index 9405d22..4f444cd 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -108,8 +108,65 @@ test01() { // tests rate limiter using bounded differences abstract domain. bool test02() { + Variable X(0); //input + Variable D(1); //input + Variable Y(2); //output + Variable S(3); //last output + Variable R(4); //actual rate + FP_Interval_Abstract_Store abstract_store(5); + FP_BD_Shape bd(abstract_store); + FP_Interval tmp(0); + FP_BD_Shape bd_begin; + + // Y = 0; + bd.affine_image(Y, FP_Linear_Form(tmp)); + + for(unsigned int n = 0; bd_begin != bd; ++n) { + + nout << "*** n = " << n << " ***" << endl; + bd_begin = bd; + + //X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X; + tmp.lower() = -128; + tmp.upper() = 128; + bd.affine_image(X, FP_Linear_Form(tmp)); + tmp.lower() = 0; + tmp.upper() = 16; + bd.affine_image(D, FP_Linear_Form(tmp)); + bd.affine_image(S, FP_Linear_Form(Y)); + bd.affine_image(R, FP_Linear_Form(X - S)); + bd.affine_image(Y, FP_Linear_Form(X)); + + //if (R <= -D) Y = S - D; + FP_BD_Shape bd_then(bd); + bd_then.refine_with_linear_form_inequality(FP_Linear_Form(R), + -FP_Linear_Form(D)); + bd_then.affine_image(Y, FP_Linear_Form(S - D)); + + bd.refine_with_linear_form_inequality(-FP_Linear_Form(D), + FP_Linear_Form(R)); + bd.upper_bound_assign(bd_then); + print_constraints(Box<FP_Interval>(bd) , + "*** if (R <= -D) Y = S - D; ***"); + + //if (R >= D) Y = S + D; + bd_then = bd; + bd_then.refine_with_linear_form_inequality(FP_Linear_Form(D), + FP_Linear_Form(R)); + bd_then.affine_image(Y, FP_Linear_Form(S + D)); - return true; + bd.refine_with_linear_form_inequality(FP_Linear_Form(R), + FP_Linear_Form(D)); + + bd.upper_bound_assign(bd_then); + print_constraints(Box<FP_Interval>(bd) , + "*** if (R >= D) Y = S + D; ***"); + } + + bd.refine_fp_interval_abstract_store(abstract_store); + tmp = abstract_store.get_interval(Y); + nout << "*** Y in " << tmp << " ***" << endl; + return tmp.is_bounded(); } // tests rate limiter using octagons abstract domain.

1 0

[GIT] ppl/ppl(floating_point): Implemented test of rate limiter using polyhedra abstract domain.
by Roberto Amadini 01 Oct '09

01 Oct '09

Module: ppl/ppl Branch: floating_point Commit: 1bdc33c7fc6f32742bd2c12760406394d5d7ab08 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1bdc33c7fc6f… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Thu Oct 1 17:32:59 2009 +0200 Implemented test of rate limiter using polyhedra abstract domain. --- tests/Floating_Point_Expression/digitalfilters1.cc | 24 ++++++++----------- 1 files changed, 10 insertions(+), 14 deletions(-) diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index 63da991..9405d22 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -101,7 +101,7 @@ test01() { } tmp = abstract_store.get_interval(Y); - nout << "*** Y in " << tmp << " ***" << endl; + nout << "*** Y in [-128 - 16n, 128 + 16n] ***" << endl; return tmp.is_bounded(); } @@ -187,11 +187,6 @@ test04() { FP_Interval_Abstract_Store abstract_store(5); NNC_Polyhedron ph(abstract_store); FP_Interval tmp(0); - abstract_store.set_interval(X, tmp); - abstract_store.set_interval(D, tmp); - abstract_store.set_interval(Y, tmp); - abstract_store.set_interval(S, tmp); - abstract_store.set_interval(R, tmp); NNC_Polyhedron ph_begin; // Y = 0; @@ -209,8 +204,11 @@ test04() { tmp.lower() = 0; tmp.upper() = 16; ph.affine_image(D, FP_Linear_Form(tmp), abstract_store); + abstract_store = Box<FP_Interval>(ph); ph.affine_image(S, FP_Linear_Form(Y), abstract_store); + abstract_store = Box<FP_Interval>(ph); ph.affine_image(R, FP_Linear_Form(X - S), abstract_store); + abstract_store = Box<FP_Interval>(ph); ph.affine_image(Y, FP_Linear_Form(X), abstract_store); //if (R <= -D) Y = S - D; @@ -218,8 +216,8 @@ test04() { FP_Interval_Abstract_Store as_then(abstract_store); ph_then.refine_with_linear_form_inequality(FP_Linear_Form(R), -FP_Linear_Form(D), - abstract_store); - ph_then.affine_image(Y, FP_Linear_Form(S - D), abstract_store); + as_then); + ph_then.affine_image(Y, FP_Linear_Form(S - D), as_then); ph.refine_with_linear_form_inequality(-FP_Linear_Form(D), FP_Linear_Form(R), @@ -234,20 +232,18 @@ test04() { as_then = abstract_store; ph_then.refine_with_linear_form_inequality(FP_Linear_Form(D), FP_Linear_Form(R), - abstract_store); - ph_then.affine_image(Y, FP_Linear_Form(S + D), abstract_store); + as_then); + ph_then.affine_image(Y, FP_Linear_Form(S + D), as_then); ph.refine_with_linear_form_inequality(FP_Linear_Form(R), FP_Linear_Form(D), abstract_store); - ph.upper_bound_assign(ph_then); abstract_store.upper_bound_assign(as_then); print_constraints(Box<FP_Interval>(ph) , "*** if (R >= D) Y = S + D; ***"); } - ph.refine_fp_interval_abstract_store(abstract_store); tmp = abstract_store.get_interval(Y); nout << "*** Y in " << tmp << " ***" << endl; return tmp.is_bounded(); @@ -257,8 +253,8 @@ test04() { } // namespace BEGIN_MAIN - //DO_TEST(test01); + DO_TEST(test01); //DO_TEST(test02); DO_TEST(test03); - //DO_TEST(test04); + DO_TEST(test04); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Modified test03 and test04.
by Roberto Amadini 01 Oct '09

01 Oct '09

Module: ppl/ppl Branch: floating_point Commit: f18c42ee75a560eb6221c759de4297b7db58bb7a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f18c42ee75a5… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Thu Oct 1 16:40:19 2009 +0200 Modified test03 and test04. --- tests/Floating_Point_Expression/Makefile.am | 14 ++-- tests/Floating_Point_Expression/digitalfilters1.cc | 87 ++++++++++++++++++-- 2 files changed, 85 insertions(+), 16 deletions(-) diff --git a/tests/Floating_Point_Expression/Makefile.am b/tests/Floating_Point_Expression/Makefile.am index 27acb8a..b6d2a0c 100644 --- a/tests/Floating_Point_Expression/Makefile.am +++ b/tests/Floating_Point_Expression/Makefile.am @@ -136,19 +136,19 @@ digitalfilters1_SOURCES = digitalfilters1.cc #bdshape2_SOURCE = bdshape2.cc -polyhedron2_SOURCES = polyhedron2.cc +#polyhedron2_SOURCES = polyhedron2.cc -polyhedron1_SOURCES = polyhedron1.cc +#polyhedron1_SOURCES = polyhedron1.cc -bdshape1_SOURCES = bdshape1.cc +#bdshape1_SOURCES = bdshape1.cc -floatingpointexpr1_SOURCES = floatingpointexpr1.cc +#floatingpointexpr1_SOURCES = floatingpointexpr1.cc -linearform1_SOURCES = linearform1.cc +#linearform1_SOURCES = linearform1.cc -octagonalshape1_SOURCES = octagonalshape1.cc +#octagonalshape1_SOURCES = octagonalshape1.cc -octagonalshape2_SOURCES = octagonalshape2.cc +#octagonalshape2_SOURCES = octagonalshape2.cc # diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index a0a5a40..63da991 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -112,7 +112,7 @@ test02() { return true; } -// tests rate limiter using octagons abstract domain and +// tests rate limiter using octagons abstract domain. bool test03() { Variable X(0); //input @@ -146,7 +146,6 @@ test03() { //if (R <= -D) Y = S - D; FP_Octagonal_Shape oc_then(oc); - FP_Interval_Abstract_Store as_then(abstract_store); oc_then.refine_with_linear_form_inequality(FP_Linear_Form(R), -FP_Linear_Form(D)); oc_then.affine_image(Y, FP_Linear_Form(S - D)); @@ -154,12 +153,11 @@ test03() { oc.refine_with_linear_form_inequality(-FP_Linear_Form(D), FP_Linear_Form(R)); oc.upper_bound_assign(oc_then); - abstract_store.upper_bound_assign(as_then); - print_constraints(Box<FP_Interval>(oc) ,"*** if (R <= -D) Y = S - D; ***"); + print_constraints(Box<FP_Interval>(oc) , + "*** if (R <= -D) Y = S - D; ***"); //if (R >= D) Y = S + D; oc_then = oc; - as_then = abstract_store; oc_then.refine_with_linear_form_inequality(FP_Linear_Form(D), FP_Linear_Form(R)); oc_then.affine_image(Y, FP_Linear_Form(S + D)); @@ -168,8 +166,8 @@ test03() { FP_Linear_Form(D)); oc.upper_bound_assign(oc_then); - abstract_store.upper_bound_assign(as_then); - print_constraints(Box<FP_Interval>(oc) ,"*** if (R >= D) Y = S + D; ***"); + print_constraints(Box<FP_Interval>(oc) , + "*** if (R >= D) Y = S + D; ***"); } oc.refine_fp_interval_abstract_store(abstract_store); @@ -178,17 +176,88 @@ test03() { return tmp.is_bounded(); } +// tests rate limiter using polyhedra abstract domain. bool test04() { + Variable X(0); //input + Variable D(1); //input + Variable Y(2); //output + Variable S(3); //last output + Variable R(4); //actual rate + FP_Interval_Abstract_Store abstract_store(5); + NNC_Polyhedron ph(abstract_store); + FP_Interval tmp(0); + abstract_store.set_interval(X, tmp); + abstract_store.set_interval(D, tmp); + abstract_store.set_interval(Y, tmp); + abstract_store.set_interval(S, tmp); + abstract_store.set_interval(R, tmp); + NNC_Polyhedron ph_begin; - return true; + // Y = 0; + ph.affine_image(Y, FP_Linear_Form(tmp), abstract_store); + + for(unsigned int n = 0; ph_begin != ph; ++n) { + + nout << "*** n = " << n << " ***" << endl; + ph_begin = ph; + + //X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X; + tmp.lower() = -128; + tmp.upper() = 128; + ph.affine_image(X, FP_Linear_Form(tmp), abstract_store); + tmp.lower() = 0; + tmp.upper() = 16; + ph.affine_image(D, FP_Linear_Form(tmp), abstract_store); + ph.affine_image(S, FP_Linear_Form(Y), abstract_store); + ph.affine_image(R, FP_Linear_Form(X - S), abstract_store); + ph.affine_image(Y, FP_Linear_Form(X), abstract_store); + + //if (R <= -D) Y = S - D; + NNC_Polyhedron ph_then(ph); + FP_Interval_Abstract_Store as_then(abstract_store); + ph_then.refine_with_linear_form_inequality(FP_Linear_Form(R), + -FP_Linear_Form(D), + abstract_store); + ph_then.affine_image(Y, FP_Linear_Form(S - D), abstract_store); + + ph.refine_with_linear_form_inequality(-FP_Linear_Form(D), + FP_Linear_Form(R), + abstract_store); + ph.upper_bound_assign(ph_then); + abstract_store.upper_bound_assign(as_then); + print_constraints(Box<FP_Interval>(ph) , + "*** if (R <= -D) Y = S - D; ***"); + + //if (R >= D) Y = S + D; + ph_then = ph; + as_then = abstract_store; + ph_then.refine_with_linear_form_inequality(FP_Linear_Form(D), + FP_Linear_Form(R), + abstract_store); + ph_then.affine_image(Y, FP_Linear_Form(S + D), abstract_store); + + ph.refine_with_linear_form_inequality(FP_Linear_Form(R), + FP_Linear_Form(D), + abstract_store); + + ph.upper_bound_assign(ph_then); + abstract_store.upper_bound_assign(as_then); + print_constraints(Box<FP_Interval>(ph) , + "*** if (R >= D) Y = S + D; ***"); + } + + ph.refine_fp_interval_abstract_store(abstract_store); + tmp = abstract_store.get_interval(Y); + nout << "*** Y in " << tmp << " ***" << endl; + return tmp.is_bounded(); } } // namespace BEGIN_MAIN - DO_TEST(test01); + //DO_TEST(test01); //DO_TEST(test02); DO_TEST(test03); //DO_TEST(test04);

1 0

[GIT] ppl/ppl(floating_point): Fixed a few assertions.
by Fabio Bossi 01 Oct '09

01 Oct '09

Module: ppl/ppl Branch: floating_point Commit: 05770258f702f3495008960334c9731ac5d26d5e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=05770258f702… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Oct 1 16:35:05 2009 +0200 Fixed a few assertions. --- src/Polyhedron.templates.hh | 5 ++--- 1 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index d35090b..8f8faa6 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -309,7 +309,6 @@ Polyhedron::refine_with_linear_form_inequality( " FP_Format not a floating point type."); PPL_ASSERT(space_dim <= store.space_dimension()); - PPL_ASSERT(store.is_bounded()); // Dimension compatibility checks. // The dimensions of left and right should not be greater than the // dimension of *this. @@ -359,7 +358,6 @@ const Box< Interval<FP_Format, Interval_Info> >& store) { " FP_Format not a floating point type."); PPL_ASSERT(space_dim <= store.space_dimension()); - PPL_ASSERT(store.is_bounded()); // Dimension compatibility checks. // The dimension of lf should not be greater than the dimension of *this. const dimension_type lf_space_dim = lf.space_dimension(); @@ -408,7 +406,6 @@ Polyhedron::overapproximate_linear_form( " FP_Format not a floating point type."); PPL_ASSERT(lf_dimension <= store.space_dimension()); - PPL_ASSERT(store.is_bounded()); typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; @@ -422,10 +419,12 @@ Polyhedron::overapproximate_linear_form( for (dimension_type i = 0; i < lf_dimension; ++i) { Variable curr_var(i); const FP_Interval_Type& curr_coeff = lf.coefficient(curr_var); + PPL_ASSERT(curr_coeff.is_bounded()); FP_Format curr_lb = curr_coeff.lower(); FP_Format curr_ub = curr_coeff.upper(); if (curr_lb != 0 || curr_ub != 0) { const FP_Interval_Type& curr_int = store.get_interval(Variable(i)); + PPL_ASSERT(curr_int.is_bounded()); FP_Interval_Type curr_addend(curr_ub - curr_lb); curr_addend *= aux_divisor2; curr_addend *= curr_int;

1 0

[GIT] ppl/ppl(pip): Fixed bugs.
by François Galea 01 Oct '09

01 Oct '09

Module: ppl/ppl Branch: pip Commit: 150b3c6db234103b9a0ad8ea24357eb8ec5fb9e1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=150b3c6db234… Author: François Galea <francois.galea(a)uvsq.fr> Date: Thu Oct 1 16:32:23 2009 +0200 Fixed bugs. --- src/PIP_Tree.cc | 7 ++++++- src/PIP_Tree.inlines.hh | 2 +- tests/PIP_Problem/pipproblem1.cc | 2 +- 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 8da372e..08c6c83 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -430,6 +430,7 @@ PIP_Solution_Node::Rational_Matrix::scale(const Coefficient &ratio) { for (i=0; i<i_max; ++i) for (j=0; j<j_max; ++j) rows[i][j] *= ratio; + denominator *= ratio; } void @@ -941,6 +942,7 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx, gcd_assign(gcd, mult, sij); Coefficient scale_factor = sij/gcd; tableau.s.scale(scale_factor); + tableau.t.scale(scale_factor); mult *= scale_factor; } tableau.s[k][j] -= mult / sij; @@ -955,6 +957,7 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx, // Must scale matrix to stay in integer case gcd_assign(gcd, c, sij); Coefficient scale_factor = sij/gcd; + tableau.s.scale(scale_factor); tableau.t.scale(scale_factor); c *= scale_factor; } @@ -992,6 +995,7 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx, gcd_assign(gcd, c, sij); Coefficient scale_factor = sij/gcd; tableau.s.scale(scale_factor); + tableau.t.scale(scale_factor); } c /= sij; } @@ -1118,7 +1122,7 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx, if (tableau.s.is_integer() && tableau.t.is_integer()) { /* The solution is integer */ #ifdef NOISY_PIP - std::cout << "Solution found for in current node." + std::cout << "Solution found for problem in current node." << std::endl; #endif return OPTIMIZED_PIP_PROBLEM; @@ -1130,6 +1134,7 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx, std::cout << "Cut generation required." << std::endl; #endif + return OPTIMIZED_PIP_PROBLEM; } } } // Main loop of the simplex algorithm diff --git a/src/PIP_Tree.inlines.hh b/src/PIP_Tree.inlines.hh index c7f66bb..79f48c1 100644 --- a/src/PIP_Tree.inlines.hh +++ b/src/PIP_Tree.inlines.hh @@ -42,7 +42,7 @@ PIP_Solution_Node::Rational_Matrix::Rational_Matrix(dimension_type n_rows, inline PIP_Solution_Node::Rational_Matrix::Rational_Matrix(const Rational_Matrix& y) : Matrix(y), - denominator(1) { + denominator(y.denominator) { } inline bool diff --git a/tests/PIP_Problem/pipproblem1.cc b/tests/PIP_Problem/pipproblem1.cc index 4895eb8..5169f0f 100644 --- a/tests/PIP_Problem/pipproblem1.cc +++ b/tests/PIP_Problem/pipproblem1.cc @@ -105,7 +105,7 @@ test02() { cs.insert(3*j >= -2*i+8); cs.insert(j <= 4*i - 4); cs.insert(j <= m); - cs.insert(j >= 0); + //cs.insert(j >= 0); cs.insert(i <= n); PIP_Problem pip(cs.space_dimension(), cs.begin(), cs.end(), params);

1 0

[GIT] ppl/ppl(floating_point): Corrected tests with Intervals and Octagons in digitalfilters1.cc.
by Roberto Amadini 01 Oct '09

01 Oct '09

Module: ppl/ppl Branch: floating_point Commit: 60337b286bc9a9a74a835d0a83b2c729ea4fe02a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=60337b286bc9… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Thu Oct 1 15:24:59 2009 +0200 Corrected tests with Intervals and Octagons in digitalfilters1.cc. Temporarily modified tests/Floating_Point_Expression/Makefile.am Implemented Variable_Floating_Point_Expression::linear_form_assign. Inserted invariant assertions in Octagonal_Shape<T>::affine_image. --- src/Octagonal_Shape.templates.hh | 13 +- src/Variable_Floating_Point_Expression.defs.hh | 4 + src/Variable_Floating_Point_Expression.inlines.hh | 27 ++ tests/Floating_Point_Expression/Makefile.am | 5 +- tests/Floating_Point_Expression/digitalfilters1.cc | 303 +++++++------------- 5 files changed, 151 insertions(+), 201 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=60337b28…

1 0

[GIT] ppl/ppl(floating_point): Added two TODO notes.
by Fabio Bossi 01 Oct '09

01 Oct '09

Module: ppl/ppl Branch: floating_point Commit: 5e933a2295368e9fb81e9c5aee2f92c1b698c6a7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5e933a229536… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Oct 1 15:06:16 2009 +0200 Added two TODO notes. --- src/Octagonal_Shape.inlines.hh | 1 + src/Polyhedron.inlines.hh | 1 + 2 files changed, 2 insertions(+), 0 deletions(-) diff --git a/src/Octagonal_Shape.inlines.hh b/src/Octagonal_Shape.inlines.hh index 0776a7e..030ce7f 100644 --- a/src/Octagonal_Shape.inlines.hh +++ b/src/Octagonal_Shape.inlines.hh @@ -621,6 +621,7 @@ Octagonal_Shape<T>::generalized_refine_with_linear_form_inequality( const Relation_Symbol relsym) { switch (relsym) { case EQUAL: + // TODO: see if we can handle this case more efficiently. refine_with_linear_form_inequality(left, right); refine_with_linear_form_inequality(right, left); break; diff --git a/src/Polyhedron.inlines.hh b/src/Polyhedron.inlines.hh index 8005c95..861c201 100644 --- a/src/Polyhedron.inlines.hh +++ b/src/Polyhedron.inlines.hh @@ -381,6 +381,7 @@ Polyhedron::generalized_refine_with_linear_form_inequality( const Box< Interval<FP_Format, Interval_Info> >& store) { switch (relsym) { case EQUAL: + // TODO: see if we can handle this case more efficiently. refine_with_linear_form_inequality(left, right, store, false); refine_with_linear_form_inequality(right, left, store, false); break;

1 0