Track deallocated/dead in an array

regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc

@@ -1,13 +1,13 @@
 CORE broken-smt-backend
 main.c
 --smt2 --outfile -
-\(= \(select array_of\.2 i\) \(ite false #b1 #b0\)\)
+\(= \(select array_of\.\d+ i\) \(ite false #b1 #b0\)\)
 \(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1\)
 \(= \(select array\.3 \(_ bv\d+ 64\)\) \(ite false #b1 #b0\)\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
-\(= \(select array_of\.2 i\) false\)
+\(= \(select array_of\.\d+ i\) false\)
 \(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\)
 \(= \(select array\.3 \(_ bv\d+ 64\)\) false\)
 --

regression/cbmc/pointer-extra-checks/test.desc

@@ -10,7 +10,6 @@ main.c
 ^\[main.pointer_dereference.5\] .* dereference failure: pointer outside dynamic object bounds in \*r: SUCCESS$
 ^\[main.pointer_dereference.6\] .* dereference failure: pointer NULL in \*s: FAILURE$
 ^\[main.pointer_dereference.7\] .* dereference failure: pointer invalid in \*s: FAILURE$
-^\[main.pointer_dereference.8\] .* dereference failure: deallocated dynamic object in \*s: FAILURE$
 ^\[main.pointer_dereference.9\] .* dereference failure: dead object in \*s: FAILURE$
 ^\[main.pointer_dereference.10\] .* dereference failure: pointer outside object bounds in \*s: FAILURE$
 ^\[main.pointer_dereference.11\] .* dereference failure: invalid integer address in \*s: FAILURE$

regression/cbmc/r_w_ok10/main.c

@@ -0,0 +1,9 @@
+#include <stdlib.h>
+
+int main()
+{
+  int *p = malloc(sizeof(int));
+  free(p);
+  __CPROVER_assume(__CPROVER_r_ok(p, sizeof(int)));
+  __CPROVER_assert(0, "should be unreachable");
+}

regression/cbmc/r_w_ok10/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test checks that __CPROVER_r_ok can safely be used in assumptions.

regression/cbmc/r_w_ok11/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void foo(char *p, char *q)
+{
+  if(p)
+    free(p);
+  if(q)
+    free(q);
+}
+
+_Bool nondet_bool();
+
+int main()
+{
+  char *p = nondet_bool() ? NULL : malloc(10);
+  char *q = nondet_bool() ? NULL : malloc(12);
+  foo(p, q);
+  // no valid objects live at p or q anymore
+  assert(!__CPROVER_r_ok(p, 0) & !__CPROVER_r_ok(q, 0));
+}

regression/cbmc/r_w_ok11/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test checks that negations of __CPROVER_r_ok can safely be used.

regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc

@@ -1,7 +1,7 @@
 CORE
 test.c
 --malloc-may-fail --malloc-fail-null
-^\[main.precondition_instance.\d+] line \d+ double free: SUCCESS$
+^\[(free.precondition|main.precondition_instance).\d+] line \d+ double free: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

src/ansi-c/ansi_c_internal_additions.cpp

@@ -171,8 +171,10 @@ void ansi_c_internal_additions(std::string &code)
       CPROVER_PREFIX "constant_infinity_uint];\n"
 
     // malloc
-    "const void *" CPROVER_PREFIX "deallocated=0;\n"
-    "const void *" CPROVER_PREFIX "dead_object=0;\n"
+    CPROVER_PREFIX "bool " CPROVER_PREFIX "deallocated["
+      CPROVER_PREFIX "constant_infinity_uint];\n"
+    CPROVER_PREFIX "bool " CPROVER_PREFIX "dead_object["
+      CPROVER_PREFIX "constant_infinity_uint];\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"

src/ansi-c/goto_check_c.cpp

@@ -2214,15 +2214,9 @@ void goto_check_ct::goto_check(
         if(local_bitvector_analysis->dirty(variable))
         {
           // need to mark the dead variable as dead
-          exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
-          exprt address_of_expr = typecast_exprt::conditional_cast(
-            address_of_exprt(variable), lhs.type());
-          if_exprt rhs(
-            side_effect_expr_nondett(bool_typet(), i.source_location()),
-            std::move(address_of_expr),
-            lhs);
+          exprt lhs = dead_object(address_of_exprt{variable}, ns);
           new_code.add(goto_programt::make_assignment(
-            code_assignt{std::move(lhs), std::move(rhs), i.source_location()},
+            code_assignt{std::move(lhs), true_exprt{}, i.source_location()},
             i.source_location()));
         }
       }

src/ansi-c/library/cprover.h

@@ -20,7 +20,7 @@ typedef signed long long __CPROVER_ssize_t;
 
 void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
 void __CPROVER_deallocate(void *);
-extern const void *__CPROVER_deallocated;
+extern __CPROVER_bool __CPROVER_deallocated[];
 extern const void *__CPROVER_new_object;
 extern __CPROVER_bool __CPROVER_malloc_is_new_array;
 extern const void *__CPROVER_memory_leak;

src/ansi-c/library/stdlib.c

@@ -130,10 +130,6 @@ __CPROVER_HIDE:;
   // and __CPROVER_allocate doesn't, but no one cares
   malloc_res = __CPROVER_allocate(alloc_size, 1);
 
-  // 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_is_new_array =
@@ -194,10 +190,6 @@ __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;
-
   // record the object size for non-determistic bounds checking
   __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
   __CPROVER_malloc_is_new_array =
@@ -225,9 +217,6 @@ void *__builtin_alloca(__CPROVER_size_t alloca_size)
   void *res;
   res = __CPROVER_allocate(alloca_size, 0);
 
-  // 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;
@@ -275,8 +264,9 @@ void free(void *ptr)
                          "free argument has offset zero");
 
   // catch double free
-  __CPROVER_precondition(ptr==0 || __CPROVER_deallocated!=ptr,
-                         "double free");
+  __CPROVER_precondition(
+    ptr == 0 || !__CPROVER_deallocated[__CPROVER_POINTER_OBJECT(ptr)],
+    "double free");
 
   // catch people who try to use free(...) for stuff
   // allocated with new[]
@@ -613,10 +603,7 @@ __CPROVER_HIDE:;
 
 /* FUNCTION: __CPROVER_deallocate */
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
-
 void __CPROVER_deallocate(void *ptr)
 {
-  if(__VERIFIER_nondet___CPROVER_bool())
-    __CPROVER_deallocated = ptr;
+  __CPROVER_deallocated[__CPROVER_POINTER_OBJECT(ptr)] = 1;
 }

src/cpp/cpp_internal_additions.cpp

@@ -88,8 +88,12 @@ void cpp_internal_additions(std::ostream &out)
       << CPROVER_PREFIX "memory[__CPROVER::constant_infinity_uint];" << '\n';
 
   // malloc
-  out << "const void *" CPROVER_PREFIX "deallocated = 0;" << '\n';
-  out << "const void *" CPROVER_PREFIX "dead_object = 0;" << '\n';
+  out << CPROVER_PREFIX "bool "
+      << CPROVER_PREFIX "deallocated[__CPROVER::constant_infinity_uint];"
+      << '\n';
+  out << CPROVER_PREFIX "bool "
+      << CPROVER_PREFIX "dead_object[__CPROVER::constant_infinity_uint];"
+      << '\n';
   out << "const void *" CPROVER_PREFIX "new_object = 0;" << '\n';
   out << "" CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array = 0;"
       << '\n';

src/cpp/library/new.c

@@ -10,9 +10,6 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size)
   void *res;
   res = __CPROVER_allocate(malloc_size, 0);
 
-  // ensure it's not recorded as deallocated
-  __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
-
   // 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;
@@ -37,9 +34,6 @@ inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size)
   void *res;
   res = __CPROVER_allocate(size*count, 0);
 
-  // ensure it's not recorded as deallocated
-  __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
-
   // 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;
@@ -77,7 +71,9 @@ inline void __delete(void *ptr)
                          "delete argument must have offset zero");
 
   // catch double delete
-  __CPROVER_precondition(ptr==0 || __CPROVER_deallocated!=ptr, "double delete");
+  __CPROVER_precondition(
+    ptr == 0 || !__CPROVER_deallocated[__CPROVER_POINTER_OBJECT(ptr)],
+    "double delete");
 
   // catch people who call delete for objects allocated with new[]
   __CPROVER_precondition(
@@ -113,8 +109,9 @@ inline void __delete_array(void *ptr)
                          "delete argument must have offset zero");
 
   // catch double delete
-  __CPROVER_precondition(ptr==0 || __CPROVER_deallocated!=ptr,
-                         "double delete");
+  __CPROVER_precondition(
+    ptr == 0 || !__CPROVER_deallocated[__CPROVER_POINTER_OBJECT(ptr)],
+    "double delete");
 
   // catch people who call delete[] for objects allocated with new
   __CPROVER_precondition(

src/goto-programs/builtin_functions.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/mathematical_expr.h>
 #include <util/mathematical_types.h>
 #include <util/pointer_expr.h>
+#include <util/pointer_predicates.h>
 #include <util/prefix.h>
 #include <util/rational.h>
 #include <util/rational_tools.h>
@@ -1415,16 +1416,9 @@ void goto_convertt::do_function_call_symbol(
       make_temp_symbol(new_lhs, "alloca", dest, mode);
 
     // mark pointer to alloca result as dead
-    symbol_exprt dead_object_sym =
-      ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
-    exprt alloca_result =
-      typecast_exprt::conditional_cast(new_lhs, dead_object_sym.type());
-    if_exprt rhs{
-      side_effect_expr_nondett{bool_typet(), source_location},
-      std::move(alloca_result),
-      dead_object_sym};
+    exprt dead_object_expr = dead_object(new_lhs, ns);
     code_assignt assign{
-      std::move(dead_object_sym), std::move(rhs), source_location};
+      std::move(dead_object_expr), true_exprt{}, source_location};
     targets.destructor_stack.add(assign);
   }
   else

src/util/pointer_predicates.cpp

@@ -45,15 +45,19 @@ exprt deallocated(const exprt &pointer, const namespacet &ns)
   // we check __CPROVER_deallocated!
   const symbolt &deallocated_symbol=ns.lookup(CPROVER_PREFIX "deallocated");
 
-  return same_object(pointer, deallocated_symbol.symbol_expr());
+  return index_exprt{
+    deallocated_symbol.symbol_expr(),
+    typecast_exprt::conditional_cast(pointer_object(pointer), index_type())};
 }
 
 exprt dead_object(const exprt &pointer, const namespacet &ns)
 {
   // we check __CPROVER_dead_object!
   const symbolt &deallocated_symbol=ns.lookup(CPROVER_PREFIX "dead_object");
 
-  return same_object(pointer, deallocated_symbol.symbol_expr());
+  return index_exprt{
+    deallocated_symbol.symbol_expr(),
+    typecast_exprt::conditional_cast(pointer_object(pointer), index_type())};
 }
 
 exprt good_pointer(const exprt &pointer)