Fixed the problem with the previous check-in.

2 files changed, 34 insertions, 24 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index bb7cbe23..fa72c6e4 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -596,9 +596,12 @@ namespace Microsoft.Dafny
   /// </summary>

   class CoMethodBodyCloner : Cloner

   {

+    readonly CoMethod context;

     readonly Expression k;

-    public CoMethodBodyCloner(Expression k) {

+    public CoMethodBodyCloner(CoMethod context, Expression k) {

+      Contract.Requires(context != null);

       Contract.Requires(k != null);

+      this.context = context;

       this.k = k;

     }

     public override Statement CloneStmt(Statement stmt) {

@@ -613,19 +616,26 @@ namespace Microsoft.Dafny
         }

       } else if (stmt is CallStmt) {

         var s = (CallStmt)stmt;

-        var lhs = s.Lhs.ConvertAll(CloneExpr);

-        var receiver = CloneExpr(s.Receiver);

-        var args = new List<Expression>();

-        args.Add(k);

-        foreach (var arg in s.Args) {

-          args.Add(CloneExpr(arg));

+        if (s.Method is CoMethod) {

+          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 to a comethod

+            var lhs = s.Lhs.ConvertAll(CloneExpr);

+            var receiver = CloneExpr(s.Receiver);

+            var args = new List<Expression>();

+            args.Add(k);

+            foreach (var arg in s.Args) {

+              args.Add(CloneExpr(arg));

+            }

+            var r = new CallStmt(Tok(s.Tok), lhs, receiver, s.MethodName + "#", args);

+

+            // don't forget to add labels to the cloned statement

+            AddStmtLabels(r, stmt.Labels);

+            r.Attributes = CloneAttributes(stmt.Attributes);

+            return r;

+          }

         }

-        var r = new CallStmt(Tok(s.Tok), lhs, receiver, s.MethodName + "#", args);

-

-        // don't forget to add labels to the cloned statement

-        AddStmtLabels(r, stmt.Labels);

-        r.Attributes = CloneAttributes(stmt.Attributes);

-        return r;

       }

       return base.CloneStmt(stmt);

     }

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 6c9e136e..a3749372 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -666,10 +666,6 @@ namespace Microsoft.Dafny
                   var com = (CoMethod)m;

                   // _k has already been added to 'formals', so append the original formals

                   formals.AddRange(com.Ins.ConvertAll(cloner.CloneFormal));

-                  // prepend "free requires 0 < _k;", since the postcondition of a comethod holds trivially if _k is 0

-                  var req = new List<MaybeFreeExpression>();

-                  req.Add(new MaybeFreeExpression(new BinaryExpr(k.tok, BinaryExpr.Opcode.Lt, new LiteralExpr(k.tok, 0), new IdentifierExpr(k.tok, k.Name)), true));

-                  req.AddRange(com.Req.ConvertAll(cloner.CloneMayBeFreeExpr));

                   // prepend _k to the given decreases clause

                   var decr = new List<Expression>();

                   decr.Add(new IdentifierExpr(com.tok, k.Name));

@@ -677,10 +673,11 @@ namespace Microsoft.Dafny
                   // Create prefix method.  Note that the body is not cloned, but simply shared.

                   com.PrefixMethod = new PrefixMethod(com.tok, extraName, com.IsStatic,

                     com.TypeArgs.ConvertAll(cloner.CloneTypeParam), k, formals, com.Outs.ConvertAll(cloner.CloneFormal),

-                    req, cloner.CloneSpecFrameExpr(com.Mod), new List<MaybeFreeExpression>(),  // Note, the postconditions are filled in after the comethod's postconditions have been resolved

+                    com.Req.ConvertAll(cloner.CloneMayBeFreeExpr), cloner.CloneSpecFrameExpr(com.Mod),

+                    new List<MaybeFreeExpression>(),  // Note, the postconditions are filled in after the comethod's postconditions have been resolved

                     new Specification<Expression>(decr, null),

                     null, // Note, the body for the prefix method will be created once the call graph has been computed and the SCC for the comethod is known

-                    null, com);

+                    cloner.CloneAttributes(com.Attributes), 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);

@@ -1183,8 +1180,11 @@ namespace Microsoft.Dafny
           // Compute the statement body of the prefix method

           if (com.Body != null) {

             var kMinusOne = new BinaryExpr(com.tok, BinaryExpr.Opcode.Sub, new IdentifierExpr(k.tok, k.Name), new LiteralExpr(com.tok, 1));

-            var subst = new CoMethodBodyCloner(kMinusOne);

-            prefixMethod.Body = subst.CloneBlockStmt(com.Body);

+            var subst = new CoMethodBodyCloner(com, kMinusOne);

+            var mainBody = subst.CloneBlockStmt(com.Body);

+            var kPositive = new BinaryExpr(com.tok, BinaryExpr.Opcode.Lt, new LiteralExpr(com.tok, 0), new IdentifierExpr(k.tok, k.Name));

+            var condBody = new IfStmt(com.BodyStartTok, kPositive, mainBody, null);

+            prefixMethod.Body = new BlockStmt(com.tok, new List<Statement>() { condBody });

           }

           // The prefix method now has all its components, so it's finally time we resolve it

           currentClass = (ClassDecl)prefixMethod.EnclosingClass;

@@ -2673,9 +2673,6 @@ namespace Microsoft.Dafny
         scope.Push(p.Name, p);

       }

 

-      // attributes are allowed to mention both in- and out-parameters

-      ResolveAttributes(m.Attributes, false);

-

       // ... continue resolving specification

       foreach (MaybeFreeExpression e in m.Ens) {

         ResolveExpression(e.E, true);

@@ -2697,6 +2694,9 @@ namespace Microsoft.Dafny
         ResolveBlockStatement(m.Body, m.IsGhost, codeContext);

       }

 

+      // attributes are allowed to mention both in- and out-parameters (including the implicit _k, for comethods)

+      ResolveAttributes(m.Attributes, false);

+

       scope.PopMarker();  // for the out-parameters and outermost-level locals

       scope.PopMarker();  // for the in-parameters

     }