Dafny: removed support for assigning to an array-range (that is, an assignment statement where the LHS has the form a[lo..hi])

3 files changed, 9 insertions, 77 deletions

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index 23477186..52a4578c 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -773,50 +773,8 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is AssignStmt) {

         AssignStmt s = (AssignStmt)stmt;

-        if (s.Lhs is SeqSelectExpr && !((SeqSelectExpr)s.Lhs).SelectOne) {

-          SeqSelectExpr sel = (SeqSelectExpr)s.Lhs;

-          if (!(s.Rhs is HavocRhs)) {

-            // Generate the following:

-            //   tmpArr = sel.Seq;

-            //   tmpLow = sel.E0;  // or 0 if sel.E0==null

-            //   tmpHigh = sel.Eq;  // or arr.Length if sel.E1==null

-            //   tmpRhs = s.Rhs;

-            //   for (int tmpI = tmpLow; tmpI < tmpHigh; tmpI++) {

-            //     tmpArr[tmpI] = tmpRhs;

-            //   }

-            string arr = "_arr" + tmpVarCount;

-            string low = "_low" + tmpVarCount;

-            string high = "_high" + tmpVarCount;

-            string rhs = "_rhs" + tmpVarCount;

-            string i = "_i" + tmpVarCount;

-            tmpVarCount++;

-            Indent(indent); wr.Write("{0} {1} = ", TypeName(cce.NonNull(sel.Seq.Type)), arr); TrExpr(sel.Seq); wr.WriteLine(";");

-            Indent(indent); wr.Write("int {0} = ", low);

-            if (sel.E0 == null) {

-              wr.Write("0");

-            } else {

-              TrExpr(sel.E0);

-            }

-            wr.WriteLine(";");

-            Indent(indent); wr.Write("int {0} = ", high);

-            if (sel.E1 == null) {

-              wr.Write("new BigInteger(arr.Length)");

-            } else {

-              TrExpr(sel.E1);

-            }

-            wr.WriteLine(";");

-            Indent(indent); wr.Write("{0} {1} = ", TypeName(cce.NonNull(sel.Type)), rhs); TrAssignmentRhs(s.Rhs); wr.WriteLine(";");

-            Indent(indent);

-            wr.WriteLine("for (BigInteger {0} = {1}; {0} < {2}; {0}++) {{", i, low, high);

-            Indent(indent + IndentAmount);

-            wr.WriteLine("{0}[(int)({1})] = {2};", arr, i, rhs);

-            Indent(indent);

-            wr.WriteLine(";");

-          }

-

-        } else {

-          TrRhs(null, s.Lhs, s.Rhs, indent);

-        }

+        Contract.Assert(!(s.Lhs is SeqSelectExpr) || ((SeqSelectExpr)s.Lhs).SelectOne);  // multi-element array assignments are not allowed

+        TrRhs(null, s.Lhs, s.Rhs, indent);

 

       } else if (stmt is VarDecl) {

         TrVarDecl((VarDecl)stmt, true, indent);

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 43c72000..e053f212 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -1259,7 +1259,7 @@ namespace Microsoft.Dafny {
         AssignStmt s = (AssignStmt)stmt;

         int prevErrorCount = ErrorCount;

         if (s.Lhs is SeqSelectExpr) {

-          ResolveSeqSelectExpr((SeqSelectExpr)s.Lhs, true, true);  // allow ghosts for now, tighted up below

+          ResolveSeqSelectExpr((SeqSelectExpr)s.Lhs, true, false);  // allow ghosts for now, tighted up below

         } else {

           ResolveExpression(s.Lhs, true);  // allow ghosts for now, tighted up below

         }

@@ -1312,7 +1312,7 @@ namespace Microsoft.Dafny {
               Error(stmt, "Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");

             }

             if (!slhs.SelectOne) {

-              Error(stmt, "cannot assign to multiple array elements (try a foreach).");

+              Error(stmt, "cannot assign to a range of array elements (try the 'parallel' statement)");

             }

           }

 

@@ -1328,7 +1328,7 @@ namespace Microsoft.Dafny {
         s.IsGhost = lvalueIsGhost;

         Type lhsType = s.Lhs.Type;

         if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) {

-          Error(stmt, "cannot assign to multiple array elements (try a foreach).");

+          Error(stmt, "cannot assign to a range of array elements (try the 'parallel' statement)");

           //lhsType = UserDefinedType.ArrayElementType(lhsType);

         } else {

           if (s.Rhs is ExprRhs) {

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index ab6e2435..9e28a6ec 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -3118,33 +3118,7 @@ namespace Microsoft.Dafny {
       } else if (stmt is AssignStmt) {

         AddComment(builder, stmt, "assignment statement");

         AssignStmt s = (AssignStmt)stmt;

-        var sel = s.Lhs.Resolved as SeqSelectExpr;

-        if (sel != null && !sel.SelectOne) {

-          // check LHS for definedness

-          TrStmt_CheckWellformed(sel, builder, locals, etran, true);

-          // array-range assignment

-          var obj = etran.TrExpr(sel.Seq);

-          Bpl.Expr low = sel.E0 == null ? Bpl.Expr.Literal(0) : etran.TrExpr(sel.E0);

-          Bpl.Expr high = sel.E1 == null ? ArrayLength(s.Tok, obj, 1, 0) : etran.TrExpr(sel.E1);

-          // check frame:

-          // assert (forall i: int :: low <= i && i < high ==> $_Frame[arr,i]);

-          Bpl.Variable iVar = new Bpl.BoundVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$i", Bpl.Type.Int));

-          Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(s.Tok, iVar);

-          Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Le(low, ie), Bpl.Expr.Lt(ie, high));

-          Bpl.Expr fieldName = FunctionCall(s.Tok, BuiltinFunction.IndexField, null, ie);

-          Bpl.Expr cons = Bpl.Expr.SelectTok(s.Tok, etran.TheFrame(s.Tok), obj, fieldName);

-          Bpl.Expr q = new Bpl.ForallExpr(s.Tok, new Bpl.VariableSeq(iVar), Bpl.Expr.Imp(ante, cons));

-          builder.Add(Assert(s.Tok, q, "assignment may update an array element not in the enclosing method's modifies clause"));

-          // compute the RHS

-          Bpl.Expr bRhs = TrAssignmentRhs(s.Tok, null, null, s.Rhs, sel.Type, builder, locals, etran);

-          // do the update:  call UpdateArrayRange(arr, low, high, rhs);

-          builder.Add(new Bpl.CallCmd(s.Tok, "UpdateArrayRange",

-            new Bpl.ExprSeq(obj, low, high, bRhs),

-            new Bpl.IdentifierExprSeq()));

-          builder.Add(CaptureState(s.Tok));

-        } else {

-          TrAssignment(stmt.Tok, s.Lhs.Resolved, s.Rhs, builder, locals, etran);

-        }

+        TrAssignment(stmt.Tok, s.Lhs.Resolved, s.Rhs, builder, locals, etran);

       } else if (stmt is VarDecl) {

         AddComment(builder, stmt, "var-declaration statement");

         VarDecl s = (VarDecl)stmt;

@@ -4556,7 +4530,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(tok != null);

       Contract.Requires(lhs != null);

       Contract.Requires(!(lhs is ConcreteSyntaxExpression));

-      Contract.Requires(!(lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne));  // array-range assignments are handled elsewhere

+      Contract.Requires(!(lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne));  // these were once allowed, but their functionality is now provided by 'parallel' statements

       Contract.Requires(rhs != null);

       Contract.Requires(builder != null);

       Contract.Requires(cce.NonNullElements(locals));

@@ -4592,7 +4566,7 @@ namespace Microsoft.Dafny {
         var lhs = lhss[i];

         // the following assumes are part of the precondition, really

         Contract.Assume(!(lhs is ConcreteSyntaxExpression));

-        Contract.Assume(!(lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne));  // array-range assignments are handled elsewhere

+        Contract.Assume(!(lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne));  // array-range assignments are not allowed

 

         Type lhsType = null;

         if (lhs is IdentifierExpr) {

@@ -4684,7 +4658,7 @@ namespace Microsoft.Dafny {
 

         } else if (lhs is SeqSelectExpr) {

           SeqSelectExpr sel = (SeqSelectExpr)lhs;

-          Contract.Assert(sel.SelectOne);  // array-range assignments are handled elsewhere, see precondition

+          Contract.Assert(sel.SelectOne);  // array-range assignments are not allowed

           Contract.Assert(sel.Seq.Type != null && sel.Seq.Type.IsArrayType);

           Contract.Assert(sel.E0 != null);

           var obj = SaveInTemp(etran.TrExpr(sel.Seq), rhsCanAffectPreviouslyKnownExpressions,