[PPL-devel] [GIT] ppl/ppl(floating_point): Avoid adding errors when casting to a more precise

[Fabio Bossi]

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

Author: Fabio Bossi <bossi at cs.unipr.it>
Date:   Fri Jul 30 16:04:19 2010 +0200

Avoid adding errors when casting to a more precise
floating point format.

---

 src/Float.defs.hh    |    6 ++++++
 src/Float.inlines.hh |    6 +++++-
 src/linearize.hh     |   13 ++++++++++---
 3 files changed, 21 insertions(+), 4 deletions(-)

diff --git a/src/Float.defs.hh b/src/Float.defs.hh
index e484458..75d2c2b 100644
--- a/src/Float.defs.hh
+++ b/src/Float.defs.hh
@@ -361,6 +361,12 @@ public:
 #endif
 
 /*! \brief
+  Returns <CODE>true</CODE> if and only if there is some floating point
+  number that is representable by \p f2 but not by \p f1.
+*/
+bool is_less_precise_than(Floating_Point_Format f1, Floating_Point_Format f2);
+
+/*! \brief
   Computes the absolute error of floating point computations.
 
   \par Template type parameters
diff --git a/src/Float.inlines.hh b/src/Float.inlines.hh
index 16e0f21..13692b8 100644
--- a/src/Float.inlines.hh
+++ b/src/Float.inlines.hh
@@ -444,6 +444,11 @@ float_ieee754_quad::build(bool negative, mpz_t mantissa, int exponent) {
     << (MANTISSA_BITS - 64);
 }
 
+inline bool
+is_less_precise_than(Floating_Point_Format f1, Floating_Point_Format f2) {
+  return f1 < f2;
+}
+
 #if PPL_SUPPORTED_FLOAT
 inline
 Float<float>::Float() {
@@ -492,7 +497,6 @@ Float<long double>::value() {
 }
 #endif
 
-
 } // namespace Parma_Polyhedra_Library
 
 #endif // !defined(PPL_Float_inlines_hh)
diff --git a/src/linearize.hh b/src/linearize.hh
index a4f131d..0093586 100644
--- a/src/linearize.hh
+++ b/src/linearize.hh
@@ -616,16 +616,23 @@ cast_linearize(const Cast_Operator<Target>& cast_expr,
   typedef Box<FP_Interval_Type> FP_Interval_Abstract_Store;
   typedef std::map<dimension_type, FP_Linear_Form> FP_Linear_Form_Abstract_Store;
 
+  Floating_Point_Format analyzed_format =
+    cast_expr.type().floating_point_format();
   const Concrete_Expression<Target>* cast_arg = cast_expr.argument();
   if (cast_arg->type().is_floating_point()) {
     if (!linearize(*cast_arg, int_store, lf_store, result))
       return false;
+    if (!is_less_precise_than(analyzed_format,
+                              cast_arg->type().floating_point_format()))
+      // We are casting to a more precise format. Do not add errors.
+      return true;
   }
-  else
+  else {
     result = FP_Linear_Form(FP_Interval_Type(cast_arg->get_integer_interval()));
+    /* FIXME: we can avoid adding errors if FP_Interval_Type::boundary_type
+       is less precise than analyzed_format. */
+  }
 
-  Floating_Point_Format analyzed_format =
-    cast_expr.type().floating_point_format();
   FP_Linear_Form rel_error;
   result.relative_error(analyzed_format, rel_error);
   result += rel_error;