Replace __CPROVER_malloc_is_new_array by an uninterpreted function

With this encoding we no longer non-deterministically track just one
such array. This enables the use in assumptions. Also, we will only
incur a cost in the encoding when actually using new/delete instead of
always having a global variable, even when unused.

Author: tautschnig

src/ansi-c/ansi_c_internal_additions.cpp

@@ -179,7 +179,6 @@ void ansi_c_internal_additions(std::string &code)
     "const void *" CPROVER_PREFIX "deallocated=0;\n"
     "const void *" CPROVER_PREFIX "dead_object=0;\n"
     "const void *" CPROVER_PREFIX "new_object=0;\n" // for C++
-    CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array=0;\n" // for C++
     "const void *" CPROVER_PREFIX "memory_leak=0;\n"
     "void *" CPROVER_PREFIX "allocate("
       CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"

src/ansi-c/library/cprover.h

@@ -13,7 +13,6 @@ typedef __typeof__(sizeof(int)) __CPROVER_size_t;
 void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
 extern const void *__CPROVER_deallocated;
 extern const void *__CPROVER_new_object;
-extern _Bool __CPROVER_malloc_is_new_array;
 extern const void *__CPROVER_memory_leak;
 
 extern int __CPROVER_malloc_failure_mode;

src/ansi-c/library/stdlib.c

@@ -109,11 +109,6 @@ __CPROVER_HIDE:;
   __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_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;
@@ -171,11 +166,6 @@ __CPROVER_HIDE:;
   __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_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;
@@ -201,10 +191,6 @@ inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
   // make sure it's not recorded as 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_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;
-
   // record alloca to detect invalid free
   __CPROVER_bool record_alloca = __VERIFIER_nondet___CPROVER_bool();
   __CPROVER_alloca_object = record_alloca ? res : __CPROVER_alloca_object;
@@ -233,6 +219,7 @@ __CPROVER_HIDE:;
 #undef free
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __CPROVER_uninterpreted_is_new_array(const void *);
 extern void *__CPROVER_alloca_object;
 
 inline void free(void *ptr)
@@ -254,7 +241,8 @@ inline void free(void *ptr)
   // catch people who try to use free(...) for stuff
   // allocated with new[]
   __CPROVER_precondition(
-    ptr == 0 || __CPROVER_new_object != ptr || !__CPROVER_malloc_is_new_array,
+    ptr == 0 || __CPROVER_new_object != ptr ||
+      !__CPROVER_uninterpreted_is_new_array(ptr),
     "free called for new[] object");
 
   // catch people who try to use free(...) with alloca

src/cpp/cpp_internal_additions.cpp

@@ -91,8 +91,6 @@ void cpp_internal_additions(std::ostream &out)
   out << "const void *" CPROVER_PREFIX "deallocated = 0;" << '\n';
   out << "const void *" CPROVER_PREFIX "dead_object = 0;" << '\n';
   out << "const void *" CPROVER_PREFIX "new_object = 0;" << '\n';
-  out << "" CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array = 0;"
-      << '\n';
   out << "const void *" CPROVER_PREFIX "memory_leak = 0;" << '\n';
   out << "void *" CPROVER_PREFIX "allocate("
       << CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);" << '\n';

src/cpp/library/cprover.h

@@ -14,7 +14,6 @@ typedef __typeof__(sizeof(int)) __CPROVER_size_t;
 void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
 extern const void *__CPROVER_deallocated;
 extern const void *__CPROVER_new_object;
-extern _Bool __CPROVER_malloc_is_new_array;
 extern const void *__CPROVER_memory_leak;
 
 void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__));

src/cpp/library/new.c

@@ -1,6 +1,7 @@
 /* FUNCTION: __new */
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __CPROVER_uninterpreted_is_new_array(const void *);
 
 inline void *__new(__typeof__(sizeof(int)) malloc_size)
 {
@@ -16,7 +17,7 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size)
   // non-deterministically record the object for delete/delete[] checking
   __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
   __CPROVER_new_object = record_malloc ? res : __CPROVER_new_object;
-  __CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;
+  __CPROVER_assume(!__CPROVER_uninterpreted_is_new_array(res));
 
   // detect memory leaks
   __CPROVER_bool record_may_leak=__VERIFIER_nondet___CPROVER_bool();
@@ -28,6 +29,7 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size)
 /* FUNCTION: __new_array */
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __CPROVER_uninterpreted_is_new_array(const void *);
 
 inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size)
 {
@@ -43,7 +45,7 @@ inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size)
   // non-deterministically record the object for delete/delete[] checking
   __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
   __CPROVER_new_object = record_malloc ? res : __CPROVER_new_object;
-  __CPROVER_malloc_is_new_array=record_malloc?1:__CPROVER_malloc_is_new_array;
+  __CPROVER_assume(__CPROVER_uninterpreted_is_new_array(res));
 
   // detect memory leaks
   __CPROVER_bool record_may_leak=__VERIFIER_nondet___CPROVER_bool();
@@ -66,6 +68,7 @@ inline void *__placement_new(__typeof__(sizeof(int)) malloc_size, void *p)
 /* FUNCTION: __delete */
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __CPROVER_uninterpreted_is_new_array(const void *);
 
 inline void __delete(void *ptr)
 {
@@ -81,7 +84,8 @@ inline void __delete(void *ptr)
 
   // catch people who call delete for objects allocated with new[]
   __CPROVER_precondition(
-    ptr == 0 || __CPROVER_new_object != ptr || !__CPROVER_malloc_is_new_array,
+    ptr == 0 || __CPROVER_new_object != ptr ||
+      !__CPROVER_uninterpreted_is_new_array(ptr),
     "delete of array object");
 
   // If ptr is NULL, no operation is performed.
@@ -101,6 +105,7 @@ inline void __delete(void *ptr)
 /* FUNCTION: __delete_array */
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __CPROVER_uninterpreted_is_new_array(const void *);
 
 inline void __delete_array(void *ptr)
 {
@@ -120,7 +125,8 @@ inline void __delete_array(void *ptr)
 
   // catch people who call delete[] for objects allocated with new
   __CPROVER_precondition(
-    ptr == 0 || __CPROVER_new_object != ptr || __CPROVER_malloc_is_new_array,
+    ptr == 0 || __CPROVER_new_object != ptr ||
+      __CPROVER_uninterpreted_is_new_array(ptr),
     "delete[] of non-array object");
 
   if(ptr!=0)