Split verification of quantifier expressions into #2 for checked and #1 for assumed.

Fixed cases where token was not being updated for refinement.

4 files changed, 84 insertions, 35 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index a0167cc0..05ca210e 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -9065,8 +9065,10 @@ namespace Microsoft.Dafny {
           var etran2 = etran.LayerOffset(1);

           var A2 = etran2.TrExpr(e.E1);

           var B2 = etran2.TrExpr(e.E2);

-          foreach (var c in CoPrefixEquality(expr.tok, codecl, A2, B2, kMinusOne, 1 + etran.layerOffset)) {

-            splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, BplOr(prefixEqK, Bpl.Expr.Imp(kPos, c))));

+          var needsTokenAdjust = TrSplitNeedsTokenAdjustment(expr);

+          foreach (var c in CoPrefixEquality(needsTokenAdjust ? new ForceCheckToken(expr.tok) : expr.tok, codecl, A2, B2, kMinusOne, 1 + etran.layerOffset)) {

+            var p = Bpl.Expr.Binary(c.tok, BinaryOperator.Opcode.Or, prefixEqK, Bpl.Expr.Imp(kPos, c));

+            splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p));

           }

           splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, prefixEqK));

           return true;

@@ -9184,11 +9186,13 @@ namespace Microsoft.Dafny {
             // recurse on body

             var ss = new List<SplitExprInfo>();

             TrSplitExpr(body, ss, position, functionHeight, etran);

+            var needsTokenAdjust = TrSplitNeedsTokenAdjustment(body);

             foreach (var s in ss) {

               if (s.IsChecked) {

                 var unboxedConjunct = etran.CondApplyUnbox(s.E.tok, s.E, f.ResultType, expr.Type);

                 var bodyOrConjunct = Bpl.Expr.Or(fargs, unboxedConjunct);

-                var p = Bpl.Expr.Binary(new NestedToken(fexp.tok, s.E.tok), BinaryOperator.Opcode.Imp, canCall, bodyOrConjunct);

+                var tok = needsTokenAdjust ? (IToken)new ForceCheckToken(body.tok) : (IToken)new NestedToken(fexp.tok, s.E.tok);

+                var p = Bpl.Expr.Binary(tok, BinaryOperator.Opcode.Imp, canCall, bodyOrConjunct);

                 splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p));

               }

             }

@@ -9246,7 +9250,10 @@ namespace Microsoft.Dafny {
           //   (forall n :: n-has-expected-type && (forall k :: k < n ==> P(k)) && case0(n)   ==> P(n))

           //   (forall n :: n-has-expected-type && (forall k :: k < n ==> P(k)) && case...(n) ==> P(n))

           // or similar for existentials.

-          var caseProduct = new List<Bpl.Expr>() { new Bpl.LiteralExpr(expr.tok, true) };  // make sure to include the correct token information

+          var caseProduct = new List<Bpl.Expr>() {

+            // make sure to include the correct token information (so, don't just use Bpl.Expr.True here)

+            new Bpl.LiteralExpr(TrSplitNeedsTokenAdjustment(expr) ? new ForceCheckToken(expr.tok) : expr.tok, true)

+          };

           var i = 0;

           foreach (var n in inductionVariables) {

             var newCases = new List<Bpl.Expr>();

@@ -9279,6 +9286,26 @@ namespace Microsoft.Dafny {
           // Finally, assume the original quantifier (forall/exists n :: P(n))

           splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, etran.TrExpr(expr)));

           return true;

+

+        } else {

+          // Don't use induction on these quantifiers.

+          // Nevertheless, produce two translated versions of the quantifier, one that uses #2 functions (that is, layerOffset 1)

+          // for checking and one that uses #1 functions (that is, layerOffset 0) for assuming.

+          var etranBoost = etran.LayerOffset(1);

+          var r = etranBoost.TrExpr(expr);

+          var needsTokenAdjustment = TrSplitNeedsTokenAdjustment(expr);

+          if (needsTokenAdjustment) {

+            r.tok = new ForceCheckToken(expr.tok);

+          }

+          if (etranBoost.Statistics_CustomLayerFunctionCount == 0) {

+            // apparently, the LayerOffset(1) we did had no effect

+            splits.Add(new SplitExprInfo(SplitExprInfo.K.Both, r));

+            return needsTokenAdjustment;

+          } else {

+            splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, r));  // check the boosted expression

+            splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, etran.TrExpr(expr)));  // assume the ordinary expression

+            return true;

+          }

         }

       }

 

@@ -9292,19 +9319,19 @@ namespace Microsoft.Dafny {
         translatedExpression = etran.TrExpr(expr);

         splitHappened = etran.Statistics_CustomLayerFunctionCount != 0;  // return true if the LayerOffset(1) came into play

       }

-      // TODO: Is the the following call to ContainsChange expensive?  It's linear in the size of "expr", but we get here many times in TrSplitExpr, so wouldn't the total

-      // time in the size of the expression passed to the first TrSplitExpr be quadratic?

-      if (RefinementToken.IsInherited(expr.tok, currentModule) && (codeContext == null || !codeContext.MustReverify) && RefinementTransformer.ContainsChange(expr, currentModule)) {

-        // If "expr" contains a subexpression that has changed from the inherited expression, we'll destructively

-        // change the token of the translated expression to make it look like it's not inherited.  This will cause "e" to

-        // be verified again in the refining module.

+      if (TrSplitNeedsTokenAdjustment(expr)) {

         translatedExpression.tok = new ForceCheckToken(expr.tok);

-        splitHappened = true;  // count this as a split, so this translated expression is not ignored

+        splitHappened = true;

       }

       splits.Add(new SplitExprInfo(SplitExprInfo.K.Both, translatedExpression));

       return splitHappened;

     }

 

+    bool TrSplitNeedsTokenAdjustment(Expression expr) {

+      Contract.Requires(expr != null);

+      return RefinementToken.IsInherited(expr.tok, currentModule) && (codeContext == null || !codeContext.MustReverify) && RefinementTransformer.ContainsChange(expr, currentModule);

+    }

+

     List<BoundVar> ApplyInduction(QuantifierExpr e) {

       return ApplyInduction(e.BoundVars, e.Attributes, new List<Expression>() { e.LogicalBody() },

         delegate(System.IO.TextWriter wr) { new Printer(Console.Out).PrintExpression(e); });

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 85d8c977..e3e513a4 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1397,6 +1397,7 @@ Execution trace:
     (0,0): anon9_Then

     (0,0): anon10_Then

 CoPrefix.dfy(139,25): Error: assertion violation

+CoPrefix.dfy(114,23): Related location: Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon9_Then

@@ -1448,11 +1449,13 @@ Execution trace:
     (0,0): anon3_Then

 CoinductiveProofs.dfy(147,1): Error BP5003: A postcondition might not hold on this return path.

 CoinductiveProofs.dfy(146,22): Related location: This is the postcondition that might not hold.

+CoinductiveProofs.dfy(1,24): Related location: Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

 CoinductiveProofs.dfy(153,1): Error BP5003: A postcondition might not hold on this return path.

 CoinductiveProofs.dfy(152,22): Related location: This is the postcondition that might not hold.

+CoinductiveProofs.dfy(1,24): Related location: Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

@@ -1506,7 +1509,7 @@ EqualityTypes.dfy(82,8): Error: type parameter 0 (T) passed to method M must sup
 

 -------------------- SplitExpr.dfy --------------------

 

-Dafny program verifier finished with 5 verified, 0 errors

+Dafny program verifier finished with 8 verified, 0 errors

 

 -------------------- LoopModifies.dfy --------------------

 LoopModifies.dfy(6,5): Error: assignment may update an array element not in the enclosing context's modifies clause

diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy
index 19375ac2..1610d8b8 100644
--- a/Test/dafny0/Predicates.dfy
+++ b/Test/dafny0/Predicates.dfy
@@ -15,7 +15,7 @@ module A {
     method N()

       modifies this;

       ensures P();

-    {

+    {  // error: in module B, the postcondition P() has been strengthened and no longer holds

       x := -28;

     }

   }

@@ -36,7 +36,7 @@ module Loose {
   class MyNumber {

     var N: int;

     ghost var Repr: set<object>;

-    predicate Valid

+    predicate Valid()

       reads this, Repr;

     {

       this in Repr && null !in Repr &&

@@ -44,20 +44,20 @@ module Loose {
     }

     constructor Init()

       modifies this;

-      ensures Valid && fresh(Repr - {this});

+      ensures Valid() && fresh(Repr - {this});

     {

       N, Repr := 0, {this};

     }

     method Inc()

-      requires Valid;

+      requires Valid();

       modifies Repr;

       ensures old(N) < N;

-      ensures Valid && fresh(Repr - old(Repr));

+      ensures Valid() && fresh(Repr - old(Repr));

     {

       N := N + 2;

     }

     method Get() returns (n: int)

-      requires Valid;

+      requires Valid();

       ensures n == N;

     {

       n := N;

@@ -67,7 +67,7 @@ module Loose {
 

 module Tight refines Loose {

   class MyNumber {

-    predicate Valid

+    predicate Valid()

     {

       N % 2 == 0

     }

@@ -107,20 +107,20 @@ module AwareClient {
 module Tricky_Base {

   class Tree {

     var x: int;

-    predicate Constrained

+    predicate Constrained()

       reads this;

     {

       x < 10

     }

-    predicate Valid

+    predicate Valid()

       reads this;

     {

       x < 100

     }

     method Init()

       modifies this;

-      ensures Valid;

-    {

+      ensures Valid();

+    {  // error: in module Tricky_Full, the strengthened postcondition Valid() no longer holds

       x := 20;

     }

   }

@@ -128,7 +128,7 @@ module Tricky_Base {
 

 module Tricky_Full refines Tricky_Base {

   class Tree {

-    predicate Valid

+    predicate Valid()

     {

       Constrained  // this causes an error to be generated for the inherited Init

     }

@@ -140,43 +140,43 @@ module Tricky_Full refines Tricky_Base {
 module Q0 {

   class C {

     var x: int;

-    predicate P

+    predicate P()

       reads this;

     {

       true

     }

     method M()

       modifies this;

-      ensures forall c: C :: c != null ==> c.P;

-    {

+      ensures forall c: C :: c != null ==> c.P();

+    {  // error: in module Q1, the postcondition no longer holds

     }

-    predicate Q

+    predicate Q()

       reads this;

     {

       x < 100

     }

     method N()

       modifies this;

-      ensures forall c :: c == this ==> c.Q;

-    {

-      x := 102;  // error: fails to establish postcondition (but this error should not be repeated in Q1 below)

+      ensures forall c :: c == this ==> c.Q();

+    {  // error: fails to establish postcondition (but this error should not be repeated in Q1 below)

+      x := 102;

     }

-    predicate R reads this;  // a body-less predicate

+    predicate R() reads this;  // a body-less predicate

   }

 }

 

 module Q1 refines Q0 {

   class C {

-    predicate P

+    predicate P()

     {

       x == 18

     }

-    predicate R  // no body yet

+    predicate R()  // no body yet

   }

 }

 

 module Q2 refines Q1 {

   class C {

-    predicate R { x % 3 == 2 }  // finally, give it a body

+    predicate R() { x % 3 == 2 }  // finally, give it a body

   }

 }

diff --git a/Test/dafny0/SplitExpr.dfy b/Test/dafny0/SplitExpr.dfy
index 80b67c10..3e67db58 100644
--- a/Test/dafny0/SplitExpr.dfy
+++ b/Test/dafny0/SplitExpr.dfy
@@ -54,3 +54,22 @@ class Node<T> {
                         next.Valid())

   }

 }

+

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

+// The following examples requires that quantifiers are boosted (that is, #2) when checked

+// versus not boosted (#1) when assumed.

+

+function F(x: nat): int

+{

+  if x == 0 then 0 else 1 + F(x-1)

+}

+

+method M(N: nat)

+{

+  var i := 0;

+  while (i < N)

+    invariant forall x {:induction false} :: 0 <= x <= i ==> F(x) == x;

+  {

+    i := i + 1;

+  }

+}