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

8 files changed, 115 insertions, 14 deletions

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index a4d0eba1..74e32823 100644
--- a/Dafny/Dafny.atg
+++ b/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/Dafny/Parser.cs b/Dafny/Parser.cs
index bd5ba6dc..489a233e 100644
--- a/Dafny/Parser.cs
+++ b/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/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs
index 28387f16..6af14b14 100644
--- a/Dafny/RefinementTransformer.cs
+++ b/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/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 24ae33db..38766b58 100644
--- a/Dafny/Resolver.cs
+++ b/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/Dafny/Translator.cs b/Dafny/Translator.cs
index 5ce0e1a1..8ecd93e7 100644
--- a/Dafny/Translator.cs
+++ b/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>();

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index ac5e6be5..46cd614b 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1607,6 +1607,14 @@ RefinementModificationChecking.dfy(17,4): Error: cannot assign to variable defin
 RefinementModificationChecking.dfy(18,4): Error: cannot assign to variable defined previously

 2 resolution/type errors detected in RefinementModificationChecking.dfy

 

+-------------------- TailCalls.dfy --------------------

+TailCalls.dfy(18,15): Error: this recursive call is not recognized as being tail recursive, because it is followed by non-ghost code

+TailCalls.dfy(30,12): Error: 'decreases *' is allowed only on tail-recursive methods

+TailCalls.dfy(37,12): Error: 'decreases *' is allowed only on tail-recursive methods

+TailCalls.dfy(42,12): Error: 'decreases *' is allowed only on tail-recursive methods

+TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive methods

+5 resolution/type errors detected in TailCalls.dfy

+

 -------------------- SmallTests.dfy --------------------

 SmallTests.dfy(30,11): Error: index out of range

 Execution trace:

diff --git a/Test/dafny0/TailCalls.dfy b/Test/dafny0/TailCalls.dfy
new file mode 100644
index 00000000..0aa46348
--- /dev/null
+++ b/Test/dafny0/TailCalls.dfy
@@ -0,0 +1,74 @@
+method {:tailrecursion} A(q: int) returns (x: int, ghost y: bool, z: nat)

+{

+  if (q < 10) {

+    x, y, z := 15, true, 20;

+  } else {

+    ghost var u;

+    x, u, z := A(q-1);

+    y := !u;

+  }

+}

+

+method {:tailrecursion} B(q: int) returns (x: int, ghost y: bool, z: nat)

+{

+  if (q < 10) {

+    x, y, z := 15, true, 20;

+  } else {

+    ghost var u;

+    x, u, z := B(q-1);  // error: not a tail call, because it is followed by an increment to x

+    y, x := !u, x + 1;

+  }

+}

+

+method C(q: int) returns (x: int)

+  decreases *;

+{

+  x := C(q-1);

+}

+

+method D(q: int) returns (x: int)

+  decreases *;  // error: not allowed, because the method is not tail recursive

+{

+  x := D(q-1);

+  x := x + 1;

+}

+

+method E0(q: int) returns (x: int)

+  decreases *;  // error: not allowed, because the method is not tail recursive (since mutually recursive methods are currently not recognized as being tail recursive)

+{

+  x := E1(q-1);

+}

+method E1(q: int) returns (x: int)

+  decreases *;  // error: not allowed, because the method is not tail recursive (since mutually recursive methods are currently not recognized as being tail recursive)

+{

+  x := E0(q);

+}

+

+method F0(q: int) returns (x: int)

+  decreases *;  // fine, but no 'decreases' spec is needed at all here

+{

+  x := D(q);

+}

+method F1(q: int) returns (x: int)

+  decreases 5;  // since this is okay (that is, you can--for no particular reason--add a 'decreases' clause to a non-recursive method), the 'decreases *' above is also allowed

+{

+  x := D(q);

+}

+

+method {:tailrecursion} G0(q: int) returns (x: int)

+  decreases *;

+{

+  x := D(q);

+}

+method {:tailrecursion false} G1(q: int) returns (x: int)

+  decreases *;  // error: even though there is no recursion in this method's body, the annotation specifically says "not tail recursive", so (the easiest thing to do in the Resolver was to) generate an error

+{

+  x := D(q);

+}

+

+method H0(q: int) returns (x: int)

+  decreases *;  // fine, but no 'decreases' spec is needed at all here

+method {:tailrecursion} H1(q: int) returns (x: int)

+  decreases *;  // fine, but no 'decreases' spec is needed at all here

+method H2(q: int) returns (x: int)

+  decreases 5;  // fine, but no 'decreases' spec is needed at all here

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 7a836c5a..1ccb292c 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -23,7 +23,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

             CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy

             Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy

-            RefinementModificationChecking.dfy) do (

+            RefinementModificationChecking.dfy TailCalls.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f