September 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): Added and modified some tests.
by Roberto Amadini 08 Sep '09

08 Sep '09

Module: ppl/ppl Branch: floating_point Commit: a7bef215e417ec62a190b860dc0c1990e688360a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a7bef215e417… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Tue Sep 8 00:06:08 2009 +0200 Added and modified some tests. --- .../floatingpointexpr1.cc | 180 +++++++++++++++----- 1 files changed, 141 insertions(+), 39 deletions(-) diff --git a/tests/Floating_Point_Expression/floatingpointexpr1.cc b/tests/Floating_Point_Expression/floatingpointexpr1.cc index 5b6dd75..d4c8fce 100644 --- a/tests/Floating_Point_Expression/floatingpointexpr1.cc +++ b/tests/Floating_Point_Expression/floatingpointexpr1.cc @@ -65,16 +65,26 @@ typedef Constant_Floating_Point_Expression<db_r_oc, IEEE754_Single>::FP_Interval typedef Floating_Point_Expression<fl_r_oc, IEEE754_Single>::FP_Linear_Form_Abstract_Store lsstr; typedef Constant_Floating_Point_Expression<db_r_oc, IEEE754_Single>::FP_Linear_Form_Abstract_Store ldstr; +//FIXME: Why the analyzed format can't be IEEE754_Double? +typedef Floating_Point_Expression<fl_r_oc, IEEE754_Double>::FP_Interval_Abstract_Store sdtr; +typedef Constant_Floating_Point_Expression<db_r_oc, IEEE754_Double>::FP_Interval_Abstract_Store ddtr; + +typedef Floating_Point_Expression<fl_r_oc, IEEE754_Double>::FP_Linear_Form_Abstract_Store lsdtr; +typedef Constant_Floating_Point_Expression<db_r_oc, IEEE754_Double>::FP_Linear_Form_Abstract_Store lddtr; + namespace { using namespace Parma_Polyhedra_Library::IO_Operators; +// Tests absolute errors. bool test01() { nout << std::numeric_limits<float>::denorm_min() << endl; nout << div_fpess::absolute_error << endl; nout << div_fpesd::absolute_error << endl; nout << div_fpeds::absolute_error << endl; + nout << div_fpedd::absolute_error << endl; + if (div_fpess::absolute_error != std::numeric_limits<float>::denorm_min()) return false; @@ -84,21 +94,15 @@ test01() { if (div_fpeds::absolute_error != std::numeric_limits<float>::denorm_min()) return false; - return true; -} - -bool -test02() { - nout << std::numeric_limits<double>::denorm_min() << endl; - nout << div_fpedd::absolute_error << endl; if (div_fpedd::absolute_error != std::numeric_limits<double>::denorm_min()) return false; return true; } +// Tests division by zero. bool -test03() { +test02() { con_fpess* num = new con_fpess(3, 5); con_fpess* den = new con_fpess(-1, 1); div_fpess div(num, den); @@ -107,53 +111,117 @@ test03() { div.linearize(sstr(), lsstr(), result); } catch (Linearization_Failed e) { + nout << "Division by zero." << endl; return true; } return false; } +// Tests multiplication by zero. +bool +test03() { + sstr store_fl; + store_fl[0] = fl_r_oc(0); + store_fl[1] = fl_r_oc(10); + con_fpess* con_fl = new con_fpess(5, 6); + var_fpess* var0_fl = new var_fpess(0); + var_fpess* var1_fl = new var_fpess(1); + dif_fpess* dif_fl = new dif_fpess(var1_fl, con_fl); + mul_fpess mul_fl(dif_fl, var0_fl); + Float_Interval_Linear_Form result_fl; + mul_fl.linearize(store_fl, lsstr(), result_fl); + + fl_r_oc kr_fl(-std::numeric_limits<float>::denorm_min()); + kr_fl.join_assign(std::numeric_limits<float>::denorm_min()); + Float_Interval_Linear_Form known_result_fl(kr_fl); + + nout << "*** known_result_fl ***" << endl + << known_result_fl << endl; + bool ok_fl = (result_fl == known_result_fl); + + dstr store_db; + store_db[0] = db_r_oc(0); + store_db[1] = db_r_oc(4); + con_fpedd* con_db = new con_fpedd(5, 6); + var_fpedd* var0_db = new var_fpedd(0); + var_fpedd* var1_db = new var_fpedd(1); + sum_fpedd* sum_db = new sum_fpedd(con_db, var1_db); + mul_fpedd mul_db(var0_db, sum_db); + Double_Interval_Linear_Form result_db; + mul_db.linearize(store_db, ldstr(), result_db); + + db_r_oc kr_db(-std::numeric_limits<double>::denorm_min()); + kr_db.join_assign(std::numeric_limits<double>::denorm_min()); + Double_Interval_Linear_Form known_result_db(kr_db); + + nout << "*** known_result_db ***" << endl + << known_result_db << endl; + bool ok_db = (result_db == known_result_db); + + return ok_fl && ok_db; +} + +// Tests the linearization of A + B. bool test04() { - sstr store; - store[0] = fl_r_oc(0); - store[1] = fl_r_oc(10); - con_fpess* con = new con_fpess(5, 6); - var_fpess* var0 = new var_fpess(0); - var_fpess* var1 = new var_fpess(1); - dif_fpess* dif = new dif_fpess(var1, con); - mul_fpess mul(dif, var0); - Float_Interval_Linear_Form result; - mul.linearize(store, lsstr(), result); - nout << result << endl; - fl_r_oc kr(-std::numeric_limits<float>::denorm_min()); - kr.join_assign(std::numeric_limits<float>::denorm_min()); - Float_Interval_Linear_Form known_result(kr); + dstr store; + db_r_oc tmp; + store[0] = tmp; + store[1] = tmp; + var_fpeds* var0 = new var_fpeds(0); + var_fpeds* var1 = new var_fpeds(1); + sum_fpeds sum(var0, var1); + Double_Interval_Linear_Form result; + sum.linearize(store, ldstr(), result); + + Variable A(0); + Variable B(1); + Double_Interval_Linear_Form known_result = Double_Interval_Linear_Form(A); + float exp = pow(2, -23); + tmp = db_r_oc(1 - exp); + tmp.join_assign(1 + exp); + known_result *= tmp; + known_result += tmp * Linear_Form<db_r_oc>(B); + tmp = db_r_oc(-std::numeric_limits<float>::denorm_min()); + tmp.join_assign(std::numeric_limits<float>::denorm_min()); + known_result += tmp; + nout << "*** known_result ***" << endl << known_result << endl; return result == known_result; } +// Tests the linearization of A - B. bool test05() { - dstr store; - store[0] = db_r_oc(0); - store[1] = db_r_oc(4); - con_fpedd* con = new con_fpedd(5, 6); - var_fpedd* var0 = new var_fpedd(0); - var_fpedd* var1 = new var_fpedd(1); - sum_fpedd* sum = new sum_fpedd(con, var1); - mul_fpedd mul(var0, sum); - Double_Interval_Linear_Form result; - mul.linearize(store, ldstr(), result); - nout << result << endl; - db_r_oc kr(-std::numeric_limits<double>::denorm_min()); - kr.join_assign(std::numeric_limits<double>::denorm_min()); - Double_Interval_Linear_Form known_result(kr); + sstr store; + fl_r_oc tmp; + store[0] = tmp; + store[1] = tmp; + var_fpess* var0 = new var_fpess(0); + var_fpess* var1 = new var_fpess(1); + dif_fpess dif(var0, var1); + Float_Interval_Linear_Form result; + dif.linearize(store, lsstr(), result); + + Variable A(0); + Variable B(1); + Float_Interval_Linear_Form known_result = Float_Interval_Linear_Form(A); + float exp = pow(2, -23); + tmp = fl_r_oc(1 - exp); + tmp.join_assign(1 + exp); + known_result *= tmp; + known_result -= tmp * Linear_Form<fl_r_oc>(B); + tmp = fl_r_oc(-std::numeric_limits<float>::denorm_min()); + tmp.join_assign(std::numeric_limits<float>::denorm_min()); + known_result += tmp; + nout << "*** known_result ***" << endl << known_result << endl; return result == known_result; } +// Tests the linearization of A * B where A = [0, 1] and B = [2, 2]. bool test06() { sstr store; @@ -166,16 +234,49 @@ test06() { mul_fpess mul(var0, var1); Float_Interval_Linear_Form result; mul.linearize(store, lsstr(), result); + tmp = fl_r_oc(-std::numeric_limits<float>::denorm_min()); tmp.join_assign(std::numeric_limits<float>::denorm_min()); float exp = pow(2, -22); - fl_r_oc coeff = fl_r_oc(-exp); - coeff.join_assign(exp); - coeff += fl_r_oc(2); + fl_r_oc coeff = fl_r_oc(2 - exp); + coeff.join_assign(2 + exp); + //fl_r_oc coeff = fl_r_oc(-exp); + //coeff.join_assign(exp); + //coeff += fl_r_oc(2); Float_Interval_Linear_Form known_result = Float_Interval_Linear_Form(Variable(0)); known_result *= coeff; known_result += tmp; + + nout << "*** known_result ***" << endl + << known_result << endl; + return result == known_result; +} + +// Tests the linearization of A / B where A = [1, 4] and B = [2, 2]. +bool +test07() { + ddtr store; + db_r_oc tmp = db_r_oc(0); + tmp.join_assign(1); + store[0] = tmp; + store[1] = db_r_oc(2); + var_fpedd* var0 = new var_fpedd(0); + var_fpedd* var1 = new var_fpedd(1); + div_fpedd div(var0, var1); + Double_Interval_Linear_Form result; + div.linearize(store, lddtr(), result); + + tmp = db_r_oc(-std::numeric_limits<double>::denorm_min()); + tmp.join_assign(std::numeric_limits<double>::denorm_min()); + float exp = pow(2, -53); + db_r_oc coeff = db_r_oc(1 / 2.0 - exp); + coeff.join_assign(1 / 2.0 + exp); + Double_Interval_Linear_Form known_result = + Double_Interval_Linear_Form(Variable(0)); + known_result *= coeff; + known_result += tmp; + nout << "*** known_result ***" << endl << known_result << endl; return result == known_result; @@ -190,4 +291,5 @@ BEGIN_MAIN DO_TEST(test04); DO_TEST(test05); DO_TEST(test06); + DO_TEST(test07); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Update documentation
by Fabio Biselli 07 Sep '09

07 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 4ea81ad27e069428baa44026d7f907c735a442f8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4ea81ad27e06… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Mon Sep 7 20:24:53 2009 +0200 Update documentation --- src/Division_Floating_Point_Expression.defs.hh | 4 +--- src/Floating_Point_Expression.defs.hh | 4 ++-- src/Variable_Floating_Point_Expression.defs.hh | 3 ++- 3 files changed, 5 insertions(+), 6 deletions(-) diff --git a/src/Division_Floating_Point_Expression.defs.hh b/src/Division_Floating_Point_Expression.defs.hh index a2a3d68..2a7738a 100644 --- a/src/Division_Floating_Point_Expression.defs.hh +++ b/src/Division_Floating_Point_Expression.defs.hh @@ -121,10 +121,8 @@ public: \param store The abstract store. \param result The linear form that will be modified. - \exception Parma_Polyhedra_Library::Linearization_Failed - Thrown if \f$0 \in\f$ - \p *this.second_operand. + Thrown if \f$0 \f$ is into second operand range. */ void linearize(const FP_Interval_Abstract_Store& int_store, const FP_Linear_Form_Abstract_Store& lf_store, diff --git a/src/Floating_Point_Expression.defs.hh b/src/Floating_Point_Expression.defs.hh index 845667a..68618a6 100644 --- a/src/Floating_Point_Expression.defs.hh +++ b/src/Floating_Point_Expression.defs.hh @@ -51,8 +51,8 @@ struct IEEE754_Double { //! A floating point expression on a given format /*! \ingroup PPL_CXX_Interface This class offers a generic implemenation of a - <EM>floating point expression</EM> of format \f$f\f$, this includes - constants, variables of format \f$f\f$, binary and unary + <EM>floating point expression</EM> of format \f$$\mathbf{f}$\f$, this + includes constants, variables of format \f$$\mathbf{f}$\f$, binary and unary arithmetic operators. \par Template type parameters diff --git a/src/Variable_Floating_Point_Expression.defs.hh b/src/Variable_Floating_Point_Expression.defs.hh index e614df4..cb1c300 100644 --- a/src/Variable_Floating_Point_Expression.defs.hh +++ b/src/Variable_Floating_Point_Expression.defs.hh @@ -106,9 +106,10 @@ public: //@} // Constructors and Destructor + //! Linearization of a variable. /*! \brief Modifies a linear form \p result in the abstract store \p store - corresponding to <CODE>this</CODE> variable with coefficent \f[1,1]\f. + corresponding to <CODE>this</CODE> variable with coefficent \f$[1,1]\f$. \param store The abstract store. \param result The linear form that will be modified.

1 0

[GIT] ppl/ppl(floating_point): Fixed a bug in method relative_error.
by Roberto Amadini 07 Sep '09

07 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 9eea1940a0dd76e2e77308044eed6acfb193da4c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9eea1940a0dd… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Mon Sep 7 18:11:16 2009 +0200 Fixed a bug in method relative_error. Edited test06 to cope with the new interface of method linearize. --- src/Floating_Point_Expression.templates.hh | 2 +- .../floatingpointexpr1.cc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Floating_Point_Expression.templates.hh b/src/Floating_Point_Expression.templates.hh index 52b71c7..8c5ce32 100644 --- a/src/Floating_Point_Expression.templates.hh +++ b/src/Floating_Point_Expression.templates.hh @@ -34,7 +34,7 @@ Floating_Point_Expression<FP_Interval_Type, FP_Format> ::relative_error(const FP_Linear_Form& lf, FP_Linear_Form& result) { /* FIXME: here we assume that boundary_type can represent (2)^(-FP_Format::fraction_bits) precisely. */ - FP_Interval_Type error_propagator(pow(-2, -FP_Format::fraction_bits)); + FP_Interval_Type error_propagator(-pow(2, -FP_Format::fraction_bits)); // FIXME: this may be incorrect for some policies. error_propagator.join_assign(FP_Interval_Type( pow(2, -FP_Format::fraction_bits))); diff --git a/tests/Floating_Point_Expression/floatingpointexpr1.cc b/tests/Floating_Point_Expression/floatingpointexpr1.cc index 334eaa5..5b6dd75 100644 --- a/tests/Floating_Point_Expression/floatingpointexpr1.cc +++ b/tests/Floating_Point_Expression/floatingpointexpr1.cc @@ -165,7 +165,7 @@ test06() { var_fpess* var1 = new var_fpess(1); mul_fpess mul(var0, var1); Float_Interval_Linear_Form result; - mul.linearize(store, result); + mul.linearize(store, lsstr(), result); tmp = fl_r_oc(-std::numeric_limits<float>::denorm_min()); tmp.join_assign(std::numeric_limits<float>::denorm_min()); float exp = pow(2, -22);

1 0

[GIT] ppl/ppl(floating_point): Added one test.
by Roberto Amadini 07 Sep '09

07 Sep '09

Module: ppl/ppl Branch: floating_point Commit: a8ecdc0727c836b3b9447accf27e9e95cbcda89c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a8ecdc0727c8… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Mon Sep 7 18:03:22 2009 +0200 Added one test. --- .../floatingpointexpr1.cc | 34 ++++++++++++++++++- 1 files changed, 32 insertions(+), 2 deletions(-) diff --git a/tests/Floating_Point_Expression/floatingpointexpr1.cc b/tests/Floating_Point_Expression/floatingpointexpr1.cc index c9a64d8..334eaa5 100644 --- a/tests/Floating_Point_Expression/floatingpointexpr1.cc +++ b/tests/Floating_Point_Expression/floatingpointexpr1.cc @@ -128,7 +128,8 @@ test04() { fl_r_oc kr(-std::numeric_limits<float>::denorm_min()); kr.join_assign(std::numeric_limits<float>::denorm_min()); Float_Interval_Linear_Form known_result(kr); - nout << known_result << endl; + nout << "*** known_result ***" << endl + << known_result << endl; return result == known_result; } @@ -148,7 +149,35 @@ test05() { db_r_oc kr(-std::numeric_limits<double>::denorm_min()); kr.join_assign(std::numeric_limits<double>::denorm_min()); Double_Interval_Linear_Form known_result(kr); - nout << known_result << endl; + nout << "*** known_result ***" << endl + << known_result << endl; + return result == known_result; +} + +bool +test06() { + sstr store; + fl_r_oc tmp = fl_r_oc(0); + tmp.join_assign(1); + store[0] = tmp; + store[1] = fl_r_oc(2); + var_fpess* var0 = new var_fpess(0); + var_fpess* var1 = new var_fpess(1); + mul_fpess mul(var0, var1); + Float_Interval_Linear_Form result; + mul.linearize(store, result); + tmp = fl_r_oc(-std::numeric_limits<float>::denorm_min()); + tmp.join_assign(std::numeric_limits<float>::denorm_min()); + float exp = pow(2, -22); + fl_r_oc coeff = fl_r_oc(-exp); + coeff.join_assign(exp); + coeff += fl_r_oc(2); + Float_Interval_Linear_Form known_result = + Float_Interval_Linear_Form(Variable(0)); + known_result *= coeff; + known_result += tmp; + nout << "*** known_result ***" << endl + << known_result << endl; return result == known_result; } @@ -160,4 +189,5 @@ BEGIN_MAIN DO_TEST(test03); DO_TEST(test04); DO_TEST(test05); + DO_TEST(test06); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Extended method linearize to also accept a linear form abstract store.
by Fabio Bossi 07 Sep '09

07 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 38cb91a8f194c039d375dc657e89a440253d90cf URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=38cb91a8f194… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Sep 7 16:12:10 2009 +0200 Extended method linearize to also accept a linear form abstract store. Adjusted tests (but NOT YET THE DOCUMENTATION) accordingly. --- src/Constant_Floating_Point_Expression.defs.hh | 7 ++++++- src/Constant_Floating_Point_Expression.inlines.hh | 3 ++- src/Difference_Floating_Point_Expression.defs.hh | 7 ++++++- ...fference_Floating_Point_Expression.templates.hh | 7 ++++--- src/Division_Floating_Point_Expression.defs.hh | 7 ++++++- ...Division_Floating_Point_Expression.templates.hh | 9 +++++---- src/Floating_Point_Expression.defs.hh | 9 +++++++-- ...ultiplication_Floating_Point_Expression.defs.hh | 7 ++++++- ...lication_Floating_Point_Expression.templates.hh | 11 ++++++----- src/Opposite_Floating_Point_Expression.defs.hh | 7 ++++++- src/Opposite_Floating_Point_Expression.inlines.hh | 5 +++-- src/Sum_Floating_Point_Expression.defs.hh | 7 ++++++- src/Sum_Floating_Point_Expression.templates.hh | 7 ++++--- src/Variable_Floating_Point_Expression.defs.hh | 10 ++++++++-- src/Variable_Floating_Point_Expression.inlines.hh | 11 +++++++++-- .../floatingpointexpr1.cc | 9 ++++++--- 16 files changed, 90 insertions(+), 33 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=38cb91a8…

1 0

[GIT] ppl/ppl(floating_point): Documentation updates
by Fabio Biselli 07 Sep '09

07 Sep '09

Module: ppl/ppl Branch: floating_point Commit: a8a6f6a79cee0ed570746c38d2a8a0c15cf2298b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a8a6f6a79cee… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Mon Sep 7 18:09:18 2009 +0200 Documentation updates --- src/Constant_Floating_Point_Expression.defs.hh | 9 +++-- src/Difference_Floating_Point_Expression.defs.hh | 9 ++++- src/Division_Floating_Point_Expression.defs.hh | 20 ++++++++++- src/Floating_Point_Expression.defs.hh | 38 ++++++++++++------- ...ultiplication_Floating_Point_Expression.defs.hh | 5 ++- src/Sum_Floating_Point_Expression.defs.hh | 5 ++- src/Variable_Floating_Point_Expression.defs.hh | 10 ++++-- 7 files changed, 70 insertions(+), 26 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=a8a6f6a7…

1 0

[GIT] ppl/ppl(floating_point): Do not ignore undefined variables while intervalizing: assert that they
by Fabio Bossi 07 Sep '09

07 Sep '09

Module: ppl/ppl Branch: floating_point Commit: db823a39805358e61caddc3122c535ffbdb5564f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=db823a398053… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Sep 7 15:00:37 2009 +0200 Do not ignore undefined variables while intervalizing: assert that they are defined instead. --- src/Floating_Point_Expression.templates.hh | 9 ++++----- 1 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/Floating_Point_Expression.templates.hh b/src/Floating_Point_Expression.templates.hh index 03654fb..52b71c7 100644 --- a/src/Floating_Point_Expression.templates.hh +++ b/src/Floating_Point_Expression.templates.hh @@ -73,11 +73,10 @@ Floating_Point_Expression<FP_Interval_Type, FP_Format> for (dimension_type i = 0; i < dimension; ++i) { typename FP_Interval_Abstract_Store::const_iterator next_variable_value = store.find(i); - if (next_variable_value != store.end()) { - FP_Interval_Type current_addend = lf.coefficient(Variable(i)); - current_addend *= next_variable_value->second; - result += current_addend; - } + assert(next_variable_value != store.end()); + FP_Interval_Type current_addend = lf.coefficient(Variable(i)); + current_addend *= next_variable_value->second; + result += current_addend; } return;

1 0

[GIT] ppl/ppl(floating_point): Fixed a bug in Linar_Form::operator== where zero coefficients were not
by Fabio Bossi 07 Sep '09

07 Sep '09

Module: ppl/ppl Branch: floating_point Commit: bf7c1eb0d35ea326d3af8c04623596826baf7e41 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bf7c1eb0d35e… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Sep 7 14:23:23 2009 +0200 Fixed a bug in Linar_Form::operator== where zero coefficients were not treated properly. Added a few simple tests for class Floating_Point_Expression. --- src/Linear_Form.templates.hh | 24 ++++++++-- .../floatingpointexpr1.cc | 48 ++++++++++++++++++- 2 files changed, 64 insertions(+), 8 deletions(-) diff --git a/src/Linear_Form.templates.hh b/src/Linear_Form.templates.hh index 19dc331..ffa6772 100644 --- a/src/Linear_Form.templates.hh +++ b/src/Linear_Form.templates.hh @@ -325,12 +325,26 @@ inline bool operator==(const Linear_Form<C>& x, const Linear_Form<C>& y) { const dimension_type x_size = x.size(); const dimension_type y_size = y.size(); - if (x_size != y_size) - return false; + if (x_size >= y_size) { + for (dimension_type i = y_size; i-- > 0; ) + if (x[i] != y[i]) + return false; - for (dimension_type i = x_size; i-- > 0; ) - if (x[i] != y[i]) - return false; + for (dimension_type i = x_size; --i > y_size; ) + if (x[i] != x.zero) + return false; + + } + else { + for (dimension_type i = x_size; i-- > 0; ) + if (x[i] != y[i]) + return false; + + for (dimension_type i = y_size; --i > x_size; ) + if (y[i] != x.zero) + return false; + + } return true; } diff --git a/tests/Floating_Point_Expression/floatingpointexpr1.cc b/tests/Floating_Point_Expression/floatingpointexpr1.cc index e0cf4e1..2e0e303 100644 --- a/tests/Floating_Point_Expression/floatingpointexpr1.cc +++ b/tests/Floating_Point_Expression/floatingpointexpr1.cc @@ -97,11 +97,11 @@ test02() { bool test03() { con_fpess* num = new con_fpess(3, 5); - con_fpess* den = new con_fpess(-1,1); + con_fpess* den = new con_fpess(-1, 1); div_fpess div(num, den); try { - Float_Interval_Linear_Form res; - div.linearize(sstr(), res); + Float_Interval_Linear_Form result; + div.linearize(sstr(), result); } catch (Linearization_Failed e) { return true; @@ -109,10 +109,52 @@ test03() { return false; } +bool +test04() { + sstr store; + store[0] = fl_r_oc(0); + store[1] = fl_r_oc(10); + con_fpess* con = new con_fpess(5, 6); + var_fpess* var0 = new var_fpess(0); + var_fpess* var1 = new var_fpess(1); + dif_fpess* dif = new dif_fpess(var1, con); + mul_fpess mul(dif, var0); + Float_Interval_Linear_Form result; + mul.linearize(store, result); + nout << result << endl; + fl_r_oc kr(-std::numeric_limits<float>::denorm_min()); + kr.join_assign(std::numeric_limits<float>::denorm_min()); + Float_Interval_Linear_Form known_result(kr); + nout << known_result << endl; + return result == known_result; +} + +bool +test05() { + dstr store; + store[0] = db_r_oc(0); + store[1] = db_r_oc(4); + con_fpedd* con = new con_fpedd(5, 6); + var_fpedd* var0 = new var_fpedd(0); + var_fpedd* var1 = new var_fpedd(1); + sum_fpedd* sum = new sum_fpedd(con, var1); + mul_fpedd mul(var0, sum); + Double_Interval_Linear_Form result; + mul.linearize(store, result); + nout << result << endl; + db_r_oc kr(-std::numeric_limits<double>::denorm_min()); + kr.join_assign(std::numeric_limits<double>::denorm_min()); + Double_Interval_Linear_Form known_result(kr); + nout << known_result << endl; + return result == known_result; +} + } // namespace BEGIN_MAIN DO_TEST(test01); DO_TEST(test02); DO_TEST(test03); + DO_TEST(test04); + DO_TEST(test05); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Added more typedefs and one test.
by Fabio Bossi 07 Sep '09

07 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 3ea4657845b39d6bdadb22fa26658f4da21c5fc2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3ea4657845b3… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Sep 7 11:07:24 2009 +0200 Added more typedefs and one test. --- .../floatingpointexpr1.cc | 15 ++++++++++++++- 1 files changed, 14 insertions(+), 1 deletions(-) diff --git a/tests/Floating_Point_Expression/floatingpointexpr1.cc b/tests/Floating_Point_Expression/floatingpointexpr1.cc index 6ac6f5a..e0cf4e1 100644 --- a/tests/Floating_Point_Expression/floatingpointexpr1.cc +++ b/tests/Floating_Point_Expression/floatingpointexpr1.cc @@ -59,6 +59,9 @@ typedef Variable_Floating_Point_Expression<db_r_oc, IEEE754_Double> var_fpedd; typedef Opposite_Floating_Point_Expression<db_r_oc, IEEE754_Single> opp_fpeds; typedef Opposite_Floating_Point_Expression<db_r_oc, IEEE754_Double> opp_fpedd; +typedef Floating_Point_Expression<fl_r_oc, IEEE754_Single>::FP_Interval_Abstract_Store sstr; +typedef Constant_Floating_Point_Expression<db_r_oc, IEEE754_Single>::FP_Interval_Abstract_Store dstr; + namespace { using namespace Parma_Polyhedra_Library::IO_Operators; @@ -93,7 +96,17 @@ test02() { bool test03() { - return true; + con_fpess* num = new con_fpess(3, 5); + con_fpess* den = new con_fpess(-1,1); + div_fpess div(num, den); + try { + Float_Interval_Linear_Form res; + div.linearize(sstr(), res); + } + catch (Linearization_Failed e) { + return true; + } + return false; } } // namespace

1 0

[GIT] ppl/ppl(floating_point): Added two simple tests.
by Fabio Bossi 07 Sep '09

07 Sep '09

Module: ppl/ppl Branch: floating_point Commit: fc9e7a5ea189bb3ebb98d3baa4d470f69b339ee4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fc9e7a5ea189… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Sep 7 10:53:07 2009 +0200 Added two simple tests. --- .../floatingpointexpr1.cc | 75 ++++++++++++++++---- 1 files changed, 60 insertions(+), 15 deletions(-) diff --git a/tests/Floating_Point_Expression/floatingpointexpr1.cc b/tests/Floating_Point_Expression/floatingpointexpr1.cc index 9f635c8..6ac6f5a 100644 --- a/tests/Floating_Point_Expression/floatingpointexpr1.cc +++ b/tests/Floating_Point_Expression/floatingpointexpr1.cc @@ -22,21 +22,42 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "ppl_test.hh" -typedef Linear_Form<fl_r_oc> Interval_Linear_Form; -typedef Division_Floating_Point_Expression<fl_r_oc, IEEE754_Single> div_fpes; -typedef Division_Floating_Point_Expression<fl_r_oc, IEEE754_Double> div_fped; -typedef Difference_Floating_Point_Expression<fl_r_oc, IEEE754_Single> dif_fpes; -typedef Difference_Floating_Point_Expression<fl_r_oc, IEEE754_Double> dif_fped; -typedef Multiplication_Floating_Point_Expression<fl_r_oc, IEEE754_Single> mul_fpes; -typedef Multiplication_Floating_Point_Expression<fl_r_oc, IEEE754_Double> mul_fped; -typedef Sum_Floating_Point_Expression<fl_r_oc, IEEE754_Single> sum_fpes; -typedef Sum_Floating_Point_Expression<fl_r_oc, IEEE754_Double> sum_fped; -typedef Constant_Floating_Point_Expression<fl_r_oc, IEEE754_Single> con_fpes; -typedef Constant_Floating_Point_Expression<fl_r_oc, IEEE754_Double> con_fped; -typedef Variable_Floating_Point_Expression<fl_r_oc, IEEE754_Single> var_fpes; -typedef Variable_Floating_Point_Expression<fl_r_oc, IEEE754_Double> var_fped; -typedef Opposite_Floating_Point_Expression<fl_r_oc, IEEE754_Single> opp_fpes; -typedef Opposite_Floating_Point_Expression<fl_r_oc, IEEE754_Double> opp_fped; +typedef Linear_Form<fl_r_oc> Float_Interval_Linear_Form; +typedef Linear_Form<db_r_oc> Double_Interval_Linear_Form; + +typedef Division_Floating_Point_Expression<fl_r_oc, IEEE754_Single> div_fpess; +typedef Division_Floating_Point_Expression<fl_r_oc, IEEE754_Double> div_fpesd; +typedef Difference_Floating_Point_Expression<fl_r_oc, IEEE754_Single> dif_fpess; +typedef Difference_Floating_Point_Expression<fl_r_oc, IEEE754_Double> dif_fpesd; +typedef Multiplication_Floating_Point_Expression<fl_r_oc, IEEE754_Single> +mul_fpess; +typedef Multiplication_Floating_Point_Expression<fl_r_oc, IEEE754_Double> +mul_fpesd; +typedef Sum_Floating_Point_Expression<fl_r_oc, IEEE754_Single> sum_fpess; +typedef Sum_Floating_Point_Expression<fl_r_oc, IEEE754_Double> sum_fpesd; +typedef Constant_Floating_Point_Expression<fl_r_oc, IEEE754_Single> con_fpess; +typedef Constant_Floating_Point_Expression<fl_r_oc, IEEE754_Double> con_fpesd; +typedef Variable_Floating_Point_Expression<fl_r_oc, IEEE754_Single> var_fpess; +typedef Variable_Floating_Point_Expression<fl_r_oc, IEEE754_Double> var_fpesd; +typedef Opposite_Floating_Point_Expression<fl_r_oc, IEEE754_Single> opp_fpess; +typedef Opposite_Floating_Point_Expression<fl_r_oc, IEEE754_Double> opp_fpesd; + +typedef Division_Floating_Point_Expression<db_r_oc, IEEE754_Single> div_fpeds; +typedef Division_Floating_Point_Expression<db_r_oc, IEEE754_Double> div_fpedd; +typedef Difference_Floating_Point_Expression<db_r_oc, IEEE754_Single> dif_fpeds; +typedef Difference_Floating_Point_Expression<db_r_oc, IEEE754_Double> dif_fpedd; +typedef Multiplication_Floating_Point_Expression<db_r_oc, IEEE754_Single> +mul_fpeds; +typedef Multiplication_Floating_Point_Expression<db_r_oc, IEEE754_Double> +mul_fpedd; +typedef Sum_Floating_Point_Expression<db_r_oc, IEEE754_Single> sum_fpeds; +typedef Sum_Floating_Point_Expression<db_r_oc, IEEE754_Double> sum_fpedd; +typedef Constant_Floating_Point_Expression<db_r_oc, IEEE754_Single> con_fpeds; +typedef Constant_Floating_Point_Expression<db_r_oc, IEEE754_Double> con_fpedd; +typedef Variable_Floating_Point_Expression<db_r_oc, IEEE754_Single> var_fpeds; +typedef Variable_Floating_Point_Expression<db_r_oc, IEEE754_Double> var_fpedd; +typedef Opposite_Floating_Point_Expression<db_r_oc, IEEE754_Single> opp_fpeds; +typedef Opposite_Floating_Point_Expression<db_r_oc, IEEE754_Double> opp_fpedd; namespace { @@ -44,11 +65,34 @@ using namespace Parma_Polyhedra_Library::IO_Operators; bool test01() { + nout << std::numeric_limits<float>::denorm_min() << endl; + nout << div_fpess::absolute_error << endl; + nout << div_fpesd::absolute_error << endl; + nout << div_fpeds::absolute_error << endl; + if (div_fpess::absolute_error != std::numeric_limits<float>::denorm_min()) + return false; + + if (div_fpesd::absolute_error != std::numeric_limits<float>::denorm_min()) + return false; + + if (div_fpeds::absolute_error != std::numeric_limits<float>::denorm_min()) + return false; + return true; } bool test02() { + nout << std::numeric_limits<double>::denorm_min() << endl; + nout << div_fpedd::absolute_error << endl; + if (div_fpedd::absolute_error != std::numeric_limits<double>::denorm_min()) + return false; + + return true; +} + +bool +test03() { return true; } @@ -57,4 +101,5 @@ test02() { BEGIN_MAIN DO_TEST(test01); DO_TEST(test02); + DO_TEST(test03); END_MAIN

1 0