Detect repeated contract enforcement in goto-instrument#8754
Open
tautschnig wants to merge 1 commit intodiffblue:developfrom
Open
Detect repeated contract enforcement in goto-instrument#8754tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig wants to merge 1 commit intodiffblue:developfrom
Conversation
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. For the non-dfcc path (contracts.cpp), check if the mangled symbol already exists before enforcing, and throw a user-facing error. For the dfcc path (dfcc.cpp), check if the __dfcc_instrumented_functions symbol exists 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 this symbol as part of normal operation. Use invalid_input_exceptiont for a user-friendly error message rather than PRECONDITION which is for programming errors. Fixes: diffblue#7830 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
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.
Comment on lines
+1223
to
+1230
| // Check if contract enforcement has already been applied to this function | ||
| if(symbol_table.has_symbol(mangled)) | ||
| { | ||
| throw invalid_input_exceptiont( | ||
| "Contract enforcement has already been applied to function '" + | ||
| id2string(function) + | ||
| "'.\nOnly one contract may be enforced at a time per function."); | ||
| } |
Comment on lines
+105
to
+111
| // Check if contract enforcement has already been applied to this binary | ||
| if(goto_model.symbol_table.has_symbol("__dfcc_instrumented_functions")) | ||
| { | ||
| throw invalid_input_exceptiont( | ||
| "Contract enforcement has already been applied to this binary.\n" | ||
| "Only one contract may be enforced at a time."); | ||
| } |
Comment on lines
+105
to
+111
| // Check if contract enforcement has already been applied to this binary | ||
| if(goto_model.symbol_table.has_symbol("__dfcc_instrumented_functions")) | ||
| { | ||
| throw invalid_input_exceptiont( | ||
| "Contract enforcement has already been applied to this binary.\n" | ||
| "Only one contract may be enforced at a time."); | ||
| } |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8754 +/- ##
===========================================
- Coverage 80.41% 80.41% -0.01%
===========================================
Files 1703 1703
Lines 188398 188406 +8
Branches 73 73
===========================================
+ Hits 151498 151501 +3
- Misses 36900 36905 +5 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
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