Allow assignment LHSs in a forall statement to be the same, so long as the they are assigned the same RHS value.

Don't include havoc assignments in LHS-duplicate checks.

4 files changed, 141 insertions, 31 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index f9cd899f..818bdcc4 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -5111,6 +5111,7 @@ namespace Microsoft.Dafny
       var update = s as UpdateStmt;

 

       var lhsNameSet = new HashSet<string>();  // used to check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification)

+      var i = 0;

       foreach (var lhs in s.Lhss) {

         var ec = ErrorCount;

         ResolveExpression(lhs, new ResolveOpts(codeContext, true));

@@ -5121,14 +5122,6 @@ namespace Microsoft.Dafny
           if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) {

             Error(lhs, "cannot assign to a range of array elements (try the 'forall' statement)");

           }

-          var ie = lhs.Resolved as IdentifierExpr;

-          if (ie != null) {

-            if (lhsNameSet.Contains(ie.Name)) {

-              Error(update, "duplicate variable in left-hand side of call statement: {0}", ie.Name);

-            } else {

-              lhsNameSet.Add(ie.Name);

-            }

-          }

         }

       }

 

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 76da73cd..0a83499c 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -6964,7 +6964,7 @@ namespace Microsoft.Dafny {
           // ProcessLhss has laid down framing conditions and the ProcessUpdateAssignRhss will check subranges (nats),

           // but we need to generate the distinctness condition (two LHS are equal only when the RHS is also

           // equal). We need both the LHS and the RHS to do this, which is why we need to do it here.

-          CheckLhssDistinctness(finalRhss, lhss, builder, etran, lhsObjs, lhsFields, lhsNames);

+          CheckLhssDistinctness(finalRhss, s.Rhss, lhss, builder, etran, lhsObjs, lhsFields, lhsNames);

           // Now actually perform the assignments to the LHS.

           for (int i = 0; i < lhss.Count; i++) {

             lhsBuilder[i](finalRhss[i], builder, etran);

@@ -7491,9 +7491,9 @@ namespace Microsoft.Dafny {
       //     assume Range[x,y := x',y'];

       //     assume !(x == x' && y == y');

       //     (a)

-      //       assert E(x,y) != E(x',y');

+      //       assert E(x,y) != E(x',y') || G(x,y) == G(x',y');

       //     (b)

-      //       assert !( A(x,y)==A(x',y') && I0(x,y)==I0(x',y') && I1(x,y)==I1(x',y') && ... );

+      //       assert !( A(x,y)==A(x',y') && I0(x,y)==I0(x',y') && I1(x,y)==I1(x',y') && ... ) || G(x,y) == G(x',y');

       //

       //     assume false;

       //

@@ -7566,24 +7566,31 @@ namespace Microsoft.Dafny {
       }

 

       // check for duplicate LHSs

-      var substMapPrime = SetupBoundVarsAsLocals(s.BoundVars, definedness, locals, etran);

-      var lhsPrime = Substitute(s0.Lhs.Resolved, null, substMapPrime);

-      range = Substitute(s.Range, null, substMapPrime);

-      definedness.Add(new Bpl.AssumeCmd(range.tok, etran.TrExpr(range)));

-      // assume !(x == x' && y == y');

-      Bpl.Expr eqs = Bpl.Expr.True;

-      foreach (var bv in s.BoundVars) {

-        var x = substMap[bv];

-        var xPrime = substMapPrime[bv];

-        // TODO: in the following line, is the term equality okay, or does it have to include things like Set#Equal sometimes too?

-        eqs = BplAnd(eqs, Bpl.Expr.Eq(etran.TrExpr(x), etran.TrExpr(xPrime)));

-      }

-      definedness.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.Not(eqs)));

-      Bpl.Expr objPrime, FPrime;

-      GetObjFieldDetails(lhsPrime, etran, out objPrime, out FPrime);

-      definedness.Add(Assert(s0.Tok,

-        Bpl.Expr.Or(Bpl.Expr.Neq(obj, objPrime), Bpl.Expr.Neq(F, FPrime)),

-        "left-hand sides for different forall-statement bound variables may refer to the same location"));

+      if (s0.Rhs is ExprRhs) {  // if Rhs denotes a havoc, then no duplicate check is performed

+        var substMapPrime = SetupBoundVarsAsLocals(s.BoundVars, definedness, locals, etran);

+        var lhsPrime = Substitute(s0.Lhs.Resolved, null, substMapPrime);

+        range = Substitute(s.Range, null, substMapPrime);

+        definedness.Add(new Bpl.AssumeCmd(range.tok, etran.TrExpr(range)));

+        // assume !(x == x' && y == y');

+        Bpl.Expr eqs = Bpl.Expr.True;

+        foreach (var bv in s.BoundVars) {

+          var x = substMap[bv];

+          var xPrime = substMapPrime[bv];

+          // TODO: in the following line, is the term equality okay, or does it have to include things like Set#Equal sometimes too?

+          eqs = BplAnd(eqs, Bpl.Expr.Eq(etran.TrExpr(x), etran.TrExpr(xPrime)));

+        }

+        definedness.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.Not(eqs)));

+        Bpl.Expr objPrime, FPrime;

+        GetObjFieldDetails(lhsPrime, etran, out objPrime, out FPrime);

+        var Rhs = ((ExprRhs)s0.Rhs).Expr;

+        var rhs = etran.TrExpr(Substitute(Rhs, null, substMap));

+        var rhsPrime = etran.TrExpr(Substitute(Rhs, null, substMapPrime));

+        definedness.Add(Assert(s0.Tok,

+          Bpl.Expr.Or(

+            Bpl.Expr.Or(Bpl.Expr.Neq(obj, objPrime), Bpl.Expr.Neq(F, FPrime)),

+            Bpl.Expr.Eq(rhs, rhsPrime)),

+          "left-hand sides for different forall-statement bound variables may refer to the same location"));

+      }

 

       definedness.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));

 

@@ -9230,9 +9237,14 @@ namespace Microsoft.Dafny {
     }

 

 

-    private void CheckLhssDistinctness(List<Bpl.IdentifierExpr> rhs, List<Expression> lhss, StmtListBuilder builder, ExpressionTranslator etran,

+    private void CheckLhssDistinctness(List<Bpl.IdentifierExpr> rhs, List<AssignmentRhs> rhsOriginal, List<Expression> lhss,

+      StmtListBuilder builder, ExpressionTranslator etran,

       Bpl.Expr[] objs, Bpl.Expr[] fields, string[] names) {

-      Contract.Requires(cce.NonNullElements(lhss));

+      Contract.Requires(rhs != null);

+      Contract.Requires(rhsOriginal != null);

+      Contract.Requires(lhss != null);

+      Contract.Requires(rhs.Count == rhsOriginal.Count);

+      Contract.Requires(lhss.Count == rhsOriginal.Count);

       Contract.Requires(builder != null);

       Contract.Requires(etran != null);

       Contract.Requires(predef != null);

@@ -9240,10 +9252,14 @@ namespace Microsoft.Dafny {
       for (int i = 0; i < lhss.Count; i++) {

         var lhs = lhss[i];

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

+        if (rhsOriginal[i] is HavocRhs) {

+          continue;

+        }

         IToken tok = lhs.tok;

 

         if (lhs is IdentifierExpr) {

           for (int j = 0; j < i; j++) {

+            if (rhsOriginal[j] is HavocRhs) { continue; }

             var prev = lhss[j] as IdentifierExpr;

             if (prev != null && names[i] == names[j]) {

               builder.Add(Assert(tok, Bpl.Expr.Imp(Bpl.Expr.True, Bpl.Expr.Eq(rhs[i], rhs[j])), string.Format("when left-hand sides {0} and {1} refer to the same location, they must be assigned the same value", j, i)));

@@ -9253,6 +9269,7 @@ namespace Microsoft.Dafny {
           var fse = (MemberSelectExpr)lhs;

           // check that this LHS is not the same as any previous LHSs

           for (int j = 0; j < i; j++) {

+            if (rhsOriginal[j] is HavocRhs) { continue; }

             var prev = lhss[j] as MemberSelectExpr;

             var field = fse.Member as Field;

             Contract.Assert(field != null);

@@ -9265,6 +9282,7 @@ namespace Microsoft.Dafny {
           SeqSelectExpr sel = (SeqSelectExpr)lhs;

           // check that this LHS is not the same as any previous LHSs

           for (int j = 0; j < i; j++) {

+            if (rhsOriginal[j] is HavocRhs) { continue; }

             var prev = lhss[j] as SeqSelectExpr;

             if (prev != null) {

               builder.Add(Assert(tok,

@@ -9276,6 +9294,7 @@ namespace Microsoft.Dafny {
           MultiSelectExpr mse = (MultiSelectExpr)lhs;

           // check that this LHS is not the same as any previous LHSs

           for (int j = 0; j < i; j++) {

+            if (rhsOriginal[j] is HavocRhs) { continue; }

             var prev = lhss[j] as MultiSelectExpr;

             if (prev != null) {

               builder.Add(Assert(tok,

diff --git a/Test/dafny0/LhsDuplicates.dfy b/Test/dafny0/LhsDuplicates.dfy
new file mode 100644
index 00000000..6a84c5a5
--- /dev/null
+++ b/Test/dafny0/LhsDuplicates.dfy
@@ -0,0 +1,70 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

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

+

+class MyClass<T> {

+  var f: T;

+}

+

+method M<T>()

+{

+  var a, b := new T[100], new T[100];

+  forall i | 0 <= i < 100 {

+    a[3] := *;  // RHS is * -- this is okay

+  }

+  forall i | 0 <= i < 100 {

+    a[0] := b[0];  // RHSs are the same -- this is okay

+  }

+  forall i | 0 <= i < 100 {

+    a[0] := b[i];  // error: LHS's may be the same (while RHSs are different)

+  }

+}

+

+method N<T>(a: MyClass<T>, b: MyClass<T>)

+  requires a != null && b != null;

+  modifies a, b;

+{

+  var q := [a, b];

+  forall i | 0 <= i < 2 {

+    q[0].f := *;  // RHS is * -- this is okay

+  }

+  forall i | 0 <= i < 2 {

+    q[0].f := q[0].f;  // RHSs are the same -- this is okay

+  }

+  forall i | 0 <= i < 2 {

+    q[0].f := q[i].f;  // error: LHS's may be the same (while RHSs are different)

+  }

+}

+

+method P<T>(t0: T, t1: T, t2: T) {

+  var a: T, b: T;

+  a, a, a := *, t0, *;  // only one non-* RHS per variable -- this is okay

+  a, a, b, a, b := *, t1, t2, *, *;  // only one non-* RHS per variable -- this is okay

+  a, a, b, a, b := *, t1, t2, t0, *;  // error: duplicate LHS -- t0 and t1 may be different

+}

+

+method Q<T>(c0: MyClass<T>, c1: MyClass<T>)

+  requires c0 != null && c1 != null;

+  modifies c0, c1;

+{

+  c0.f, c1.f := c0.f, c0.f;  // okay -- RHSs are the same

+  c0.f, c0.f, c0.f, c0.f := *, *, c1.f, *;  // okay -- only one RHS is non-*

+  c0.f, c0.f, c0.f, c0.f := c0.f, *, c1.f, *;  // error -- duplicate LHR

+}

+

+method R<T>(i: nat, j: nat)

+  requires i < 10 && j < 10;

+{

+  var a := new T[10];

+  a[i], a[j] := a[5], a[5];  // okay -- RHSs are the same

+  a[i], a[i], a[i], a[i] := *, *, a[5], *;  // okay -- only one RHS is non-*

+  a[i], a[i], a[i], a[j] := *, a[i], a[j], a[i];  // error -- possible duplicate LHS

+}

+

+method S<T>(i: nat, j: nat)

+  requires i < 10 && j < 20;

+{

+  var a := new T[10,20];

+  a[i,j], a[i,i] := a[5,7], a[5,7];  // okay -- RHSs are the same

+  a[i,j], a[i,j], a[i,j], a[i,j] := *, *, a[5,7], *;  // okay -- only one RHS is non-*

+  a[i,j], a[i,j], a[i,j], a[i,i] := *, a[i,i], a[i,j], a[i,i];  // error -- possible duplicate LHS

+}

diff --git a/Test/dafny0/LhsDuplicates.dfy.expect b/Test/dafny0/LhsDuplicates.dfy.expect
new file mode 100644
index 00000000..a864390f
--- /dev/null
+++ b/Test/dafny0/LhsDuplicates.dfy.expect
@@ -0,0 +1,28 @@
+LhsDuplicates.dfy(18,10): Error: left-hand sides for different forall-statement bound variables may refer to the same location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon16_Else

+    (0,0): anon18_Else

+    (0,0): anon21_Then

+    (0,0): anon13

+LhsDuplicates.dfy(34,12): Error: left-hand sides for different forall-statement bound variables may refer to the same location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon16_Else

+    (0,0): anon18_Else

+    (0,0): anon21_Then

+    (0,0): anon13

+LhsDuplicates.dfy(42,12): Error: when left-hand sides 1 and 3 refer to the same location, they must be assigned the same value

+Execution trace:

+    (0,0): anon0

+LhsDuplicates.dfy(51,18): Error: when left-hand sides 0 and 2 refer to the same location, they must be assigned the same value

+Execution trace:

+    (0,0): anon0

+LhsDuplicates.dfy(60,16): Error: when left-hand sides 1 and 2 may refer to the same location, they must be assigned the same value

+Execution trace:

+    (0,0): anon0

+LhsDuplicates.dfy(69,20): Error: when left-hand sides 1 and 2 refer to the same location, they must be assigned the same value

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 6 verified, 6 errors