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

1 files changed, 19 insertions, 5 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;