Merge pull request #3421 from diffblue/smt2-fapp-type-checking

SMT2 type checking for define-fun

Author: Daniel Kroening

regression/smt2_solver/function-applications/function-application1.desc

@@ -0,0 +1,7 @@
+CORE
+function-application1.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--

regression/smt2_solver/function-applications/function-application1.smt2

@@ -0,0 +1,13 @@
+(set-logic QF_BV)
+
+(define-fun min ((a (_ BitVec 8)) (b (_ BitVec 8))) (_ BitVec 8)
+    (ite (bvule a b) a b))
+
+(define-fun p1 () Bool (= (min #x01 #x02) #x01))
+(define-fun p2 () Bool (= (min #xff #xfe) #xfe))
+
+; all must be true
+
+(assert (not (and p1 p2)))
+
+(check-sat)

regression/smt2_solver/function-applications/function-application2.desc

@@ -0,0 +1,7 @@
+CORE
+function-application2.smt2
+
+^EXIT=134$
+^SIGNAL=0$
+^line 5: type mismatch in function definition: expected `\(_ BitVec 16\)' but got `\(_ BitVec 8\)'$
+--

regression/smt2_solver/function-applications/function-application2.smt2

@@ -0,0 +1,14 @@
+(set-logic QF_BV)
+
+; the range type doesn't match!
+(define-fun min ((a (_ BitVec 8)) (b (_ BitVec 8))) (_ BitVec 16)
+    (ite (bvule a b) a b))
+
+(define-fun p1 () Bool (= (min #x01 #x02) #x01))
+(define-fun p2 () Bool (= (min #xff #xfe) #xfe))
+
+; all must be true
+
+(assert (not (and p1 p2)))
+
+(check-sat)

scripts/delete_failing_smt2_solver_tests

@@ -58,12 +58,14 @@ rm Float8/test.desc
 rm Free2/test.desc
 rm Function1/test.desc
 rm Function_Pointer3/test.desc
+rm Initialization6/test.desc
 rm Linking4/test.desc
 rm Linking7/test.desc
 rm Malloc17/test.desc
 rm Malloc18/test.desc
 rm Malloc19/test.desc
 rm Malloc20/test.desc
+rm Malloc21/test.desc
 rm Malloc23/test.desc
 rm Malloc24/test.desc
 rm Memmove1/test.desc

src/solvers/smt2/smt2_parser.cpp

@@ -10,6 +10,22 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 
+std::ostream &operator<<(std::ostream &out, const smt2_parsert::smt2_format &f)
+{
+  if(f.type.id() == ID_unsignedbv)
+    out << "(_ BitVec " << to_unsignedbv_type(f.type).get_width() << ')';
+  else if(f.type.id() == ID_bool)
+    out << "Bool";
+  else if(f.type.id() == ID_integer)
+    out << "Int";
+  else if(f.type.id() == ID_real)
+    out << "Real";
+  else
+    out << "? " << f.type.id();
+
+  return out;
+}
+
 void smt2_parsert::command_sequence()
 {
   exit=false;
@@ -360,8 +376,8 @@ exprt smt2_parsert::multi_ary(irep_idt id, const exprt::operandst &op)
       {
         error() << "expression must have operands with matching types,"
                    " but got `"
-                << op[0].type().pretty()
-                << "' and `" << op[i].type().pretty() << '\'' << eom;
+                << smt2_format(op[0].type()) << "' and `"
+                << smt2_format(op[i].type()) << '\'' << eom;
         return nil_exprt();
       }
     }
@@ -385,8 +401,8 @@ exprt smt2_parsert::binary_predicate(irep_idt id, const exprt::operandst &op)
     {
       error() << "expression must have operands with matching types,"
                  " but got `"
-              << op[0].type().pretty()
-              << "' and `" << op[1].type().pretty() << '\'' << eom;
+              << smt2_format(op[0].type()) << "' and `"
+              << smt2_format(op[1].type()) << '\'' << eom;
       return nil_exprt();
     }
 
@@ -1187,6 +1203,26 @@ void smt2_parsert::command(const std::string &c)
     auto signature=function_signature_definition();
     exprt body=expression();
 
+    // check type of body
+    if(signature.id() == ID_mathematical_function)
+    {
+      const auto &f_signature = to_mathematical_function_type(signature);
+      if(body.type() != f_signature.codomain())
+      {
+        error() << "type mismatch in function definition: expected `"
+                << smt2_format(f_signature.codomain()) << "' but got `"
+                << smt2_format(body.type()) << '\'' << eom;
+        return;
+      }
+    }
+    else if(body.type() != signature)
+    {
+      error() << "type mismatch in function definition: expected `"
+              << smt2_format(signature) << "' but got `"
+              << smt2_format(body.type()) << '\'' << eom;
+      return;
+    }
+
     // set up the entry
     auto &entry=id_map[id];
     entry.type=signature;

src/solvers/smt2/smt2_parser.h

@@ -43,6 +43,15 @@ class smt2_parsert:public smt2_tokenizert
   using id_mapt=std::map<irep_idt, idt>;
   id_mapt id_map;
 
+  struct smt2_format
+  {
+    explicit smt2_format(const typet &_type) : type(_type)
+    {
+    }
+
+    const typet type;
+  };
+
 protected:
   bool exit;
   void command_sequence();
@@ -82,4 +91,6 @@ class smt2_parsert:public smt2_tokenizert
   exprt cast_bv_to_unsigned(const exprt &);
 };
 
+std::ostream &operator<<(std::ostream &, const smt2_parsert::smt2_format &);
+
 #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H