Skip to content

smt2: fix float conversions #3656

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

Closed
wants to merge 2 commits into from
Closed

smt2: fix float conversions #3656

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
97759a3
floatbv can now do floatbv_typecast from c_bit_field
Jan 1, 2019
bea0345
smt2: fix the casts from c_bit_field to floatbv
Jan 1, 2019
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
63 changes: 57 additions & 6 deletions src/solvers/floatbv/float_bv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,21 @@ exprt float_bvt::convert(const exprt &expr) const
return not_exprt(is_equal(expr.op0(), expr.op1(), get_spec(expr.op0())));
else if(expr.id()==ID_floatbv_typecast)
{
const typet &src_type=expr.op0().type();
const typet &dest_type=expr.type();
const auto &floatbv_typecast_expr = to_floatbv_typecast_expr(expr);

const exprt &src = floatbv_typecast_expr.op();
const exprt &rm = floatbv_typecast_expr.rounding_mode();
const typet &src_type = src.type();
const typet &dest_type = floatbv_typecast_expr.type();

if(src_type.id() == ID_c_bit_field)
{
// go through underlying type
return convert(floatbv_typecast_exprt(
typecast_exprt(src, to_c_bit_field_type(src_type).subtype()),
rm,
dest_type));
}

if(dest_type.id()==ID_signedbv &&
src_type.id()==ID_floatbv) // float -> signed
Expand Down Expand Up @@ -60,10 +73,30 @@ exprt float_bvt::convert(const exprt &expr) const
else
return nil_exprt();
}
else if(expr.id()==ID_typecast &&
expr.type().id()==ID_bool &&
expr.op0().type().id()==ID_floatbv) // float -> bool
return not_exprt(is_zero(expr.op0()));
else if(expr.id() == ID_typecast)
{
const typet &src_type = expr.op0().type();
const typet &dest_type = expr.type();

if(
dest_type.id() == ID_bool && src_type.id() == ID_floatbv) // float -> bool
{
return not_exprt(is_zero(expr.op0()));
}
else if(
src_type.id() == ID_c_bool &&
dest_type.id() == ID_floatbv) // c_bool -> float
{
return from_c_bool(expr.op0(), get_spec(expr));
}
else if(
src_type.id() == ID_bool && dest_type.id() == ID_floatbv) // bool -> float
{
return from_bool(expr.op0(), get_spec(expr));
}
else
return nil_exprt();
}
else if(expr.id()==ID_floatbv_plus)
return add_sub(false, expr.op0(), expr.op1(), expr.op2(), get_spec(expr));
else if(expr.id()==ID_floatbv_minus)
Expand Down Expand Up @@ -254,6 +287,24 @@ exprt float_bvt::from_unsigned_integer(
return rounder(result, rm, spec);
}

exprt float_bvt::from_bool(const exprt &src, const ieee_float_spect &spec) const
{
ieee_floatt zero(spec);
zero.make_zero();
const auto zero_expr = zero.to_expr();
ieee_floatt one(spec);
one.build(1, 0);
const auto one_expr = one.to_expr();
return if_exprt(src, one_expr, zero_expr);
}

exprt float_bvt::from_c_bool(const exprt &src, const ieee_float_spect &spec)
const
{
// we go via bool
return from_bool(typecast_exprt(src, bool_typet()), spec);
}

exprt float_bvt::to_signed_integer(
const exprt &src,
std::size_t dest_width,
Expand Down
2 changes: 2 additions & 0 deletions src/solvers/floatbv/float_bv.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ class float_bvt
const exprt &,
const exprt &rm,
const ieee_float_spect &) const;
exprt from_c_bool(const exprt &, const ieee_float_spect &) const;
exprt from_bool(const exprt &, const ieee_float_spect &) const;
exprt from_signed_integer(
const exprt &,
const exprt &rm,
Expand Down
69 changes: 36 additions & 33 deletions src/solvers/smt2/smt2_conv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -812,6 +812,19 @@ std::string smt2_convt::type2id(const typet &type) const
{
return type2id(ns.follow_tag(to_c_enum_tag_type(type)).subtype());
}
else if(type.id() == ID_c_bit_field)
{
const auto &c_bit_field_type = to_c_bit_field_type(type);
// use underlying type
if(c_bit_field_type.subtype().id() == ID_unsignedbv)
return type2id(unsignedbv_typet(c_bit_field_type.get_width()));
else if(c_bit_field_type.subtype().id() == ID_signedbv)
return type2id(signedbv_typet(c_bit_field_type.get_width()));
else if(c_bit_field_type.subtype().id() == ID_c_bool)
return type2id(c_bool_typet(c_bit_field_type.get_width()));
else
UNIMPLEMENTED;
}
else
{
UNREACHABLE;
Expand Down Expand Up @@ -2352,46 +2365,28 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
}
else if(dest_type.id()==ID_floatbv)
{
const auto &dest_floatbv_type = to_floatbv_type(dest_type);

// Typecast from integer to floating-point should have be been
// converted to ID_floatbv_typecast during symbolic execution,
// adding the rounding mode. See
// smt2_convt::convert_floatbv_typecast.
// The exception is bool and c_bool to float.
// The exceptions are bool and c_bool to float,
// and non-semantic conversion.

if(src_type.id()==ID_bool)
if(src_type.id() == ID_bool || src_type.id() == ID_c_bool)
{
constant_exprt val(irep_idt(), dest_type);

ieee_floatt a(to_floatbv_type(dest_type));

mp_integer significand;
mp_integer exponent;

out << "(ite ";
convert_expr(src);
out << " ";

significand = 1;
exponent = 0;
a.build(significand, exponent);
val.set(ID_value, integer2binary(a.pack(), a.spec.width()));

convert_constant(val);
out << " ";

significand = 0;
exponent = 0;
a.build(significand, exponent);
val.set(ID_value, integer2binary(a.pack(), a.spec.width()));

convert_constant(val);
out << ")";
convert_expr(float_bv(expr));
}
else if(src_type.id()==ID_c_bool)
else if(src_type.id() == ID_bv)
{
// turn into proper bool
const typecast_exprt tmp(src, bool_typet());
convert_typecast(typecast_exprt(tmp, dest_type));
if(to_bv_type(src_type).get_width() == dest_floatbv_type.get_width())
{
// preserve representation, this just changes the type
convert_expr(src);
}
else
UNEXPECTEDCASE("typecast bv -> float with wrong width");
}
else
UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> float");
Expand Down Expand Up @@ -2429,7 +2424,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
void smt2_convt::convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
{
const exprt &src=expr.op();
// const exprt &rounding_mode=expr.rounding_mode();
const exprt &rounding_mode = expr.rounding_mode();
const typet &src_type=src.type();
const typet &dest_type=expr.type();

Expand Down Expand Up @@ -2533,6 +2528,14 @@ void smt2_convt::convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
ns.follow_tag(to_c_enum_tag_type(src_type)).subtype());
convert_floatbv_typecast(tmp);
}
else if(src_type.id() == ID_c_bit_field)
{
// go through underlying type
convert_floatbv_typecast(floatbv_typecast_exprt(
typecast_exprt(src, to_c_bit_field_type(src_type).subtype()),
rounding_mode,
dest_type));
}
else
UNEXPECTEDCASE(
"TODO typecast11 "+src_type.id_string()+" -> "+dest_type.id_string());
Expand Down