Fixed some checking of recursive method/copredicate calls

4 files changed, 53 insertions, 6 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 2262c4da..0dbf7a27 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2141,6 +2141,11 @@ namespace Microsoft.Dafny
           }

           Visit(e.LogicalBody(), cp);

           return false;

+        } else if (expr is StmtExpr) {

+          var e = (StmtExpr)expr;

+          Visit(e.E, cp);

+          Visit(e.S, CallingPosition.Neither);

+          return false;

         } else if (expr is ConcreteSyntaxExpression) {

           // do the sub-parts with the same "cp"

           return true;

@@ -2149,6 +2154,22 @@ namespace Microsoft.Dafny
         cp = CallingPosition.Neither;

         return true;

       }

+

+      protected override bool VisitOneStmt(Statement stmt, ref CallingPosition st) {

+        if (stmt is CallStmt) {

+          var s = (CallStmt)stmt;

+          var moduleCaller = context.EnclosingClass.Module;

+          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

+            Error(stmt.Tok, "a recursive call from a copredicate can go only to other copredicates");

+          }

+          // do the sub-parts with the same "cp"

+          return true;

+        } else {

+          return base.VisitOneStmt(stmt, ref st);

+        }

+      }

     }

 

     void CoPredicateChecks(Expression expr, CoPredicate context, CallingPosition cp) {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index f56af482..78d6c126 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1350,7 +1350,8 @@ Coinductive.dfy(103,17): Error: a copredicate can be called recursively only in
 Coinductive.dfy(113,24): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

 Coinductive.dfy(119,15): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

 Coinductive.dfy(120,10): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

-15 resolution/type errors detected in Coinductive.dfy

+Coinductive.dfy(145,5): Error: a recursive call from a copredicate can go only to other copredicates

+16 resolution/type errors detected in Coinductive.dfy

 

 -------------------- Corecursion.dfy --------------------

 Corecursion.dfy(15,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without side effects can be called co-recursively)

@@ -1395,11 +1396,15 @@ CoResolution.dfy(83,20): Error: a recursive call from a copredicate can go only
 CoResolution.dfy(92,4): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

 CoResolution.dfy(106,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

 CoResolution.dfy(107,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

+CoResolution.dfy(112,17): Error: a recursive call from a copredicate can go only to other copredicates

+CoResolution.dfy(118,17): Error: a recursive call from a copredicate can go only to other copredicates

 CoResolution.dfy(126,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

 CoResolution.dfy(127,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

+CoResolution.dfy(132,17): Error: a recursive call from a copredicate can go only to other copredicates

+CoResolution.dfy(138,17): Error: a recursive call from a copredicate can go only to other copredicates

 CoResolution.dfy(146,4): Error: a recursive call from a copredicate can go only to other copredicates

 CoResolution.dfy(148,4): Error: a recursive call from a copredicate can go only to other copredicates

-16 resolution/type errors detected in CoResolution.dfy

+20 resolution/type errors detected in CoResolution.dfy

 

 -------------------- CoPrefix.dfy --------------------

 CoPrefix.dfy(161,3): Error BP5003: A postcondition might not hold on this return path.

diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy
index a7111a09..bf224f25 100644
--- a/Test/dafny0/CoResolution.dfy
+++ b/Test/dafny0/CoResolution.dfy
@@ -109,13 +109,13 @@ module CallGraph {
 

   copredicate Q(n: nat)

   {

-    calc { 87; { CoLemma(n); } }

+    calc { 87; { CoLemma(n); } }  // error: this recursive call not allowed

     false

   }

 

   copredicate R(n: nat)

   {

-    calc { 87; { CoLemma#[n](n); } }

+    calc { 87; { CoLemma#[n](n); } }  // error: this recursive call not allowed

     false

   }

 

@@ -129,13 +129,13 @@ module CallGraph {
 

   copredicate Q_D(n: nat)

   {

-    calc { 88; { CoLemma_D(n); } }

+    calc { 88; { CoLemma_D(n); } }  // error: this recursive call not allowed

     false

   }

 

   copredicate R_D(n: nat)

   {

-    calc { 89; { CoLemma_D#[n](n); } }

+    calc { 89; { CoLemma_D#[n](n); } }  // error: this recursive call not allowed

     false

   }

 

diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy
index 27b279c3..d6466f73 100644
--- a/Test/dafny0/Coinductive.dfy
+++ b/Test/dafny0/Coinductive.dfy
@@ -129,6 +129,27 @@ module CoPredicateResolutionErrors {
     ensures Even(Doubles(n));

   {

   }

+

+  copredicate CoStmtExpr_Good(s: Stream<int>)

+  {

+    s.head > 0 && (MyLemma(s.head); CoStmtExpr_Good(s.tail))

+  }

+

+  lemma MyLemma(x: int)

+  {

+  }

+

+  copredicate CoStmtExpr_Bad(s: Stream<int>)

+  {

+    s.head > 0 &&

+    (MyRecursiveLemma(s.head);  // error: cannot call method recursively from copredicate

+     CoStmtExpr_Bad(s.tail))

+  }

+

+  lemma MyRecursiveLemma(x: int)

+  {

+    var p := CoStmtExpr_Bad(Upward(x));

+  }

 }

 

 // --------------------------------------------------