chore: xUnit-based lit test runner (#680)

Adds an xUnit-based test runner for all of the lit tests under Test.

The new runner supports executing commands such as %dafny by directly invoking the main entry point of the corresponding C# package (i.e. DafnyDriver), which makes running the debugger against a particular test much more convenient. By default this is disabled and the runner creates a separate dafny process just as lit does, however. This is because the main CLI implementation currently has shared static state, which causes errors when invoking the CLI in the same process on multiple inputs in sequence, much less in parallel. Future changes will address this so that the in-process Main invocation can be used instead, however, which will likely improve performance but more importantly allow us to measure code coverage of the test suite.

Where this alternate runner really shines is in IDEs that support .NET test frameworks:

Getting a tree of test results in the UI
Being able to re-run/debug individual tests by right-clicking on them
Filtering by test name (e.g. dotnet test --filter DisplayName~allocated)
(Earlier versions of this PR went further and aimed to convert the lit tests to a new format. We may still want to do this in the future, but parsing and understanding the existing test suite is a necessary prerequisite anyway.)

This change adds two new .NET packages:

XUnitExtensions - Contains a few generic extensions to xUnit to support file-based parameterized tests (a.k.a. Theories), and the alternate Lit test interpreter.
IntegrationTests - Contains a single file-based parameterized xUnit test to run all lit tests in the Test directory.
Other .NET projects that use lit, such as Boogie, could also leverage this runner by depending on the generic XUnitExtensions package and defining a similar second package.

There is one fundamental difference in behavior between the two runners: our current lit configuration uses the immediate directory of each test case as the current directory, whereas .NET test runners always run in the single project output directory (e.g. IntegrationTests/bin/Debug/net5.0). It wouldn't be feasible to change the current directory to match lit's behavior, since multiple parallel tests cannot do this at the same time. Instead, I prepended the %S substitution macro to a handful of command arguments that were relative paths, and otherwise ensured the tests did not depend on the current directory.

Because the IntegrationTests package runs all tests out of the output directory rather than the Test directory, its csproj configuration and its dependencies ensure that a few additional files are also copied into that directory, such as z3 and the necessary runtime files. I also applied this technique to the other test projects to avoid the manual step of copying z3 as described in the wiki (and will remove that step once this PR is merged).

Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com>
Co-authored-by: Remy Willems <rgv.willems@gmail.com>

.github/workflows/msbuild.yml

@@ -124,7 +124,6 @@ jobs:
  - if: runner.os != 'Windows'
  run: |
  unzip dafny/Package/CI.zip -d unzippedRelease
- - name: Run lit tests
+ - name: Run integration tests
  run: |
- ## lit in this context needs the executables specified
- lit --time-tests -v --num-shards=5 --run-shard=${{ matrix.shard }} --param executable=$PWD/unzippedRelease/dafny/dafny --param serverExecutable=$PWD/unzippedRelease/dafny/DafnyServer dafny/Test
+ XUNIT_SHARD=${{ matrix.shard }} XUNIT_SHARD_COUNT=5 DAFNY_RELEASE=$PWD/unzippedRelease/dafny dotnet test -v:n dafny/Source/IntegrationTests/IntegrationTests.csproj

.github/workflows/xunit-tests.yml

@@ -30,9 +30,6 @@ jobs:
  chmod: true
  coverage: false
  env:
- testPath1: Source/DafnyLanguageServer.Test/bin/Debug/net5.0
- testPath2: Source/DafnyPipeline.Test/bin/Debug/net5.0
- testPath3: Source/DafnyTestGeneration.Test/bin/Debug/net5.0
  solutionPath: Source/Dafny.sln
  z3BaseUri: https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5
  steps:
@@ -45,22 +42,22 @@ jobs:
  dotnet-version: 5.0.x
  - name: Install dependencies
  run: dotnet restore ${{env.solutionPath}}
- - name: Build
- run: dotnet build --no-restore ${{env.solutionPath}}
  - name: Load Z3
  shell: pwsh
  run: |
  Invoke-WebRequest ${{env.z3BaseUri}}/${{matrix.z3}}.zip -OutFile z3.zip
  Expand-Archive z3.zip .
  Remove-Item z3.zip
- Copy-Item ${{matrix.z3}} ${{env.testPath1}}/z3 -Recurse
- Copy-Item ${{matrix.z3}} ${{env.testPath2}}/z3 -Recurse
- Copy-Item ${{matrix.z3}} ${{env.testPath3}}/z3 -Recurse
+ Copy-Item ${{matrix.z3}} Binaries/z3 -Recurse
  - name: Set Z3 Permissions
  if: ${{matrix.chmod}}
- run: | 
- chmod +x ${{env.testPath1}}/z3/bin/z3
- chmod +x ${{env.testPath2}}/z3/bin/z3
- chmod +x ${{env.testPath3}}/z3/bin/z3
- - name: Run Tests
- run: dotnet test --no-restore --verbosity normal ${{env.solutionPath}}
+ run: |
+ chmod +x Binaries/z3/bin/z3
+ - name: Build
+ run: dotnet build --no-restore ${{env.solutionPath}}
+ - name: Run DafnyLanguageServer Tests
+ run: dotnet test --no-restore --verbosity normal Source/DafnyLanguageServer.Test
+ - name: Run DafnyPipeline Tests
+ run: dotnet test --no-restore --verbosity normal Source/DafnyPipeline.Test
+ - name: Run DafnyTestGeneration Tests
+ run: dotnet test --no-restore --verbosity normal Source/DafnyTestGeneration.Test

Scripts/package.py

@@ -47,8 +47,6 @@
 ## On unix systems, which Dafny files should be marked as executable? (Glob syntax; Z3's permissions are preserved)
 UNIX_EXECUTABLES = ["dafny", "dafny-server"]
 
-ETCs = ["DafnyRuntime.js", "DafnyRuntime.go", "DafnyRuntime.jar", "DafnyRuntime.h"]
-
 # Constants
 
 THIS_FILE = path.realpath(__file__)
@@ -125,7 +123,6 @@ def build(self):
  if path.exists(self.buildDirectory):
  shutil.rmtree(self.buildDirectory)
  run(["make", "--quiet", "clean"])
- run(["make", "--quiet", "runtime"])
  run(["dotnet", "publish", path.join(SOURCE_DIRECTORY, "DafnyLanguageServer", "DafnyLanguageServer.csproj"),
  "--nologo",
  "-f", "net5.0",
@@ -166,7 +163,7 @@ def pack(self):
  lowercaseDafny = path.join(self.buildDirectory, "dafny")
  shutil.move(uppercaseDafny, lowercaseDafny)
  os.chmod(lowercaseDafny, stat.S_IEXEC| os.lstat(lowercaseDafny).st_mode)
- paths = pathsInDirectory(self.buildDirectory) + list(map(lambda etc: path.join(BINARIES_DIRECTORY, etc), ETCs)) + OTHERS
+ paths = pathsInDirectory(self.buildDirectory) + OTHERS
  for fpath in paths:
  if os.path.isdir(fpath):
  continue

Source/Dafny.sln

@@ -7,6 +7,8 @@ Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "DafnyRuntime", "DafnyRuntim
 EndProject
 Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "DafnyPipeline", "Dafny\DafnyPipeline.csproj", "{45FFD363-CFE0-4ABC-984F-7EB58C8BEDE5}"
 EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyPipeline.Test", "DafnyPipeline.Test\DafnyPipeline.Test.csproj", "{FA2A3A73-3035-497B-B9D7-B6BC4888A058}"
+EndProject
 Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "DafnyDriver", "DafnyDriver\DafnyDriver.csproj", "{4B74F970-8FEB-46A1-BD14-FBF2B5D5F285}"
 EndProject
 Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "DafnyServer", "DafnyServer\DafnyServer.csproj", "{71208DB9-31D6-4071-838B-8D44A37CF0F1}"
@@ -16,11 +18,13 @@ Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Solution Items", "Solution
  version.cs = version.cs
  EndProjectSection
 EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "IntegrationTests", "IntegrationTests\IntegrationTests.csproj", "{A4BC2C77-3A48-4917-AA22-41978DFFE24E}"
+EndProject
 Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "DafnyLanguageServer", "DafnyLanguageServer\DafnyLanguageServer.csproj", "{CD05D26C-C672-4F43-835E-7A3E1741E4D8}"
 EndProject
 Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "DafnyLanguageServer.Test", "DafnyLanguageServer.Test\DafnyLanguageServer.Test.csproj", "{320C02A3-D3E6-4AC7-A7E2-170AF86A6EEC}"
 EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyPipeline.Test", "DafnyPipeline.Test\DafnyPipeline.Test.csproj", "{FA2A3A73-3035-497B-B9D7-B6BC4888A058}"
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "XUnitExtensions", "XUnitExtensions\XUnitExtensions.csproj", "{43731A57-DBA9-43AC-BC83-A9211DA7EB77}"
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyTestGeneration", "DafnyTestGeneration\DafnyTestGeneration.csproj", "{229E0F23-2B99-4331-8BD8-C2EBCB7C9DAC}"
 EndProject
@@ -60,6 +64,14 @@ Global
  {FA2A3A73-3035-497B-B9D7-B6BC4888A058}.Debug|Any CPU.Build.0 = Debug|Any CPU
  {FA2A3A73-3035-497B-B9D7-B6BC4888A058}.Release|Any CPU.ActiveCfg = Release|Any CPU
  {FA2A3A73-3035-497B-B9D7-B6BC4888A058}.Release|Any CPU.Build.0 = Release|Any CPU
+ {A4BC2C77-3A48-4917-AA22-41978DFFE24E}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {A4BC2C77-3A48-4917-AA22-41978DFFE24E}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {896E7F24-FD59-4B34-A1BF-41978DFFE24E}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {896E7F24-FD59-4B34-A1BF-41978DFFE24E}.Release|Any CPU.Build.0 = Release|Any CPU
+ {43731A57-DBA9-43AC-BC83-A9211DA7EB77}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {43731A57-DBA9-43AC-BC83-A9211DA7EB77}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {43731A57-DBA9-43AC-BC83-A9211DA7EB77}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {43731A57-DBA9-43AC-BC83-A9211DA7EB77}.Release|Any CPU.Build.0 = Release|Any CPU
  {229E0F23-2B99-4331-8BD8-C2EBCB7C9DAC}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
  {229E0F23-2B99-4331-8BD8-C2EBCB7C9DAC}.Debug|Any CPU.Build.0 = Debug|Any CPU
  {229E0F23-2B99-4331-8BD8-C2EBCB7C9DAC}.Release|Any CPU.ActiveCfg = Release|Any CPU

Source/Dafny/Compilers/Compiler-cpp.cs

@@ -2387,8 +2387,7 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target
  CreateNoWindow = true,
  UseShellExecute = false,
  RedirectStandardOutput = true,
- RedirectStandardError = true,
- WorkingDirectory = Path.GetDirectoryName(Path.GetFullPath(targetFilename))
+ RedirectStandardError = true
  };
  var proc = Process.Start(psi);
  while (!proc.StandardOutput.EndOfStream) {
@@ -2408,14 +2407,11 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target
  public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string targetFilename, ReadOnlyCollection<string> otherFileNames,
  object compilationResult, TextWriter outputWriter) {
  var exeName = ComputeExeName(targetFilename);
- var dir = Path.GetDirectoryName(Path.GetFullPath(targetFilename));
- var exePath = Path.Combine(dir, exeName);
- var psi = new ProcessStartInfo(exePath) {
+ var psi = new ProcessStartInfo(exeName) {
  CreateNoWindow = true,
  UseShellExecute = false,
  RedirectStandardOutput = true,
  RedirectStandardError = true,
- WorkingDirectory = dir
  };
  var proc = Process.Start(psi);
  while (!proc.StandardOutput.EndOfStream) {

Source/Dafny/Dafny.atg

@@ -875,7 +875,10 @@ Dafny
  { TopDecl<defaultModule, membersDefaultClass, /* isTopLevel */ true, /* isAbstract */ false> }
  (. // find the default class in the default module, then append membersDefaultClass to its member list
  if (membersDefaultClass.Count == 0 && defaultModule.Includes.Count == 0 && defaultModule.TopLevelDecls.Count == 0) {
- errors.Warning(defaultModule.tok, "File contains no code: " + Path.GetRelativePath(Directory.GetCurrentDirectory(), scanner.FullFilename));
+ var fileName = DafnyOptions.Clo.UseBaseNameForFileName 
+ ? Path.GetFileName(scanner.FullFilename) 
+ : Path.GetRelativePath(Directory.GetCurrentDirectory(), scanner.FullFilename);
+ errors.Warning(defaultModule.tok, "File contains no code: " + fileName);
  }
  DefaultClassDecl defaultClass = null;
  foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {

Source/Dafny/DafnyPipeline.csproj

@@ -34,10 +34,7 @@
  <ItemGroup>
  <Compile Include="..\version.cs" />
  </ItemGroup>
-
  <ItemGroup>
- <None Update="DafnyPrelude.bpl">
- <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
- </None>
+ <Content Include="DafnyPrelude.bpl" CopyToOutputDirectory="PreserveNewest" />
  </ItemGroup>
 </Project>

Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj

@@ -21,6 +21,10 @@
  </ItemGroup>
 
  <ItemGroup>
+ <Content Include="..\..\Binaries\z3\**\*.*" LinkBase="z3">
+ <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
+ </Content>
+
  <None Update="Lookup\TestFiles\foreign.dfy">
  <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
  </None>

Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj

@@ -24,4 +24,10 @@
  <ProjectReference Include="..\Dafny\DafnyPipeline.csproj" />
  </ItemGroup>
 
+ <ItemGroup>
+ <Content Include="..\..\Binaries\z3\**\*.*" LinkBase="z3">
+ <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
+ </Content>
+ </ItemGroup>
+
 </Project>

Source/DafnyRuntime/DafnyRuntime.csproj

@@ -20,6 +20,31 @@
  <Compile Update="DafnyRuntime.cs">
  <CopyToOutputDirectory>Always</CopyToOutputDirectory>
  </Compile>
+ <Content Include="DafnyRuntime.js" CopyToOutputDirectory="PreserveNewest" />
+ <Content Include="DafnyRuntime.go" CopyToOutputDirectory="PreserveNewest" />
+ <Content Include="DafnyRuntime.h" CopyToOutputDirectory="PreserveNewest" />
+ <Content Include="DafnyRuntimeJava\build\libs\DafnyRuntime.jar" Link="DafnyRuntime.jar" CopyToOutputDirectory="PreserveNewest" />
  </ItemGroup>
 
+ <ItemGroup>
+ <DafnyRuntimeJavaInputFile Include="./DafnyRuntimeJava/**/*.*" />
+ <DafnyRuntimeJavaInputFile Remove="./DafnyRuntimeJava/build/**/*.*" />
+ </ItemGroup>
+
+ <ItemGroup>
+ <Folder Include="DafnyRuntimeJava\build\libs" />
+ </ItemGroup>
+ <PropertyGroup>
+ <DafnyRuntimeJar>DafnyRuntimeJava/build/libs/DafnyRuntime.jar</DafnyRuntimeJar>
+ </PropertyGroup>
+ <Target Name="BuildDafnyRuntimeJar" AfterTargets="ResolveReferences" BeforeTargets="CoreCompile" Inputs="$(MSBuildProjectFile);@(DafnyRuntimeJavaInputFile)" Outputs="$(DafnyRuntimeJar)">
+
+ <Message Text="Compiling DafnyRuntimeJava to $(DafnyRuntimeJar)..." Importance="high" />
+ <Exec WorkingDirectory="DafnyRuntimeJava" Command="./gradlew -q clean build" />
+ <ItemGroup>
+ <!-- Register the generated file to be deleted when cleaning -->
+ <FileWrites Include="$(DafnyRuntimeJar)" />
+ </ItemGroup>
+ </Target>
+
 </Project>

Source/DafnyRuntime/DafnyRuntimeJava/build.gradle

@@ -26,16 +26,6 @@ test {
  useJUnitPlatform()
 }
 
-task copyJarToBinaries {
- dependsOn build
- doLast {
- copy {
- from 'build/libs/DafnyRuntime.jar'
- into '../../../Binaries'
- }
- }
-}
-
 clean {
  delete '../../../Binaries/DafnyRuntime.jar'
 }

Source/DafnyServer/Server.cs

@@ -8,7 +8,7 @@
 using Microsoft.Boogie;
 
 namespace Microsoft.Dafny {
- class Server {
+ public class Server {
  private bool running;
 
  static void Main(string[] args) {

Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj

@@ -17,4 +17,9 @@
  <ProjectReference Include="..\DafnyTestGeneration\DafnyTestGeneration.csproj" />
  </ItemGroup>
 
+ <ItemGroup>
+ <Content Include="..\..\Binaries\z3\**\*.*" LinkBase="z3">
+ <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
+ </Content>
+ </ItemGroup>
 </Project>

Source/IntegrationTests/IntegrationTests.csproj

@@ -0,0 +1,44 @@
+<Project Sdk="Microsoft.NET.Sdk">
+
+ <PropertyGroup>
+ <TargetFramework>net5.0</TargetFramework>
+ <GenerateEmbeddedFilesManifest>true</GenerateEmbeddedFilesManifest>
+ <IsPackable>false</IsPackable>
+ <Nullable>enable</Nullable>
+ </PropertyGroup>
+
+ <ItemGroup>
+ <PackageReference Include="Microsoft.NET.Test.Sdk" Version="16.9.4" />
+ <PackageReference Include="xunit" Version="2.4.1" />
+ <PackageReference Include="xunit.runner.visualstudio" Version="2.4.3">
+ <IncludeAssets>runtime; build; native; contentfiles; analyzers; buildtransitive</IncludeAssets>
+ <PrivateAssets>all</PrivateAssets>
+ </PackageReference>
+ <PackageReference Include="coverlet.collector" Version="3.0.2">
+ <IncludeAssets>runtime; build; native; contentfiles; analyzers; buildtransitive</IncludeAssets>
+ <PrivateAssets>all</PrivateAssets>
+ </PackageReference>
+ </ItemGroup>
+
+ <ItemGroup>
+ <ProjectReference Include="..\DafnyDriver\DafnyDriver.csproj" />
+ <ProjectReference Include="..\DafnyServer\DafnyServer.csproj" />
+ <ProjectReference Include="..\XUnitExtensions\XUnitExtensions.csproj" />
+ </ItemGroup>
+
+ <ItemGroup>
+ <Content Include="..\..\Binaries\z3\**\*.*" LinkBase="z3">
+ <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
+ </Content>
+ <Content Include="..\..\Test\**\*.*" LinkBase="TestFiles\LitTests\LitTest">
+ <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
+ </Content>
+ <Content Include="..\..\docs\DafnyRef\examples\**\*.*" LinkBase="TestFiles\LitTests\LitTest\refman\examples">
+ <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
+ </Content>
+ <Content Include="..\..\node_modules\**\*.*" LinkBase="TestFiles\LitTests\LitTest\node_modules">
+ <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
+ </Content>
+ </ItemGroup>
+
+</Project>