Malloc should fail on too large allocations

doc/cprover-manual/properties.md

@@ -319,3 +319,19 @@ example, replacing functions or setting global variables with the `__CPROVER`
 prefix might make analysis impossible. To avoid doing this by accident, negative
 lookahead can be used. For example, `(?!__).*` matches all names not starting
 with `__`.
+
+### Malloc failure mode
+
+|Flag                    |  Check                                          |
+|------------------------|-------------------------------------------------|
+| `--malloc-fail-null`   |  in case malloc fails return NULL               |
+| `--malloc-fail-assert` |  in case malloc fails report as failed property |
+
+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
+failures to occur. The option `--malloc-fail-null` results in `malloc` returning
+the NULL pointer when failing. The option `--malloc-fail-assert` places
+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.

regression/cbmc/Pointer_byte_extract5/main.i

@@ -11,13 +11,15 @@ typedef union
 typedef struct
 {
   int Count;
-  Union List[1];
+  // flexible array member -- note that smt conversion does not yet support
+  // 0-sized arrays
+  Union List[0];
 } Struct3;
 #pragma pack(pop)
 
 int main()
 {
-  Struct3 *p = malloc(sizeof(Struct3) + sizeof(Union));
+  Struct3 *p = malloc(sizeof(Struct3) + 2 * sizeof(Union));
   p->Count = 3;
   int po=0;
 

regression/cbmc/Pointer_byte_extract5/no-simplify.desc

@@ -1,14 +1,15 @@
-CORE
+CORE broken-smt-backend
 main.i
 --bounds-check --32 --no-simplify
 ^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
 --
 Test is built from SV-COMP's memsafety/20051113-1.c_false-valid-memtrack.c.
 C90 did not have flexible arrays, and using arrays of size 1 was common
-practice: http://c-faq.com/struct/structhack.html. We need to treat those as if
-it were a zero-sized array.
+practice: http://c-faq.com/struct/structhack.html. But past C90 using
+non-flexible members for struct-hack is undefined, hence we changed the test to
+use flexible member instead.

regression/cbmc/Pointer_byte_extract5/test.desc

@@ -4,11 +4,12 @@ main.i
 ^EXIT=10$
 ^SIGNAL=0$
 array\.List dynamic object upper bound in p->List\[2\]: FAILURE
-\*\* 1 of 11 failed 
+\*\* 1 of 13 failed
 --
 ^warning: ignoring
 --
 Test is built from SV-COMP's memsafety/20051113-1.c_false-valid-memtrack.c.
 C90 did not have flexible arrays, and using arrays of size 1 was common
-practice: http://c-faq.com/struct/structhack.html. We need to treat those as if
-it were a zero-sized array.
+practice: http://c-faq.com/struct/structhack.html. But past C90 using
+non-flexible members for struct-hack is undefined, hence we changed the test to
+use flexible member instead.

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

regression/cbmc/malloc-too-large/largest_representable.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+int main()
+{
+  int *p = malloc(__CPROVER_max_malloc_size); // try to allocate exactly the max
+
+  return 0;
+}

regression/cbmc/malloc-too-large/largest_representable.desc

@@ -0,0 +1,9 @@
+CORE
+largest_representable.c
+--malloc-fail-assert
+^EXIT=0$
+^SIGNAL=0$
+^\[malloc.assertion.\d+\] line \d+ max allocation size exceeded: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/malloc-too-large/max_size.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+int main()
+{
+  int *p = malloc(SIZE_MAX);
+
+  return 0;
+}

regression/cbmc/malloc-too-large/max_size.desc

@@ -0,0 +1,9 @@
+CORE
+max_size.c
+--malloc-fail-assert
+^EXIT=10$
+^SIGNAL=0$
+^\[malloc.assertion.\d+\] line \d+ max allocation size exceeded: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/malloc-too-large/one_byte_too_large.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+int main()
+{
+  // try to allocate the smallest violating amount
+  int *p = malloc(__CPROVER_max_malloc_size + 1);
+  assert(p);
+
+  return 0;
+}

regression/cbmc/malloc-too-large/one_byte_too_large.desc

@@ -0,0 +1,9 @@
+CORE
+one_byte_too_large.c
+--malloc-fail-null
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.\d+\] line \d+ assertion p: FAILURE$
+^VERIFICATION FAILED$
+--
+^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 11 failed
+^\*\* 8 of 12 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 10 failed
+^\*\* 2 of 11 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: 6, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, 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: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, 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: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, 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: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, 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: 12, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 12, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 13, 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: 6, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 16, function calls: 2$
 --
 ^warning: ignoring

regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-first,second,string_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 5
+first,second,string_size,prefix --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 5
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL

src/ansi-c/ansi_c_internal_additions.cpp

@@ -155,6 +155,15 @@ 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="+
+    std::to_string(1 << (config.ansi_c.pointer_width -
+                         config.bv_encoding.object_bits - 1))+";\n"
 
     // this is ANSI-C
     "extern " CPROVER_PREFIX "thread_local const char __func__["

src/ansi-c/library/cprover.h

@@ -16,6 +16,12 @@ 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;
+
+// malloc failure modes
+extern int __CPROVER_malloc_failure_mode_return_null;
+extern int __CPROVER_malloc_failure_mode_assert_then_assume;
 
 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,47 @@ 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;
+    if(
+      __CPROVER_malloc_failure_mode ==
+      __CPROVER_malloc_failure_mode_return_null)
+    {
+      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);
+    }
 
-  // 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/cbmc/cbmc_parse_options.cpp

@@ -1067,6 +1067,9 @@ void cbmc_parse_optionst::help()
     " --error-label label          check that label is unreachable\n"
     " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
     " --mm MM                      memory consistency model for concurrent programs\n" // NOLINT(*)
+    // 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"
     HELP_REACHABILITY_SLICER
     HELP_REACHABILITY_SLICER_FB
     " --full-slice                 run full slicer (experimental)\n" // NOLINT(*)

src/cbmc/cbmc_parse_options.h

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

src/util/config.cpp

@@ -1093,6 +1093,16 @@ bool configt::set(const cmdlinet &cmdline)
     bv_encoding.is_object_bits_default = false;
   }
 
+  if(cmdline.isset("malloc-fail-assert") && cmdline.isset("malloc-fail-null"))
+  {
+    throw invalid_command_line_argument_exceptiont{
+      "at most one malloc failure mode is acceptable", "--malloc-fail-null"};
+  }
+  if(cmdline.isset("malloc-fail-null"))
+    ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_return_null;
+  if(cmdline.isset("malloc-fail-assert"))
+    ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_assert_then_assume;
+
   return false;
 }
 

src/util/config.h

@@ -130,6 +130,15 @@ class configt
 
     bool string_abstraction;
 
+    enum malloc_failure_modet
+    {
+      malloc_failure_mode_none = 0,
+      malloc_failure_mode_return_null = 1,
+      malloc_failure_mode_assert_then_assume = 2
+    };
+
+    malloc_failure_modet malloc_failure_mode = malloc_failure_mode_none;
+
     static const std::size_t default_object_bits=8;
   } ansi_c;