summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Binaries/DafnyRuntime.cs1
-rw-r--r--Source/Dafny/Compiler.cs106
-rw-r--r--Test/VSComp2010/runtest.bat4
-rw-r--r--Test/VSI-Benchmarks/runtest.bat14
-rw-r--r--Test/dafny1/runtest.bat9
-rw-r--r--Test/vacid0/runtest.bat9
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<T>
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<T> {
// Base_Dt<T> d;
- // public Base_Dt<T> D {
+ // public Base_Dt<T> _D {
// get { if (d == null) { d = Default; } return d; }
// }
// public Dt(Base_Dt<T> d) { this.d = d; }
@@ -243,9 +245,9 @@ namespace Microsoft.Dafny {
// get { return ...; }
// }
// public override bool Equals(object other) {
- // return other is Dt<T> && D.Equals(((Dt<T>)other).D);
+ // return other is Dt<T> && _D.Equals(((Dt<T>)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<string>() != null);
+ Contract.Requires(formal != null);
+ Contract.Ensures(Contract.Result<string>() != 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<Pair<{0},{1}>> {2} = new List<Pair<{0},{1}>>();", 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
)
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-31 05:57:45 +0000