Dafny: allow 'decreases *' (that is, non-terminating recursion) on tail-recursive methods

5 files changed, 32 insertions, 13 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index a4d0eba1..74e32823 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -487,7 +487,7 @@ MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/
     ( "requires" Expression<out e> SYNC ";"                       (. req.Add(new MaybeFreeExpression(e, isFree)); .)

     | "ensures" { IF(IsAttribute()) Attribute<ref ensAttrs> } Expression<out e> SYNC ";"          (. ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); .)

     )

-  | "decreases" { IF(IsAttribute()) Attribute<ref decAttrs> } DecreasesList<decreases, false> SYNC ";"

+  | "decreases" { IF(IsAttribute()) Attribute<ref decAttrs> } DecreasesList<decreases, true> SYNC ";"

   )

   .

 Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals, out IToken openParen.>

@@ -1087,13 +1087,13 @@ Invariant<out MaybeFreeExpression/*!*/ invariant>
 DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>

 = (. Expression/*!*/ e; .)

   PossiblyWildExpression<out e>          (. if (!allowWildcard && e is WildcardExpr) {

-                                              SemErr(e.tok, "'decreases *' is only allowed on loops");

+                                              SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");

                                             } else {

                                               decreases.Add(e);

                                             }

                                          .)

   { "," PossiblyWildExpression<out e>    (. if (!allowWildcard && e is WildcardExpr) {

-                                              SemErr(e.tok, "'decreases *' is only allowed on loops");

+                                              SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");

                                             } else {

                                               decreases.Add(e);

                                             }

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index bd5ba6dc..489a233e 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -980,7 +980,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			while (IsAttribute()) {

 				Attribute(ref decAttrs);

 			}

-			DecreasesList(decreases, false);

+			DecreasesList(decreases, true);

 			while (!(la.kind == 0 || la.kind == 14)) {SynErr(137); Get();}

 			Expect(14);

 		} else SynErr(138);

@@ -1032,7 +1032,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression/*!*/ e; 

 		PossiblyWildExpression(out e);

 		if (!allowWildcard && e is WildcardExpr) {

-		 SemErr(e.tok, "'decreases *' is only allowed on loops");

+		 SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");

 		} else {

 		 decreases.Add(e);

 		}

@@ -1041,7 +1041,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 			PossiblyWildExpression(out e);

 			if (!allowWildcard && e is WildcardExpr) {

-			 SemErr(e.tok, "'decreases *' is only allowed on loops");

+			 SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");

 			} else {

 			 decreases.Add(e);

 			}

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 28387f16..6af14b14 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -502,14 +502,14 @@ namespace Microsoft.Dafny
       }

     }

 

-    Method CloneMethod(Method m, List<MaybeFreeExpression> moreEnsures, BlockStmt replacementBody) {

+    Method CloneMethod(Method m, List<MaybeFreeExpression> moreEnsures, Specification<Expression> decreases, BlockStmt replacementBody) {

       Contract.Requires(m != null);

+      Contract.Requires(decreases != null);

 

       var tps = m.TypeArgs.ConvertAll(refinementCloner.CloneTypeParam);

       var ins = m.Ins.ConvertAll(refinementCloner.CloneFormal);

       var req = m.Req.ConvertAll(refinementCloner.CloneMayBeFreeExpr);

       var mod = refinementCloner.CloneSpecFrameExpr(m.Mod);

-      var decreases = refinementCloner.CloneSpecExpr(m.Decreases);

 

       List<MaybeFreeExpression> ens;

       if (replacementBody != null)

@@ -619,10 +619,15 @@ namespace Microsoft.Dafny
               if (m.Mod.Expressions.Count != 0) {

                 reporter.Error(m.Mod.Expressions[0].E.tok, "a refining method is not allowed to extend the modifies clause");

               }

-              if (m.Decreases.Expressions.Count != 0) {

-                reporter.Error(m.Decreases.Expressions[0].tok, "decreases clause on refining method not supported");

+              Specification<Expression> decreases;

+              if (Contract.Exists(prevMethod.Decreases.Expressions, e => e is WildcardExpr)) {

+                decreases = m.Decreases;

+              } else {

+                if (m.Decreases.Expressions.Count != 0) {

+                  reporter.Error(m.Decreases.Expressions[0].tok, "decreases clause on refining method not supported, unless the refined method was specified with 'decreases *'");

+                }

+                decreases = refinementCloner.CloneSpecExpr(prevMethod.Decreases);

               }

-

               if (prevMethod.IsStatic != m.IsStatic) {

                 reporter.Error(m, "a method in a refining module cannot be changed from static to non-static or vice versa: {0}", m.Name);

               }

@@ -649,7 +654,7 @@ namespace Microsoft.Dafny
                   replacementBody = MergeBlockStmt(replacementBody, prevMethod.Body);

                 }

               }

-              nw.Members[index] = CloneMethod(prevMethod, m.Ens, replacementBody);

+              nw.Members[index] = CloneMethod(prevMethod, m.Ens, decreases, replacementBody);

             }

           }

         }

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 24ae33db..38766b58 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -976,6 +976,8 @@ namespace Microsoft.Dafny
                   bool hasTailRecursionPreference = Attributes.ContainsBool(m.Attributes, "tailrecursion", ref tail);

                   if (hasTailRecursionPreference && !tail) {

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

+                  } else if (hasTailRecursionPreference && tail && m.IsGhost) {

+                    Error(m.tok, "tail recursion can be specified only for methods that will be compiled, not for ghost methods");

                   } else {

                     var module = m.EnclosingClass.Module;

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

@@ -984,12 +986,15 @@ namespace Microsoft.Dafny
                     } 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)) {

+                      if (status != TailRecursionStatus.NotTailRecursive) {

                         m.IsTailRecursive = true;

                       }

                     }

                   }

                 }

+                if (!m.IsTailRecursive && m.Body != null && Contract.Exists(m.Decreases.Expressions, e => e is WildcardExpr)) {

+                  Error(m.Decreases.Expressions[0].tok, "'decreases *' is allowed only on tail-recursive methods");

+                }

               } else if (member is Function) {

                 var f = (Function)member;

                 if (f.Body != null) {

@@ -2275,6 +2280,9 @@ namespace Microsoft.Dafny
       foreach (Expression e in m.Decreases.Expressions) {

         ResolveExpression(e, false);

         // any type is fine

+        if (m.IsGhost && e is WildcardExpr) {

+          Error(e, "'decreases *' is not allowed on ghost methods");

+        }

       }

 

       // Add out-parameters to a new scope that will also include the outermost-level locals of the body

@@ -3363,6 +3371,7 @@ namespace Microsoft.Dafny
       foreach (var a in s.ResolvedStatements) {

         ResolveStatement(a, specContextOnly, method);

       }

+      s.IsGhost = s.ResolvedStatements.TrueForAll(ss => ss.IsGhost);

     }

 

     bool ResolveAlternatives(List<GuardedAlternative> alternatives, bool specContextOnly, AlternativeLoopStmt loopToCatchBreaks, Method method) {

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 5ce0e1a1..8ecd93e7 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -5042,6 +5042,11 @@ namespace Microsoft.Dafny {
       // order where elements from different Dafny types are incomparable.  Thus, as an optimization below, if two

       // components from different types are compared, the answer is taken to be false.

 

+      if (Contract.Exists(calleeDecreases, e => e is WildcardExpr)) {

+        // no check needed

+        return;

+      }

+

       int N = Math.Min(contextDecreases.Count, calleeDecreases.Count);

       List<IToken> toks = new List<IToken>();

       List<Type> types = new List<Type>();