Add malloc-may-fail option to goto-check

doc/cprover-manual/properties.md

@@ -326,6 +326,7 @@ with `__`.
 |------------------------|-------------------------------------------------|
 | `--malloc-fail-null`   |  in case malloc fails return NULL               |
 | `--malloc-fail-assert` |  in case malloc fails report as failed property |
+| `--malloc-may-fail`    |  malloc may non-deterministically fail          |
 
 Calling `malloc` may fail for a number of reasons and the function may return a
 NULL pointer. The users can choose if and how they want the `malloc`-related
@@ -335,3 +336,7 @@ additional properties inside `malloc` that are checked and if failing the
 verification is terminated (by `assume(false)`). One such property is that the
 allocated size is not too large, i.e. internally representable. When neither of
 those two options are used, CBMC will assume that `malloc` does not fail.
+
+Malloc may also fail for external reasons which are not modelled by CProver. If
+you want to replicate this behaviour use the option `--malloc-may-fail` in
+conjunction with one of the above modes of failure.

regression/cbmc/Pointer_byte_extract5/no-simplify.desc

@@ -4,7 +4,7 @@ main.i
 ^EXIT=10$
 ^SIGNAL=0$
 array\.List dynamic object upper bound in p->List\[2\]: FAILURE
-\*\* 1 of 15 failed
+\*\* 1 of 16 failed
 --
 ^warning: ignoring
 --

regression/cbmc/Pointer_byte_extract5/test.desc

@@ -4,7 +4,7 @@ main.i
 ^EXIT=10$
 ^SIGNAL=0$
 array\.List dynamic object upper bound in p->List\[2\]: FAILURE
-\*\* 1 of 13 failed
+\*\* 1 of 14 failed
 --
 ^warning: ignoring
 --

regression/cbmc/array_constraints1/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^\*\* 2 of 15
+^\*\* 2 of 16
 --
 ^warning: ignoring

regression/cbmc/malloc-may-fail/main.c

@@ -0,0 +1,7 @@
+#include <stdlib.h>
+
+int main()
+{
+  char *p = malloc(100);
+  assert(p); // should fail, given the malloc-may-fail option
+}

regression/cbmc/malloc-may-fail/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--malloc-may-fail --malloc-fail-null
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.\d+\] line \d+ assertion p: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/malloc-may-fail/test_without_option.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.\d+\] line \d+ assertion p: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/pointer-overflow1/test.desc

@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 ^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : SUCCESS
 ^VERIFICATION FAILED$
-^\*\* 8 of 12 failed
+^\*\* 8 of 13 failed
 --
 ^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE
 ^warning: ignoring

regression/cbmc/r_w_ok1/test.desc

@@ -2,7 +2,7 @@ CORE
 main.c
 
 __CPROVER_[rw]_ok\(arbitrary_size, n \+ 1\): FAILURE$
-^\*\* 2 of 11 failed
+^\*\* 2 of 12 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/goto-analyzer/constant_propagation_01/test.desc

@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 18, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_02/test.desc

@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 9, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_03/test.desc

@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 9, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_04/test.desc

@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 9, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_07/test.desc

@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 13, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 14, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_12/test.desc

@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 16, function calls: 2$
 --
 ^warning: ignoring

src/ansi-c/ansi_c_internal_additions.cpp

@@ -185,15 +185,18 @@ void ansi_c_internal_additions(std::string &code)
     "void *" CPROVER_PREFIX "allocate("
       CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
     "const void *" CPROVER_PREFIX "alloca_object = 0;\n"
+
     "int " CPROVER_PREFIX "malloc_failure_mode="+
       std::to_string(config.ansi_c.malloc_failure_mode)+";\n"
     "int " CPROVER_PREFIX "malloc_failure_mode_return_null="+
     std::to_string(config.ansi_c.malloc_failure_mode_return_null)+";\n"
     "int " CPROVER_PREFIX "malloc_failure_mode_assert_then_assume="+
     std::to_string(config.ansi_c.malloc_failure_mode_assert_then_assume)+";\n"
     CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+
-      integer2string(max_malloc_size(config.ansi_c.pointer_width, config
+    integer2string(max_malloc_size(config.ansi_c.pointer_width, config
     .bv_encoding.object_bits))+";\n"
+    CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_may_fail = " +
+    std::to_string(config.ansi_c.malloc_may_fail) + ";\n"
 
     // this is ANSI-C
     "extern " CPROVER_PREFIX "thread_local const char __func__["

src/ansi-c/library/cprover.h

@@ -16,8 +16,10 @@ extern const void *__CPROVER_malloc_object;
 extern __CPROVER_size_t __CPROVER_malloc_size;
 extern _Bool __CPROVER_malloc_is_new_array;
 extern const void *__CPROVER_memory_leak;
+
 extern int __CPROVER_malloc_failure_mode;
 extern __CPROVER_size_t __CPROVER_max_malloc_size;
+extern _Bool __CPROVER_malloc_may_fail;
 
 // malloc failure modes
 extern int __CPROVER_malloc_failure_mode_return_null;

src/ansi-c/library/stdlib.c

@@ -75,6 +75,31 @@ __CPROVER_HIDE:;
   __CPROVER_size_t alloc_size = nmemb * size;
 #pragma CPROVER check pop
 
+  if(__CPROVER_malloc_failure_mode == __CPROVER_malloc_failure_mode_return_null)
+  {
+    __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
+    if(
+      alloc_size > __CPROVER_max_malloc_size ||
+      (__CPROVER_malloc_may_fail && should_malloc_fail))
+    {
+      return (void *)0;
+    }
+  }
+  else if(
+    __CPROVER_malloc_failure_mode ==
+    __CPROVER_malloc_failure_mode_assert_then_assume)
+  {
+    __CPROVER_assert(
+      alloc_size <= __CPROVER_max_malloc_size, "max allocation size exceeded");
+    __CPROVER_assume(alloc_size <= __CPROVER_max_malloc_size);
+
+    __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
+    __CPROVER_assert(
+      !__CPROVER_malloc_may_fail || !should_malloc_fail,
+      "max allocation may fail");
+    __CPROVER_assume(!__CPROVER_malloc_may_fail || !should_malloc_fail);
+  }
+
   void *malloc_res;
   // realistically, calloc may return NULL,
   // and __CPROVER_allocate doesn't, but no one cares
@@ -112,50 +137,55 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 
 inline void *malloc(__CPROVER_size_t malloc_size)
 {
-  // realistically, malloc may return NULL,
-  // and __CPROVER_allocate doesn't, but no one cares
-  __CPROVER_HIDE:;
+// realistically, malloc may return NULL,
+// but we only do so if `--malloc-may-fail` is set
+__CPROVER_HIDE:;
 
+  if(__CPROVER_malloc_failure_mode == __CPROVER_malloc_failure_mode_return_null)
+  {
+    __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
     if(
-      __CPROVER_malloc_failure_mode ==
-      __CPROVER_malloc_failure_mode_return_null)
+      malloc_size > __CPROVER_max_malloc_size ||
+      (__CPROVER_malloc_may_fail && should_malloc_fail))
     {
-      if(malloc_size > __CPROVER_max_malloc_size)
-      {
-        return (void *)0;
-      }
-    }
-    else if(
-      __CPROVER_malloc_failure_mode ==
-      __CPROVER_malloc_failure_mode_assert_then_assume)
-    {
-      __CPROVER_assert(
-        malloc_size <= __CPROVER_max_malloc_size,
-        "max allocation size exceeded");
-      __CPROVER_assume(malloc_size <= __CPROVER_max_malloc_size);
+      return (void *)0;
     }
+  }
+  else if(
+    __CPROVER_malloc_failure_mode ==
+    __CPROVER_malloc_failure_mode_assert_then_assume)
+  {
+    __CPROVER_assert(
+      malloc_size <= __CPROVER_max_malloc_size, "max allocation size exceeded");
+    __CPROVER_assume(malloc_size <= __CPROVER_max_malloc_size);
+
+    __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
+    __CPROVER_assert(
+      !__CPROVER_malloc_may_fail || !should_malloc_fail,
+      "max allocation may fail");
+    __CPROVER_assume(!__CPROVER_malloc_may_fail || !should_malloc_fail);
+  }
 
-    void *malloc_res;
-    malloc_res = __CPROVER_allocate(malloc_size, 0);
+  void *malloc_res;
+  malloc_res = __CPROVER_allocate(malloc_size, 0);
 
-    // make sure it's not recorded as deallocated
-    __CPROVER_deallocated =
-      (malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated;
+  // make sure it's not recorded as deallocated
+  __CPROVER_deallocated =
+    (malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated;
 
-    // record the object size for non-determistic bounds checking
-    __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
-    __CPROVER_malloc_object =
-      record_malloc ? malloc_res : __CPROVER_malloc_object;
-    __CPROVER_malloc_size = record_malloc ? malloc_size : __CPROVER_malloc_size;
-    __CPROVER_malloc_is_new_array =
-      record_malloc ? 0 : __CPROVER_malloc_is_new_array;
+  // record the object size for non-determistic bounds checking
+  __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
+  __CPROVER_malloc_object =
+    record_malloc ? malloc_res : __CPROVER_malloc_object;
+  __CPROVER_malloc_size = record_malloc ? malloc_size : __CPROVER_malloc_size;
+  __CPROVER_malloc_is_new_array =
+    record_malloc ? 0 : __CPROVER_malloc_is_new_array;
 
-    // detect memory leaks
-    __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
-    __CPROVER_memory_leak =
-      record_may_leak ? malloc_res : __CPROVER_memory_leak;
+  // detect memory leaks
+  __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
+  __CPROVER_memory_leak = record_may_leak ? malloc_res : __CPROVER_memory_leak;
 
-    return malloc_res;
+  return malloc_res;
 }
 
 /* FUNCTION: __builtin_alloca */
@@ -446,7 +476,8 @@ inline void *realloc(void *ptr, __CPROVER_size_t malloc_size)
   // this shouldn't move if the new size isn't bigger
   void *res;
   res=malloc(malloc_size);
-  __CPROVER_array_copy(res, ptr);
+  if(res != (void *)0)
+    __CPROVER_array_copy(res, ptr);
   free(ptr);
 
   return res;

src/cbmc/cbmc_parse_options.cpp

@@ -1076,6 +1076,8 @@ void cbmc_parse_optionst::help()
     // NOLINTNEXTLINE(whitespace/line_length)
     " --malloc-fail-assert         set malloc failure mode to assert-then-assume\n"
     " --malloc-fail-null           set malloc failure mode to return null\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --malloc-may-fail            allow malloc calls to return a null pointer\n"
     HELP_REACHABILITY_SLICER
     HELP_REACHABILITY_SLICER_FB
     " --full-slice                 run full slicer (experimental)\n" // NOLINT(*)

src/cbmc/cbmc_parse_options.h

@@ -52,6 +52,7 @@ class optionst;
   OPT_GOTO_CHECK \
   "(no-assertions)(no-assumptions)" \
   "(malloc-fail-assert)(malloc-fail-null)" \
+  "(malloc-may-fail)" \
   OPT_XML_INTERFACE \
   OPT_JSON_INTERFACE \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \

src/util/config.cpp

@@ -1103,6 +1103,8 @@ bool configt::set(const cmdlinet &cmdline)
   if(cmdline.isset("malloc-fail-assert"))
     ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_assert_then_assume;
 
+  ansi_c.malloc_may_fail = cmdline.isset("malloc-may-fail");
+
   return false;
 }
 

src/util/config.h

@@ -129,6 +129,7 @@ class configt
     libt lib;
 
     bool string_abstraction;
+    bool malloc_may_fail = false;
 
     enum malloc_failure_modet
     {