Concrete floats #89
Merged
Concrete floats #89
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
|
Will fix #5 when merged. |
|
@kquick, This isn't quite ready to merge yet, but I'm interested in your thoughts about the new kind of tests I've been working on (CF https://github.com/GaloisInc/what4/blob/concrete-floats/what4/test/TestTemplate.hs). Currently they're focused on the floating-point operations, but there's no particular reason the templates idea couldn't be extended to most or all of the main what4 interface. |
robdockins
force-pushed
the
concrete-floats
branch
from
6edf9e9
to
9b266a3
Compare
based on the `libBF` representation. Change the `GroundValue` type for floating point values to use `BigFloat`. Still TOOD: constant folding in the expression builder, ground evaluation, hashing and (maybe?) abstract domains.
produces a bunch of failures related to evaluating floating-point values, which indicate what work needs to be done in the ground evaluation module.
and test that expression constant folding agrees with ground evaluation.
…ator computes a value for an expression, the solver can prove the expression must have that value. This complements the previous solver test, which showed that the solver computes the same value in a computed satisfying model. This complementary test proves that the value we compute is the _only_ value this term may take on, which demonstrates that we are not computing any underspecified values.
This provides support for floating-point values that hide their precision at the type level, similar to how the `SWord` module hides the width of bitvectors.
robdockins
force-pushed
the
concrete-floats
branch
from
9b266a3
to
0de69f1
Compare
This was referenced Feb 4, 2021
Closed
Closed
robdockins
added a commit
to GaloisInc/saw-core
that referenced
this pull request
Feb 16, 2021
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.
Use the
libBFlibrary to implement concrete floating-point ground evaluation and constant folding.This is especially a tricky area to get right, so I've implemented a new testing technique using "expression templates." These are fragments of syntax containing variables at base types. We can enumerate an interesting collection of these templates and use them to generate test cases. For each test case, we will chose random concrete values for the variables and evaluate the syntax in a variety of ways and test that they agree. In particular, we can ask solvers to act as computational oracles and verify that our ground evaluation agrees with their theory.