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

This change exposes new floating_point_to_java_string function which
lets the user convert floating point numbers to java-compatible
strings without having to cast them to expression and creating an
unnecessary namespace beforehand.

Author: Lukasz A.J. Wrona

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, kroening@cs.cmu.edu
 #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