Merge pull request diffblue#1808 from LAJW/lajw/floating-point-to-java-string

TG-2667 Refactor and expose floating point to java conversion in expr2java.h

Author: Thomas Kiley

src/java_bytecode/expr2java.cpp

@@ -228,53 +228,11 @@ std::string expr2javat::convert_constant(
   else if((src.type()==java_float_type()) ||
           (src.type()==java_double_type()))
   {
-    ieee_floatt ieee_repr(to_constant_expr(src));
-    std::string result;
-
-    bool is_java_float=(src.type()==java_float_type());
-    if(ieee_repr.is_zero())
-    {
-      if(ieee_repr.get_sign())
-        result+='-';
-      result+="0.0";
-      if(is_java_float)
-        result+='f';
-      return result;
-    }
-
-    if(ieee_repr.is_NaN())
-    {
-       if(is_java_float)
-         return "Float.NaN";
-       else
-         return "Double.NaN";
-    }
-
-    if(ieee_repr.is_infinity())
-    {
-      if(is_java_float)
-      {
-        if(ieee_repr.get_sign())
-          return "Float.NEGATIVE_INFINITY";
-        else
-          return "Float.POSITIVE_INFINITY";
-      }
-      else
-      {
-        if(ieee_repr.get_sign())
-          return "Double.NEGATIVE_INFINITY";
-        else
-          return "Double.POSITIVE_INFINITY";
-      }
-    }
-
-    std::stringstream buffer;
-    buffer << std::hexfloat;
-    if(is_java_float)
-      buffer << ieee_repr.to_float() << 'f';
-    else
-      buffer << ieee_repr.to_double();
-    return buffer.str();
+    // This converts NaNs to the canonical NaN
+    const ieee_floatt ieee_repr(to_constant_expr(src));
+    if(ieee_repr.is_double())
+      return floating_point_to_java_string(ieee_repr.to_double());
+    return floating_point_to_java_string(ieee_repr.to_float());
   }
 
 

src/java_bytecode/expr2java.h

@@ -10,6 +10,9 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_EXPR2JAVA_H
 #define CPROVER_JAVA_BYTECODE_EXPR2JAVA_H
 
+#include <cmath>
+#include <numeric>
+#include <sstream>
 #include <string>
 #include <ansi-c/expr2c_class.h>
 
@@ -50,4 +53,53 @@ class expr2javat:public expr2ct
 std::string expr2java(const exprt &expr, const namespacet &ns);
 std::string type2java(const typet &type, const namespacet &ns);
 
+/// Convert floating point number to a string without printing
+/// unnecessary zeros. Prints decimal if precision is not lost.
+/// Prints hexadecimal otherwise, and/or java-friendly NaN and Infinity
+template <typename float_type>
+std::string floating_point_to_java_string(float_type value)
+{
+  const auto is_float = std::is_same<float_type, float>::value;
+  static const std::string class_name = is_float ? "Float" : "Double";
+  if(std::isnan(value))
+    return class_name + ".NaN";
+  if(std::isinf(value) && value >= 0.)
+    return class_name + ".POSITIVE_INFINITY";
+  if(std::isinf(value) && value <= 0.)
+    return class_name + ".NEGATIVE_INFINITY";
+  const std::string decimal = [&]() -> std::string { // NOLINT
+    // Using ostringstream instead of to_string to get string without
+    // trailing zeros
+    std::ostringstream raw_stream;
+    raw_stream << value;
+    const auto raw_decimal = raw_stream.str();
+    if(raw_decimal.find('.') == std::string::npos)
+      return raw_decimal + ".0";
+    return raw_decimal;
+  }();
+  const bool is_lossless = [&] { // NOLINT
+    if(value == std::numeric_limits<float_type>::min())
+      return true;
+    try
+    {
+      return std::stod(decimal) == value;
+    }
+    catch(std::out_of_range)
+    {
+      return false;
+    }
+  }();
+  const std::string lossless = [&]() -> std::string { // NOLINT
+    if(is_lossless)
+      return decimal;
+    std::ostringstream stream;
+    stream << std::hexfloat << value;
+    return stream.str();
+  }();
+  const auto literal = is_float ? lossless + 'f' : lossless;
+  if(is_lossless)
+    return literal;
+  return literal + " /* " + decimal + " */";
+}
+
 #endif // CPROVER_JAVA_BYTECODE_EXPR2JAVA_H

unit/java_bytecode/expr2java.cpp

@@ -0,0 +1,116 @@
+/*******************************************************************\
+
+ Module: Unit tests for expr-to-java string conversion
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+#include <java_bytecode/expr2java.h>
+
+TEST_CASE(
+  "expr2java tests",
+  "[core][java_bytecode][expr2java][floating_point_to_java_string]")
+{
+  SECTION("0.0 double to string")
+  {
+    REQUIRE(floating_point_to_java_string(0.0) == "0.0");
+  }
+
+  SECTION("0.0 float to string")
+  {
+    REQUIRE(floating_point_to_java_string(0.0f) == "0.0f");
+  }
+
+  SECTION("-0.0 double to string")
+  {
+    REQUIRE(floating_point_to_java_string(-0.0) == "-0.0");
+  }
+
+  SECTION("-0.0 float to string")
+  {
+    REQUIRE(floating_point_to_java_string(-0.0f) == "-0.0f");
+  }
+
+  SECTION("1.0 double to string")
+  {
+    REQUIRE(floating_point_to_java_string(1.0) == "1.0");
+  }
+
+  SECTION("1.0 float to string")
+  {
+    REQUIRE(floating_point_to_java_string(1.0f) == "1.0f");
+  }
+
+  SECTION("-1.0 double to string")
+  {
+    REQUIRE(floating_point_to_java_string(-1.0) == "-1.0");
+  }
+
+  SECTION("-1.0 float to string")
+  {
+    REQUIRE(floating_point_to_java_string(-1.0f) == "-1.0f");
+  }
+
+  SECTION("Infinity double to string")
+  {
+    REQUIRE(
+      floating_point_to_java_string(static_cast<double>(INFINITY)) ==
+      "Double.POSITIVE_INFINITY");
+  }
+
+  SECTION("Infinity float to string")
+  {
+    REQUIRE(
+      floating_point_to_java_string(static_cast<float>(INFINITY)) ==
+      "Float.POSITIVE_INFINITY");
+  }
+
+  SECTION("Negative infinity double to string")
+  {
+    REQUIRE(
+      floating_point_to_java_string(static_cast<double>(-INFINITY)) ==
+      "Double.NEGATIVE_INFINITY");
+  }
+
+  SECTION("Negative infinity float to string")
+  {
+    REQUIRE(
+      floating_point_to_java_string(static_cast<float>(-INFINITY)) ==
+      "Float.NEGATIVE_INFINITY");
+  }
+
+  SECTION("Float NaN to string")
+  {
+    REQUIRE(
+      floating_point_to_java_string(static_cast<float>(NAN)) == "Float.NaN");
+  }
+
+  SECTION("Double NaN to string")
+  {
+    REQUIRE(
+      floating_point_to_java_string(static_cast<double>(NAN)) == "Double.NaN");
+  }
+
+  SECTION("Hex float to string (print a comment)")
+  {
+    const float value = std::strtod("0x1p+37f", nullptr);
+    REQUIRE(
+      floating_point_to_java_string(value) == "0x1p+37f /* 1.37439e+11 */");
+  }
+
+  SECTION("Hex double to string (print a comment)")
+  {
+    const double value = std::strtod("0x1p+37f", nullptr);
+    REQUIRE(
+      floating_point_to_java_string(value) == "0x1p+37 /* 1.37439e+11 */");
+  }
+
+  SECTION("Beyond numeric limits")
+  {
+    REQUIRE(
+      floating_point_to_java_string(-5.56268e-309)
+        .find("/* -5.56268e-309 */") != std::string::npos);
+  }
+}