September 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): Renamed float_IBM_single and float_IBM_double lowering the case for IBM.
by Roberto Bagnara 22 Sep '09

22 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 7dbbf2813ae8021abce08336d6f7fdd1579958b3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7dbbf2813ae8… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Sep 22 17:57:29 2009 +0200 Renamed float_IBM_single and float_IBM_double lowering the case for IBM. --- src/Float.defs.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Float.defs.hh b/src/Float.defs.hh index 2053a9a..6586e0e 100644 --- a/src/Float.defs.hh +++ b/src/Float.defs.hh @@ -125,7 +125,7 @@ struct float_ieee754_double { /*! \ingroup PPL_CXX_interface */ #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) -struct float_IBM_single { +struct float_ibm_single { static const unsigned int EXPONENT_BITS = 7; static const unsigned int MANTISSA_BITS = 24; static const int EXPONENT_BIAS = 64; @@ -135,7 +135,7 @@ struct float_IBM_single { /*! \ingroup PPL_CXX_interface */ #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) -struct float_IBM_double { +struct float_ibm_double { static const unsigned int EXPONENT_BITS = 7; static const unsigned int MANTISSA_BITS = 56; static const int EXPONENT_BIAS = 64;

1 0

[GIT] ppl/ppl(floating_point): Added some infrastructure to perform parametric tests.
by Roberto Bagnara 22 Sep '09

22 Sep '09

Module: ppl/ppl Branch: floating_point Commit: c142c06f9e4788c00e65dc0cfb999feb0402d4b1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c142c06f9e47… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Sep 22 17:56:33 2009 +0200 Added some infrastructure to perform parametric tests. --- tests/Floating_Point_Expression/.gitignore | 1 + tests/Floating_Point_Expression/Makefile.am | 110 +++++++++++++++++++++++---- tests/Floating_Point_Expression/run_tests | 55 +++++++++++++ 3 files changed, 152 insertions(+), 14 deletions(-) diff --git a/tests/Floating_Point_Expression/.gitignore b/tests/Floating_Point_Expression/.gitignore new file mode 100644 index 0000000..ee6ecf8 --- /dev/null +++ b/tests/Floating_Point_Expression/.gitignore @@ -0,0 +1 @@ +dirty_marker diff --git a/tests/Floating_Point_Expression/Makefile.am b/tests/Floating_Point_Expression/Makefile.am index 1c10370..5df7796 100755 --- a/tests/Floating_Point_Expression/Makefile.am +++ b/tests/Floating_Point_Expression/Makefile.am @@ -36,10 +36,11 @@ endif !VALGRIND_TESTS_ENABLED TESTS_ENVIRONMENT = $(CHECKER) AM_CPPFLAGS = \ --I$(top_srcdir)/src \ +$(TEST_CPPFLAGS) \ -I$(top_builddir)/src \ --I$(top_srcdir)/utils \ +-I$(top_srcdir)/src \ -I$(top_srcdir)/tests \ +-I$(top_srcdir)/utils \ @extra_includes@ \ @debug_flag@ @@ -49,34 +50,115 @@ $(top_builddir)/tests/libppl_tests.a \ $(top_builddir)/src/libppl.la \ @extra_libraries@ -TESTS = linearform1 \ +ORIGINAL_TESTS = \ +bdshape1 \ floatingpointexpr1 \ +linearform1 \ octagonalshape1 \ -octagonalshape2 \ -bdshape1 +octagonalshape2 + +DERIVED_TESTS = + +ALL_TESTS = $(ORIGINAL_TESTS) $(DERIVED_TESTS) + +# This will be overridden by the `run_tests' script. +TEST_CPPFLAGS=-DANALYZER_FP_FORMAT=fl_r_oc -DANALYZED_FP_FORMAT=float_ieee754_half + +dist_check_SCRIPTS = run_tests + +TESTS = run_tests.stamp + +.PHONY: run_tests.stamp +run_tests.stamp: run_tests + +MAKE=$(MAKE) $(srcdir)/run_tests + echo "true" >run_tests.stamp + chmod +x run_tests.stamp XFAIL_TESTS = -BUGS = +# Do not change the ordering in what follows. +if SUPPORTED_FLOAT +FLOAT_INSTANCES= \ +fl_r_oc/float_ieee754_half \ +fl_r_oc/float_ieee754_single \ +fl_r_oc/float_ieee754_double \ +fl_r_oc/float_ieee754_quad \ +fl_r_oc/float_ibm_single \ +fl_r_oc/float_ibm_double \ +fl_r_oc/float_intel_double_extended +endif +if SUPPORTED_DOUBLE +DOUBLE_INSTANCES= \ +db_r_oc/float_ieee754_half \ +db_r_oc/float_ieee754_single \ +db_r_oc/float_ieee754_double \ +db_r_oc/float_ieee754_quad \ +db_r_oc/float_ibm_single \ +db_r_oc/float_ibm_double \ +db_r_oc/float_intel_double_extended +endif +if SUPPORTED_LONG_DOUBLE +LONG_DOUBLE_INSTANCES= \ +ld_r_oc/float_ieee754_half \ +ld_r_oc/float_ieee754_single \ +ld_r_oc/float_ieee754_double \ +ld_r_oc/float_ieee754_quad \ +ld_r_oc/float_ibm_single \ +ld_r_oc/float_ibm_double \ +ld_r_oc/float_intel_double_extended +endif + +# Do not change the ordering in what follows. +INSTANCES = \ +$(FLOAT_INSTANCES) \ +$(DOUBLE_INSTANCES) \ +$(LONG_DOUBLE_INSTANCES) + +print_check_PROGRAMS: + echo $(check_PROGRAMS) + +print_INSTANCES: + echo $(INSTANCES) + # # Sources for the tests # -linearform1_SOURCES = linearform1.cc +bdshape1_SOURCES = bdshape1.cc + floatingpointexpr1_SOURCES = floatingpointexpr1.cc + +linearform1_SOURCES = linearform1.cc + octagonalshape1_SOURCES = octagonalshape1.cc + octagonalshape2_SOURCES = octagonalshape2.cc -bdshape1_SOURCES = bdshape1.cc -check_PROGRAMS = \ -$(TESTS) \ -$(WATCHDOG_TESTS) \ -$(BUGS) -EXTRA_DIST = +# +# Sources and compilation flags for the derived check programs +# + +DERIVED_CXXFLAGS = -DDERIVED_TEST $(AM_CXXFLAGS) + +#nnc_frompolyhedron1_SOURCES = frompolyhedron1.cc +#nnc_frompolyhedron1_CXXFLAGS = $(DERIVED_CXXFLAGS) + +BUGS = + +check_PROGRAMS = $(ALL_TESTS) $(BUGS) + +#EXTRA_DIST = $(refinewithconstraints2_SRCS) + +#MOSTLYCLEANFILES = \ +#ascii_dump_load1.dat + +CLEANFILES = \ +run_tests.stamp -MOSTLYCLEANFILES = +DISTCLEANFILES = \ +dirty_marker $(top_builddir)/utils/libppl_utils.a: $(MAKE) $(AM_MAKEFLAGS) -C $(top_builddir)/utils libppl_utils.a diff --git a/tests/Floating_Point_Expression/run_tests b/tests/Floating_Point_Expression/run_tests new file mode 100755 index 0000000..f72431a --- /dev/null +++ b/tests/Floating_Point_Expression/run_tests @@ -0,0 +1,55 @@ +#!/bin/sh + +# Run the Floating_Point_Expression tests. +# Copyright (C) 2001-2009 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/ . + +mpz_class_XFAIL_TESTS= +mpq_class_XFAIL_TESTS= +int8_t_XFAIL_TESTS= +int16_t_XFAIL_TESTS= +int32_t_XFAIL_TESTS= +int64_t_XFAIL_TESTS= +float_XFAIL_TESTS= +double_XFAIL_TESTS= +long_double_XFAIL_TESTS= + +if [ -z "$MAKE" ] +then + MAKE=make +fi + +instances=`MAKEFLAGS='' $MAKE -s print_INSTANCES` + +check_PROGRAMS=`MAKEFLAGS='' $MAKE -s print_check_PROGRAMS` + +for instance in $instances +do + echo "**************************** " $instance " ****************************" + eval xfail_tests='"$'$instance'_XFAIL_TESTS"' + [ -f dirty_marker ] && $MAKE clean + touch dirty_marker + analyzer_fp_format=${instance%/*} + analyzed_fp_format=${instance#*/} + $MAKE check TESTS="$check_PROGRAMS" TESTS_ENVIRONMENT="$CHECKER" TEST_CPPFLAGS="-DANALYZER_FP_FORMAT=$analyzer_fp_format -DANALYZED_FP_FORMAT=$analyzed_fp_format" XFAIL_TESTS=$xfail_tests || exit 1 + $MAKE clean && rm dirty_marker +done +exit 0

1 0

[GIT] ppl/ppl(floating_point): Added a few details about other floating point formats.
by Fabio Bossi 22 Sep '09

22 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 655d6cc8016a48e74e52358d754c0e88d8edc13e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=655d6cc8016a… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 22 17:08:31 2009 +0200 Added a few details about other floating point formats. --- src/Float.defs.hh | 30 ++++++++++++++++++++++++++++++ 1 files changed, 30 insertions(+), 0 deletions(-) diff --git a/src/Float.defs.hh b/src/Float.defs.hh index e743b77..2053a9a 100644 --- a/src/Float.defs.hh +++ b/src/Float.defs.hh @@ -41,6 +41,16 @@ namespace Parma_Polyhedra_Library { /*! \ingroup PPL_CXX_interface */ #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) +struct float_ieee754_half { + static const unsigned int EXPONENT_BITS = 5; + static const unsigned int MANTISSA_BITS = 10; + static const int EXPONENT_BIAS = 15; +}; + +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS +/*! \ingroup PPL_CXX_interface */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) + struct float_ieee754_single { uint32_t word; static const uint32_t SGN_MASK = 0x80000000; @@ -115,6 +125,26 @@ struct float_ieee754_double { /*! \ingroup PPL_CXX_interface */ #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) +struct float_IBM_single { + static const unsigned int EXPONENT_BITS = 7; + static const unsigned int MANTISSA_BITS = 24; + static const int EXPONENT_BIAS = 64; +}; + +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS +/*! \ingroup PPL_CXX_interface */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) + +struct float_IBM_double { + static const unsigned int EXPONENT_BITS = 7; + static const unsigned int MANTISSA_BITS = 56; + static const int EXPONENT_BIAS = 64; +}; + +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS +/*! \ingroup PPL_CXX_interface */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) + struct float_intel_double_extended { #ifdef PPL_WORDS_BIGENDIAN uint32_t msp;

1 0

[GIT] ppl/ppl(floating_point): Small documentation corrections.
by Fabio Bossi 22 Sep '09

22 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 9b7c8767e9c0d4056c4d6e4a0696c2e43133fbc6 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9b7c8767e9c0… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 22 16:49:03 2009 +0200 Small documentation corrections. --- doc/definitions.dox | 9 ++++++--- src/Polyhedron.defs.hh | 2 +- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index dd68fd4..43a7afb 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2719,9 +2719,12 @@ composed by two parts: \f$\fund{\rho^{\#}_l}{\cV}{\mathbb{L}_a}\f$ associating each variable with its current approximating linear form. -Both stores are represented by maps of the Standard Template Library and are -required by the linearize method. Please see the documentation of floating -point expression classes for more information. +An interval abstract store is represented by a +\link Parma_Polyhedra_Library::Box \c Box \endlink with floating point +boundaries, while a linear form abstract store is a map +of the Standard Template Library. The <CODE>linearize</CODE> method requires +both stores as its arguments. Please see the documentation of floating point +expression classes for more information. The linearization of a floating point expression \f$e\f$ in the composite abstract store \f$\left \langle \rho^{\#}, \rho^{\#}_l \right \rangle\f$ will diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index 55d7c44..b402794 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -2673,7 +2673,7 @@ protected: It should be the result of an application of static method <CODE>overapproximate_linear_form</CODE>. - \param l_dimension + \param lf_dimension Must be the space dimension of \p lf. \param result

1 0

[GIT] ppl/ppl(floating_point): Adapted test files to new representation of interval abstract stores.
by Roberto Amadini 22 Sep '09

22 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 2b4f0299f6b37e644ac34f43601d0bfbbc6cf7e1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2b4f0299f6b3… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Tue Sep 22 16:37:05 2009 +0200 Adapted test files to new representation of interval abstract stores. --- .../floatingpointexpr1.cc | 66 ++++++++------------ tests/Floating_Point_Expression/octagonalshape2.cc | 22 +++--- 2 files changed, 38 insertions(+), 50 deletions(-) diff --git a/tests/Floating_Point_Expression/floatingpointexpr1.cc b/tests/Floating_Point_Expression/floatingpointexpr1.cc index 6763b9d..f39bca0 100644 --- a/tests/Floating_Point_Expression/floatingpointexpr1.cc +++ b/tests/Floating_Point_Expression/floatingpointexpr1.cc @@ -81,22 +81,10 @@ typedef Opposite_Floating_Point_Expression<db_r_oc, float_ieee754_single> opp_fpeds; typedef Opposite_Floating_Point_Expression<db_r_oc, float_ieee754_double> opp_fpedd; - -typedef Floating_Point_Expression<fl_r_oc, - float_ieee754_single>::FP_Interval_Abstract_Store sstr; -typedef Floating_Point_Expression<db_r_oc, - float_ieee754_single>::FP_Interval_Abstract_Store dstr; - typedef Floating_Point_Expression<fl_r_oc, float_ieee754_single>::FP_Linear_Form_Abstract_Store lsstr; typedef Floating_Point_Expression<db_r_oc, float_ieee754_single>::FP_Linear_Form_Abstract_Store ldstr; - -typedef Floating_Point_Expression<fl_r_oc, - float_ieee754_double>::FP_Interval_Abstract_Store sdtr; -typedef Floating_Point_Expression<db_r_oc, - float_ieee754_double>::FP_Interval_Abstract_Store ddtr; - typedef Floating_Point_Expression<fl_r_oc, float_ieee754_double>::FP_Linear_Form_Abstract_Store lsdtr; typedef Floating_Point_Expression<db_r_oc, @@ -138,7 +126,7 @@ test02() { div_fpess div(num, den); try { Float_Interval_Linear_Form result; - div.linearize(sstr(), lsstr(), result); + div.linearize(Box<fl_r_oc>(0), lsstr(), result); } catch (Linearization_Failed e) { nout << "*** Linearization failed due to division by zero. ***" << endl; @@ -150,9 +138,9 @@ test02() { // Tests multiplication by zero. bool test03() { - sstr store_fl; - store_fl[0] = fl_r_oc(0); - store_fl[1] = fl_r_oc(10); + Box<fl_r_oc> store_fl(2); + store_fl.set_interval(Variable(0), fl_r_oc(0)); + store_fl.set_interval(Variable(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); @@ -168,9 +156,9 @@ test03() { << 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); + Box<db_r_oc> store_db(2); + store_db.set_interval(Variable(0), db_r_oc(0)); + store_db.set_interval(Variable(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); @@ -199,7 +187,7 @@ test04() { store_fl[0] = known_result_fl; var_fpesd var_fl(0); Float_Interval_Linear_Form result_fl; - var_fl.linearize(sdtr(), store_fl, result_fl); + var_fl.linearize(Box<fl_r_oc>(0), store_fl, result_fl); nout << "*** known_result_fl ***" << endl << known_result_fl << endl; @@ -211,7 +199,7 @@ test04() { store_db[0] = known_result_db; var_fpedd var_db(0); Double_Interval_Linear_Form result_db; - var_db.linearize(ddtr(), store_db, result_db); + var_db.linearize(Box<db_r_oc>(0), store_db, result_db); nout << "*** known_result_db ***" << endl << known_result_db << endl; @@ -223,10 +211,10 @@ test04() { // Tests the linearization of A + B. bool test05() { - dstr store; db_r_oc tmp; - store[0] = tmp; - store[1] = tmp; + Box<db_r_oc> store(2); + store.set_interval(Variable(0), tmp); + store.set_interval(Variable(1), tmp); var_fpeds* var0 = new var_fpeds(0); var_fpeds* var1 = new var_fpeds(1); sum_fpeds sum(var0, var1); @@ -253,10 +241,10 @@ test05() { // Tests the linearization of A - B. bool test06() { - sstr store; fl_r_oc tmp; - store[0] = tmp; - store[1] = tmp; + Box<fl_r_oc> store(2); + store.set_interval(Variable(0), tmp); + store.set_interval(Variable(1), tmp); var_fpess* var0 = new var_fpess(0); var_fpess* var1 = new var_fpess(1); dif_fpess dif(var0, var1); @@ -283,11 +271,11 @@ test06() { // Tests the linearization of A * B where A = [0, 1] and B = [2, 2]. bool test07() { - sstr store; + Box<fl_r_oc> store(2); fl_r_oc tmp(0); tmp.join_assign(1); - store[0] = tmp; - store[1] = fl_r_oc(2); + store.set_interval(Variable(0), tmp); + store.set_interval(Variable(1), fl_r_oc(2)); var_fpess* var0 = new var_fpess(0); var_fpess* var1 = new var_fpess(1); mul_fpess mul(var0, var1); @@ -309,14 +297,14 @@ test07() { return result == known_result; } -// Tests the linearization of A / B where A = [1, 4] and B = [2, 2]. +// Tests the linearization of A / B where A = [0, 1] and B = [2, 2]. bool test08() { - ddtr store; + Box<db_r_oc> store(2); db_r_oc tmp(0); tmp.join_assign(1); - store[0] = tmp; - store[1] = db_r_oc(2); + store.set_interval(Variable(0), tmp); + store.set_interval(Variable(1), db_r_oc(2)); var_fpedd* var0 = new var_fpedd(0); var_fpedd* var1 = new var_fpedd(1); div_fpedd div(var0, var1); @@ -341,10 +329,10 @@ test08() { // Tests the linearization of [1/4, 1/2] * (-A) where A = [1, 10]. bool test09() { - sdtr store; + Box<fl_r_oc> store(1); fl_r_oc tmp(1); tmp.join_assign(10); - store[0] = tmp; + store.set_interval(Variable(0), tmp); con_fpesd* con = new con_fpesd(1 / 4.0, 1 / 2.0); var_fpesd* var0 = new var_fpesd(0); opp_fpesd* opp = new opp_fpesd(var0); @@ -381,7 +369,7 @@ test10() { con_fpess* con3 = new con_fpess(0, 0); mul_fpess mul(con3, sum); Float_Interval_Linear_Form result; - mul.linearize(sstr(), lsstr(), result); + mul.linearize(Box<fl_r_oc>(), lsstr(), result); nout << "*** known_result1 ***" << endl << known_result1 << endl; @@ -398,7 +386,7 @@ test10() { con_fpedd* con6 = new con_fpedd(0, 0); mul_fpedd mul2(sum2, con6); Double_Interval_Linear_Form result2; - mul2.linearize(ddtr(), lddtr(), result2); + mul2.linearize(Box<db_r_oc>(), lddtr(), result2); nout << "*** known_result2 ***" << endl << known_result2 << endl; @@ -414,7 +402,7 @@ test10() { bool ok3 = false; try { - mul3.linearize(ddtr(), lddtr(), result2); + mul3.linearize(Box<db_r_oc>(), lddtr(), result2); } catch (Linearization_Failed e) { nout << "*** Linearization failed due to overflow. ***" << endl; diff --git a/tests/Floating_Point_Expression/octagonalshape2.cc b/tests/Floating_Point_Expression/octagonalshape2.cc index cbba75d..a3f2785 100644 --- a/tests/Floating_Point_Expression/octagonalshape2.cc +++ b/tests/Floating_Point_Expression/octagonalshape2.cc @@ -23,8 +23,6 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "ppl_test.hh" -typedef Floating_Point_Expression<db_r_oc, float_ieee754_double>::FP_Interval_Abstract_Store ddtr; - namespace { // tests trivial cases @@ -412,13 +410,13 @@ bool test11() { Variable A(0); Variable B(1); - ddtr store; + Box<db_r_oc> store(2); db_r_oc tmp(-2.5); tmp.join_assign(3.5); - store[0] = tmp; + store.set_interval(A, tmp); tmp.lower() = -4; tmp.upper() = 4; - store[1] = tmp; + store.set_interval(B, tmp); Octagonal_Shape<double> oc1(2); oc1.add_constraint(A <= 2); oc1.add_constraint(B <= 2); @@ -426,25 +424,27 @@ test11() { oc1.add_constraint(2*B >= -3); oc1.refine_fp_interval_abstract_store(store); - nout << "*** store[0] ***" << endl - << store[0] << endl; + tmp = store.get_interval(A); + nout << "*** store.get_interval(A) ***" << endl + << tmp << endl; db_r_oc known_result1(-2.5); known_result1.join_assign(2); nout << "*** known_result1 ***" << endl << known_result1 << endl; - bool ok1 = (store[0] == known_result1); + bool ok1 = (tmp == known_result1); - nout << "*** store[1] ***" << endl - << store[1] << endl; + tmp = store.get_interval(B); + nout << "*** store.get_interval(B) ***" << endl + << tmp << endl; db_r_oc known_result2(-1.5); known_result2.join_assign(2); nout << "*** known_result2 ***" << endl << known_result2 << endl; - bool ok2 = (store[1] == known_result2); + bool ok2 = (tmp == known_result2); return ok1 && ok2; }

1 0

[GIT] ppl/ppl(floating_point): Added missing static casts so that tests now pass again.
by Fabio Bossi 22 Sep '09

22 Sep '09

Module: ppl/ppl Branch: floating_point Commit: d8e7d618dd4a429e1f9b80aacf5c4477d9f5aca3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d8e7d618dd4a… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 22 15:54:49 2009 +0200 Added missing static casts so that tests now pass again. --- src/Floating_Point_Expression.defs.hh | 2 +- src/Floating_Point_Expression.templates.hh | 5 ++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/Floating_Point_Expression.defs.hh b/src/Floating_Point_Expression.defs.hh index f0cd9c5..effb30d 100644 --- a/src/Floating_Point_Expression.defs.hh +++ b/src/Floating_Point_Expression.defs.hh @@ -193,7 +193,7 @@ typename Floating_Point_Expression<FP_Interval_Type, FP_Format>::boundary_type Floating_Point_Expression<FP_Interval_Type, FP_Format>::absolute_error = std::max(static_cast<typename Floating_Point_Expression<FP_Interval_Type, FP_Format>::boundary_type> - (pow(2, 1 - FP_Format::EXPONENT_BIAS - FP_Format::MANTISSA_BITS)), + (pow(2, static_cast<typename Floating_Point_Expression<FP_Interval_Type, FP_Format>::boundary_type>(1) - FP_Format::EXPONENT_BIAS - FP_Format::MANTISSA_BITS)), std::numeric_limits<typename Floating_Point_Expression<FP_Interval_Type, FP_Format> ::boundary_type>::denorm_min()); diff --git a/src/Floating_Point_Expression.templates.hh b/src/Floating_Point_Expression.templates.hh index 17e796d..0343bff 100644 --- a/src/Floating_Point_Expression.templates.hh +++ b/src/Floating_Point_Expression.templates.hh @@ -35,10 +35,9 @@ 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::MANTISSA_BITS) precisely. */ - FP_Interval_Type error_propagator(-pow(2, -FP_Format::MANTISSA_BITS)); + FP_Interval_Type error_propagator(-pow(2, -static_cast<typename Floating_Point_Expression<FP_Interval_Type, FP_Format>::boundary_type>(FP_Format::MANTISSA_BITS))); // FIXME: this may be incorrect for some policies. - error_propagator.join_assign(FP_Interval_Type( - pow(2, -FP_Format::MANTISSA_BITS))); + error_propagator.join_assign(FP_Interval_Type(pow(2, -static_cast<typename Floating_Point_Expression<FP_Interval_Type, FP_Format>::boundary_type>(FP_Format::MANTISSA_BITS)))); // Handle the inhomogeneous term. const FP_Interval_Type* current_term = &lf.inhomogeneous_term();

1 0

[GIT] ppl/ppl(floating_point): Use Box to represent an interval abstract store.
by Fabio Bossi 22 Sep '09

22 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 79572e84de987a3e979f8629b3f468659dee2d84 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=79572e84de98… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 22 15:46:05 2009 +0200 Use Box to represent an interval abstract store. --- src/Floating_Point_Expression.defs.hh | 10 +++++-- src/Floating_Point_Expression.inlines.hh | 1 + src/Floating_Point_Expression.templates.hh | 9 +++--- src/Octagonal_Shape.defs.hh | 3 +- src/Octagonal_Shape.templates.hh | 32 ++-------------------- src/Polyhedron.defs.hh | 2 +- src/Polyhedron.templates.hh | 39 ++------------------------- 7 files changed, 21 insertions(+), 75 deletions(-) diff --git a/src/Floating_Point_Expression.defs.hh b/src/Floating_Point_Expression.defs.hh index 6d6b336..f0cd9c5 100644 --- a/src/Floating_Point_Expression.defs.hh +++ b/src/Floating_Point_Expression.defs.hh @@ -25,7 +25,8 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "globals.defs.hh" #include "Floating_Point_Expression.types.hh" -#include "Linear_Form.defs.hh" +#include "Linear_Form.types.hh" +#include "Box.types.hh" #include <cmath> #include <map> @@ -62,11 +63,14 @@ public: typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; //! Alias for a map that associates a variable index to an interval. - /*! + /*! \brief + Alias for a Box storing lower and upper bounds for floating point + variables. + The type a linear form abstract store associating each variable with an interval that correctly approximates its value. */ - typedef std::map<dimension_type, FP_Interval_Type> FP_Interval_Abstract_Store; + typedef Box<FP_Interval_Type> FP_Interval_Abstract_Store; //! Alias for a map that associates a variable index to a linear form. /*! diff --git a/src/Floating_Point_Expression.inlines.hh b/src/Floating_Point_Expression.inlines.hh index 3e38dd2..f55488e 100644 --- a/src/Floating_Point_Expression.inlines.hh +++ b/src/Floating_Point_Expression.inlines.hh @@ -24,6 +24,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #define PPL_Floating_Point_Expression_inlines_hh 1 #include "globals.defs.hh" +#include "Linear_Form.defs.hh" namespace Parma_Polyhedra_Library { diff --git a/src/Floating_Point_Expression.templates.hh b/src/Floating_Point_Expression.templates.hh index 557cddc..17e796d 100644 --- a/src/Floating_Point_Expression.templates.hh +++ b/src/Floating_Point_Expression.templates.hh @@ -24,6 +24,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #ifndef PPL_Floating_Point_Expression_templates_hh #define PPL_Floating_Point_Expression_templates_hh 1 +#include "Linear_Form.defs.hh" #include <cmath> namespace Parma_Polyhedra_Library { @@ -70,12 +71,12 @@ Floating_Point_Expression<FP_Interval_Type, FP_Format> FP_Interval_Type& result) { result = FP_Interval_Type(lf.inhomogeneous_term()); dimension_type dimension = lf.space_dimension(); + assert(dimension <= store.space_dimension()); for (dimension_type i = 0; i < dimension; ++i) { - typename FP_Interval_Abstract_Store::const_iterator - next_variable_value = store.find(i); - assert(next_variable_value != store.end()); FP_Interval_Type current_addend = lf.coefficient(Variable(i)); - current_addend *= next_variable_value->second; + const FP_Interval_Type& curr_int = store.get_interval(Variable(i)); + assert(curr_int.is_bounded()); + current_addend *= curr_int; result += current_addend; } diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 6f910d2..81ddf92 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -1746,8 +1746,7 @@ public: */ template <typename Interval_Info> void refine_fp_interval_abstract_store( - std::map< dimension_type, Interval<T, Interval_Info> >& store) - const; + Box< Interval<T, Interval_Info> >& store) const; //@} // Member Functions that May Modify the Dimension of the Vector Space diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index e3ae567..04906d6 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -30,6 +30,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Interval.defs.hh" #include "Linear_Form.defs.hh" #include "meta_programming.hh" +#include "Box.defs.hh" #include "assert.hh" #include <vector> #include <map> @@ -5426,43 +5427,16 @@ template <typename Interval_Info> void Octagonal_Shape<T>:: refine_fp_interval_abstract_store( - std::map< dimension_type, Interval<T, Interval_Info> >& store) const { + Box< Interval<T, Interval_Info> >& store) const { // Check that T is a floating point type. PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact, "Octagonal_Shape<T>::refine_fp_interval_abstract_store:" " T not a floating point type."); - strong_closure_assign(); - typedef Interval<T, Interval_Info> FP_Interval_Type; - typedef typename std::map<dimension_type, FP_Interval_Type>::iterator - Map_Iterator; - - PPL_DIRTY_TEMP(N, upper_bound); - Map_Iterator store_end = store.end(); - for (Map_Iterator ite = store.begin(); ite != store_end; ++ite) { - dimension_type curr_var = ite->first; - PPL_ASSERT(curr_var < space_dim); - dimension_type n_curr_var = curr_var * 2; - FP_Interval_Type& curr_int = ite->second; - T& lb = curr_int.lower(); - T& ub = curr_int.upper(); - // Now get the upper bound for curr_var in the octagon. - assign_r(upper_bound, matrix[n_curr_var+1][n_curr_var], ROUND_NOT_NEEDED); - div_2exp_assign_r(upper_bound, upper_bound, 1, ROUND_UP); - - if (upper_bound < ub) - ub = upper_bound.raw_value(); - - // Now get the lower bound for curr_var in the octagon. - neg_assign_r(upper_bound, matrix[n_curr_var][n_curr_var+1], - ROUND_NOT_NEEDED); - div_2exp_assign_r(upper_bound, upper_bound, 1, ROUND_DOWN); + store.intersection_assign(Box<FP_Interval_Type>(*this)); - if (upper_bound > lb) - lb = upper_bound.raw_value(); - } } template <typename T> diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index 7f17172..55d7c44 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -1018,7 +1018,7 @@ public: */ template <typename FP_Format, typename Interval_Info> void refine_fp_interval_abstract_store( - std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) + Box< Interval<FP_Format, Interval_Info> >& store) const; /*! \brief diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index 8ad8b01..c312028 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -543,8 +543,7 @@ template <typename FP_Format, typename Interval_Info> void Polyhedron:: refine_fp_interval_abstract_store( - std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) - const { + Box< Interval<FP_Format, Interval_Info> >& store) const { // Check that FP_Format is indeed a floating point type. PPL_COMPILE_TIME_CHECK(!std::numeric_limits<FP_Format>::is_exact, @@ -552,40 +551,8 @@ refine_fp_interval_abstract_store( " T not a floating point type."); typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; - typedef typename std::map<dimension_type, FP_Interval_Type>::iterator - Map_Iterator; - - // FIXME: there could be restrictions on Interval_Info. - Box<FP_Interval_Type> limits(*this); - PPL_DIRTY_TEMP_COEFFICIENT(numerator); - PPL_DIRTY_TEMP_COEFFICIENT(denominator); - Map_Iterator store_end = store.end(); - for (Map_Iterator ite = store.begin(); ite != store_end; ++ite) { - dimension_type curr_var = ite->first; - PPL_ASSERT(curr_var < space_dim); - Variable var(curr_var); - Linear_Expression var_exp(var); - bool dummy; - FP_Interval_Type& curr_int = ite->second; - FP_Format& lb = curr_int.lower(); - FP_Format& ub = curr_int.upper(); - FP_Format comparison_term; - mpq_class tmp_rational; - if (limits.minimize(var_exp, numerator, denominator, dummy)) { - assign_r(tmp_rational.get_num(), numerator, ROUND_NOT_NEEDED); - assign_r(tmp_rational.get_den(), denominator, ROUND_NOT_NEEDED); - assign_r(comparison_term, tmp_rational, ROUND_DOWN); - if (comparison_term > lb) - lb = comparison_term; - } - if (limits.maximize(var_exp, numerator, denominator, dummy)) { - assign_r(tmp_rational.get_num(), numerator, ROUND_NOT_NEEDED); - assign_r(tmp_rational.get_den(), denominator, ROUND_NOT_NEEDED); - assign_r(comparison_term, tmp_rational, ROUND_UP); - if (comparison_term < ub) - ub = comparison_term; - } - } + store.intersection_assign(Box<FP_Interval_Type>(*this)); + } template <typename C>

1 0

[GIT] ppl/ppl(floating_point): Replaced typedefs according to the new policies.
by Roberto Amadini 22 Sep '09

22 Sep '09

Module: ppl/ppl Branch: floating_point Commit: e2b71307d51988448bcc885d7637c7f111fce86a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e2b71307d519… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Tue Sep 22 15:47:37 2009 +0200 Replaced typedefs according to the new policies. --- .../floatingpointexpr1.cc | 122 ++++++++++++-------- tests/Floating_Point_Expression/octagonalshape2.cc | 2 +- 2 files changed, 77 insertions(+), 47 deletions(-) diff --git a/tests/Floating_Point_Expression/floatingpointexpr1.cc b/tests/Floating_Point_Expression/floatingpointexpr1.cc index 624f00f..6763b9d 100644 --- a/tests/Floating_Point_Expression/floatingpointexpr1.cc +++ b/tests/Floating_Point_Expression/floatingpointexpr1.cc @@ -25,51 +25,82 @@ site: http://www.cs.unipr.it/ppl/ . */ 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; - -typedef Floating_Point_Expression<fl_r_oc, IEEE754_Single>::FP_Interval_Abstract_Store sstr; -typedef Floating_Point_Expression<db_r_oc, IEEE754_Single>::FP_Interval_Abstract_Store dstr; - -typedef Floating_Point_Expression<fl_r_oc, IEEE754_Single>::FP_Linear_Form_Abstract_Store lsstr; -typedef Floating_Point_Expression<db_r_oc, IEEE754_Single>::FP_Linear_Form_Abstract_Store ldstr; - -typedef Floating_Point_Expression<fl_r_oc, IEEE754_Double>::FP_Interval_Abstract_Store sdtr; -typedef 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 Floating_Point_Expression<db_r_oc, IEEE754_Double>::FP_Linear_Form_Abstract_Store lddtr; +typedef Division_Floating_Point_Expression<fl_r_oc, + float_ieee754_single> div_fpess; +typedef Division_Floating_Point_Expression<fl_r_oc, + float_ieee754_double> div_fpesd; +typedef Difference_Floating_Point_Expression<fl_r_oc, + float_ieee754_single> dif_fpess; +typedef Difference_Floating_Point_Expression<fl_r_oc, + float_ieee754_double> dif_fpesd; +typedef Multiplication_Floating_Point_Expression<fl_r_oc, + float_ieee754_single> mul_fpess; +typedef Multiplication_Floating_Point_Expression<fl_r_oc, + float_ieee754_double> mul_fpesd; +typedef Sum_Floating_Point_Expression<fl_r_oc, + float_ieee754_single> sum_fpess; +typedef Sum_Floating_Point_Expression<fl_r_oc, + float_ieee754_double> sum_fpesd; +typedef Constant_Floating_Point_Expression<fl_r_oc, + float_ieee754_single> con_fpess; +typedef Constant_Floating_Point_Expression<fl_r_oc, + float_ieee754_double> con_fpesd; +typedef Variable_Floating_Point_Expression<fl_r_oc, + float_ieee754_single> var_fpess; +typedef Variable_Floating_Point_Expression<fl_r_oc, + float_ieee754_double> var_fpesd; +typedef Opposite_Floating_Point_Expression<fl_r_oc, + float_ieee754_single> opp_fpess; +typedef Opposite_Floating_Point_Expression<fl_r_oc, + float_ieee754_double> opp_fpesd; +typedef Division_Floating_Point_Expression<db_r_oc, + float_ieee754_single> div_fpeds; +typedef Division_Floating_Point_Expression<db_r_oc, + float_ieee754_double> div_fpedd; +typedef Difference_Floating_Point_Expression<db_r_oc, + float_ieee754_single> dif_fpeds; +typedef Difference_Floating_Point_Expression<db_r_oc, + float_ieee754_double> dif_fpedd; +typedef Multiplication_Floating_Point_Expression<db_r_oc, + float_ieee754_single> mul_fpeds; +typedef Multiplication_Floating_Point_Expression<db_r_oc, + float_ieee754_double> mul_fpedd; +typedef Sum_Floating_Point_Expression<db_r_oc, + float_ieee754_single> sum_fpeds; +typedef Sum_Floating_Point_Expression<db_r_oc, + float_ieee754_double> sum_fpedd; +typedef Constant_Floating_Point_Expression<db_r_oc, + float_ieee754_single> con_fpeds; +typedef Constant_Floating_Point_Expression<db_r_oc, + float_ieee754_double> con_fpedd; +typedef Variable_Floating_Point_Expression<db_r_oc, + float_ieee754_single> var_fpeds; +typedef Variable_Floating_Point_Expression<db_r_oc, + float_ieee754_double> var_fpedd; +typedef Opposite_Floating_Point_Expression<db_r_oc, + float_ieee754_single> opp_fpeds; +typedef Opposite_Floating_Point_Expression<db_r_oc, + float_ieee754_double> opp_fpedd; + +typedef Floating_Point_Expression<fl_r_oc, + float_ieee754_single>::FP_Interval_Abstract_Store sstr; +typedef Floating_Point_Expression<db_r_oc, + float_ieee754_single>::FP_Interval_Abstract_Store dstr; + +typedef Floating_Point_Expression<fl_r_oc, + float_ieee754_single>::FP_Linear_Form_Abstract_Store lsstr; +typedef Floating_Point_Expression<db_r_oc, + float_ieee754_single>::FP_Linear_Form_Abstract_Store ldstr; + +typedef Floating_Point_Expression<fl_r_oc, + float_ieee754_double>::FP_Interval_Abstract_Store sdtr; +typedef Floating_Point_Expression<db_r_oc, + float_ieee754_double>::FP_Interval_Abstract_Store ddtr; + +typedef Floating_Point_Expression<fl_r_oc, + float_ieee754_double>::FP_Linear_Form_Abstract_Store lsdtr; +typedef Floating_Point_Expression<db_r_oc, + float_ieee754_double>::FP_Linear_Form_Abstract_Store lddtr; namespace { @@ -129,7 +160,6 @@ test03() { 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); diff --git a/tests/Floating_Point_Expression/octagonalshape2.cc b/tests/Floating_Point_Expression/octagonalshape2.cc index 5c9a7bc..cbba75d 100644 --- a/tests/Floating_Point_Expression/octagonalshape2.cc +++ b/tests/Floating_Point_Expression/octagonalshape2.cc @@ -23,7 +23,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "ppl_test.hh" -typedef Floating_Point_Expression<db_r_oc, IEEE754_Double>::FP_Interval_Abstract_Store ddtr; +typedef Floating_Point_Expression<db_r_oc, float_ieee754_double>::FP_Interval_Abstract_Store ddtr; namespace {

1 0

[GIT] ppl/ppl(floating_point): Refactoring of test files into test/ Floating_Point_Expression.
by Roberto Amadini 22 Sep '09

22 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 4e2e5ca265d96893834be726b5f359255e506aaa URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4e2e5ca265d9… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Tue Sep 22 14:02:34 2009 +0200 Refactoring of test files into test/Floating_Point_Expression. --- tests/Floating_Point_Expression/Makefile.am | 12 ++++--- .../linearform1.cc | 30 ++++++++++++++----- .../{affineimage3.cc => octagonalshape1.cc} | 0 .../{refinelf1.cc => octagonalshape2.cc} | 0 tests/Polyhedron/Makefile.am | 3 -- 5 files changed, 29 insertions(+), 16 deletions(-) diff --git a/tests/Floating_Point_Expression/Makefile.am b/tests/Floating_Point_Expression/Makefile.am index baaf213..1c10370 100755 --- a/tests/Floating_Point_Expression/Makefile.am +++ b/tests/Floating_Point_Expression/Makefile.am @@ -49,9 +49,10 @@ $(top_builddir)/tests/libppl_tests.a \ $(top_builddir)/src/libppl.la \ @extra_libraries@ -TESTS = floatingpointexpr1 \ -affineimage3 \ -refinelf1 \ +TESTS = linearform1 \ +floatingpointexpr1 \ +octagonalshape1 \ +octagonalshape2 \ bdshape1 XFAIL_TESTS = @@ -62,9 +63,10 @@ BUGS = # Sources for the tests # +linearform1_SOURCES = linearform1.cc floatingpointexpr1_SOURCES = floatingpointexpr1.cc -affineimage3_SOURCES = affineimage3.cc -refinelf1_SOURCES = refinelf1.cc +octagonalshape1_SOURCES = octagonalshape1.cc +octagonalshape2_SOURCES = octagonalshape2.cc bdshape1_SOURCES = bdshape1.cc check_PROGRAMS = \ diff --git a/tests/Polyhedron/linearform1.cc b/tests/Floating_Point_Expression/linearform1.cc similarity index 94% rename from tests/Polyhedron/linearform1.cc rename to tests/Floating_Point_Expression/linearform1.cc index c6ba2ab..3f3f42a 100644 --- a/tests/Polyhedron/linearform1.cc +++ b/tests/Floating_Point_Expression/linearform1.cc @@ -1,4 +1,4 @@ -/* Testing Linear_Expression. +/* Testing Linear_Form on floating point intervals. Copyright (C) 2001-2009 Roberto Bagnara <bagnara(a)cs.unipr.it> This file is part of the Parma Polyhedra Library (PPL). @@ -243,38 +243,52 @@ test08() { ok2 = true; } - Linear_Form<db_r_oc> g; bool ok3 = false; try { - g = f - A; + f -= A; } catch(std::length_error e) { - nout << "Overflow in operator-(Linear_Form<C>& f, const Variable v)." + nout << "Overflow in operator-=(Linear_Form<C>& f, const Variable v)." << endl; + Variable B(1); + Variable C(2); + Linear_Form<db_r_oc> g(B); + g -= C; ok3 = true; } + Linear_Form<db_r_oc> g; bool ok4 = false; try { - g = A - f; + g = f - A; } catch(std::length_error e) { - nout << "Overflow in operator-(const Variable v, Linear_Form<C>& f)." + nout << "Overflow in operator-(Linear_Form<C>& f, const Variable v)." << endl; ok4 = true; } bool ok5 = false; try { + g = A - f; + } + catch(std::length_error e) { + nout << "Overflow in operator-(const Variable v, Linear_Form<C>& f)." + << endl; + ok5 = true; + } + + bool ok6 = false; + try { g = A + f; } catch(std::length_error e) { nout << "Overflow in operator+(const Variable v, Linear_Form<C>& f)." << endl; - ok5 = true; + ok6 = true; } - return ok1 && ok2 && ok3 && ok4 && ok5; + return ok1 && ok2 && ok3 && ok4 && ok5 && ok6; } } // namespace diff --git a/tests/Floating_Point_Expression/affineimage3.cc b/tests/Floating_Point_Expression/octagonalshape1.cc similarity index 100% rename from tests/Floating_Point_Expression/affineimage3.cc rename to tests/Floating_Point_Expression/octagonalshape1.cc diff --git a/tests/Floating_Point_Expression/refinelf1.cc b/tests/Floating_Point_Expression/octagonalshape2.cc similarity index 100% rename from tests/Floating_Point_Expression/refinelf1.cc rename to tests/Floating_Point_Expression/octagonalshape2.cc diff --git a/tests/Polyhedron/Makefile.am b/tests/Polyhedron/Makefile.am index 2c7db48..fa094e5 100644 --- a/tests/Polyhedron/Makefile.am +++ b/tests/Polyhedron/Makefile.am @@ -101,7 +101,6 @@ limitedbhrz03extrapolation1 \ limitedh79extrapolation1 \ linearpartition1 \ linearexpression1 \ -linearform1 \ linearsystem1 \ mapspacedims1 \ matrix1 \ @@ -335,8 +334,6 @@ linearpartition1_SOURCES = linearpartition1.cc linearexpression1_SOURCES = linearexpression1.cc -linearform1_SOURCES = linearform1.cc - linearsystem1_SOURCES = linearsystem1.cc mapspacedims1_SOURCES = mapspacedims1.cc

1 0

[GIT] ppl/ppl(floating_point): Adapted the class to the policies defined in Float.defs.hh.
by Fabio Bossi 22 Sep '09

22 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 96ade840e5152064796d08ef099b735ecabe21a6 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=96ade840e515… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 22 13:51:48 2009 +0200 Adapted the class to the policies defined in Float.defs.hh. --- src/Floating_Point_Expression.defs.hh | 60 ++-------------------------- src/Floating_Point_Expression.templates.hh | 6 +- 2 files changed, 7 insertions(+), 59 deletions(-) diff --git a/src/Floating_Point_Expression.defs.hh b/src/Floating_Point_Expression.defs.hh index ffaf2b7..6d6b336 100644 --- a/src/Floating_Point_Expression.defs.hh +++ b/src/Floating_Point_Expression.defs.hh @@ -34,54 +34,6 @@ namespace Parma_Polyhedra_Library { //! Exception class indicating the failure of a linearization attempt. class Linearization_Failed {}; -/* - FIXME: considering adapting the whole code of Floating_Point_Expression - to use the policies defined in Float.defs.hh instead of the following - ones that contain duplicate information. -*/ - -//! Policy class defining the IEEE754 half precision format. -struct IEEE754_Half { - static const unsigned short fraction_bits = 10; - static const unsigned short exponent_bits = 5; - static const unsigned short exponent_bias = 15; -}; - -//! Policy class defining the IEEE754 single precision format. -struct IEEE754_Single { - static const unsigned short fraction_bits = 23; - static const unsigned short exponent_bits = 8; - static const unsigned short exponent_bias = 127; -}; - -//! Policy class defining the IEEE754 double precision format. -struct IEEE754_Double { - static const unsigned short fraction_bits = 52; - static const unsigned short exponent_bits = 11; - static const unsigned short exponent_bias = 1023; -}; - -//! Policy class defining the IEEE754 quadruple precision format. -struct IEEE754_Quadruple { - static const unsigned short fraction_bits = 112; - static const unsigned short exponent_bits = 15; - static const unsigned short exponent_bias = 16383; -}; - -//! Policy class defining the IBM single precision format. -struct IBM_Single { - static const unsigned short fraction_bits = 24; - static const unsigned short exponent_bits = 7; - static const unsigned short exponent_bias = 64; -}; - -//! Policy class defining the IBM double precision format. -struct IBM_Double { - static const unsigned short fraction_bits = 56; - static const unsigned short exponent_bits = 7; - static const unsigned short exponent_bias = 64; -}; - /*! \brief \ingroup PPL_CXX_Interface A floating point expression on a given format. @@ -97,13 +49,9 @@ struct IBM_Double { should have a floating point type. - The class template type parameter \p FP_Format represents the floating point format used in the concrete domain. - This parameter must be a struct which contains three fields: - -# <CODE>static const unsigned short fraction_bits</CODE> that represents - the number of bits of the fraction. - -# <CODE>static const unsigned short exponent_bits</CODE> that represents - the number of bits of the exponent. - -# <CODE>static const unsigned short exponent_bias</CODE> that represents - the value of exponent bias. + This parameter must be a struct similar to the ones defined in file + Float.defs.hh, even though it is sufficient to define the two + fields MANTISSA_BITS and EXPONENT_BIAS. */ template <typename FP_Interval_Type, typename FP_Format> class Floating_Point_Expression { @@ -241,7 +189,7 @@ typename Floating_Point_Expression<FP_Interval_Type, FP_Format>::boundary_type Floating_Point_Expression<FP_Interval_Type, FP_Format>::absolute_error = std::max(static_cast<typename Floating_Point_Expression<FP_Interval_Type, FP_Format>::boundary_type> - (pow(2, 1 - FP_Format::exponent_bias - FP_Format::fraction_bits)), + (pow(2, 1 - FP_Format::EXPONENT_BIAS - FP_Format::MANTISSA_BITS)), std::numeric_limits<typename Floating_Point_Expression<FP_Interval_Type, FP_Format> ::boundary_type>::denorm_min()); diff --git a/src/Floating_Point_Expression.templates.hh b/src/Floating_Point_Expression.templates.hh index 8c5ce32..557cddc 100644 --- a/src/Floating_Point_Expression.templates.hh +++ b/src/Floating_Point_Expression.templates.hh @@ -33,11 +33,11 @@ void 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)); + (2)^(-FP_Format::MANTISSA_BITS) precisely. */ + FP_Interval_Type error_propagator(-pow(2, -FP_Format::MANTISSA_BITS)); // FIXME: this may be incorrect for some policies. error_propagator.join_assign(FP_Interval_Type( - pow(2, -FP_Format::fraction_bits))); + pow(2, -FP_Format::MANTISSA_BITS))); // Handle the inhomogeneous term. const FP_Interval_Type* current_term = &lf.inhomogeneous_term();

1 0