Allow including a test runner using 'dafny translate'

Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs

@@ -3393,7 +3393,7 @@ protected override void EmitSingleValueGenerator(Expression e, bool inLetExprBod
     }
 
     private void AddTestCheckerIfNeeded(string name, Declaration decl, ConcreteSyntaxTree wr) {
-      if (Options.Compile || Options.RunAllTests || !Attributes.Contains(decl.Attributes, "test")) {
+      if (Options.Compile || Options.Get(RunAllTestsMainMethod.IncludeTestRunner) || !Attributes.Contains(decl.Attributes, "test")) {
         return;
       }
 

Source/DafnyCore/DafnyOptions.cs

@@ -261,7 +261,6 @@ public enum ContractTestingMode {
     public string DafnyPrintCompiledFile = null;
     public string CoverageLegendFile = null;
     public string MainMethod = null;
-    public bool RunAllTests = false;
     public bool ForceCompile = false;
     public bool RunAfterCompile = false;
     public uint SpillTargetCode = 0; // [0..4]
@@ -469,15 +468,6 @@ protected bool ParseDafnySpecificOption(string name, Bpl.CommandLineParseState p
             return true;
           }
 
-        case "runAllTests": {
-            int runAllTests = 0;
-            if (ps.GetIntArgument(ref runAllTests, 2)) {
-              RunAllTests = runAllTests != 0; // convert to boolean
-            }
-
-            return true;
-          }
-
         case "dafnyVerify": {
             int verify = 0;
             if (ps.GetIntArgument(ref verify, 2)) {
@@ -1444,15 +1434,6 @@ A Main method can have at most one (non-ghost) argument of type `seq<string>`
     When running a Dafny file through /compile:3 or /compile:4, '--args' provides
     all arguments after it to the Main function, at index starting at 1.
     Index 0 is used to store the executable's name if it exists.
-/runAllTests:<n> (experimental)
-    0 (default) - Annotates compiled methods with the {{:test}}
-        attribute such that they can be tested using a testing framework
-        in the target language (e.g. xUnit for C#).
-    1 - Emits a main method in the target language that will execute
-        every method in the program with the {{:test}} attribute. Cannot
-        be used if the program already contains a main method. Note that
-        /compile:3 or 4 must be provided as well to actually execute
-        this main method!
 
 /compileVerbose:<n>
     0 - Don't print status of compilation to the console.

Source/DafnyCore/Rewriters/RewriterCollection.cs

@@ -29,7 +29,7 @@ public static IList<IRewriter> GetRewriters(ErrorReporter reporter, Program prog
       result.Add(new ExpectContracts(reporter));
     }
 
-    if (reporter.Options.RunAllTests) {
+    if (reporter.Options.Get(RunAllTestsMainMethod.IncludeTestRunner)) {
       result.Add(new RunAllTestsMainMethod(reporter));
     }
 

Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs

@@ -1,13 +1,22 @@
 using System.Collections.Generic;
+using System.CommandLine;
 using System.Diagnostics.Contracts;
 using System.Linq;
 using System.Text.RegularExpressions;
+using DafnyCore;
 using static Microsoft.Dafny.RewriterErrors;
 
 namespace Microsoft.Dafny;
 
 public class RunAllTestsMainMethod : IRewriter {
 
+  static RunAllTestsMainMethod() {
+    DooFile.RegisterNoChecksNeeded(IncludeTestRunner);
+  }
+
+  public static Option<bool> IncludeTestRunner = new("--include-test-runner",
+    "Include a program entry point that will run all methods marked with {:test}");
+
   /** 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. **/

Source/DafnyDriver/Commands/TestCommand.cs

@@ -5,6 +5,22 @@
 namespace Microsoft.Dafny;
 
 static class TestCommand {
+
+  static TestCommand() {
+    DafnyOptions.RegisterLegacyBinding(MethodsToTest, (o, v) => { o.MethodsToTest = v; });
+
+    DooFile.RegisterNoChecksNeeded(MethodsToTest);
+
+    DafnyOptions.RegisterLegacyUi(RunAllTestsMainMethod.IncludeTestRunner, DafnyOptions.ParseBoolean, "Compilation options", "runAllTests", @"0 (default) - Annotates compiled methods with the {:test}
+        attribute such that they can be tested using a testing framework
+        in the target language (e.g. xUnit for C#).
+    1 - Emits a main method in the target language that will execute
+        every method in the program with the {:test} attribute. Cannot
+        be used if the program already contains a main method. Note that
+        /compile:3 or 4 must be provided as well to actually execute
+        this main method!", argumentName: "n");
+  }
+
   public static IEnumerable<Option> Options =>
     new Option[] {
       CommonOptionBag.Output,
@@ -17,13 +33,6 @@ static class TestCommand {
     "A regex (over fully qualified names) selecting which methods or functions to test") {
   };
 
-  static TestCommand() {
-    DafnyOptions.RegisterLegacyBinding(MethodsToTest, (o, v) => { o.MethodsToTest = v; });
-
-    DooFile.RegisterNoChecksNeeded(MethodsToTest);
-  }
-
-
   public static Command Create() {
     var result = new Command("test", "(Experimental) Execute every method in the program that's annotated with the {:test} attribute.");
     result.AddArgument(DafnyCommands.FilesArgument);
@@ -34,7 +43,7 @@ public static Command Create() {
     DafnyCli.SetHandlerUsingDafnyOptionsContinuation(result, (options, _) => {
       options.Compile = true;
       options.RunAfterCompile = true;
-      options.RunAllTests = true;
+      options.Set(RunAllTestsMainMethod.IncludeTestRunner, true);
       options.ForceCompile = options.Get(BoogieOptionBag.NoVerify);
       options.MainMethod = RunAllTestsMainMethod.SyntheticTestMainName;
       return CompilerDriver.RunCompiler(options);

Source/DafnyDriver/Commands/TranslateCommand.cs

@@ -8,11 +8,15 @@ namespace Microsoft.Dafny;
 
 static class TranslateCommand {
 
+  static TranslateCommand() {
+  }
+
   public static IEnumerable<Option> Options =>
     new Option[] {
       CommonOptionBag.Output,
       IExecutableBackend.OuterModule,
       CommonOptionBag.IncludeRuntimeOption,
+      RunAllTestsMainMethod.IncludeTestRunner
     }.Concat(DafnyCommands.TranslationOptions).
       Concat(DafnyCommands.ConsoleOutputOptions).
       Concat(DafnyCommands.ResolverOptions);

Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTests.csproj

@@ -0,0 +1,11 @@
+<?xml version="1.0" encoding="utf-8"?>
+<Project Sdk="Microsoft.NET.Sdk">
+  <PropertyGroup>
+    <OutputType>Exe</OutputType>
+    <TargetFramework>net6.0</TargetFramework>
+    <EnableDefaultItems>false</EnableDefaultItems>
+  </PropertyGroup>
+  <ItemGroup>
+    <Compile Include="Output/manual/program.cs" />
+  </ItemGroup>
+</Project>

Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTestsOption.dfy → Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTestsOption.dfy

@@ -1,13 +1,15 @@
 // RUN: %verify "%s" > "%t"
+// RUN: %translate cs %args %s --include-runtime --include-test-runner --unicode-char false --no-verify --output %S/Output/manual/program.cs >> "%t"
+// RUN: ! dotnet run -v q --property WarningLevel=0 --project %S/RunAllTests.csproj >> "%t"
 // RUN: ! %baredafny test %args --unicode-char:false --no-verify --target:cs "%s" >> "%t"
 // RUN: ! %baredafny test %args --unicode-char:false --no-verify --target:java "%s" >> "%t"
 // RUN: ! %baredafny test %args --unicode-char:false --no-verify --target:go "%s" >> "%t"
 // RUN: ! %baredafny test %args --unicode-char:false --no-verify --target:js "%s" >> "%t"
 // RUN: ! %baredafny test %args --unicode-char:false --no-verify --target:py "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t" 
 
-include "../exceptions/VoidOutcomeDt.dfy"
-include "../exceptions/NatOutcomeDt.dfy"
+include "../../exceptions/VoidOutcomeDt.dfy"
+include "../../exceptions/NatOutcomeDt.dfy"
 
 method {:test} Passing1() {
   expect 2 == 2;

Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTestsOption.dfy.expect

@@ -0,0 +1,86 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
+
+Dafny program verifier did not attempt verification
+TestModule.Passing1: PASSED
+Passing1: PASSED
+Passing2: PASSED
+Failing1: FAILED
+	RunAllTestsOption.dfy(23,2): expectation violation
+Passing3: PASSED
+Failing2: FAILED
+	RunAllTestsOption.dfy(31,2): expectation violation
+FailingReturnValue: FAILED
+	VoidOutcome.VoidFailure(Whoopsie)
+[Program halted] RunAllTestsOption.dfy(11,0): Test failures occurred: see above.
+
+
+Dafny program verifier did not attempt verification
+TestModule.Passing1: PASSED
+Passing1: PASSED
+Passing2: PASSED
+Failing1: FAILED
+	RunAllTestsOption.dfy(23,2): expectation violation
+Passing3: PASSED
+Failing2: FAILED
+	RunAllTestsOption.dfy(31,2): expectation violation
+FailingReturnValue: FAILED
+	VoidOutcome.VoidFailure(Whoopsie)
+[Program halted] RunAllTestsOption.dfy(11,0): Test failures occurred: see above.
+
+
+Dafny program verifier did not attempt verification
+TestModule.Passing1: PASSED
+Passing1: PASSED
+Passing2: PASSED
+Failing1: FAILED
+	RunAllTestsOption.dfy(23,2): expectation violation
+Passing3: PASSED
+Failing2: FAILED
+	RunAllTestsOption.dfy(31,2): expectation violation
+FailingReturnValue: FAILED
+	VoidOutcome.VoidFailure(Whoopsie)
+[Program halted] RunAllTestsOption.dfy(11,0): Test failures occurred: see above.
+
+
+Dafny program verifier did not attempt verification
+TestModule.Passing1: PASSED
+Passing1: PASSED
+Passing2: PASSED
+Failing1: FAILED
+	RunAllTestsOption.dfy(23,2): expectation violation
+Passing3: PASSED
+Failing2: FAILED
+	RunAllTestsOption.dfy(31,2): expectation violation
+FailingReturnValue: FAILED
+	VoidOutcome.VoidFailure(Whoopsie)
+[Program halted] RunAllTestsOption.dfy(11,0): Test failures occurred: see above.
+
+
+Dafny program verifier did not attempt verification
+TestModule.Passing1: PASSED
+Passing1: PASSED
+Passing2: PASSED
+Failing1: FAILED
+	RunAllTestsOption.dfy(23,2): expectation violation
+Passing3: PASSED
+Failing2: FAILED
+	RunAllTestsOption.dfy(31,2): expectation violation
+FailingReturnValue: FAILED
+	VoidOutcome.VoidFailure(Whoopsie)
+[Program halted] RunAllTestsOption.dfy(11,0): Test failures occurred: see above.
+
+
+Dafny program verifier did not attempt verification
+TestModule.Passing1: PASSED
+Passing1: PASSED
+Passing2: PASSED
+Failing1: FAILED
+	RunAllTestsOption.dfy(23,2): expectation violation
+Passing3: PASSED
+Failing2: FAILED
+	RunAllTestsOption.dfy(31,2): expectation violation
+FailingReturnValue: FAILED
+	VoidOutcome.VoidFailure(Whoopsie)
+[Program halted] RunAllTestsOption.dfy(11,0): Test failures occurred: see above.
+

Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/TestAttribute.dfy → Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/TestAttribute/TestAttribute.dfy

@@ -1,20 +1,20 @@
 // RUN: %exits-with 3 %dafny /compileVerbose:1 /compile:0 /spillTargetCode:3 /noVerify "%s" > "%t"
-// RUN: ! dotnet test -v:q %S 2>> %t
+// RUN: ! dotnet test -v:q %S/TestAttribute.csproj 2>> %t
 //
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 // CHECK: .*Error: Post-conditions on function Identity might be unsatisfied when synthesizing code for method mockUnsafe.*
 // CHECK: .*Error: Stubbing fields is not recommended \(field value of object e inside method MockField\).*
 // CHECK: .*Error: Stubbing fields is not recommended \(field value of object e inside method ParametrizedMock\).*
-// CHECK: .*_module.__default.FailingTest_CheckForFailureForXunit.*
 // CHECK: .*_module.__default.FailingTestUsingMock.*
-// CHECK: .*_module.__default.FailingTestUsingExpectWithMessage.*
-// CHECK: .*_module.__default.FailingTestUsingExpect.*
 // CHECK: .*_module.__default.FailingTestUsingNoLHSAssignOrHalt.*
+// CHECK: .*_module.__default.FailingTestUsingExpectWithMessage.*
+// CHECK: .*_module.__default.FailingTest_CheckForFailureForXunit.*
 // CHECK: .*_module.__default.FailingTestUsingAssignOrHalt.*
+// CHECK: .*_module.__default.FailingTestUsingExpect.*
 // CHECK-NOT: .*PassingTest.*
 
-include "../exceptions/VoidOutcomeDt.dfy"
-include "../exceptions/NatOutcomeDt.dfy"
+include "../../exceptions/VoidOutcomeDt.dfy"
+include "../../exceptions/NatOutcomeDt.dfy"
 
 function SafeDivide(a: nat, b: nat): NatOutcome {
   if b == 0 then

Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/DafnyTests/RunAllTestsOption.dfy

@@ -5,4 +5,4 @@
 // RUN: ! %baredafny test %args --unicode-char --no-verify --target:js "%s" >> "%t"
 // RUN: ! %baredafny test %args --unicode-char --no-verify --target:py "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t" 
-include "../../DafnyTests/RunAllTestsOption.dfy"
+include "../../DafnyTests/RunAllTests/RunAllTestsOption.dfy"