generate assert(false) when calling undefined function

This changes the symbolic execution engine to emit an assert(false) when
processing a call to a function without body, instead of merely emitting a
warning.

The key benefit is that undefined function bodies are a threat to soundness,
especially when CBMC is run without a human operator (say in CI) who might
spot the warning.  A common scenario is a call to a function that was
renamed, or whose signature has changed.  This scenario now triggers a
verification failure.

Users who prefer the previous, or other alternative behaviors, can achieve
this via program instrumentation, say using goto-instrument.

Author: kroening

regression/cbmc-cpp/Overloading_Functions4/main.cpp

@@ -1,7 +1,9 @@
 double pow(double _X, double _Y);
 double pow(double _X, int _Y);
 float pow(float _X, float _Y);
-float pow(float _X, int _Y);
+float pow(float _X, int _Y)
+{
+}
 long double pow(long double _X, long double _Y);
 long double pow(long double _X, int _Y);
 

regression/cbmc-library/fprintf-01/__fprintf_chk.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check --bounds-check -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2
 ^EXIT=0$
@@ -7,3 +7,5 @@ main.c
 --
 ^\*\*\*\* WARNING: no body for function __fprintf_chk
 ^warning: ignoring
+--
+We are missing __builtin_va_arg_pack

regression/cbmc-library/printf-01/__printf_chk.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check --bounds-check -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2
 ^EXIT=10$
@@ -8,3 +8,5 @@ main.c
 --
 ^\*\*\*\* WARNING: no body for function __printf_chk
 ^warning: ignoring
+--
+We are missing __builtin_va_arg_pack

regression/cbmc-library/syslog-01/__syslog_chk.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check --bounds-check -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2
 ^EXIT=0$
@@ -7,3 +7,5 @@ main.c
 --
 ^\*\*\*\* WARNING: no body for function __syslog_chk
 ^warning: ignoring
+--
+We are missing _syslog$DARWIN_EXTSN

regression/cbmc-library/syslog-01/test.desc

@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+We are missing _syslog$DARWIN_EXTSN

regression/cbmc/Array_UF17/main.c

@@ -31,7 +31,9 @@ int istrchr(const char *s, int c);
 int istrrchr(const char *s, int c);
 int istrncmp(const char *s1, int start, const char *s2, size_t n);
 int istrstr(const char *haystack, const char *needle);
-char *r_strncpy(char *dest, const char *src, size_t n);
+char *r_strncpy(char *dest, const char *src, size_t n)
+{
+}
 char *r_strcpy(char *dest, const char *src);
 char *r_strcat(char *dest, const char *src);
 char *r_strncat(char *dest, const char *src, size_t n);

regression/cbmc/Function_Pointer5/main.c

@@ -1,7 +1,13 @@
 // this is a pointer to a function that takes a function pointer as argument
 
-void signal1(int, void (*)(int));
-void signal2(int, void (*h)(int));
+void signal1(int, void (*)(int))
+{
+}
+
+void signal2(int, void (*h)(int))
+{
+  h(123);
+}
 
 void handler(int x)
 {

regression/cbmc/Malloc2/main.c

@@ -1,4 +1,4 @@
-typedef unsigned int size_t;
+typedef __CPROVER_size_t size_t;
 typedef int ssize_t;
 typedef int atomic_t;
 typedef unsigned gfp_t;

regression/cbmc/Pointer28/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+KNOWNBUG no-new-smt
 main.c
 --little-endian
 ^EXIT=0$

regression/cbmc/Promotion4/main.i

@@ -1,10 +1,12 @@
+unsigned nondet_unsigned();
+
 int main(int argc, char *argv[])
 {
   __CPROVER_assert(sizeof(unsigned int) == 2, "[--16] size of int is 16 bit");
   __CPROVER_assert(
     sizeof(unsigned long) == 4, "[--LP32] size of long is 32 bit");
 
-  unsigned int k = non_det_unsigned();
+  unsigned int k = nondet_unsigned();
   __CPROVER_assume(k < 1);
   __CPROVER_assert(k != 0xffff, "false counter example 16Bit?");
 

regression/cbmc/String_Abstraction11/anon-retval.c

@@ -1,4 +1,4 @@
-void *malloc(unsigned);
+void *malloc(__CPROVER_size_t);
 
 char *foo()
 {

regression/cbmc/String_Abstraction19/structs.c

@@ -1,4 +1,4 @@
-void *malloc(unsigned);
+void *malloc(__CPROVER_size_t);
 
 typedef struct str_struct
 {

regression/cbmc/Undefined_Function1/test.desc

@@ -1,9 +1,10 @@
 CORE
 main.c
 
+^\[f\.no-body\] line 9 no body for callee f: FAILURE$
+^\[main\.assertion\.1] line 10 assertion i==1: FAILURE$
+^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
-^\*\*\*\* WARNING: no body for function f$
-^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc/Undefined_Function2/test.desc

@@ -1,9 +1,10 @@
 CORE
 main.c
 
+^\[asd\.no-body\] line 7 no body for callee asd: FAILURE$
+^\[main\.assertion\.1\] line 8 assertion v1==v2: FAILURE$
+^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
-^\*\*\*\* WARNING: no body for function asd$
-^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc/issue_5952_soundness_bug_smt_encoding/short.c

@@ -1,9 +1,11 @@
 #include <assert.h>
 #include <stdlib.h>
 
+_Bool nondet_bool();
+
 void main()
 {
   char *data;
-  data = nondet() ? malloc(1) : malloc(2);
+  data = nondet_bool() ? malloc(1) : malloc(2);
   assert(__CPROVER_OBJECT_SIZE(data) <= 2);
 }

regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc

@@ -4,9 +4,9 @@ short.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-\[main.assertion.\d\] line \d assertion __CPROVER_OBJECT_SIZE\(data\) <= 2: SUCCESS
+^\[main\.assertion.\d\] line \d assertion __CPROVER_OBJECT_SIZE\(data\) <= 2: SUCCESS$
 --
-\[main.assertion.\d\] line \d assertion __CPROVER_OBJECT_SIZE\(data\) <= 2: FAILURE
+^\[main\.assertion.\d\] line \d assertion __CPROVER_OBJECT_SIZE\(data\) <= 2: FAILURE$
 --
 This is the reduced version of the issue described in
 https://github.com/diffblue/cbmc/issues/5952

regression/cbmc/memory_allocation2/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=10$

regression/cbmc/pointer-overflow2/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-overflow-check
 ^EXIT=0$

regression/cbmc/union12/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+KNOWNBUG broken-smt-backend
 main.c
 
 ^EXIT=10$

regression/contracts/assigns_replace_02/main.c

@@ -1,5 +1,9 @@
 #include <assert.h>
 
+void bar(int *)
+{
+}
+
 void foo(int *x, int *y) __CPROVER_assigns(*x)
 {
   *x = 7;

regression/contracts/cprover-assignable-pass/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 CALL __CPROVER_object_whole

regression/goto-instrument/dump-vararg1/test.desc

@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 --dump-c
 ^EXIT=0$
 ^SIGNAL=0$
 va_list
 --
 ^warning: ignoring
+--
+We are missing __CPROVER_va_start

regression/goto-instrument/inline_16/test.desc

@@ -1,12 +1,12 @@
 CORE
 main.c
 --inline
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^VERIFICATION FAILED$
 func1\(\)
 ret.*=.*func2\(\)
-no body for function.*func1
-no body for function.*func2
+^\[func1\.no-body\] file main.c line 3 no body for callee func1: FAILURE$
+^\[func2\.no-body\] file main.c line 3 no body for callee func2: FAILURE$
 --
 ^warning: ignoring

regression/goto-instrument/inline_17/test.desc

@@ -1,9 +1,10 @@
 CORE
 main.c
 --function-inline func1
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^\[func2\.no-body\] line 3 no body for callee func2: FAILURE$
+^VERIFICATION FAILED$
 func1\(\)
 func2\(\)
 --

regression/goto-instrument/remove-function-body1/test.desc

@@ -1,9 +1,11 @@
 CORE
 main.c
 --remove-function-body foo --remove-function-body bar
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^\[foo\.no-body\] line 19 no body for callee foo: FAILURE$
+^\[bar\.no-body\] line 20 no body for callee bar: FAILURE$
+^VERIFICATION FAILED$
 --
 ^warning: ignoring
 ^bar

src/goto-checker/symex_bmc.cpp

@@ -209,18 +209,3 @@ bool symex_bmct::get_unwind_recursion(
 
   return abort;
 }
-
-void symex_bmct::no_body(const irep_idt &identifier)
-{
-  if(body_warnings.insert(identifier).second)
-  {
-    log.warning() << "**** WARNING: no body for function " << identifier;
-
-    if(havoc_bodyless_functions)
-    {
-      log.warning()
-        << "; assigning non-deterministic values to any pointer arguments";
-    }
-    log.warning() << log.eom;
-  }
-}

src/goto-checker/symex_bmc.h

@@ -110,10 +110,6 @@ class symex_bmct : public goto_symext
     unsigned thread_nr,
     unsigned unwind) override;
 
-  void no_body(const irep_idt &identifier) override;
-
-  std::unordered_set<irep_idt> body_warnings;
-
   symex_coveraget symex_coverage;
 };
 

src/goto-symex/goto_symex.h

@@ -444,12 +444,6 @@ class goto_symext
 
   virtual void loop_bound_exceeded(statet &state, const exprt &guard);
 
-  /// Log a warning that a function has no body
-  /// \param identifier: The name of the function with no body
-  virtual void no_body(const irep_idt &identifier)
-  {
-  }
-
   /// Symbolically execute a FUNCTION_CALL instruction.
   /// Only functions that are symbols are supported, see
   /// \ref goto_symext::symex_function_call_symbol.

src/goto-symex/symex_function_call.cpp

@@ -288,7 +288,17 @@ void goto_symext::symex_function_call_post_clean(
 
   if(!goto_function.body_available())
   {
-    no_body(identifier);
+    // create an assertion
+    if(symex_config.unwinding_assertions)
+    {
+      const auto &symbol = ns.lookup(identifier);
+      const std::string property_id = id2string(identifier) + ".no-body";
+      vcc(
+        false_exprt(),
+        property_id,
+        "no body for callee " + id2string(symbol.display_name()),
+        state);
+    }
 
     // record the return
     target.function_return(
@@ -301,26 +311,6 @@ void goto_symext::symex_function_call_post_clean(
       symex_assign(state, cleaned_lhs, rhs);
     }
 
-    if(symex_config.havoc_undefined_functions)
-    {
-      // assign non det to function arguments if pointers
-      // are not const
-      for(const auto &arg : cleaned_arguments)
-      {
-        if(
-          arg.type().id() == ID_pointer &&
-          !to_pointer_type(arg.type()).base_type().get_bool(ID_C_constant) &&
-          to_pointer_type(arg.type()).base_type().id() != ID_code)
-        {
-          exprt object =
-            dereference_exprt(arg, to_pointer_type(arg.type()).base_type());
-          exprt cleaned_object = clean_expr(object, state, true);
-          const guardt guard(true_exprt(), state.guard_manager);
-          havoc_rec(state, guard, cleaned_object);
-        }
-      }
-    }
-
     symex_transition(state);
     return;
   }