Merge pull request #5210 from xbauch/fix/malloc-size-too-large

Malloc should fail on too large allocations

Author: petr-bauch

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;
+}