October 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(pip): Fixed bug in compatiblity_check().
by François Galea 06 Oct '09

06 Oct '09

Module: ppl/ppl Branch: pip Commit: 0d0b02fa391aeeaac40981792d56abe9e563cef2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0d0b02fa391a… Author: François Galea <francois.galea(a)uvsq.fr> Date: Tue Oct 6 10:52:35 2009 +0200 Fixed bug in compatiblity_check(). --- src/PIP_Tree.cc | 22 +++++++++++++--------- 1 files changed, 13 insertions(+), 9 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index bb47121..f2866e7 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -636,7 +636,7 @@ bool PIP_Solution_Node::compatibility_check(const Matrix &ctx, const Row &cnst) { Matrix s(ctx); s.add_row(cnst); - dimension_type i, j, k, j_; + dimension_type i, j, k, j_, j__; dimension_type num_rows = s.num_rows(); dimension_type num_cols = s.num_columns(); bool result = false; @@ -664,38 +664,42 @@ PIP_Solution_Node::compatibility_check(const Matrix &ctx, const Row &cnst) { break; } // Perform a pivot operation on the matrix - const Coefficient &sij = p[j]; + const Coefficient& sij = p[j]; for (j_=0; j_<num_cols; ++j_) { if (j_ == j) continue; - const Coefficient &sij_ = p[j_]; + const Coefficient& sij_ = p[j_]; for (k=0; k<num_rows; ++k) { if (k == i) continue; - Coefficient mult = s[k][j] * sij_; + Row& row = s[k]; + Coefficient mult = row[j] * sij_; if (mult % sij != 0) { // Must scale row to stay in integer case Coefficient gcd; gcd_assign(gcd, mult, sij); Coefficient scale_factor = sij/gcd; - add_assign(s[k], s[k], scale_factor); + for (j__=0; j__<num_cols; ++j__) + row[j__] *= scale_factor; mult *= scale_factor; } - s[k][j_] -= mult / sij; + row[j_] -= mult / sij; } s[i][j_] = 0; } for (k=0; k<num_rows; ++k) { - Coefficient skj = s[k][j]; + Row& row = s[k]; + Coefficient& skj = row[j]; if (skj % sij != 0) { // as above, we must perform row scaling Coefficient gcd; gcd_assign(gcd, skj, sij); Coefficient scale_factor = sij/gcd; - add_assign(s[k], s[k], scale_factor); + for (j__=0; j__<num_cols; ++j__) + row[j__] *= scale_factor; skj *= scale_factor; } - s[k][j] = skj/sij; + skj /= sij; } }

1 0

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

06 Oct '09

Module: ppl/ppl Branch: floating_point Commit: f77babe87a9d40dfb248bc5c3f15a736feb217a9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f77babe87a9d… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Tue Oct 6 01:22:33 2009 +0200 Fixed test03. --- tests/Floating_Point_Expression/digitalfilters1.cc | 15 +++++++++------ 1 files changed, 9 insertions(+), 6 deletions(-) diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index 141cdff..5c3a4fd 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -216,7 +216,6 @@ test02() { // tests rate limiter using octagons abstract domain // and ignoring rounding errors. -// FIXME: Not pass at the moment, bool test03() { // Input signal. @@ -282,6 +281,7 @@ test03() { oc.upper_bound_assign(oc_begin); Constraint_System cs; PPL_DIRTY_TEMP_COEFFICIENT(M); + PPL_DIRTY_TEMP_COEFFICIENT(N); ANALYZER_FP_FORMAT max_analyzed = (2 - pow(2, -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS))) @@ -291,10 +291,13 @@ test03() { std::numeric_limits<ANALYZER_FP_FORMAT>::max(); max_analyzer = std::min(max_analyzer, max_analyzed); assign_r(M, max_analyzer, ROUND_DOWN); - cs.insert(Y <= M); - cs.insert(Y >= -M); - //Octagonal_Shape<float> oc1(cs); - //print_constraints(oc1, "*** oc1 ***"); + div_2exp_assign_r(N, M, 1, ROUND_DOWN); + // FIXME: By inserting the constraints Y <= M and Y >= -M, we obtain + // Y + Y <= 2 * M = +inf and -Y - Y <= -2 * M = +inf. + // For a more precise analysis, it is better to insert the + // constraints Y <= N and Y >= -N, where N = M / 2. + cs.insert(Y <= N); + cs.insert(Y >= -N); oc.limited_BHMZ05_extrapolation_assign(oc_begin, cs); Box<FP_Interval> box(oc); print_constraints(box, "*** after widening ***"); @@ -638,7 +641,7 @@ test06() { BEGIN_MAIN DO_TEST(test01); DO_TEST(test02); - //DO_TEST(test03); + DO_TEST(test03); DO_TEST(test04); //DO_TEST(test05); //DO_TEST(test06);

1 0

[GIT] ppl/ppl(floating_point): Computed the largest non-infinity number in digitalfilters1.cc
by Roberto Amadini 06 Oct '09

06 Oct '09

Module: ppl/ppl Branch: floating_point Commit: eda13a1edf15b0f6a21f0a853a68b6a9b7979d7c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=eda13a1edf15… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Tue Oct 6 00:34:52 2009 +0200 Computed the largest non-infinity number in digitalfilters1.cc Fixed a bug in Float.defs.hh --- src/Float.defs.hh | 2 +- tests/Floating_Point_Expression/digitalfilters1.cc | 95 ++++++++++++-------- 2 files changed, 59 insertions(+), 38 deletions(-) diff --git a/src/Float.defs.hh b/src/Float.defs.hh index 41b9f83..3f65b2b 100644 --- a/src/Float.defs.hh +++ b/src/Float.defs.hh @@ -303,7 +303,7 @@ public: template <> class Float<long double> : public True { public: -#if PPL_CXX_LONG_BINARY_FORMAT == PPL_FLOAT_IEEE754_HALF +#if PPL_CXX_LONG_DOUBLE_BINARY_FORMAT == PPL_FLOAT_IEEE754_HALF typedef float_ieee754_half Binary; #elif PPL_CXX_LONG_DOUBLE_BINARY_FORMAT == PPL_FLOAT_IEEE754_SINGLE typedef float_ieee754_single Binary; diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index b778e38..141cdff 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -104,13 +104,16 @@ test01() { abstract_store.upper_bound_assign(as_begin); Constraint_System cs; - // FIXME: It's a temporary solution, waiting for a complete - // implementation of ANALYZED_FP_FORMAT. PPL_DIRTY_TEMP_COEFFICIENT(M); - ANALYZED_FP_FORMAT max; - max.set_max(false); - //assign_r(M, max, ROUND_DOWN); - assign_r(M, 200, ROUND_DOWN); + ANALYZER_FP_FORMAT max_analyzed = + (2 - pow(2, + -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS))) + * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS) + - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2); + ANALYZER_FP_FORMAT max_analyzer = + std::numeric_limits<ANALYZER_FP_FORMAT>::max(); + max_analyzer = std::min(max_analyzer, max_analyzed); + assign_r(M, max_analyzer, ROUND_DOWN); cs.insert(Y <= M); cs.insert(Y >= -M); abstract_store.limited_CC76_extrapolation_assign(as_begin, cs); @@ -189,13 +192,16 @@ test02() { bd.upper_bound_assign(bd_begin); Constraint_System cs; - // FIXME: It's a temporary solution, waiting for a complete - // implementation of ANALYZED_FP_FORMAT. PPL_DIRTY_TEMP_COEFFICIENT(M); - ANALYZED_FP_FORMAT max; - max.set_max(false); - //assign_r(M, max, ROUND_DOWN); - assign_r(M, 200, ROUND_DOWN); + ANALYZER_FP_FORMAT max_analyzed = + (2 - pow(2, + -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS))) + * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS) + - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2); + ANALYZER_FP_FORMAT max_analyzer = + std::numeric_limits<ANALYZER_FP_FORMAT>::max(); + max_analyzer = std::min(max_analyzer, max_analyzed); + assign_r(M, max_analyzer, ROUND_DOWN); cs.insert(Y <= M); cs.insert(Y >= -M); bd.limited_BHMZ05_extrapolation_assign(bd_begin, cs); @@ -210,6 +216,7 @@ test02() { // tests rate limiter using octagons abstract domain // and ignoring rounding errors. +// FIXME: Not pass at the moment, bool test03() { // Input signal. @@ -274,15 +281,20 @@ test03() { oc.upper_bound_assign(oc_begin); Constraint_System cs; - // FIXME: It's a temporary solution, waiting for a complete - // implementation of ANALYZED_FP_FORMAT. PPL_DIRTY_TEMP_COEFFICIENT(M); - ANALYZED_FP_FORMAT max; - max.set_max(false); - //assign_r(M, max, ROUND_DOWN); - assign_r(M, 200, ROUND_DOWN); + ANALYZER_FP_FORMAT max_analyzed = + (2 - pow(2, + -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS))) + * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS) + - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2); + ANALYZER_FP_FORMAT max_analyzer = + std::numeric_limits<ANALYZER_FP_FORMAT>::max(); + max_analyzer = std::min(max_analyzer, max_analyzed); + assign_r(M, max_analyzer, ROUND_DOWN); cs.insert(Y <= M); cs.insert(Y >= -M); + //Octagonal_Shape<float> oc1(cs); + //print_constraints(oc1, "*** oc1 ***"); oc.limited_BHMZ05_extrapolation_assign(oc_begin, cs); Box<FP_Interval> box(oc); print_constraints(box, "*** after widening ***"); @@ -365,13 +377,16 @@ test04() { ph.upper_bound_assign(ph_begin); Constraint_System cs; - // FIXME: It's a temporary solution, waiting for a complete - // implementation of ANALYZED_FP_FORMAT. PPL_DIRTY_TEMP_COEFFICIENT(M); - ANALYZED_FP_FORMAT max; - max.set_max(false); - //assign_r(M, max, ROUND_DOWN); - assign_r(M, 200, ROUND_DOWN); + ANALYZER_FP_FORMAT max_analyzed = + (2 - pow(2, + -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS))) + * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS) + - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2); + ANALYZER_FP_FORMAT max_analyzer = + std::numeric_limits<ANALYZER_FP_FORMAT>::max(); + max_analyzer = std::min(max_analyzer, max_analyzed); + assign_r(M, max_analyzer, ROUND_DOWN); cs.insert(Y <= M); cs.insert(Y >= -M); ph.limited_BHRZ03_extrapolation_assign(ph_begin, cs); @@ -475,13 +490,16 @@ test05() { oc.upper_bound_assign(oc_begin); Constraint_System cs; - // FIXME: It's a temporary solution, waiting for a complete - // implementation of ANALYZED_FP_FORMAT. PPL_DIRTY_TEMP_COEFFICIENT(M); - ANALYZED_FP_FORMAT max; - max.set_max(false); - //assign_r(M, max, ROUND_DOWN); - assign_r(M, 200, ROUND_DOWN); + ANALYZER_FP_FORMAT max_analyzed = + (2 - pow(2, + -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS))) + * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS) + - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2); + ANALYZER_FP_FORMAT max_analyzer = + std::numeric_limits<ANALYZER_FP_FORMAT>::max(); + max_analyzer = std::min(max_analyzer, max_analyzed); + assign_r(M, max_analyzer, ROUND_DOWN); cs.insert(Y <= M); cs.insert(Y >= -M); oc.limited_BHMZ05_extrapolation_assign(oc_begin, cs); @@ -593,13 +611,16 @@ test06() { ph.upper_bound_assign(ph_begin); Constraint_System cs; - // FIXME: It's a temporary solution, waiting for a complete - // implementation of ANALYZED_FP_FORMAT. PPL_DIRTY_TEMP_COEFFICIENT(M); - ANALYZED_FP_FORMAT max; - max.set_max(false); - //assign_r(M, max, ROUND_DOWN); - assign_r(M, 200, ROUND_DOWN); + ANALYZER_FP_FORMAT max_analyzed = + (2 - pow(2, + -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS))) + * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS) + - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2); + ANALYZER_FP_FORMAT max_analyzer = + std::numeric_limits<ANALYZER_FP_FORMAT>::max(); + max_analyzer = std::min(max_analyzer, max_analyzed); + assign_r(M, max_analyzer, ROUND_DOWN); cs.insert(Y <= M); cs.insert(Y >= -M); ph.limited_BHRZ03_extrapolation_assign(ph_begin, cs); @@ -617,7 +638,7 @@ test06() { BEGIN_MAIN DO_TEST(test01); DO_TEST(test02); - DO_TEST(test03); + //DO_TEST(test03); DO_TEST(test04); //DO_TEST(test05); //DO_TEST(test06);

1 0

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

05 Oct '09

Module: ppl/ppl Branch: floating_point Commit: 32a8e23b60707354fb5c8393b6ccc640976382b1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=32a8e23b6070… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Mon Oct 5 17:53:37 2009 +0200 Removed comments. --- tests/Floating_Point_Expression/digitalfilters1.cc | 30 ++++++++----------- 1 files changed, 13 insertions(+), 17 deletions(-) diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index 1e47843..b778e38 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -106,8 +106,9 @@ test01() { 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); + ANALYZED_FP_FORMAT max; + max.set_max(false); //assign_r(M, max, ROUND_DOWN); assign_r(M, 200, ROUND_DOWN); cs.insert(Y <= M); @@ -187,11 +188,12 @@ test02() { "*** if (R >= D) Y = S + D; ***"); bd.upper_bound_assign(bd_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); + ANALYZED_FP_FORMAT max; + max.set_max(false); //assign_r(M, max, ROUND_DOWN); assign_r(M, 200, ROUND_DOWN); cs.insert(Y <= M); @@ -274,8 +276,9 @@ test03() { 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); + ANALYZED_FP_FORMAT max; + max.set_max(false); //assign_r(M, max, ROUND_DOWN); assign_r(M, 200, ROUND_DOWN); cs.insert(Y <= M); @@ -364,8 +367,9 @@ test04() { 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); + ANALYZED_FP_FORMAT max; + max.set_max(false); //assign_r(M, max, ROUND_DOWN); assign_r(M, 200, ROUND_DOWN); cs.insert(Y <= M); @@ -473,8 +477,9 @@ test05() { 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); + ANALYZED_FP_FORMAT max; + max.set_max(false); //assign_r(M, max, ROUND_DOWN); assign_r(M, 200, ROUND_DOWN); cs.insert(Y <= M); @@ -590,22 +595,13 @@ test06() { 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); + ANALYZED_FP_FORMAT max; + max.set_max(false); //assign_r(M, max, ROUND_DOWN); assign_r(M, 200, ROUND_DOWN); cs.insert(Y <= M); cs.insert(Y >= -M); - // FIXME: not sound. - // ANALYZED_FP_FORMAT max = std::numeric_limits<ANALYZED_FP_FORMAT>::max(); - // NOTE: std::max() not correct, try use following solution. - // ANALYZED_FP_FORMAT max; - // max.set_max(false); - //PPL_DIRTY_TEMP_COEFFICIENT(M); - //assign_r(M, max, 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 ***");

1 0

[GIT] ppl/ppl(floating_point): Minor changes.
by Fabio Biselli 05 Oct '09

05 Oct '09

Module: ppl/ppl Branch: floating_point Commit: c05f09104471cd518f40b822cfb4066bb2e65925 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c05f09104471… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Mon Oct 5 19:09:24 2009 +0200 Minor changes. --- tests/Floating_Point_Expression/digitalfilters1.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index 3deda9f..1e47843 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -605,7 +605,7 @@ test06() { //assign_r(M, max, 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 ***");

1 0

[GIT] ppl/ppl(floating_point): Extended float_ieee754_half format.
by Fabio Biselli 05 Oct '09

05 Oct '09

Module: ppl/ppl Branch: floating_point Commit: 8847a837fb858259f80990b984956d8a34689ed7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8847a837fb85… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Mon Oct 5 16:34:35 2009 +0200 Extended float_ieee754_half format. Fixed a function call in test06 with a possible solution. --- src/Float.defs.hh | 35 +++++++++++-- src/Float.inlines.hh | 58 ++++++++++++++++++++ tests/Floating_Point_Expression/digitalfilters1.cc | 10 ++++ 3 files changed, 99 insertions(+), 4 deletions(-) diff --git a/src/Float.defs.hh b/src/Float.defs.hh index 6586e0e..41b9f83 100644 --- a/src/Float.defs.hh +++ b/src/Float.defs.hh @@ -42,9 +42,30 @@ namespace Parma_Polyhedra_Library { #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) struct float_ieee754_half { + uint32_t word; + static const uint32_t SGN_MASK = 0x8000; + static const uint32_t EXP_MASK = 0xfc00; + static const uint32_t POS_INF = 0xfc00; + static const uint32_t NEG_INF = 0x7c00; + static const uint32_t POS_ZERO = 0x0000; + static const uint32_t NEG_ZERO = 0x8000; static const unsigned int EXPONENT_BITS = 5; static const unsigned int MANTISSA_BITS = 10; - static const int EXPONENT_BIAS = 15; + static const int EXPONENT_MAX = (1 << (EXPONENT_BITS - 1)) - 1; + static const int EXPONENT_BIAS = EXPONENT_MAX; + static const int EXPONENT_MIN = -EXPONENT_MAX + 1; + static const int EXPONENT_MIN_DENORM = EXPONENT_MIN + - static_cast<int>(MANTISSA_BITS); + int is_inf() const; + int is_nan() const; + int is_zero() const; + int sign_bit() const; + void negate(); + void dec(); + void inc(); + void set_max(bool negative); + void build(bool negative, mpz_t mantissa, int exponent); + }; #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS @@ -228,7 +249,9 @@ class Float : public False { }; template <> class Float<float> : public True { public: -#if PPL_CXX_FLOAT_BINARY_FORMAT == PPL_FLOAT_IEEE754_SINGLE +#if PPL_CXX_FLOAT_BINARY_FORMAT == PPL_FLOAT_IEEE754_HALF + typedef float_ieee754_half Binary; +#elif PPL_CXX_FLOAT_BINARY_FORMAT == PPL_FLOAT_IEEE754_SINGLE typedef float_ieee754_single Binary; #elif PPL_CXX_FLOAT_BINARY_FORMAT == PPL_FLOAT_IEEE754_DOUBLE typedef float_ieee754_double Binary; @@ -253,7 +276,9 @@ public: template <> class Float<double> : public True { public: -#if PPL_CXX_DOUBLE_BINARY_FORMAT == PPL_FLOAT_IEEE754_SINGLE +#if PPL_CXX_DOUBLE_BINARY_FORMAT == PPL_FLOAT_IEEE754_HALF + typedef float_ieee754_half Binary; +#elif PPL_CXX_DOUBLE_BINARY_FORMAT == PPL_FLOAT_IEEE754_SINGLE typedef float_ieee754_single Binary; #elif PPL_CXX_DOUBLE_BINARY_FORMAT == PPL_FLOAT_IEEE754_DOUBLE typedef float_ieee754_double Binary; @@ -278,7 +303,9 @@ public: template <> class Float<long double> : public True { public: -#if PPL_CXX_LONG_DOUBLE_BINARY_FORMAT == PPL_FLOAT_IEEE754_SINGLE +#if PPL_CXX_LONG_BINARY_FORMAT == PPL_FLOAT_IEEE754_HALF + typedef float_ieee754_half Binary; +#elif PPL_CXX_LONG_DOUBLE_BINARY_FORMAT == PPL_FLOAT_IEEE754_SINGLE typedef float_ieee754_single Binary; #elif PPL_CXX_LONG_DOUBLE_BINARY_FORMAT == PPL_FLOAT_IEEE754_DOUBLE typedef float_ieee754_double Binary; diff --git a/src/Float.inlines.hh b/src/Float.inlines.hh index 2796f9e..dcbe93f 100644 --- a/src/Float.inlines.hh +++ b/src/Float.inlines.hh @@ -26,6 +26,64 @@ site: http://www.cs.unipr.it/ppl/ . */ #include <climits> namespace Parma_Polyhedra_Library { + +inline int +float_ieee754_half::is_inf() const { + if (word == NEG_INF) + return -1; + if (word == POS_INF) + return 1; + return 0; +} + +inline int +float_ieee754_half::is_nan() const { + return (word & ~SGN_MASK) > POS_INF; +} + +inline int +float_ieee754_half::is_zero() const { + if (word == NEG_ZERO) + return -1; + if (word == POS_ZERO) + return 1; + return 0; +} + +inline void +float_ieee754_half::negate() { + word ^= SGN_MASK; +} + +inline int +float_ieee754_half::sign_bit() const { + return !!(word & SGN_MASK); +} + +inline void +float_ieee754_half::dec() { + --word; +} + +inline void +float_ieee754_half::inc() { + ++word; +} + +inline void +float_ieee754_half::set_max(bool negative) { + word = 0x7bff; + if (negative) + word |= SGN_MASK; +} + +inline void +float_ieee754_half::build(bool negative, mpz_t mantissa, int exponent) { + word = mpz_get_ui(mantissa) & ((1UL << MANTISSA_BITS) - 1); + if (negative) + word |= SGN_MASK; + word |= static_cast<uint32_t>(exponent + EXPONENT_BIAS) << MANTISSA_BITS; +} inline int float_ieee754_single::is_inf() const { diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index fccd823..3deda9f 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -596,6 +596,16 @@ test06() { assign_r(M, 200, ROUND_DOWN); cs.insert(Y <= M); cs.insert(Y >= -M); + // FIXME: not sound. + // ANALYZED_FP_FORMAT max = std::numeric_limits<ANALYZED_FP_FORMAT>::max(); + // NOTE: std::max() not correct, try use following solution. + // ANALYZED_FP_FORMAT max; + // max.set_max(false); + //PPL_DIRTY_TEMP_COEFFICIENT(M); + //assign_r(M, max, 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 ***");

1 0

[GIT] ppl/ppl(floating_point): Removed few comments.
by Fabio Biselli 05 Oct '09

05 Oct '09

Module: ppl/ppl Branch: floating_point Commit: c83d68a8f97fbd008a49e5eabc4c950db1eaa208 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c83d68a8f97f… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Sun Oct 4 12:09:35 2009 +0200 Removed few comments. --- src/BD_Shape.templates.hh | 14 ++++---------- 1 files changed, 4 insertions(+), 10 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index e408ad0..202135b 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4340,9 +4340,6 @@ void BD_Shape<T>::refine_with_linear_form_inequality( 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 - // shorten it at the expense of a bit of efficiency. - if (left_t == 0) { if (right_t == 0) { // The constraint involves constants only. Ignore it: it is up to @@ -4366,11 +4363,10 @@ void BD_Shape<T>::refine_with_linear_form_inequality( } } - // General case. general_refine(left_w_id, right_w_id, left, right); PPL_ASSERT(OK()); -} // end of refine +} // end of refine_with_linear_form_inequality template <typename T> template <typename Interval_Info> @@ -4471,8 +4467,7 @@ BD_Shape<T> return; } if (is_left_coeff_one && is_right_coeff_minus_one) { - // We fall back to a previous case - // (but we do not need to multiply the result by two). + // We fall back to a previous case. 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(); @@ -4484,9 +4479,8 @@ BD_Shape<T> return; } if (is_left_coeff_minus_one && is_right_coeff_one) { - // We fall back to a previous case - // (but we do not need to multiply the result by two). - PPL_DIRTY_TEMP(N, a_plus_minus_b_minus); + // We fall back to a previous case. + 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(),

1 0

[GIT] ppl/ppl(floating_point): Fixed Polyhedron:: refine_with_linear_form_inequality.
by Roberto Amadini 05 Oct '09

05 Oct '09

Module: ppl/ppl Branch: floating_point Commit: a92c340364deac28398db6f6533913458be3e652 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a92c340364de… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Mon Oct 5 17:06:17 2009 +0200 Fixed Polyhedron::refine_with_linear_form_inequality. Adapted tests on polyhedra. --- src/Polyhedron.templates.hh | 24 ++++++------ tests/Floating_Point_Expression/digitalfilters1.cc | 8 ++-- tests/Floating_Point_Expression/polyhedron1.cc | 42 ++++++++++---------- tests/Floating_Point_Expression/polyhedron2.cc | 32 +++++++------- 4 files changed, 53 insertions(+), 53 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=a92c3403…

1 0

[GIT] ppl/ppl(floating_point): Removed abstract_store parameter of Polyhedron::affine_image and
by Roberto Amadini 05 Oct '09

05 Oct '09

Module: ppl/ppl Branch: floating_point Commit: eda8bee287a3e0d969c46105bfb86198b88db7f9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=eda8bee287a3… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Mon Oct 5 16:05:44 2009 +0200 Removed abstract_store parameter of Polyhedron::affine_image and Polyhedron::refine_with_linear_form_inequality in digitalfilters1.cc --- tests/Floating_Point_Expression/digitalfilters1.cc | 49 +++++++++----------- 1 files changed, 22 insertions(+), 27 deletions(-) diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index bd047e4..3fd1157 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -311,7 +311,7 @@ test04() { NNC_Polyhedron ph_begin; // Y = 0; - ph.affine_image(Y, FP_Linear_Form(tmp), abstract_store); + ph.affine_image(Y, FP_Linear_Form(tmp)); for(unsigned short n = 0; ph_begin != ph; ++n) { @@ -321,28 +321,26 @@ test04() { // 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); + ph.affine_image(X, FP_Linear_Form(tmp)); tmp.lower() = 0; tmp.upper() = 16; - ph.affine_image(D, FP_Linear_Form(tmp), abstract_store); + ph.affine_image(D, FP_Linear_Form(tmp)); abstract_store = Box<FP_Interval>(ph); - ph.affine_image(S, FP_Linear_Form(Y), abstract_store); + ph.affine_image(S, FP_Linear_Form(Y)); abstract_store = Box<FP_Interval>(ph); - ph.affine_image(R, FP_Linear_Form(X - S), abstract_store); + ph.affine_image(R, FP_Linear_Form(X - S)); abstract_store = Box<FP_Interval>(ph); - ph.affine_image(Y, FP_Linear_Form(X), abstract_store); + ph.affine_image(Y, FP_Linear_Form(X)); // 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), - as_then); - ph_then.affine_image(Y, FP_Linear_Form(S - D), as_then); + -FP_Linear_Form(D)); + ph_then.affine_image(Y, FP_Linear_Form(S - D)); ph.refine_with_linear_form_inequality(-FP_Linear_Form(D), - FP_Linear_Form(R), - abstract_store); + FP_Linear_Form(R)); ph.upper_bound_assign(ph_then); abstract_store.upper_bound_assign(as_then); print_constraints(Box<FP_Interval>(ph) , @@ -352,13 +350,11 @@ test04() { ph_then = ph; as_then = abstract_store; ph_then.refine_with_linear_form_inequality(FP_Linear_Form(D), - FP_Linear_Form(R), - as_then); + FP_Linear_Form(R)); 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); + FP_Linear_Form(D)); ph.upper_bound_assign(ph_then); abstract_store.upper_bound_assign(as_then); print_constraints(Box<FP_Interval>(ph) , @@ -487,7 +483,6 @@ test05() { Box<FP_Interval> box(oc); print_constraints(box, "*** after widening ***"); tmp = box.get_interval(Y); - } nout << "*** Y in " << tmp << " ***" << endl; @@ -523,7 +518,7 @@ test06() { // Y = 0; con_y.linearize(abstract_store, lf_abstract_store, lk); - ph.affine_image(Y, lk, abstract_store); + ph.affine_image(Y, lk); for(unsigned short n = 0; ph_begin != ph; ++n) { @@ -533,28 +528,28 @@ test06() { // 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); + ph.affine_image(X, lk); Con_FP_Expression con_d(0, 16); con_d.linearize(abstract_store, lf_abstract_store, lk); - ph.affine_image(D, lk, abstract_store); + ph.affine_image(D, lk); 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); + ph.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); abstract_store = Box<FP_Interval>(ph); x_dif_s.linearize(abstract_store, lf_abstract_store, lr); - ph.affine_image(R, lr, abstract_store); + ph.affine_image(R, lr); 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); + ph.affine_image(Y, lx); // if (R <= -D) Y = S - D; NNC_Polyhedron ph_then(ph); @@ -564,9 +559,9 @@ test06() { 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_then.affine_image(Y, ly); - ph.refine_with_linear_form_inequality(-lk, lr, abstract_store); + ph.refine_with_linear_form_inequality(-lk, lr); ph.upper_bound_assign(ph_then); abstract_store.upper_bound_assign(as_then); @@ -576,15 +571,15 @@ test06() { // if (R >= D) Y = S + D; ph_then = ph; as_then = abstract_store; - ph_then.refine_with_linear_form_inequality(lk, lr, as_then); + ph_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); - ph_then.affine_image(Y, ly, as_then); + ph_then.affine_image(Y, ly); - ph.refine_with_linear_form_inequality(lr, lk, abstract_store); + ph.refine_with_linear_form_inequality(lr, lk); ph.upper_bound_assign(ph_then); abstract_store.upper_bound_assign(as_then);

1 0

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

05 Oct '09

Module: ppl/ppl Branch: floating_point Commit: b37ac0cb3045394b6f2c36d3998bb8cd06498677 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b37ac0cb3045… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Oct 5 15:39:57 2009 +0200 Fixed a few typos. --- src/Polyhedron.defs.hh | 2 +- src/Polyhedron.templates.hh | 18 ++++++++++++------ 2 files changed, 13 insertions(+), 7 deletions(-) diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index 1cb2007..0dfcf54 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -2684,7 +2684,7 @@ protected: considered as singletons. */ template <typename FP_Format, typename Interval_Info> - static void overapproximate_linear_form( + void overapproximate_linear_form( const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, const dimension_type lf_dimension, Linear_Form<Interval <FP_Format, Interval_Info> >& result); diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index 3b86858..ac4ad97 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -325,10 +325,12 @@ Polyhedron::refine_with_linear_form_inequality( // We assume that the analyzer will not refine an unreachable test. PPL_ASSERT(!marked_empty()); - if (Floating_Point_Expression::overflows(left)) + if (Floating_Point_Expression<FP_Format, float_ieee754_single>:: + overflows(left)) return; - if (Floating_Point_Expression::overflows(right)) + if (Floating_Point_Expression<FP_Format, float_ieee754_single>:: + overflows(right)) return; typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; @@ -337,13 +339,15 @@ Polyhedron::refine_with_linear_form_inequality( // Overapproximate left - right. FP_Linear_Form left_minus_right(left); left_minus_right -= right; - if (Floating_Point_Expression::overflows(left_minus_right)) + if (Floating_Point_Expression<FP_Format, float_ieee754_single>:: + overflows(left_minus_right)) return; dimension_type lf_space_dim = left_minus_right.space_dimension(); FP_Linear_Form lf_approx; overapproximate_linear_form(left_minus_right, lf_space_dim, lf_approx); - if (Floating_Point_Expression::overflows(lf_approx)) + if (Floating_Point_Expression<FP_Format, float_ieee754_single>:: + overflows(lf_approx)) return; // Normalize left - right. @@ -381,7 +385,8 @@ const Linear_Form<Interval <FP_Format, Interval_Info> >& lf) { // We assume that the analyzer will not perform an unreachable assignment. PPL_ASSERT(!marked_empty()); - if (Floating_Point_Expression::overflows(lf)) { + if (Floating_Point_Expression<FP_Format, float_ieee754_single>:: + overflows(lf)) { *this = Polyhedron(topology(), space_dim, UNIVERSE); return; } @@ -393,7 +398,8 @@ const Linear_Form<Interval <FP_Format, Interval_Info> >& lf) { FP_Linear_Form lf_approx; overapproximate_linear_form(lf, lf_space_dim, lf_approx); - if (Floating_Point_Expression::overflows(lf_approx)) { + if (Floating_Point_Expression<FP_Format, float_ieee754_single>:: + overflows(lf_approx)) { *this = Polyhedron(topology(), space_dim, UNIVERSE); return; }

1 0