Fix invalidation of CARs on free and DEAD instructions

regression/contracts/assigns_enforce_free_dead/main.c

@@ -0,0 +1,65 @@
+#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, unconditionally
+  }
+
+  if(p && *p)
+    **p = 0;
+
+  int a = 1;
+
+  if(x == NULL)
+  {
+    return 1;
+    // a goes DEAD here, conditionally
+  }
+
+  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, unconditionally
+  }
+
+  free(z);
+
+  z = malloc(sizeof(int));
+  if(nondet_bool())
+  {
+    free(z);
+    // here z is deallocated, conditionally
+  }
+
+  *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,43 @@
+CORE
+main.c
+--enforce-contract foo _ --malloc-may-fail --malloc-fail-null --pointer-primitive-check
+^\[foo.\d+\] line \d+ Check that \*\(\*p\) is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that \*\(\*p\) is assignable: FAILURE$
+^\[foo.\d+\] line \d+ Check that \*p is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that \*q is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that \*w is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that q is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that w is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that x is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: SUCCESS$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^\[foo.\d+\] line \d+ Check that \*p is assignable: FAILURE$
+^\[foo.\d+\] line \d+ Check that \*q is assignable: FAILURE$
+^\[foo.\d+\] line \d+ Check that \*w is assignable: FAILURE$
+^\[foo.\d+\] line \d+ Check that \*x is assignable: FAILURE$
+^\[foo.\d+\] line \d+ Check that a is assignable: FAILURE$
+^\[foo.\d+\] line \d+ Check that q is assignable: FAILURE$
+^\[foo.\d+\] line \d+ Check that w is assignable: FAILURE$
+^\[foo.\d+\] line \d+ Check that x is assignable: FAILURE$
+^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$
+^\[foo.\d+\] line \d+ Check that z is assignable: FAILURE$
+^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: FAILURE$
+^.*tmp_cc\$\d+.*: FAILURE$
+--
+Checks that invalidated CARs are correctly tracked on `free` and `DEAD`.
+
+Since several variables are assigned multiple times,
+we rule out all failures using the negative regex matches above.
+
+We also check (using positive regex matches above) that
+`**p` should be assignable in one case and should not be assignable in the other.
+
+Finally, we check that there should be no "internal" assertion failures
+on `tmp_cc` variables used to track CARs.

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/assigns.cpp

@@ -86,6 +86,15 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
   instructions.add(goto_programt::make_decl(lower_bound_address_var, location));
   instructions.add(goto_programt::make_decl(upper_bound_address_var, location));
 
+  instructions.add(goto_programt::make_assignment(
+    lower_bound_address_var,
+    null_pointer_exprt{to_pointer_type(slice.first.type())},
+    location));
+  instructions.add(goto_programt::make_assignment(
+    upper_bound_address_var,
+    null_pointer_exprt{to_pointer_type(slice.first.type())},
+    location));
+
   goto_programt skip_program;
   const auto skip_target = skip_program.add(goto_programt::make_skip(location));
 

src/goto-instrument/contracts/contracts.cpp

@@ -37,7 +37,6 @@ Date: February 2016
 #include <util/pointer_predicates.h>
 #include <util/replace_symbol.h>
 
-#include "assigns.h"
 #include "memory_predicates.h"
 #include "utils.h"
 
@@ -637,7 +636,7 @@ void code_contractst::instrument_assign_statement(
     "The first instruction of instrument_assign_statement should always be"
     " an assignment");
 
-  add_containment_check(
+  add_inclusion_check(
     program, assigns_clause, instruction_it, instruction_it->assign_lhs());
 }
 
@@ -669,21 +668,98 @@ 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(
+    const auto free_car = add_inclusion_check(
       body,
       assigns,
       instruction_it,
       pointer_object(instruction_it->call_arguments().front()));
-    return;
+
+    // skip all invalidation business if we're freeing invalid memory
+    goto_programt alias_checking_instructions, skip_program;
+    alias_checking_instructions.add(goto_programt::make_goto(
+      skip_program.add(
+        goto_programt::make_skip(instruction_it->source_location)),
+      not_exprt{free_car.validity_condition_var},
+      instruction_it->source_location));
+
+    // Since the argument to free may be an "alias" (but not identical)
+    // to existing CARs' 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.
+    std::unordered_set<exprt, irep_hash> write_set_validity_addrs;
+    for(const auto &w_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();
+      write_set_validity_addrs.insert(object_validity_var_addr);
+
+      alias_checking_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
+      alias_checking_instructions.add(goto_programt::make_assignment(
+        object_validity_var_addr,
+        if_exprt{
+          and_exprt{
+            w_car.validity_condition_var,
+            same_object(
+              free_car.lower_bound_address_var, w_car.lower_bound_address_var)},
+          address_of_exprt{w_car.validity_condition_var},
+          null_pointer_exprt{to_pointer_type(object_validity_var_addr.type())}},
+        instruction_it->source_location));
+    }
+
+    alias_checking_instructions.destructive_append(skip_program);
+    insert_before_swap_and_advance(
+      body, instruction_it, alias_checking_instructions);
+
+    // move past the call and then insert the invalidation instructions
+    instruction_it++;
+
+    // skip all invalidation business if we're freeing invalid memory
+    goto_programt invalidation_instructions;
+    skip_program.clear();
+    invalidation_instructions.add(goto_programt::make_goto(
+      skip_program.add(
+        goto_programt::make_skip(instruction_it->source_location)),
+      not_exprt{free_car.validity_condition_var},
+      instruction_it->source_location));
+
+    // invalidate all recorded CAR validity variables
+    for(const auto &w_car_validity_addr : write_set_validity_addrs)
+    {
+      goto_programt w_car_skip_program;
+      invalidation_instructions.add(goto_programt::make_goto(
+        w_car_skip_program.add(
+          goto_programt::make_skip(instruction_it->source_location)),
+        null_pointer(w_car_validity_addr),
+        instruction_it->source_location));
+      invalidation_instructions.add(goto_programt::make_assignment(
+        dereference_exprt{w_car_validity_addr},
+        false_exprt{},
+        instruction_it->source_location));
+      invalidation_instructions.destructive_append(w_car_skip_program);
+    }
+
+    invalidation_instructions.destructive_append(skip_program);
+    insert_before_swap_and_advance(
+      body, instruction_it, invalidation_instructions);
+
+    instruction_it--;
   }
 }
 
@@ -823,9 +899,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,20 +914,42 @@ 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() &&
       instruction_it->get_other().get_statement() == ID_havoc_object)
     {
       const exprt &havoc_argument = dereference_exprt(
         to_typecast_expr(instruction_it->get_other().operands().front()).op());
-      add_containment_check(body, assigns, instruction_it, havoc_argument);
+      add_inclusion_check(body, assigns, instruction_it, havoc_argument);
     }
   }
 }
 
-void code_contractst::add_containment_check(
+const assigns_clauset::conditional_address_ranget
+code_contractst::add_inclusion_check(
   goto_programt &program,
   const assigns_clauset &assigns,
   goto_programt::instructionst::iterator &instruction_it,
@@ -868,6 +966,8 @@ void code_contractst::add_containment_check(
   assertion.instructions.back().source_location.set_comment(
     "Check that " + from_expr(ns, expr.id(), expr) + " is assignable");
   insert_before_swap_and_advance(program, instruction_it, assertion);
+
+  return car;
 }
 
 bool code_contractst::enforce_contract(const irep_idt &function)

src/goto-instrument/contracts/contracts.h

@@ -30,6 +30,8 @@ Date: February 2016
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
 
+#include "assigns.h"
+
 #define FLAG_LOOP_CONTRACTS "apply-loop-contracts"
 #define HELP_LOOP_CONTRACTS                                                    \
   " --apply-loop-contracts\n"                                                  \
@@ -44,7 +46,6 @@ Date: February 2016
 #define HELP_ENFORCE_CONTRACT                                                  \
   " --enforce-contract <fun>     wrap fun with an assertion of its contract\n"
 
-class assigns_clauset;
 class local_may_aliast;
 class replace_symbolt;
 
@@ -134,7 +135,7 @@ class code_contractst
 
   /// Inserts an assertion into the goto program to ensure that
   /// an expression is within the assignable memory frame.
-  void add_containment_check(
+  const assigns_clauset::conditional_address_ranget add_inclusion_check(
     goto_programt &,
     const assigns_clauset &,
     goto_programt::instructionst::iterator &,
@@ -144,19 +145,17 @@ class code_contractst
   /// a goto statement that jumps back.
   bool check_for_looped_mallocs(const goto_programt &program);
 
-  /// Inserts an assertion statement into program before the assignment
+  /// Inserts an assertion into program immediately before the assignment
   /// instruction_it, to ensure that the left-hand-side of the assignment
-  /// aliases some expression in original_references, unless it is contained
-  /// in freely assignable set.
+  /// is "included" in the (conditional address ranges in the) write set.
   void instrument_assign_statement(
     goto_programt::instructionst::iterator &,
     goto_programt &,
     assigns_clauset &);
 
-  /// Inserts an assertion statement into program before the function call at
-  /// ins_it, to ensure that any memory which may be written by the call is
-  /// aliased by some expression in assigns_references, unless it is contained
-  /// in freely assignable set.
+  /// Inserts an assertion into program immediately before the function call at
+  /// instruction_it, to ensure that all memory locations written to by the
+  // callee are "included" in the (conditional address ranges in the) write set.
   void instrument_call_statement(
     goto_programt::instructionst::iterator &,
     const irep_idt &,