July 2010 - PPL-devel - BUGSENG Mailman

Problems with test suite on alpha
by Michael Tautschnig 09 Sep '10

09 Sep '10

Hi PPL developers, I've reported problems with some test cases because of suspected gcc bugs on alpha earlier already. Now it seems that even more test cases are broken, most probably because of the very same bug (I suspect it to be http://gcc.gnu.org/bugzilla/show_bug.cgi?id=8966). My question now is: How to proceed? Shall I specifically disable the failing test cases by surrounding them with an #ifndef __alpha__ or disable the entire test suite on alpha? Thanks, Michael

2 6

[GIT] ppl/ppl(floating_point): Rewritten test06 and test07.
by Fabio Bossi 31 Jul '10

31 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 17105335ca1841766bd314c9275649e87475e931 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=17105335ca18… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Sat Jul 31 16:08:03 2010 +0200 Rewritten test06 and test07. --- tests/Concrete_Expression/digitalfilters1.cc | 442 +++++++++++++++++++++++++- 1 files changed, 440 insertions(+), 2 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=17105335…

1 0

[GIT] ppl/ppl(floating_point): Do not perform interval analysis on an assignment
by Fabio Bossi 31 Jul '10

31 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 41ec2a4972b2682d0237880e2c3f5f2df238bb5c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=41ec2a4972b2… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Sat Jul 31 15:39:01 2010 +0200 Do not perform interval analysis on an assignment before linearization. --- tests/Concrete_Expression/digitalfilters1.cc | 379 ++------------------------ 1 files changed, 17 insertions(+), 362 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=41ec2a49…

1 0

[GIT] ppl/ppl(floating_point): Float:
by Fabio Bossi 31 Jul '10

31 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 1c9679165d7d9719426ed316f6b26dcaace36b58 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1c9679165d7d… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Sat Jul 31 12:53:20 2010 +0200 Float: Added a few functions that operate on linear form abstract stores. linearize.cc: test05 now consistently utilizes linear form abstract stores. --- src/Float.defs.hh | 32 ++++++++++++++ src/Float.inlines.hh | 14 ++++++ src/Float.templates.hh | 52 +++++++++++++++++++++++ tests/Concrete_Expression/digitalfilters1.cc | 57 ++++++++++++++++++++----- 4 files changed, 143 insertions(+), 12 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=1c967916…

1 0

[GIT] ppl/ppl(floating_point): Rewritten test05 ( still lacks proper use of the linear
by Fabio Bossi 30 Jul '10

30 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 3b3495a1556330ec9ae4cf72c00398db01a10c46 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3b3495a15563… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Fri Jul 30 19:21:33 2010 +0200 Rewritten test05 (still lacks proper use of the linear form abstract store). --- tests/Concrete_Expression/digitalfilters1.cc | 87 +++++++++++++------------- 1 files changed, 44 insertions(+), 43 deletions(-) diff --git a/tests/Concrete_Expression/digitalfilters1.cc b/tests/Concrete_Expression/digitalfilters1.cc index 204ef54..75deac5 100644 --- a/tests/Concrete_Expression/digitalfilters1.cc +++ b/tests/Concrete_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 "C_Expr.defs.hh" namespace { @@ -423,7 +424,7 @@ test04() { return (tmp.lower() == -128 && tmp.upper() == 128); } -/* + // Tests rate limiter using bounded differences and linearization of // floating point expressions. // In order to improve the analysis, the interval domain is used @@ -459,23 +460,22 @@ test05() { cs.insert(Y <= M); cs.insert(Y >= -M); - Con_FP_Expression con_y("0"); + Floating_Point_Constant<C_Expr> con_y("0", 2); // The constant floating point expression con_y is linearized into // the interval linear form lk. If linearization succeeded, we model // the assignment Y = 0, invoking affine_form_image method. - // FIXME: In order to refine the analysis, all the transer function are + // In order to refine the analysis, all the transer function are // performed in parallel in the interval domain and in the bounded // differences domain. // Then, we consider the intersection between these abstract domains. interval_store.affine_form_image(Y, FP_Linear_Form(tmp)); - if (con_y.linearize(interval_store, lf_abstract_store, lk)) + if (linearize(con_y, interval_store, lf_abstract_store, lk)) bd.affine_form_image(Y, lk); else - bd.affine_form_image(Y, FP_Linear_Form(interval_store.get_interval(Y))); + bd.intersection_assign(FP_BD_Shape(interval_store)); interval_store.intersection_assign(FP_Interval_Abstract_Store(bd)); - // This loop iterate until a fixed point is reached. do { @@ -489,74 +489,73 @@ test05() { tmp.lower() = -128; tmp.upper() = 128; interval_store.affine_form_image(X, FP_Linear_Form(tmp)); - Con_FP_Expression con_x(-128, 128); - if (con_x.linearize(interval_store, lf_abstract_store, lk)) - bd.affine_form_image(X, lk); - else - bd.affine_form_image(X, FP_Linear_Form(interval_store.get_interval(X))); + bd.affine_form_image(X, FP_Linear_Form(tmp)); interval_store.intersection_assign(FP_Interval_Abstract_Store(bd)); // D = [0, 16]; tmp.lower() = 0; tmp.upper() = 16; interval_store.affine_form_image(D, FP_Linear_Form(tmp)); - Con_FP_Expression con_d(0, 16); - if (con_d.linearize(interval_store, lf_abstract_store, lk)) - bd.affine_form_image(D, lk); - else - bd.affine_form_image(D, FP_Linear_Form(interval_store.get_interval(D))); + bd.affine_form_image(D, FP_Linear_Form(tmp)); interval_store.intersection_assign(FP_Interval_Abstract_Store(bd)); // S = Y; interval_store.affine_form_image(S, FP_Linear_Form(Y)); - Var_FP_Expression var_y(Y.id()); - if (var_y.linearize(interval_store, lf_abstract_store, ly)) + Approximable_Reference<C_Expr> var_y(FP_Type, Int_Interval(mpz_class(0)), + Y.id()); + if (linearize(var_y, interval_store, lf_abstract_store, ly)) bd.affine_form_image(S, ly); else - bd.affine_form_image(S, FP_Linear_Form(interval_store.get_interval(S))); + bd.intersection_assign(FP_BD_Shape(interval_store)); interval_store.intersection_assign(FP_Interval_Abstract_Store(bd)); // R = X - S; - Var_FP_Expression* px = new Var_FP_Expression(X.id()); - Var_FP_Expression* ps = new Var_FP_Expression(S.id()); - Dif_FP_Expression x_dif_s(px, ps); + Approximable_Reference<C_Expr> px(FP_Type, Int_Interval(mpz_class(0)), + X.id()); + Approximable_Reference<C_Expr> ps(FP_Type, Int_Interval(mpz_class(0)), + S.id()); + Binary_Operator<C_Expr> x_dif_s(FP_Type, Binary_Operator<C_Expr>::SUB, + &px, &ps); interval_store.affine_form_image(R, FP_Linear_Form(X - S)); - if (x_dif_s.linearize(interval_store, lf_abstract_store, lr)) + if (linearize(x_dif_s, interval_store, lf_abstract_store, lr)) bd.affine_form_image(R, lr); else - bd.affine_form_image(R, FP_Linear_Form(interval_store.get_interval(R))); + bd.intersection_assign(FP_BD_Shape(interval_store)); interval_store.intersection_assign(FP_Interval_Abstract_Store(bd)); // Y = X; - Var_FP_Expression var_x(X.id()); interval_store.affine_form_image(Y, FP_Linear_Form(X)); - if (var_x.linearize(interval_store, lf_abstract_store, lx)) + if (linearize(px, interval_store, lf_abstract_store, lx)) bd.affine_form_image(Y, lx); else - bd.affine_form_image(Y, FP_Linear_Form(interval_store.get_interval(Y))); + bd.intersection_assign(FP_BD_Shape(interval_store)); interval_store.intersection_assign(FP_Interval_Abstract_Store(bd)); // if (R <= -D) FP_BD_Shape bd_then(bd); FP_Interval_Abstract_Store is_then(interval_store); is_then.refine_with_constraint(R <= -D); - bd_then.refine_with_linear_form_inequality(lr, -lk); + bd_then.refine_with_linear_form_inequality(FP_Linear_Form(R), + -FP_Linear_Form(D)); is_then.intersection_assign(FP_Interval_Abstract_Store(bd_then)); // then Y = S - D; - Var_FP_Expression* pd = new Var_FP_Expression(D.id()); - Var_FP_Expression* ps2 = new Var_FP_Expression(S.id()); - Dif_FP_Expression s_dif_d(ps2, pd); + Approximable_Reference<C_Expr> pd(FP_Type, Int_Interval(mpz_class(0)), + D.id()); + Binary_Operator<C_Expr> s_dif_d(FP_Type, Binary_Operator<C_Expr>::SUB, + &ps, &pd); is_then.affine_form_image(Y, FP_Linear_Form(S - D)); - if (s_dif_d.linearize(is_then, lf_abstract_store, ly)) + if (linearize(s_dif_d, is_then, lf_abstract_store, ly)) bd_then.affine_form_image(Y, ly); else - bd_then.affine_form_image(Y, FP_Linear_Form(is_then.get_interval(Y))); + bd_then.intersection_assign(FP_BD_Shape(is_then)); is_then.intersection_assign(FP_Interval_Abstract_Store(bd_then)); // else skip; interval_store.refine_with_constraint(R > -D); - bd.refine_with_linear_form_inequality(-lk, lr); + bd.refine_with_linear_form_inequality(-FP_Linear_Form(D), + FP_Linear_Form(R)); + bd.intersection_assign(FP_BD_Shape(interval_store)); interval_store.intersection_assign(FP_Interval_Abstract_Store(bd)); // LUB between then and else branches. @@ -568,22 +567,23 @@ test05() { bd_then = bd; is_then = interval_store; is_then.refine_with_constraint(R >= D); - bd_then.refine_with_linear_form_inequality(lk, lr); + bd_then.refine_with_linear_form_inequality(FP_Linear_Form(D), + FP_Linear_Form(R)); is_then.intersection_assign(FP_Interval_Abstract_Store(bd_then)); // then Y = S + D; - Var_FP_Expression* pd1 = new Var_FP_Expression(D.id()); - Var_FP_Expression* ps3 = new Var_FP_Expression(S.id()); - Sum_FP_Expression s_sum_d(ps3, pd1); + Binary_Operator<C_Expr> s_sum_d(FP_Type, Binary_Operator<C_Expr>::ADD, + &ps, &pd); is_then.affine_form_image(Y, FP_Linear_Form(S + D)); - if (s_sum_d.linearize(is_then, lf_abstract_store, ly)) + if (linearize(s_sum_d, is_then, lf_abstract_store, ly)) bd_then.affine_form_image(Y, ly); else - bd_then.affine_form_image(Y, FP_Linear_Form(is_then.get_interval(Y))); + bd_then.intersection_assign(FP_BD_Shape(is_then)); is_then.intersection_assign(FP_Interval_Abstract_Store(bd_then)); // else skip; - bd.refine_with_linear_form_inequality(lr, lk); + bd.refine_with_linear_form_inequality(FP_Linear_Form(R), + FP_Linear_Form(D)); interval_store.refine_with_constraint(R < D); bd.intersection_assign(FP_BD_Shape(interval_store)); interval_store.intersection_assign(FP_Interval_Abstract_Store(bd)); @@ -612,7 +612,7 @@ test05() { return (tmp.lower() == -144 && tmp.upper() == 144); } - +/* // Tests rate limiter using octagonal shapes and linearization of // floating point expressions. // In order to improve the analysis, the interval domain is used @@ -990,7 +990,7 @@ BEGIN_MAIN DO_TEST_F8(test02); DO_TEST_F8(test03); DO_TEST_F64A(test04); -/* + #define COND_float PPL_CPP_EQ(PPL_CPP_FP_FORMAT(ANALYZER_FP_FORMAT), 1) #define COND_double PPL_CPP_EQ(PPL_CPP_FP_FORMAT(ANALYZER_FP_FORMAT), 2) #define COND_float_or_double PPL_CPP_OR(COND_float, COND_double) @@ -1002,6 +1002,7 @@ BEGIN_MAIN PPL_CPP_OR(COND_F64, PPL_CPP_OR(PPL_CUSTOM_COND_32, PPL_CUSTOM_COND_64)) COND_DO_TEST(PPL_CUSTOM_COND, test05); +/* COND_DO_TEST(PPL_CUSTOM_COND, test06); DO_TEST_F64(test07);

1 0

[GIT] ppl/ppl(floating_point): Started rewriting tests on digital filters.
by Fabio Bossi 30 Jul '10

30 Jul '10

Module: ppl/ppl Branch: floating_point Commit: e85af354adc157725146aa506a6dc2f9507407e4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e85af354adc1… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Fri Jul 30 17:54:02 2010 +0200 Started rewriting tests on digital filters. --- tests/Concrete_Expression/Makefile.am | 2 +- tests/Concrete_Expression/digitalfilters1.cc | 13 ++++++++++--- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/tests/Concrete_Expression/Makefile.am b/tests/Concrete_Expression/Makefile.am index 3c64827..dd5983f 100644 --- a/tests/Concrete_Expression/Makefile.am +++ b/tests/Concrete_Expression/Makefile.am @@ -52,11 +52,11 @@ $(top_builddir)/src/libppl.la \ ORIGINAL_TESTS = \ C_Expr \ +digitalfilters1 \ linearform1 \ linearize #bdshape1 \ #bdshape2 \ -#digitalfilters1 \ #floatingpointexpr1 \ #octagonalshape1 \ #octagonalshape2 \ diff --git a/tests/Concrete_Expression/digitalfilters1.cc b/tests/Concrete_Expression/digitalfilters1.cc index 41c6229..204ef54 100644 --- a/tests/Concrete_Expression/digitalfilters1.cc +++ b/tests/Concrete_Expression/digitalfilters1.cc @@ -25,6 +25,10 @@ site: http://www.cs.unipr.it/ppl/ . */ namespace { using namespace Parma_Polyhedra_Library::IO_Operators; +Concrete_Expression_Type FP_Type = + Concrete_Expression_Type::floating_point(ANALYZED_FP_FORMAT); + +typedef Integer_Interval_Type Int_Interval; /* This file tests a rate limiter that, given random input flows of floating @@ -105,7 +109,7 @@ test01() { // D = [0, 16]; tmp.lower() = 0; tmp.upper() = 16; - abstract_store.affine_form_image(X, FP_Linear_Form(tmp)); + abstract_store.affine_form_image(D, FP_Linear_Form(tmp)); // S = Y; abstract_store.affine_form_image(S, FP_Linear_Form(Y)); @@ -193,7 +197,7 @@ test02() { tmp.upper() = 16; abstract_store.affine_form_image(D, FP_Linear_Form(tmp)); - // S = tmp; + // S = Y; abstract_store.affine_form_image(S, FP_Linear_Form(Y)); // R = X - S; @@ -419,6 +423,7 @@ test04() { return (tmp.lower() == -128 && tmp.upper() == 128); } +/* // Tests rate limiter using bounded differences and linearization of // floating point expressions. // In order to improve the analysis, the interval domain is used @@ -976,6 +981,7 @@ test07() { nout << "*** Y in " << tmp << " ***" << endl; return (tmp.lower() == -144 && tmp.upper() == 144); } +*/ } // namespace @@ -984,7 +990,7 @@ BEGIN_MAIN DO_TEST_F8(test02); DO_TEST_F8(test03); DO_TEST_F64A(test04); - +/* #define COND_float PPL_CPP_EQ(PPL_CPP_FP_FORMAT(ANALYZER_FP_FORMAT), 1) #define COND_double PPL_CPP_EQ(PPL_CPP_FP_FORMAT(ANALYZER_FP_FORMAT), 2) #define COND_float_or_double PPL_CPP_OR(COND_float, COND_double) @@ -999,4 +1005,5 @@ BEGIN_MAIN COND_DO_TEST(PPL_CUSTOM_COND, test06); DO_TEST_F64(test07); +*/ END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Do not add errors after rounding to a less precise format.
by Fabio Bossi 30 Jul '10

30 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 8cfeaf81d2f501d2040e6af07815763173d7357c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8cfeaf81d2f5… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Fri Jul 30 17:04:16 2010 +0200 Do not add errors after rounding to a less precise format. --- src/Float.defs.hh | 6 ++++++ src/linearize.hh | 5 +++-- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/src/Float.defs.hh b/src/Float.defs.hh index 75d2c2b..219e7d3 100644 --- a/src/Float.defs.hh +++ b/src/Float.defs.hh @@ -58,6 +58,7 @@ struct float_ieee754_half { static const int EXPONENT_MIN = -EXPONENT_MAX + 1; static const int EXPONENT_MIN_DENORM = EXPONENT_MIN - static_cast<int>(MANTISSA_BITS); + static const Floating_Point_Format floating_point_format = IEEE754_HALF; int is_inf() const; int is_nan() const; int is_zero() const; @@ -90,6 +91,7 @@ struct float_ieee754_single { static const int EXPONENT_MIN = -EXPONENT_MAX + 1; static const int EXPONENT_MIN_DENORM = EXPONENT_MIN - static_cast<int>(MANTISSA_BITS); + static const Floating_Point_Format floating_point_format = IEEE754_SINGLE; int is_inf() const; int is_nan() const; int is_zero() const; @@ -135,6 +137,7 @@ struct float_ieee754_double { static const int EXPONENT_MIN = -EXPONENT_MAX + 1; static const int EXPONENT_MIN_DENORM = EXPONENT_MIN - static_cast<int>(MANTISSA_BITS); + static const Floating_Point_Format floating_point_format = IEEE754_DOUBLE; int is_inf() const; int is_nan() const; int is_zero() const; @@ -166,6 +169,7 @@ struct float_ibm_single { static const int EXPONENT_MIN = -EXPONENT_MAX + 1; static const int EXPONENT_MIN_DENORM = EXPONENT_MIN - static_cast<int>(MANTISSA_BITS); + static const Floating_Point_Format floating_point_format = IBM_SINGLE; int is_inf() const; int is_nan() const; int is_zero() const; @@ -217,6 +221,8 @@ struct float_intel_double_extended { static const int EXPONENT_MIN = -EXPONENT_MAX + 1; static const int EXPONENT_MIN_DENORM = EXPONENT_MIN - static_cast<int>(MANTISSA_BITS); + static const Floating_Point_Format floating_point_format = + INTEL_DOUBLE_EXTENDED; int is_inf() const; int is_nan() const; int is_zero() const; diff --git a/src/linearize.hh b/src/linearize.hh index 0093586..d21e5cb 100644 --- a/src/linearize.hh +++ b/src/linearize.hh @@ -629,8 +629,9 @@ cast_linearize(const Cast_Operator<Target>& cast_expr, } else { result = FP_Linear_Form(FP_Interval_Type(cast_arg->get_integer_interval())); - /* FIXME: we can avoid adding errors if FP_Interval_Type::boundary_type - is less precise than analyzed_format. */ + if (is_less_precise_than(Float<analyzer_format>::Binary::floating_point_format, analyzed_format)) + // We are rounding to a less precise format. Do not add errors. + return true; } FP_Linear_Form rel_error;

1 0

[GIT] ppl/ppl(master): Moved two methods in the right place.
by Abramo Bagnara 30 Jul '10

30 Jul '10

Module: ppl/ppl Branch: master Commit: afcafb8e2d3c9a8c1da3ac005d86e66819e22059 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=afcafb8e2d3c… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri Jul 30 16:35:04 2010 +0200 Moved two methods in the right place. --- src/Interval.defs.hh | 46 +-------------------------------------- src/Interval.templates.hh | 52 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 54 insertions(+), 44 deletions(-) diff --git a/src/Interval.defs.hh b/src/Interval.defs.hh index ac6ce24..e751eb7 100644 --- a/src/Interval.defs.hh +++ b/src/Interval.defs.hh @@ -296,28 +296,7 @@ public: template <typename C> typename Enable_If<Is_Same_Or_Derived<I_Constraint_Base, C>::value, I_Result>::type - lower_extend(const C& c) { - PPL_ASSERT(OK()); - bool open; - switch (c.rel()) { - case V_LGE: - return lower_extend(); - case V_NAN: - return I_NOT_EMPTY | I_EXACT | I_UNCHANGED; - case V_GT: - open = true; - break; - case V_GE: - case V_EQ: - open = false; - break; - default: - PPL_ASSERT(false); - } - min_assign(LOWER, lower(), info(), LOWER, c.value(), f_info(c.value(), open)); - PPL_ASSERT(OK()); - return I_ANY; - } + lower_extend(const C& c); I_Result upper_extend() { info().clear_boundary_properties(UPPER); @@ -327,28 +306,7 @@ public: template <typename C> typename Enable_If<Is_Same_Or_Derived<I_Constraint_Base, C>::value, I_Result>::type - upper_extend(const C& c) { - PPL_ASSERT(OK()); - bool open; - switch (c.rel()) { - case V_LGE: - return lower_extend(); - case V_NAN: - return I_NOT_EMPTY | I_EXACT | I_UNCHANGED; - case V_LT: - open = true; - break; - case V_LE: - case V_EQ: - open = false; - break; - default: - PPL_ASSERT(false); - } - max_assign(UPPER, upper(), info(), UPPER, c.value(), f_info(c.value(), open)); - PPL_ASSERT(OK()); - return I_ANY; - } + upper_extend(const C& c); I_Result build() { return assign(UNIVERSE); diff --git a/src/Interval.templates.hh b/src/Interval.templates.hh index 0c17b64..456458e 100644 --- a/src/Interval.templates.hh +++ b/src/Interval.templates.hh @@ -28,6 +28,58 @@ site: http://www.cs.unipr.it/ppl/ . */ namespace Parma_Polyhedra_Library { template <typename Boundary, typename Info> +template <typename C> +typename Enable_If<Is_Same_Or_Derived<I_Constraint_Base, C>::value, I_Result>::type +Interval<Boundary, Info>::lower_extend(const C& c) { + PPL_ASSERT(OK()); + bool open; + switch (c.rel()) { + case V_LGE: + return lower_extend(); + case V_NAN: + return I_NOT_EMPTY | I_EXACT | I_UNCHANGED; + case V_GT: + open = true; + break; + case V_GE: + case V_EQ: + open = false; + break; + default: + PPL_ASSERT(false); + } + min_assign(LOWER, lower(), info(), LOWER, c.value(), f_info(c.value(), open)); + PPL_ASSERT(OK()); + return I_ANY; +} + +template <typename Boundary, typename Info> +template <typename C> +typename Enable_If<Is_Same_Or_Derived<I_Constraint_Base, C>::value, I_Result>::type +Interval<Boundary, Info>::upper_extend(const C& c) { + PPL_ASSERT(OK()); + bool open; + switch (c.rel()) { + case V_LGE: + return lower_extend(); + case V_NAN: + return I_NOT_EMPTY | I_EXACT | I_UNCHANGED; + case V_LT: + open = true; + break; + case V_LE: + case V_EQ: + open = false; + break; + default: + PPL_ASSERT(false); + } + max_assign(UPPER, upper(), info(), UPPER, c.value(), f_info(c.value(), open)); + PPL_ASSERT(OK()); + return I_ANY; +} + +template <typename Boundary, typename Info> template <typename From, typename Iterator> typename Enable_If<Is_Interval<From>::value, void>::type Interval<Boundary, Info>::CC76_widening_assign(const From& y,

1 0

[GIT] ppl/ppl(floating_point): Avoid adding errors when casting to a more precise
by Fabio Bossi 30 Jul '10

30 Jul '10

Module: ppl/ppl Branch: floating_point Commit: a69cc00cdd67f30135df670f9ebb4b2061c9fb35 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a69cc00cdd67… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Fri Jul 30 16:04:19 2010 +0200 Avoid adding errors when casting to a more precise floating point format. --- src/Float.defs.hh | 6 ++++++ src/Float.inlines.hh | 6 +++++- src/linearize.hh | 13 ++++++++++--- 3 files changed, 21 insertions(+), 4 deletions(-) diff --git a/src/Float.defs.hh b/src/Float.defs.hh index e484458..75d2c2b 100644 --- a/src/Float.defs.hh +++ b/src/Float.defs.hh @@ -361,6 +361,12 @@ public: #endif /*! \brief + Returns <CODE>true</CODE> if and only if there is some floating point + number that is representable by \p f2 but not by \p f1. +*/ +bool is_less_precise_than(Floating_Point_Format f1, Floating_Point_Format f2); + +/*! \brief Computes the absolute error of floating point computations. \par Template type parameters diff --git a/src/Float.inlines.hh b/src/Float.inlines.hh index 16e0f21..13692b8 100644 --- a/src/Float.inlines.hh +++ b/src/Float.inlines.hh @@ -444,6 +444,11 @@ float_ieee754_quad::build(bool negative, mpz_t mantissa, int exponent) { << (MANTISSA_BITS - 64); } +inline bool +is_less_precise_than(Floating_Point_Format f1, Floating_Point_Format f2) { + return f1 < f2; +} + #if PPL_SUPPORTED_FLOAT inline Float<float>::Float() { @@ -492,7 +497,6 @@ Float<long double>::value() { } #endif - } // namespace Parma_Polyhedra_Library #endif // !defined(PPL_Float_inlines_hh) diff --git a/src/linearize.hh b/src/linearize.hh index a4f131d..0093586 100644 --- a/src/linearize.hh +++ b/src/linearize.hh @@ -616,16 +616,23 @@ cast_linearize(const Cast_Operator<Target>& cast_expr, typedef Box<FP_Interval_Type> FP_Interval_Abstract_Store; typedef std::map<dimension_type, FP_Linear_Form> FP_Linear_Form_Abstract_Store; + Floating_Point_Format analyzed_format = + cast_expr.type().floating_point_format(); const Concrete_Expression<Target>* cast_arg = cast_expr.argument(); if (cast_arg->type().is_floating_point()) { if (!linearize(*cast_arg, int_store, lf_store, result)) return false; + if (!is_less_precise_than(analyzed_format, + cast_arg->type().floating_point_format())) + // We are casting to a more precise format. Do not add errors. + return true; } - else + else { result = FP_Linear_Form(FP_Interval_Type(cast_arg->get_integer_interval())); + /* FIXME: we can avoid adding errors if FP_Interval_Type::boundary_type + is less precise than analyzed_format. */ + } - Floating_Point_Format analyzed_format = - cast_expr.type().floating_point_format(); FP_Linear_Form rel_error; result.relative_error(analyzed_format, rel_error); result += rel_error;

1 0

[GIT] ppl/ppl(floating_point): Removed a test file.
by Fabio Bossi 30 Jul '10

30 Jul '10

Module: ppl/ppl Branch: floating_point Commit: fcb542b0c0c0beca4216ece67163b0013ec2b61d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fcb542b0c0c0… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Fri Jul 30 10:49:47 2010 +0200 Removed a test file. --- tests/Concrete_Expression/Makefile.am | 3 -- tests/Concrete_Expression/float.cc | 44 --------------------------------- 2 files changed, 0 insertions(+), 47 deletions(-) diff --git a/tests/Concrete_Expression/Makefile.am b/tests/Concrete_Expression/Makefile.am index ead3d19..3c64827 100644 --- a/tests/Concrete_Expression/Makefile.am +++ b/tests/Concrete_Expression/Makefile.am @@ -52,7 +52,6 @@ $(top_builddir)/src/libppl.la \ ORIGINAL_TESTS = \ C_Expr \ -float \ linearform1 \ linearize #bdshape1 \ @@ -140,8 +139,6 @@ bdshape2_SOURCES = bdshape2.cc digitalfilters1_SOURCES = digitalfilters1.cc -float_SOURCES = float.cc - floatingpointexpr1_SOURCES = floatingpointexpr1.cc linearform1_SOURCES = linearform1.cc diff --git a/tests/Concrete_Expression/float.cc b/tests/Concrete_Expression/float.cc deleted file mode 100644 index 7506993..0000000 --- a/tests/Concrete_Expression/float.cc +++ /dev/null @@ -1,44 +0,0 @@ -/* Test function compute_absolute_error. - Copyright (C) 2001-2010 Roberto Bagnara <bagnara(a)cs.unipr.it> - -This file is part of the Parma Polyhedra Library (PPL). - -The PPL is free software; you can redistribute it and/or modify it -under the terms of the GNU General Public License as published by the -Free Software Foundation; either version 3 of the License, or (at your -option) any later version. - -The PPL is distributed in the hope that it will be useful, but WITHOUT -ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or -FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License -for more details. - -You should have received a copy of the GNU General Public License -along with this program; if not, write to the Free Software Foundation, -Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. - -For the most up-to-date information see the Parma Polyhedra Library -site: http://www.cs.unipr.it/ppl/ . */ - -#include "ppl_test.hh" - -namespace { - -using namespace Parma_Polyhedra_Library::IO_Operators; - -bool -test01() { - std::cout << compute_absolute_error<FP_Interval>(ANALYZED_FP_FORMAT) << - std::endl; - - std::cout << compute_absolute_error<FP_Interval>(ANALYZED_FP_FORMAT) << - std::endl; - - return 1; -} - -} - -BEGIN_MAIN - DO_TEST(test01); -END_MAIN

1 0