diff --git a/src/solvers/floatbv/float_bv.cpp b/src/solvers/floatbv/float_bv.cpp index 10a65a64e00..590733bdc49 100644 --- a/src/solvers/floatbv/float_bv.cpp +++ b/src/solvers/floatbv/float_bv.cpp @@ -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 @@ -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) @@ -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, diff --git a/src/solvers/floatbv/float_bv.h b/src/solvers/floatbv/float_bv.h index b5b26eeb564..a8eb6553418 100644 --- a/src/solvers/floatbv/float_bv.h +++ b/src/solvers/floatbv/float_bv.h @@ -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, diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 2ab17ef6c77..6e7bc7a549f 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -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; @@ -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"); @@ -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(); @@ -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());