SyGuS, match concrete size array #1178
Merged
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
This also reverts the test output changes from commit 23cc439, as the option which caused the change is no longer enabled by default.
RyanGlScott
added a commit
to GaloisInc/saw-script
that referenced
this pull request
Mar 1, 2024
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
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.
kquick
approved these changes
May 14, 2024
RyanGlScott
added a commit
to GaloisInc/saw-script
that referenced
this pull request
May 15, 2024
* 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>
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 is a consolidation of the changes in #1074 and #1166. This also bumps the
what4submodule to bring in the changes from GaloisInc/what4#256.