Path sat fix #873
Merged
Path sat fix #873
Conversation
This file contains 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
robdockins
force-pushed
the
path-sat-fix
branch
from
596c489 to
8029801
Compare
andreistefanescu
approved these changes
Oct 22, 2020
src/SAWScript/Crucible/LLVM/X86.hs
Outdated
| @@ -277,7 +277,7 @@ crucible_llvm_verify_x86 bic opts (Some (llvmModule :: LLVMModule x)) path nm gl | |||
| ] | |||
|
|
|||
| liftIO $ printOutLn opts Info "Examining specification to determine preconditions" | |||
| methodSpec <- buildMethodSpec bic opts llvmModule nm (show addr) setup | |||
| methodSpec <- buildMethodSpec bic opts {- TODO! checkSat -} llvmModule nm (show addr) setup | |||
There was a problem hiding this comment.
_checkSat is in scope
There was a problem hiding this comment.
True, but the code otherwise ignores it, and the haddocks explicitly claim it isn't used. I don't know offhand if there is a deep reason path satisfiability was never hooked up for the X86 verification methods, or if it is only that we never got to it.
There was a problem hiding this comment.
let's hook it up, there isn't a reason not to use it
src/SAWScript/Crucible/LLVM/X86.hs
Outdated
| @@ -427,7 +427,7 @@ buildMethodSpec :: | |||
| LLVMCrucibleSetupM () -> | |||
| TopLevel (MS.CrucibleMethodSpecIR LLVM) | |||
| buildMethodSpec bic opts lm nm loc setup = | |||
| setupLLVMCrucibleContext bic opts lm $ \cc -> do | |||
| setupLLVMCrucibleContext bic opts False {- TODO! checkSat -} lm $ \cc -> do | |||
There was a problem hiding this comment.
False is ok, the context is used only to initialize the method spec
This was referenced Oct 23, 2020
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.
Fixes the path satisfiability feature of
crucible_llvm_verify.Previously, the backend integration code was not properly maintaining the state of the external solver when updating its internal bookeeping datastructures regarding path conditions. As a result, satisfiability checks were only considering the immediate condition being branched on, and not previous path conditions.