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