Refactored code for dealing with SCCs in the call graph.

Fixed bug.

7 files changed, 165 insertions, 100 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 452c71e4..97e88e3d 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -681,7 +681,7 @@ namespace Microsoft.Dafny
           var call = (CallStmt)s.ResolvedStatements[0];

           var moduleCaller = context.EnclosingClass.Module;

           var moduleCallee = call.Method.EnclosingClass.Module;

-          if (call.Method is CoLemma && moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(call.Method)) {

+          if (call.Method is CoLemma && ModuleDefinition.InSameSCC(context, call.Method)) {

             // we're looking at a recursive call to a colemma

             var args = new List<Expression>();

             args.Add(k);

@@ -700,9 +700,7 @@ namespace Microsoft.Dafny
       } else if (stmt is CallStmt) {

         var s = (CallStmt)stmt;

         if (s.Method is CoLemma) {

-          var moduleCaller = context.EnclosingClass.Module;

-          var moduleCallee = s.Method.EnclosingClass.Module;

-          if (s.Method is CoLemma && moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(s.Method)) {

+          if (s.Method is CoLemma && ModuleDefinition.InSameSCC(context, s.Method)) {

             // we're looking at a recursive call to a colemma

             var args = new List<Expression>();

             args.Add(k);

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index eee1b06f..a8c3f56d 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1105,6 +1105,41 @@ namespace Microsoft.Dafny {
       }

     }

 

+    /// <summary>

+    /// Determines if "a" and "b" are in the same strongly connected component of the call graph, that is,

+    /// if "a" and "b" are mutually recursive.

+    /// Assumes that CallGraph has already been filled in for the modules containing "a" and "b".

+    /// </summary>

+    public static bool InSameSCC(ICallable a, ICallable b) {

+      Contract.Requires(a != null);

+      Contract.Requires(b != null);

+      var module = a.EnclosingModule;

+      return module == b.EnclosingModule && module.CallGraph.GetSCCRepresentative(a) == module.CallGraph.GetSCCRepresentative(b);

+    }

+

+    /// <summary>

+    /// Return the representative elements of the SCCs that contain contain any member declaration in a

+    /// class in "declarations".

+    /// Note, the representative element may in some cases be a Method, not necessarily a Function.

+    /// </summary>

+    public static IEnumerable<ICallable> AllFunctionSCCs(List<TopLevelDecl> declarations) {

+      var set = new HashSet<ICallable>();

+      foreach (var d in declarations) {

+        var cl = d as ClassDecl;

+        if (cl != null) {

+          var module = cl.Module;

+          foreach (var member in cl.Members) {

+            var fn = member as Function;

+            if (fn != null) {

+              var repr = module.CallGraph.GetSCCRepresentative(fn);

+              set.Add(repr);

+            }

+          }

+        }

+      }

+      return set;

+    }

+

     public static IEnumerable<Function> AllFunctions(List<TopLevelDecl> declarations) {

       foreach (var d in declarations) {

         var cl = d as ClassDecl;

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 57527202..ccbd9a29 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1469,39 +1469,40 @@ namespace Microsoft.Dafny
 

       if (ErrorCount == prevErrorCount) {  // because CheckCoCalls requires the given expression to have been successfully resolved

         // Perform the guardedness check on co-datatypes

-        foreach (var fn in ModuleDefinition.AllFunctions(declarations)) {

-          var module = fn.EnclosingClass.Module;

-          if (fn.Body != null && module.CallGraph.GetSCCRepresentative(fn) == fn) {

-            bool dealsWithCodatatypes = false;

-            foreach (var m in module.CallGraph.GetSCC(fn)) {

-              var f = m as Function;

-              if (f != null && f.ResultType.InvolvesCoDatatype) {

-                dealsWithCodatatypes = true;

-                break;

-              }

+        foreach (var repr in ModuleDefinition.AllFunctionSCCs(declarations)) {

+          var module = repr.EnclosingModule;

+          bool dealsWithCodatatypes = false;

+          foreach (var m in module.CallGraph.GetSCC(repr)) {

+            var f = m as Function;

+            if (f != null && f.ResultType.InvolvesCoDatatype) {

+              dealsWithCodatatypes = true;

+              break;

             }

-            var coCandidates = new List<CoCallResolution.CoCallInfo>();

-            var hasIntraClusterCallsInDestructiveContexts = false;

-            foreach (var m in module.CallGraph.GetSCC(fn)) {

-              var f = m as Function;

-              if (f != null && f.Body != null) {

-                var checker = new CoCallResolution(f, dealsWithCodatatypes);

-                checker.CheckCoCalls(f.Body);

-                coCandidates.AddRange(checker.FinalCandidates);

-                hasIntraClusterCallsInDestructiveContexts |= checker.HasIntraClusterCallsInDestructiveContexts;

+          }

+          var coCandidates = new List<CoCallResolution.CoCallInfo>();

+          var hasIntraClusterCallsInDestructiveContexts = false;

+          foreach (var m in module.CallGraph.GetSCC(repr)) {

+            var f = m as Function;

+            if (f != null && f.Body != null) {

+              var checker = new CoCallResolution(f, dealsWithCodatatypes);

+              checker.CheckCoCalls(f.Body);

+              coCandidates.AddRange(checker.FinalCandidates);

+              hasIntraClusterCallsInDestructiveContexts |= checker.HasIntraClusterCallsInDestructiveContexts;

+            } else if (f == null) {

+              // the SCC contains a method, which we always consider to be a destructive context

+              hasIntraClusterCallsInDestructiveContexts = true;

+            }

+          }

+          if (coCandidates.Count != 0) {

+            if (hasIntraClusterCallsInDestructiveContexts) {

+              foreach (var c in coCandidates) {

+                c.CandidateCall.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseRecursiveCallsInDestructiveContext;

               }

-            }

-            if (coCandidates.Count != 0) {

-              if (hasIntraClusterCallsInDestructiveContexts) {

-                foreach (var c in coCandidates) {

-                  c.CandidateCall.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseRecursiveCallsInDestructiveContext;

-                }

-              } else {

-                foreach (var c in coCandidates) {

-                  c.CandidateCall.CoCall = FunctionCallExpr.CoCallResolution.Yes;

-                  c.EnclosingCoConstructor.IsCoCall = true;

-                  ReportAdditionalInformation(c.CandidateCall.tok, "co-recursive call", c.CandidateCall.Name.Length);

-                }

+            } else {

+              foreach (var c in coCandidates) {

+                c.CandidateCall.CoCall = FunctionCallExpr.CoCallResolution.Yes;

+                c.EnclosingCoConstructor.IsCoCall = true;

+                ReportAdditionalInformation(c.CandidateCall.tok, "co-recursive call", c.CandidateCall.Name.Length);

               }

             }

           }

@@ -2070,9 +2071,7 @@ namespace Microsoft.Dafny
       protected override bool VisitOneExpr(Expression expr, ref CallingPosition cp) {

         if (expr is FunctionCallExpr) {

           var e = (FunctionCallExpr)expr;

-          var moduleCaller = context.EnclosingClass.Module;

-          var moduleCallee = e.Function.EnclosingClass.Module;

-          if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(e.Function)) {

+          if (ModuleDefinition.InSameSCC(context, e.Function)) {

             // we're looking at a recursive call

             if (!(e.Function is CoPredicate)) {

               Error(e, "a recursive call from a copredicate can go only to other copredicates");

@@ -2158,9 +2157,7 @@ namespace Microsoft.Dafny
       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)) {

+          if (ModuleDefinition.InSameSCC(context, s.Method)) {

             // we're looking at a recursive call

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

           }

@@ -2200,9 +2197,7 @@ namespace Microsoft.Dafny
             // all is cool

           } else {

             // the call goes from a colemma context to a non-colemma callee

-            var moduleCaller = context.EnclosingClass.Module;

-            var moduleCallee = s.Method.EnclosingClass.Module;

-            if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(s.Method)) {

+            if (ModuleDefinition.InSameSCC(context, s.Method)) {

               // we're looking at a recursive call (to a non-colemma)

               Error(s.Tok, "a recursive call from a colemma can go only to other colemmas and prefix lemmas");

             }

@@ -2214,9 +2209,7 @@ namespace Microsoft.Dafny
         if (expr is FunctionCallExpr) {

           var e = (FunctionCallExpr)expr;

           // the call goes from a colemma context to a non-colemma callee

-          var moduleCaller = context.EnclosingClass.Module;

-          var moduleCallee = e.Function.EnclosingClass.Module;

-          if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(e.Function)) {

+          if (ModuleDefinition.InSameSCC(context, e.Function)) {

             // we're looking at a recursive call (to a non-colemma)

             Error(e.tok, "a recursive call from a colemma can go only to other colemmas and prefix lemmas");

           }

@@ -7815,7 +7808,6 @@ namespace Microsoft.Dafny
 

   class CoCallResolution

   {

-    readonly ModuleDefinition currentModule;

     readonly Function currentFunction;

     readonly bool dealsWithCodatatypes;

     public bool HasIntraClusterCallsInDestructiveContexts = false;

@@ -7823,7 +7815,6 @@ namespace Microsoft.Dafny
 

     public CoCallResolution(Function currentFunction, bool dealsWithCodatatypes) {

       Contract.Requires(currentFunction != null);

-      this.currentModule = currentFunction.EnclosingClass.Module;

       this.currentFunction = currentFunction;

       this.dealsWithCodatatypes = dealsWithCodatatypes;

     }

@@ -7922,9 +7913,7 @@ namespace Microsoft.Dafny
           CheckCoCalls(arg, int.MaxValue, null, coCandidates);

         }

         // Second, investigate the possibility that this call itself may be a candidate co-call

-        var calleeModule = e.Function.EnclosingClass.Module;

-        if (currentModule == calleeModule &&

-          currentModule.CallGraph.GetSCCRepresentative(currentFunction) == calleeModule.CallGraph.GetSCCRepresentative(e.Function)) {

+        if (ModuleDefinition.InSameSCC(currentFunction, e.Function)) {

           // This call goes to another function in the same recursive cluster

           if (destructionLevel > 0) {

             // a potentially destructive context

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 67fc7268..83623399 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -773,8 +773,7 @@ namespace Microsoft.Dafny
           reqs.AddRange(generateAutoReqs(arg));

         }

 

-        ModuleDefinition module = e.Function.EnclosingClass.Module;

-        if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(parentFunction)) {

+        if (ModuleDefinition.InSameSCC(e.Function, parentFunction)) {

           // We're making a call within the same SCC, so don't descend into this function

         } else {

           reqs.AddRange(gatherReqs(e.Function, e.Args, e.Receiver));

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index cb316008..c6c82193 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3633,49 +3633,46 @@ namespace Microsoft.Dafny {
         Bpl.Expr allowance = null;

         if (codeContext != null && e.CoCall != FunctionCallExpr.CoCallResolution.Yes && !(e.Function is CoPredicate)) {

           // check that the decreases measure goes down

-          ModuleDefinition module = cce.NonNull(e.Function.EnclosingClass).Module;

-          if (module == codeContext.EnclosingModule) {

-            if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(codeContext)) {

-              List<Expression> contextDecreases = codeContext.Decreases.Expressions;

-              List<Expression> calleeDecreases = e.Function.Decreases.Expressions;

-              if (e.Function == options.SelfCallsAllowance) {

-                allowance = Bpl.Expr.True;

-                if (!e.Function.IsStatic) {

-                  allowance = BplAnd(allowance, Bpl.Expr.Eq(etran.TrExpr(e.Receiver), new Bpl.IdentifierExpr(e.tok, etran.This, predef.RefType)));

-                }

-                for (int i = 0; i < e.Args.Count; i++) {

-                  Expression ee = e.Args[i];

-                  Formal ff = e.Function.Formals[i];

-                  allowance = BplAnd(allowance, Bpl.Expr.Eq(etran.TrExpr(ee), new Bpl.IdentifierExpr(e.tok, ff.AssignUniqueName(currentDeclaration), TrType(ff.Type))));

-                }

+          if (ModuleDefinition.InSameSCC(e.Function, codeContext)) {

+            List<Expression> contextDecreases = codeContext.Decreases.Expressions;

+            List<Expression> calleeDecreases = e.Function.Decreases.Expressions;

+            if (e.Function == options.SelfCallsAllowance) {

+              allowance = Bpl.Expr.True;

+              if (!e.Function.IsStatic) {

+                allowance = BplAnd(allowance, Bpl.Expr.Eq(etran.TrExpr(e.Receiver), new Bpl.IdentifierExpr(e.tok, etran.This, predef.RefType)));

               }

-              string hint;

-              switch (e.CoCall) {

-                case FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasSideEffects:

-                  hint = "note that only functions without side effects can be called co-recursively";

-                  break;

-                case FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasPostcondition:

-                  hint = "note that only functions without any ensures clause can be called co-recursively";

-                  break;

-                case FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded:

-                  hint = "note that the call is not sufficiently guarded to be used co-recursively";

-                  break;

-                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;

-                default:

-                  Contract.Assert(false);  // unexpected CoCallResolution

-                  goto case FunctionCallExpr.CoCallResolution.No;  // please the compiler

+              for (int i = 0; i < e.Args.Count; i++) {

+                Expression ee = e.Args[i];

+                Formal ff = e.Function.Formals[i];

+                allowance = BplAnd(allowance, Bpl.Expr.Eq(etran.TrExpr(ee), new Bpl.IdentifierExpr(e.tok, ff.AssignUniqueName(currentDeclaration), TrType(ff.Type))));

               }

-              CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, allowance, e.Receiver, substMap, etran, etran, builder,

-                codeContext.InferredDecreases, hint);

             }

+            string hint;

+            switch (e.CoCall) {

+              case FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasSideEffects:

+                hint = "note that only functions without side effects can be called co-recursively";

+                break;

+              case FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasPostcondition:

+                hint = "note that only functions without any ensures clause can be called co-recursively";

+                break;

+              case FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded:

+                hint = "note that the call is not sufficiently guarded to be used co-recursively";

+                break;

+              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;

+              default:

+                Contract.Assert(false);  // unexpected CoCallResolution

+                goto case FunctionCallExpr.CoCallResolution.No;  // please the compiler

+            }

+            CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, allowance, e.Receiver, substMap, etran, etran, builder,

+              codeContext.InferredDecreases, hint);

           }

         }

         // all is okay, so allow this function application access to the function's axiom, except if it was okay because of the self-call allowance.

@@ -6327,7 +6324,7 @@ namespace Microsoft.Dafny {
           codeContext is PrefixLemma ? ((PrefixLemma)codeContext).Co :

           codeContext is IteratorDecl ? ((IteratorDecl)codeContext).Member_MoveNext :

           codeContext;

-        if (module.CallGraph.GetSCCRepresentative(method) == module.CallGraph.GetSCCRepresentative(cllr)) {

+        if (ModuleDefinition.InSameSCC(method, cllr)) {

           isRecursiveCall = true;

         }

       }

@@ -8165,8 +8162,7 @@ namespace Microsoft.Dafny {
             ModuleDefinition module = e.Function.EnclosingClass.Module;

             if (this.applyLimited_CurrentFunction != null &&

               this.layerIntraCluster != null &&

-              module == applyLimited_CurrentFunction.EnclosingClass.Module &&

-              module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(applyLimited_CurrentFunction)) {

+              ModuleDefinition.InSameSCC(e.Function, applyLimited_CurrentFunction)) {

               layerArgument = this.layerIntraCluster;

             } else {

               layerArgument = LayerN(layerInterCluster);

@@ -10341,8 +10337,7 @@ namespace Microsoft.Dafny {
         if (expr is FunctionCallExpr) {

           var e = (FunctionCallExpr)expr;

           var cof = e.Function as CoPredicate;

-          if (cof != null && cof.EnclosingClass.Module == module &&

-            module.CallGraph.GetSCCRepresentative(cof) == module.CallGraph.GetSCCRepresentative(coPred)) {

+          if (cof != null && ModuleDefinition.InSameSCC(cof, coPred)) {

             expr = cof.CreatePrefixPredicateCall(e, coDepth);

           }

         }

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 7b546c36..1521376e 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1380,8 +1380,16 @@ Execution trace:
     (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Then

+Corecursion.dfy(146,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+Corecursion.dfy(159,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

 

-Dafny program verifier finished with 10 verified, 6 errors

+Dafny program verifier finished with 15 verified, 8 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 d8eb296d..e22bbf84 100644
--- a/Test/dafny0/Corecursion.dfy
+++ b/Test/dafny0/Corecursion.dfy
@@ -124,3 +124,44 @@ module MixRecursiveAndCorecursive {
     X(n-1)

   }

 }

+

+// --------------------------------------------------

+

+module FunctionSCCsWithMethods {

+  codatatype Stream<T> = Cons(head: T, tail: Stream)

+

+  lemma M(n: nat)

+    decreases n, 0;

+  {

+    if n != 0 {

+      var p := Cons(10, F(n-1));

+    }

+  }

+

+  function F(n: nat): Stream<int>

+    decreases n;

+  {

+    M(n);

+    // the following call to F is not considered co-recursive, because the SCC contains a method

+    Cons(5, F(n))  // error: cannot prove termination

+  }

+

+  function G(): Stream<int>

+  {

+    Lemma();

+    H()

+  }

+

+  function H(): Stream<int>

+    decreases 0;

+  {

+    // the following call to G is not considered co-recursive, because the SCC contains a method

+    Cons(5, G())  // error: cannot prove termination

+  }

+

+  lemma Lemma()

+    decreases 1;

+  {

+    var h := H();

+  }

+}