Add malloc-may-fail option to cbmc

petr-bauch · petr-bauch · commit 993b47b511a8 · 2020-01-24T17:03:52.000Z
and hard-code appropriate assertion inside our `stdlib.c`.
diff --git a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc b/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 14 failed
+\*\* 1 of 15 failed
 --
 ^warning: ignoring
 --
diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/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 11 failed 
+\*\* 1 of 12 failed
 --
 ^warning: ignoring
 --
diff --git a/regression/cbmc/array_constraints1/test.desc b/regression/cbmc/array_constraints1/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^\*\* 2 of 14
+^\*\* 2 of 15
 --
 ^warning: ignoring
diff --git a/regression/cbmc/malloc-may-fail/main.c b/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
+}
diff --git a/regression/cbmc/malloc-may-fail/test.desc b/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
diff --git a/regression/cbmc/pointer-overflow1/test.desc b/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 11 failed
+^\*\* 8 of 12 failed
 --
 ^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE
 ^warning: ignoring
diff --git a/regression/cbmc/r_w_ok1/test.desc b/regression/cbmc/r_w_ok1/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 
 __CPROVER_[rw]_ok\(arbitrary_size, n \+ 1\): FAILURE$
-^\*\* 2 of 10 failed
+^\*\* 2 of 11 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/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: 6, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/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: 7, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/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: 7, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/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: 7, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/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: 12, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 13, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 12, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/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: 6, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$
 --
 ^warning: ignoring
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/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__["
diff --git a/src/ansi-c/library/cprover.h b/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);
diff --git a/src/ansi-c/library/stdlib.c b/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 */
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -1041,6 +1041,7 @@ void cbmc_parse_optionst::help()
     "\n"
     "Backend options:\n"
     " --object-bits n              number of bits used for object addresses\n"
+    " --malloc-may-fail            enable failures for malloc calls\n"
     " --dimacs                     generate CNF in DIMACS format\n"
     " --beautify                   beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
     " --localize-faults            localize faults (experimental)\n"
diff --git a/src/cbmc/cbmc_parse_options.h b/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 \
diff --git a/src/util/config.cpp b/src/util/config.cpp
@@ -1093,6 +1093,11 @@ bool configt::set(const cmdlinet &cmdline)
     bv_encoding.is_object_bits_default = false;
   }
 
+  if(cmdline.isset("malloc-may-fail"))
+  {
+    ansi_c.malloc_may_fail = true;
+  }
+
   return false;
 }
 
diff --git a/src/util/config.h b/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;
