Constrain the malloc/alloca size to fit our object:offset encoding

See diffblue#311 for an extended discussion.

Author: tautschnig

src/ansi-c/library/new.c

@@ -8,6 +8,12 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size)
   // This just does memory allocation.
   __CPROVER_HIDE:;
   void *res;
+  // ensure that all bytes in the allocated memory can be addressed
+  // using our object:offset encoding as specified in
+  // flattening/pointer_logic.h; also avoid sign-extension issues
+  // for 32-bit systems that yields a maximum allocation of 2^23-1,
+  // i.e., just under 8MB
+  __CPROVER_assume(malloc_size < (1ULL << ((sizeof(char*) - 1) * 8 - 1)));
   res = __CPROVER_allocate(malloc_size, 0);
 
   // ensure it's not recorded as deallocated
@@ -34,22 +40,32 @@ inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size)
 {
   // The constructor call is done by the front-end.
   // This just does memory allocation.
-  __CPROVER_HIDE:;
+
+__CPROVER_HIDE:;
+
+  // ensure that all bytes in the allocated memory can be addressed
+  // using our object:offset encoding as specified in
+  // flattening/pointer_logic.h; also avoid sign-extension issues
+  // for 32-bit systems that yields a maximum allocation of 2^23-1,
+  // i.e., just under 8MB
+  __CPROVER_assume(size * count < (1ULL << ((sizeof(char*) - 1) * 8 - 1)));
   void *res;
-  res = __CPROVER_allocate(size*count, 0);
+  res = __CPROVER_allocate(size * count, 0);
 
   // ensure it's not recorded as deallocated
-  __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
+  __CPROVER_deallocated =
+    (res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated;
 
   // non-deterministically record the object size for bounds checking
-  __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
-  __CPROVER_malloc_object=record_malloc?res:__CPROVER_malloc_object;
-  __CPROVER_malloc_size=record_malloc?size*count:__CPROVER_malloc_size;
-  __CPROVER_malloc_is_new_array=record_malloc?1:__CPROVER_malloc_is_new_array;
+  __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
+  __CPROVER_malloc_object = record_malloc ? res : __CPROVER_malloc_object;
+  __CPROVER_malloc_size = record_malloc ? size * count : __CPROVER_malloc_size;
+  __CPROVER_malloc_is_new_array =
+    record_malloc ? 1 : __CPROVER_malloc_is_new_array;
 
   // detect memory leaks
-  __CPROVER_bool record_may_leak=__VERIFIER_nondet___CPROVER_bool();
-  __CPROVER_memory_leak=record_may_leak?res:__CPROVER_memory_leak;
+  __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
+  __CPROVER_memory_leak = record_may_leak ? res : __CPROVER_memory_leak;
 
   return res;
 }

src/ansi-c/library/stdlib.c

@@ -65,9 +65,17 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 
 inline void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
 {
-  // realistically, calloc may return NULL,
-  // and __CPROVER_allocate doesn't, but no one cares
-  __CPROVER_HIDE:;
+// realistically, calloc may return NULL,
+// and __CPROVER_allocate doesn't, but no one cares
+
+__CPROVER_HIDE:;
+
+  // ensure that all bytes in the allocated memory can be addressed
+  // using our object:offset encoding as specified in
+  // flattening/pointer_logic.h; also avoid sign-extension issues
+  // for 32-bit systems that yields a maximum allocation of 2^23-1,
+  // i.e., just under 8MB
+  __CPROVER_assume(nmemb * size < (1ULL << ((sizeof(char*) - 1) * 8 - 1)));
   void *malloc_res;
   malloc_res = __CPROVER_allocate(nmemb * size, 1);
 
@@ -104,8 +112,16 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 inline void *malloc(__CPROVER_size_t malloc_size)
 {
   // realistically, malloc may return NULL,
-  // and __CPROVER_allocate doesn't, but no one cares
-  __CPROVER_HIDE:;
+// and __CPROVER_allocate doesn't, but no one cares
+
+__CPROVER_HIDE:;
+
+  // ensure that all bytes in the allocated memory can be addressed
+  // using our object:offset encoding as specified in
+  // flattening/pointer_logic.h; also avoid sign-extension issues
+  // for 32-bit systems that yields a maximum allocation of 2^23-1,
+  // i.e., just under 8MB
+  __CPROVER_assume(malloc_size < (1ULL << ((sizeof(char*) - 1) * 8 - 1)));
   void *malloc_res;
   malloc_res = __CPROVER_allocate(malloc_size, 0);
 
@@ -131,18 +147,27 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 
 inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
 {
-  __CPROVER_HIDE:;
+__CPROVER_HIDE:;
+
+  // ensure that all bytes in the allocated memory can be addressed
+  // using our object:offset encoding as specified in
+  // flattening/pointer_logic.h; also avoid sign-extension issues
+  // for 32-bit systems that yields a maximum allocation of 2^23-1,
+  // i.e., just under 8MB
+  __CPROVER_assume(alloca_size < (1ULL << ((sizeof(char*) - 1) * 8 - 1)));
   void *res;
   res = __CPROVER_allocate(alloca_size, 0);
 
   // make sure it's not recorded as deallocated
-  __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
+  __CPROVER_deallocated =
+    (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?res:__CPROVER_malloc_object;
-  __CPROVER_malloc_size=record_malloc?alloca_size:__CPROVER_malloc_size;
-  __CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;
+  __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
+  __CPROVER_malloc_object = record_malloc ? res : __CPROVER_malloc_object;
+  __CPROVER_malloc_size = record_malloc ? alloca_size : __CPROVER_malloc_size;
+  __CPROVER_malloc_is_new_array =
+    record_malloc ? 0 : __CPROVER_malloc_is_new_array;
 
   return res;
 }