Fix allocated 4 #3609
Fix allocated 4 #3609
Conversation
chore: Improve code
…c axiom for the entire type, rather than generating one $IsAlloc axiom per constructor.
# Conflicts: # Source/DafnyCore/AST/Types/ArrowType.cs # Source/DafnyCore/Resolver/InferDecreasesClause.cs # Source/DafnyCore/Rewriters/ForallStmtRewriter.cs # Source/DafnyCore/Verifier/Translator.DataTypes.cs # Source/DafnyCore/Verifier/Translator.cs
Fixes dafny-lang#3605 with /allocated:4 Fixes dafny-lang#3606 Fixes dafny-lang#3607
|
Is it now the case that a function (can be used in a reads clause) if and only if ((it is of type ->) or (it is of type -->)) ? |
|
Is it now the case that a reads function is (of type ->) or (or type -->)? |
There was a problem hiding this comment.
Summary. A long-standing issue with Dafny's logic is that universal quantification over objects was defined so that it bounded both allocated and unallocated objects, allowing to state properties of objects before they even exist. This problem had been addressed with a more careful translation and the fix was available through the non-default flag /allocated:4. We plan on making /allocated:4 the default (and only) interpretation of universal quantification over objects in Dafny 4 and this PR is preparing for that change. To that end, this PR addresses a few issues with the current implementation of /allocated:4. In particular, it restricts which functions can be used or defined as reads clauses. This fixes must also be applied to implicit forms of quantification, such as set comprehension. The bulk of the modifications consist in tracking the set of bound objects explicitly. The PR also include a change to the translation of datatypes so that the generated allocation axioms are not defined recursively for pure datatypes.
| var mayInvolveReferences = UserDefinedType.FromTopLevelDecl(dt.tok, dt).MayInvolveReferences; | ||
| var constructorFunctions = dt.Ctors.ToDictionary(ctor => ctor, ctor => AddDataTypeConstructor(dt, ctor, mayInvolveReferences)); | ||
| if (!mayInvolveReferences) { | ||
| AddCommonIsAllocConstructorAxiom(dt); |
There was a problem hiding this comment.
Why does this work? Consider the value Cons(3,Cons(4,Nil)). Does it work because if Cons(3,Cons(4,Nil)) is allocated, then we can easily deduct that Cons(4,Nil) is as well? Or is it because it is always good enough to know that Cons(3,Cons(4,Nil)) is allocated?
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 | trueas 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:4the default and remove the possibility for users to choose how allocation state is encoded (that is, we should remove theallocatedflag altogether). However, it seems best to get this PR into Dafny version 3.Last, then make/allocated:4the default in Dafny 4.0 (and probably deprecate the/allocatedflag at that time, too), and later remove the/allocatedswitch.The general changes in this PR include three breaking changes and one change that may affect verification.
readsclauses are no longer allowed. It was a bug that these were allowed before. This is checked by the resolver.requiresandreadsclauses 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./allocated:3and is fixed in/allocated:4. (Historically, this problem was not known at the time/allocated:3was designed. The intended design of/allocated:4does not have the problem, but the implementation of/allocated:4was previously incomplete and buggy.) So, switching from the default/allocated:3to/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./allocated:3and/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:4tests. Fortunately, I did run the entire test suite locally with/allocated:4and it passes. So, the lack of many/allocated:4tests will be remedied as soon as we switch to/allocated:4as 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 ingit-issue-19[ab].dfy).More details
The rewrite of functions in
readsclauses 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:
ASTVisitor.VisitTopLevelFrameExpression.requiredVirtuesparameter toComprehensionExpr.GetBest, since it was always passed in as0.FrameExpression, capture user-supplied frame expressions into.OriginalExpression, add.DesugaredExpressionto hold any possible frame-expression rewrite (in particular, functions inreadsclauses get desugared during resolution, and this desugaring is stored in.DesugaredExpression), and let.Ereturn the "better" of these two fields.FrameArrowToObjectSetmethod fromArrowTypetoBoundsDiscoveryVisitor.AstVisitorContexttype parameter in the implementation ofBoundsDiscoveryVisitor.AstVisitorContexttype parameter in the implementation ofTypeInferenceChecker. This makes it clearer what parts of the context are important to type-inference checking..Boundsfor various quantifiers/comprehensions/forall-statements that are generated automatically. (These are needed, because/allocated:4expects.Boundsto be set.)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 (roughlyforall c: Color :: IsAlloc(c)). This makes the axiom more useful where there isn't already a case split for each constructor.allocated(_)made it sometimes not provable. (This has to do with boxing and has now been fixed.)/allocated:4and there were no tests for/allocated:4. This PR fixes the code.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.