Changes #1165
Merged
Changes #1165
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
RyanGlScott
reviewed
Jan 19, 2024
There was a problem hiding this comment.
Per the CI, one crux-llvm test case's golden output needs to be updated to account for simplification changes made in GaloisInc/what4#252:
float-cast2.ll
solver=z3
loop-merging=loop
clang-range=pre-clang13
z3 4.8.14
float-cast2
float-cast2 crux run: OK (0.04s)
float-cast2 crux result: OK
float-cast2 crux output: FAIL
test/Test.hs:310:
MISMATCH for expected (test-data/golden/golden/float-cast2.z3.good)
and actual (test-data/golden/golden/float-cast2.z3.z3.out) output:
F-expect>|bvZext 32 (ite (floatIsNaN cX@3:f) 0x0:[1] 0x1:[1])
F-actual>|ite (floatIsNaN cX@3:f) 0x0:[32] 0x1:[32]
F |[Crux] Overall status: Valid.
Comment on lines
+644
to
+646
| -- log to stdout | ||
| let logData = defaultLogData | ||
| { logCallbackVerbose = \_ -> putStrLn |
There was a problem hiding this comment.
Do we really want to always log things to stdout? I would expect the user to have to specify this manually if they want a higher-than-normal log setting.
There was a problem hiding this comment.
copy-pasta
| -- log to stdout | ||
| let logData = defaultLogData | ||
| { logCallbackVerbose = \_ -> putStrLn | ||
| , logReason = "SAW inv" |
There was a problem hiding this comment.
This code lives in Crucible, not SAW... shouldn't the logReason mention Crucible instead?
Comment on lines
+630
to
+632
| -- | Run the CHC solver on the current proof obligations, and return the | ||
| -- solution as a substitution from the uninterpreted functions to their | ||
| -- definitions. |
There was a problem hiding this comment.
It might be worth mentioning the use of the BV<->LIA transformation somewhere in the Haddocks, since this part wasn't obvious to me until I read the source code carefully.
RyanGlScott
added a commit
that referenced
this pull request
Mar 1, 2024
RyanGlScott
added a commit
that referenced
this pull request
May 14, 2024
* 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>
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.
No description provided.