Fix invalidation for DEAD and free instructions

Author: SaswatPadhi

regression/contracts/assigns_enforce_free_dead/main.c

@@ -0,0 +1,44 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int foo(int *x) __CPROVER_assigns(*x)
+{
+  {
+    int y;
+    y = 1;
+    *x = 0;
+    // y goes DEAD here
+  }
+
+  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;
+  foo(&z);
+}

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.

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() &&