Improve /allocate for Dafny 4.0 #3600
Milestone
Comments
Merged
jtristan
added a commit
that referenced
this issue
Feb 23, 2023
Fixes #3606 Fixes #3607 Under the now-fixed `/allocated:4`, also fixes #19 and #3605. This PR discovered a necessary change in the standard library: dafny-lang/libraries#99 (which has been merged) Also, this PR is what's referred to in #3600. This PR fixes several previous problems with quantifications and comprehensions over reference types. For example, previously, the verifier encoded `set o: object | true` as the set of _all_ objects, both allocated and unallocated, which is wrong in spirit and also allowed for unsound verification. The PR makes several general fixes and some fixes under just `/allocated:4` (which is not yet the default). We should make `/allocated:4` the default and remove the possibility for users to choose how allocation state is encoded (that is, we should remove the `allocated` flag altogether). However, it seems best to get this PR into Dafny version 3.Last, then make `/allocated:4` the default in Dafny 4.0 (and probably deprecate the `/allocated` flag at that time, too), and later remove the `/allocated` switch. The general changes in this PR include three breaking changes and one change that may affect verification. * One breaking change is that some functions used in `reads` clauses are no longer allowed. It was a bug that these were allowed before. This is checked by the resolver. * Another breaking change is that lambda expressions, including the `requires` and `reads` clauses of lambda expressions, are no longer allowed to depend on the allocation state. The previous omission of this check was a bug. This is checked by the resolver. * The third breaking change is that the verifier now include allocation antecedents for bound variables whose allocation isn't already implied by the body of the quantifier/comprehension. This is a virtue of (the buggy design of) `/allocated:3` and is fixed in `/allocated:4`. (Historically, this problem was not known at the time `/allocated:3` was designed. The intended design of `/allocated:4` does not have the problem, but the implementation of `/allocated:4` was previously incomplete and buggy.) So, switching from the default `/allocated:3` to `/allocated:4` (which will soon be the new default) changes (fixes!) the encoding of these allocation antecedents, which may be a breaking change for programs that (intentionally or inadvertently) made use of the previous, buggy encoding. * The possible change to verification is that this PR generalizes one axiom. Logically, adding an axiom does not make any verifying program not verify. However, as with any change in the verifier, in cases where verification was previously unstable, the presence of this new axiom may change verification behavior (e.g., change in verification performance or verification outcome). This axiom is added for both `/allocated:3` and `/allocated:4`. Unfortunately, there were no tests for `/allocated:4`, so no wonder it didn't work. Fortunately, this PR fixes `/allocated:4`. Unfortunately, the PR adds only a scant amount of specific `/allocated:4` tests. Fortunately, I did run the entire test suite locally with `/allocated:4` and it passes. So, the lack of many `/allocated:4` tests will be remedied as soon as we switch to `/allocated:4` as the default (in a separate PR). The long-standing issue #19 is fixed with this PR. Actually, the original program reported in #19 has been fixed for a while, but the long discussion of #19 showed many more issues. With `/allocated:4`, all of those have been fixed (and all of them are recorded in tests in `git-issue-19[ab].dfy`). ## More details The rewrite of functions in `reads` clauses was previously done in more than place. Now, this happens as a desugaring that's part of the resolver's bounds-discovery phase. Here are descriptions of the changes in the PR, listed more or less in the order that github shows the changes: * (code improvement) Add `ASTVisitor.VisitTopLevelFrameExpression`. * (code improvement) Remove `requiredVirtues` parameter to `ComprehensionExpr.GetBest`, since it was always passed in as `0`. * In `FrameExpression`, capture user-supplied frame expressions into `.OriginalExpression`, add `.DesugaredExpression` to hold any possible frame-expression rewrite (in particular, functions in `reads` clauses get desugared during resolution, and this desugaring is stored in `.DesugaredExpression`), and let `.E` return the "better" of these two fields. * (code improvement) Move `FrameArrowToObjectSet` method from `ArrowType` to `BoundsDiscoveryVisitor`. * (code improvement) Specialized the `AstVisitor` `Context` type parameter in the implementation of `BoundsDiscoveryVisitor`. * (code improvement) Specialized the `AstVisitor` `Context` type parameter in the implementation of `TypeInferenceChecker`. This makes it clearer what parts of the context are important to type-inference checking. * (fix) Fill in `.Bounds` for various quantifiers/comprehensions/forall-statements that are generated automatically. (These are needed, because `/allocated:4` expects `.Bounds` to be set.) * Previously, each datatype constructor gave rise to an allocation axiom, roughly `forall x, xs :: IsAlloc(x) && IsAlloc(xs) ==> IsAlloc(Cons(x, xs))`. Now, if no constructor depends on the allocation state, the entire type gets one allocation axiom, rather than having a separate one for each constructor (roughly `forall c: Color :: IsAlloc(c)`). This makes the axiom more useful where there isn't already a case split for each constructor. * (fix) The previous translation of `allocated(_)` made it sometimes not provable. (This has to do with boxing and has now been fixed.) * (fix) There was a code path for generating an allocation-consequence axiom for functions. However, it was broken in many places. Apparently, this was not detected, because the axiom is generated only for `/allocated:4` and there were no tests for `/allocated:4`. This PR fixes the code. * Make some error messages more specific. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: John Tristan <[email protected]>
|
Main PR merged and task to switch the default tracked under #2548 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Placeholder based on a conversation with @RustanLeino about improvements he has already implemented and may be deliverable for Dafny 4.0.
The text was updated successfully, but these errors were encountered: