Detect repeated contract enforcement in goto-instrument#8754
Open
tautschnig wants to merge 1 commit into
Open
Conversation
tautschnig
force-pushed
the
fix-7830-contracts-twice
branch
from
6f45e45 to
e1ff67c
Compare
tautschnig
requested review from
feliperodri and
remi-delmas-3000
as code owners
There was a problem hiding this comment.
Pull request overview
Adds guards to prevent re-applying contract enforcement instrumentation when goto-instrument is run multiple times on already-instrumented binaries.
Changes:
- Detect prior DFCC instrumentation via a marker symbol and abort with an exception.
- Detect prior per-function contract enforcement by checking for the mangled “original” symbol and abort.
- Reorder
check_frame_conditions_functionto run after the new “already enforced” guard.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
| src/goto-instrument/contracts/dynamic-frames/dfcc.cpp | Adds a binary-level “already enforced” check via a marker symbol and throws invalid_input_exceptiont. |
| src/goto-instrument/contracts/contracts.cpp | Adds an “already enforced” check in enforce_contract by detecting the pre-existing mangled original symbol. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8754 +/- ##
===========================================
- Coverage 80.55% 80.55% -0.01%
===========================================
Files 1707 1707
Lines 189051 189061 +10
Branches 73 73
===========================================
+ Hits 152299 152307 +8
- Misses 36752 36754 +2 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
tautschnig
force-pushed
the
fix-7830-contracts-twice
branch
from
e1ff67c to
6b74fab
Compare
tautschnig
requested review from
a team,
kroening and
peterschrammel
as code owners
tautschnig
force-pushed
the
fix-7830-contracts-twice
branch
from
6b74fab to
6e62bc6
Compare
When goto-instrument is invoked multiple times to enforce contracts on
the same goto binary, the semantics break: without dfcc it fails during
checking, and with dfcc it fails due to arity mismatches from prior
instrumentation. The two paths have different invariants and the
diagnostics reflect that:
Non-dfcc path (contracts.cpp): the check is *per function*. A given
function can only be enforced once across the lifetime of a goto
binary; enforcing different functions across separate invocations
remains supported (each function gets its own
__CPROVER_contracts_original_<F> wrapper, so the wrappers do not
conflict). Enforcing multiple distinct functions in a *single*
invocation -- as exercised by regression/contracts/assigns_enforce_03
-- continues to work.
Dfcc path (dfcc.cpp): the check is *per binary*. The dfcc pipeline
cannot be applied a second time to a binary it has already
instrumented, regardless of which mode (--enforce-contract,
--replace-call-with-contract, --apply-loop-contracts, ...) ran the
first time.
For the non-dfcc path, check whether the mangled wrapper symbol
already exists for the function being enforced and throw an
invalid_input_exceptiont with a per-function error message.
For the dfcc path, check whether the marker symbol left by a prior
dfcc pass is present in the input goto binary, before constructing
the dfcct object. This check must happen before the dfcc library is
loaded, since the library constructor creates the marker as part of
normal operation. Use invalid_input_exceptiont for a user-friendly
error rather than PRECONDITION (which is for programming errors).
The error wording was kept generic ("DFCC instrumentation has already
been applied to this binary; only one DFCC pass per binary is
supported") because the guard fires for *any* prior dfcc pass, not
just contract enforcement.
Refactor: rename the marker symbol from "__dfcc_instrumented_functions"
to "__CPROVER_dfcc_instrumented_functions" to follow the reserved
namespace convention used elsewhere; expose its name as a public
constant `dfcc_libraryt::INSTRUMENTED_FUNCTIONS_MAP_NAME` and add a
public static helper `dfcc_libraryt::is_dfcc_instrumented(const
goto_modelt &)` so the check has a single source of truth and a
self-explanatory name.
Tests: add regression/contracts-repeat/ with a small custom chain.sh
that runs goto-instrument twice, and four test directories covering:
* enforce-same-function: the same function on both passes; second
pass must fail with the per-function error.
* enforce-different-functions: different functions on each pass;
both passes must succeed (locks in the asymmetric semantics).
* dfcc-enforce-twice: dfcc + --enforce-contract on both passes;
second pass must fail with the per-binary dfcc error.
* dfcc-replace-then-replace: dfcc + --replace-call-with-contract on
both passes (no --enforce-contract on either); confirms the dfcc
guard fires for non-enforce dfcc passes too, validating the
generic error wording.
Wire regression/contracts-repeat/ into regression/Makefile and
regression/CMakeLists.txt alongside contracts/ and contracts-dfcc/.
Fixes: diffblue#7830
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
fix-7830-contracts-twice
branch
from
6e62bc6 to
927af32
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
goto-instrument must detect when it is being invoked again when contract enforcement has already been run as only one contract can be enforced at a time.
Fixes: #7830