From 90f890087c87221d1268d07d2641b2ba8eb6c969 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 11 May 2011 17:03:02 -0700 Subject: Dafny: fixed compilation bugs, added @-signs in front of identifiers to avoid clashes with C# keywords, added switch in runtest scripts to turn on compilation --- Binaries/DafnyRuntime.cs | 1 + Source/Dafny/Compiler.cs | 106 +++++++++++++++++++++------------------- Test/VSComp2010/runtest.bat | 4 +- Test/VSI-Benchmarks/runtest.bat | 14 ++++-- Test/dafny1/runtest.bat | 9 +++- Test/vacid0/runtest.bat | 9 +++- 6 files changed, 86 insertions(+), 57 deletions(-) diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 63cca64a..b10aeac9 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -122,6 +122,7 @@ namespace Dafny // return the first one return t; } + return default(T); } } public class Sequence diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 62270067..9495d64e 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -66,7 +66,7 @@ namespace Microsoft.Dafny { foreach (ModuleDecl m in program.Modules) { int indent = 0; if (!m.IsDefaultModule) { - wr.WriteLine("namespace {0} {{", m.Name); + wr.WriteLine("namespace @{0} {{", m.Name); indent += IndentAmount; } foreach (TopLevelDecl d in m.TopLevelDecls) { @@ -84,7 +84,7 @@ namespace Microsoft.Dafny { } else { ClassDecl cl = (ClassDecl)d; Indent(indent); - wr.Write("public class {0}", cl.Name); + wr.Write("public class @{0}", cl.Name); if (cl.TypeArgs.Count != 0) { wr.Write("<{0}>", TypeParameters(cl.TypeArgs)); } @@ -199,17 +199,17 @@ namespace Microsoft.Dafny { wr.Write(">"); } wr.Write(" : Base_{0}", dt.Name); - wr.WriteLine(" {"); if (dt.TypeArgs.Count != 0) { wr.Write("<{0}>", TypeParameters(dt.TypeArgs)); } + wr.WriteLine(" {"); int ind = indent + IndentAmount; int i = 0; foreach (Formal arg in ctor.Formals) { if (!arg.IsGhost) { Indent(ind); - wr.WriteLine("public readonly {0} {1};", TypeName(arg.Type), FormalName(arg, i)); + wr.WriteLine("public readonly {0} @{1};", TypeName(arg.Type), FormalName(arg, i)); i++; } } @@ -222,7 +222,7 @@ namespace Microsoft.Dafny { foreach (Formal arg in ctor.Formals) { if (!arg.IsGhost) { Indent(ind + IndentAmount); - wr.WriteLine("this.{0} = {0};", FormalName(arg, i)); + wr.WriteLine("this.@{0} = @{0};", FormalName(arg, i)); i++; } } @@ -232,10 +232,12 @@ namespace Microsoft.Dafny { } } - void CompileDatatypeStruct(DatatypeDecl dt, int indent) {Contract.Requires(dt != null); + void CompileDatatypeStruct(DatatypeDecl dt, int indent) { + Contract.Requires(dt != null); + // public struct Dt { // Base_Dt d; - // public Base_Dt D { + // public Base_Dt _D { // get { if (d == null) { d = Default; } return d; } // } // public Dt(Base_Dt d) { this.d = d; } @@ -243,9 +245,9 @@ namespace Microsoft.Dafny { // get { return ...; } // } // public override bool Equals(object other) { - // return other is Dt && D.Equals(((Dt)other).D); + // return other is Dt && _D.Equals(((Dt)other)._D); // } - // public override int GetHashCode() { return D.GetHashCode(); } + // public override int GetHashCode() { return _D.GetHashCode(); } // } string DtT = dt.Name; if (dt.TypeArgs.Count != 0) { @@ -253,27 +255,29 @@ namespace Microsoft.Dafny { } Indent(indent); - wr.WriteLine("public struct {0} {{", DtT); + wr.WriteLine("public struct @{0} {{", DtT); int ind = indent + IndentAmount; Indent(ind); wr.WriteLine("Base_{0} d;", DtT); Indent(ind); - wr.WriteLine("public Base_{0} D {{", DtT); + wr.WriteLine("public Base_{0} _D {{", DtT); Indent(ind + IndentAmount); wr.WriteLine("get { if (d == null) { d = Default; } return d; }"); Indent(ind); wr.WriteLine("}"); Indent(ind); - wr.WriteLine("public {0}(Base_{1} d) {{ this.d = d; }}", dt.Name, DtT); + wr.WriteLine("public @{0}(Base_{1} d) {{ this.d = d; }}", dt.Name, DtT); Indent(ind); wr.WriteLine("public static Base_{0} Default {{", DtT); Indent(ind + IndentAmount); wr.Write("get { return "); wr.Write("new {0}", DtCtorName(cce.NonNull(dt.DefaultCtor))); - // todo: type parameters + if (dt.TypeArgs.Count != 0) { + wr.Write("<{0}>", TypeParameters(dt.TypeArgs)); + } wr.Write("("); string sep = ""; foreach (Formal f in dt.DefaultCtor.Formals) { @@ -288,11 +292,11 @@ namespace Microsoft.Dafny { Indent(ind); wr.WriteLine("public override bool Equals(object other) {"); Indent(ind + IndentAmount); - wr.WriteLine("return other is {0} && D.Equals((({0})other).D);", DtT); + wr.WriteLine("return other is @{0} && _D.Equals(((@{0})other)._D);", DtT); Indent(ind); wr.WriteLine("}"); Indent(ind); - wr.WriteLine("public override int GetHashCode() { return D.GetHashCode(); }"); + wr.WriteLine("public override int GetHashCode() { return _D.GetHashCode(); }"); Indent(indent); wr.WriteLine("}"); @@ -306,7 +310,7 @@ namespace Microsoft.Dafny { foreach (Formal arg in formals) { if (!arg.IsGhost) { string name = FormalName(arg, i); - wr.Write("{0}{1}{2} {3}", sep, arg.InParam ? "" : "out ", TypeName(arg.Type), name); + wr.Write("{0}{1}{2} @{3}", sep, arg.InParam ? "" : "out ", TypeName(arg.Type), name); sep = ", "; i++; } @@ -314,7 +318,8 @@ namespace Microsoft.Dafny { } string FormalName(Formal formal, int i) { - Contract.Requires(formal != null);Contract.Ensures(Contract.Result() != null); + Contract.Requires(formal != null); + Contract.Ensures(Contract.Result() != null); return formal.Name.StartsWith("#") ? "a" + i : formal.Name; } @@ -333,7 +338,7 @@ namespace Microsoft.Dafny { Field f = (Field)member; if (!f.IsGhost) { Indent(indent); - wr.WriteLine("public {0} {1} = {2};", TypeName(f.Type), f.Name, DefaultValue(f.Type)); + wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type), f.Name, DefaultValue(f.Type)); } } else if (member is Function) { @@ -344,7 +349,7 @@ namespace Microsoft.Dafny { Error("Function {0} has no body", f.FullName); } else { Indent(indent); - wr.Write("public {0}{1} {2}", f.IsStatic ? "static " : "", TypeName(f.ResultType), f.Name); + wr.Write("public {0}{1} @{2}", f.IsStatic ? "static " : "", TypeName(f.ResultType), f.Name); if (f.TypeArgs.Count != 0) { wr.Write("<{0}>", TypeParameters(f.TypeArgs)); } @@ -354,8 +359,8 @@ namespace Microsoft.Dafny { if (f.Body is MatchExpr) { MatchExpr me = (MatchExpr)f.Body; // Type source = e; - // if (source.D is Dt_Ctor0) { - // FormalType f0 = ((Dt_Ctor0)source.D).a0; + // if (source._D is Dt_Ctor0) { + // FormalType f0 = ((Dt_Ctor0)source._D).a0; // ... // return Body0; // } else if (...) { @@ -397,7 +402,7 @@ namespace Microsoft.Dafny { Method m = (Method)member; if (!m.IsGhost) { Indent(indent); - wr.Write("public {0}void {1}", m.IsStatic ? "static " : "", m.Name); + wr.Write("public {0}void @{1}", m.IsStatic ? "static " : "", m.Name); if (m.TypeArgs.Count != 0) { wr.Write("<{0}>", TypeParameters(m.TypeArgs)); } @@ -412,7 +417,7 @@ namespace Microsoft.Dafny { foreach (Formal p in m.Outs) { if (!p.IsGhost) { Indent(indent + IndentAmount); - wr.WriteLine("{0} = {1};", p.Name, DefaultValue(p.Type)); + wr.WriteLine("@{0} = {1};", p.Name, DefaultValue(p.Type)); } } if (m.Body == null) { @@ -428,7 +433,7 @@ namespace Microsoft.Dafny { wr.WriteLine("public static void Main(string[] args) {"); ClassDecl cl = cce.NonNull(m.EnclosingClass); Indent(indent + IndentAmount); - wr.Write("{0} b = new {0}", cl.Name); + wr.Write("@{0} b = new @{0}", cl.Name); if (cl.TypeArgs.Count != 0) { // instantiate every parameter, it doesn't particularly matter how wr.Write("<"); @@ -493,7 +498,7 @@ namespace Microsoft.Dafny { return name + "]"; } else if (type is UserDefinedType) { UserDefinedType udt = (UserDefinedType)type; - string s = udt.Name; + string s = "@" + udt.Name; if (udt.TypeArgs.Count != 0) { if (Contract.Exists(udt.TypeArgs, argType =>argType is ObjectType)) { Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost"); @@ -538,7 +543,7 @@ namespace Microsoft.Dafny { string s = ""; string sep = ""; foreach (TypeParameter tp in targs) { - s += sep + tp.Name; + s += sep + "@" + tp.Name; sep = ","; } return s; @@ -569,14 +574,14 @@ namespace Microsoft.Dafny { return "null"; } else if (type.IsDatatype) { UserDefinedType udt = (UserDefinedType)type; - string s = udt.Name; + string s = "@" + udt.Name; if (udt.TypeArgs.Count != 0) { s += "<" + TypeNames(udt.TypeArgs) + ">"; } - return s + ".Default"; + return string.Format("new {0}({0}.Default)", s); } else if (type.IsTypeParameter) { UserDefinedType udt = (UserDefinedType)type; - return "default(" + udt.Name + ")"; + return "default(@" + udt.Name + ")"; } else if (type is SetType) { return DafnySetClass + "<" + TypeName(((SetType)type).Arg) + ">.Empty"; } else if (type is SeqType) { @@ -667,12 +672,10 @@ namespace Microsoft.Dafny { string nw = "_nw" + tmpVarCount; tmpVarCount++; Indent(indent); - wr.Write("{0} = ", nw); + wr.Write("var {0} = ", nw); TrAssignmentRhs(s.Rhs); wr.WriteLine(";"); - Indent(indent); TrCallStmt(tRhs.InitCall, nw, indent); - wr.WriteLine(";"); Indent(indent); TrExpr(s.Lhs); wr.WriteLine(" = {0};", nw); @@ -709,7 +712,7 @@ namespace Microsoft.Dafny { } TrStmt(s.Thn, indent); - if (s.Els != null) { + if (s.Els != null && s.Guard != null) { Indent(indent); wr.WriteLine("else"); TrStmt(s.Els, indent); } @@ -749,7 +752,7 @@ namespace Microsoft.Dafny { wr.WriteLine("List> {2} = new List>();", TType, RhsType, pu); Indent(indent); - wr.Write("foreach ({0} {1} in (", TType, s.BoundVar.Name); + wr.Write("foreach ({0} @{1} in (", TType, s.BoundVar.Name); TrExpr(s.Collection); wr.WriteLine(").Elements) {"); @@ -762,7 +765,7 @@ namespace Microsoft.Dafny { TrStmt(p, indent + 2*IndentAmount); } Indent(indent + 2*IndentAmount); - wr.Write("{0}.Add(new Pair<{1},{2}>({3}, ", pu, TType, RhsType, s.BoundVar.Name); + wr.Write("{0}.Add(new Pair<{1},{2}>(@{3}, ", pu, TType, RhsType, s.BoundVar.Name); ExprRhs rhsExpr = s.BodyAssign.Rhs as ExprRhs; if (rhsExpr != null) { TrExpr(rhsExpr.Expr); @@ -783,8 +786,8 @@ namespace Microsoft.Dafny { } else if (stmt is MatchStmt) { MatchStmt s = (MatchStmt)stmt; // Type source = e; - // if (source.D is Dt_Ctor0) { - // FormalType f0 = ((Dt_Ctor0)source.D).a0; + // if (source._D is Dt_Ctor0) { + // FormalType f0 = ((Dt_Ctor0)source._D).a0; // ... // Body0; // } else if (...) { @@ -823,13 +826,13 @@ namespace Microsoft.Dafny { Contract.Assert(s.Method != null); // follows from the fact that stmt has been successfully resolved Indent(indent); if (receiverReplacement != null) { - wr.Write(receiverReplacement); + wr.Write("@" + receiverReplacement); } else if (s.Method.IsStatic) { wr.Write(TypeName(cce.NonNull(s.Receiver.Type))); } else { TrParenExpr(s.Receiver); } - wr.Write(".{0}(", s.Method.Name); + wr.Write(".@{0}(", s.Method.Name); string sep = ""; for (int i = 0; i < s.Method.Ins.Count; i++) { @@ -921,8 +924,13 @@ namespace Microsoft.Dafny { void TrVarDecl(VarDecl s, bool alwaysInitialize, int indent) { Contract.Requires(s != null); + if (s.IsGhost) { + // only emit non-ghosts (we get here only for local variables introduced implicitly by call statements) + return; + } + Indent(indent); - wr.Write("{0} {1}", TypeName(s.Type), s.Name); + wr.Write("{0} @{1}", TypeName(s.Type), s.Name); if (s.Rhs != null) { wr.Write(" = "); TrAssignmentRhs(s.Rhs); @@ -943,15 +951,15 @@ namespace Microsoft.Dafny { Contract.Requires(source != null); Contract.Requires(ctor != null); Contract.Requires(cce.NonNullElements(arguments)); - // if (source.D is Dt_Ctor0) { - // FormalType f0 = ((Dt_Ctor0)source.D).a0; + // if (source._D is Dt_Ctor0) { + // FormalType f0 = ((Dt_Ctor0)source._D).a0; // ... Indent(indent); wr.Write("{0}if (", caseIndex == 0 ? "" : "} else "); if (caseIndex == caseCount - 1) { wr.Write("true"); } else { - wr.Write("{0}.D is {1}", source, DtCtorName(ctor)); + wr.Write("{0}._D is {1}", source, DtCtorName(ctor)); } wr.WriteLine(") {"); @@ -960,9 +968,9 @@ namespace Microsoft.Dafny { Formal arg = ctor.Formals[m]; if (!arg.IsGhost) { BoundVar bv = arguments[m]; - // FormalType f0 = ((Dt_Ctor0)source.D).a0; + // FormalType f0 = ((Dt_Ctor0)source._D).a0; Indent(indent + IndentAmount); - wr.WriteLine("{0} {1} = (({2}){3}.D).{4};", + wr.WriteLine("{0} @{1} = (({2}){3}._D).@{4};", TypeName(bv.Type), bv.Name, DtCtorName(ctor), source, FormalName(arg, k)); k++; } @@ -1022,7 +1030,7 @@ namespace Microsoft.Dafny { } else if (expr is IdentifierExpr) { IdentifierExpr e = (IdentifierExpr)expr; - wr.Write(cce.NonNull(e.Var).Name); + wr.Write("@" + e.Var.Name); } else if (expr is SetDisplayExpr) { SetDisplayExpr e = (SetDisplayExpr)expr; @@ -1050,7 +1058,7 @@ namespace Microsoft.Dafny { } } else { TrParenExpr(e.Obj); - wr.Write(".{0}", e.Field.Name); + wr.Write(".@{0}", e.Field.Name); } } else if (expr is SeqSelectExpr) { @@ -1103,7 +1111,7 @@ namespace Microsoft.Dafny { } else { TrParenExpr(e.Receiver); } - wr.Write(".{0}", f.Name); + wr.Write(".@{0}", f.Name); wr.Write("("); string sep = ""; for (int i = 0; i < e.Args.Count; i++) { @@ -1325,7 +1333,7 @@ namespace Microsoft.Dafny { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected BoundedPool type } wr.Write("{0}, ", expr is ForallExpr ? "true" : "false"); - wr.Write("{0} => ", bv.Name); + wr.Write("@{0} => ", bv.Name); } TrExpr(e.Body); for (int i = 0; i < n; i++) { diff --git a/Test/VSComp2010/runtest.bat b/Test/VSComp2010/runtest.bat index e39abe7d..e16eda13 100644 --- a/Test/VSComp2010/runtest.bat +++ b/Test/VSComp2010/runtest.bat @@ -4,7 +4,7 @@ setlocal set BOOGIEDIR=..\..\Binaries set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe set BPLEXE=%BOOGIEDIR%\Boogie.exe - +set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy Problem3-FindZero.dfy Problem4-Queens.dfy @@ -12,4 +12,6 @@ for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy echo. echo -------------------- %%f -------------------- %DAFNY_EXE% %* %%f + + IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs ) diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat index 0cd898c4..a733a1c0 100644 --- a/Test/VSI-Benchmarks/runtest.bat +++ b/Test/VSI-Benchmarks/runtest.bat @@ -4,12 +4,16 @@ setlocal set BOOGIEDIR=..\..\Binaries set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe set BPLEXE=%BOOGIEDIR%\Boogie.exe +set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe - - -for %%f in ( b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy - b8.dfy ) do ( +for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do ( echo. echo -------------------- %%f -------------------- - %DAFNY_EXE% /compile:0 %* %%f + + REM The following line will just run the verifier + IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 %* %%f + + REM Alternatively, the following lines also produce C# code and compile it + IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f + IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs ) diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index b6fc7f62..36b93883 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -4,6 +4,7 @@ setlocal set BOOGIEDIR=..\..\Binaries set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe set BPLEXE=%BOOGIEDIR%\Boogie.exe +set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe for %%f in (BQueue.bpl) do ( echo. @@ -25,5 +26,11 @@ for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy UltraFilter.dfy) do ( echo. echo -------------------- %%f -------------------- - %DAFNY_EXE% /compile:0 %* %%f + + REM The following line will just run the verifier + IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 %* %%f + + REM Alternatively, the following lines also produce C# code and compile it + IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f + IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs ) diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat index d6af7b71..32c6a984 100644 --- a/Test/vacid0/runtest.bat +++ b/Test/vacid0/runtest.bat @@ -4,9 +4,16 @@ setlocal set BOOGIEDIR=..\..\Binaries set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe set BPLEXE=%BOOGIEDIR%\Boogie.exe +set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do ( echo. echo -------------------- %%f -------------------- - %DAFNY_EXE% /compile:0 %* %%f + + REM The following line will just run the verifier + IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 %* %%f + + REM Alternatively, the following lines also produce C# code and compile it + IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f + IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs ) -- cgit v1.2.3