Update crucible and macaw submodules, changes to x86 initial stack #1110
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
chameco
commented
Mar 4, 2021
src/SAWScript/Crucible/LLVM/X86.hs
Outdated
| @@ -235,11 +237,13 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se | |||
| opts <- getOptions | |||
| basic_ss <- getBasicSS | |||
| sym <- liftIO $ newSAWCoreBackend sc | |||
| rw <- getTopLevelRW | |||
| cacheTermsSetting <- liftIO $ W4.getOptionSetting W4.B.cacheTerms $ W4.getConfiguration sym | |||
| _ <- liftIO $ W4.setOpt cacheTermsSetting $ rwWhat4HashConsing rw | |||
There was a problem hiding this comment.
Makes enable_what4_hash_consing do the expected thing
chameco
commented
Mar 4, 2021
| @@ -304,7 +308,7 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se | |||
| pure | |||
| ( C.cfgHandle funcCFG | |||
| , st & C.stateContext . C.functionBindings | |||
| %~ C.insertHandleMap (C.cfgHandle funcCFG) (C.UseCFG funcCFG $ C.postdomInfo funcCFG) | |||
| %~ C.FnBindings . C.insertHandleMap (C.cfgHandle funcCFG) (C.UseCFG funcCFG $ C.postdomInfo funcCFG) . C.fnBindings | |||
There was a problem hiding this comment.
Update for GaloisInc/crucible@049000a
chameco
commented
Mar 4, 2021
| @@ -322,7 +326,7 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se | |||
| Macaw.macawExtensions (Macaw.x86_64MacawEvalFn sfs) mvar | |||
| (mkGlobalMap . Map.singleton 0 $ preState ^. x86GlobalBase) | |||
| funcLookup noExtraValidityPred | |||
| , C._functionBindings = C.insertHandleMap (C.cfgHandle cfg) (C.UseCFG cfg $ C.postdomInfo cfg) C.emptyHandleMap | |||
| , C._functionBindings = C.FnBindings $ C.insertHandleMap (C.cfgHandle cfg) (C.UseCFG cfg $ C.postdomInfo cfg) C.emptyHandleMap | |||
There was a problem hiding this comment.
Update for GaloisInc/crucible@049000a
chameco
commented
Mar 4, 2021
| insertHandleMap (cfgHandle cfg) (UseCFG cfg (postdomInfo cfg)) $ | ||
| emptyHandleMap | ||
| , _functionBindings = FnBindings $ | ||
| insertHandleMap (cfgHandle cfg) (UseCFG cfg (postdomInfo cfg)) emptyHandleMap |
There was a problem hiding this comment.
Update for GaloisInc/crucible@049000a
chameco
commented
Mar 4, 2021
| @@ -1082,7 +1082,7 @@ setupGlobals opts gs fs s | |||
| let halloc = simHandleAllocator (st ^. stateContext) | |||
| h <- mkHandle halloc fname | |||
| let addBinding = over (stateContext . functionBindings) | |||
| (insertHandleMap h (UseOverride o)) | |||
| (FnBindings . insertHandleMap h (UseOverride o) . fnBindings) | |||
There was a problem hiding this comment.
Update for GaloisInc/crucible@049000a
|
I think the problem with the
I'm going to add a distinct option for What4 hash consing during simulation and see if that works out. It's unfortunately quite ugly and cumbersome to pile up more options in |
andreistefanescu
approved these changes
Mar 10, 2021
chameco
added
the
PR: ready to merge
RyanGlScott
added
the
subsystem: x86
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.
(This PR bundles two somewhat-related changes for the next https://github.com/GaloisInc/blst-verification release, in the interest of expediency. GaloisInc/what4#105 is also relevant in that context, and I plan to bump that submodule here as well if there are no strong objections.)
The changes to x86 verification amount to increasing the alignment of the base of RSP while shrinking the alignment of the initial offset. The actual alignment of the initial RSP remains 16 bytes. This makes it more viable to verify code that performs bitwise operations on pointers derived from RSP (given GaloisInc/macaw#192).