diff --git a/regression/cbmc/Float-div2/test.desc b/regression/cbmc/Float-div2/test.desc index 8f1b838d89c..e40801d9f85 100644 --- a/regression/cbmc/Float-div2/test.desc +++ b/regression/cbmc/Float-div2/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE broken-z3-smt-backend main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc/Float-no-simp6/test.desc b/regression/cbmc/Float-no-simp6/test.desc index e0bfef5401b..4d2a93e6e26 100644 --- a/regression/cbmc/Float-no-simp6/test.desc +++ b/regression/cbmc/Float-no-simp6/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --floatbv --no-simplify ^EXIT=0$ diff --git a/regression/cbmc/Float-no-simp7/test.desc b/regression/cbmc/Float-no-simp7/test.desc index e0bfef5401b..4d2a93e6e26 100644 --- a/regression/cbmc/Float-no-simp7/test.desc +++ b/regression/cbmc/Float-no-simp7/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --floatbv --no-simplify ^EXIT=0$ diff --git a/regression/cbmc/Float20/test.desc b/regression/cbmc/Float20/test.desc index 8f1b838d89c..b7d95a28215 100644 --- a/regression/cbmc/Float20/test.desc +++ b/regression/cbmc/Float20/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc/Float23/test.desc b/regression/cbmc/Float23/test.desc index 39d9265e8a7..9efefbc7362 100644 --- a/regression/cbmc/Float23/test.desc +++ b/regression/cbmc/Float23/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c ^EXIT=0$ diff --git a/regression/cbmc/Float3/test.desc b/regression/cbmc/Float3/test.desc index 8f1b838d89c..e40801d9f85 100644 --- a/regression/cbmc/Float3/test.desc +++ b/regression/cbmc/Float3/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE broken-z3-smt-backend main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc/Float5/test.desc b/regression/cbmc/Float5/test.desc index 8f1b838d89c..b7d95a28215 100644 --- a/regression/cbmc/Float5/test.desc +++ b/regression/cbmc/Float5/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc/Float6/test.desc b/regression/cbmc/Float6/test.desc index 8f1b838d89c..b7d95a28215 100644 --- a/regression/cbmc/Float6/test.desc +++ b/regression/cbmc/Float6/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc/Float8/test.desc b/regression/cbmc/Float8/test.desc index 39d9265e8a7..9efefbc7362 100644 --- a/regression/cbmc/Float8/test.desc +++ b/regression/cbmc/Float8/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c ^EXIT=0$ diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index f4e19cb6666..d9da852ab62 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -85,6 +85,7 @@ smt2_convt::smt2_convt( break; case solvert::CPROVER_SMT2: + use_FPA_theory = true; use_array_of_bool = true; use_as_const = true; use_check_sat_assuming = true; @@ -406,7 +407,7 @@ constant_exprt smt2_convt::parse_literal( { std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string()); std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string()); - return ieee_floatt::plus_infinity(ieee_float_spect(s, e)).to_expr(); + return ieee_floatt::plus_infinity(ieee_float_spect(s - 1, e)).to_expr(); } else if(src.get_sub().size()==4 && src.get_sub()[0].id()=="_" && @@ -414,7 +415,7 @@ constant_exprt smt2_convt::parse_literal( { std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string()); std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string()); - return ieee_floatt::minus_infinity(ieee_float_spect(s, e)).to_expr(); + return ieee_floatt::minus_infinity(ieee_float_spect(s - 1, e)).to_expr(); } else if(src.get_sub().size()==4 && src.get_sub()[0].id()=="_" && @@ -422,7 +423,7 @@ constant_exprt smt2_convt::parse_literal( { std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string()); std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string()); - return ieee_floatt::NaN(ieee_float_spect(s, e)).to_expr(); + return ieee_floatt::NaN(ieee_float_spect(s - 1, e)).to_expr(); } if(type.id()==ID_signedbv || diff --git a/src/solvers/smt2/smt2_format.cpp b/src/solvers/smt2/smt2_format.cpp index 08d3318778e..838be81ebfd 100644 --- a/src/solvers/smt2/smt2_format.cpp +++ b/src/solvers/smt2/smt2_format.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include std::ostream &smt2_format_rec(std::ostream &out, const typet &type) { @@ -92,7 +93,33 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr) } else if(expr_type.id() == ID_floatbv) { - out << value; + const ieee_floatt v = ieee_floatt(constant_expr); + const size_t e = v.spec.e; + const size_t f = v.spec.f + 1; // SMT-LIB counts the hidden bit + + if(v.is_NaN()) + { + out << "(_ NaN " << e << " " << f << ")"; + } + else if(v.is_infinity()) + { + if(v.get_sign()) + out << "(_ -oo " << e << " " << f << ")"; + else + out << "(_ +oo " << e << " " << f << ")"; + } + else + { + // Zero, normal or subnormal + + mp_integer binary = v.pack(); + std::string binaryString(integer2binary(v.pack(), v.spec.width())); + + out << "(fp " + << "#b" << binaryString.substr(0, 1) << " " + << "#b" << binaryString.substr(1, e) << " " + << "#b" << binaryString.substr(1 + e, f - 1) << ")"; + } } else DATA_INVARIANT(false, "unhandled constant: " + expr_type.id_string()); diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index 2231537cb33..e2dea2e9383 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -500,7 +500,10 @@ exprt smt2_parsert::function_application() if(next_token() != smt2_tokenizert::SYMBOL) throw error("expected symbol after '_'"); - if(has_prefix(smt2_tokenizer.get_buffer(), "bv")) + // copy, the reference won't be stable + const auto id = smt2_tokenizer.get_buffer(); + + if(has_prefix(id, "bv")) { mp_integer i = string2integer( std::string(smt2_tokenizer.get_buffer(), 2, std::string::npos)); @@ -515,10 +518,36 @@ exprt smt2_parsert::function_application() return from_integer(i, unsignedbv_typet(width)); } + else if(id == "+oo" || id == "-oo" || id == "NaN") + { + // These are the "plus infinity", "minus infinity" and NaN + // floating-point literals. + if(next_token() != smt2_tokenizert::NUMERAL) + throw error() << "expected number after " << id; + + auto width_e = std::stoll(smt2_tokenizer.get_buffer()); + + if(next_token() != smt2_tokenizert::NUMERAL) + throw error() << "expected second number after " << id; + + auto width_f = std::stoll(smt2_tokenizer.get_buffer()); + + if(next_token() != smt2_tokenizert::CLOSE) + throw error() << "expected ')' after " << id; + + // width_f *includes* the hidden bit + const ieee_float_spect spec(width_f - 1, width_e); + + if(id == "+oo") + return ieee_floatt::plus_infinity(spec).to_expr(); + else if(id == "-oo") + return ieee_floatt::minus_infinity(spec).to_expr(); + else // NaN + return ieee_floatt::NaN(spec).to_expr(); + } else { - throw error() << "unknown indexed identifier " - << smt2_tokenizer.get_buffer(); + throw error() << "unknown indexed identifier " << id; } } else if(smt2_tokenizer.get_buffer() == "!") @@ -699,44 +728,83 @@ exprt smt2_parsert::function_application() if(next_token() != smt2_tokenizert::CLOSE) throw error("expected ')' after to_fp"); - auto rounding_mode = expression(); + // width_f *includes* the hidden bit + const ieee_float_spect spec(width_f - 1, width_e); - if(next_token() != smt2_tokenizert::NUMERAL) - throw error("expected number after to_fp"); + auto rounding_mode = expression(); - auto real_number = smt2_tokenizer.get_buffer(); + auto source_op = expression(); if(next_token() != smt2_tokenizert::CLOSE) throw error("expected ')' at the end of to_fp"); - mp_integer significand, exponent; - - auto dot_pos = real_number.find('.'); - if(dot_pos == std::string::npos) + // There are several options for the source operand: + // 1) real or integer + // 2) bit-vector, which is interpreted as signed 2's complement + // 3) another floating-point format + if( + source_op.type().id() == ID_real || + source_op.type().id() == ID_integer) { - exponent = 0; - significand = string2integer(real_number); + // For now, we can only do this when + // the source operand is a constant. + if(source_op.id() == ID_constant) + { + mp_integer significand, exponent; + + const auto &real_number = + id2string(to_constant_expr(source_op).get_value()); + auto dot_pos = real_number.find('.'); + if(dot_pos == std::string::npos) + { + exponent = 0; + significand = string2integer(real_number); + } + else + { + // remove the '.' + std::string significand_str; + significand_str.reserve(real_number.size()); + for(auto ch : real_number) + { + if(ch != '.') + significand_str += ch; + } + + exponent = + mp_integer(dot_pos) - mp_integer(real_number.size()) + 1; + significand = string2integer(significand_str); + } + + ieee_floatt a( + spec, + static_cast( + numeric_cast_v(to_constant_expr(rounding_mode)))); + a.from_base10(significand, exponent); + return a.to_expr(); + } + else + throw error() + << "to_fp for non-constant real expressions is not implemented"; } - else + else if(source_op.type().id() == ID_unsignedbv) { - // remove the '.', if any - std::string significand_str; - significand_str.reserve(real_number.size()); - for(auto ch : real_number) - if(ch != '.') - significand_str += ch; - - exponent = mp_integer(dot_pos) - mp_integer(real_number.size()) + 1; - significand = string2integer(significand_str); + // The operand is hard-wired to be interpreted as a signed number. + return floatbv_typecast_exprt( + typecast_exprt( + source_op, + signedbv_typet( + to_unsignedbv_type(source_op.type()).get_width())), + rounding_mode, + spec.to_type()); } - - // width_f *includes* the hidden bit - ieee_float_spect spec(width_f - 1, width_e); - ieee_floatt a(spec); - a.rounding_mode = static_cast( - numeric_cast_v(to_constant_expr(rounding_mode))); - a.from_base10(significand, exponent); - return a.to_expr(); + else if(source_op.type().id() == ID_floatbv) + { + return floatbv_typecast_exprt( + source_op, rounding_mode, spec.to_type()); + } + else + throw error() << "unexpected sort given as operand to to_fp"; } else { @@ -1106,6 +1174,18 @@ void smt2_parsert::setup_expressions() return with_exprt(op[0], op[1], op[2]); }; + expressions["fp.abs"] = [this] { + auto op = operands(); + + if(op.size() != 1) + throw error("fp.abs takes one operand"); + + if(op[0].type().id() != ID_floatbv) + throw error("fp.abs takes FloatingPoint operand"); + + return abs_exprt(op[0]); + }; + expressions["fp.isNaN"] = [this] { auto op = operands(); diff --git a/src/util/ieee_float.h b/src/util/ieee_float.h index 2e5d92a1426..b1d7e85f40b 100644 --- a/src/util/ieee_float.h +++ b/src/util/ieee_float.h @@ -139,6 +139,17 @@ class ieee_floatt { } + explicit ieee_floatt(ieee_float_spect __spec, rounding_modet __rounding_mode) + : rounding_mode(__rounding_mode), + spec(std::move(__spec)), + sign_flag(false), + exponent(0), + fraction(0), + NaN_flag(false), + infinity_flag(false) + { + } + explicit ieee_floatt(const floatbv_typet &type): rounding_mode(ROUND_TO_EVEN), spec(ieee_float_spect(type)),