Fix: multi-dimensional OOB errors were sometimes reported on incorrect locations.

3 files changed, 34 insertions, 8 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 524466c9..09ca32e0 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -4885,16 +4885,17 @@ namespace Microsoft.Dafny {
         MultiSelectExpr e = (MultiSelectExpr)expr;

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

         Bpl.Expr array = etran.TrExpr(e.Array);

-        int i = 0;

-        foreach (Expression idx in e.Indices) {

+        for (int idxId = 0; idxId < e.Indices.Count; idxId++) {

+          var idx = e.Indices[idxId];

           CheckWellformed(idx, options, locals, builder, etran);

 

-          Bpl.Expr index = etran.TrExpr(idx);

-          Bpl.Expr lower = Bpl.Expr.Le(Bpl.Expr.Literal(0), index);

-          Bpl.Expr length = ArrayLength(idx.tok, array, e.Indices.Count, i);

-          Bpl.Expr upper = Bpl.Expr.Lt(index, length);

-          builder.Add(Assert(idx.tok, Bpl.Expr.And(lower, upper), "index " + i + " out of range", options.AssertKv));

-          i++;

+          var index = etran.TrExpr(idx);

+          var lower = Bpl.Expr.Le(Bpl.Expr.Literal(0), index);

+          var length = ArrayLength(idx.tok, array, e.Indices.Count, idxId);

+          var upper = Bpl.Expr.Lt(index, length);

+          var tok = idx is IdentifierExpr ? e.tok : idx.tok; // TODO: Reusing the token of an identifier expression would underline its definition. but this is still not perfect.

+

+          builder.Add(Assert(tok, Bpl.Expr.And(lower, upper), String.Format("index {0} out of range", idxId), options.AssertKv));

         }

       } else if (expr is SeqUpdateExpr) {

         SeqUpdateExpr e = (SeqUpdateExpr)expr;

diff --git a/Test/dafny0/Matrix-OOB.dfy b/Test/dafny0/Matrix-OOB.dfy
new file mode 100644
index 00000000..2e5c0366
--- /dev/null
+++ b/Test/dafny0/Matrix-OOB.dfy
@@ -0,0 +1,13 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /printTooltips "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This is a regression test: OOB errors for matrices used to be reported on the

+// quantifier that introduced the variables that constituted the invalid indices.

+

+// WISH: It would be even better to report the error on the variables inside the

+// array instead of the array itself.

+

+method M(m: array2<int>)

+  requires m != null

+  ensures forall i, j :: m[i, j] == 0

+{ }

diff --git a/Test/dafny0/Matrix-OOB.dfy.expect b/Test/dafny0/Matrix-OOB.dfy.expect
new file mode 100644
index 00000000..94e77aa4
--- /dev/null
+++ b/Test/dafny0/Matrix-OOB.dfy.expect
@@ -0,0 +1,12 @@
+Matrix-OOB.dfy(12,26): Error: index 0 out of range

+Execution trace:

+    (0,0): anon0

+Matrix-OOB.dfy(12,26): Error: index 1 out of range

+Execution trace:

+    (0,0): anon0

+Matrix-OOB.dfy(13,0): Error BP5003: A postcondition might not hold on this return path.

+Matrix-OOB.dfy(12,10): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 0 verified, 3 errors