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

6 files changed, 37 insertions, 96 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 32430fd3..1fe21204 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -489,13 +489,6 @@ axiom (forall r: ref, h: HeapType ::
 function array.Length(a: ref): int;

 axiom (forall o: ref :: 0 <= array.Length(o));

 

-procedure UpdateArrayRange(arr: ref, low: int, high: int, rhs: BoxType);

-  modifies $Heap;

-  ensures $HeapSucc(old($Heap), $Heap);

-  ensures (forall i: int :: { read($Heap, arr, IndexField(i)) } low <= i && i < high ==> read($Heap, arr, IndexField(i)) == rhs);

-  ensures (forall<alpha> o: ref, f: Field alpha :: { read($Heap, o, f) } read($Heap, o, f) == read(old($Heap), o, f) ||

-            (o == arr && FDim(f) == 1 && low <= IndexField_Inverse(f) && IndexField_Inverse(f) < high));

-

 // ---------------------------------------------------------------

 // -- The heap ---------------------------------------------------

 // ---------------------------------------------------------------

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 23477186..52a4578c 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/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/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 43c72000..e053f212 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/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/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index ab6e2435..9e28a6ec 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/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,

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 4745ae48..697bdd9e 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -58,7 +58,7 @@ class C {
 Dafny program verifier finished with 0 verified, 0 errors

 

 -------------------- TypeTests.dfy --------------------

-TypeTests.dfy(84,9): Error: sorry, cannot instantiate collection type with a subrange type

+TypeTests.dfy(89,9): Error: sorry, cannot instantiate collection type with a subrange type

 TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)

 TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)

 TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)

@@ -74,14 +74,25 @@ TypeTests.dfy(58,8): Error: Duplicate local-variable name: x
 TypeTests.dfy(61,6): Error: Duplicate local-variable name: y

 TypeTests.dfy(68,17): Error: member F in type C does not refer to a method

 TypeTests.dfy(69,17): Error: a method called as an initialization method must not have any result arguments

-TypeTests.dfy(78,10): Error: cannot assign to multiple array elements (try a foreach).

-TypeTests.dfy(78,10): Error: cannot assign to multiple array elements (try a foreach).

-TypeTests.dfy(79,10): Error: cannot assign to multiple array elements (try a foreach).

-TypeTests.dfy(79,10): Error: cannot assign to multiple array elements (try a foreach).

-TypeTests.dfy(85,9): Error: sorry, cannot instantiate type parameter with a subrange type

-TypeTests.dfy(86,8): Error: sorry, cannot instantiate 'array' type with a subrange type

-TypeTests.dfy(87,8): Error: sorry, cannot instantiate 'array' type with a subrange type

-23 resolution/type errors detected in TypeTests.dfy

+TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

+TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

+TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

+TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

+TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

+TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

+TypeTests.dfy(82,2): Error: LHS of array assignment must denote an array element (found seq<C>)

+TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

+TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

+TypeTests.dfy(83,2): Error: LHS of array assignment must denote an array element (found seq<C>)

+TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

+TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

+TypeTests.dfy(84,2): Error: LHS of array assignment must denote an array element (found seq<C>)

+TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

+TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

+TypeTests.dfy(90,9): Error: sorry, cannot instantiate type parameter with a subrange type

+TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type

+TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type

+34 resolution/type errors detected in TypeTests.dfy

 

 -------------------- NatTypes.dfy --------------------

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

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 2208051d..29274381 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -72,11 +72,16 @@ method InitCalls() {
 

 // ---------------------

 

-method ArrayRangeAssignments(a: array<C>)

+method ArrayRangeAssignments(a: array<C>, c: C)

   requires a != null && 10 <= a.Length;

 {

-  a[0..5] := new C;  // this is not allowed

-  a[1..4] := *;  // this is not allowed

+  a[0..5] := new C;  // error: this is not allowed

+  a[1..4] := *;  // error: this is not allowed

+  a[2..3] := c;  // error: this is not allowed

+  var s: seq<C> := [null,null,null,null,null];

+  s[0..5] := new C;  // error: this is not allowed

+  s[1..4] := *;  // error: this is not allowed

+  s[2..3] := c;  // error: this is not allowed

 }

 

 // --------------------- tests of restrictions on subranges (nat)