Some additional resolution checks for co stuff.

Beefed up some test cases.

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<Expression>(new List<Expression>() { 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<Expression>(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 {
     }

 

     /// <summary>

-    /// 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'.

     /// </summary>

     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<T>(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<int>)

-{

-  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<int>)

+  {

+    a == null && P(true)

+  }

 

-copredicate S(d: set<int>)

-{

-  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<int>)

+  {

+    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<int>)

-{

-  var b;

-  b := this.S#[5](d);

-  b := S#[5](d);

-  this.CM#[5](d);

-  CM#[5](d);

+  comethod CM(d: set<int>)

+  {

+    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

+}