From 40021fe7042eb08ed5b4d16034e23c9ed022c4aa Mon Sep 17 00:00:00 2001 From: rustanleino Date: Tue, 21 Sep 2010 00:17:44 +0000 Subject: Dafny: Compilation of multi-dimensional arrays --- Binaries/DafnyRuntime.cs | 15 -------- Source/Dafny/Compiler.cs | 96 +++++++++++++++++++++++++++++++++++++++++++++-- Source/Dafny/DafnyAst.cs | 12 +++++- Test/dafny1/Answer | 2 +- Test/dafny1/MatrixFun.dfy | 41 ++++++++++++++++++++ 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(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(BigInteger size0, BigInteger size1) { + Indent(3 * IndentAmount); + wr.Write("public static T["); + RepeatWrite(wr, dims, "", ","); + wr.Write("] InitNewArray{0}(", 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/*!*/ 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(m: array2) } } } + +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(m: array2) + 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; + } +} -- cgit v1.2.3