Skip to content

Commit c4a0c3f

Browse files
RustanLeinoRustanLeino
authored
Allow more Main entry points (#1090)
Fixes #1085
1 parent 42cccc1 commit c4a0c3f

File tree

11 files changed

+310
-67
lines changed

11 files changed

+310
-67
lines changed

‎Source/Dafny/Compiler-Csharp.cs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2914,13 +2914,13 @@ private void AddTestCheckerIfNeeded(string name, Declaration decl, TargetWriter
29142914
}
29152915

29162916
public override void EmitCallToMain(Method mainMethod, string baseName, TargetWriter wr) {
2917-
var companion = TypeName_Companion(mainMethod.EnclosingClass as TopLevelDecl, wr, mainMethod.tok);
2917+
var companion = TypeName_Companion(UserDefinedType.FromTopLevelDeclWithAllBooleanTypeParameters(mainMethod.EnclosingClass), wr, mainMethod.tok, mainMethod);
29182918
var wClass = wr.NewNamedBlock("class __CallToMain");
29192919
var wBody = wClass.NewNamedBlock("public static void Main(string[] args)");
29202920
var modName = mainMethod.EnclosingClass.EnclosingModuleDefinition.CompileName == "_module" ? "_module." : "";
29212921
companion = modName + companion;
29222922

2923-
var idName = mainMethod.IsStatic ? IdName(mainMethod) : "_StaticMain";
2923+
var idName = IssueCreateStaticMain(mainMethod) ? "_StaticMain" : IdName(mainMethod);
29242924

29252925
Coverage.EmitSetup(wBody);
29262926
wBody.WriteLine($"{GetHelperModuleName()}.WithHaltHandling({companion}.{idName});");

‎Source/Dafny/Compiler-go.cs‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -89,12 +89,15 @@ void EmitImports(TargetWriter wr, out TargetWriter importWriter, out TargetWrite
8989
}
9090

9191
public override void EmitCallToMain(Method mainMethod, string baseName, TargetWriter wr) {
92-
var companion = TypeName_Companion(mainMethod.EnclosingClass as ClassDecl, wr, mainMethod.tok);
92+
var companion = TypeName_Companion(UserDefinedType.FromTopLevelDeclWithAllBooleanTypeParameters(mainMethod.EnclosingClass), wr, mainMethod.tok, mainMethod);
9393

9494
var wBody = wr.NewNamedBlock("func main()");
9595
wBody.WriteLine("defer _dafny.CatchHalt()");
96+
97+
var idName = IssueCreateStaticMain(mainMethod) ? "Main" : IdName(mainMethod);
98+
9699
Coverage.EmitSetup(wBody);
97-
wBody.WriteLine("{0}.{1}()", companion, mainMethod.IsStatic ? IdName(mainMethod) : "Main");
100+
wBody.WriteLine("{0}.{1}()", companion, idName);
98101
Coverage.EmitTearDown(wBody);
99102
}
100103

‎Source/Dafny/Compiler-java.cs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -308,7 +308,7 @@ public override void EmitCallToMain(Method mainMethod, string baseName, TargetWr
308308
var className = TransformToClassName(baseName);
309309
wr = wr.NewBlock($"public class {className}");
310310

311-
var companion = TypeName_Companion(mainMethod.EnclosingClass as ClassDecl, wr, mainMethod.tok);
311+
var companion = TypeName_Companion(UserDefinedType.FromTopLevelDeclWithAllBooleanTypeParameters(mainMethod.EnclosingClass), wr, mainMethod.tok, mainMethod);
312312
var wBody = wr.NewNamedBlock("public static void main(String[] args)");
313313
var modName = mainMethod.EnclosingClass.EnclosingModuleDefinition.CompileName == "_module" ? "_System." : "";
314314
companion = modName + companion;

‎Source/Dafny/Compiler.cs‎

Lines changed: 50 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1346,12 +1346,9 @@ public bool HasMain(Program program, out Method mainMethod) {
13461346
continue;
13471347
}
13481348
foreach (var decl in module.TopLevelDecls) {
1349-
var c = decl as TopLevelDeclWithMembers;
1350-
if (c != null) {
1349+
if (decl is TopLevelDeclWithMembers c) {
13511350
foreach (MemberDecl member in c.Members) {
1352-
var m = member as Method;
1353-
if (m == null) continue;
1354-
if (member.FullDafnyName == name) {
1351+
if (member is Method m && member.FullDafnyName == name) {
13551352
mainMethod = m;
13561353
if (!IsPermittedAsMain(mainMethod, out string reason)) {
13571354
Error(mainMethod.tok, "The method \"{0}\" is not permitted as a main method ({1}).", null, name, reason);
@@ -1471,13 +1468,26 @@ public static bool IsPermittedAsMain(Method m, out String reason) {
14711468
reason = "the method has type parameters";
14721469
return false;
14731470
}
1474-
if (cl.TypeArgs.Count != 0) {
1475-
reason = "the enclosing class has type parameters";
1471+
if (cl is OpaqueTypeDecl) {
1472+
reason = "the enclosing type is an opaque type";
14761473
return false;
14771474
}
1478-
if (!m.IsStatic && !cl.Members.TrueForAll(f => !(f is Constructor))) {
1479-
reason = "the method is not static and the enclosing class has constructors";
1480-
return false;
1475+
if (!m.IsStatic) {
1476+
if (cl is TraitDecl) {
1477+
reason = "the method is not static and the enclosing type does not support auto-initialization";
1478+
return false;
1479+
} else if (cl is ClassDecl) {
1480+
if (cl.Members.Exists(f => f is Constructor)) {
1481+
reason = "the method is not static and the enclosing class has constructors";
1482+
return false;
1483+
}
1484+
} else {
1485+
var ty = UserDefinedType.FromTopLevelDeclWithAllBooleanTypeParameters(cl);
1486+
if (!ty.HasCompilableValue) {
1487+
reason = "the method is not static and the enclosing type does not support auto-initialization";
1488+
return false;
1489+
}
1490+
}
14811491
}
14821492
if (!m.Ins.TrueForAll(f => f.IsGhost)) {
14831493
reason = "the method has non-ghost parameters";
@@ -2196,21 +2206,43 @@ private void CompileMethod(Program program, Method m, IClassWriter cw, bool look
21962206

21972207
if (m == program.MainMethod && IssueCreateStaticMain(m)) {
21982208
w = CreateStaticMain(cw);
2209+
var ty = UserDefinedType.FromTopLevelDeclWithAllBooleanTypeParameters(m.EnclosingClass);
2210+
LocalVariable receiver = null;
21992211
if (!m.IsStatic) {
2200-
var c = m.EnclosingClass;
2201-
var typeArgs = c.TypeArgs.ConvertAll(tp => (Type)Type.Bool);
2202-
var ty = new UserDefinedType(m.tok, c.Name, c, typeArgs);
2203-
var wRhs = DeclareLocalVar("b", ty, m.tok, w);
2204-
EmitNew(ty, m.tok, null, wRhs);
2205-
w.WriteLine("b.{0}();", IdName(m));
2212+
receiver = new LocalVariable(m.tok, m.tok, "b", ty, false) {
2213+
type = ty
2214+
};
2215+
if (m.EnclosingClass is ClassDecl) {
2216+
var wRhs = DeclareLocalVar(IdName(receiver), ty, m.tok, w);
2217+
EmitNew(ty, m.tok, null, wRhs);
2218+
} else {
2219+
TrLocalVar(receiver, true, w);
2220+
}
2221+
}
2222+
var typeArgs = CombineAllTypeArguments(m, ty.TypeArgs, m.TypeArgs.ConvertAll(tp => (Type)Type.Bool));
2223+
bool customReceiver = !(m.EnclosingClass is TraitDecl) && NeedsCustomReceiver(m);
2224+
2225+
if (receiver != null && !customReceiver) {
2226+
w.Write("{0}.", IdName(receiver));
22062227
} else {
2207-
w.WriteLine("{0}();", IdName(m));
2228+
var companion = TypeName_Companion(UserDefinedType.FromTopLevelDeclWithAllBooleanTypeParameters(m.EnclosingClass), w, m.tok, m);
2229+
w.Write("{0}.", companion);
2230+
}
2231+
EmitNameAndActualTypeArgs(IdName(m), TypeArgumentInstantiation.ToActuals(ForTypeParameters(typeArgs, m, false)), m.tok, w);
2232+
w.Write("(");
2233+
var sep = "";
2234+
if (receiver != null && customReceiver) {
2235+
w.Write("{0}", IdName(receiver));
2236+
sep = ", ";
22082237
}
2238+
EmitTypeDescriptorsActuals(ForTypeDescriptors(typeArgs, m, false), m.tok, w, ref sep);
2239+
w.Write(")");
2240+
EndStmt(w);
22092241
}
22102242
}
22112243

22122244
protected virtual bool IssueCreateStaticMain(Method m) {
2213-
return !m.IsStatic;
2245+
return !m.IsStatic || m.EnclosingClass.TypeArgs.Count != 0;
22142246
}
22152247

22162248

‎Source/Dafny/DafnyAst.cs‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2835,6 +2835,14 @@ public static UserDefinedType FromTopLevelDecl(IToken tok, TopLevelDecl cd, List
28352835
}
28362836
}
28372837

2838+
public static UserDefinedType FromTopLevelDeclWithAllBooleanTypeParameters(TopLevelDecl cd) {
2839+
Contract.Requires(cd != null);
2840+
Contract.Requires(!(cd is ArrowTypeDecl));
2841+
2842+
var typeArgs = cd.TypeArgs.ConvertAll(tp => (Type)Type.Bool);
2843+
return new UserDefinedType(cd.tok, cd.Name, cd, typeArgs);
2844+
}
2845+
28382846
/// <summary>
28392847
/// If "member" is non-null, then:
28402848
/// Return the upcast of "receiverType" that has base type "member.EnclosingClass".

‎Test/comp/MainMethod.dfy‎

Lines changed: 73 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
1+
// RUN: %dafny /compile:0 "%s" > "%t"
2+
3+
// RUN: %dafny /noVerify /compile:4 /Main:Cl.Static /compileTarget:cs "%s" >> "%t"
4+
// RUN: %dafny /noVerify /compile:4 /Main:Cl.Instance /compileTarget:cs "%s" >> "%t"
5+
// RUN: %dafny /noVerify /compile:4 /Main:Tr.Static /compileTarget:cs "%s" >> "%t"
6+
// RUN: %dafny /noVerify /compile:4 /Main:Dt.Static /compileTarget:cs "%s" >> "%t"
7+
// RUN: %dafny /noVerify /compile:4 /Main:Dt.Instance /compileTarget:cs "%s" >> "%t"
8+
// RUN: %dafny /noVerify /compile:4 /Main:Co.Static /compileTarget:cs "%s" >> "%t"
9+
// RUN: %dafny /noVerify /compile:4 /Main:Co.Instance /compileTarget:cs "%s" >> "%t"
10+
// RUN: %dafny /noVerify /compile:4 /Main:Nt.Static /compileTarget:cs "%s" >> "%t"
11+
// RUN: %dafny /noVerify /compile:4 /Main:Nt.Instance /compileTarget:cs "%s" >> "%t"
12+
13+
// RUN: %dafny /noVerify /compile:4 /Main:Cl.Static /compileTarget:js "%s" >> "%t"
14+
// RUN: %dafny /noVerify /compile:4 /Main:Cl.Instance /compileTarget:js "%s" >> "%t"
15+
// RUN: %dafny /noVerify /compile:4 /Main:Tr.Static /compileTarget:js "%s" >> "%t"
16+
// RUN: %dafny /noVerify /compile:4 /Main:Dt.Static /compileTarget:js "%s" >> "%t"
17+
// RUN: %dafny /noVerify /compile:4 /Main:Dt.Instance /compileTarget:js "%s" >> "%t"
18+
// RUN: %dafny /noVerify /compile:4 /Main:Co.Static /compileTarget:js "%s" >> "%t"
19+
// RUN: %dafny /noVerify /compile:4 /Main:Co.Instance /compileTarget:js "%s" >> "%t"
20+
// RUN: %dafny /noVerify /compile:4 /Main:Nt.Static /compileTarget:js "%s" >> "%t"
21+
// RUN: %dafny /noVerify /compile:4 /Main:Nt.Instance /compileTarget:js "%s" >> "%t"
22+
23+
// RUN: %dafny /noVerify /compile:4 /Main:Cl.Static /compileTarget:go "%s" >> "%t"
24+
// RUN: %dafny /noVerify /compile:4 /Main:Cl.Instance /compileTarget:go "%s" >> "%t"
25+
// RUN: %dafny /noVerify /compile:4 /Main:Tr.Static /compileTarget:go "%s" >> "%t"
26+
// RUN: %dafny /noVerify /compile:4 /Main:Dt.Static /compileTarget:go "%s" >> "%t"
27+
// RUN: %dafny /noVerify /compile:4 /Main:Dt.Instance /compileTarget:go "%s" >> "%t"
28+
// RUN: %dafny /noVerify /compile:4 /Main:Co.Static /compileTarget:go "%s" >> "%t"
29+
// RUN: %dafny /noVerify /compile:4 /Main:Co.Instance /compileTarget:go "%s" >> "%t"
30+
// RUN: %dafny /noVerify /compile:4 /Main:Nt.Static /compileTarget:go "%s" >> "%t"
31+
// RUN: %dafny /noVerify /compile:4 /Main:Nt.Instance /compileTarget:go "%s" >> "%t"
32+
33+
// RUN: %dafny /noVerify /compile:4 /Main:Cl.Static /compileTarget:java "%s" >> "%t"
34+
// RUN: %dafny /noVerify /compile:4 /Main:Cl.Instance /compileTarget:java "%s" >> "%t"
35+
// RUN: %dafny /noVerify /compile:4 /Main:Tr.Static /compileTarget:java "%s" >> "%t"
36+
// RUN: %dafny /noVerify /compile:4 /Main:Dt.Static /compileTarget:java "%s" >> "%t"
37+
// RUN: %dafny /noVerify /compile:4 /Main:Dt.Instance /compileTarget:java "%s" >> "%t"
38+
// RUN: %dafny /noVerify /compile:4 /Main:Co.Static /compileTarget:java "%s" >> "%t"
39+
// RUN: %dafny /noVerify /compile:4 /Main:Co.Instance /compileTarget:java "%s" >> "%t"
40+
// RUN: %dafny /noVerify /compile:4 /Main:Nt.Static /compileTarget:java "%s" >> "%t"
41+
// RUN: %dafny /noVerify /compile:4 /Main:Nt.Instance /compileTarget:java "%s" >> "%t"
42+
43+
// RUN: %diff "%s.expect" "%t"
44+
45+
type plural = x | 2 <= x witness 2
46+
47+
class Cl<X(0)> {
48+
var p: plural
49+
var c: real
50+
var x: X
51+
static method Static() { print "Cl: static\n"; }
52+
method Instance() { print "Cl: ", p, " ", c, " ", x, "\n"; }
53+
}
54+
55+
trait Tr<X> {
56+
static method Static() { print "Tr: static\n"; }
57+
}
58+
59+
datatype Dt<X> = Dt0(plural, X) | Dt1(real, X) {
60+
static method Static() { print "Dt: static\n"; }
61+
method Instance() { print "Dt: ", this, "\n"; }
62+
}
63+
64+
codatatype Co<X> = CoMore(plural, X, Co) {
65+
static method Static() { print "Co: static\n"; }
66+
method Instance() { print "Co: ", this, "\n"; }
67+
}
68+
69+
newtype Nt = x | -0x8000_0000 <= x <= 0x8000_0000 {
70+
const c: plural
71+
static method Static() { print "Nt: static\n"; }
72+
method Instance() { print "Nt: ", this, " ", c, "\n"; }
73+
}

‎Test/comp/MainMethod.dfy.expect‎

Lines changed: 110 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,110 @@
1+
2+
Dafny program verifier finished with 2 verified, 0 errors
3+
4+
Dafny program verifier did not attempt verification
5+
Cl: static
6+
7+
Dafny program verifier did not attempt verification
8+
Cl: 2 0.0 false
9+
10+
Dafny program verifier did not attempt verification
11+
Tr: static
12+
13+
Dafny program verifier did not attempt verification
14+
Dt: static
15+
16+
Dafny program verifier did not attempt verification
17+
Dt: Dt.Dt0(2, false)
18+
19+
Dafny program verifier did not attempt verification
20+
Co: static
21+
22+
Dafny program verifier did not attempt verification
23+
Co: Co.CoMore
24+
25+
Dafny program verifier did not attempt verification
26+
Nt: static
27+
28+
Dafny program verifier did not attempt verification
29+
Nt: 0 2
30+
31+
Dafny program verifier did not attempt verification
32+
Cl: static
33+
34+
Dafny program verifier did not attempt verification
35+
Cl: 2 0.0 false
36+
37+
Dafny program verifier did not attempt verification
38+
Tr: static
39+
40+
Dafny program verifier did not attempt verification
41+
Dt: static
42+
43+
Dafny program verifier did not attempt verification
44+
Dt: Dt.Dt0(2, false)
45+
46+
Dafny program verifier did not attempt verification
47+
Co: static
48+
49+
Dafny program verifier did not attempt verification
50+
Co: Co.CoMore
51+
52+
Dafny program verifier did not attempt verification
53+
Nt: static
54+
55+
Dafny program verifier did not attempt verification
56+
Nt: 0 2
57+
58+
Dafny program verifier did not attempt verification
59+
Cl: static
60+
61+
Dafny program verifier did not attempt verification
62+
Cl: 2 0.0 false
63+
64+
Dafny program verifier did not attempt verification
65+
Tr: static
66+
67+
Dafny program verifier did not attempt verification
68+
Dt: static
69+
70+
Dafny program verifier did not attempt verification
71+
Dt: Dt.Dt0(2, false)
72+
73+
Dafny program verifier did not attempt verification
74+
Co: static
75+
76+
Dafny program verifier did not attempt verification
77+
Co: Co.CoMore
78+
79+
Dafny program verifier did not attempt verification
80+
Nt: static
81+
82+
Dafny program verifier did not attempt verification
83+
Nt: 0 2
84+
85+
Dafny program verifier did not attempt verification
86+
Cl: static
87+
88+
Dafny program verifier did not attempt verification
89+
Cl: 2 0.0 false
90+
91+
Dafny program verifier did not attempt verification
92+
Tr: static
93+
94+
Dafny program verifier did not attempt verification
95+
Dt: static
96+
97+
Dafny program verifier did not attempt verification
98+
Dt: Dt.Dt0(2, false)
99+
100+
Dafny program verifier did not attempt verification
101+
Co: static
102+
103+
Dafny program verifier did not attempt verification
104+
Co: Co.CoMore
105+
106+
Dafny program verifier did not attempt verification
107+
Nt: static
108+
109+
Dafny program verifier did not attempt verification
110+
Nt: 0 2

‎Test/git-issues/git-issue-MainE.dfy‎

Lines changed: 30 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,9 @@
1111
// RUN: %dafny /noVerify /compile:4 /Main:K.Test "%s" >> "%t"
1212
// RUN: %dafny /noVerify /compile:4 /Main: "%s" >> "%t"
1313
// RUN: %dafny /noVerify /compile:4 /Main:- "%s" >> "%t"
14+
// RUN: %dafny /noVerify /compile:4 /Main:Tr.Instance "%s" >> "%t"
15+
// RUN: %dafny /noVerify /compile:4 /Main:Opaque.Static "%s" >> "%t"
16+
// RUN: %dafny /noVerify /compile:4 /Main:Opaque.Instance "%s" >> "%t"
1417
// RUN: %diff "%s.expect" "%t"
1518

1619
class A {
@@ -20,7 +23,7 @@ class B {
2023
method Test<T>() { print "Bad\n"; }
2124
}
2225
class C<T> {
23-
method Test() { print "Bad\n"; }
26+
method Test() { print "OK-C\n"; }
2427
}
2528
class D {
2629
constructor() {}
@@ -49,4 +52,30 @@ class Z {
4952
method Main() { print "Main\n"; }
5053
}
5154

55+
// Of the remaining methods, this file tests only the error cases.
56+
// The cases that compile are tested in Test/comp/MainMethod.dfy.
57+
58+
trait Tr {
59+
static method Static() { print "OK-Tr\n"; }
60+
method Instance() { print "Bad\n"; }
61+
}
62+
63+
datatype Dt = Dt0(int) | Dt1(real) {
64+
static method Static() { print "OK-Dt: static\n"; }
65+
method Instance() { print "OK-Dt: ", this, "\n"; }
66+
}
67+
68+
codatatype Co = CoMore(Co) {
69+
static method Static() { print "OK-Co: static\n"; }
70+
method Instance() { print "OK-Co: ", this, "\n"; }
71+
}
5272

73+
newtype Nt = x | -0x8000_0000 <= x <= 0x8000_0000 {
74+
static method Static() { print "OK-Nt: static\n"; }
75+
method Instance() { print "OK-Nt: ", this, "\n"; }
76+
}
77+
78+
type {:extern "OpaqueX"} Opaque {
79+
static method Static() { print "Bad\n"; }
80+
method Instance() { print "Bad\n"; }
81+
}

0 commit comments

Comments
 (0)