Skip to content

Commit 1c1fb76

Browse files
kroeningkroening
authored
Merge pull request #6132 from diffblue/smt2_solver_FPA
Use FloatingPoint theory when using --cprover-smt2
2 parents fd65126 + cd9dff8 commit 1c1fb76

File tree

13 files changed

+163
-44
lines changed

13 files changed

+163
-44
lines changed

‎regression/cbmc/Float-div2/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE broken-z3-smt-backend
22
main.c
33
--floatbv
44
^EXIT=0$

‎regression/cbmc/Float-no-simp6/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33
--floatbv --no-simplify
44
^EXIT=0$

‎regression/cbmc/Float-no-simp7/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33
--floatbv --no-simplify
44
^EXIT=0$

‎regression/cbmc/Float20/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33
--floatbv
44
^EXIT=0$

‎regression/cbmc/Float23/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33

44
^EXIT=0$

‎regression/cbmc/Float3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE broken-z3-smt-backend
22
main.c
33
--floatbv
44
^EXIT=0$

‎regression/cbmc/Float5/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33
--floatbv
44
^EXIT=0$

‎regression/cbmc/Float6/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33
--floatbv
44
^EXIT=0$

‎regression/cbmc/Float8/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33

44
^EXIT=0$

‎src/solvers/smt2/smt2_conv.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,7 @@ smt2_convt::smt2_convt(
8585
break;
8686

8787
case solvert::CPROVER_SMT2:
88+
use_FPA_theory = true;
8889
use_array_of_bool = true;
8990
use_as_const = true;
9091
use_check_sat_assuming = true;
@@ -406,23 +407,23 @@ constant_exprt smt2_convt::parse_literal(
406407
{
407408
std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
408409
std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
409-
return ieee_floatt::plus_infinity(ieee_float_spect(s, e)).to_expr();
410+
return ieee_floatt::plus_infinity(ieee_float_spect(s - 1, e)).to_expr();
410411
}
411412
else if(src.get_sub().size()==4 &&
412413
src.get_sub()[0].id()=="_" &&
413414
src.get_sub()[1].id()=="-oo") // (_ -oo e s)
414415
{
415416
std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
416417
std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
417-
return ieee_floatt::minus_infinity(ieee_float_spect(s, e)).to_expr();
418+
return ieee_floatt::minus_infinity(ieee_float_spect(s - 1, e)).to_expr();
418419
}
419420
else if(src.get_sub().size()==4 &&
420421
src.get_sub()[0].id()=="_" &&
421422
src.get_sub()[1].id()=="NaN") // (_ NaN e s)
422423
{
423424
std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
424425
std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
425-
return ieee_floatt::NaN(ieee_float_spect(s, e)).to_expr();
426+
return ieee_floatt::NaN(ieee_float_spect(s - 1, e)).to_expr();
426427
}
427428

428429
if(type.id()==ID_signedbv ||

‎src/solvers/smt2/smt2_format.cpp

Lines changed: 28 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
1010

1111
#include <util/arith_tools.h>
1212
#include <util/bitvector_types.h>
13+
#include <util/ieee_float.h>
1314

1415
std::ostream &smt2_format_rec(std::ostream &out, const typet &type)
1516
{
@@ -92,7 +93,33 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
9293
}
9394
else if(expr_type.id() == ID_floatbv)
9495
{
95-
out << value;
96+
const ieee_floatt v = ieee_floatt(constant_expr);
97+
const size_t e = v.spec.e;
98+
const size_t f = v.spec.f + 1; // SMT-LIB counts the hidden bit
99+
100+
if(v.is_NaN())
101+
{
102+
out << "(_ NaN " << e << " " << f << ")";
103+
}
104+
else if(v.is_infinity())
105+
{
106+
if(v.get_sign())
107+
out << "(_ -oo " << e << " " << f << ")";
108+
else
109+
out << "(_ +oo " << e << " " << f << ")";
110+
}
111+
else
112+
{
113+
// Zero, normal or subnormal
114+
115+
mp_integer binary = v.pack();
116+
std::string binaryString(integer2binary(v.pack(), v.spec.width()));
117+
118+
out << "(fp "
119+
<< "#b" << binaryString.substr(0, 1) << " "
120+
<< "#b" << binaryString.substr(1, e) << " "
121+
<< "#b" << binaryString.substr(1 + e, f - 1) << ")";
122+
}
96123
}
97124
else
98125
DATA_INVARIANT(false, "unhandled constant: " + expr_type.id_string());

‎src/solvers/smt2/smt2_parser.cpp

Lines changed: 111 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -500,7 +500,10 @@ exprt smt2_parsert::function_application()
500500
if(next_token() != smt2_tokenizert::SYMBOL)
501501
throw error("expected symbol after '_'");
502502

503-
if(has_prefix(smt2_tokenizer.get_buffer(), "bv"))
503+
// copy, the reference won't be stable
504+
const auto id = smt2_tokenizer.get_buffer();
505+
506+
if(has_prefix(id, "bv"))
504507
{
505508
mp_integer i = string2integer(
506509
std::string(smt2_tokenizer.get_buffer(), 2, std::string::npos));
@@ -515,10 +518,36 @@ exprt smt2_parsert::function_application()
515518

516519
return from_integer(i, unsignedbv_typet(width));
517520
}
521+
else if(id == "+oo" || id == "-oo" || id == "NaN")
522+
{
523+
// These are the "plus infinity", "minus infinity" and NaN
524+
// floating-point literals.
525+
if(next_token() != smt2_tokenizert::NUMERAL)
526+
throw error() << "expected number after " << id;
527+
528+
auto width_e = std::stoll(smt2_tokenizer.get_buffer());
529+
530+
if(next_token() != smt2_tokenizert::NUMERAL)
531+
throw error() << "expected second number after " << id;
532+
533+
auto width_f = std::stoll(smt2_tokenizer.get_buffer());
534+
535+
if(next_token() != smt2_tokenizert::CLOSE)
536+
throw error() << "expected ')' after " << id;
537+
538+
// width_f *includes* the hidden bit
539+
const ieee_float_spect spec(width_f - 1, width_e);
540+
541+
if(id == "+oo")
542+
return ieee_floatt::plus_infinity(spec).to_expr();
543+
else if(id == "-oo")
544+
return ieee_floatt::minus_infinity(spec).to_expr();
545+
else // NaN
546+
return ieee_floatt::NaN(spec).to_expr();
547+
}
518548
else
519549
{
520-
throw error() << "unknown indexed identifier "
521-
<< smt2_tokenizer.get_buffer();
550+
throw error() << "unknown indexed identifier " << id;
522551
}
523552
}
524553
else if(smt2_tokenizer.get_buffer() == "!")
@@ -699,44 +728,83 @@ exprt smt2_parsert::function_application()
699728
if(next_token() != smt2_tokenizert::CLOSE)
700729
throw error("expected ')' after to_fp");
701730

702-
auto rounding_mode = expression();
731+
// width_f *includes* the hidden bit
732+
const ieee_float_spect spec(width_f - 1, width_e);
703733

704-
if(next_token() != smt2_tokenizert::NUMERAL)
705-
throw error("expected number after to_fp");
734+
auto rounding_mode = expression();
706735

707-
auto real_number = smt2_tokenizer.get_buffer();
736+
auto source_op = expression();
708737

709738
if(next_token() != smt2_tokenizert::CLOSE)
710739
throw error("expected ')' at the end of to_fp");
711740

712-
mp_integer significand, exponent;
713-
714-
auto dot_pos = real_number.find('.');
715-
if(dot_pos == std::string::npos)
741+
// There are several options for the source operand:
742+
// 1) real or integer
743+
// 2) bit-vector, which is interpreted as signed 2's complement
744+
// 3) another floating-point format
745+
if(
746+
source_op.type().id() == ID_real ||
747+
source_op.type().id() == ID_integer)
716748
{
717-
exponent = 0;
718-
significand = string2integer(real_number);
749+
// For now, we can only do this when
750+
// the source operand is a constant.
751+
if(source_op.id() == ID_constant)
752+
{
753+
mp_integer significand, exponent;
754+
755+
const auto &real_number =
756+
id2string(to_constant_expr(source_op).get_value());
757+
auto dot_pos = real_number.find('.');
758+
if(dot_pos == std::string::npos)
759+
{
760+
exponent = 0;
761+
significand = string2integer(real_number);
762+
}
763+
else
764+
{
765+
// remove the '.'
766+
std::string significand_str;
767+
significand_str.reserve(real_number.size());
768+
for(auto ch : real_number)
769+
{
770+
if(ch != '.')
771+
significand_str += ch;
772+
}
773+
774+
exponent =
775+
mp_integer(dot_pos) - mp_integer(real_number.size()) + 1;
776+
significand = string2integer(significand_str);
777+
}
778+
779+
ieee_floatt a(
780+
spec,
781+
static_cast<ieee_floatt::rounding_modet>(
782+
numeric_cast_v<int>(to_constant_expr(rounding_mode))));
783+
a.from_base10(significand, exponent);
784+
return a.to_expr();
785+
}
786+
else
787+
throw error()
788+
<< "to_fp for non-constant real expressions is not implemented";
719789
}
720-
else
790+
else if(source_op.type().id() == ID_unsignedbv)
721791
{
722-
// remove the '.', if any
723-
std::string significand_str;
724-
significand_str.reserve(real_number.size());
725-
for(auto ch : real_number)
726-
if(ch != '.')
727-
significand_str += ch;
728-
729-
exponent = mp_integer(dot_pos) - mp_integer(real_number.size()) + 1;
730-
significand = string2integer(significand_str);
792+
// The operand is hard-wired to be interpreted as a signed number.
793+
return floatbv_typecast_exprt(
794+
typecast_exprt(
795+
source_op,
796+
signedbv_typet(
797+
to_unsignedbv_type(source_op.type()).get_width())),
798+
rounding_mode,
799+
spec.to_type());
731800
}
732-
733-
// width_f *includes* the hidden bit
734-
ieee_float_spect spec(width_f - 1, width_e);
735-
ieee_floatt a(spec);
736-
a.rounding_mode = static_cast<ieee_floatt::rounding_modet>(
737-
numeric_cast_v<int>(to_constant_expr(rounding_mode)));
738-
a.from_base10(significand, exponent);
739-
return a.to_expr();
801+
else if(source_op.type().id() == ID_floatbv)
802+
{
803+
return floatbv_typecast_exprt(
804+
source_op, rounding_mode, spec.to_type());
805+
}
806+
else
807+
throw error() << "unexpected sort given as operand to to_fp";
740808
}
741809
else
742810
{
@@ -1106,6 +1174,18 @@ void smt2_parsert::setup_expressions()
11061174
return with_exprt(op[0], op[1], op[2]);
11071175
};
11081176

1177+
expressions["fp.abs"] = [this] {
1178+
auto op = operands();
1179+
1180+
if(op.size() != 1)
1181+
throw error("fp.abs takes one operand");
1182+
1183+
if(op[0].type().id() != ID_floatbv)
1184+
throw error("fp.abs takes FloatingPoint operand");
1185+
1186+
return abs_exprt(op[0]);
1187+
};
1188+
11091189
expressions["fp.isNaN"] = [this] {
11101190
auto op = operands();
11111191

‎src/util/ieee_float.h

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -139,6 +139,17 @@ class ieee_floatt
139139
{
140140
}
141141

142+
explicit ieee_floatt(ieee_float_spect __spec, rounding_modet __rounding_mode)
143+
: rounding_mode(__rounding_mode),
144+
spec(std::move(__spec)),
145+
sign_flag(false),
146+
exponent(0),
147+
fraction(0),
148+
NaN_flag(false),
149+
infinity_flag(false)
150+
{
151+
}
152+
142153
explicit ieee_floatt(const floatbv_typet &type):
143154
rounding_mode(ROUND_TO_EVEN),
144155
spec(ieee_float_spect(type)),

0 commit comments

Comments
 (0)