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

@@ -6,6 +6,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_malloc(malloc_size);
 
   // ensure it's not recorded as deallocated
@@ -31,6 +37,12 @@ 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:;
+  // 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_malloc(size*count);
 

src/ansi-c/library/stdlib.c

@@ -67,6 +67,12 @@ inline void *malloc(__CPROVER_size_t malloc_size);
 inline void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
 {
   __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 *res;
   res=malloc(nmemb*size);
   #ifdef __CPROVER_STRING_ABSTRACTION
@@ -92,6 +98,12 @@ inline void *malloc(__CPROVER_size_t malloc_size)
   // realistically, malloc may return NULL,
   // and __CPROVER_malloc 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_malloc(malloc_size);
 
@@ -116,6 +128,12 @@ inline void *malloc(__CPROVER_size_t malloc_size)
 inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
 {
   __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_malloc(alloca_size);