Move __CPROVER_uninterpreted_* conversion to C type checker

regression/ansi-c/undeclared_function/undeclared_uninterpreted.desc

@@ -2,7 +2,7 @@ CORE
 uninterpreted.c
 
 missing type information required to construct call to uninterpreted function
-^EXIT=70$
+^EXIT=(1|64)$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/contracts-dfcc/quantifiers-uninterpreted-function/main.c

@@ -0,0 +1,28 @@
+#include <ctype.h>
+
+int __CPROVER_uninterpreted_tolower(int);
+
+// clang-format off
+void tl1(char *dst, __CPROVER_size_t len)
+  __CPROVER_requires(__CPROVER_is_fresh(dst, len))
+  __CPROVER_assigns(__CPROVER_object_whole(dst))
+  __CPROVER_ensures(__CPROVER_forall {
+    int i;
+    (0 <= i && i < len) ==> dst[i % len] ==
+      __CPROVER_uninterpreted_tolower(__CPROVER_old(dst[i % len]))
+  });
+// clang-format on
+
+void tl1(char *dst, __CPROVER_size_t len)
+{
+  for(__CPROVER_size_t i = 0; i < len; i++)
+  {
+    dst[i] = tolower(dst[i]);
+  }
+}
+
+int main()
+{
+  char st[8] = "HELLOROD";
+  tl1(st, 8);
+}

regression/contracts-dfcc/quantifiers-uninterpreted-function/test.desc

@@ -0,0 +1,13 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract tl1
+^\[tl1.postcondition.1\] line \d+ Check ensures clause of contract contract::tl1 for function tl1: FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can use uninterpreted functions
+within quantifiers.

src/ansi-c/c_typecheck_base.cpp

@@ -142,7 +142,8 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol)
     {
       if(
         (!old_it->second.is_static_lifetime || !symbol.is_static_lifetime) &&
-        symbol.type.id() != ID_code)
+        (symbol.type.id() != ID_code &&
+         symbol.type.id() != ID_mathematical_function))
       {
         error().source_location = symbol.location;
         error() << "redeclaration of '" << symbol.display_name()
@@ -346,8 +347,12 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
   }
 
   // do initializer, this may change the type
-  if(new_symbol.type.id() != ID_code && !new_symbol.is_macro)
+  if(
+    new_symbol.type.id() != ID_code &&
+    new_symbol.type.id() != ID_mathematical_function && !new_symbol.is_macro)
+  {
     do_initializer(new_symbol);
+  }
 
   const typet &final_new = new_symbol.type;
 
@@ -871,6 +876,18 @@ void c_typecheck_baset::typecheck_declaration(
       irep_idt identifier=symbol.name;
       declarator.set_name(identifier);
 
+      if(
+        symbol.type.id() == ID_code &&
+        identifier.starts_with(CPROVER_PREFIX "uninterpreted_"))
+      {
+        const code_typet &function_call_type = to_code_type(symbol.type);
+        mathematical_function_typet::domaint domain;
+        for(const auto &parameter : function_call_type.parameters())
+          domain.push_back(parameter.type());
+        symbol.type =
+          mathematical_function_typet{domain, function_call_type.return_type()};
+      }
+
       typecheck_symbol(symbol);
 
       // check the contract, if any

src/ansi-c/c_typecheck_expr.cpp

@@ -2424,6 +2424,16 @@
       }
       else
       {
+        if(identifier.starts_with(CPROVER_PREFIX "uninterpreted_"))
+        {
+          throw invalid_source_file_exceptiont{
+            "'" + id2string(identifier) +
+              "' is not declared, "
+              "missing type information required to construct call to "
+              "uninterpreted function",
+            expr.source_location()};
+        }
+
         // This is an undeclared function that's not a builtin.
         // Let's just add it.
         // We do a bit of return-type guessing, but just a bit.
@@ -2480,13 +2490,14 @@
     for(auto &p :
         make_range(expr.arguments()).zip(mathematical_function_type.domain()))
     {
-      if(p.first.type() != p.second)
-      {
-        error().source_location = p.first.source_location();
-        error() << "expected argument of type " << to_string(p.second)
-                << " but got " << to_string(p.first.type()) << eom;
-        throw 0;
-      }
+      implicit_typecast(p.first, p.second);
+    }
+
+    if(f_op.id() != ID_lambda && f_op.id() != ID_symbol)
+    {
+      throw invalid_source_file_exceptiont{
+        "expected function symbol or lambda, but got " + id2string(f_op.id()),
+        f_op.source_location()};
     }
 
     function_application_exprt function_application(f_op, expr.arguments());

src/ansi-c/goto-conversion/builtin_functions.cpp

@@ -17,8 +17,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/expr_initializer.h>
 #include <util/expr_util.h>
 #include <util/fresh_symbol.h>
-#include <util/mathematical_expr.h>
-#include <util/mathematical_types.h>
 #include <util/pointer_expr.h>
 #include <util/rational.h>
 #include <util/rational_tools.h>
@@ -1089,34 +1087,6 @@ void goto_convertt::do_function_call_symbol(
     assignment.add_source_location() = function.source_location();
     copy(assignment, ASSIGN, dest);
   }
-  else if(identifier.starts_with(CPROVER_PREFIX "uninterpreted_"))
-  {
-    // make it a side effect if there is an LHS
-    if(lhs.is_nil())
-      return;
-
-    if(function.type().get_bool(ID_C_incomplete))
-    {
-      error().source_location = function.find_source_location();
-      error() << "'" << identifier << "' is not declared, "
-              << "missing type information required to construct call to "
-              << "uninterpreted function" << eom;
-      throw 0;
-    }
-
-    const code_typet &function_call_type = to_code_type(function.type());
-    mathematical_function_typet::domaint domain;
-    for(const auto &parameter : function_call_type.parameters())
-      domain.push_back(parameter.type());
-    mathematical_function_typet function_type{
-      domain, function_call_type.return_type()};
-    const function_application_exprt rhs(
-      symbol_exprt{function.get_identifier(), function_type}, arguments);
-
-    code_assignt assignment(lhs, rhs);
-    assignment.add_source_location() = function.source_location();
-    copy(assignment, ASSIGN, dest);
-  }
   else if(identifier == CPROVER_PREFIX "array_equal")
   {
     do_array_op(ID_array_equal, lhs, function, arguments, dest);