Dafny: fixed bug in reads checking of array-to-sequence conversions

3 files changed, 121 insertions, 25 deletions

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 28146a7f..2cc15c5a 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -2074,16 +2074,30 @@ namespace Microsoft.Dafny {
         if (e.E0 != null) {

           e0 = etran.TrExpr(e.E0);

           CheckWellformed(e.E0, options, locals, builder, etran);

-          builder.Add(Assert(expr.tok, InSeqRange(expr.tok, e0, seq, isSequence, null, !e.SelectOne), "index out of range", options.AssertKv));

+          builder.Add(Assert(expr.tok, InSeqRange(expr.tok, e0, seq, isSequence, null, !e.SelectOne), e.SelectOne ? "index out of range" : "lower bound out of range", options.AssertKv));

         }

         if (e.E1 != null) {

           CheckWellformed(e.E1, options, locals, builder, etran);

-          builder.Add(Assert(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true), "end-of-range beyond length of " + (isSequence ? "sequence" : "array"), options.AssertKv));

+          builder.Add(Assert(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true), "upper bound " + (e.E0 == null ? "" : "below lower bound or ") + "above length of " + (isSequence ? "sequence" : "array"), options.AssertKv));

         }

         if (options.DoReadsChecks && cce.NonNull(e.Seq.Type).IsArrayType) {

-          Contract.Assert(e.E0 != null);

-          Bpl.Expr fieldName = FunctionCall(expr.tok, BuiltinFunction.IndexField, null, etran.TrExpr(e.E0));

-          builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), seq, fieldName), "insufficient reads clause to read array element", options.AssertKv));

+          if (e.SelectOne) {

+            Contract.Assert(e.E0 != null);

+            Bpl.Expr fieldName = FunctionCall(expr.tok, BuiltinFunction.IndexField, null, etran.TrExpr(e.E0));

+            builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), seq, fieldName), "insufficient reads clause to read array element", options.AssertKv));

+          } else {

+            Bpl.Expr lowerBound = e.E0 == null ? Bpl.Expr.Literal(0) : etran.TrExpr(e.E0);

+            Contract.Assert((e.Seq.Type).AsArrayType.Dims == 1);

+            Bpl.Expr upperBound = e.E1 == null ? ArrayLength(e.tok, seq, 1, 0) : etran.TrExpr(e.E1);

+            // check that, for all i in lowerBound..upperBound, a[i] is in the frame

+            Bpl.BoundVariable iVar = new Bpl.BoundVariable(e.tok, new Bpl.TypedIdent(e.tok, "$i", Bpl.Type.Int));

+            Bpl.IdentifierExpr i = new Bpl.IdentifierExpr(e.tok, iVar);

+            var range = BplAnd(Bpl.Expr.Le(lowerBound, i), Bpl.Expr.Lt(i, upperBound));

+            var fieldName = FunctionCall(e.tok, BuiltinFunction.IndexField, null, i);

+            var allowedToRead = Bpl.Expr.SelectTok(e.tok, etran.TheFrame(e.tok), seq, fieldName);

+            var qq = new Bpl.ForallExpr(e.tok, new Bpl.VariableSeq(iVar), Bpl.Expr.Imp(range, allowedToRead));

+            builder.Add(Assert(expr.tok, qq, "insufficient reads clause to read the indicated range of array elements", options.AssertKv));

+          }

         }

       } else if (expr is MultiSelectExpr) {

         MultiSelectExpr e = (MultiSelectExpr)expr;

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index b2914776..bdbb8822 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -522,48 +522,80 @@ Execution trace:
     (0,0): anon5_Then

     (0,0): anon2

     (0,0): anon6_Then

-Array.dfy(97,6): Error: insufficient reads clause to read array element

+Array.dfy(107,21): Error: upper bound below lower bound or above length of array

+Execution trace:

+    (0,0): anon0

+    (0,0): anon14_Else

+    (0,0): anon18_Then

+    (0,0): anon19_Then

+    (0,0): anon20_Then

+    (0,0): anon11

+Array.dfy(117,8): Error: insufficient reads clause to read the indicated range of array elements

+Execution trace:

+    (0,0): anon9_Else

+    (0,0): anon10_Then

+    (0,0): anon11_Then

+    (0,0): anon12_Then

+Array.dfy(119,8): Error: insufficient reads clause to read the indicated range of array elements

+Execution trace:

+    (0,0): anon9_Else

+    (0,0): anon10_Then

+    (0,0): anon11_Then

+    (0,0): anon12_Else

+Array.dfy(120,8): Error: insufficient reads clause to read the indicated range of array elements

+Execution trace:

+    (0,0): anon9_Else

+    (0,0): anon10_Then

+    (0,0): anon11_Then

+    (0,0): anon12_Else

+Array.dfy(121,8): Error: insufficient reads clause to read the indicated range of array elements

+Execution trace:

+    (0,0): anon9_Else

+    (0,0): anon10_Then

+    (0,0): anon11_Then

+    (0,0): anon12_Else

+Array.dfy(147,6): Error: insufficient reads clause to read array element

 Execution trace:

     (0,0): anon7_Else

     (0,0): anon8_Then

     (0,0): anon9_Then

-Array.dfy(105,6): Error: insufficient reads clause to read array element

+Array.dfy(155,6): Error: insufficient reads clause to read array element

 Execution trace:

     (0,0): anon7_Else

     (0,0): anon8_Then

     (0,0): anon9_Then

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

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

 Execution trace:

     (0,0): anon0

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

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

 Execution trace:

     (0,0): anon0

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

-Array.dfy(152,11): Related location: This is the postcondition that might not hold.

+Array.dfy(203,1): Error BP5003: A postcondition might not hold on this return path.

+Array.dfy(202,11): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-Array.dfy(177,1): Error BP5003: A postcondition might not hold on this return path.

-Array.dfy(176,11): Related location: This is the postcondition that might not hold.

+Array.dfy(227,1): Error BP5003: A postcondition might not hold on this return path.

+Array.dfy(226,11): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-Array.dfy(183,1): Error BP5003: A postcondition might not hold on this return path.

-Array.dfy(182,11): Related location: This is the postcondition that might not hold.

+Array.dfy(233,1): Error BP5003: A postcondition might not hold on this return path.

+Array.dfy(232,11): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-Array.dfy(198,10): Error: value assigned to a nat must be non-negative

+Array.dfy(248,10): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

     (0,0): anon2

     (0,0): anon6_Then

-Array.dfy(199,5): Error: value assigned to a nat must be non-negative

+Array.dfy(249,5): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

     (0,0): anon2

     (0,0): anon6_Then

 

-Dafny program verifier finished with 31 verified, 15 errors

+Dafny program verifier finished with 34 verified, 20 errors

 

 -------------------- MultiDimArray.dfy --------------------

 MultiDimArray.dfy(53,21): Error: assertion violation

diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy
index 613cdd83..17500c97 100644
--- a/Test/dafny0/Array.dfy
+++ b/Test/dafny0/Array.dfy
@@ -74,16 +74,66 @@ class A {
   method Q() {

     var a := new int[5];

     a[0],a[1],a[2],a[3],a[4] := 0,1,2,3,4;

-	

-	assert [1,2,3,4] == a[1..];

-	assert [1,2,3,4] == a[1.. a.Length];

-	assert [1] == a[1..2];

-	assert [0,1] == a[..2];

-	assert [0,1] == a[0..2];

-	assert forall i :: 0 <= i <= a.Length ==> [] == a[i..i];

+

+    assert [1,2,3,4] == a[1..];

+    assert [1,2,3,4] == a[1.. a.Length];

+    assert [1] == a[1..2];

+    assert [0,1] == a[..2];

+    assert [0,1] == a[0..2];

+    assert forall i :: 0 <= i <= a.Length ==> [] == a[i..i];

     assert [0,1,2,3,4] == a[..];

     assert forall i :: 0 <= i < a.Length ==> a[i] == i;

   }

+

+  method ArrayToSequenceTests(a: array<int>, lo: int, hi: int)

+    requires a != null;

+  {

+    if (a.Length == 10) {

+      var s;

+      s := a[2..5];

+      assert |s| == 3;

+      s := a[..5];

+      assert |s| == 5;

+      s := a[2..];

+      assert |s| == 8;

+      s := a[..];

+      assert |s| == 10;

+      s := a[..10] + a[0..];

+    } else {

+      if {

+        case 0 <= lo <= a.Length =>

+          var s := a[lo..] + a[..lo];

+        case 0 <= lo <= a.Length && 0 <= hi <= a.Length =>

+          var s := a[lo..hi];  // error: lo may be greater than hi

+        case true =>

+      }

+    }

+  }

+

+  function BadRangeReads(a: array<int>, all: bool): bool

+  {

+    a != null && a.Length == 10 &&

+    if all then

+      a[..] == []  // error: not allowed to read the elements of a

+    else

+      a[2..5] +       // error: not allowed to read the elements of a

+      a[..5] +        // error: not allowed to read the elements of a

+      a[2..] == []    // error: not allowed to read the elements of a

+  }

+  function GoodRangeReads(a: array<int>, all: bool): bool

+    reads a;

+  {

+    a != null && a.Length == 10 &&

+    if all then

+      a[..] == []  // no prob, since we now have a reads clause

+    else

+      a[2..5] + a[..5] + a[2..] == []  // no prob, since we now have a reads clause

+  }

+  function AnotherGoodRangeReads(a: array<int>, j: int): bool

+  {

+    a != null && 0 <= j && j <= a.Length &&

+    a[j..j] == []

+  }

 }

 

 class B { }