From d9127df9c2f0b3643780247f6330d10d4a248a3b Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 7 Sep 2012 19:00:09 -0700 Subject: Dafny: Added detection and support for tail recursive calls (and an optional "tailrecursion" attribute). Also, let the cloner also clone attributes. --- Dafny/Cloner.cs | 58 ++++++++++------ Dafny/Compiler.cs | 170 +++++++++++++++++++++++++++++++-------------- Dafny/DafnyAst.cs | 3 +- Dafny/Resolver.cs | 203 ++++++++++++++++++++++++++++++++++++++++++++++++++++-- 4 files changed, 354 insertions(+), 80 deletions(-) diff --git a/Dafny/Cloner.cs b/Dafny/Cloner.cs index 4b588289..6d99ce9b 100644 --- a/Dafny/Cloner.cs +++ b/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 CloneSpecExpr(Specification spec) { var ee = spec.Expressions == null ? null : spec.Expressions.ConvertAll(CloneExpr); - return new Specification(ee, null); + return new Specification(ee, CloneAttributes(spec.Attributes)); } public Specification CloneSpecFrameExpr(Specification frame) { var ee = frame.Expressions == null ? null : frame.Expressions.ConvertAll(CloneFrameExpr); - return new Specification(ee, null); + return new Specification(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/Dafny/Compiler.cs b/Dafny/Compiler.cs index 18721cf3..8715c047 100644 --- a/Dafny/Compiler.cs +++ b/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(); - 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(); + 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(); - 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(); + 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(); + 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/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index 46c15cf9..c8c61c55 100644 --- a/Dafny/DafnyAst.cs +++ b/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 refinementBase, Attributes attributes, bool isBuiltinName) + public ModuleDefinition(IToken tok, string name, bool isGhost, bool isAbstract, List 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/*!*/ Ens; public readonly Specification/*!*/ 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/Dafny/Resolver.cs b/Dafny/Resolver.cs index 363eb4e0..24ae33db 100644 --- a/Dafny/Resolver.cs +++ b/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 + } + + /// + /// 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). + /// + TailRecursionStatus CheckTailRecursive(List 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; + } + + /// + /// See CheckTailRecursive(List Statement, ...), including its description of "tailCall". + /// In the current implementation, "enclosingMethod" is not allowed to be a mutually recursive method. + /// + 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; -- cgit v1.2.3