Exposing --output and --spill-translation in dafny test, per Issue 3612

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -1621,7 +1621,9 @@ public static bool HasMain(Program program, out Method mainMethod) {
             }
           }
         }
-        ReportError(program.Reporter, program.DefaultModule.tok, "Could not find the method named by the -Main option: {0}", null, name);
+        if (name != RunAllTestsMainMethod.SyntheticTestMainName) {
+          ReportError(program.Reporter, program.DefaultModule.tok, "Could not find the method named by the -Main option: {0}", null, name);
+        }
       }
       foreach (var module in program.CompileModules) {
         if (module.IsAbstract) {

Source/DafnyCore/DafnyOptions.cs

@@ -290,6 +290,7 @@ public enum ContractTestingMode {
     public bool RewriteFocalPredicates = true;
     public bool PrintTooltips = false;
     public bool PrintStats = false;
+    public string MethodsToTest = null;
     public bool DisallowConstructorCaseWithoutParentheses = false;
     public bool PrintFunctionCallGraph = false;
     public bool WarnShadowing = false;

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -154,6 +154,12 @@ Note that quantifier variable domains (<- <Domain>) are available in both syntax
   };
   public static readonly Option<bool> VerifyIncludedFiles = new("--verify-included-files",
     "Verify code in included files.");
+  public static readonly Option<bool> UseBaseFileName = new("--use-basename-for-filename",
+    "When parsing use basename of file for tokens instead of the path supplied on the command line") {
+  };
+  public static readonly Option<bool> SpillTranslation = new("--spill-translation",
+    @"In case the Dafny source code is translated to another language, emit that translation.") {
+  };
   public static readonly Option<bool> WarningAsErrors = new("--warn-as-errors",
     "Treat warnings as errors.");
   public static readonly Option<bool> WarnMissingConstructorParenthesis = new("--warn-missing-constructor-parentheses",
@@ -201,6 +207,7 @@ static CommonOptionBag() {
       }
     });
     DafnyOptions.RegisterLegacyBinding(IncludeRuntimeOption, (options, value) => { options.IncludeRuntime = value; });
+    DafnyOptions.RegisterLegacyBinding(UseBaseFileName, (o, f) => o.UseBaseNameForFileName = f);
     DafnyOptions.RegisterLegacyBinding(UseJavadocLikeDocstringRewriterOption,
       (options, value) => { options.UseJavadocLikeDocstringRewriter = value; });
     DafnyOptions.RegisterLegacyBinding(WarnShadowing, (options, value) => { options.WarnShadowing = value; });
@@ -252,6 +259,7 @@ static CommonOptionBag() {
       }
     });
     DafnyOptions.RegisterLegacyBinding(SolverLog, (o, v) => o.ProverLogFilePath = v);
+    DafnyOptions.RegisterLegacyBinding(SpillTranslation, (o, f) => o.SpillTargetCode = f ? 1U : 0U);
 
     DafnyOptions.RegisterLegacyBinding(EnforceDeterminism, (options, value) => {
       options.ForbidNondeterminism = value;

Source/DafnyCore/Options/DeveloperOptionBag.cs

@@ -5,15 +5,6 @@ namespace Microsoft.Dafny;
 
 public class DeveloperOptionBag {
 
-  public static readonly Option<bool> SpillTranslation = new("--spill-translation",
-    @"In case the Dafny source code is translated to another language, emit that translation.") {
-    IsHidden = true
-  };
-
-  public static readonly Option<bool> UseBaseFileName = new("--use-basename-for-filename",
-    "When parsing use basename of file for tokens instead of the path supplied on the command line") {
-  };
-
   public static readonly Option<string> BoogiePrint = new("--bprint",
   @"
 Print Boogie program translated from Dafny
@@ -44,7 +35,6 @@ Print Dafny program after resolving it.
   };
 
   static DeveloperOptionBag() {
-    DafnyOptions.RegisterLegacyBinding(SpillTranslation, (o, f) => o.SpillTargetCode = f ? 1U : 0U);
 
     DafnyOptions.RegisterLegacyBinding(ResolvedPrint, (options, value) => {
       options.DafnyPrintResolvedFile = value;
@@ -58,7 +48,6 @@ static DeveloperOptionBag() {
         options.FileTimestamp);
     });
 
-    DafnyOptions.RegisterLegacyBinding(UseBaseFileName, (o, f) => o.UseBaseNameForFileName = f);
     DafnyOptions.RegisterLegacyBinding(BoogiePrint, (options, f) => {
       options.PrintFile = f;
       options.ExpandFilename(options.PrintFile, x => options.PrintFile = x, options.LogPrefix,

Source/DafnyCore/Options/ICommandSpec.cs

@@ -24,7 +24,6 @@ static ICommandSpec() {
     CommonOptionBag.Check,
     CommonOptionBag.Verbose,
     CommonOptionBag.FormatPrint,
-    DeveloperOptionBag.UseBaseFileName
   }.Concat(ParserOptions);
 
   public static IReadOnlyList<Option> VerificationOptions = new Option[] {
@@ -53,12 +52,11 @@ static ICommandSpec() {
 
   public static IReadOnlyList<Option> ExecutionOptions = new Option[] {
     CommonOptionBag.Target,
-    DeveloperOptionBag.SpillTranslation
+    CommonOptionBag.SpillTranslation
   }.Concat(TranslationOptions).ToList();
 
   public static IReadOnlyList<Option> ConsoleOutputOptions = new List<Option>(new Option[] {
     DafnyConsolePrinter.ShowSnippets,
-    DeveloperOptionBag.UseBaseFileName,
     DeveloperOptionBag.Print,
     DeveloperOptionBag.ResolvedPrint,
     DeveloperOptionBag.BoogiePrint,
@@ -75,6 +73,7 @@ static ICommandSpec() {
     Function.FunctionSyntaxOption,
     CommonOptionBag.QuantifierSyntax,
     CommonOptionBag.UnicodeCharacters,
+    CommonOptionBag.UseBaseFileName,
     CommonOptionBag.TypeSystemRefresh,
     CommonOptionBag.ErrorLimit,
   });

Source/DafnyCore/Resolver/RunAllTestsMainMethod.cs

@@ -2,11 +2,17 @@
 using System.Diagnostics.Contracts;
 using System.Linq;
 using Microsoft.Boogie;
+using System.Text.RegularExpressions;
 
 namespace Microsoft.Dafny; 
 
 public class RunAllTestsMainMethod : IRewriter {
 
+  /** The name used for Main when executing tests. Should be a name that cannot be a Dafny name,
+      that Dafny will not use as a mangled Dafny name for any backend, and that is not likely
+      to be chosen by the user as an extern name. **/
+  public static string SyntheticTestMainName = "_Test__Main_";
+
   public RunAllTestsMainMethod(ErrorReporter reporter) : base(reporter) {
   }
 
@@ -19,17 +25,12 @@ public RunAllTestsMainMethod(ErrorReporter reporter) : base(reporter) {
   /// errors much earlier in the pipeline.
   /// </summary>
   internal override void PreResolve(Program program) {
-    var hasMain = Compilers.SinglePassCompiler.HasMain(program, out var mainMethod);
-    if (hasMain) {
-      Reporter.Error(MessageSource.Rewriter, mainMethod.tok, "Cannot use /runAllTests on a program with a main method");
-      return;
-    }
 
     // Verifying the method isn't yet possible since the translation of try/recover statments is not implemented,
     // and would be low-value anyway.
     var noVerifyAttribute = new Attributes("verify", new List<Expression> { new LiteralExpr(Token.NoToken, false) }, null);
 
-    mainMethod = new Method(RangeToken.NoToken, new Name("Main"), false, false,
+    var mainMethod = new Method(RangeToken.NoToken, new Name(SyntheticTestMainName), false, false,
       new List<TypeParameter>(), new List<Formal>(), new List<Formal>(),
       new List<AttributedExpression>(),
       new Specification<FrameExpression>(new List<FrameExpression>(), null),
@@ -98,6 +99,12 @@ internal override void PostResolve(Program program) {
     foreach (var moduleDefinition in program.CompileModules) {
       foreach (var callable in ModuleDefinition.AllCallables(moduleDefinition.TopLevelDecls)) {
         if ((callable is Method method) && Attributes.Contains(method.Attributes, "test")) {
+          var regex = program.Options.MethodsToTest;
+          if (regex != null) {
+            string name = method.FullDafnyName;
+            if (!Regex.Match(name, regex).Success) continue;
+          }
+
           // print "TestMethod: ";
           mainMethodStatements.Add(Statement.CreatePrintStmt(tok,
             Expression.CreateStringLiteral(tok, $"{method.FullDafnyName}: ")));

Source/DafnyDriver/Commands/TestCommand.cs

@@ -8,10 +8,21 @@ namespace Microsoft.Dafny;
 public class TestCommand : ICommandSpec {
   public IEnumerable<Option> Options =>
     new Option[] {
+      CommonOptionBag.Output,
+      MethodsToTest,
     }.Concat(ICommandSpec.ExecutionOptions).
       Concat(ICommandSpec.ConsoleOutputOptions).
       Concat(ICommandSpec.ResolverOptions);
 
+  public static readonly Option<string> MethodsToTest = new("--methods-to-test",
+    "A regex (over fully qualified names) selecting which methods or functions to test") {
+  };
+
+  static TestCommand() {
+    DafnyOptions.RegisterLegacyBinding(MethodsToTest, (o, v) => { o.MethodsToTest = v; });
+  }
+
+
   public Command Create() {
     var result = new Command("test", "(Experimental) Execute every method in the program that's annotated with the {:test} attribute.");
     result.AddArgument(ICommandSpec.FilesArgument);
@@ -24,5 +35,6 @@ public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationCo
     dafnyOptions.RunAllTests = true;
     dafnyOptions.ForceCompile = dafnyOptions.Get(BoogieOptionBag.NoVerify);
     dafnyOptions.CompileVerbose = false;
+    dafnyOptions.MainMethod = RunAllTestsMainMethod.SyntheticTestMainName;
   }
 }

Test/git-issues/git-issue-3221.dfy

@@ -0,0 +1,27 @@
+// RUN: %baredafny test "%s" > "%t"
+// RUN: %baredafny test --methods-to-test='q' "%s" >> "%t"
+// RUN: %baredafny test --methods-to-test='m' "%s" >> "%t"
+// RUN: %baredafny test --methods-to-test='M.*' "%s" >> "%t"
+// RUN: %baredafny test --methods-to-test='^.$' "%s" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method {:test} m() {
+  print "Testing m\n";
+}
+method {:test} q() {
+  print "Testing q\n";
+}
+method {:test} pp() {
+  print "Testing pp\n";
+}
+
+module M {
+
+  method {:test} m() {
+    print "Testing M.m\n";
+  }
+  method {:test} t() {
+    print "Testing M.t\n";
+  }
+}
+

Test/git-issues/git-issue-3221.dfy.expect

@@ -0,0 +1,34 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
+M.m: Testing M.m
+PASSED
+M.t: Testing M.t
+PASSED
+m: Testing m
+PASSED
+q: Testing q
+PASSED
+pp: Testing pp
+PASSED
+
+Dafny program verifier finished with 0 verified, 0 errors
+q: Testing q
+PASSED
+
+Dafny program verifier finished with 0 verified, 0 errors
+M.m: Testing M.m
+PASSED
+m: Testing m
+PASSED
+
+Dafny program verifier finished with 0 verified, 0 errors
+M.m: Testing M.m
+PASSED
+M.t: Testing M.t
+PASSED
+
+Dafny program verifier finished with 0 verified, 0 errors
+m: Testing m
+PASSED
+q: Testing q
+PASSED

Test/git-issues/git-issue-3744.dfy

@@ -0,0 +1,11 @@
+// RUN: %baredafny test "%s" > "%t"
+// RUN: %baredafny run "%s" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main() {
+  print "Main\n";
+}
+
+method {:test} Test() {
+  print "Test\n";
+}

Test/git-issues/git-issue-3744.dfy.expect

@@ -0,0 +1,7 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
+Test: Test
+PASSED
+
+Dafny program verifier finished with 0 verified, 0 errors
+Main

docs/DafnyRef/UserGuide.md

@@ -434,11 +434,16 @@ errors or if --check is stipulated and at least one file is not the same as its
 
 #### 13.5.1.10. `dafny test` {#sec-dafny-test}
 
-This _experimental_ command (verifies and compiles the program and) runs every method in the program that is annotated with the `{:test}` attribute.
+This command (verifies and compiles the program and) runs every method in the program that is annotated with the `{:test}` attribute.
 Verification can be disabled using the `--no-verify` option. `dafny test` also accepts all other options of the `dafny build` command. 
 In particular, it accepts the `--target` option that specifies the programming language used in the build and execution phases.
 
-There are currently no other options specific to the `dafny test` command.
+`dafny test` also accepts these options:
+
+- `-spill-translation` - (default disabled) when enabled the compilation artifacts are retained
+- `--output` - gives the folder and filename root for compilation artifacts
+- `--methods-to-test` - the value is a (.NET) regular expression that is matched against the fully
+  qualified name of the method; only those methods that match are tested
 
 The order in which the tests are run is not specified.
 
@@ -479,6 +484,17 @@ Hi!
 PASSED
 ```
 
+and this command-line
+```bash
+dafny test --no-verify --methods-to-test='m' t.dfy
+```
+produces this output text:
+```text
+m: mm
+Hi!
+PASSED
+```
+
 #### 13.5.1.11. `dafny generate-tests` {#sec-dafny-generate-tests}
 
 This _experimental_ command (verifies the program and) then generates unit test code (as Dafny source code) that provides

docs/dev/news/3221.fix

@@ -0,0 +1 @@
+* dafny test accepts a --methods-to-test option whose value is a regular expression selecting which tests to include in the test run

docs/dev/news/3612.feat

@@ -0,0 +1,2 @@
+* Exposes the --output and --spill-translation options for the dafny test command
+

docs/dev/news/3744.fix

@@ -0,0 +1 @@
+* Main and {:test} methods may now be in the same program