Dafny: Compilation of multi-dimensional arrays

5 files changed, 145 insertions, 21 deletions

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index 610cd2f3..982683b9 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -218,19 +218,4 @@ namespace Dafny
       this.Cdr = b;

     }

   }

-  public class Helpers

-  {

-    public static T[] InitNewArray<T>(BigInteger size) {

-      int sz = (int)size;

-      T[] a = new T[sz];

-      BigInteger[] b = a as BigInteger[];

-      if (b != null) {

-        BigInteger z = new BigInteger(0);

-        for (int i = 0; i < sz; i++) {

-          b[i] = z;

-        }

-      }

-      return a;

-    }

-  }

 }

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 6115f026..648be451 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -61,6 +61,7 @@ namespace Microsoft.Dafny {
       wr.WriteLine("// Dafny program {0} compiled into C#", program.Name);

       wr.WriteLine();

       ReadRuntimeSystem();

+      CompileBuiltIns(program.BuiltIns);

 

       foreach (ModuleDecl m in program.Modules) {

         int indent = 0;

@@ -98,6 +99,82 @@ namespace Microsoft.Dafny {
       }

     }

 

+    void CompileBuiltIns(BuiltIns builtIns) {

+      wr.WriteLine("namespace Dafny {");

+      Indent(IndentAmount);

+      wr.WriteLine("public class Helpers {");

+      foreach (var decl in builtIns.SystemModule.TopLevelDecls) {

+        if (decl is ArrayClassDecl) {

+          int dims = ((ArrayClassDecl)decl).Dims;

+          // public static T[,] InitNewArray2<T>(BigInteger size0, BigInteger size1) {

+          Indent(3 * IndentAmount);

+          wr.Write("public static T[");

+          RepeatWrite(wr, dims, "", ",");

+          wr.Write("] InitNewArray{0}<T>(", dims);

+          RepeatWrite(wr, dims, "BigInteger size{0}", ", ");

+          wr.WriteLine(") {");

+          // int s0 = (int)size0;

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

+            Indent(4 * IndentAmount);

+            wr.WriteLine("int s{0} = (int)size{0};", i);

+          }

+          // T[,] a = new T[s0, s1];

+          Indent(4 * IndentAmount);

+          wr.Write("T[");

+          RepeatWrite(wr, dims, "", ",");

+          wr.Write("] a = new T[");

+          RepeatWrite(wr, dims, "s{0}", ",");

+          wr.WriteLine("];");

+          // BigInteger[,] b = a as BigInteger[,];

+          Indent(4 * IndentAmount);

+          wr.Write("BigInteger[");

+          RepeatWrite(wr, dims, "", ",");

+          wr.Write("] b = a as BigInteger[");

+          RepeatWrite(wr, dims, "", ",");

+          wr.WriteLine("];");

+          // if (b != null) {

+          Indent(4 * IndentAmount);

+          wr.WriteLine("if (b != null) {");

+          // BigInteger z = new BigInteger(0);

+          Indent(5 * IndentAmount);

+          wr.WriteLine("BigInteger z = new BigInteger(0);");

+          // for (int i0 = 0; i0 < s0; i0++)

+          //   for (int i1 = 0; i1 < s1; i1++)

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

+            Indent((5+i) * IndentAmount);

+            wr.WriteLine("for (int i{0} = 0; i{0} < s{0}; i{0}++)", i);

+          }

+          // b[i0,i1] = z;

+          Indent((5+dims) * IndentAmount);

+          wr.Write("b[");

+          RepeatWrite(wr, dims, "i{0}", ",");

+          wr.WriteLine("] = z;");

+          // }

+          Indent(4 * IndentAmount);

+          wr.WriteLine("}");

+          // return a;

+          Indent(4 * IndentAmount);

+          wr.WriteLine("return a;");

+          // }

+          Indent(3 * IndentAmount);

+          wr.WriteLine("}");  // end of method

+        }

+      }

+      Indent(IndentAmount);

+      wr.WriteLine("}");  // end of class Helpers

+      wr.WriteLine("}");  // end of namespace

+    }

+

+    static void RepeatWrite(TextWriter wr, int times, string template, string separator) {

+      Contract.Requires(1 <= times);

+      string s = "";

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

+        wr.Write(s);

+        wr.Write(template, i);

+        s = separator;

+      }

+    }

+

     void CompileDatatypeConstructors(DatatypeDecl dt, int indent)

     {Contract.Requires(dt != null);

       foreach (DatatypeCtor ctor in dt.Ctors) {

@@ -767,8 +844,7 @@ namespace Microsoft.Dafny {
           if (tp.EType is IntType || tp.EType.IsTypeParameter) {

             // Because the default constructor for BigInteger does not generate a valid BigInteger, we have

             // to excplicitly initialize the elements of an integer array.  This is all done in a helper routine.

-            Contract.Assume(tp.ArrayDimensions.Count == 1);  // TODO: multi-dimensional arrays

-            wr.Write("Dafny.Helpers.InitNewArray<{0}>(", TypeName(tp.EType));

+            wr.Write("Dafny.Helpers.InitNewArray{0}<{1}>", tp.ArrayDimensions.Count, TypeName(tp.EType));

             string prefix = "(";

             foreach (Expression dim in tp.ArrayDimensions) {

               wr.Write(prefix);

@@ -931,8 +1007,20 @@ namespace Microsoft.Dafny {
       

       } else if (expr is FieldSelectExpr) {

         FieldSelectExpr e = (FieldSelectExpr)expr;

-        TrParenExpr(e.Obj);

-        wr.Write(".{0}", e.FieldName);

+        SpecialField sf = e.Field as SpecialField;

+        if (sf != null) {

+          if (sf.Type is IntType) {

+            wr.Write("new BigInteger(");

+          }

+          TrParenExpr(e.Obj);

+          wr.Write(".{0}", sf.CompiledName);

+          if (sf.Type is IntType) {

+            wr.Write(")");

+          }

+        } else {

+          TrParenExpr(e.Obj);

+          wr.Write(".{0}", e.Field.Name);

+        }

         

       } else if (expr is SeqSelectExpr) {

         SeqSelectExpr e = (SeqSelectExpr)expr;

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index f21a5b3e..27f5e3a5 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -58,7 +58,8 @@ namespace Microsoft.Dafny {
         ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule);

         for (int d = 0; d < dims; d++) {

           string name = dims == 1 ? "Length" : "Length" + d;

-          Field len = new Field(Token.NoToken, name, false, false, Type.Int, null);

+          string compiledName = dims == 1 ? "Length" : "GetLength(" + d + ")";

+          Field len = new SpecialField(Token.NoToken, name, compiledName, false, false, Type.Int, null);

           len.EnclosingClass = arrayClass;  // resolve here

           arrayClass.Members.Add(len);

         }

@@ -791,6 +792,15 @@ namespace Microsoft.Dafny {
     }

   }

 

+  public class SpecialField : Field

+  {

+    public readonly string CompiledName;

+    public SpecialField(IToken tok, string name, string compiledName, bool isGhost, bool isMutable, Type type, Attributes attributes)

+      : base(tok, name, isGhost, isMutable, type, attributes) {

+      CompiledName = compiledName;

+    }

+  }

+

   public class CouplingInvariant : MemberDecl {

     public readonly Expression Expr;

     public readonly List<IToken/*!*/>/*!*/ Toks;

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index c81c0268..306de96c 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -33,7 +33,7 @@ Dafny program verifier finished with 9 verified, 0 errors
 

 -------------------- MatrixFun.dfy --------------------

 

-Dafny program verifier finished with 4 verified, 0 errors

+Dafny program verifier finished with 8 verified, 0 errors

 

 -------------------- SchorrWaite.dfy --------------------

 

diff --git a/Test/dafny1/MatrixFun.dfy b/Test/dafny1/MatrixFun.dfy
index 96d89ad6..86ad451d 100644
--- a/Test/dafny1/MatrixFun.dfy
+++ b/Test/dafny1/MatrixFun.dfy
@@ -57,3 +57,44 @@ method Flip<T>(m: array2<T>)
     }

   }

 }

+

+method Main()

+{

+  var B := new bool[2,5];

+  B[0,0] := true;  B[0,1] := false;  B[0,2] := false;  B[0,3] := true;  B[0,4] := false;

+  B[1,0] := true;  B[1,1] := true;   B[1,2] := true;   B[1,3] := true;  B[1,4] := false;

+  print "Before:\n";

+  call PrintMatrix(B);

+  call MirrorImage(B);

+  print "Mirror image:\n";

+  call PrintMatrix(B);

+

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

+  A[0,0] := 5;  A[0,1] := 7;  A[0,2] := 9;

+  A[1,0] := 6;  A[1,1] := 2;  A[1,2] := 3;

+  A[2,0] := 7;  A[2,1] := 1;  A[2,2] := 0;

+  print "Before:\n";

+  call PrintMatrix(A);

+  call Flip(A);

+  print "Flip:\n";

+  call PrintMatrix(A);

+}

+

+method PrintMatrix<T>(m: array2<T>)

+  requires m != null;

+{

+  var i := 0;

+  while (i < m.Length0) {

+    var j := 0;

+    while (j < m.Length1) {

+      print m[i,j];

+      j := j + 1;

+      if (j == m.Length1) {

+        print "\n";

+      } else {

+        print ", ";

+      }

+    }

+    i := i + 1;

+  }

+}