diff --git a/src/java_bytecode/expr2java.cpp b/src/java_bytecode/expr2java.cpp index 206718b2c81..cf6bb8a897a 100644 --- a/src/java_bytecode/expr2java.cpp +++ b/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()); } diff --git a/src/java_bytecode/expr2java.h b/src/java_bytecode/expr2java.h index daf4efb36b8..a0c9b828e6c 100644 --- a/src/java_bytecode/expr2java.h +++ b/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 +#include +#include #include #include @@ -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 +std::string floating_point_to_java_string(float_type value) +{ + const auto is_float = std::is_same::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::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 diff --git a/unit/java_bytecode/expr2java.cpp b/unit/java_bytecode/expr2java.cpp new file mode 100644 index 00000000000..eede0bf0a51 --- /dev/null +++ b/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 +#include + +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(INFINITY)) == + "Double.POSITIVE_INFINITY"); + } + + SECTION("Infinity float to string") + { + REQUIRE( + floating_point_to_java_string(static_cast(INFINITY)) == + "Float.POSITIVE_INFINITY"); + } + + SECTION("Negative infinity double to string") + { + REQUIRE( + floating_point_to_java_string(static_cast(-INFINITY)) == + "Double.NEGATIVE_INFINITY"); + } + + SECTION("Negative infinity float to string") + { + REQUIRE( + floating_point_to_java_string(static_cast(-INFINITY)) == + "Float.NEGATIVE_INFINITY"); + } + + SECTION("Float NaN to string") + { + REQUIRE( + floating_point_to_java_string(static_cast(NAN)) == "Float.NaN"); + } + + SECTION("Double NaN to string") + { + REQUIRE( + floating_point_to_java_string(static_cast(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); + } +}