CONTRACTS: don't instrument __CPROVER_dead_object anymore.

This change fixes spurious violations on GOTO models generated from MIR programs by Kani. MIR programs declare all stack-allocated place variables at the top of the function regardless of the original scope of the variable, and uses `storageLive` and `storageDead` events to delimit their dynamic lifetime. Kani uses a DECL to introduce place variables and uses dynamic assignments to `__CPROVER_dead_object` to encode `storageLive` and `storageDead`. DFCC instrumentation would only pick up `storageDead` events, not `storageLive`, resulting in spurious proof failures.

With this change we go back to relying only on DECL/DEAD for object liftetime tracking in DFCC and completely ignoring dynamic assignments `__CPROVER_dead_object`. This means that contract instrumentation won't be able to detect bad accesses to objects for which the lifetime is managed via `__CPROVER_dead_object`, for intance: dynamic stack-allocated objects created using `alloca`, or MIR place variables as encoded by Kani. As a consequence `--pointer-checks` have to be enabled when analysing contracts-instrumented code.

Author: Remi Delmas

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp

@@ -735,31 +735,6 @@ void dfcc_instrumentt::instrument_lhs(
   insert_before_swap_and_advance(goto_program, target, payload);
 }
 
-/// Checks if lhs is the `dead_object`, and if the rhs
-/// is an `if_exprt(nondet, ptr, dead_object)` expression.
-/// Returns `ptr` if the pattern was matched, nullptr otherwise.
-std::optional<exprt>
-dfcc_instrumentt::is_dead_object_update(const exprt &lhs, const exprt &rhs)
-{
-  if(
-    lhs.id() == ID_symbol &&
-    to_symbol_expr(lhs).get_identifier() == CPROVER_PREFIX "dead_object" &&
-    rhs.id() == ID_if)
-  {
-    // only handle `if_exprt(nondet, ptr, dead_object)`
-    auto &if_expr = to_if_expr(rhs);
-    if(
-      if_expr.cond().id() == ID_side_effect &&
-      to_side_effect_expr(if_expr.cond()).get_statement() == ID_nondet &&
-      if_expr.false_case() == lhs)
-    {
-      return if_expr.true_case();
-    }
-  }
-
-  return {};
-}
-
 void dfcc_instrumentt::instrument_assign(
   const irep_idt &function_id,
   goto_programt::targett &target,
@@ -775,43 +750,6 @@ void dfcc_instrumentt::instrument_assign(
   if(cfg_info.must_check_lhs(target))
     instrument_lhs(function_id, target, lhs, goto_program, cfg_info);
 
-  // handle dead_object updates (created by __builtin_alloca for instance)
-  // Remark: we do not really need to track this deallocation since the default
-  // CBMC checks are already able to detect writes to DEAD objects
-  const auto dead_ptr = is_dead_object_update(lhs, rhs);
-  if(dead_ptr.has_value())
-  {
-    // ```
-    // ASSIGN dead_object := if_exprt(nondet, ptr, dead_object);
-    // ----
-    // IF !write_set GOTO skip_target;
-    // CALL record_deallocated(write_set, ptr);
-    // skip_target: SKIP;
-    // ```
-
-    // step over the instruction
-    target++;
-
-    goto_programt payload;
-
-    auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
-      dfcc_utilst::make_null_check_expr(write_set), target_location));
-
-    payload.add(goto_programt::make_function_call(
-      library.write_set_record_dead_call(
-        write_set, dead_ptr.value(), target_location),
-      target_location));
-
-    auto label_instruction =
-      payload.add(goto_programt::make_skip(target_location));
-    goto_instruction->complete_goto(label_instruction);
-
-    insert_before_swap_and_advance(goto_program, target, payload);
-
-    // step back
-    target--;
-  }
-
   // is the rhs expression a side_effect("allocate") expression ?
   if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_allocate)
   {

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h

@@ -283,13 +283,6 @@ class dfcc_instrumentt
     goto_programt &goto_program,
     dfcc_cfg_infot &cfg_info);
 
-  /// Checks if \p lhs is the `dead_object`, and if \p rhs
-  /// is an `if_exprt(nondet, ptr, dead_object)` expression.
-  /// Returns a pointer to the `ptr` expression if the pattern was matched,
-  /// returns `nullptr` otherwise.
-  std::optional<exprt>
-  is_dead_object_update(const exprt &lhs, const exprt &rhs);
-
   /// Instrument the \p lhs of an `ASSIGN lhs := rhs` instruction by
   /// adding an inclusion check of \p lhs in \p write_set.
   /// If \ref is_dead_object_update returns a successful match, the matched