Add malloc-may-fail option to goto-checker

and hard-code appropriate assertion inside our `stdlib.c`.

Author: petr-bauch

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

@@ -0,0 +1,6 @@
+#include <stdlib.h>
+
+int main()
+{
+  char *p = malloc(100); // may fail, since malloc may fail
+}

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

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

src/analyses/goto_check.cpp

@@ -72,6 +72,7 @@ class goto_checkt
     enable_built_in_assertions=_options.get_bool_option("built-in-assertions");
     enable_assumptions=_options.get_bool_option("assumptions");
     error_labels=_options.get_list_option("error-label");
+    config.ansi_c.malloc_may_fail = _options.get_bool_option("malloc-may-fail");
   }
 
   typedef goto_functionst::goto_functiont goto_functiont;

src/analyses/goto_check.h

@@ -38,7 +38,8 @@ void goto_check(
   "(div-by-zero-check)(enum-range-check)(signed-overflow-check)(unsigned-"     \
   "overflow-check)"                                                            \
   "(pointer-overflow-check)(conversion-check)(undefined-shift-check)"          \
-  "(float-overflow-check)(nan-check)(no-built-in-assertions)"
+  "(float-overflow-check)(nan-check)(no-built-in-assertions)"                  \
+  "(malloc-may-fail)"
 
 // clang-format off
 #define HELP_GOTO_CHECK \
@@ -55,6 +56,7 @@ void goto_check(
   " --nan-check                  check floating-point for NaN\n" \
   " --no-built-in-assertions     ignore assertions in built-in library\n" \
   " --enum-range-check           checks that all enum type expressions have values in the enum range\n" /* NOLINT(whitespace/line_length) */ \
+  " --malloc-may-fail            enable failures for malloc calls\n" \
 // clang-format on
 
 #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
@@ -70,6 +72,7 @@ void goto_check(
   options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("nan-check", cmdline.isset("nan-check")); \
-  options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")) /* NOLINT(whitespace/line_length) */
+  options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")); /* NOLINT(whitespace/line_length) */ \
+  options.set_option("malloc-may-fail", cmdline.isset("malloc-may-fail"))
 
 #endif // CPROVER_ANALYSES_GOTO_CHECK_H

src/ansi-c/ansi_c_internal_additions.cpp

@@ -155,6 +155,7 @@ 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"
+    CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_may_fail = " + (config.ansi_c.malloc_may_fail ? "1" : "0") + ";\n"
 
     // this is ANSI-C
     "extern " CPROVER_PREFIX "thread_local const char __func__["

src/ansi-c/library/cprover.h

@@ -16,6 +16,7 @@ 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 _Bool __CPROVER_malloc_may_fail;
 
 void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__));
 void __CPROVER_assert(__CPROVER_bool assertion, const char *description);

src/ansi-c/library/stdlib.c

@@ -115,23 +115,31 @@ inline void *malloc(__CPROVER_size_t malloc_size)
   // realistically, malloc may return NULL,
   // and __CPROVER_allocate doesn't, but no one cares
   __CPROVER_HIDE:;
-  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;
+    __CPROVER_assert(
+      __CPROVER_malloc_may_fail != (__CPROVER_bool)0, "malloc may fail");
 
-  // 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;
+    void *malloc_res;
+    malloc_res = __CPROVER_allocate(malloc_size, 0);
 
-  // detect memory leaks
-  __CPROVER_bool record_may_leak=__VERIFIER_nondet___CPROVER_bool();
-  __CPROVER_memory_leak=record_may_leak?malloc_res:__CPROVER_memory_leak;
+    // make sure it's not recorded as deallocated
+    __CPROVER_deallocated =
+      (malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated;
 
-  return malloc_res;
+    // 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;
+
+    return malloc_res;
 }
 
 /* FUNCTION: __builtin_alloca */

src/util/config.h

@@ -129,6 +129,7 @@ class configt
     libt lib;
 
     bool string_abstraction;
+    bool malloc_may_fail = false;
 
     static const std::size_t default_object_bits=8;
   } ansi_c;