Fix invalidation of CARs on free and DEAD

SaswatPadhi · SaswatPadhi · commit 998d1417e0bd · 2021-10-06T23:57:05.000Z
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.
diff --git a/regression/contracts/assigns_enforce_free_dead/main.c b/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);
+}
diff --git a/regression/contracts/assigns_enforce_free_dead/test.desc b/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.
diff --git a/regression/contracts/test_aliasing_ensure_indirect/test.desc b/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
diff --git a/src/goto-instrument/contracts/contracts.cpp b/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"
 
@@ -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_inclusion_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,7 +914,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() &&
@@ -851,7 +948,8 @@ void code_contractst::check_frame_conditions(
   }
 }
 
-void code_contractst::add_inclusion_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_inclusion_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)
diff --git a/src/goto-instrument/contracts/contracts.h b/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_inclusion_check(
+  const assigns_clauset::conditional_address_ranget add_inclusion_check(
     goto_programt &,
     const assigns_clauset &,
     goto_programt::instructionst::iterator &,
