Dafny: Added detection and support for tail recursive calls (and an optional "tailrecursion" attribute). Also, let the cloner also clone attributes.

4 files changed, 354 insertions, 80 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 4b588289..6d99ce9b 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -14,7 +14,7 @@ namespace Microsoft.Dafny
       if (m is DefaultModuleDecl) {

         nw = new DefaultModuleDecl();

       } else {

-        nw = new ModuleDefinition(Tok(m.tok), name, m.IsGhost, m.IsAbstract, m.RefinementBaseName, null, true);

+        nw = new ModuleDefinition(Tok(m.tok), name, m.IsGhost, m.IsAbstract, m.RefinementBaseName, CloneAttributes(m.Attributes), true);

       }

       foreach (var d in m.TopLevelDecls) {

         nw.TopLevelDecls.Add(CloneDeclaration(d, nw));

@@ -29,18 +29,18 @@ namespace Microsoft.Dafny
 

       if (d is ArbitraryTypeDecl) {

         var dd = (ArbitraryTypeDecl)d;

-        return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, null);

+        return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, CloneAttributes(dd.Attributes));

       } else if (d is IndDatatypeDecl) {

         var dd = (IndDatatypeDecl)d;

         var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

         var ctors = dd.Ctors.ConvertAll(CloneCtor);

-        var dt = new IndDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);

+        var dt = new IndDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, CloneAttributes(dd.Attributes));

         return dt;

       } else if (d is CoDatatypeDecl) {

         var dd = (CoDatatypeDecl)d;

         var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

         var ctors = dd.Ctors.ConvertAll(CloneCtor);

-        var dt = new CoDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);

+        var dt = new CoDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, CloneAttributes(dd.Attributes));

         return dt;

       } else if (d is ClassDecl) {

         if (d is DefaultClassDecl) {

@@ -53,7 +53,7 @@ namespace Microsoft.Dafny
           var dd = (ClassDecl)d;

           var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

           var mm = dd.Members.ConvertAll(CloneMember);

-          var cl = new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, null);

+          var cl = new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes));

           return cl;

         }

       } else if (d is ModuleDecl) {

@@ -84,7 +84,7 @@ namespace Microsoft.Dafny
     }

 

     public DatatypeCtor CloneCtor(DatatypeCtor ct) {

-      return new DatatypeCtor(Tok(ct.tok), ct.Name, ct.Formals.ConvertAll(CloneFormal), null);

+      return new DatatypeCtor(Tok(ct.tok), ct.Name, ct.Formals.ConvertAll(CloneFormal), CloneAttributes(ct.Attributes));

     }

 

     public TypeParameter CloneTypeParam(TypeParameter tp) {

@@ -93,8 +93,9 @@ namespace Microsoft.Dafny
 

     public MemberDecl CloneMember(MemberDecl member) {

       if (member is Field) {

+        Contract.Assert(!(member is SpecialField));  // we don't expect a SpecialField to be cloned (or do we?)

         var f = (Field)member;

-        return new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, CloneType(f.Type), null);

+        return new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, CloneType(f.Type), CloneAttributes(f.Attributes));

       } else if (member is Function) {

         var f = (Function)member;

         return CloneFunction(f);

@@ -142,17 +143,24 @@ namespace Microsoft.Dafny
 

     public Specification<Expression> CloneSpecExpr(Specification<Expression> spec) {

       var ee = spec.Expressions == null ? null : spec.Expressions.ConvertAll(CloneExpr);

-      return new Specification<Expression>(ee, null);

+      return new Specification<Expression>(ee, CloneAttributes(spec.Attributes));

     }

 

     public Specification<FrameExpression> CloneSpecFrameExpr(Specification<FrameExpression> frame) {

       var ee = frame.Expressions == null ? null : frame.Expressions.ConvertAll(CloneFrameExpr);

-      return new Specification<FrameExpression>(ee, null);

+      return new Specification<FrameExpression>(ee, CloneAttributes(frame.Attributes));

     }

 

     public FrameExpression CloneFrameExpr(FrameExpression frame) {

       return new FrameExpression(Tok(frame.tok), CloneExpr(frame.E), frame.FieldName);

     }

+    public Attributes CloneAttributes(Attributes attrs) {

+      if (attrs == null) {

+        return null;

+      } else {

+        return new Attributes(attrs.Name, attrs.Args.ConvertAll(CloneAttrArg), CloneAttributes(attrs.Prev));

+      }

+    }

     public Attributes.Argument CloneAttrArg(Attributes.Argument aa) {

       if (aa.E != null) {

         return new Attributes.Argument(Tok(aa.Tok), CloneExpr(aa.E));

@@ -162,7 +170,9 @@ namespace Microsoft.Dafny
     }

 

     public MaybeFreeExpression CloneMayBeFreeExpr(MaybeFreeExpression expr) {

-      return new MaybeFreeExpression(CloneExpr(expr.E), expr.IsFree);

+      var mfe = new MaybeFreeExpression(CloneExpr(expr.E), expr.IsFree);

+      mfe.Attributes = CloneAttributes(expr.Attributes);

+      return mfe;

     }

 

     public virtual Expression CloneExpr(Expression expr) {

@@ -273,9 +283,9 @@ namespace Microsoft.Dafny
         var range = CloneExpr(e.Range);

         var term = CloneExpr(e.Term);

         if (e is ForallExpr) {

-          return new ForallExpr(tk, bvs, range, term, null);

+          return new ForallExpr(tk, bvs, range, term, CloneAttributes(e.Attributes));

         } else if (e is ExistsExpr) {

-          return new ExistsExpr(tk, bvs, range, term, null);

+          return new ExistsExpr(tk, bvs, range, term, CloneAttributes(e.Attributes));

         } else if (e is MapComprehension) {

           return new MapComprehension(tk, bvs, range, term);

         } else {

@@ -319,21 +329,24 @@ namespace Microsoft.Dafny
     }

 

     public AssignmentRhs CloneRHS(AssignmentRhs rhs) {

+      AssignmentRhs c;

       if (rhs is ExprRhs) {

         var r = (ExprRhs)rhs;

-        return new ExprRhs(CloneExpr(r.Expr));

+        c = new ExprRhs(CloneExpr(r.Expr));

       } else if (rhs is HavocRhs) {

-        return new HavocRhs(Tok(rhs.Tok));

+        c = new HavocRhs(Tok(rhs.Tok));

       } else {

         var r = (TypeRhs)rhs;

         if (r.ArrayDimensions != null) {

-          return new TypeRhs(Tok(r.Tok), CloneType(r.EType), r.ArrayDimensions.ConvertAll(CloneExpr));

+          c = new TypeRhs(Tok(r.Tok), CloneType(r.EType), r.ArrayDimensions.ConvertAll(CloneExpr));

         } else if (r.InitCall != null) {

-          return new TypeRhs(Tok(r.Tok), CloneType(r.EType), (CallStmt)CloneStmt(r.InitCall));

+          c = new TypeRhs(Tok(r.Tok), CloneType(r.EType), (CallStmt)CloneStmt(r.InitCall));

         } else {

-          return new TypeRhs(Tok(r.Tok), CloneType(r.EType));

+          c = new TypeRhs(Tok(r.Tok), CloneType(r.EType));

         }

       }

+      c.Attributes = CloneAttributes(rhs.Attributes);

+      return c;

     }

 

     public BlockStmt CloneBlockStmt(BlockStmt stmt) {

@@ -432,6 +445,7 @@ namespace Microsoft.Dafny
 

       // add labels to the cloned statement

       AddStmtLabels(r, stmt.Labels);

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

 

       return r;

     }

@@ -462,13 +476,13 @@ namespace Microsoft.Dafny
 

       if (f is Predicate) {

         return new Predicate(Tok(f.tok), f.Name, f.IsStatic, f.IsGhost, tps, f.OpenParen, formals,

-          req, reads, ens, decreases, body, Predicate.BodyOriginKind.OriginalOrInherited, null, false);

+          req, reads, ens, decreases, body, Predicate.BodyOriginKind.OriginalOrInherited, CloneAttributes(f.Attributes), false);

       } else if (f is CoPredicate) {

         return new CoPredicate(Tok(f.tok), f.Name, f.IsStatic, tps, f.OpenParen, formals,

-          req, reads, ens, body, null, false);

+          req, reads, ens, body, CloneAttributes(f.Attributes), false);

       } else {

         return new Function(Tok(f.tok), f.Name, f.IsStatic, f.IsGhost, tps, f.OpenParen, formals, CloneType(f.ResultType),

-          req, reads, ens, decreases, body, null, false);

+          req, reads, ens, decreases, body, CloneAttributes(f.Attributes), false);

       }

     }

 

@@ -486,10 +500,10 @@ namespace Microsoft.Dafny
       var body = CloneBlockStmt(m.Body);

       if (m is Constructor) {

         return new Constructor(Tok(m.tok), m.Name, tps, ins,

-          req, mod, ens, decreases, body, null, false);

+          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), false);

       } else {

         return new Method(Tok(m.tok), m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal),

-          req, mod, ens, decreases, body, null, false);

+          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), false);

       }

     }

     public virtual IToken Tok(IToken tok) {

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 18721cf3..8715c047 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -25,6 +25,7 @@ namespace Microsoft.Dafny {
     }

 

     TextWriter wr;

+    Method enclosingMethod;  // non-null when a method body is being translated

 

     public int ErrorCount;

     void Error(string msg, params object[] args) {

@@ -633,7 +634,17 @@ namespace Microsoft.Dafny {
             if (m.Body == null) {

               Error("Method {0} has no body", m.FullName);

             } else {

+              if (m.IsTailRecursive) {

+                Indent(indent); wr.WriteLine("TAIL_CALL_START: ;");

+                if (!m.IsStatic) {

+                  Indent(indent); wr.WriteLine("var _this = this;");

+                }

+              }

+              Contract.Assert(enclosingMethod == null);

+              enclosingMethod = m;

               TrStmtList(m.Body.Body, indent);

+              Contract.Assert(enclosingMethod == m);

+              enclosingMethod = null;

             }

             Indent(indent);  wr.WriteLine("}");

 

@@ -1408,66 +1419,125 @@ namespace Microsoft.Dafny {
       Contract.Requires(s != null);

       Contract.Assert(s.Method != null);  // follows from the fact that stmt has been successfully resolved

 

-      var lvalues = new List<string>();

-      Contract.Assert(s.Lhs.Count == s.Method.Outs.Count);

-      for (int i = 0; i < s.Method.Outs.Count; i++) {

-        Formal p = s.Method.Outs[i];

-        if (!p.IsGhost) {

-          lvalues.Add(CreateLvalue(s.Lhs[i], indent));

+      if (s.Method == enclosingMethod && enclosingMethod.IsTailRecursive) {

+        // compile call as tail-recursive

+

+        // assign the actual in-parameters to temporary variables

+        var inTmps = new List<string>();

+        for (int i = 0; i < s.Method.Ins.Count; i++) {

+          Formal p = s.Method.Ins[i];

+          if (!p.IsGhost) {

+            SpillLetVariableDecls(s.Args[i], indent);

+          }

         }

-      }

-      var outTmps = new List<string>();

-      for (int i = 0; i < s.Method.Outs.Count; i++) {

-        Formal p = s.Method.Outs[i];

-        if (!p.IsGhost) {

-          string target = "_out" + tmpVarCount;

+        if (receiverReplacement != null) {

+          // TODO:  What to do here?  When does this happen, what does it mean?

+        } else if (!s.Method.IsStatic) {

+          SpillLetVariableDecls(s.Receiver, indent);

+

+          string inTmp = "_in" + tmpVarCount;

           tmpVarCount++;

-          outTmps.Add(target);

+          inTmps.Add(inTmp);

           Indent(indent);

-          wr.WriteLine("{0} {1};", TypeName(s.Lhs[i].Type), target);

+          wr.Write("var {0} = ", inTmp);

+          TrExpr(s.Receiver);

+          wr.WriteLine(";");

         }

-      }

-      Contract.Assert(lvalues.Count == outTmps.Count);

-

-      for (int i = 0; i < s.Method.Ins.Count; i++) {

-        Formal p = s.Method.Ins[i];

-        if (!p.IsGhost) {

-          SpillLetVariableDecls(s.Args[i], indent);

+        for (int i = 0; i < s.Method.Ins.Count; i++) {

+          Formal p = s.Method.Ins[i];

+          if (!p.IsGhost) {

+            string inTmp = "_in" + tmpVarCount;

+            tmpVarCount++;

+            inTmps.Add(inTmp);

+            Indent(indent);

+            wr.Write("var {0} = ", inTmp);

+            TrExpr(s.Args[i]);

+            wr.WriteLine(";");

+          }

         }

-      }

-      if (receiverReplacement != null) {

-        Indent(indent);

-        wr.Write("@" + receiverReplacement);

-      } else if (s.Method.IsStatic) {

+        // Now, assign to the formals

+        int n = 0;

+        if (!s.Method.IsStatic) {

+          Indent(indent);

+          wr.WriteLine("_this = {0};", inTmps[n]);

+          n++;

+        }

+        foreach (var p in s.Method.Ins) {

+          if (!p.IsGhost) {

+            Indent(indent);

+            wr.WriteLine("{0} = {1};", p.CompileName, inTmps[n]);

+            n++;

+          }

+        }

+        Contract.Assert(n == inTmps.Count);

+        // finally, the jump back to the head of the method

         Indent(indent);

-        wr.Write(TypeName(cce.NonNull(s.Receiver.Type)));

+        wr.WriteLine("goto TAIL_CALL_START;");

+

       } else {

-        SpillLetVariableDecls(s.Receiver, indent);

-        Indent(indent);

-        TrParenExpr(s.Receiver);

-      }

-      wr.Write(".@{0}(", s.Method.CompileName);

+        // compile call as a regular call

+

+        var lvalues = new List<string>();

+        Contract.Assert(s.Lhs.Count == s.Method.Outs.Count);

+        for (int i = 0; i < s.Method.Outs.Count; i++) {

+          Formal p = s.Method.Outs[i];

+          if (!p.IsGhost) {

+            lvalues.Add(CreateLvalue(s.Lhs[i], indent));

+          }

+        }

+        var outTmps = new List<string>();

+        for (int i = 0; i < s.Method.Outs.Count; i++) {

+          Formal p = s.Method.Outs[i];

+          if (!p.IsGhost) {

+            string target = "_out" + tmpVarCount;

+            tmpVarCount++;

+            outTmps.Add(target);

+            Indent(indent);

+            wr.WriteLine("{0} {1};", TypeName(s.Lhs[i].Type), target);

+          }

+        }

+        Contract.Assert(lvalues.Count == outTmps.Count);

 

-      string sep = "";

-      for (int i = 0; i < s.Method.Ins.Count; i++) {

-        Formal p = s.Method.Ins[i];

-        if (!p.IsGhost) {

-          wr.Write(sep);

-          TrExpr(s.Args[i]);

-          sep = ", ";

+        for (int i = 0; i < s.Method.Ins.Count; i++) {

+          Formal p = s.Method.Ins[i];

+          if (!p.IsGhost) {

+            SpillLetVariableDecls(s.Args[i], indent);

+          }

         }

-      }

+        if (receiverReplacement != null) {

+          Indent(indent);

+          wr.Write("@" + receiverReplacement);

+        } else if (s.Method.IsStatic) {

+          Indent(indent);

+          wr.Write(TypeName(cce.NonNull(s.Receiver.Type)));

+        } else {

+          SpillLetVariableDecls(s.Receiver, indent);

+          Indent(indent);

+          TrParenExpr(s.Receiver);

+        }

+        wr.Write(".@{0}(", s.Method.CompileName);

 

-      foreach (var outTmp in outTmps) {

-        wr.Write("{0}out {1}", sep, outTmp);

-        sep = ", ";

-      }

-      wr.WriteLine(");");

+        string sep = "";

+        for (int i = 0; i < s.Method.Ins.Count; i++) {

+          Formal p = s.Method.Ins[i];

+          if (!p.IsGhost) {

+            wr.Write(sep);

+            TrExpr(s.Args[i]);

+            sep = ", ";

+          }

+        }

 

-      // assign to the actual LHSs

-      for (int j = 0; j < lvalues.Count; j++) {

-        Indent(indent);

-        wr.WriteLine("{0} = {1};", lvalues[j], outTmps[j]);

+        foreach (var outTmp in outTmps) {

+          wr.Write("{0}out {1}", sep, outTmp);

+          sep = ", ";

+        }

+        wr.WriteLine(");");

+

+        // assign to the actual LHSs

+        for (int j = 0; j < lvalues.Count; j++) {

+          Indent(indent);

+          wr.WriteLine("{0} = {1};", lvalues[j], outTmps[j]);

+        }

       }

     }

 

@@ -1651,7 +1721,7 @@ namespace Microsoft.Dafny {
         }

 

       } else if (expr is ThisExpr) {

-        wr.Write("this");

+        wr.Write(enclosingMethod != null && enclosingMethod.IsTailRecursive ? "_this" : "this");

 

       } else if (expr is IdentifierExpr) {

         IdentifierExpr e = (IdentifierExpr)expr;

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 46c15cf9..c8c61c55 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -909,7 +909,7 @@ namespace Microsoft.Dafny {
       Contract.Invariant(CallGraph != null);

     }

 

-    public ModuleDefinition(IToken tok, string name, bool isGhost, bool isAbstract, List<IToken> refinementBase,  Attributes attributes, bool isBuiltinName)

+    public ModuleDefinition(IToken tok, string name, bool isGhost, bool isAbstract, List<IToken> refinementBase, Attributes attributes, bool isBuiltinName)

       : base(tok, name, attributes) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

@@ -1600,6 +1600,7 @@ namespace Microsoft.Dafny {
     public readonly List<MaybeFreeExpression/*!*/>/*!*/ Ens;

     public readonly Specification<Expression>/*!*/ Decreases;

     public BlockStmt Body;  // Body is readonly after construction, except for any kind of rewrite that may take place around the time of resolution

+    public bool IsTailRecursive;  // filled in during resolution

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 363eb4e0..24ae33db 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -969,13 +969,36 @@ namespace Microsoft.Dafny
           if (d is ClassDecl) {

             foreach (var member in ((ClassDecl)d).Members) {

               if (member is Method) {

-                var m = ((Method)member);

-                if (m.Body != null)

+                var m = (Method)member;

+                if (m.Body != null) {

                   CheckTypeInference(m.Body);

+                  bool tail = true;

+                  bool hasTailRecursionPreference = Attributes.ContainsBool(m.Attributes, "tailrecursion", ref tail);

+                  if (hasTailRecursionPreference && !tail) {

+                    // the user specifically requested no tail recursion, so do nothing else

+                  } else {

+                    var module = m.EnclosingClass.Module;

+                    var sccSize = module.CallGraph.GetSCCSize(m);

+                    if (hasTailRecursionPreference && 2 <= sccSize) {

+                      Error(m.tok, "sorry, tail-call optimizations are not supported for mutually recursive methods");

+                    } else if (hasTailRecursionPreference || sccSize == 1) {

+                      CallStmt tailCall = null;

+                      var status = CheckTailRecursive(m.Body.Body, m, ref tailCall, hasTailRecursionPreference);

+                      if (status == TailRecursionStatus.TailCallSpent || (hasTailRecursionPreference && status == TailRecursionStatus.CanBeFollowedByAnything)) {

+                        m.IsTailRecursive = true;

+                      }

+                    }

+                  }

+                }

               } else if (member is Function) {

                 var f = (Function)member;

-                if (f.Body != null)

+                if (f.Body != null) {

                   CheckTypeInference(f.Body);

+                  bool tail = true;

+                  if (Attributes.ContainsBool(f.Attributes, "tailrecursion", ref tail) && tail) {

+                    Error(f.tok, "sorry, tail-call functions are not supported");

+                  }

+                }

               }

             }

           }

@@ -1144,6 +1167,172 @@ namespace Microsoft.Dafny
       }

     }

 

+    enum TailRecursionStatus

+    {

+      NotTailRecursive, // contains code that makes the enclosing method body not tail recursive (in way that is supported)

+      CanBeFollowedByAnything, // the code just analyzed does not do any recursive calls

+      TailCallSpent, // the method body is tail recursive, provided that all code that follows it in the method body is ghost

+    }

+

+    /// <summary>

+    /// Checks if "stmts" can be considered tail recursive, and (provided "reportsError" is true) reports an error if not.

+    /// Note, the current implementation is rather conservative in its analysis; upon need, the

+    /// algorithm could be improved.

+    /// In the current implementation, "enclosingMethod" is not allowed to be a mutually recursive method.

+    /// 

+    /// The incoming value of "tailCall" is not used, but it's nevertheless a 'ref' parameter to allow the

+    /// body to return the incoming value or to omit assignments to it.

+    /// If the return value is CanBeFollowedByAnything, "tailCall" is unchanged.

+    /// If the return value is TailCallSpent, "tailCall" shows one of the calls where the tail call was spent.  (Note,

+    /// there could be several if the statements have branches.)

+    /// If the return value is NoTailRecursive, "tailCall" could be anything.  In this case, an error

+    /// message has been reported (provided "reportsErrors" is true).

+    /// </summary>

+    TailRecursionStatus CheckTailRecursive(List<Statement> stmts, Method enclosingMethod, ref CallStmt tailCall, bool reportErrors) {

+      Contract.Requires(stmts != null);

+      var status = TailRecursionStatus.CanBeFollowedByAnything;

+      foreach (var s in stmts) {

+        if (!s.IsGhost) {

+          if (s is ReturnStmt && ((ReturnStmt)s).hiddenUpdate == null) {

+            return status;

+          }

+          if (status == TailRecursionStatus.TailCallSpent) {

+            // a tail call cannot be followed by non-ghost code

+            if (reportErrors) {

+              Error(tailCall.Tok, "this recursive call is not recognized as being tail recursive, because it is followed by non-ghost code");

+            }

+            return TailRecursionStatus.NotTailRecursive;

+          }

+          status = CheckTailRecursive(s, enclosingMethod, ref tailCall, reportErrors);

+          if (status == TailRecursionStatus.NotTailRecursive) {

+            return status;

+          }

+        }

+      }

+      return status;

+    }

+

+    /// <summary>

+    /// See CheckTailRecursive(List Statement, ...), including its description of "tailCall".

+    /// In the current implementation, "enclosingMethod" is not allowed to be a mutually recursive method.

+    /// </summary>

+    TailRecursionStatus CheckTailRecursive(Statement stmt, Method enclosingMethod, ref CallStmt tailCall, bool reportErrors) {

+      Contract.Requires(stmt != null && !stmt.IsGhost);

+      if (stmt is PrintStmt) {

+      } else if (stmt is BreakStmt) {

+      } else if (stmt is ReturnStmt) {

+        var s = (ReturnStmt)stmt;

+        if (s.hiddenUpdate != null) {

+          return CheckTailRecursive(s.hiddenUpdate, enclosingMethod, ref tailCall, reportErrors);

+        }

+      } else if (stmt is AssignStmt) {

+      } else if (stmt is VarDecl) {

+      } else if (stmt is CallStmt) {

+        var s = (CallStmt)stmt;

+        if (s.Method == enclosingMethod) {

+          // It's a recursive call.  It can be considered a tail call only if the LHS of the call are the

+          // formal out-parameters of the method

+          for (int i = 0; i < s.Lhs.Count; i++) {

+            var formal = enclosingMethod.Outs[i];

+            if (!formal.IsGhost) {

+              var lhs = s.Lhs[i] as IdentifierExpr;

+              if (lhs != null && lhs.Var == formal) {

+                // all is good

+              } else {

+                if (reportErrors) {

+                  Error(s.Tok, "the recursive call to '{0}' is not tail recursive because the actual out-parameter {1} is not the formal out-parameter '{2}'", s.Method.Name, i, formal.Name);

+                }

+                return TailRecursionStatus.NotTailRecursive;

+              }

+            }

+          }

+          tailCall = s;

+          return TailRecursionStatus.TailCallSpent;

+        }

+      } else if (stmt is BlockStmt) {

+        var s = (BlockStmt)stmt;

+        return CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors);

+      } else if (stmt is IfStmt) {

+        var s = (IfStmt)stmt;

+        var stThen = CheckTailRecursive(s.Thn, enclosingMethod, ref tailCall, reportErrors);

+        if (stThen == TailRecursionStatus.NotTailRecursive) {

+          return stThen;

+        }

+        var stElse = s.Els == null ? TailRecursionStatus.CanBeFollowedByAnything : CheckTailRecursive(s.Els, enclosingMethod, ref tailCall, reportErrors);

+        if (stElse == TailRecursionStatus.NotTailRecursive) {

+          return stElse;

+        } else if (stThen == TailRecursionStatus.TailCallSpent || stElse == TailRecursionStatus.TailCallSpent) {

+          return TailRecursionStatus.TailCallSpent;

+        }

+      } else if (stmt is AlternativeStmt) {

+        var s = (AlternativeStmt)stmt;

+        var status = TailRecursionStatus.CanBeFollowedByAnything;

+        foreach (var alt in s.Alternatives) {

+          var st = CheckTailRecursive(alt.Body, enclosingMethod, ref tailCall, reportErrors);

+          if (st == TailRecursionStatus.NotTailRecursive) {

+            return st;

+          } else if (st == TailRecursionStatus.TailCallSpent) {

+            status = st;

+          }

+        }

+        return status;

+      } else if (stmt is WhileStmt) {

+        var s = (WhileStmt)stmt;

+        var status = CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors);

+        if (status != TailRecursionStatus.CanBeFollowedByAnything) {

+          if (status == TailRecursionStatus.NotTailRecursive) {

+            // an error has already been reported

+          } else if (reportErrors) {

+            Error(tailCall.Tok, "a recursive call inside a loop is not recognized as being a tail call");

+          }

+          return TailRecursionStatus.NotTailRecursive;

+        }

+      } else if (stmt is AlternativeLoopStmt) {

+        var s = (AlternativeLoopStmt)stmt;

+        foreach (var alt in s.Alternatives) {

+          var status = CheckTailRecursive(alt.Body, enclosingMethod, ref tailCall, reportErrors);

+          if (status != TailRecursionStatus.CanBeFollowedByAnything) {

+            if (status == TailRecursionStatus.NotTailRecursive) {

+              // an error has already been reported

+            } else if (reportErrors) {

+              Error(tailCall.Tok, "a recursive call inside a loop is not recognized as being a tail call");

+            }

+            return TailRecursionStatus.NotTailRecursive;

+          }

+        }

+      } else if (stmt is ParallelStmt) {

+        var s = (ParallelStmt)stmt;

+        var status = CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors);

+        if (status != TailRecursionStatus.CanBeFollowedByAnything) {

+          if (status == TailRecursionStatus.NotTailRecursive) {

+            // an error has already been reported

+          } else if (reportErrors) {

+            Error(tailCall.Tok, "a recursive call inside a parallel statement is not a tail call");

+          }

+          return TailRecursionStatus.NotTailRecursive;

+        }

+      } else if (stmt is MatchStmt) {

+        var s = (MatchStmt)stmt;

+        var status = TailRecursionStatus.CanBeFollowedByAnything;

+        foreach (var kase in s.Cases) {

+          var st = CheckTailRecursive(kase.Body, enclosingMethod, ref tailCall, reportErrors);

+          if (st == TailRecursionStatus.NotTailRecursive) {

+            return st;

+          } else if (st == TailRecursionStatus.TailCallSpent) {

+            status = st;

+          }

+        }

+        return status;

+      } else if (stmt is AssignSuchThatStmt) {

+      } else if (stmt is ConcreteSyntaxStatement) {

+        var s = (ConcreteSyntaxStatement)stmt;

+        return CheckTailRecursive(s.ResolvedStatements, enclosingMethod, ref tailCall, reportErrors);

+      } else {

+        Contract.Assert(false);  // unexpected statement type

+      }

+      return TailRecursionStatus.CanBeFollowedByAnything;

+    }

+

     enum CallingPosition { Positive, Negative, Neither }

 

     static CallingPosition Invert(CallingPosition cp) {

@@ -4997,7 +5186,7 @@ namespace Microsoft.Dafny
     ///   -- every IntBoundedPool returned has both a lower and an upper bound

     ///   -- no SuperSetBoundedPool is returned

     /// If "returnAllBounds" is true, then:

-    ///   -- a variable may give rise to BoundedPool's

+    ///   -- a variable may give rise to several BoundedPool's

     ///   -- IntBoundedPool bounds may have just one component

     ///   -- a non-null return value means that some bound were found for each variable (but, for example, perhaps one

     ///      variable only has lower bounds, no upper bounds)

@@ -5033,7 +5222,7 @@ namespace Microsoft.Dafny
           Expression lowerBound = bv.Type is NatType ? new LiteralExpr(bv.tok, new BigInteger(0)) : null;

           Expression upperBound = null;

           bool foundBoundsForBv = false;

-          if (lowerBound != null) {

+          if (returnAllBounds && lowerBound != null) {

             bounds.Add(new ComprehensionExpr.IntBoundedPool(lowerBound, upperBound));

             lowerBound = null;

             foundBoundsForBv = true;

@@ -5118,8 +5307,8 @@ namespace Microsoft.Dafny
             }

             if ((lowerBound != null && upperBound != null) ||

                 (returnAllBounds && (lowerBound != null || upperBound != null))) {

-              // we have found two halves

-                  bounds.Add(new ComprehensionExpr.IntBoundedPool(lowerBound, upperBound));

+              // we have found two halves (or, in the case of returnAllBounds, we have found some bound)

+              bounds.Add(new ComprehensionExpr.IntBoundedPool(lowerBound, upperBound));

               lowerBound = null;

               upperBound = null;

               foundBoundsForBv = true;