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