diff options
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 3 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 107 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 3 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 10 | ||||
| -rw-r--r-- | Test/dafny0/Corecursion.dfy | 45 |
5 files changed, 131 insertions, 37 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 0aac1cd6..b58f392c 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -3933,7 +3933,8 @@ namespace Microsoft.Dafny { NoBecauseFunctionHasSideEffects,
NoBecauseFunctionHasPostcondition,
NoBecauseRecursiveCallsAreNotAllowedInThisContext,
- NoBecauseIsNotGuarded
+ NoBecauseIsNotGuarded,
+ NoBecauseRecursiveCallsInDestructiveContext
}
public CoCallResolution CoCall = CoCallResolution.No; // indicates whether or not the call is a co-recursive call; filled in by resolution
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 9fe4b3e2..8b28ade5 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1277,10 +1277,25 @@ namespace Microsoft.Dafny break;
}
}
+ var coCandidates = new List<CoCallResolution.CoCallInfo>();
+ var hasIntraClusterCallsInDestructiveContexts = false;
foreach (var m in module.CallGraph.GetSCC(fn)) {
var f = (Function)m;
var checker = new CoCallResolution(f, dealsWithCodatatypes);
checker.CheckCoCalls(f.Body);
+ coCandidates.AddRange(checker.FinalCandidates);
+ hasIntraClusterCallsInDestructiveContexts |= checker.HasIntraClusterCallsInDestructiveContexts;
+ }
+ if (coCandidates.Count != 0) {
+ if (hasIntraClusterCallsInDestructiveContexts) {
+ foreach (var c in coCandidates) {
+ c.CandidateCall.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseRecursiveCallsInDestructiveContext;
+ }
+ } else {
+ foreach (var c in coCandidates) {
+ c.EnclosingCoConstructor.IsCoCall = true;
+ }
+ }
}
}
}
@@ -2806,8 +2821,12 @@ namespace Microsoft.Dafny // Add out-parameters to a new scope that will also include the outermost-level locals of the body
// Don't care about any duplication errors among the out-parameters, since they have already been reported
scope.PushMarker();
- foreach (Formal p in m.Outs) {
- scope.Push(p.Name, p);
+ if (m is CoMethod && m.Outs.Count != 0) {
+ Error(m.Outs[0].tok, "comethods are not allowed to have out-parameters");
+ } else {
+ foreach (Formal p in m.Outs) {
+ scope.Push(p.Name, p);
+ }
}
// ... continue resolving specification
@@ -7351,6 +7370,8 @@ namespace Microsoft.Dafny readonly ModuleDefinition currentModule;
readonly Function currentFunction;
readonly bool dealsWithCodatatypes;
+ public bool HasIntraClusterCallsInDestructiveContexts = false;
+ public readonly List<CoCallInfo> FinalCandidates = new List<CoCallInfo>();
public CoCallResolution(Function currentFunction, bool dealsWithCodatatypes) {
Contract.Requires(currentFunction != null);
@@ -7362,15 +7383,16 @@ namespace Microsoft.Dafny /// <summary>
/// Determines which calls in "expr" can be considered to be co-calls, which co-constructor
/// invocations host such co-calls, and which destructor operations are not allowed.
+ /// Also records whether or not there are any intra-cluster calls in a destructive context.
/// Assumes "expr" to have been successfully resolved.
/// </summary>
public void CheckCoCalls(Expression expr) {
Contract.Requires(expr != null);
- var candidates = CheckCoCalls(expr, true, null);
+ var candidates = CheckCoCalls(expr, 0, true, null);
ProcessCoCallInfo(candidates);
}
- struct CoCallInfo
+ public struct CoCallInfo
{
public int GuardCount;
public FunctionCallExpr CandidateCall;
@@ -7389,6 +7411,8 @@ namespace Microsoft.Dafny }
}
+ const int InfiniteDestruction = 1000000000; // assume co-constructor and co-destructor calls are never nested deeper than 1 billion levels
+
/// <summary>
/// Recursively goes through the entire "expr". Every call within the same recursive cluster is a potential
/// co-call. All such calls will get their .CoCall field filled in, indicating whether or not the call
@@ -7399,7 +7423,7 @@ namespace Microsoft.Dafny /// controlling the uses of "expr" (for example, if the enclosing context passes "expr" to a function or binds
/// "expr" to a variable).
/// </summary>
- List<CoCallInfo> CheckCoCalls(Expression expr, bool allowCallsWithinRecursiveCluster, DatatypeValue coContext) {
+ List<CoCallInfo> CheckCoCalls(Expression expr, int destructionLevel, bool allowCallsWithinRecursiveCluster, DatatypeValue coContext) {
Contract.Requires(expr != null);
Contract.Ensures(allowCallsWithinRecursiveCluster || Contract.Result<List<CoCallInfo>>().Count == 0);
@@ -7409,7 +7433,7 @@ namespace Microsoft.Dafny var e = (DatatypeValue)expr;
if (e.Ctor.EnclosingDatatype is CoDatatypeDecl) {
foreach (var arg in e.Arguments) {
- foreach (var c in CheckCoCalls(arg, allowCallsWithinRecursiveCluster, e)) {
+ foreach (var c in CheckCoCalls(arg, destructionLevel - 1, allowCallsWithinRecursiveCluster, e)) {
c.AdjustGuardCount(1);
candidates.Add(c);
}
@@ -7419,7 +7443,7 @@ namespace Microsoft.Dafny } else if (expr is FieldSelectExpr) {
var e = (FieldSelectExpr)expr;
if (e.Field.EnclosingClass is CoDatatypeDecl) {
- foreach (var c in CheckCoCalls(e.Obj, allowCallsWithinRecursiveCluster, null)) {
+ foreach (var c in CheckCoCalls(e.Obj, destructionLevel + 1, allowCallsWithinRecursiveCluster, null)) {
if (c.GuardCount <= 1) {
// This call was not guarded (c.GuardedCount == 0) or the guard for this candidate co-call is
// being removed (c.GuardedCount == 1), so this call is not allowed as a co-call.
@@ -7437,18 +7461,30 @@ namespace Microsoft.Dafny if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.EqCommon || e.ResolvedOp == BinaryExpr.ResolvedOpcode.NeqCommon) {
// Equality and disequality (for any type that may contain a co-datatype) are as destructive as can be--in essence,
// they destruct the values indefinitely--so don't allow any co-recursive calls in the operands.
- var r = CheckCoCalls(e.E0, false, null);
+ var r = CheckCoCalls(e.E0, InfiniteDestruction, false, null);
Contract.Assert(r.Count == 0); // follows from postcondition of CheckCoCalls, given that we pass in allowCallsWithinRecursiveCluster==false
- r = CheckCoCalls(e.E1, false, null);
+ r = CheckCoCalls(e.E1, InfiniteDestruction, false, null);
+ Contract.Assert(r.Count == 0); // follows from postcondition of CheckCoCalls, given that we pass in allowCallsWithinRecursiveCluster==false
+ return candidates;
+ }
+ } else if (expr is TernaryExpr) {
+ var e = (TernaryExpr)expr;
+ if (e.Op == TernaryExpr.Opcode.PrefixEqOp || e.Op == TernaryExpr.Opcode.PrefixNeqOp) {
+ // Prefix equality and disequality (for any type that may contain a co-datatype) are destructive.
+ var r = CheckCoCalls(e.E0, InfiniteDestruction, false, null);
+ Contract.Assert(r.Count == 0); // follows from postcondition of CheckCoCalls, given that we pass in allowCallsWithinRecursiveCluster==false
+ r = CheckCoCalls(e.E1, InfiniteDestruction, false, null);
+ Contract.Assert(r.Count == 0); // follows from postcondition of CheckCoCalls, given that we pass in allowCallsWithinRecursiveCluster==false
+ r = CheckCoCalls(e.E2, InfiniteDestruction, false, null);
Contract.Assert(r.Count == 0); // follows from postcondition of CheckCoCalls, given that we pass in allowCallsWithinRecursiveCluster==false
return candidates;
}
} else if (expr is MatchExpr) {
var e = (MatchExpr)expr;
- var r = CheckCoCalls(e.Source, false, null);
+ var r = CheckCoCalls(e.Source, InfiniteDestruction, false, null);
Contract.Assert(r.Count == 0); // follows from postcondition of CheckCoCalls
foreach (var kase in e.Cases) {
- r = CheckCoCalls(kase.Body, allowCallsWithinRecursiveCluster, null);
+ r = CheckCoCalls(kase.Body, destructionLevel, allowCallsWithinRecursiveCluster, null);
candidates.AddRange(r);
}
return candidates;
@@ -7458,13 +7494,30 @@ namespace Microsoft.Dafny // (Note, if functions could have a "destruction level" declaration that promised to only destruct its arguments by
// so much, then some recursive calls within the cluster could be allowed.)
foreach (var arg in e.Args) {
- var r = CheckCoCalls(arg, false, null);
+ var r = CheckCoCalls(arg, InfiniteDestruction, false, null);
Contract.Assert(r.Count == 0); // follows from postcondition of CheckCoCalls
}
// Second, investigate the possibility that this call itself may be a candidate co-call
if (currentModule.CallGraph.GetSCCRepresentative(currentFunction) == currentModule.CallGraph.GetSCCRepresentative(e.Function)) {
// This call goes to another function in the same recursive cluster
- if (e.Function.Reads.Count != 0) {
+ if (0 < destructionLevel) {
+ HasIntraClusterCallsInDestructiveContexts = true;
+ }
+ if (!allowCallsWithinRecursiveCluster) {
+ // a potentially destructive context
+ if (!dealsWithCodatatypes) {
+ e.CoCall = FunctionCallExpr.CoCallResolution.No;
+ } else {
+ e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseRecursiveCallsAreNotAllowedInThisContext;
+ }
+ } else if (coContext == null) {
+ // no immediately enclosing co-constructor
+ if (!dealsWithCodatatypes) {
+ e.CoCall = FunctionCallExpr.CoCallResolution.No;
+ } else {
+ e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded;
+ }
+ } else if (e.Function.Reads.Count != 0) {
// this call is disqualified from being a co-call, because of side effects
if (!dealsWithCodatatypes) {
e.CoCall = FunctionCallExpr.CoCallResolution.No;
@@ -7485,18 +7538,6 @@ namespace Microsoft.Dafny } else {
e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded;
}
- } else if (!allowCallsWithinRecursiveCluster) {
- if (!dealsWithCodatatypes) {
- e.CoCall = FunctionCallExpr.CoCallResolution.No;
- } else {
- e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseRecursiveCallsAreNotAllowedInThisContext;
- }
- } else if (coContext == null) {
- if (!dealsWithCodatatypes) {
- e.CoCall = FunctionCallExpr.CoCallResolution.No;
- } else {
- e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded;
- }
} else {
// e.CoCall is not filled in here, but will be filled in when the list of candidates are processed
candidates.Add(new CoCallInfo(0, e, coContext));
@@ -7506,19 +7547,19 @@ namespace Microsoft.Dafny } else if (expr is OldExpr) {
var e = (OldExpr)expr;
// here, "coContext" is passed along (the use of "old" says this must be ghost code, so the compiler does not need to handle this case)
- return CheckCoCalls(e.E, allowCallsWithinRecursiveCluster, coContext);
+ return CheckCoCalls(e.E, destructionLevel, allowCallsWithinRecursiveCluster, coContext);
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
foreach (var rhs in e.RHSs) {
- var r = CheckCoCalls(rhs, false, null);
+ var r = CheckCoCalls(rhs, InfiniteDestruction, false, null);
Contract.Assert(r.Count == 0); // follows from postcondition of CheckCoCalls
}
- return CheckCoCalls(e.Body, allowCallsWithinRecursiveCluster, null);
+ return CheckCoCalls(e.Body, destructionLevel, allowCallsWithinRecursiveCluster, null);
}
// Default handling:
foreach (var ee in expr.SubExpressions) {
- var r = CheckCoCalls(ee, allowCallsWithinRecursiveCluster, null);
+ var r = CheckCoCalls(ee, destructionLevel, allowCallsWithinRecursiveCluster, null);
candidates.AddRange(r);
}
if (expr.Type is BasicType) {
@@ -7529,15 +7570,11 @@ namespace Microsoft.Dafny return candidates;
}
- /// <summary>
- /// This method is to be called when it has been determined that all candidate
- /// co-calls in "info" are indeed allowed as co-calls.
- /// </summary>
void ProcessCoCallInfo(List<CoCallInfo> coCandidates) {
foreach (var c in coCandidates) {
if (c.GuardCount != 0) {
- c.CandidateCall.CoCall = FunctionCallExpr.CoCallResolution.Yes;
- c.EnclosingCoConstructor.IsCoCall = true;
+ FinalCandidates.Add(c);
+ c.CandidateCall.CoCall = FunctionCallExpr.CoCallResolution.Yes; // this tentative decision may be reverted if there are intra-cluster calls in destructive contexts
} else if (dealsWithCodatatypes) {
c.CandidateCall.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded;
} else {
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 46620fb0..356b36a7 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -3441,6 +3441,9 @@ namespace Microsoft.Dafny { case FunctionCallExpr.CoCallResolution.NoBecauseRecursiveCallsAreNotAllowedInThisContext:
hint = "note that calls cannot be co-recursive in this context";
break;
+ case FunctionCallExpr.CoCallResolution.NoBecauseRecursiveCallsInDestructiveContext:
+ hint = "note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts";
+ break;
case FunctionCallExpr.CoCallResolution.No:
hint = null;
break;
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index da6d1caa..38b7c120 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1157,8 +1157,16 @@ Execution trace: Corecursion.dfy(69,16): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context)
Execution trace:
(0,0): anon5_Else
+Corecursion.dfy(91,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)
+Execution trace:
+ (0,0): anon5_Else
+ (0,0): anon6_Then
+Corecursion.dfy(101,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)
+Execution trace:
+ (0,0): anon5_Else
+ (0,0): anon6_Then
-Dafny program verifier finished with 7 verified, 4 errors
+Dafny program verifier finished with 10 verified, 6 errors
-------------------- CoResolution.dfy --------------------
CoResolution.dfy(14,9): Error: member Undeclared# does not exist in class _default
diff --git a/Test/dafny0/Corecursion.dfy b/Test/dafny0/Corecursion.dfy index 5025dae9..3193db12 100644 --- a/Test/dafny0/Corecursion.dfy +++ b/Test/dafny0/Corecursion.dfy @@ -79,3 +79,48 @@ module EqualityIsSuperDestructive { assert false;
}
}
+
+// --------------------------------------------------
+
+module MixRecursiveAndCorecursive {
+ codatatype Stream<T> = Cons(head: T, tail: Stream)
+
+ function F(n: nat): Stream<int>
+ {
+ if n == 0 then
+ Cons(0, F(5)) // error: cannot prove termination -- by itself, this would look like a properly guarded co-recursive call...
+ else
+ F(n - 1).tail // but the fact that this recursive call is not tail recursive means that call in the 'then' branch is not
+ // allowed to be a co-recursive
+ }
+
+ // same thing but with some mutual recursion going on
+ function G(n: nat): Stream<int>
+ {
+ if n == 0 then
+ Cons(0, H(5)) // error: cannot prove termination
+ else
+ H(n)
+ }
+ function H(n: nat): Stream<int>
+ requires n != 0;
+ decreases n, 0;
+ {
+ G(n-1).tail
+ }
+
+ // but if all the recursive calls are tail recursive, then all is cool
+ function X(n: nat): Stream<int>
+ {
+ if n == 0 then
+ Cons(0, Y(5)) // error: cannot prove termination
+ else
+ Y(n)
+ }
+ function Y(n: nat): Stream<int>
+ requires n != 0;
+ decreases n, 0;
+ {
+ X(n-1)
+ }
+}
|