Use Boogie's "argument" encoding for polymorphism #4210
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
atomb
force-pushed
the
arg-encoding
branch
2 times, most recently
from
80b1fb4
to
cc1e5bf
Compare
atomb
added a commit
that referenced
this pull request
Jul 3, 2023
…ings in Boogie (anticipating #4210) (#4229) This PR updates counterexample parsing so that it works with different polymorphism encodings, anticipating #4210. Here is a list of changes that were necessary to support the new type encoding: 1) Create a wrapper around Boogie's `Model.Func` that ignores type arguments, making counterexample extraction independent from the type encoding. 2) For the same purpose, remove all references to `type` function, which Boogie only emits when using the `Predicates` type encoding. 3) Update all counterexample and test generation tests to run twice, once under each encoding. 4) Remove several bugs and sources of nondeterminism in tests that surface after these changes (including having to do with the choice between reporting a nullable or a non-nullable type, a base type vs subset type, sorting counterexamples by position in the program, etc.). Add corresponding tests and fix existing ones. 5) Remove DatatypeType class that was used by counterexample code to distinguish between class types and datatype types but which is no longer necessary given how test generation works. Propagate this change to test generation. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --------- Co-authored-by: Aleksandr Fedchin <[email protected]> Co-authored-by: Aaron Tomb <[email protected]>
This changes the default. The previously-default `Predicates` mode is still available with the `/typeEncoding:p` flag.
This again fails to prove one assertion it failed to prove with Z3 4.8.5, and some errors are reordered.
Account for reordering and different counterexamples.
This reverts commit 7f65b45.
MikaelMayer
reviewed
Jul 20, 2023
| @@ -1,6 +1,7 @@ | |||
| Fuel.dfy(129,8): Error: Fuel can only increase within a given scope. | |||
| Fuel.dfy(407,8): Error: Fuel can only increase within a given scope. | |||
| Fuel.dfy(17,22): Error: assertion might not hold | |||
| Fuel.dfy(65,27): Error: assertion might not hold | |||
There was a problem hiding this comment.
Looks like you fixed a test here, nice.
There was a problem hiding this comment.
This one disappeared during the Z3 upgrade and has now reappeared. It seems very sensitive to SMT encoding details.
MikaelMayer
approved these changes
Jul 21, 2023
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 generally has better performance than the previously-default "predicate" encoding, though a few tests need to be updated to pass with this encoding.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.