Refactor entry point validation towards symex-callers#8782
Open
tautschnig wants to merge 1 commit intodiffblue:developfrom
Open
Refactor entry point validation towards symex-callers#8782tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig wants to merge 1 commit intodiffblue:developfrom
Conversation
e119656 to
c0d7491
Compare
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #8782 +/- ##
===========================================
- Coverage 80.02% 80.01% -0.01%
===========================================
Files 1700 1700
Lines 188345 188354 +9
Branches 73 73
===========================================
- Hits 150716 150711 -5
- Misses 37629 37643 +14 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
c0d7491 to
7f3aa29
Compare
There was a problem hiding this comment.
Pull request overview
This PR refactors entry point validation by moving the check for the existence of an entry point function from deep inside goto_symext::initialize_entry_point_state() to the caller sites. Previously, a std::out_of_range exception was caught and re-thrown as an unsupported_operation_exceptiont; now callers validate the entry point exists before invoking symex, and the function documents this as a precondition.
Changes:
- Removed the try/catch block in
initialize_entry_point_state()and added a precondition comment, changing the variable from a pointer to a reference. - Added entry point existence validation in four caller sites (
multi_path_symex_only_checker,single_path_symex_only_checker,single_loop_incremental_symex_checker, and their respective methods). - Extended
lazy_goto_functions_mapt::can_produce_function()to also check the symbol table for functions with code type and non-nil value.
Reviewed changes
Copilot reviewed 6 out of 6 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
src/goto-symex/symex_main.cpp |
Removed try/catch, changed pointer to reference, added precondition documentation |
src/goto-symex/goto_symex.h |
Added \pre documentation for entry point existence requirement |
src/goto-checker/single_path_symex_only_checker.cpp |
Added entry point validation before calling symex |
src/goto-checker/single_loop_incremental_symex_checker.cpp |
Added entry point validation before calling symex |
src/goto-checker/multi_path_symex_only_checker.cpp |
Added entry point validation before calling symex |
jbmc/src/java_bytecode/lazy_goto_functions_map.h |
Extended can_produce_function to also check symbol table |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
We can detect the absence of an entry point much earlier and do not need to perform unnecessary work before inevitably failing. This also fixes a bug where `can_produce_function` did not accurately reflect what functions could be produced. Fixes: diffblue#1847 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
7f3aa29 to
5b8c6ac
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.
We can detect the absence of an entry point much earlier and do not need to perform unnecessary work before inevitably failing.
Fixes: #1847