Bug fixes in the compilation of forall statements.

3 files changed, 118 insertions, 5 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 0e8b886b..0b8c4254 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1552,9 +1552,14 @@ namespace Microsoft.Dafny {
         //   ingredients.Add(new L-Tuple( LHS0(w,x,y,z), LHS1(w,x,y,z), ..., RHS(w,x,y,z) ));

         // }

         Indent(indent + n * IndentAmount);

-        wr.Write("if ");

-        TrParenExpr(s.Range);

-        wr.WriteLine(" {");

+        wr.Write("if (");

+        foreach (var bv in s.BoundVars) {

+          if (bv.Type.NormalizeExpand() is NatType) {

+            wr.Write("0 <= {0} && ", bv.CompileName);

+          }

+        }

+        TrExpr(s.Range);

+        wr.WriteLine(") {");

 

         var indFinal = indent + (n + 1) * IndentAmount;

         Indent(indFinal);

@@ -1576,7 +1581,6 @@ namespace Microsoft.Dafny {
             TrExpr(lhs.Indices[i]);

             wr.Write(")");

           }

-          wr.WriteLine("] = {0}.Item{1};", tup, L);

         }

         wr.Write(", ");

         TrExpr(rhs);

@@ -1604,7 +1608,7 @@ namespace Microsoft.Dafny {
           wr.WriteLine("{0}.Item1[{0}.Item2] = {0}.Item3;", tup);

         } else {

           var lhs = (MultiSelectExpr)s0.Lhs;

-          wr.Write("{0}.Item1[");

+          wr.Write("{0}.Item1[", tup);

           string sep = "";

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

             wr.Write("{0}{1}.Item{2}", sep, tup, i + 2);

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

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

+

+method Main() {

+  var c := new MyClass;

+  c.arr := new int[10,20];

+  c.K0(3, 12);

+  c.K1(3, 12);

+  c.K2(3, 12);

+  c.K3(3, 12);

+  c.K4(12);

+  c.M();

+  c.N();

+  c.P();

+  c.Q();

+}

+

+class MyClass

+{

+  var arr: array2<int>;

+

+  method K0(i: int, j: int)

+    requires arr != null && 0 <= i < arr.Length0 && 0 <= j < arr.Length1;

+    modifies arr;

+  {

+    forall k | k in {-3, 4} {

+      arr[i,j] := 50;

+    }

+  }

+

+  method K1(i: int, j: int)

+    requires arr != null && 0 <= i < arr.Length0 && 0 <= j < arr.Length1;

+    // note the absence of a modifies clause

+  {

+    forall k: int | k in {} {

+      arr[i,j] := k;  // fine, since control will never reach here

+    }

+  }

+

+  method K2(i: int, j: int)

+    requires arr != null && 0 <= i < arr.Length0 && 0 <= j < arr.Length1;

+    modifies arr;

+  {

+    forall k: int | k in {-3, 4} {

+      // The following would have been an error (since this test file tests

+      // compilation, we don't include the test here):

+      // arr[i,j] := k;  // error: k can take on more than one value

+    }

+  }

+

+  method K3(i: int, j: int)

+    requires arr != null && 0 <= i < arr.Length0 && 0 <= j < arr.Length1;

+    modifies arr;

+  {

+    forall k: nat | k in {-3, 4} && k <= i {

+      arr[k,j] := 50;  // fine, since k:nat is at least 0

+    }

+  }

+

+  method K4(j: int)

+    requires arr != null && 0 <= j < arr.Length1;

+    modifies arr;

+  {

+    forall i, k: nat | 0 <= i < arr.Length0 && k in {-3, 4} {

+      arr[i,j] := k;  // fine, since k can only take on one value

+    }

+  }

+

+  method M()

+  {

+    var ar := new int [3,3];

+    var S: set<int> := {2,0};

+    forall k | k in S {

+      ar[k,1]:= 0;

+    }

+    forall k, j | k in S && j in S {

+      ar[k,j]:= 0;

+    }

+  }

+

+  method N() {

+    var ar := new int[3, 3];

+    ar[2,2] := 0;

+  }

+

+  method P() {

+    var ar := new int[3];

+    var prev := ar[..];

+    var S: set<int> := {};

+    forall k | k in S {

+      ar[k] := 0;

+    }

+    assert ar[..] == prev;

+  }

+

+  method Q() {

+    var ar := new int[3,3];

+    var S: set<int> := {1,2};

+    forall k | k in S {

+      ar[0,0] := 0;

+    }

+    assert ar[0,0] == 0;

+  }

+}

diff --git a/Test/dafny0/ForallCompilation.dfy.expect b/Test/dafny0/ForallCompilation.dfy.expect
new file mode 100644
index 00000000..b9a40d66
--- /dev/null
+++ b/Test/dafny0/ForallCompilation.dfy.expect
@@ -0,0 +1,5 @@
+

+Dafny program verifier finished with 20 verified, 0 errors

+Program compiled successfully

+Running...

+