Fix invalidation of CARs on free and DEAD

Previously, corresponding CARs were completely removed on DEAD
instructions. While this is "okay" for unconditionally dead symbols, it
resulted in spurious non-assignable errors when symbols were only
conditionally DEAD, e.g. RETURN within a conditional block.

Previously, invalid CARs from free calls were simply left behind,
because (in theory) the CAR validation condition should automatically
guard against conditions.

However, in both these cases, we need to check dead/deallocated status
of individual objects to avoid spurious errors from CBMC's internal
pointer checks, which only track a single dead/deallocated object
nondeterministically.

Author: SaswatPadhi

regression/contracts/assigns_enforce_free_dead/main.c

@@ -0,0 +1,58 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int foo(int *x, int **p) __CPROVER_assigns(*x, *p, **p)
+{
+  if(p && *p)
+    **p = 0;
+
+  {
+    int y;
+    y = 1;
+    *x = 0;
+
+    if(nondet_bool())
+      return 0;
+
+    if(p)
+      *p = &y;
+
+    // y goes DEAD here
+  }
+
+  if(p && *p)
+    **p = 0;
+
+  int a = 1;
+
+  if(x == NULL)
+  {
+    return 1;
+    // a goes DEAD here
+  }
+
+  int *z = malloc(100 * sizeof(int));
+  int *w = NULL;
+
+  if(z)
+  {
+    w = &(z[10]);
+    *w = 0;
+
+    int *q = &(z[20]);
+    *q = 1;
+    // q goes DEAD here
+  }
+
+  free(z);
+
+  *x = 1;
+  x = 0;
+}
+
+int main()
+{
+  int z;
+  int *x = malloc(sizeof(int));
+  foo(&z, &x);
+}

regression/contracts/assigns_enforce_free_dead/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo _ --malloc-may-fail --malloc-fail-null --pointer-primitive-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether CBMC properly tracks invalidated CARs
+on free and DEAD instructions.

regression/contracts/test_aliasing_ensure_indirect/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract foo --enforce-contract bar
+--enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
 \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS

src/goto-instrument/contracts/contracts.cpp

@@ -669,21 +669,75 @@ void code_contractst::instrument_call_statement(
       auto snapshot_instructions = car->generate_snapshot_instructions();
       insert_before_swap_and_advance(
         body, instruction_it, snapshot_instructions);
-      // since CAR was inserted *after* the malloc,
+      // since CAR was inserted *after* the malloc call,
       // move the instruction pointer backward,
       // because the caller increments it in a `for` loop
       instruction_it--;
     }
-    return;
   }
   else if(callee_name == "free")
   {
-    add_containment_check(
-      body,
-      assigns,
-      instruction_it,
-      pointer_object(instruction_it->call_arguments().front()));
-    return;
+    const auto &pointer = instruction_it->call_arguments().front();
+    const auto object = pointer_object(pointer);
+    add_containment_check(body, assigns, instruction_it, object);
+
+    // Since the argument to free would be an "alias" (but not identical)
+    // to an existing CAR's source_expr, structural equality wouldn't work.
+    // Moreover, multiple CARs in the writeset might be aliased to the
+    // same underlying object.
+    // So, we first find the corresponding CAR using `same_object` checks.
+    goto_programt invalidation_instructions;
+    std::unordered_set<exprt, irep_hash> temps;
+
+    for(const auto &car : assigns.get_write_set())
+    {
+      const auto object_validity_var_addr =
+        new_tmp_symbol(
+          pointer_type(bool_typet{}),
+          instruction_it->source_location,
+          symbol_table.lookup_ref(function).mode,
+          symbol_table)
+          .symbol_expr();
+      temps.insert(object_validity_var_addr);
+
+      invalidation_instructions.add(goto_programt::make_decl(
+        object_validity_var_addr, instruction_it->source_location));
+      // if the CAR was defined on the same_object as the one being `free`d,
+      // record its validity variable's address, otherwise record NULL
+      invalidation_instructions.add(goto_programt::make_assignment(
+        object_validity_var_addr,
+        if_exprt{
+          and_exprt{car.validity_condition_var,
+                    same_object(pointer, car.lower_bound_address_var)},
+          address_of_exprt{car.validity_condition_var},
+          null_pointer_exprt{to_pointer_type(object_validity_var_addr.type())}},
+        instruction_it->source_location));
+    }
+
+    insert_before_swap_and_advance(
+      body, instruction_it, invalidation_instructions);
+
+    // move past the call and then insert the invalidation instructions
+    instruction_it++;
+    // invalidate all recorded CAR validity variables
+    for(const auto &car_validity_addr : temps)
+    {
+      goto_programt skip_program;
+      const auto skip_target = skip_program.add(
+        goto_programt::make_skip(instruction_it->source_location));
+      invalidation_instructions.add(goto_programt::make_goto(
+        skip_target,
+        null_pointer(car_validity_addr),
+        instruction_it->source_location));
+      invalidation_instructions.add(goto_programt::make_assignment(
+        dereference_exprt{car_validity_addr},
+        false_exprt{},
+        instruction_it->source_location));
+      invalidation_instructions.destructive_append(skip_program);
+    }
+    insert_before_swap_and_advance(
+      body, instruction_it, invalidation_instructions);
+    instruction_it--;
   }
 }
 
@@ -823,9 +877,9 @@ void code_contractst::check_frame_conditions(
       auto snapshot_instructions = car->generate_snapshot_instructions();
       insert_before_swap_and_advance(
         body, instruction_it, snapshot_instructions);
-      // since CAR was inserted *after* the DECL,
+      // since CAR was inserted *after* the DECL instruction,
       // move the instruction pointer backward,
-      // because the caller increments it in a `for` loop
+      // because the `for` loop takes care of the increment
       instruction_it--;
     }
     else if(instruction_it->is_assign())
@@ -838,7 +892,28 @@ void code_contractst::check_frame_conditions(
     }
     else if(instruction_it->is_dead())
     {
-      assigns.remove_from_write_set(instruction_it->dead_symbol());
+      const auto &symbol = instruction_it->dead_symbol();
+      // CAR equality and hash are defined on source_expr alone,
+      // therefore this temporary CAR should be "found"
+      const auto &symbol_car = assigns.get_write_set().find(
+        assigns_clauset::conditional_address_ranget{assigns, symbol});
+      if(symbol_car != assigns.get_write_set().end())
+      {
+        instruction_it++;
+        auto invalidation_assignment = goto_programt::make_assignment(
+          symbol_car->validity_condition_var,
+          false_exprt{},
+          instruction_it->source_location);
+        // note that instruction_it is not advanced by this call,
+        // so no need to move it backwards
+        body.insert_before_swap(instruction_it, invalidation_assignment);
+      }
+      else
+      {
+        throw incorrect_goto_program_exceptiont(
+          "Found a `DEAD` variable without corresponding `DECL`!",
+          instruction_it->source_location);
+      }
     }
     else if(
       instruction_it->is_other() &&