-
Notifications
You must be signed in to change notification settings - Fork 261
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
feat: Introduce :older attribute #1936
Conversation
Note that some tests are commented out, awaiting dafny-lang#1935 to be merged.
These `:older` attributes on `ReachableVia` will once again allow the `SchorrWaite*.dfy` tests, as soon as dafny-lang#1936 is merged.
Do I understand correctly that using
instead of
Or is that not possible because Heap and IsAlloc are not accessible in user space? Would it be an option to make those accessible in certain circumstances? And if How often do we expect Also would it be possible to implement this change are purely an extension to the Dafny compiler, with all the code being in a separate file? Given that it's adding an attribute that seems like it should not be a problem. I think that having the code not be intertwined with the existing code would lower the cost of having it by a lot. |
+1 to @keyboardDrummer's questions - I get the motivation of being able to ensure a pure expression does not depend on future allocations, but I'm definitely not convinced this feature is the best way to deliver that functionality. |
Would it also be possible to use reads clauses to indicate this? Something like:
|
Here are two cryptic answers to questions brought up above:
To understand the situation better, let me write down the motivation. (please stand by) |
MotivationLet me lead up to the motivation, starting with some background information about memory safety, references, quantifiers, and functions. Quantifications implicitly quantify over allocated stateDafny is a memory-safe programming language. Consequently, every object reference is either This property should carry over to comprehensions and quantifications as well. (Everything I'll say about quantifications applies to comprehensions in general; for example, set comprehensions. But I'll just say "quantifications" to stay more focused.) So, in Dafny, if forall c: C :: ... quantifies over all references to allocated What I said applies not just to object types, but to any type that contains a reference. For example, given datatype List<T> = Nil | Cons(T, List<T>) the type forall cs: List<C> :: ... quantifies over all lists whose every Functions are not allowed to depend on the allocation stateConsider the following attempted program: class Cell {
const data: int
constructor (x: int) {
this.data := x;
}
}
function P() {
forall cell: Cell :: c.data == 10 // Dafny does not allow this quantifier in a function
}
method M() returns (c: Cell)
requires P()
ensures P()
{
c := new Cell(8);
} It would be bad if this program would verify, because If a function were allowed to depend on the allocation state (like the attempted Instead, Dafny bans quantification over any reference-containing type in function bodies. Thus, Dafny rejects the program above. The check is enforced syntactically by the resolver--even before the program gets to the verifier. Allowing some quantifications over reference-containing typesThere are cases where Dafny's ban of quantifications over reference-containing types (henceforth called The Ban) is too strict. For example, suppose you want to define a predicate that says a given relation is transitive. You might write: predicate Transitive<X>(R: (X, X) -> bool) {
forall x, y, z :: R(x, y) && R(y, z) ==> R(x, z) // Dafny does not allow this quantifier in a function
} Alas, The Ban forbids the predicate, since it may be that type predicate Transitive<X(!new)>(R: (X, X) -> bool) {
forall x, y, z :: R(x, y) && R(y, z) ==> R(x, z) // since X is declared with (!new), the quantification is allowed
} Allowing more quantificationsDafny's syntactic check that enforces The Ban is not quite as strict as I've described it. It allows quantifications if the bound variables are limited to things that are allocated already. For example, you are allowed to write predicate Transitive<X>(R: (X, X) -> bool, universe: set<X>) {
forall x, y, z ::
x in universe && y in universe && z in universe ==>
R(x, y) && R(y, z) ==> R(x, z)
} (note the absence of var b0 := Transitive(R, U);
var c := new Cell(8);
var b1 := Transitive(R, U);
assert b0 == b1; Stated differently, User-declared "older" relationsHere is a simple, typical quantification that is allowed in a function: predicate AllZeros(S: set<Cell>) {
forall c :: c in S ==> c.data == 0
} As I mentioned above, the syntactic scan performed by the enforcement of The Ban detects the expression But what if you wanted to write the expression predicate AllZeros(S: set<Cell>) {
forall c :: InMySet(c, S) ==> c.data == 0
}
predicate InMySet(c: Cell, S: set<Cell>) {
c in S
} This is not allowed, because the syntactic check performed by The Ban doesn't trace through the call to This PR introduces an attribute that lets The Ban understand user-defined predicates as ones that ensure something about "older". The idea is that you declare predicate {:older c} InMySet(c: Cell, S: set<Cell>) {
c in S
} which expresses that
This PR introduces the Note that this design lets The Ban remain a syntactic check (it looks for the Why bother?Predicate class Node {
var children: seq<Node>
}
datatype Path<T> = Empty | Extend(Path, T)
predicate Reachable(source: Node, sink: Node, S: set<Node>)
reads S
{
exists via: Path<Node> :: ReachableVia(source, via, sink, S) // allowed because of {:older p} on ReachableVia
}
predicate {:older p} ReachableVia(source: Node, p: Path<Node>, sink: Node, S: set<Node>)
reads S
decreases p
{
match p
case Empty => source == sink
case Extend(prefix, n) => n in S && sink in n.children && ReachableVia(source, prefix, n, S)
} Since A final note: If this was a problem in |
Thanks for the great explanation. It helps a lot. That said though, I'm still not confident about any thoughts I have on this topic, but I'll share them anyways. Please bear with me.
Is that to make the proofs more tractable? What if quantifications also implicitly quantify over readable state? In your example, Or differently, shouldn't quantifier variables always be older than the parameters of the function containing the quantifier? Why do I still need to specify an older annotation? In your example, the
already causes references in Would it be possible to use an expression instead of an attribute for this, to make it more flexible? Like
Or
|
This is a fantastic detailed explanation on why we need Something isn't quite right though on your last example: |
No, it's part of story of claiming that the language is memory safe.
This is an intriguing idea, which I have not considered before. The "implicitly" part of the suggestion is rather subtle, since a function like predicate ContainsNothingButC(c: C, S: set<C>) {
forall x :: x in S ==> x == c
} would need to declare To make things less subtle, another variation of the idea would be to use the A different idea, which I have considered before, is introduce a specification that says the function can depend on the allocated state. (The syntax I have imagined for this is
Yes, I believe they should be. If the quantifier variables are older than the parameters, then the quantification does not depend on the allocation state. More precisely, I think the desired condition is that the quantifier variables are older than some parameter. But how do you encode this (into Boogie)? You'd have to arrange pass in the maximum allocation state (that is, the newest allocation time) of the parameters. For example, in var b0 := MyPredicate(x, y, z);
var c := new MyClass();
var b1 := MyPredicate(x, y, z); the two calls to
Indeed, this is why the proof obligation for
Such an The postcondition of |
Yikes! Let me think about this one. |
@MikaelMayer Thanks for your observation. I believe the semantic property is encoded correctly and the In a nutshell, previously, the error message implied that (when the predicate returns
I changed the error message to say you must prove that
|
Have you considered making |
Source/Dafny/Resolver.cs
Outdated
@@ -17338,6 +17401,30 @@ class DefaultValueSubstituter : Substituter { | |||
} | |||
continue; | |||
} | |||
if (conjunct is FunctionCallExpr fce) { |
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.
I don't like to ask this, but could you follow-up with moving all bounds-related code from Resolver.cs to a separate file?
Also, in this PR, could you put this new block of code in a separate method?
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.
Good idea. I moved all bounds-discovery code into a separate file, and also moved the FunctionCallExpr block into a separate method.
The fact that The enforcement of Another attribute that might be construed as on the border between syntax and semantics is An attribute that I think should be replaced by a keyword in the language is So, I still favor |
@RustanLeino Is the following a correct understanding of the origin of the problem? A function with a reads clause takes an implicit heap parameter. We want to restrict references that originate from quantifiers to those that are allocated in the implicitly passed in heap, to provide memory safety. However, we want the result of the function to only depend on its explicit parameters, so we have to restrict references originating from quantifiers further to a subset that's entirely determined by the explicit parameters. Given the above, wouldn't it be possible to always pass a modified version of the heap to functions, where the modified heap consists of only objects reachable from the function's explicit parameters? That way if the heap changes in ways unrelated to the function's explicit parameters, such as new objects being allocated, then the modified heap passed to the function does not change. One I don't understand is why functions that don't have a reads clause, so they don't take an implicit heap, still have restrictions on their quantifiers. For example:
gives the definition axiom:
there's still a "a forall expression involved in a predicate definition is not allowed to depend on the set of allocated references" error message. Is this an occurrence of The Ban being too strict? Also, in Boogie I don't see where the references from quantifiers are restricted to being allocated. Is that always done implicitly, in this case by the |
return; | ||
} | ||
|
||
// local worker function: |
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.
Isn't any nested function a local worker function?
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.
Yes, that's what the comment (redundantly) says.
Thanks for explanation. I regret that we're asking Dafny users to understand yet another concept, that of Is it really important to be able to draw values from the allocated heap, like you do in the motivating example? Can your motivating example not be replaced by:
? Regarding the syntax. You mention
Can the user not workaround that by making the callable static and the receiver explicit? If yes, then I'm not sure we need to solve this problem.
Why would you want it to be an attribute, instead of a modifier keyword on parameters?
One thing I'm missing in error messages on quantifiers is the suggestion to
Gives the error message:
How does the user find out they should use Regarding the documentation, for me the motivating example you provided:
to provide more clarity than just
Because the motivating example makes it clear why we can't add |
# Conflicts: # RELEASE_NOTES.md
Though the first draft of the reference manual was written by Richard Ford and the subsequent major revision of it was written by David Cok, the reference manual has since received contributions for many others. Moreover, in additional to a team-wide effort to fill in TODOs in the manual, we are now updating the reference manual when source change require such updates. Rather than trying to list every contributor, it seems appropriate to treat the reference manual as having the same authors as the general contributors to the source code.
Note, some of these tests are now performed by `Test/dafny0/ParseErrors.dfy`
And fix direction of error message for new/non-new
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.
Added some minor comments. I'm OOTO from the 26th PST time to the end of the week. If you want to make more changes, feel free to have someone else review just those. I'm approving the current ones.
} else { | ||
reporter.Error(MessageSource.Resolver, arg.tok, ":older attribute has duplicated argument: '{0}'", name); | ||
// parameters are not allowed to be marked 'older' | ||
foreach (var formal in f.Formals) { |
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.
Nitpick: consider using linq:
if (f.Formals.Any(formal => formal.IsOlder)) {
reporter.Error(MessageSource.Resolver, formal.tok, "only predicates and two-state predicates are allowed 'older' parameters");
}
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.
The code produces one error for each older
formal. This could be done with an .Iter(formal => { ... })
, but for that, I think the current foreach
is more readable.
} | ||
var formals = fce.Function.Formals; | ||
Contract.Assert(formals.Count == fce.Args.Count); | ||
for (var i = 0; i < formals.Count; i++) { |
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.
Nitpick: consider using LINQ
var olderBound = xs.Zip(ys).FirstOrDefault(t => t.First.IsOlder && t.Second.Resolved is IdentifierExpr ide && ide.Var == (IVariable)boundVariable);
if (olderBound != null) {
bounds.Add(new ComprehensionExpr.OlderBoundedPool());
}
Source/Dafny/Verifier/Translator.cs
Outdated
@@ -2180,14 +2179,19 @@ class Specialization { | |||
} | |||
} | |||
|
|||
Bpl.Expr OlderCondition(Function f, Bpl.Expr funcAppl, List<Bpl.Variable> inParams, ISet<string> olderParameters, Dictionary<IVariable, Expression> substMap) { | |||
int OlderCondition(Function f, Bpl.Expr funcAppl, List<Bpl.Variable> inParams, out Bpl.Expr olderCondition) { |
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.
Nitpick: C# also supports returning tuples with elegant syntax, which seems to be preferred over using out parameters (link), so you could also write:
(int olderParameterCount, Bpl.Expr olderCondition) OlderCondition(
Function f, Bpl.Expr funcAppl, List<Bpl.Variable> inParams) {
}
@@ -238,12 +238,12 @@ public class IsAllocated : ProofObligationDescription { | |||
|
|||
public class IsOlder : ProofObligationDescription { |
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.
Consider naming this IsOlderObligation
, so later on you can write IsOlderObligation
instead of PODesc.IsOlder
. The latter contains enough acronyms that I have to look up what it means.
docs/DafnyRef/Attributes.md
Outdated
@@ -462,6 +461,7 @@ BOUNDVARS = ID : ID | |||
| BOUNDVARS, BOUNDVARS | |||
``` | |||
|
|||
|
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.
Is this intentional?
@@ -2,7 +2,7 @@ | |||
<script src="https://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML" type="text/javascript"></script> | |||
|
|||
<font size="+4"><p style="text-align: center;">Dafny Reference Manual</p></font> <!-- PDFOMIT --> | |||
<p style="text-align: center;">K. Rustan M. Leino, Richard L. Ford, David R. Cok</p> <!-- PDFOMIT --> | |||
<p style="text-align: center;">The dafny-lang community</p> <!-- PDFOMIT --> |
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.
Congrats!
docs/DafnyRef/Types.md
Outdated
* This property is ensured by disallowing _open-ended_ quantifiers. | ||
More precisely, the object references that a quantifier may range | ||
over must be shown to be confined to object references that are | ||
already allocated. Quantifiers that are not open-ended are called |
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.
"already", what is the current time? I think it's not the time at which the predicate is called, because if I do two predicate calls with equivalent arguments, then the quantifier references must be allocated before the first call, even when evaluating the second call.
Shouldn't this say "More precisely, the object references that a quantifier may range
over must be shown to be confined to object references that were allocated before one of the parameters passed to the predicate." ?
# Conflicts: # RELEASE_NOTES.md
Source/Dafny/Resolver.cs
Outdated
reporter.Error(MessageSource.Resolver, attributeToken, "a :older attribute is allowed only on predicates and two-state predicates"); | ||
return; | ||
} else if (older.Args.Count == 0) { | ||
reporter.Error(MessageSource.Resolver, attributeToken, "a :older attribute expects as arguments one or more of the predicate's parameters"); |
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.
Add a return here maybe (for clarity?)
Source/Dafny/Resolver.cs
Outdated
if (!f.ResultType.IsBoolType || f is PrefixPredicate || f is ExtremePredicate) { | ||
reporter.Error(MessageSource.Resolver, attributeToken, "a :older attribute is allowed only on predicates and two-state predicates"); | ||
return; | ||
} else if (older.Args.Count == 0) { |
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.
No need for else
Source/Dafny/Resolver.cs
Outdated
foreach (var argument in older.Args) { | ||
var arg = argument.Resolved; | ||
string name; | ||
if (arg is ThisExpr) { |
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.
This whole if could be a case
Source/Dafny/Resolver.cs
Outdated
if (!givenFormals.Contains(name)) { | ||
givenFormals.Add(name); | ||
} else { | ||
reporter.Error(MessageSource.Resolver, arg.tok, ":older attribute has duplicated argument: '{0}'", name); | ||
} |
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.
Purely stylistic, but I would flip the condition and move the Add out of the if: `if (contains) { Error(); } Add
private string SuccessOlder => olderParameterCount == 1 ? " is" : "s are"; | ||
private string SuccessOther => otherParameterCount == 1 ? "the" : "any"; | ||
private string FailureOlder => olderParameterCount == 1 ? "the" : "an"; | ||
private string FailureOther => | ||
olderParameterCount == 1 && otherParameterCount == 1 ? "the other parameter" : | ||
otherParameterCount == 1 ? "the non-'older' parameter" : | ||
"all non-'older' parameters"; | ||
private string PluralOlderParameters => 2 <= olderParameterCount ? "s" : ""; |
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.
I would inline all these.
@@ -0,0 +1,15 @@ | |||
OlderVerification.dfy(89,12): Error: the 'older' parameter might be newer than all non-'older' parameters when the predicate returns 'true' |
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.
Maybe mention the name of the parameter? Parameter… is marked older but may be newer than all non-'older' parameters when predicate … returns 'true'
?
This PR introduces a new parameter modifier,
older
, which can be used with the parameters of a predicate to say that, if the predicate returnstrue
, then the parameters declared asolder
are necessarily equally old as or older than the other parameters.The updated reference manual contains a section that motivates and describes
older
. That's the text aimed at users. Here is a smaller--but not terribly motivated--example, along with an implementation-centric explanation:For a predicate
the
older
modifier claimsThat is, if the predicate returns
true
, then in any heap wherey
is allocated, then so isx
--- in short,x
is older thany
.The reason for wanting to declare a predicate with
older
parameters is so that the predicate can be used as a way to ensure a quantified expression does not depend on the allocation state. For example,Here is another example, using an
iset
comprehension:Dafny does not allow a function to depend on the allocation state; that is, the act of allocating more objects should not change the value of a function. But if
X
is a type that contains references, then, at first glance, it looks as if this function does depend on the allocation state. For instance, ifX
is a class type, then allocating moreX
objects gives more candidate values for theiset
comprehension to consider, and if thoseX
objects satisfy theP
constraint, then theiset
would become larger. By using theolder
modifier onP
's parameterx
, it becomes known that anyx
that satisfiesP(x, y)
in this comprehension is older thany
. Thus, theiset
comprehension, in fact, does not depend on the allocation state.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.