Merge pull request #6132 from diffblue/smt2_solver_FPA

kroening · web-flow · commit 1c1fb761006f · 2021-05-20T12:55:27.000+01:00
Use FloatingPoint theory when using --cprover-smt2
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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,23 +407,23 @@ 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()=="_" &&
           src.get_sub()[1].id()=="-oo") // (_ -oo e s)
   {
     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()=="_" &&
           src.get_sub()[1].id()=="NaN") // (_ NaN e s)
   {
     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
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/bitvector_types.h>
+#include <util/ieee_float.h>
 
 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
@@ -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<ieee_floatt::rounding_modet>(
+                  numeric_cast_v<int>(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<ieee_floatt::rounding_modet>(
-            numeric_cast_v<int>(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
@@ -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)),

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE broken-smt-backend`
	`1`	`+CORE broken-z3-smt-backend`
`2`	`2`	`main.c`
`3`	`3`	`--floatbv`
`4`	`4`	`^EXIT=0$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE broken-smt-backend`
	`1`	`+CORE`
`2`	`2`	`main.c`
`3`	`3`	`--floatbv --no-simplify`
`4`	`4`	`^EXIT=0$`
Original file line number	Diff line number	Diff line change
`@@ -85,6 +85,7 @@ smt2_convt::smt2_convt(`
`85`	`85`	`break;`
`86`	`86`
`87`	`87`	`case solvert::CPROVER_SMT2:`
	`88`	`+ use_FPA_theory = true;`
`88`	`89`	`use_array_of_bool = true;`
`89`	`90`	`use_as_const = true;`
`90`	`91`	`use_check_sat_assuming = true;`
`@@ -406,23 +407,23 @@ constant_exprt smt2_convt::parse_literal(`
`406`	`407`	`{`
`407`	`408`	`std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());`
`408`	`409`	`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();`
`410`	`411`	`}`
`411`	`412`	`else if(src.get_sub().size()==4 &&`
`412`	`413`	`src.get_sub()[0].id()=="_" &&`
`413`	`414`	`src.get_sub()[1].id()=="-oo") // (_ -oo e s)`
`414`	`415`	`{`
`415`	`416`	`std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());`
`416`	`417`	`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();`
`418`	`419`	`}`
`419`	`420`	`else if(src.get_sub().size()==4 &&`
`420`	`421`	`src.get_sub()[0].id()=="_" &&`
`421`	`422`	`src.get_sub()[1].id()=="NaN") // (_ NaN e s)`
`422`	`423`	`{`
`423`	`424`	`std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());`
`424`	`425`	`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();`
`426`	`427`	`}`
`427`	`428`
`428`	`429`	`if(type.id()==ID_signedbv \|\|`