[PPL-devel] [GIT] ppl/ppl(floating_point): Extended float_ieee754_half format.

[Fabio Biselli]

Module: ppl/ppl
Branch: floating_point
Commit: 8847a837fb858259f80990b984956d8a34689ed7
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8847a837fb858259f80990b984956d8a34689ed7

Author: Fabio Biselli <fabio.biselli at 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 ***");