Skip to content
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

ieee_floatt: introduce NOT_SET rounding mode #8541

Draft
wants to merge 1 commit into
base: develop
Choose a base branch
from
Draft

ieee_floatt: introduce NOT_SET rounding mode #8541

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
4 changes: 3 additions & 1 deletion src/ansi-c/literals/convert_float_literal.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
3 changes: 3 additions & 0 deletions src/solvers/floatbv/float_utils.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
7 changes: 4 additions & 3 deletions src/solvers/smt2/smt2_conv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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;

Expand Down Expand Up @@ -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() << ")";
}
Expand Down
16 changes: 16 additions & 0 deletions src/util/ieee_float.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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;
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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();
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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;

Expand Down
72 changes: 50 additions & 22 deletions src/util/ieee_float.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
{
}

Expand All @@ -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);
}
Expand Down
11 changes: 8 additions & 3 deletions src/util/simplify_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down Expand Up @@ -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());
}
Expand Down Expand Up @@ -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();
Expand Down Expand Up @@ -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)
Expand All @@ -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());
Expand Down Expand Up @@ -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();
Expand Down
3 changes: 2 additions & 1 deletion src/util/simplify_expr_int.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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())));
Expand Down
Loading