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 --- Source/Dafny/Compiler.cs | 96 ++++++++++++++++++++++++++++++++++++++++++++++-- Source/Dafny/DafnyAst.cs | 12 +++++- 2 files changed, 103 insertions(+), 5 deletions(-) (limited to 'Source') 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; -- cgit v1.2.3