Fixed unsoundness (and also allowed other, sound cases) in the admissability checks for co-recursive calls

3 files changed, 50 insertions, 18 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index d6393b02..762bcc7e 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -7382,6 +7382,19 @@ namespace Microsoft.Dafny
           }

           return candidates;

         }

+      } else if (expr is BinaryExpr) {

+        var e = (BinaryExpr)expr;

+        if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.EqCommon || e.ResolvedOp == BinaryExpr.ResolvedOpcode.NeqCommon) {

+          if (e.E0.Type.IsCoDatatype) {

+            // Co-datatype equality (and disequality) are as destructive as can be--in essence, they destruct the values indefinitely--so don't allow

+            // any co-recursive calls in the operands.

+            var r = CheckCoCalls(e.E0, false, null);

+            Contract.Assert(r.Count == 0);  // follows from postcondition of CheckCoCalls, given that we pass in allowCallsWithinRecursiveCluster==false

+            r = CheckCoCalls(e.E1, false, null);

+            Contract.Assert(r.Count == 0);  // follows from postcondition of CheckCoCalls, given that we pass in allowCallsWithinRecursiveCluster==false

+            return candidates;

+          }

+        }

       } else if (expr is MatchExpr) {

         var e = (MatchExpr)expr;

         var r = CheckCoCalls(e.Source, false, null);

@@ -7435,13 +7448,6 @@ namespace Microsoft.Dafny
           Contract.Assert(r.Count == 0);  // follows from postcondition of CheckCoCalls

         }

         return CheckCoCalls(e.Body, allowCallsWithinRecursiveCluster, null);

-      } else if (expr is ComprehensionExpr) {

-        var e = (ComprehensionExpr)expr;

-        foreach (var ee in e.SubExpressions) {

-          var r = CheckCoCalls(ee, false, null);

-          Contract.Assert(r.Count == 0);  // follows from postcondition of CheckCoCalls

-        }

-        return candidates;

       }

 

       // Default handling:

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 97097cfd..36a6eda9 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1151,8 +1151,11 @@ Execution trace:
 Corecursion.dfy(50,5): Error: cannot prove termination; try supplying a decreases clause

 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)

+Execution trace:

+    (0,0): anon5_Else

 

-Dafny program verifier finished with 5 verified, 2 errors

+Dafny program verifier finished with 7 verified, 3 errors

 

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

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

@@ -1696,36 +1699,36 @@ Execution trace:
 Dafny program verifier finished with 1 verified, 4 errors

 

 -------------------- Superposition.dfy --------------------

-
+

 Verifying CheckWellformed$$_0_M0.C.M ...

   [0 proof obligations]  verified

-
+

 Verifying Impl$$_0_M0.C.M ...

   [4 proof obligations]  verified

-
+

 Verifying CheckWellformed$$_0_M0.C.P ...

   [4 proof obligations]  verified

-
+

 Verifying CheckWellformed$$_0_M0.C.Q ...

   [3 proof obligations]  error

 Superposition.dfy(24,15): Error BP5003: A postcondition might not hold on this return path.

 Superposition.dfy(25,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon5_Else

-
+

 Verifying CheckWellformed$$_0_M0.C.R ...

   [3 proof obligations]  error

 Superposition.dfy(30,15): Error BP5003: A postcondition might not hold on this return path.

 Superposition.dfy(31,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon5_Else

-
+

 Verifying CheckWellformed$$_1_M1.C.M ...

   [0 proof obligations]  verified

-
+

 Verifying Impl$$_1_M1.C.M ...

   [1 proof obligation]  verified

-
+

 Verifying CheckWellformed$$_1_M1.C.P ...

   [1 proof obligation]  error

 Superposition.dfy(47,15): Error BP5003: A postcondition might not hold on this return path.

@@ -1734,10 +1737,10 @@ Execution trace:
     (0,0): anon7_Else

     (0,0): anon9_Then

     (0,0): anon6

-
+

 Verifying CheckWellformed$$_1_M1.C.Q ...

   [0 proof obligations]  verified

-
+

 Verifying CheckWellformed$$_1_M1.C.R ...

   [0 proof obligations]  verified

 

diff --git a/Test/dafny0/Corecursion.dfy b/Test/dafny0/Corecursion.dfy
index 0918d6f5..6d3a0e13 100644
--- a/Test/dafny0/Corecursion.dfy
+++ b/Test/dafny0/Corecursion.dfy
@@ -50,3 +50,26 @@ module CoRecursionNotUsed {
     Diverge(n)  // error: cannot prove termination

   }

 }

+

+// --------------------------------------------------

+

+module EqualityIsSuperDestructive {

+  codatatype Stream<T> = Cons(head: T, tail: Stream)

+

+  function F(s: Stream<int>): Stream<int>

+  {

+    // Co-recursive calls are not allowed in arguments of equality, so the following call to

+    // F(s) is a recursive call.

+    if Cons(1, F(s)) == Cons(1, Cons(1, s))  // error: cannot prove termination

+    then Cons(2, s) else Cons(1, s)

+  }

+

+  ghost method lemma(s: Stream<int>)

+  {

+    // The following three assertions follow from the definition of F, so F had better

+    // generate some error (which it does -- the recursive call to F in F does not terminate).

+    assert F(s) == Cons(1, s);

+    assert F(s) == Cons(2, s);

+    assert false;

+  }

+}