WIP: Incremental symbolic execution with eager solving #7178
Conversation
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
Collaborator
tautschnig
commented
Sep 30, 2022
tautschnig
commented
- Each commit message has a non-empty body, explaining why the change was made.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- White-space or formatting changes outside the feature-related changed lines are in commits of their own.
Using the new option --eager-solving, runs symbolic execution only up until an assertion is encountered and then queries the solver. Continues doing so until symbolic execution is complete.
NEXT STEPS - debug eager_multi_path_symex_checker CEX - solve in background using pool of solvers (worklist?) Overall goal: reducing the overhead when checking multiple properties in parallel. High-level idea: each time an assertion is encountered during symbolic execution, create a new thread to process this assertion (which is part of a property); the parent thread will continue doing symbolic execution. Expected savings: all the steps up to (and including) symbolic execution will be done no more often than when doing all-properties-at-once. The following development tasks need to be completed: 1) Make the solver available to symbolic execution (via a parameter or via a call-back). 2) Generate local copies or overlays of the equation system to annotate these with slicing information. 3) Maintain a map that not only maps expressions to literals, but also makes available the entire formula behind these literals. 4) Run solvers in separate threads, collect their results. 5) Produce output once all results have been obtained. 6) Make output available as soon as possible. This requires to clearly communicate that a property may be revisited (for example, via further loop unwindings) and may change its status from "SUCCESS" to "FAILURE." Ensure output is written by a single thread or under some global lock.
Incremental symbolic execution requires post-processing in each step, and not just after the first one.
Codecov ReportBase: 77.82% // Head: 77.76% // Decreases project coverage by
Additional details and impacted files@@ Coverage Diff @@
## develop #7178 +/- ##
===========================================
- Coverage 77.82% 77.76% -0.07%
===========================================
Files 1578 1581 +3
Lines 182209 182377 +168
===========================================
+ Hits 141805 141826 +21
- Misses 40404 40551 +147
Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here. ☔ View full report at Codecov. |
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.