diff --git a/src/ansi-c/literals/convert_float_literal.cpp b/src/ansi-c/literals/convert_float_literal.cpp
index 283a852c074..13fe67da2aa 100644
--- a/src/ansi-c/literals/convert_float_literal.cpp
+++ b/src/ansi-c/literals/convert_float_literal.cpp
@@ -71,7 +71,9 @@ exprt convert_float_literal(const std::string &src)
// but these aren't handled anywhere
}
- ieee_floatt a(type);
+ // Compile-time rounding is implementation defined.
+ // The choice below is arbitrary.
+ ieee_floatt a(type, ieee_floatt::rounding_modet::ROUND_TO_EVEN);
if(parsed_float.exponent_base==10)
a.from_base10(parsed_float.significand, parsed_float.exponent);
diff --git a/src/solvers/floatbv/float_utils.h b/src/solvers/floatbv/float_utils.h
index 989c8d53377..d7ca648c8fc 100644
--- a/src/solvers/floatbv/float_utils.h
+++ b/src/solvers/floatbv/float_utils.h
@@ -41,6 +41,9 @@ class float_utilst
switch(mode)
{
+ case ieee_floatt::NOT_SET:
+ PRECONDITION(false);
+
case ieee_floatt::ROUND_TO_EVEN:
round_to_even=const_literal(true);
break;
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 3662b8f5e1e..e2ad8f202dc 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -3066,7 +3066,8 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
{
constant_exprt val(irep_idt(), dest_type);
- ieee_floatt a(dest_floatbv_type);
+ // The rounding mode doesn't matter for 0/1.
+ ieee_floatt a(dest_floatbv_type, ieee_floatt::rounding_modet::ROUND_TO_EVEN);
mp_integer significand;
mp_integer exponent;
@@ -3464,7 +3465,7 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
significands including the hidden bit. Thus some encoding
is needed to get to IEEE-754 style representations. */
- ieee_floatt v=ieee_floatt(expr);
+ ieee_floatt v=ieee_floatt(expr); // no rounding needed
size_t e=floatbv_type.get_e();
size_t f=floatbv_type.get_f()+1;
@@ -3503,7 +3504,7 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
else
{
// produce corresponding bit-vector
- const ieee_float_spect spec(floatbv_type);
+ const ieee_float_spect spec(floatbv_type); // no rounding needed
const mp_integer v = bvrep2integer(expr.get_value(), spec.width(), false);
out << "(_ bv" << v << " " << spec.width() << ")";
}
diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp
index 52a507ff958..9cfa701f815 100644
--- a/src/util/ieee_float.cpp
+++ b/src/util/ieee_float.cpp
@@ -474,6 +474,8 @@ void ieee_floatt::build(
const mp_integer &_fraction,
const mp_integer &_exponent)
{
+ PRECONDITION(rounding_mode != rounding_modet::NOT_SET);
+
sign_flag=_fraction<0;
fraction=_fraction;
if(sign_flag)
@@ -488,6 +490,8 @@ void ieee_floatt::from_base10(
const mp_integer &_fraction,
const mp_integer &_exponent)
{
+ PRECONDITION(rounding_mode != rounding_modet::NOT_SET);
+
NaN_flag=infinity_flag=false;
sign_flag=_fraction<0;
fraction=_fraction;
@@ -584,6 +588,9 @@ void ieee_floatt::align()
// we need to consider the rounding mode here
switch(rounding_mode)
{
+ case NOT_SET:
+ PRECONDITION(false);
+
case UNKNOWN:
case NONDETERMINISTIC:
case ROUND_TO_EVEN:
@@ -660,6 +667,9 @@ void ieee_floatt::divide_and_round(
{
switch(rounding_mode)
{
+ case NOT_SET:
+ PRECONDITION(false);
+
case ROUND_TO_EVEN:
{
mp_integer divisor_middle = divisor / 2;
@@ -708,6 +718,7 @@ constant_exprt ieee_floatt::to_expr() const
ieee_floatt &ieee_floatt::operator/=(const ieee_floatt &other)
{
PRECONDITION(other.spec.f == spec.f);
+ PRECONDITION(rounding_mode != rounding_modet::NOT_SET);
// NaN/x = NaN
if(NaN_flag)
@@ -782,6 +793,7 @@ ieee_floatt &ieee_floatt::operator/=(const ieee_floatt &other)
ieee_floatt &ieee_floatt::operator*=(const ieee_floatt &other)
{
PRECONDITION(other.spec.f == spec.f);
+ PRECONDITION(rounding_mode != rounding_modet::NOT_SET);
if(other.NaN_flag)
make_NaN();
@@ -818,6 +830,8 @@ ieee_floatt &ieee_floatt::operator*=(const ieee_floatt &other)
ieee_floatt &ieee_floatt::operator+=(const ieee_floatt &other)
{
PRECONDITION(other.spec == spec);
+ PRECONDITION(rounding_mode != rounding_modet::NOT_SET);
+
ieee_floatt _other=other;
if(other.NaN_flag)
@@ -1058,6 +1072,8 @@ bool ieee_floatt::ieee_not_equal(const ieee_floatt &other) const
void ieee_floatt::change_spec(const ieee_float_spect &dest_spec)
{
+ PRECONDITION(rounding_mode != rounding_modet::NOT_SET);
+
mp_integer _exponent=exponent-spec.f;
mp_integer _fraction=fraction;
diff --git a/src/util/ieee_float.h b/src/util/ieee_float.h
index 788975ba040..528f1480cb3 100644
--- a/src/util/ieee_float.h
+++ b/src/util/ieee_float.h
@@ -121,22 +121,29 @@ class ieee_floatt
// what is recommended in C11 5.2.4.2.2
enum rounding_modet
{
- ROUND_TO_EVEN=0, ROUND_TO_MINUS_INF=1,
- ROUND_TO_PLUS_INF=2, ROUND_TO_ZERO=3,
- UNKNOWN, NONDETERMINISTIC
+ ROUND_TO_EVEN = 0,
+ ROUND_TO_MINUS_INF = 1,
+ ROUND_TO_PLUS_INF = 2,
+ ROUND_TO_ZERO = 3,
+ UNKNOWN,
+ NONDETERMINISTIC,
+ NOT_SET
};
// A helper to turn a rounding mode into a constant bitvector expression
static constant_exprt rounding_mode_expr(rounding_modet);
- rounding_modet rounding_mode;
+ rounding_modet rounding_mode = rounding_modet::NOT_SET;
ieee_float_spect spec;
- explicit ieee_floatt(const ieee_float_spect &_spec):
- rounding_mode(ROUND_TO_EVEN),
- spec(_spec), sign_flag(false), exponent(0), fraction(0),
- NaN_flag(false), infinity_flag(false)
+ explicit ieee_floatt(const ieee_float_spect &_spec)
+ : spec(_spec),
+ sign_flag(false),
+ exponent(0),
+ fraction(0),
+ NaN_flag(false),
+ infinity_flag(false)
{
}
@@ -151,26 +158,47 @@ class ieee_floatt
{
}
- explicit ieee_floatt(const floatbv_typet &type):
- rounding_mode(ROUND_TO_EVEN),
- spec(ieee_float_spect(type)),
- sign_flag(false),
- exponent(0),
- fraction(0),
- NaN_flag(false),
- infinity_flag(false)
+ explicit ieee_floatt(const floatbv_typet &type)
+ : spec(ieee_float_spect(type)),
+ sign_flag(false),
+ exponent(0),
+ fraction(0),
+ NaN_flag(false),
+ infinity_flag(false)
{
}
- ieee_floatt():
- rounding_mode(ROUND_TO_EVEN),
- sign_flag(false), exponent(0), fraction(0),
- NaN_flag(false), infinity_flag(false)
+ explicit ieee_floatt(
+ const floatbv_typet &type,
+ rounding_modet __rounding_mode)
+ : rounding_mode(__rounding_mode),
+ spec(ieee_float_spect(type)),
+ sign_flag(false),
+ exponent(0),
+ fraction(0),
+ NaN_flag(false),
+ infinity_flag(false)
{
}
- explicit ieee_floatt(const constant_exprt &expr):
- rounding_mode(ROUND_TO_EVEN)
+ ieee_floatt()
+ : sign_flag(false),
+ exponent(0),
+ fraction(0),
+ NaN_flag(false),
+ infinity_flag(false)
+ {
+ }
+
+ explicit ieee_floatt(const constant_exprt &expr)
+ {
+ from_expr(expr);
+ }
+
+ explicit ieee_floatt(
+ const constant_exprt &expr,
+ rounding_modet __rounding_mode)
+ : rounding_mode(__rounding_mode)
{
from_expr(expr);
}
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index c425602cbf5..2ee95f8fae9 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -70,6 +70,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_abs(const abs_exprt &expr)
if(type.id()==ID_floatbv)
{
+ // Does not need rounding
ieee_floatt value(to_constant_expr(to_unary_expr(expr).op()));
value.set_sign(false);
return value.to_expr();
@@ -104,6 +105,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_sign(const sign_exprt &expr)
if(type.id()==ID_floatbv)
{
+ // Does not need rounding
ieee_floatt value(to_constant_expr(expr.op()));
return make_boolean_expr(value.get_sign());
}
@@ -1179,7 +1181,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
const floatbv_typet &f_expr_type=
to_floatbv_type(expr_type);
- ieee_floatt f(f_expr_type);
+ ieee_floatt f(f_expr_type, ieee_floatt::rounding_modet::ROUND_TO_EVEN);
f.from_integer(int_value);
return f.to_expr();
@@ -1215,7 +1217,9 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
}
else if(op_type_id==ID_floatbv)
{
- ieee_floatt f(to_constant_expr(expr.op()));
+ ieee_floatt f{
+ to_constant_expr(expr.op()),
+ ieee_floatt::rounding_modet::ROUND_TO_EVEN};
if(expr_type_id==ID_unsignedbv ||
expr_type_id==ID_signedbv)
@@ -1233,7 +1237,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
{
fixedbvt fixedbv;
fixedbv.spec=fixedbv_spect(to_fixedbv_type(expr_type));
- ieee_floatt factor(f.spec);
+ ieee_floatt factor(f.spec, ieee_floatt::rounding_modet::ROUND_TO_EVEN);
factor.from_integer(power(2, fixedbv.spec.get_fraction_bits()));
f*=factor;
fixedbv.set_value(f.to_integer());
@@ -1267,6 +1271,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
{
const auto width = to_bv_type(op_type).get_width();
const auto int_value = bvrep2integer(value, width, false);
+ // Does not need rounding.
ieee_floatt ieee_float{to_floatbv_type(expr_type)};
ieee_float.unpack(int_value);
return ieee_float.to_expr();
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index 6cdb467e25b..21d23f61a19 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -1889,7 +1889,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
expr.op0().id() == ID_typecast && expr.op0().type().id() == ID_floatbv &&
to_typecast_expr(expr.op0()).op().type().id() == ID_floatbv)
{
- ieee_floatt const_val(to_constant_expr(expr.op1()));
+ ieee_floatt const_val{
+ to_constant_expr(expr.op1()), ieee_floatt::rounding_modet::ROUND_TO_EVEN};
ieee_floatt const_val_converted=const_val;
const_val_converted.change_spec(ieee_float_spect(
to_floatbv_type(to_typecast_expr(expr.op0()).op().type())));