July 2010 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): Added method get_integer_interval() ( make check not working yet).
by Fabio Bossi 28 Jul '10

28 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 986fb317391e4e937a918d53a955594f2abe84c6 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=986fb317391e… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Jul 28 19:03:22 2010 +0200 Added method get_integer_interval() (make check not working yet). --- src/Concrete_Expression.defs.hh | 27 +++++++++++- tests/Concrete_Expression/C_Expr.defs.hh | 63 ++++++++++++++++++++++++++- tests/Concrete_Expression/C_Expr.inlines.hh | 40 +++++++++++++++++ tests/Concrete_Expression/linearize.cc | 24 ++++++----- 4 files changed, 141 insertions(+), 13 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=986fb317…

1 0

[GIT] ppl/ppl(floating_point): Avoid dangerous casts when computing errors.
by Fabio Bossi 28 Jul '10

28 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 5a827fc7a229ed6474101c2d951da3aa14c2d358 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5a827fc7a229… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Jul 28 11:51:32 2010 +0200 Avoid dangerous casts when computing errors. --- src/Float.templates.hh | 12 ++++++------ src/Linear_Form.templates.hh | 8 +++++--- 2 files changed, 11 insertions(+), 9 deletions(-) diff --git a/src/Float.templates.hh b/src/Float.templates.hh index a784723..6b911ac 100644 --- a/src/Float.templates.hh +++ b/src/Float.templates.hh @@ -109,12 +109,12 @@ const FP_Interval_Type& compute_absolute_error( PPL_ASSERT(to_compute != NULL); - // FIXME: the inner cast may be dangerous. - analyzer_format omega = std::max( - static_cast<analyzer_format>(pow(f_base, - static_cast<analyzer_format>(1) - - f_exponent_bias - f_mantissa_bits)), - std::numeric_limits<analyzer_format>::denorm_min()); + // We assume that f_base is a power of 2. + analyzer_format omega; + int power = static_cast<int>(log2(f_base)) * + (1 - f_exponent_bias - f_mantissa_bits); + omega = std::max(static_cast<analyzer_format>(ldexpl(1.0, power)), + std::numeric_limits<analyzer_format>::denorm_min()); to_compute->build(i_constraint(GREATER_OR_EQUAL, -omega), i_constraint(LESS_OR_EQUAL, omega)); diff --git a/src/Linear_Form.templates.hh b/src/Linear_Form.templates.hh index fcb57c7..5bb64c0 100644 --- a/src/Linear_Form.templates.hh +++ b/src/Linear_Form.templates.hh @@ -418,9 +418,11 @@ Linear_Form<C>::relative_error( } C error_propagator; - // FIXME: this cast may be dangerous. - analyzer_format lb = -pow(f_base, - -static_cast<analyzer_format>(f_mantissa_bits)); + // We assume that f_base is a power of 2. + int power = static_cast<int>(log2(f_base)) * + (-f_mantissa_bits); + analyzer_format lb = -static_cast<analyzer_format>(ldexpl(1.0, power)); + error_propagator.build(i_constraint(GREATER_OR_EQUAL, lb), i_constraint(LESS_OR_EQUAL, -lb));

1 0

[GIT] ppl/ppl(floating_point): Constructors now take a Concrete_Expression_Type.
by Fabio Bossi 28 Jul '10

28 Jul '10

Module: ppl/ppl Branch: floating_point Commit: f396b2fa43531c01bca0fee89127acdf8c001de9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f396b2fa4353… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Jul 28 10:39:33 2010 +0200 Constructors now take a Concrete_Expression_Type. --- tests/Concrete_Expression/C_Expr.defs.hh | 21 ++++++++------ tests/Concrete_Expression/C_Expr.inlines.hh | 40 +++++++++++++++------------ tests/Concrete_Expression/linearize.cc | 38 +++++++++++++------------ 3 files changed, 54 insertions(+), 45 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=f396b2fa…

1 0

[GIT] ppl/ppl(floating_point): Fixed a bug in is().
by Fabio Bossi 28 Jul '10

28 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 60479359fdb9e44b03132077149759c216343fcf URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=60479359fdb9… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Jul 28 09:56:28 2010 +0200 Fixed a bug in is(). Make check now works again. --- src/Concrete_Expression.inlines.hh | 3 ++- 1 files changed, 2 insertions(+), 1 deletions(-) diff --git a/src/Concrete_Expression.inlines.hh b/src/Concrete_Expression.inlines.hh index 1d1d222..cf65a8a 100644 --- a/src/Concrete_Expression.inlines.hh +++ b/src/Concrete_Expression.inlines.hh @@ -92,7 +92,8 @@ template <typename Target> template <template <typename T> class Derived> inline bool Concrete_Expression_Common<Target>::is() const { - return Concrete_Expression<Target>::kind() == Derived<Target>::KIND; + return static_cast<const Concrete_Expression<Target>*>(this)->kind() == + Derived<Target>::KIND; } template <typename Target>

1 0

[GIT] ppl/ppl(floating_point): Commented and moved methods is() and as().
by Fabio Bossi 28 Jul '10

28 Jul '10

Module: ppl/ppl Branch: floating_point Commit: ba58fa9f47cfefd4464f8e366e34ae92beded2d3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ba58fa9f47cf… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Jul 28 09:47:52 2010 +0200 Commented and moved methods is() and as(). Make check not working due to bad implementation of is(). --- src/Concrete_Expression.defs.hh | 23 ++++++++++++----------- src/Concrete_Expression.inlines.hh | 23 +++++++++++++++++++++++ 2 files changed, 35 insertions(+), 11 deletions(-) diff --git a/src/Concrete_Expression.defs.hh b/src/Concrete_Expression.defs.hh index 3bafbbd..d52cad6 100644 --- a/src/Concrete_Expression.defs.hh +++ b/src/Concrete_Expression.defs.hh @@ -124,22 +124,23 @@ public: //! Returns the kind of \* this. Concrete_Expression_Kind kind() const; + //! Tests if \p *this has the same kind as <CODE>Derived<Target></CODE>. template <template <typename T> class Derived> - bool is() const { - return Concrete_Expression<Target>::kind() == Derived<Target>::KIND; - } + bool is() const; + /*! \brief + Returns a pointer to \p *this converted to type + <CODE>Derived<Target>*</CODE>. + */ template <template <typename T> class Derived> - Derived<Target>* as() { - PPL_ASSERT(is<Derived>()); - return static_cast<Derived<Target>*>(this); - } + Derived<Target>* as(); + /*! \brief + Returns a pointer to \p *this converted to type + <CODE>const Derived<Target>*</CODE>. + */ template <template <typename T> class Derived> - const Derived<Target>* as() const { - PPL_ASSERT(is<Derived>()); - return static_cast<const Derived<Target>*>(this); - } + const Derived<Target>* as() const; }; diff --git a/src/Concrete_Expression.inlines.hh b/src/Concrete_Expression.inlines.hh index c812919..1d1d222 100644 --- a/src/Concrete_Expression.inlines.hh +++ b/src/Concrete_Expression.inlines.hh @@ -88,6 +88,29 @@ Concrete_Expression_Type::floating_point_format() const { return impl.floating_point_format; } +template <typename Target> +template <template <typename T> class Derived> +inline bool +Concrete_Expression_Common<Target>::is() const { + return Concrete_Expression<Target>::kind() == Derived<Target>::KIND; +} + +template <typename Target> +template <template <typename T> class Derived> +inline Derived<Target>* +Concrete_Expression_Common<Target>::as() { + PPL_ASSERT(is<Derived>()); + return static_cast<Derived<Target>*>(this); +} + +template <typename Target> +template <template <typename T> class Derived> +inline const Derived<Target>* +Concrete_Expression_Common<Target>::as() const { + PPL_ASSERT(is<Derived>()); + return static_cast<const Derived<Target>*>(this); +} + } // namespace Parma_Polyhedra_Library #endif // !defined(PPL_Concrete_Expression_inlines_hh)

1 0

[GIT] ppl/ppl(floating_point): Added is and as methods.
by Abramo Bagnara 28 Jul '10

28 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 743a6e470392137a963641956f7c273b84b04f05 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=743a6e470392… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Wed Jul 28 00:47:30 2010 +0200 Added is and as methods. --- src/Concrete_Expression.defs.hh | 18 ++++++++++++++++++ src/linearize.hh | 8 ++++---- tests/Concrete_Expression/C_Expr.defs.hh | 1 + 3 files changed, 23 insertions(+), 4 deletions(-) diff --git a/src/Concrete_Expression.defs.hh b/src/Concrete_Expression.defs.hh index 88fbca8..3bafbbd 100644 --- a/src/Concrete_Expression.defs.hh +++ b/src/Concrete_Expression.defs.hh @@ -123,6 +123,24 @@ public: //! Returns the kind of \* this. Concrete_Expression_Kind kind() const; + + template <template <typename T> class Derived> + bool is() const { + return Concrete_Expression<Target>::kind() == Derived<Target>::KIND; + } + + template <template <typename T> class Derived> + Derived<Target>* as() { + PPL_ASSERT(is<Derived>()); + return static_cast<Derived<Target>*>(this); + } + + template <template <typename T> class Derived> + const Derived<Target>* as() const { + PPL_ASSERT(is<Derived>()); + return static_cast<const Derived<Target>*>(this); + } + }; template <typename Target> diff --git a/src/linearize.hh b/src/linearize.hh index ee8abc1..5fee0da 100644 --- a/src/linearize.hh +++ b/src/linearize.hh @@ -630,7 +630,7 @@ linearize(const Concrete_Expression<Target>& expr, case Floating_Point_Constant<Target>::KIND: { const Floating_Point_Constant<Target>* fpc_expr = - static_cast<const Floating_Point_Constant<Target>* >(&expr); + expr.template as<Floating_Point_Constant>(); result = FP_Linear_Form(FP_Interval_Type(fpc_expr->get_value_as_string())); return true; break; @@ -638,7 +638,7 @@ linearize(const Concrete_Expression<Target>& expr, case Unary_Operator<Target>::KIND: { const Unary_Operator<Target>* uop_expr = - static_cast<const Unary_Operator<Target>* >(&expr); + expr.template as<Unary_Operator>(); switch (uop_expr->unary_operator()) { case Unary_Operator<Target>::UPLUS: return linearize(*(uop_expr->argument()), int_store, lf_store, result); @@ -661,7 +661,7 @@ linearize(const Concrete_Expression<Target>& expr, case Binary_Operator<Target>::KIND: { const Binary_Operator<Target>* bop_expr = - static_cast<const Binary_Operator<Target>* >(&expr); + expr.template as<Binary_Operator>(); switch (bop_expr->binary_operator()) { case Binary_Operator<Target>::ADD: return add_linearize(*bop_expr, int_store, lf_store, result); @@ -692,7 +692,7 @@ linearize(const Concrete_Expression<Target>& expr, case Approximable_Reference<Target>::KIND: { const Approximable_Reference<Target>* ref_expr = - static_cast<const Approximable_Reference<Target>* >(&expr); + expr.template as<Approximable_Reference>(); /* Variable references are the only that we are currently able to analyze */ dimension_type variable_index = ref_expr->associated_dimension(); diff --git a/tests/Concrete_Expression/C_Expr.defs.hh b/tests/Concrete_Expression/C_Expr.defs.hh index 96bc1cd..0391a9c 100644 --- a/tests/Concrete_Expression/C_Expr.defs.hh +++ b/tests/Concrete_Expression/C_Expr.defs.hh @@ -49,6 +49,7 @@ public: //! Returns the kind of \* this. Concrete_Expression_Kind kind() const; + private: //! The expression's kind. C_Expr_Kind expr_kind;

1 0

[GIT] ppl/ppl(master): Added missing inclusion.
by Roberto Bagnara 27 Jul '10

27 Jul '10

Module: ppl/ppl Branch: master Commit: 6e11577095f565d2016f1b72656b31df64066a53 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6e11577095f5… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Jul 27 21:39:45 2010 +0200 Added missing inclusion. --- src/termination.templates.hh | 1 + 1 files changed, 1 insertions(+), 0 deletions(-) diff --git a/src/termination.templates.hh b/src/termination.templates.hh index 8582e22..2a92f75 100644 --- a/src/termination.templates.hh +++ b/src/termination.templates.hh @@ -28,6 +28,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Generator.defs.hh" #include "Constraint_System.defs.hh" #include "C_Polyhedron.defs.hh" +#include "NNC_Polyhedron.defs.hh" #include <stdexcept>

1 0

[GIT] ppl/ppl(floating_point): Added a few tests.
by Fabio Bossi 27 Jul '10

27 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 1957eb995c4d4f3fa283cfabbd73f0ac2a632e6e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1957eb995c4d… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Jul 27 18:13:15 2010 +0200 Added a few tests. --- tests/Concrete_Expression/linearize.cc | 123 ++++++++++++++++++++++++++++++++ 1 files changed, 123 insertions(+), 0 deletions(-) diff --git a/tests/Concrete_Expression/linearize.cc b/tests/Concrete_Expression/linearize.cc index d382749..3f1e172 100644 --- a/tests/Concrete_Expression/linearize.cc +++ b/tests/Concrete_Expression/linearize.cc @@ -83,10 +83,133 @@ test03() { return ok; } +// Tests linearization of A + B. +bool +test04() { + FP_Interval tmp(0); + FP_Interval_Abstract_Store store(2); + store.set_interval(Variable(0), tmp); + store.set_interval(Variable(1), tmp); + Approximable_Reference<C_Expr> var0(0); + Approximable_Reference<C_Expr> var1(1); + Binary_Operator<C_Expr> sum(Binary_Operator<C_Expr>::ADD, &var0, &var1); + FP_Linear_Form result; + linearize(sum, store, FP_Linear_Form_Abstract_Store(), result); + + Variable A(0); + Variable B(1); + FP_Linear_Form known_result = FP_Linear_Form(A); + FP_Linear_Form rel_err1; + known_result.relative_error(ANALYZED_FP_FORMAT, rel_err1); + known_result += rel_err1; + FP_Linear_Form lb = FP_Linear_Form(B); + known_result += lb; + FP_Linear_Form rel_err2; + lb.relative_error(ANALYZED_FP_FORMAT, rel_err2); + known_result += rel_err2; + known_result += compute_absolute_error<FP_Interval>(ANALYZED_FP_FORMAT); + + bool ok = result == known_result; + + return ok; +} + +// Tests the linearization of A - B. +bool +test05() { + FP_Interval tmp(0); + FP_Interval_Abstract_Store store(2); + store.set_interval(Variable(0), tmp); + store.set_interval(Variable(1), tmp); + Approximable_Reference<C_Expr> var0(0); + Approximable_Reference<C_Expr> var1(1); + Binary_Operator<C_Expr> dif(Binary_Operator<C_Expr>::SUB, &var0, &var1); + FP_Linear_Form result; + linearize(dif, store, FP_Linear_Form_Abstract_Store(), result); + + Variable A(0); + Variable B(1); + FP_Linear_Form known_result = FP_Linear_Form(A); + FP_Linear_Form rel_err1; + known_result.relative_error(ANALYZED_FP_FORMAT, rel_err1); + known_result += rel_err1; + FP_Linear_Form lb = FP_Linear_Form(B); + lb.negate(); + known_result += lb; + FP_Linear_Form rel_err2; + lb.relative_error(ANALYZED_FP_FORMAT, rel_err2); + known_result += rel_err2; + known_result += compute_absolute_error<FP_Interval>(ANALYZED_FP_FORMAT); + + bool ok = result == known_result; + + return ok; +} + +// Tests linearization of A * B where A in [0, 1] and B in [2, 2]. +bool +test06() { + FP_Interval tmp(0); + tmp.join_assign(1); + FP_Interval_Abstract_Store store(2); + store.set_interval(Variable(0), tmp); + store.set_interval(Variable(1), FP_Interval(2)); + Approximable_Reference<C_Expr> var0(0); + Approximable_Reference<C_Expr> var1(1); + Binary_Operator<C_Expr> mul(Binary_Operator<C_Expr>::MUL, &var0, &var1); + FP_Linear_Form result; + linearize(mul, store, FP_Linear_Form_Abstract_Store(), result); + + Variable A(0); + FP_Interval coeff = FP_Interval(2); + FP_Linear_Form known_result = FP_Linear_Form(A); + FP_Linear_Form rel_err; + known_result.relative_error(ANALYZED_FP_FORMAT, rel_err); + known_result *= coeff; + known_result += coeff * rel_err; + known_result += compute_absolute_error<FP_Interval>(ANALYZED_FP_FORMAT); + + bool ok = (result == known_result); + + return ok; +} + +// Tests the linearization of A / B where A = [0, 1] and B = [2, 2]. +bool +test07() { + FP_Interval tmp(0); + tmp.join_assign(1); + FP_Interval_Abstract_Store store(2); + store.set_interval(Variable(0), tmp); + store.set_interval(Variable(1), FP_Interval(2)); + Approximable_Reference<C_Expr> var0(0); + Approximable_Reference<C_Expr> var1(1); + Binary_Operator<C_Expr> div(Binary_Operator<C_Expr>::DIV, &var0, &var1); + FP_Linear_Form result; + linearize(div, store, FP_Linear_Form_Abstract_Store(), result); + + Variable A(0); + FP_Interval coeff = FP_Interval(1 / 2.0); + FP_Linear_Form known_result = FP_Linear_Form(A); + FP_Linear_Form rel_err; + known_result.relative_error(ANALYZED_FP_FORMAT, rel_err); + known_result *= coeff; + known_result += rel_err * coeff; + known_result += compute_absolute_error<FP_Interval>(ANALYZED_FP_FORMAT); + + bool ok = (result == known_result); + + return ok; +} + } // namespace BEGIN_MAIN DO_TEST(test01); DO_TEST(test02); DO_TEST(test03); + DO_TEST(test04); + DO_TEST(test05); + DO_TEST(test06); + DO_TEST(test07); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Fixed a typo.
by Fabio Bossi 27 Jul '10

27 Jul '10

Module: ppl/ppl Branch: floating_point Commit: ee0a91950dcdced4bc81b76daf294f4838c7c97a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ee0a91950dcd… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Jul 27 16:19:45 2010 +0200 Fixed a typo. --- src/Linear_Form.templates.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/Linear_Form.templates.hh b/src/Linear_Form.templates.hh index 97f915b..fcb57c7 100644 --- a/src/Linear_Form.templates.hh +++ b/src/Linear_Form.templates.hh @@ -418,7 +418,7 @@ Linear_Form<C>::relative_error( } C error_propagator; - // FIXME: this cast may be dangerous, + // FIXME: this cast may be dangerous. analyzer_format lb = -pow(f_base, -static_cast<analyzer_format>(f_mantissa_bits)); error_propagator.build(i_constraint(GREATER_OR_EQUAL, lb),

1 0

[GIT] ppl/ppl(floating_point): Added two FIXME notes.
by Fabio Bossi 27 Jul '10

27 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 5bdcb742713de7e2f0303d7a311b03393768560b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5bdcb742713d… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Jul 27 16:18:55 2010 +0200 Added two FIXME notes. --- src/Float.templates.hh | 1 + src/Linear_Form.templates.hh | 1 + 2 files changed, 2 insertions(+), 0 deletions(-) diff --git a/src/Float.templates.hh b/src/Float.templates.hh index e5bf852..a784723 100644 --- a/src/Float.templates.hh +++ b/src/Float.templates.hh @@ -109,6 +109,7 @@ const FP_Interval_Type& compute_absolute_error( PPL_ASSERT(to_compute != NULL); + // FIXME: the inner cast may be dangerous. analyzer_format omega = std::max( static_cast<analyzer_format>(pow(f_base, static_cast<analyzer_format>(1) - diff --git a/src/Linear_Form.templates.hh b/src/Linear_Form.templates.hh index e508759..97f915b 100644 --- a/src/Linear_Form.templates.hh +++ b/src/Linear_Form.templates.hh @@ -418,6 +418,7 @@ Linear_Form<C>::relative_error( } C error_propagator; + // FIXME: this cast may be dangerous, analyzer_format lb = -pow(f_base, -static_cast<analyzer_format>(f_mantissa_bits)); error_propagator.build(i_constraint(GREATER_OR_EQUAL, lb),

1 0