Guard mux-pushing simplifications behind option #256
Conversation
This also reverts the test output changes from commit 23cc439, as the option which caused the change is no longer enabled by default.
This bumps: * The `crucible` submodule to bring in the changes from GaloisInc/crucible#1178 * The `what4` submodule to bring in the changes from GaloisInc/what4#256
There was a problem hiding this comment.
IIUC, this patch adds a config flag to control the push-down, and the push-down is originally added in a different patch that is also post 1.5.1. Thus, the default for most clients (unless they had updated to a commit of what4 lying within these two changes) is unchanged and the new behavior only occurs when the new config is set.
My concern here is clients like Macaw that use pattern-based recognition (especially for end-of-block dispatching) that might be broken by this push-down behavior. Unless you think this concern is unfounded, you might want to add this information to the PR description to help forensic efforts for any of this kind of downstream breakage folks might encounter.
Other than this concern and the help text, the other comments are just stylistic, so I'm approving and you are free to choose what changes you'd like to make or not make before merging.
| | otherwise = do | ||
| Just LeqProof <- return $ testLeq (knownNat :: NatRepr 1) w | ||
| sbMakeExpr sym $ BVZext w x | ||
| pmo <- CFG.getOpt (sbPushMuxOps sym) |
There was a problem hiding this comment.
Quick check: looks like you had to do this in 6-8 other locations as well. Do you think it's reasonable to float this getOpt to the top before the primary case on expr so that the case pattern match branches can be largely as they were with just the pmo check? I'm fine either way (based on the assumption that getOpt is inexpensive), but just wanted to call this out for you to make a decision on.
There was a problem hiding this comment.
If I understand you correctly, you are suggesting to call getOpt at the beginning of each method's implementation to minimize the diff to the actual logic of the code itself? If so, I'm not sure that that would actually have the desired effect. In particular, each method of this IsExprBuilder instance is implemented using pattern guards, so in order to call getOpt before the pattern guards, we'd likely need to do something like this:
bvZext sym w x = do
pmo <- CFG.getOpt (sbPushMuxOps sym)
if | Just xv <- asBV x = do ...
| Just (BVZext _ y) <- asApp x = do ...
| ...But using MultiWayIf (or a similar refactoring) here would cause the diff to be just as large (if not larger) than it is currently. As such, I opted to localize the getOpt calls to the parts of the code that actually make use of the option.
There was a problem hiding this comment.
My concern here is clients like Macaw that use pattern-based recognition (especially for end-of-block dispatching) that might be broken by this push-down behavior. Unless you think this concern is unfounded, you might want to add this information to the PR description to help forensic efforts for any of this kind of downstream breakage folks might encounter.
To be clear, Macaw isn't yet making use of the new behavior, and by the time Macaw bumps its What4 submodule, the new behavior will be guarded behind an opt-in flag. As a result, Macaw's behavior won't change unless it specifically opts into the new behavior. (Indeed, this was the whole point of guarding this behavior behind a flag, as the new behavior proved problematic for certain use cases, such as in certain SAW proofs.)
| | otherwise = do | ||
| Just LeqProof <- return $ testLeq (knownNat :: NatRepr 1) w | ||
| sbMakeExpr sym $ BVZext w x | ||
| pmo <- CFG.getOpt (sbPushMuxOps sym) |
There was a problem hiding this comment.
If I understand you correctly, you are suggesting to call getOpt at the beginning of each method's implementation to minimize the diff to the actual logic of the code itself? If so, I'm not sure that that would actually have the desired effect. In particular, each method of this IsExprBuilder instance is implemented using pattern guards, so in order to call getOpt before the pattern guards, we'd likely need to do something like this:
bvZext sym w x = do
pmo <- CFG.getOpt (sbPushMuxOps sym)
if | Just xv <- asBV x = do ...
| Just (BVZext _ y) <- asApp x = do ...
| ...But using MultiWayIf (or a similar refactoring) here would cause the diff to be just as large (if not larger) than it is currently. As such, I opted to localize the getOpt calls to the parts of the code that actually make use of the option.
Exactly the situation I was hoping for. We probably discussed this back then but I subsequently forgot. Thanks for the confirmation. |
* Code refactoring. * Find SMT array write of a fixed size. * Cache tail traversal in findArrayStore. * Load SMT array with concrete size. * Load SMT array with 0 size. * Add cache for base pointers with array stores. * Add noSatisfyingWriteFreshConstant option. * wip * Cleanup. * Derive Show. * Add updateHandleMap. * Add parentWTOComponent. * Export writeSourceSize. * Add runCHC and helpers. * Bump what4. * wip * Fix build error with GHC 8.10 * Bump what4 submodule to incorporate GaloisInc/what4#256 This also reverts the test output changes from commit 23cc439, as the option which caused the change is no longer enabled by default. * Fix build warnings introduced in #1165 * crucible: Clearer error messages for runCHC * Additional documentation * Comment out putStrLns * Remove redundant export * More accurate logReason * Remove redundant import * Don't log everything to foo.* files * Pass pointer size to writeSouceSize * Replace putStrLn's with ?logMessage's * Fix build warnings * Rename SimpleLoopFixpoint to SimpleLoopFixpointCHC SimpleLoopFixpointCHC is not quite suitable for being a full replacement for SimpleLoopFixpoint as of yet. For now, we will offer the CHC functionality in a separate module, and we will restore the old SimpleLoopFixpoint functionality in a subsequent commit. * Restore previous SimpleLoopFixpoint functionality * Fix -Wunused-do-bind warning * Bump what4 to bring in latest changes from GaloisInc/what4#256 * Remove commented-out exports * Review comments --------- Co-authored-by: Andrei Stefanescu <andrei@stefanescu.io>
* Find SMT array write of a fixed size. * Load SMT array with concrete size. * Add test. * Add noSatisfyingWriteFreshConstant option. * Add invariant substitution to getPoststateObligations. * Bump what4. * wip * wip * Use simplified term in resolveSAWPred. * Bump crucible. * Remove unused sc. * Use simplified term in resolveSAWPred. * Bump crucible. * Update src/SAWScript/Crucible/LLVM/Builtins.hs Co-authored-by: Ryan Scott <rscott@galois.com> * Fix -Wunused-matches warning * Bump crucible, what4 submodules This bumps: * The `crucible` submodule to bring in the changes from GaloisInc/crucible#1178 * The `what4` submodule to bring in the changes from GaloisInc/what4#256 * Remove debugging-only code * Bump cryptol-specs to incorporate GaloisInc/cryptol-specs#72 * Repair AES example to work with `type Nk = AES256` * Add expert options for enabling What4-, Crucible-related SyGuS features * Split off separate llvm_verify_fixpoint_chc_x86 command * Only enable doPtrCmp optimizations with SimpleFixpointCHC * crucible: Revert popFrame refactoring * Uniformly apply pushMuxOps option to all ExprBuilders SAW creates a variety of different ExprBuilders in the course of a typical SAW script, but we were only applying the pushMuxOps option to some of them. This patch makes the treatment a bit more comprehensive. Unfortunately, doing so requires a rather uncomfortable amount of extra plumbing in `SAWScript.Proof`, but I'm not sure how to do better without refactoring all of `SAWScript.Proof` to use `TopLevel` instead of `IO` (and it's unclear if that is desirable). * Bump cryptol-specs, what4, crucible submodules to latest * Bump what4, crucible submodules * Adapt to recent crucible-llvm API changes --------- Co-authored-by: Andrei Stefanescu <andrei@stefanescu.io>
Add
pushMuxOpsandpushMuxOpsOption. If this option is enabled, What4 will push certainExprBuilderoperations (e.g.,zext) down to the branches ofiteexpressions. In some (but not all) circumstances, this can result in operations that are easier for SMT solvers to reason about.