CPROVER library: __builtin_X falls back to the model of X

regression/cbmc/gcc_builtin_library_functions/main.c

@@ -0,0 +1,26 @@
+// GCC and Clang provide __builtin_X for the C library functions X, with X's
+// meaning ("Other Built-in Functions Provided by GCC").  The CPROVER library
+// models X; __builtin_X now gets that model (libc++'s <cmath> calls
+// __builtin_ceilf, __builtin_sqrt, ...).
+#include <assert.h>
+
+int main()
+{
+  double d = 1.5;
+  assert(__builtin_ceil(d) == 2.0);
+  assert(__builtin_floorf(1.5f) == 1.0f);
+  assert(__builtin_truncl(-1.5l) == -1.0l);
+  assert(__builtin_sqrt(4.0) == 2.0);
+  assert(__builtin_fmax(1.0, 2.0) == 2.0);
+  assert(__builtin_copysign(1.0, -0.0) == -1.0);
+  const char *s = "abc";
+  assert(__builtin_strchr(s, 'b') == s + 1);
+  assert(__builtin_strrchr(s, 'z') == 0);
+  assert(__builtin_strncmp(s, "abd", 2) == 0);
+  assert(__builtin_strcmp(s, "abd") < 0);
+  assert(__builtin_strlen(s) == 3);
+  assert(__builtin_memcmp(s, "abd", 2) == 0);
+  // a model of its own is still used
+  assert(__builtin_fabs(-2.0) == 2.0);
+  return 0;
+}

regression/cbmc/gcc_builtin_library_functions/test.desc

@@ -0,0 +1,13 @@
+CORE gcc-only no-new-smt broken-cprover-smt-backend
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+no body for callee
+The incremental SMT2 back end does not finish on the floating-point models
+(sqrt, ceil on long double) within the CI timeout, hence no-new-smt; the
+cprover SMT2 solver fails an invariant in flatten2bv on them
+(broken-cprover-smt-backend).

src/ansi-c/cprover_library.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "ansi_c_language.h"
 
+#include <cctype>
 #include <sstream>
 
 static std::string get_cprover_library_text(
@@ -64,6 +65,54 @@ static std::string get_cprover_library_text(
     functions, symbol_table, cprover_library, library_text.str(), force_load);
 }
 
+/// \p model with every occurrence of the identifier \p from (as a whole
+/// word, outside `#include' lines) replaced by \p to.
+static std::string rename_in_model(
+  const std::string &model,
+  const std::string &from,
+  const std::string &to)
+{
+  const auto is_word = [](char c)
+  { return std::isalnum(static_cast<unsigned char>(c)) || c == '_'; };
+  std::istringstream in(model);
+  std::ostringstream out;
+  std::string line;
+  while(std::getline(in, line))
+  {
+    std::size_t first = line.find_first_not_of(" \t");
+    if(first != std::string::npos && line.compare(first, 1, "#") == 0)
+    {
+      std::size_t directive = line.find_first_not_of(" \t", first + 1);
+      if(
+        directive != std::string::npos &&
+        line.compare(directive, 7, "include") == 0)
+      {
+        out << line << '\n';
+        continue;
+      }
+    }
+    std::string result;
+    std::size_t pos = 0;
+    while(true)
+    {
+      const std::size_t hit = line.find(from, pos);
+      if(hit == std::string::npos)
+      {
+        result.append(line, pos, std::string::npos);
+        break;
+      }
+      const std::size_t end = hit + from.size();
+      const bool whole = (hit == 0 || !is_word(line[hit - 1])) &&
+                         (end == line.size() || !is_word(line[end]));
+      result.append(line, pos, hit - pos);
+      result += whole ? to : from;
+      pos = end;
+    }
+    out << result << '\n';
+  }
+  return out.str();
+}
+
 std::string get_cprover_library_text(
   const std::set<irep_idt> &functions,
   const symbol_table_baset &symbol_table,
@@ -97,6 +146,51 @@ std::string get_cprover_library_text(
     }
   }
 
+  // GCC and Clang provide `__builtin_X' for each C library function X, with
+  // X's meaning (GCC manual, "Other Built-in Functions Provided by GCC";
+  // libc++'s <cmath> calls __builtin_ceil, __builtin_sqrt, ...).  Without a
+  // model of its own, `__builtin_X' gets X's model under its own name.
+  for(const auto &id : functions)
+  {
+    const std::string name = id2string(id);
+    const std::string prefix = "__builtin_";
+    if(name.compare(0, prefix.size(), prefix) != 0)
+      continue;
+    const std::string plain = name.substr(prefix.size());
+    if(plain.empty())
+      continue;
+    const cprover_library_entryt *own = nullptr;
+    const cprover_library_entryt *of_plain = nullptr;
+    for(const cprover_library_entryt *e = cprover_library;
+        e->function != nullptr;
+        e++)
+    {
+      if(name == e->function)
+        own = e;
+      else if(plain == e->function)
+        of_plain = e;
+    }
+    // A model taking a va_list (vsnprintf, ...) is not reused: where
+    // va_list is a struct (aarch64), the C++ declaration of __builtin_X and
+    // the C model then have different parameter types, and linking left
+    // the model's va_list typedef dangling (--validate-goto-model:
+    // "va_list not found").
+    if(
+      own != nullptr || of_plain == nullptr ||
+      std::string{of_plain->model}.find("va_list") != std::string::npos)
+    {
+      continue;
+    }
+    const auto old = symbol_table.symbols.find(id);
+    if(
+      force_load ||
+      (old != symbol_table.symbols.end() && old->second.value.is_nil()))
+    {
+      count++;
+      library_text << rename_in_model(of_plain->model, plain, name) << '\n';
+    }
+  }
+
   if(count==0)
     return std::string();
   else