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

protect ieee_floatt::rounding_mode #8551

Merged
merged 1 commit into from
Jan 2, 2025
Merged

protect ieee_floatt::rounding_mode #8551

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
17 changes: 7 additions & 10 deletions src/solvers/refinement/refine_arithmetic.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -171,12 +171,6 @@ void bv_refinementt::check_SAT(approximationt &a)
if(a.over_state==MAX_STATE)
return;

ieee_float_spect spec(to_floatbv_type(type));
ieee_floatt o0(spec), o1(spec);

o0.unpack(a.op0_value);
o1.unpack(a.op1_value);

// get actual rounding mode
constant_exprt rounding_mode_expr =
to_constant_expr(get(float_op.rounding_mode()));
Expand All @@ -185,10 +179,13 @@ void bv_refinementt::check_SAT(approximationt &a)
ieee_floatt::rounding_modet rounding_mode =
(ieee_floatt::rounding_modet)rounding_mode_int;

ieee_floatt result=o0;
o0.rounding_mode=rounding_mode;
o1.rounding_mode=rounding_mode;
result.rounding_mode=rounding_mode;
ieee_float_spect spec(to_floatbv_type(type));
ieee_floatt o0(spec, rounding_mode), o1(spec, rounding_mode);

o0.unpack(a.op0_value);
o1.unpack(a.op1_value);

ieee_floatt result = o0;

if(a.expr.id()==ID_floatbv_plus)
result+=o1;
Expand Down
57 changes: 40 additions & 17 deletions src/util/ieee_float.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -129,20 +129,22 @@ class ieee_floatt
// A helper to turn a rounding mode into a constant bitvector expression
static constant_exprt rounding_mode_expr(rounding_modet);

rounding_modet rounding_mode;

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),
rounding_mode(ROUND_TO_EVEN),
sign_flag(false),
exponent(0),
fraction(0),
NaN_flag(false),
infinity_flag(false)
{
}

explicit ieee_floatt(ieee_float_spect __spec, rounding_modet __rounding_mode)
: rounding_mode(__rounding_mode),
spec(std::move(__spec)),
ieee_floatt(ieee_float_spect __spec, rounding_modet __rounding_mode)
: spec(std::move(__spec)),
rounding_mode(__rounding_mode),
sign_flag(false),
exponent(0),
fraction(0),
Expand All @@ -151,14 +153,27 @@ 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)),
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)
: spec(ieee_float_spect(type)),
rounding_mode(__rounding_mode),
sign_flag(false),
exponent(0),
fraction(0),
NaN_flag(false),
infinity_flag(false)
{
}

Expand All @@ -175,6 +190,12 @@ class ieee_floatt
from_expr(expr);
}

ieee_floatt(const constant_exprt &expr, rounding_modet __rounding_mode)
: rounding_mode(__rounding_mode)
{
from_expr(expr);
}

void negate()
{
sign_flag=!sign_flag;
Expand Down Expand Up @@ -316,6 +337,8 @@ class ieee_floatt
void align();
void next_representable(bool greater);

rounding_modet rounding_mode;

// we store the number unpacked
bool sign_flag;
mp_integer exponent; // this is unbiased
Expand Down
26 changes: 13 additions & 13 deletions src/util/simplify_expr_floatbv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -190,10 +190,10 @@ simplify_exprt::simplify_floatbv_typecast(const floatbv_typecast_exprt &expr)
{
if(dest_type.id()==ID_floatbv) // float to float
{
ieee_floatt result(to_constant_expr(casted_expr));
result.rounding_mode =
auto rounding_mode =
(ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(
*rounding_mode_index);
ieee_floatt result(to_constant_expr(casted_expr), rounding_mode);
result.change_spec(
ieee_float_spect(to_floatbv_type(dest_type)));
return result.to_expr();
Expand All @@ -203,10 +203,10 @@ simplify_exprt::simplify_floatbv_typecast(const floatbv_typecast_exprt &expr)
{
if(*rounding_mode_index == ieee_floatt::ROUND_TO_ZERO)
{
ieee_floatt result(to_constant_expr(casted_expr));
result.rounding_mode =
auto rounding_mode =
(ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(
*rounding_mode_index);
ieee_floatt result(to_constant_expr(casted_expr), rounding_mode);
mp_integer value=result.to_integer();
return from_integer(value, dest_type);
}
Expand All @@ -220,10 +220,10 @@ simplify_exprt::simplify_floatbv_typecast(const floatbv_typecast_exprt &expr)
{
if(dest_type.id()==ID_floatbv) // int to float
{
ieee_floatt result(to_floatbv_type(dest_type));
result.rounding_mode =
auto rounding_mode =
(ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(
*rounding_mode_index);
ieee_floatt result(to_floatbv_type(dest_type), rounding_mode);
result.from_integer(*value);
return result.to_expr();
}
Expand Down Expand Up @@ -296,16 +296,16 @@ simplify_exprt::simplify_floatbv_op(const ieee_float_op_exprt &expr)

if(op0.is_constant() && op1.is_constant() && op2.is_constant())
{
ieee_floatt v0(to_constant_expr(op0));
ieee_floatt v1(to_constant_expr(op1));
const auto rounding_mode_opt = numeric_cast<mp_integer>(op2);

const auto rounding_mode = numeric_cast<mp_integer>(op2);
if(rounding_mode.has_value())
if(rounding_mode_opt.has_value())
{
v0.rounding_mode =
const auto rounding_mode =
(ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(
*rounding_mode);
v1.rounding_mode=v0.rounding_mode;
*rounding_mode_opt);

ieee_floatt v0(to_constant_expr(op0), rounding_mode);
ieee_floatt v1(to_constant_expr(op1), rounding_mode);

ieee_floatt result=v0;

Expand Down
Loading