Malloc should fail on too large assertions

1: introduce `pointer-width` and `object-width` as new `cprover-start` variables
2: assert-then-assume about the size limit in our `stdlib.c` implementation of
`malloc`
3: add some tests, and assume about the alloc size in others

Note: this PR removes the C90-style structhack in test
`cbmc/Pointer_byte_extract5`. This may need to be amended if SV-Comp decides
they want to keep it.

Author: petr-bauch

regression/cbmc-library/memcpy-04/main.c

@@ -11,6 +11,11 @@ void publish(info_t *info)
 {
   size_t size;
   __CPROVER_assume(size >= info->len);
+  // alloc size is arbitrary but no larger than what CBMC can represent
+  size_t pointer_width = sizeof(void *) * 8;
+  size_t object_bits = 8; // by default
+  size_t cbmc_max_alloc_size = ((size_t)1 << (pointer_width - object_bits)) - 1;
+  __CPROVER_assume(size <= cbmc_max_alloc_size);
   unsigned char *buffer = malloc(size);
   memcpy(buffer, info->name, info->len);
   if(info->len > 42)
@@ -24,6 +29,13 @@ void main()
 {
   info_t info;
   size_t name_len;
+
+  // alloc size is arbitrary but no larger than what CBMC can represent
+  size_t pointer_width = sizeof(void *) * 8;
+  size_t object_bits = 8; // by default
+  size_t cbmc_max_alloc_size = ((size_t)1 << (pointer_width - object_bits)) - 1;
+  __CPROVER_assume(name_len <= cbmc_max_alloc_size);
+
   info.name = malloc(name_len);
   info.len = name_len;
   if(name_len > 42)

regression/cbmc-library/memcpy-04/test.desc

@@ -1,8 +1,8 @@
 CORE
 main.c
 
-^\[publish.assertion.1\] line 18 should pass: SUCCESS$
-^\[publish.assertion.2\] line 19 should fail: FAILURE$
+^\[publish.assertion.\d+\] line \d+ should pass: SUCCESS$
+^\[publish.assertion.\d+\] line \d+ should fail: FAILURE$
 ^\*\* 1 of \d+ failed
 ^VERIFICATION FAILED$
 ^EXIT=10$

regression/cbmc/Malloc25/main.c

@@ -2,6 +2,13 @@
 
 int main(int argc, char *argv[])
 {
-  int *p = malloc((size_t)argc * (size_t)argc * sizeof(int));
+  size_t alloc_size = (size_t)argc * (size_t)argc * sizeof(int);
+  // alloc size is arbitrary but no larger than what CBMC can represent
+  size_t pointer_width = sizeof(void *) * 8;
+  size_t object_bits = 8; // by default
+  size_t cbmc_max_alloc_size = ((size_t)1 << (pointer_width - object_bits)) - 1;
+  __CPROVER_assume(alloc_size <= cbmc_max_alloc_size);
+
+  int *p = malloc(alloc_size);
   return 0;
 }

regression/cbmc/Pointer_byte_extract5/main.i

@@ -11,13 +11,13 @@ typedef union
 typedef struct
 {
   int Count;
-  Union List[1];
+  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

@@ -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
 --

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 13 failed
 --
 ^warning: ignoring
 --

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,13 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+int main()
+{
+  size_t pointer_width = sizeof(void *) * 8;
+  size_t object_bits = 8; // by default
+  size_t cbmc_max_alloc_size = ((size_t)1 << (pointer_width - object_bits)) - 1;
+  int *p = malloc(cbmc_max_alloc_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
+
+^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
+
+^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,14 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+int main()
+{
+  size_t pointer_width = sizeof(void *) * 8;
+  size_t object_bits = 8; // by default
+  size_t cbmc_max_alloc_size = ((size_t)1 << (pointer_width - object_bits)) - 1;
+  // try to allocate the smallest violating amount
+  int *p = malloc(cbmc_max_alloc_size + 1);
+
+  return 0;
+}

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

@@ -0,0 +1,9 @@
+CORE
+one_byte_too_large.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[malloc.assertion.\d+\] line \d+ max allocation size exceeded: 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 13 failed
 --
 ^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE
 ^warning: ignoring

regression/cbmc/r_w_ok1/main.c

@@ -16,6 +16,13 @@ int main()
   assert(__CPROVER_w_ok(p, sizeof(int)));
 
   size_t n;
+
+  // n is arbitrary but no larger than what CBMC can represent
+  size_t pointer_width = sizeof(void *) * 8;
+  size_t object_bits = 8; // by default
+  size_t cbmc_max_alloc_size = ((size_t)1 << (pointer_width - object_bits)) - 1;
+  __CPROVER_assume(n <= cbmc_max_alloc_size);
+
   char *arbitrary_size = malloc(n);
 
   assert(__CPROVER_r_ok(arbitrary_size, n));

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$

src/ansi-c/ansi_c_internal_additions.cpp

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

src/ansi-c/library/cprover.h

@@ -16,6 +16,8 @@ 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 __CPROVER_size_t __CPROVER_pointer_width;
+extern __CPROVER_size_t __CPROVER_object_bits;
 
 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,36 @@ 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(
+      malloc_size < ((__CPROVER_size_t)1
+                     << (__CPROVER_pointer_width - __CPROVER_object_bits)),
+      "max allocation size exceeded");
+    __CPROVER_assume(
+      malloc_size < ((__CPROVER_size_t)1
+                     << (__CPROVER_pointer_width - __CPROVER_object_bits)));
+
+    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;
+
+    // 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;
 
-  // 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;
+    // 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;
+    return malloc_res;
 }
 
 /* FUNCTION: __builtin_alloca */