Fixed soundness bug with co-recursive calls: co-recursive calls may now no longer to to functions with ensures clauses

7 files changed, 59 insertions, 10 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 61ed3419..f5010443 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3921,7 +3921,14 @@ namespace Microsoft.Dafny {
     public readonly IToken OpenParen;  // can be null if Args.Count == 0

     public readonly List<Expression/*!*/>/*!*/ Args;

     public Dictionary<TypeParameter, Type> TypeArgumentSubstitutions;  // created, initialized, and used by resolution (and also used by translation)

-    public enum CoCallResolution { No, Yes, NoBecauseFunctionHasSideEffects, NoBecauseRecursiveCallsAreNotAllowedInThisContext, NoBecauseIsNotGuarded }

+    public enum CoCallResolution {

+      No,

+      Yes,

+      NoBecauseFunctionHasSideEffects,

+      NoBecauseFunctionHasPostcondition,

+      NoBecauseRecursiveCallsAreNotAllowedInThisContext,

+      NoBecauseIsNotGuarded

+    }

     public CoCallResolution CoCall = CoCallResolution.No;  // indicates whether or not the call is a co-recursive call; filled in by resolution

 

     [ContractInvariantMethod]

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 762bcc7e..dd59bf57 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -7425,6 +7425,18 @@ namespace Microsoft.Dafny
             } else {

               e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded;

             }

+          } else if (e.Function.Ens.Count != 0) {

+            // this call is disqualified from being a co-call, because it has a postcondition

+            // (a postcondition could be allowed, as long as it does not get to be used with

+            // co-recursive calls, because that could be unsound; for example, consider

+            // "ensures false;")

+            if (!dealsWithCodatatypes) {

+              e.CoCall = FunctionCallExpr.CoCallResolution.No;

+            } else if (coContext != null) {

+              e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasPostcondition;

+            } else {

+              e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded;

+            }

           } else if (!allowCallsWithinRecursiveCluster) {

             if (!dealsWithCodatatypes) {

               e.CoCall = FunctionCallExpr.CoCallResolution.No;

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index ba993caf..49173230 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3303,7 +3303,10 @@ namespace Microsoft.Dafny {
                 string hint;

                 switch (e.CoCall) {

                   case FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasSideEffects:

-                    hint = "note that only functions without side effects can called co-recursively";

+                    hint = "note that only functions without side effects can be called co-recursively";

+                    break;

+                  case FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasPostcondition:

+                    hint = "note that only functions without any ensures clause can be called co-recursively";

                     break;

                   case FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded:

                     hint = "note that the call is not sufficiently guarded to be used co-recursively";

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 36a6eda9..e20227e7 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1145,17 +1145,20 @@ Coinductive.dfy(92,21): Error: a recursive copredicate call can only be done in
 8 resolution/type errors detected in Coinductive.dfy

 

 -------------------- Corecursion.dfy --------------------

-Corecursion.dfy(15,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without side effects can called co-recursively)

+Corecursion.dfy(15,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without side effects can be called co-recursively)

 Execution trace:

     (0,0): anon3_Else

-Corecursion.dfy(50,5): Error: cannot prove termination; try supplying a decreases clause

+Corecursion.dfy(21,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without any ensures clause can be called co-recursively)

 Execution trace:

     (0,0): anon3_Else

-Corecursion.dfy(63,16): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context)

+Corecursion.dfy(56,5): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon3_Else

+Corecursion.dfy(69,16): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context)

 Execution trace:

     (0,0): anon5_Else

 

-Dafny program verifier finished with 7 verified, 3 errors

+Dafny program verifier finished with 7 verified, 4 errors

 

 -------------------- CoResolution.dfy --------------------

 CoResolution.dfy(14,9): Error: member Undeclared# does not exist in class _default

diff --git a/Test/dafny0/Corecursion.dfy b/Test/dafny0/Corecursion.dfy
index 6d3a0e13..5025dae9 100644
--- a/Test/dafny0/Corecursion.dfy
+++ b/Test/dafny0/Corecursion.dfy
@@ -15,6 +15,12 @@ module CoRecursion {
     More(n, AscendingChainAndRead(n+1))  // error: cannot prove termination

   }

 

+  function AscendingChainAndPostcondition(n: nat): Stream<int>

+    ensures false;  // with an ensures clause, this function is not a co-recusvie function

+  {

+    More(n, AscendingChainAndPostcondition(n+1))  // error: cannot prove termination

+  }

+

   datatype List<T> = Nil | Cons(T, List);

 

   function Prefix(n: nat, s: Stream): List

diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer
index 9c6a2598..6ca8aafa 100644
--- a/Test/dafny3/Answer
+++ b/Test/dafny3/Answer
@@ -5,7 +5,7 @@ Dafny program verifier finished with 15 verified, 0 errors
 

 -------------------- Streams.dfy --------------------

 

-Dafny program verifier finished with 50 verified, 0 errors

+Dafny program verifier finished with 52 verified, 0 errors

 

 -------------------- Dijkstra.dfy --------------------

 

diff --git a/Test/dafny3/Streams.dfy b/Test/dafny3/Streams.dfy
index 1198c7e0..f13c5c0a 100644
--- a/Test/dafny3/Streams.dfy
+++ b/Test/dafny3/Streams.dfy
@@ -235,22 +235,40 @@ function PrependThenFlattenNonEmpties(prefix: Stream, M: Stream<Stream>): Stream
 // of a given stream of streams.

 

 function Prepend<T>(x: T, M: Stream<Stream>): Stream<Stream>

-  ensures StreamOfNonEmpties(Prepend(x, M));

 {

   match M

   case Nil => Nil

   case Cons(s, N) => Cons(Cons(x, s), Prepend(x, N))

 }

 

+comethod Prepend_Lemma<T>(x: T, M: Stream<Stream>)

+  ensures StreamOfNonEmpties(Prepend(x, M));

+{

+  match M {

+    case Nil =>

+    case Cons(s, N) =>  Prepend_Lemma(x, N);

+  }

+}

+

 ghost method Theorem_Flatten<T>(M: Stream<Stream>, startMarker: T)

-  ensures FlattenStartMarker(M, startMarker) == FlattenNonEmpties(Prepend(startMarker, M));

+  ensures

+    StreamOfNonEmpties(Prepend(startMarker, M)) ==> // always holds, on account of Prepend_Lemma;

+                                          // but until (co-)method can be called from functions,

+                                          // this condition is used as an antecedent here

+    FlattenStartMarker(M, startMarker) == FlattenNonEmpties(Prepend(startMarker, M));

 {

+  Prepend_Lemma(startMarker, M);

   Lemma_Flatten(Nil, M, startMarker);

 }

 

 comethod Lemma_Flatten<T>(prefix: Stream, M: Stream<Stream>, startMarker: T)

-  ensures PrependThenFlattenStartMarker(prefix, M, startMarker) == PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, M));

+  ensures

+    StreamOfNonEmpties(Prepend(startMarker, M)) ==> // always holds, on account of Prepend_Lemma;

+                                          // but until (co-)method can be called from functions,

+                                          // this condition is used as an antecedent here

+    PrependThenFlattenStartMarker(prefix, M, startMarker) == PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, M));

 {

+  Prepend_Lemma(startMarker, M);

   match (prefix) {

     case Cons(hd, tl) =>

     Lemma_Flatten(tl, M, startMarker);