smt2 parser: check type of body of function definition

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

@@ -1203,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;