From 39f9c874aecc2d704e10c560d842ff11b198483f Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 3 Jan 2025 12:44:52 -0500 Subject: [PATCH 1/2] 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. --- .../dynamic-frames/dfcc_instrument.cpp | 62 ------------------- .../dynamic-frames/dfcc_instrument.h | 7 --- 2 files changed, 69 deletions(-) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp index 5e0fdd92c5e..ea0417d3371 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/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 -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) { diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h index 1d3494de226..1b9836e9752 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h +++ b/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 - 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 From b6bae9014d93a2b2ebbfb0ab007cac70f97ac290 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 3 Jan 2025 12:53:51 -0500 Subject: [PATCH 2/2] Fix dangling doxygen ref. --- src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h index 1b9836e9752..809542d1919 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h @@ -285,8 +285,6 @@ class dfcc_instrumentt /// 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 - /// pointer expression is removed from \p write_set. /// If \p rhs is a `side_effect_expr(ID_allocate)`, the allocated pointer gets /// added to the \p write_set. /// \pre \p target points to an `ASSIGN` instruction.