Add malloc-may-fail option to cbmc

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

Note: minus clang-format.

Author: petr-bauch

src/ansi-c/ansi_c_internal_additions.cpp

@@ -155,6 +155,8 @@ 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 = " +
+    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,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

@@ -112,9 +112,14 @@ __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_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
+  if(__CPROVER_malloc_may_fail && should_malloc_fail)
+    return (void *)0;
+
   void *malloc_res;
   malloc_res = __CPROVER_allocate(malloc_size, 0);
 

src/cbmc/cbmc_parse_options.cpp

@@ -1041,6 +1041,8 @@ void cbmc_parse_optionst::help()
     "\n"
     "Backend options:\n"
     " --object-bits n              number of bits used for object addresses\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --malloc-may-fail            allow malloc calls to return a null pointer\n"
     " --dimacs                     generate CNF in DIMACS format\n"
     " --beautify                   beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
     " --localize-faults            localize faults (experimental)\n"

src/cbmc/cbmc_parse_options.h

@@ -48,6 +48,7 @@ class optionst;
   "(document-subgoals)(outfile):(test-preprocessor)" \
   "D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
   "(object-bits):" \
+  "(malloc-may-fail)" \
   OPT_GOTO_CHECK \
   "(no-assertions)(no-assumptions)" \
   OPT_XML_INTERFACE \

src/util/config.cpp

@@ -1093,6 +1093,8 @@ bool configt::set(const cmdlinet &cmdline)
     bv_encoding.is_object_bits_default = false;
   }
 
+  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;
 
     static const std::size_t default_object_bits=8;
   } ansi_c;