October 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): Do not use an abstract store: extract lower and upper bounds of variables
by Fabio Bossi 05 Oct '09

05 Oct '09

Module: ppl/ppl Branch: floating_point Commit: 531ab36b1f699617e6bd94a7c526f36431d1531e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=531ab36b1f69… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Oct 5 15:29:29 2009 +0200 Do not use an abstract store: extract lower and upper bounds of variables from the polyhedron itself instead. Fixed a bug in refine_with_linear_form_inequality that was triggered when both parameters left and right were bounded but left - right was not bounded. --- src/Polyhedron.defs.hh | 36 +++++++----------------------------- src/Polyhedron.inlines.hh | 15 +++++++-------- src/Polyhedron.templates.hh | 43 +++++++++++++++++++++++++++++++------------ 3 files changed, 45 insertions(+), 49 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=531ab36b…

1 0

[GIT] ppl/ppl(floating_point): Modified test03, test05 and test06.
by Roberto Amadini 05 Oct '09

05 Oct '09

Module: ppl/ppl Branch: floating_point Commit: e90bc74ac6035a0980bf27f37e00cd2e22a71444 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e90bc74ac603… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Mon Oct 5 15:08:27 2009 +0200 Modified test03, test05 and test06. --- src/BD_Shape.templates.hh | 1 - tests/Floating_Point_Expression/digitalfilters1.cc | 31 +++++++++++--------- 2 files changed, 17 insertions(+), 15 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index 70be7c8..e408ad0 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4282,7 +4282,6 @@ template <typename Interval_Info> void BD_Shape<T>::refine_with_linear_form_inequality( const Linear_Form< Interval<T, Interval_Info> >& left, const Linear_Form< Interval<T, Interval_Info> >& right) { - // Check that T is a floating point type. PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact, "Octagonal_Shape<T>::refine_with_linear_form_inequality:" diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index 27b15dc..bd047e4 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -21,7 +21,6 @@ For the most up-to-date information see the Parma Polyhedra Library site: http://www.cs.unipr.it/ppl/ . */ #include "ppl_test.hh" -#include <limits> namespace { @@ -272,15 +271,15 @@ test03() { "*** if (R >= D) Y = S + D; ***"); oc.upper_bound_assign(oc_begin); - Constraint_System cs(abstract_store.constraints()); + Constraint_System cs; // FIXME: It's a temporary solution, waiting for a complete // implementation of ANALYZED_FP_FORMAT. //ANALYZED_FP_FORMAT max = std::numeric_limits<ANALYZED_FP_FORMAT>::max(); PPL_DIRTY_TEMP_COEFFICIENT(M); //assign_r(M, max, ROUND_DOWN); assign_r(M, 200, ROUND_DOWN); - cs.insert(Y <= 500);//M); - cs.insert(Y >= -500);//-M); + cs.insert(Y <= M); + cs.insert(Y >= -M); oc.limited_BHMZ05_extrapolation_assign(oc_begin, cs); Box<FP_Interval> box(oc); print_constraints(box, "*** after widening ***"); @@ -366,7 +365,7 @@ test04() { "*** if (R >= D) Y = S + D; ***"); ph.upper_bound_assign(ph_begin); - Constraint_System cs(abstract_store.constraints()); + Constraint_System cs; // FIXME: It's a temporary solution, waiting for a complete // implementation of ANALYZED_FP_FORMAT. //ANALYZED_FP_FORMAT max = std::numeric_limits<ANALYZED_FP_FORMAT>::max(); @@ -475,11 +474,13 @@ test05() { print_constraints(Box<FP_Interval>(oc), "*** if (R >= D) Y = S + D; ***"); oc.upper_bound_assign(oc_begin); - Constraint_System cs(oc.constraints()); - // FIXME: Not sound, we should use ANALYZED_FP_FORMAT. - ANALYZER_FP_FORMAT max = std::numeric_limits<ANALYZER_FP_FORMAT>::max(); + Constraint_System cs; + // FIXME: It's a temporary solution, waiting for a complete + // implementation of ANALYZED_FP_FORMAT. + //ANALYZED_FP_FORMAT max = std::numeric_limits<ANALYZED_FP_FORMAT>::max(); PPL_DIRTY_TEMP_COEFFICIENT(M); - assign_r(M, max, ROUND_DOWN); + //assign_r(M, max, ROUND_DOWN); + assign_r(M, 200, ROUND_DOWN); cs.insert(Y <= M); cs.insert(Y >= -M); oc.limited_BHMZ05_extrapolation_assign(oc_begin, cs); @@ -592,10 +593,12 @@ test06() { ph.upper_bound_assign(ph_begin); Constraint_System cs; - // FIXME: This is not sound, it should use ANALYZED_FP_FORMAT - ANALYZER_FP_FORMAT max = std::numeric_limits<ANALYZER_FP_FORMAT>::max(); + // FIXME: It's a temporary solution, waiting for a complete + // implementation of ANALYZED_FP_FORMAT. + //ANALYZED_FP_FORMAT max = std::numeric_limits<ANALYZED_FP_FORMAT>::max(); PPL_DIRTY_TEMP_COEFFICIENT(M); - assign_r(M, max, ROUND_DOWN); + //assign_r(M, max, ROUND_DOWN); + assign_r(M, 200, ROUND_DOWN); cs.insert(Y <= M); cs.insert(Y >= -M); ph.limited_BHRZ03_extrapolation_assign(ph_begin, cs); @@ -615,6 +618,6 @@ BEGIN_MAIN DO_TEST(test02); DO_TEST(test03); DO_TEST(test04); - //DO_TEST(test05); - //DO_TEST(test06); + DO_TEST(test05); + DO_TEST(test06); END_MAIN

1 0

[GIT] ppl/ppl(pip): Added code for selection of the deepest cut.
by François Galea 05 Oct '09

05 Oct '09

Module: ppl/ppl Branch: pip Commit: 90400149d3e368041a6b6bd2e01e1455e0d0c4a8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=90400149d3e3… Author: François Galea <francois.galea(a)uvsq.fr> Date: Mon Oct 5 08:46:45 2009 +0200 Added code for selection of the deepest cut. --- src/PIP_Tree.cc | 22 +++++++++++++++++++++- 1 files changed, 21 insertions(+), 1 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 0e7c211..bb47121 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -1213,11 +1213,32 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx, } else { /* The solution is non-integer. We have to generate a cut. */ + Coefficient mod; + /* Look for row which will generate the "deepest" cut */ + Coefficient score; + Coefficient best = 0; + dimension_type best_i = i; + for (i_ = i; i_ < num_rows; ++i_) { + const Row& row = tableau.t[i_]; + score = 0; + for (j = 0; j < num_params; ++j) { + mod_assign(mod, row[j], d); + if (mod != 0) + score += d - mod; + } + if (score > best) { + best = score; + best_i = i_; + } + } + i = best_i; + #ifdef NOISY_PIP std::cout << "Row " << i << " contains non-integer coefficients. " << "Cut generation required." << std::endl; #endif + tableau.t.add_zero_columns(1); tableau.s.add_zero_rows(1, Row::Flags()); tableau.t.add_zero_rows(1, Row::Flags()); @@ -1227,7 +1248,6 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx, const Row& row_t = tableau.t[i]; Linear_Expression e; Variables_Set::const_iterator p; - Coefficient mod; mod_assign(mod, row_t[0], d); if (mod != 0) e += (d-mod);

1 0

[GIT] ppl/ppl(pip): Implemented cut generation. Not stable yet.
by François Galea 05 Oct '09

05 Oct '09

Module: ppl/ppl Branch: pip Commit: 11dea7cc6e76b78d9276da8fbb3045f1d2c06378 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=11dea7cc6e76… Author: François Galea <francois.galea(a)uvsq.fr> Date: Sun Oct 4 18:41:13 2009 +0200 Implemented cut generation. Not stable yet. --- src/PIP_Tree.cc | 210 +++++++++++++++++++++++++++++++------- src/PIP_Tree.defs.hh | 45 +++++++- src/PIP_Tree.inlines.hh | 10 ++ tests/PIP_Problem/pipproblem1.cc | 38 ++++++-- 4 files changed, 255 insertions(+), 48 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=11dea7cc…

1 0

[GIT] ppl/ppl(pip): Added test problem.
by François Galea 05 Oct '09

05 Oct '09

Module: ppl/ppl Branch: pip Commit: 74cf01fdacb0218ad144420a370c875b4d3f2f6d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=74cf01fdacb0… Author: François Galea <francois.galea(a)uvsq.fr> Date: Sun Oct 4 12:09:57 2009 +0200 Added test problem. --- tests/PIP_Problem/pipproblem1.cc | 23 +++++++++++++++++++++++ 1 files changed, 23 insertions(+), 0 deletions(-) diff --git a/tests/PIP_Problem/pipproblem1.cc b/tests/PIP_Problem/pipproblem1.cc index 5169f0f..b29f062 100644 --- a/tests/PIP_Problem/pipproblem1.cc +++ b/tests/PIP_Problem/pipproblem1.cc @@ -114,6 +114,28 @@ test02() { if (ok) { const PIP_Tree solution = pip.solution(); display_solution(solution, Variables_Set(i, j)); + +bool +test03() { + Variable i(0); + Variable j(1); + Variable k(2); + Variable m(3); + Variable n(4); + Variables_Set params(k, n); + + Constraint_System cs; + cs.insert(i <= m); + cs.insert(j <= n); + cs.insert(2*i+j <= 2*m+n-k); + cs.insert(2*i+j >= 2*m+n-k); + + PIP_Problem pip(cs.space_dimension(), cs.begin(), cs.end(), params); + + bool ok = (pip.solve() == OPTIMIZED_PIP_PROBLEM); + if (ok) { + const PIP_Tree solution = pip.solution(); + display_solution(solution, params, Variables_Set(i, j)); } return ok; @@ -124,4 +146,5 @@ test02() { BEGIN_MAIN DO_TEST(test01); DO_TEST(test02); + DO_TEST(test03); END_MAIN

1 0

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

04 Oct '09

Module: ppl/ppl Branch: floating_point Commit: a0f084e697e6f17780d18ffa96e80a254d5e7620 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a0f084e697e6… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Sun Oct 4 21:39:47 2009 +0200 Modified test01, test02, test03 and test04. --- tests/Floating_Point_Expression/digitalfilters1.cc | 77 ++++++++++++++------ 1 files changed, 55 insertions(+), 22 deletions(-) diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index 937e50e..27b15dc 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -21,6 +21,7 @@ For the most up-to-date information see the Parma Polyhedra Library site: http://www.cs.unipr.it/ppl/ . */ #include "ppl_test.hh" +#include <limits> namespace { @@ -73,7 +74,7 @@ test01() { nout << "*** n = " << n << " ***" << endl; as_begin = abstract_store; - //X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X; + // X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X; tmp.lower() = -128; tmp.upper() = 128; abstract_store.set_interval(X, tmp); @@ -84,7 +85,7 @@ test01() { abstract_store.affine_image(R, X - S); abstract_store.affine_image(Y, X); - //if (R <= -D) Y = S - D; + // if (R <= -D) Y = S - D; FP_Interval_Abstract_Store as_then(abstract_store); as_then.refine_with_constraint(R <= -D); as_then.affine_image(Y, S - D); @@ -92,7 +93,7 @@ test01() { abstract_store.upper_bound_assign(as_then); print_constraints(abstract_store ,"*** if (R <= -D) Y = S - D; ***"); - //if (R >= D) Y = S + D; + // if (R >= D) Y = S + D; as_then = abstract_store; as_then.refine_with_constraint(R >= D); as_then.affine_image(Y, S + D); @@ -103,8 +104,16 @@ test01() { print_constraints(abstract_store ,"*** if (R >= D) Y = S + D; ***"); abstract_store.upper_bound_assign(as_begin); - Constraint_System cs(abstract_store.constraints()); - abstract_store.widening_assign(as_begin); + Constraint_System cs; + // FIXME: It's a temporary solution, waiting for a complete + // implementation of ANALYZED_FP_FORMAT. + //ANALYZED_FP_FORMAT max = std::numeric_limits<ANALYZED_FP_FORMAT>::max(); + PPL_DIRTY_TEMP_COEFFICIENT(M); + //assign_r(M, max, ROUND_DOWN); + assign_r(M, 200, ROUND_DOWN); + cs.insert(Y <= M); + cs.insert(Y >= -M); + abstract_store.limited_CC76_extrapolation_assign(as_begin, cs); Box<FP_Interval> box(abstract_store); print_constraints(box, "*** after widening ***"); tmp = box.get_interval(Y); @@ -142,7 +151,7 @@ test02() { nout << "*** n = " << n << " ***" << endl; bd_begin = bd; - //X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X; + // 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)); @@ -153,7 +162,7 @@ test02() { bd.affine_image(R, FP_Linear_Form(X - S)); bd.affine_image(Y, FP_Linear_Form(X)); - //if (R <= -D) Y = S - D; + // 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)); @@ -165,7 +174,7 @@ test02() { print_constraints(Box<FP_Interval>(bd) , "*** if (R <= -D) Y = S - D; ***"); - //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)); @@ -179,8 +188,16 @@ test02() { "*** if (R >= D) Y = S + D; ***"); bd.upper_bound_assign(bd_begin); - Constraint_System cs(bd.constraints()); - bd.widening_assign(bd_begin); + Constraint_System cs(abstract_store.constraints()); + // FIXME: It's a temporary solution, waiting for a complete + // implementation of ANALYZED_FP_FORMAT. + //ANALYZED_FP_FORMAT max = std::numeric_limits<ANALYZED_FP_FORMAT>::max(); + PPL_DIRTY_TEMP_COEFFICIENT(M); + //assign_r(M, max, ROUND_DOWN); + assign_r(M, 200, ROUND_DOWN); + cs.insert(Y <= M); + cs.insert(Y >= -M); + bd.limited_BHMZ05_extrapolation_assign(bd_begin, cs); Box<FP_Interval> box(bd); print_constraints(box, "*** after widening ***"); tmp = box.get_interval(Y); @@ -255,7 +272,15 @@ test03() { "*** if (R >= D) Y = S + D; ***"); oc.upper_bound_assign(oc_begin); - Constraint_System cs(oc.constraints()); + Constraint_System cs(abstract_store.constraints()); + // FIXME: It's a temporary solution, waiting for a complete + // implementation of ANALYZED_FP_FORMAT. + //ANALYZED_FP_FORMAT max = std::numeric_limits<ANALYZED_FP_FORMAT>::max(); + PPL_DIRTY_TEMP_COEFFICIENT(M); + //assign_r(M, max, ROUND_DOWN); + assign_r(M, 200, ROUND_DOWN); + cs.insert(Y <= 500);//M); + cs.insert(Y >= -500);//-M); oc.limited_BHMZ05_extrapolation_assign(oc_begin, cs); Box<FP_Interval> box(oc); print_constraints(box, "*** after widening ***"); @@ -294,7 +319,7 @@ test04() { nout << "*** n = " << n << " ***" << endl; ph_begin = ph; - //X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X; + // 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); @@ -308,7 +333,7 @@ test04() { abstract_store = Box<FP_Interval>(ph); ph.affine_image(Y, FP_Linear_Form(X), abstract_store); - //if (R <= -D) Y = S - D; + // 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), @@ -324,7 +349,7 @@ test04() { print_constraints(Box<FP_Interval>(ph) , "*** if (R <= -D) Y = S - D; ***"); - //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), @@ -341,7 +366,15 @@ test04() { "*** if (R >= D) Y = S + D; ***"); ph.upper_bound_assign(ph_begin); - Constraint_System cs(ph.constraints()); + Constraint_System cs(abstract_store.constraints()); + // FIXME: It's a temporary solution, waiting for a complete + // implementation of ANALYZED_FP_FORMAT. + //ANALYZED_FP_FORMAT max = std::numeric_limits<ANALYZED_FP_FORMAT>::max(); + PPL_DIRTY_TEMP_COEFFICIENT(M); + //assign_r(M, max, ROUND_DOWN); + assign_r(M, 200, ROUND_DOWN); + cs.insert(Y <= M); + cs.insert(Y >= -M); ph.limited_BHRZ03_extrapolation_assign(ph_begin, cs); Box<FP_Interval> box(ph); print_constraints(box, "*** after widening ***"); @@ -410,7 +443,7 @@ test05() { var_x.linearize(abstract_store, lf_abstract_store, lx); oc.affine_image(Y, lx); - //if (R <= -D) Y = S - D; + // if (R <= -D) Y = S - D; FP_Octagonal_Shape oc_then(oc); oc_then.refine_with_linear_form_inequality(lr, -lk); @@ -426,7 +459,7 @@ test05() { print_constraints(Box<FP_Interval>(oc) , "*** if (R <= -D) Y = S - D; ***"); - //if (R >= D) Y = S + D; + // if (R >= D) Y = S + D; oc_then = oc; oc_then.refine_with_linear_form_inequality(lk, lr); @@ -443,7 +476,7 @@ test05() { oc.upper_bound_assign(oc_begin); Constraint_System cs(oc.constraints()); - // FIXME: not sound. + // FIXME: Not sound, we should use ANALYZED_FP_FORMAT. ANALYZER_FP_FORMAT max = std::numeric_limits<ANALYZER_FP_FORMAT>::max(); PPL_DIRTY_TEMP_COEFFICIENT(M); assign_r(M, max, ROUND_DOWN); @@ -496,7 +529,7 @@ test06() { nout << "*** n = " << n << " ***" << endl; ph_begin = ph; - //X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X; + // X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X; Con_FP_Expression con_x(-128, 128); con_x.linearize(abstract_store, lf_abstract_store, lk); ph.affine_image(X, lk, abstract_store); @@ -522,7 +555,7 @@ test06() { var_x.linearize(abstract_store, lf_abstract_store, lx); ph.affine_image(Y, lx, abstract_store); - //if (R <= -D) Y = S - D; + // 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(lr, -lk, as_then); @@ -539,7 +572,7 @@ test06() { print_constraints(Box<FP_Interval>(ph) , "*** if (R <= -D) Y = S - D; ***"); - //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(lk, lr, as_then); @@ -559,7 +592,7 @@ test06() { ph.upper_bound_assign(ph_begin); Constraint_System cs; - // FIXME: not sound. + // FIXME: This is not sound, it should use ANALYZED_FP_FORMAT ANALYZER_FP_FORMAT max = std::numeric_limits<ANALYZER_FP_FORMAT>::max(); PPL_DIRTY_TEMP_COEFFICIENT(M); assign_r(M, max, ROUND_DOWN);

1 0

[GIT] ppl/ppl(floating_point): Added widening and extrapolation operators in test01, test02,
by Roberto Amadini 03 Oct '09

03 Oct '09

Module: ppl/ppl Branch: floating_point Commit: 4b736b1ec4842142b5f18c61e59a6795db3dab6d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4b736b1ec484… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Sat Oct 3 21:05:04 2009 +0200 Added widening and extrapolation operators in test01, test02, test03 and test04. --- tests/Floating_Point_Expression/digitalfilters1.cc | 162 ++++++++++++-------- 1 files changed, 101 insertions(+), 61 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=4b736b1e…

1 0

[GIT] ppl/ppl(floating_point): Fixed comments.
by Roberto Amadini 03 Oct '09

03 Oct '09

Module: ppl/ppl Branch: floating_point Commit: 112fb00917eba78c9dd2213f098f11a76e71b249 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=112fb00917eb… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Sat Oct 3 14:37:44 2009 +0200 Fixed comments. --- tests/Floating_Point_Expression/digitalfilters1.cc | 122 +++++++++++++------- 1 files changed, 81 insertions(+), 41 deletions(-) diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index 636bea9..9e20d71 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -46,14 +46,21 @@ for (n = 0; n < N; ++n) { } */ -// tests rate limiter using intervals abstract domain. +// tests rate limiter using intervals abstract domain +// and ignoring rounding errors. bool test01() { - Variable X(0); //input - Variable D(1); //input - Variable Y(2); //output - Variable S(3); //last output - Variable R(4); //actual rate + //input signal + Variable X(0); + //maximum allowed for |R| + Variable D(1); + //output signal + Variable Y(2); + //last output + Variable S(3); + //actual rate + Variable R(4); + FP_Interval_Abstract_Store abstract_store(5); FP_Interval tmp(0); FP_Interval_Abstract_Store as_begin; @@ -61,8 +68,8 @@ test01() { // Y = 0; abstract_store.set_interval(Y, tmp); - unsigned int N = 5; - for(unsigned int n = 0; n < N; ++n) { + unsigned short N = 5; + for(unsigned short n = 0; n < N; ++n) { nout << "*** n = " << n << " ***" << endl; as_begin = abstract_store; @@ -104,14 +111,21 @@ test01() { return tmp.is_bounded(); } -// tests rate limiter using bounded differences abstract domain. +// tests rate limiter using bounded differences abstract domain +// and ignoring rounding errors. bool test02() { - Variable X(0); //input - Variable D(1); //input - Variable Y(2); //output - Variable S(3); //last output - Variable R(4); //actual rate + //input signal + Variable X(0); + //maximum allowed for |R| + Variable D(1); + //output signal + Variable Y(2); + //last output + Variable S(3); + //actual rate + Variable R(4); + FP_Interval_Abstract_Store abstract_store(5); FP_BD_Shape bd(abstract_store); FP_Interval tmp(0); @@ -120,7 +134,7 @@ test02() { // Y = 0; bd.affine_image(Y, FP_Linear_Form(tmp)); - for(unsigned int n = 0; n < 5; ++n) { + for(unsigned short n = 0; n < 5; ++n) { nout << "*** n = " << n << " ***" << endl; bd_begin = bd; @@ -166,14 +180,21 @@ test02() { return tmp.is_bounded(); } -// tests rate limiter using octagons abstract domain. +// tests rate limiter using octagons abstract domain +// and ignoring rounding errors. bool test03() { - Variable X(0); //input - Variable D(1); //input - Variable Y(2); //output - Variable S(3); //last output - Variable R(4); //actual rate + //input signal + Variable X(0); + //maximum allowed for |R| + Variable D(1); + //output signal + Variable Y(2); + //last output + Variable S(3); + //actual rate + Variable R(4); + FP_Interval_Abstract_Store abstract_store(5); FP_Octagonal_Shape oc(abstract_store); FP_Interval tmp(0); @@ -182,7 +203,7 @@ test03() { // Y = 0; oc.affine_image(Y, FP_Linear_Form(tmp)); - for(unsigned int n = 0; oc_begin != oc; ++n) { + for(unsigned short n = 0; oc_begin != oc; ++n) { nout << "*** n = " << n << " ***" << endl; oc_begin = oc; @@ -230,14 +251,21 @@ test03() { return tmp.is_bounded(); } -// tests rate limiter using polyhedra abstract domain. +// tests rate limiter using polyhedra abstract domain +// and ignoring rounding errors. bool test04() { - Variable X(0); //input - Variable D(1); //input - Variable Y(2); //output - Variable S(3); //last output - Variable R(4); //actual rate + //input signal + Variable X(0); + //maximum allowed for |R| + Variable D(1); + //output signal + Variable Y(2); + //last output + Variable S(3); + //actual rate + Variable R(4); + FP_Interval_Abstract_Store abstract_store(5); NNC_Polyhedron ph(abstract_store); FP_Interval tmp(0); @@ -246,7 +274,7 @@ test04() { // Y = 0; ph.affine_image(Y, FP_Linear_Form(tmp), abstract_store); - for(unsigned int n = 0; ph_begin != ph; ++n) { + for(unsigned short n = 0; ph_begin != ph; ++n) { nout << "*** n = " << n << " ***" << endl; ph_begin = ph; @@ -307,11 +335,17 @@ test04() { // 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 + //input signal + Variable X(0); + //maximum allowed for |R| + Variable D(1); + //output signal + Variable Y(2); + //last output + Variable S(3); + //actual rate + Variable R(4); + FP_Interval_Abstract_Store abstract_store(5); FP_Linear_Form_Abstract_Store lf_abstract_store; FP_Octagonal_Shape oc(abstract_store); @@ -330,7 +364,7 @@ test05() { FP_Interval threshold(-144); threshold.join_assign(144); - for(unsigned int n = 0; !tmp.contains(threshold); ++n) { + for(unsigned short n = 0; n < 10 /* !tmp.contains(threshold) */; ++n) { nout << "*** n = " << n << " ***" << endl; oc_begin = oc; @@ -399,11 +433,17 @@ test05() { // linearization of floating point expressions. bool test06() { - Variable X(0); //input - Variable D(1); //input - Variable Y(2); //output - Variable S(3); //last output - Variable R(4); //actual rate + //input signal + Variable X(0); + //maximum allowed for |R| + Variable D(1); + //output signal + Variable Y(2); + //last output + Variable S(3); + //actual rate + Variable R(4); + FP_Interval_Abstract_Store abstract_store(5); FP_Linear_Form_Abstract_Store lf_abstract_store; NNC_Polyhedron ph(abstract_store); @@ -423,7 +463,7 @@ test06() { FP_Interval threshold(-144); threshold.join_assign(144); - for(unsigned int n = 0; !tmp.contains(threshold); ++n) { + for(unsigned short n = 0; !tmp.contains(threshold); ++n) { nout << "*** n = " << n << " ***" << endl; ph_begin = ph;

1 0

[GIT] ppl/w3ppl(master): Completed BagnaraHZ09TCS.
by Roberto Bagnara 03 Oct '09

03 Oct '09

Module: ppl/w3ppl Branch: master Commit: 913755bfd4892a4a8e40dcd7b915376683e7ed83 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=913755bfd4… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Oct 3 09:00:57 2009 +0200 Completed BagnaraHZ09TCS. --- htdocs/Documentation/ppl.bib | 1 + 1 files changed, 1 insertions(+), 0 deletions(-) diff --git a/htdocs/Documentation/ppl.bib b/htdocs/Documentation/ppl.bib index 80ff5e3..e3bcf0d 100644 --- a/htdocs/Documentation/ppl.bib +++ b/htdocs/Documentation/ppl.bib @@ -913,6 +913,7 @@ Journal = "Theoretical Computer Science", Volume = 410, Number = 46, + Pages = "4672--4691", Publisher = "Elsevier", Year = 2009, Abstract = "Convex polyhedra are the basis for several abstractions

1 0

[GIT] ppl/ppl(floating_point): Implemented a test on polyhedra abstract domain with linearization
by Roberto Amadini 02 Oct '09

02 Oct '09

Module: ppl/ppl Branch: floating_point Commit: 7d2306abb07146aadaeb9a2fc6468550a4212b47 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7d2306abb071… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Fri Oct 2 18:56:19 2009 +0200 Implemented a test on polyhedra abstract domain with linearization of floating point expressions. --- tests/Floating_Point_Expression/digitalfilters1.cc | 110 +++++++++++++++++++- 1 files changed, 105 insertions(+), 5 deletions(-) diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index bc77d19..636bea9 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -326,10 +326,11 @@ test05() { // 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) { + FP_Interval threshold(-144); + threshold.join_assign(144); + + for(unsigned int n = 0; !tmp.contains(threshold); ++n) { nout << "*** n = " << n << " ***" << endl; oc_begin = oc; @@ -390,8 +391,106 @@ test05() { 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(); +} + +// tests rate limiter using polyhedra abstract domain and +// linearization of floating point expressions. +bool +test06() { + 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; + NNC_Polyhedron ph(abstract_store); + FP_Interval tmp(0); + NNC_Polyhedron ph_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); + ph.affine_image(Y, lk, abstract_store); + + //FIXME: Can the threshold be more precise than [-144, 144]? + FP_Interval threshold(-144); + threshold.join_assign(144); + + for(unsigned int n = 0; !tmp.contains(threshold); ++n) { + + nout << "*** n = " << n << " ***" << endl; + ph_begin = ph; + + //X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X; + Con_FP_Expression con_x(-128, 128); + con_x.linearize(abstract_store, lf_abstract_store, lk); + ph.affine_image(X, lk, abstract_store); + + Con_FP_Expression con_d(0, 16); + con_d.linearize(abstract_store, lf_abstract_store, lk); + ph.affine_image(D, lk, abstract_store); + + Var_FP_Expression var_y(2); + abstract_store = Box<FP_Interval>(ph); + var_y.linearize(abstract_store, lf_abstract_store, ly); + ph.affine_image(S, ly, abstract_store); + + 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); + abstract_store = Box<FP_Interval>(ph); + x_dif_s.linearize(abstract_store, lf_abstract_store, lr); + ph.affine_image(R, lr, abstract_store); + + Var_FP_Expression var_x(0); + abstract_store = Box<FP_Interval>(ph); + var_x.linearize(abstract_store, lf_abstract_store, lx); + ph.affine_image(Y, lx, 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(lr, -lk, as_then); + 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); + ph_then.affine_image(Y, ly, abstract_store); + + ph.refine_with_linear_form_inequality(-lk, lr, 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(lk, lr, as_then); + + 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); + ph_then.affine_image(Y, ly, as_then); + + ph.refine_with_linear_form_inequality(lr, lk, abstract_store); + + ph.upper_bound_assign(ph_then); + Box<FP_Interval> box(ph); + abstract_store.upper_bound_assign(as_then); + print_constraints(box, "*** if (R >= D) Y = S + D; ***"); + tmp = box.get_interval(Y); + } + nout << "*** Y in " << tmp << " ***" << endl; return tmp.is_bounded(); } @@ -404,4 +503,5 @@ BEGIN_MAIN DO_TEST(test03); DO_TEST(test04); DO_TEST(test05); + DO_TEST(test06); END_MAIN

2 1