Allow more tail calls, on account of considering non-loop aggregate statements with only ghost sub-statements to be ghost

3 files changed, 49 insertions, 3 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 1aebf057..502f7f8a 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -998,6 +998,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(stmt != null);

       if (stmt.IsGhost) {

         CheckHasNoAssumes(stmt);

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

         return;

       }

 

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 9b7e1a98..ac56db1e 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1670,7 +1670,10 @@ namespace Microsoft.Dafny
     /// 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);

+      Contract.Requires(stmt != null);

+      if (stmt.IsGhost) {

+        return TailRecursionStatus.NotTailRecursive;

+      }

       if (stmt is PrintStmt) {

       } else if (stmt is BreakStmt) {

       } else if (stmt is ReturnStmt) {

@@ -3644,6 +3647,9 @@ namespace Microsoft.Dafny
           ResolveStatement(s.Update, specContextOnly, codeContext);

           s.ResolvedStatements.Add(s.Update);

         }

+        if (!s.IsGhost) {

+          s.IsGhost = s.Lhss.All(v => v.IsGhost);

+        }

 

       } else if (stmt is AssignStmt) {

         AssignStmt s = (AssignStmt)stmt;

@@ -3764,8 +3770,12 @@ namespace Microsoft.Dafny
         ResolveCallStmt(s, specContextOnly, codeContext, null);

 

       } else if (stmt is BlockStmt) {

+        var s = (BlockStmt)stmt;

         scope.PushMarker();

-        ResolveBlockStatement((BlockStmt)stmt, specContextOnly, codeContext);

+        ResolveBlockStatement(s, specContextOnly, codeContext);

+        if (!s.IsGhost) {

+          s.IsGhost = s.Body.All(ss => ss.IsGhost);  // mark the block statement as ghost if all its substatements are ghost

+        }

         scope.PopMarker();

 

       } else if (stmt is IfStmt) {

@@ -3788,10 +3798,17 @@ namespace Microsoft.Dafny
         if (s.Els != null) {

           ResolveStatement(s.Els, branchesAreSpecOnly, codeContext);

         }

+        if (!s.IsGhost && s.Thn.IsGhost && (s.Els == null || s.Els.IsGhost)) {

+          // mark the entire 'if' statement as ghost if its branches are ghost

+          s.IsGhost = true;

+        }

 

       } else if (stmt is AlternativeStmt) {

         var s = (AlternativeStmt)stmt;

         s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, null, codeContext);

+        if (!s.IsGhost) {

+          s.IsGhost = s.Alternatives.All(alt => alt.Body.All(ss => ss.IsGhost));

+        }

 

       } else if (stmt is WhileStmt) {

         WhileStmt s = (WhileStmt)stmt;

@@ -4071,7 +4088,9 @@ namespace Microsoft.Dafny
           }

           Contract.Assert(memberNamesUsed.Count + s.MissingCases.Count == dtd.Ctors.Count);

         }

-

+        if (!s.IsGhost) {

+          s.IsGhost = s.Cases.All(cs => cs.Body.All(ss => ss.IsGhost));

+        }

 

       } else if (stmt is SkeletonStatement) {

         var s = (SkeletonStatement)stmt;

diff --git a/Test/dafny0/TailCalls.dfy b/Test/dafny0/TailCalls.dfy
index 0aa46348..41a8c49b 100644
--- a/Test/dafny0/TailCalls.dfy
+++ b/Test/dafny0/TailCalls.dfy
@@ -72,3 +72,29 @@ 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

+

+class {:autocontracts} MyAutoContractClass {

+  var left: MyAutoContractClass;

+

+  predicate Valid() { true }

+

+  method {:tailrecursion} VisitLeft(val: int)

+  {

+    if left != null {

+      left.VisitLeft(val);  // this is a tail call, because what :autocontracts appends is ghost

+    }

+  }

+}

+

+method {:tailrecursion} OtherTailCall(n: int) {

+  ghost var x := 12;

+  if n > 0 {

+    OtherTailCall(n-1);  // tail call

+  }

+  x := 14;

+  { x := 13; }

+  ghost var h := 15;

+  if n < h*30 { } // this is a ghost statement as well

+  if n < 230 { } // and this can be (and is) considered ghost as well

+  if (*) { x := x + 1; }  // this, too

+}