Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Mar 2, 2018
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7ac4fda
Refactor and expose floating point to java conversion in expr2java.h
Feb 7, 2018
b3f2320
Add unit test for floating_point_to_java_string
Feb 9, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
52 changes: 5 additions & 47 deletions src/java_bytecode/expr2java.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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());
}


Expand Down
52 changes: 52 additions & 0 deletions src/java_bytecode/expr2java.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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>

Expand Down Expand Up @@ -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;
}();
Copy link
Collaborator

@tautschnig tautschnig Feb 12, 2018 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just curious: what is the reason to use the lambda here? The following would seem more concise to me (just 5 lines instead of 8), but I could easily be wrong:

std::ostringstream raw_stream;
raw_stream << value;
if(raw_stream.str().find('.') == std::string::npos)
  raw_stream << ".0";
const std::string decimal = raw_stream.str();

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It is less code, but the lambda makes the mutable raw_stream inaccessible.

Copy link
Contributor Author

@LAJW LAJW Feb 12, 2018 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I like to group values like that with lambdas. When reading code, we're usually asking ourselves the question of "where did this value come from". Grouping values in lambdas like this makes it obvious - the results of each "code block" is plainly visible and indented. Reduces the mental load, and should the lambda become too large - it can be easily detached into a discrete function.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess that's where I tend to use blank lines. We probably agree to disagree on matters of style :-)

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think a new line after each lambda call would make this function a lot more readable

Copy link
Contributor Author

@LAJW LAJW Feb 13, 2018 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think not. These kinds of lambdas serve the same purpose as new lines. The benefit of using them instead is giving smaller scopes to variable names and enabling more const. They are already indented, so I don't think additional new lines would help.

This isn't new, I'm just borrowing the concept from functional-ish languages (OCaml, F#), eg:

let topLevelName = 
    let nestedName1 = someExpression
    let nestedName2 = someOtherExpression
    finalExpression

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The rest of the code base doesn't use lambdas like this and we don't need more inconsistency. Also if I have to choose between a slightly smaller scope on variables and simpler code which works with more debuggers and profiling tools; the choice is obvious. Please don't PR code like this.

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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think this is a very clear variable name, perhaps lossless_representation

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
116 changes: 116 additions & 0 deletions unit/java_bytecode/expr2java.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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);
}
}