Track deallocated/dead in an array

This enables tracking of all deallocations and all dead objects, and
thereby use of deallocated/dead_object predicates within assumptions.

Author: tautschnig

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/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

@@ -264,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[]
@@ -602,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';