-
Notifications
You must be signed in to change notification settings - Fork 256
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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 | 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 theallocated
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.
reads
clauses are no longer allowed. It was a bug that these were allowed before. This is checked by the resolver.requires
andreads
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./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./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 ingit-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:
ASTVisitor.VisitTopLevelFrameExpression
.requiredVirtues
parameter toComprehensionExpr.GetBest
, since it was always passed in as0
.FrameExpression
, capture user-supplied frame expressions into.OriginalExpression
, add.DesugaredExpression
to hold any possible frame-expression rewrite (in particular, functions inreads
clauses get desugared during resolution, and this desugaring is stored in.DesugaredExpression
), and let.E
return the "better" of these two fields.FrameArrowToObjectSet
method fromArrowType
toBoundsDiscoveryVisitor
.AstVisitor
Context
type parameter in the implementation ofBoundsDiscoveryVisitor
.AstVisitor
Context
type parameter in the implementation ofTypeInferenceChecker
. This makes it clearer what parts of the context are important to type-inference checking..Bounds
for various quantifiers/comprehensions/forall-statements that are generated automatically. (These are needed, because/allocated:4
expects.Bounds
to 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:4
and 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.