From 472f3de939e7b5d652a0d7b478a3edc1fec17a99 Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 18 Jan 2013 17:54:04 -0800 Subject: Some additional resolution checks for co stuff. Beefed up some test cases. --- Source/Dafny/Printer.cs | 2 +- Source/Dafny/Resolver.cs | 31 ++++++++++++-- Source/Dafny/SccGraph.cs | 2 +- Test/dafny0/Answer | 39 +++++++++++------- Test/dafny0/CoPrefix.dfy | 7 ++-- Test/dafny0/CoResolution.dfy | 96 +++++++++++++++++++++++++++++--------------- 6 files changed, 121 insertions(+), 56 deletions(-) diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 9394ef40..cff105bd 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -298,7 +298,7 @@ namespace Microsoft.Dafny { public void PrintFunction(Function f, int indent) { Contract.Requires(f != null); - var isPredicate = f is Predicate; + var isPredicate = f is Predicate || f is PrefixPredicate; Indent(indent); string k = isPredicate ? "predicate" : f is CoPredicate ? "copredicate" : "function"; if (f.IsStatic) { k = "static " + k; } diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 8a11e6a6..b8fc0aed 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -660,6 +660,8 @@ namespace Microsoft.Dafny new Specification(new List() { new IdentifierExpr(cop.tok, k.Name) }, null), cop.Body, null, cop); extraMember = cop.PrefixPredicate; + // In the call graph, add an edge from P# to P, since this will have the desired effect of detecting unwanted cycles. + moduleDef.CallGraph.AddEdge(cop.PrefixPredicate, cop); } else { var com = (CoMethod)m; // _k has already been added to 'formals', so append the original formals @@ -679,6 +681,8 @@ namespace Microsoft.Dafny new Specification(decr, null), com.Body, null, com); extraMember = com.PrefixMethod; + // In the call graph, add an edge from M# to M, since this will have the desired effect of detecting unwanted cycles. + moduleDef.CallGraph.AddEdge(com.PrefixMethod, com); } members.Add(extraName, extraMember); } @@ -1414,6 +1418,15 @@ namespace Microsoft.Dafny foreach (var member in ((ClassDecl)d).Members) { if (member is CoPredicate) { var fn = (CoPredicate)member; + // Check here for the presence of any 'ensures' clauses, which are not allowed (because we're not sure + // of their soundness) + if (fn.Ens.Count != 0) { + Error(fn.Ens[0].tok, "a copredicate is not allowed to declare any ensures clause"); + } + // Also check for 'reads' clauses + if (fn.Reads.Count != 0) { + Error(fn.Reads[0].tok, "a copredicate is not allowed to declare any reads clause"); // (why?) + } if (fn.Body != null) { CoPredicateChecks(fn.Body, fn, CallingPosition.Positive); } @@ -1621,7 +1634,14 @@ namespace Microsoft.Dafny if (!(e.Function is CoPredicate)) { Error(e, "a recursive call from a copredicate can go only to other copredicates"); } else if (cp != CallingPosition.Positive) { - Error(e, "a recursive copredicate call can only be done in positive positions"); + var msg = "a recursive copredicate call can only be done in positive positions"; + if (cp == CallingPosition.Neither) { + // this may be inside a + msg += " and cannot sit inside an existential quantifier"; + } else { + // the co-call is not inside an existential quantifier, so don't bother mentioning the part of existentials in the error message + } + Error(e, msg); } else { e.CoCall = FunctionCallExpr.CoCallResolution.Yes; } @@ -1665,6 +1685,11 @@ namespace Microsoft.Dafny return; } else if (expr is QuantifierExpr) { var e = (QuantifierExpr)expr; + if ((cp == CallingPosition.Positive && e is ExistsExpr) || (cp == CallingPosition.Negative && e is ForallExpr)) { + // Don't allow any co-recursive calls under an existential, because that can be unsound. + // (Actually, I think we could be more liberal here--we could allow this if the range is finite.) + cp = CallingPosition.Neither; + } if (e.Range != null) { CoPredicateChecks(e.Range, context, e is ExistsExpr ? Invert(cp) : cp); } @@ -1679,7 +1704,7 @@ namespace Microsoft.Dafny Contract.Requires(context != null); if (stmt is CallStmt) { var s = (CallStmt)stmt; - if (s.Method is CoMethod) { + if (s.Method is CoMethod || s.Method is PrefixMethod) { // all is cool } else { // the call goes from a comethod context to a non-comethod callee @@ -1687,7 +1712,7 @@ namespace Microsoft.Dafny var moduleCallee = s.Method.EnclosingClass.Module; if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(s.Method)) { // we're looking at a recursive call (to a non-comethod) - Error(s, "a recursive call from a comethod can go only to other comethods"); + Error(s, "a recursive call from a comethod can go only to other comethods and prefix methods"); } } } else { diff --git a/Source/Dafny/SccGraph.cs b/Source/Dafny/SccGraph.cs index 4ae1c185..01a72fc5 100644 --- a/Source/Dafny/SccGraph.cs +++ b/Source/Dafny/SccGraph.cs @@ -108,7 +108,7 @@ namespace Microsoft.Dafny { } /// - /// Idempotently adds verices 'from' and 'to' the graph, and then + /// Idempotently adds vertices 'from' and 'to' the graph, and then /// adds an edge from 'from' to 'to'. /// public void AddEdge(Node from, Node to) { diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 34fa3232..a8e2ba1c 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1308,8 +1308,8 @@ Coinductive.dfy(35,11): Error: because of cyclic dependencies among constructor Coinductive.dfy(61,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed Coinductive.dfy(90,8): Error: a recursive copredicate call can only be done in positive positions Coinductive.dfy(91,8): Error: a recursive copredicate call can only be done in positive positions -Coinductive.dfy(92,8): Error: a recursive copredicate call can only be done in positive positions -Coinductive.dfy(92,21): Error: a recursive copredicate call can only be done in positive positions +Coinductive.dfy(92,8): Error: a recursive copredicate call can only be done in positive positions and cannot sit inside an existential quantifier +Coinductive.dfy(92,21): Error: a recursive copredicate call can only be done in positive positions and cannot sit inside an existential quantifier Coinductive.dfy(117,12): Error: only copredicates and equalities of codatatypes are allowed as conclusions of comethods Coinductive.dfy(126,19): Error: only copredicates and equalities of codatatypes are allowed as conclusions of comethods Coinductive.dfy(128,35): Error: only copredicates and equalities of codatatypes are allowed as conclusions of comethods @@ -1327,35 +1327,44 @@ Execution trace: Dafny program verifier finished with 5 verified, 2 errors -------------------- CoResolution.dfy -------------------- -CoResolution.dfy(43,8): Error: == can only be applied to expressions of types that support equality (got Stream<_T0>) -CoResolution.dfy(54,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -CoResolution.dfy(22,7): Error: member Undeclared# does not exist in class _default -CoResolution.dfy(23,2): Error: unresolved identifier: Undeclared# -CoResolution.dfy(26,5): Error: unresolved identifier: _k -5 resolution/type errors detected in CoResolution.dfy +CoResolution.dfy(14,9): Error: member Undeclared# does not exist in class _default +CoResolution.dfy(15,4): Error: unresolved identifier: Undeclared# +CoResolution.dfy(18,7): Error: unresolved identifier: _k +CoResolution.dfy(36,8): Error: == can only be applied to expressions of types that support equality (got Stream<_T0>) +CoResolution.dfy(47,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +CoResolution.dfy(64,10): Error: a copredicate is not allowed to declare any reads clause +CoResolution.dfy(70,31): Error: a copredicate is not allowed to declare any ensures clause +CoResolution.dfy(79,20): Error: a recursive call from a copredicate can go only to other copredicates +CoResolution.dfy(83,20): Error: a recursive call from a copredicate can go only to other copredicates +CoResolution.dfy(92,4): Error: a recursive call from a comethod can go only to other comethods and prefix methods +10 resolution/type errors detected in CoResolution.dfy -------------------- CoPrefix.dfy -------------------- -CoPrefix.dfy(61,7): Error: failure to decrease termination measure +CoPrefix.dfy(60,7): Error: failure to decrease termination measure Execution trace: (0,0): anon0 (0,0): anon5_Else (0,0): anon6_Then -CoPrefix.dfy(74,7): Error: cannot prove termination; try supplying a decreases clause +CoPrefix.dfy(73,7): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 (0,0): anon5_Else (0,0): anon6_Then -CoPrefix.dfy(112,1): Error BP5003: A postcondition might not hold on this return path. -CoPrefix.dfy(111,11): Related location: This is the postcondition that might not hold. -CoPrefix.dfy(99,17): Related location: Related location +CoPrefix.dfy(111,1): Error BP5003: A postcondition might not hold on this return path. +CoPrefix.dfy(110,11): Related location: This is the postcondition that might not hold. +CoPrefix.dfy(98,17): Related location: Related location Execution trace: (0,0): anon0 -CoPrefix.dfy(136,25): Error: assertion violation +CoPrefix.dfy(135,25): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon7_Then +CoPrefix.dfy(139,25): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon9_Then -Dafny program verifier finished with 23 verified, 4 errors +Dafny program verifier finished with 23 verified, 5 errors -------------------- CoinductiveProofs.dfy -------------------- CoinductiveProofs.dfy(26,12): Error: assertion violation diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy index d3d804e2..8cbe5394 100644 --- a/Test/dafny0/CoPrefix.dfy +++ b/Test/dafny0/CoPrefix.dfy @@ -44,7 +44,6 @@ ghost method Theorem0_Manual() parallel (k: nat) { Theorem0_Lemma(k); } - assume (forall k: nat :: atmost#[k](zeros(), ones())) ==> atmost(zeros(), ones()); } datatype Natural = Zero | Succ(Natural); @@ -135,11 +134,11 @@ comethod Compare(h: T) case true => assert FF(h).tail == GG(h).tail; // error: full equality is not known here case true => -// assert FF(h).tail == GG(h).tail; + assert FF(h) ==#[_k] GG(h); // yes, this is the postcondition to be proved, and it is known to hold case true => -// assert FF(h).tail ==#[_k] GG(h).tail; + assert FF(h).tail ==#[_k] GG(h).tail; // error: only _k-1 equality of the tails is known here case true => -// assert FF(h).tail ==#[_k - 1] GG(h).tail; + assert FF(h).tail ==#[_k - 1] GG(h).tail; // yes, follows from call to Compare case true => } } diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy index 3146147e..1b1923c3 100644 --- a/Test/dafny0/CoResolution.dfy +++ b/Test/dafny0/CoResolution.dfy @@ -1,38 +1,31 @@ -copredicate P(b: bool) -{ - !b && Q(null) -} - -copredicate Q(a: array) -{ - a == null && P(true) -} - -//copredicate A() { B() } -//predicate B() { A() } // error: SCC of a copredicate must include only copredicates +module TestModule { + copredicate P(b: bool) + { + !b && Q(null) + } -copredicate D() - reads this; // error: copredicates are not allowed to have a reads clause -- WHY NOT? -{ - true -} + copredicate Q(a: array) + { + a == null && P(true) + } -copredicate S(d: set) -{ - this.Undeclared#[5](d) && // error: 'Undeclared#' is undeclared - Undeclared#[5](d) && // error: 'Undeclared#' is undeclared - this.S#[5](d) && - S#[5](d) && - S#[_k](d) // error: _k is not an identifier in scope -} + copredicate S(d: set) + { + this.Undeclared#[5](d) && // error: 'Undeclared#' is undeclared + Undeclared#[5](d) && // error: 'Undeclared#' is undeclared + this.S#[5](d) && + S#[5](d) && + S#[_k](d) // error: _k is not an identifier in scope + } -comethod CM(d: set) -{ - var b; - b := this.S#[5](d); - b := S#[5](d); - this.CM#[5](d); - CM#[5](d); + comethod CM(d: set) + { + var b; + b := this.S#[5](d); + b := S#[5](d); + this.CM#[5](d); + CM#[5](d); + } } module GhostCheck0 { @@ -65,3 +58,42 @@ module GhostCheck2 { } } } + +module Mojul0 { + copredicate D() + reads this; // error: copredicates are not allowed to have a reads clause -- WHY NOT? + { + true + } + + copredicate NoEnsuresPlease(m: nat) + ensures NoEnsuresPlease(m) ==> m < 100; // error: a copredicate is not allowed to have an 'ensures' clause + { + m < 75 + } + + // Note, 'decreases' clauses are also disallowed on copredicates, but the parser takes care of that +} + +module Mojul1 { + copredicate A() { B() } // error: SCC of a copredicate must include only copredicates + predicate B() { A() } + + copredicate X() { Y() } + copredicate Y() { X#[10]() } // error: X is not allowed to depend on X# + + comethod M() + { + N(); + } + comethod N() + { + Z(); + W(); // error: not allowed to make co-recursive call to non-comethod + } + ghost method Z() { } + ghost method W() { M(); } + + comethod G() { H(); } + comethod H() { G#[10](); } // fine for comethod/prefix-method +} -- cgit v1.2.3