diff --git a/.github/workflows/msbuild.yml b/.github/workflows/msbuild.yml index bd9312ba557..abf0591c51a 100644 --- a/.github/workflows/msbuild.yml +++ b/.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 diff --git a/.github/workflows/xunit-tests.yml b/.github/workflows/xunit-tests.yml index 7b583d5c96d..d7fd8dc3652 100644 --- a/.github/workflows/xunit-tests.yml +++ b/.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 diff --git a/Scripts/package.py b/Scripts/package.py index d8c30cd037e..00c820e81d6 100755 --- a/Scripts/package.py +++ b/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 diff --git a/Source/Dafny.sln b/Source/Dafny.sln index 3cc1738d764..36bb4d93baa 100644 --- a/Source/Dafny.sln +++ b/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 diff --git a/Source/Dafny/Compilers/Compiler-cpp.cs b/Source/Dafny/Compilers/Compiler-cpp.cs index ef112ff9c24..da41eb9630a 100644 --- a/Source/Dafny/Compilers/Compiler-cpp.cs +++ b/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 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) { diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index e75695e9157..48a9c994afe 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -875,7 +875,10 @@ Dafny { TopDecl } (. // 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) { diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj index 7e7f957a8f0..0e383f93139 100644 --- a/Source/Dafny/DafnyPipeline.csproj +++ b/Source/Dafny/DafnyPipeline.csproj @@ -34,10 +34,7 @@ - - - PreserveNewest - + diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj index 9c45bb2404c..bc0988475e2 100644 --- a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj +++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj @@ -21,6 +21,10 @@ + + PreserveNewest + + PreserveNewest diff --git a/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj b/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj index 675331b71f0..fac62db3754 100644 --- a/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj +++ b/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj @@ -24,4 +24,10 @@ + + + PreserveNewest + + + diff --git a/Source/DafnyRuntime/DafnyRuntime.csproj b/Source/DafnyRuntime/DafnyRuntime.csproj index 04b202d9dbe..64f4fd0371c 100755 --- a/Source/DafnyRuntime/DafnyRuntime.csproj +++ b/Source/DafnyRuntime/DafnyRuntime.csproj @@ -20,6 +20,31 @@ Always + + + + + + + + + + + + + + DafnyRuntimeJava/build/libs/DafnyRuntime.jar + + + + + + + + + + + diff --git a/Binaries/DafnyRuntime.go b/Source/DafnyRuntime/DafnyRuntime.go similarity index 100% rename from Binaries/DafnyRuntime.go rename to Source/DafnyRuntime/DafnyRuntime.go diff --git a/Binaries/DafnyRuntime.h b/Source/DafnyRuntime/DafnyRuntime.h similarity index 100% rename from Binaries/DafnyRuntime.h rename to Source/DafnyRuntime/DafnyRuntime.h diff --git a/Binaries/DafnyRuntime.js b/Source/DafnyRuntime/DafnyRuntime.js similarity index 100% rename from Binaries/DafnyRuntime.js rename to Source/DafnyRuntime/DafnyRuntime.js diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/build.gradle b/Source/DafnyRuntime/DafnyRuntimeJava/build.gradle index a516b1e9ffe..cc41949815b 100644 --- a/Source/DafnyRuntime/DafnyRuntimeJava/build.gradle +++ b/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' } diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index b4e9259c7bb..781ac041acf 100644 --- a/Source/DafnyServer/Server.cs +++ b/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) { diff --git a/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj b/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj index 222a855a3bb..e8c1199552e 100644 --- a/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj +++ b/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj @@ -17,4 +17,9 @@ + + + PreserveNewest + + diff --git a/Source/IntegrationTests/IntegrationTests.csproj b/Source/IntegrationTests/IntegrationTests.csproj new file mode 100644 index 00000000000..db1c9c3be9d --- /dev/null +++ b/Source/IntegrationTests/IntegrationTests.csproj @@ -0,0 +1,44 @@ + + + + net5.0 + true + false + enable + + + + + + + runtime; build; native; contentfiles; analyzers; buildtransitive + all + + + runtime; build; native; contentfiles; analyzers; buildtransitive + all + + + + + + + + + + + + PreserveNewest + + + PreserveNewest + + + PreserveNewest + + + PreserveNewest + + + + diff --git a/Source/IntegrationTests/LitTests.cs b/Source/IntegrationTests/LitTests.cs new file mode 100644 index 00000000000..50af64270bf --- /dev/null +++ b/Source/IntegrationTests/LitTests.cs @@ -0,0 +1,104 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Reflection; +using System.Runtime.InteropServices; +using Microsoft.Dafny; +using Xunit; +using Xunit.Abstractions; +using XUnitExtensions; +using XUnitExtensions.Lit; + +[assembly: TestCollectionOrderer("XUnitExtensions.TestCollectionShardFilter", "XUnitExtensions")] + +namespace IntegrationTests { + public class LitTests { + + private static readonly Assembly DafnyDriverAssembly = typeof(DafnyDriver).Assembly; + private static readonly Assembly DafnyServerAssembly = typeof(Server).Assembly; + + private static readonly string[] DefaultDafnyArguments = new[] { + "/countVerificationErrors:0", + + // We do not want absolute or relative paths in error messages, just the basename of the file + "/useBaseNameForFileName", + + // We do not want output such as "Compiled program written to Foo.cs" + // from the compilers, since that changes with the target language + "/compileVerbose:0", + + // Hide Boogie execution traces since they are meaningless for Dafny programs + "/errorTrace:0", + + // Set a default time limit, to catch cases where verification time runs off the rails + "/timeLimit:300" + }; + + private static ILitCommand MainWithArguments(Assembly assembly, IEnumerable arguments, LitTestConfiguration config, bool invokeDirectly) { + return MainMethodLitCommand.Parse(assembly, arguments, config, invokeDirectly); + } + + private static readonly LitTestConfiguration Config; + static LitTests() { + var substitutions = new Dictionary { + { "%diff", "diff" }, + { "%binaryDir", "." }, + { "%z3", Path.Join("z3", "bin", "z3") }, + { "%refmanexamples", Path.Join("TestFiles", "LitTests", "LitTest", "refman", "examples") } + }; + + var commands = new Dictionary, LitTestConfiguration, ILitCommand>> { + { + "%baredafny", (args, config) => + MainWithArguments(DafnyDriverAssembly, args, config, false) + }, { + "%dafny", (args, config) => + MainWithArguments(DafnyDriverAssembly, DefaultDafnyArguments.Concat(args), config, false) + }, { + "%server", (args, config) => + MainWithArguments(DafnyServerAssembly, args, config, false) + } + }; + + var passthroughEnvironmentVariables = new[] { "PATH", "HOME" }; + + string[] features; + if (RuntimeInformation.IsOSPlatform(OSPlatform.Linux)) { + features = new[] { "ubuntu", "posix" }; + } else if (RuntimeInformation.IsOSPlatform(OSPlatform.Windows)) { + features = new[] { "windows" }; + } else if (RuntimeInformation.IsOSPlatform(OSPlatform.OSX)) { + features = new[] { "macosx", "posix" }; + } else { + throw new Exception($"Unsupported OS: {RuntimeInformation.OSDescription}"); + } + + var dafnyReleaseDir = Environment.GetEnvironmentVariable("DAFNY_RELEASE"); + if (dafnyReleaseDir != null) { + commands["%baredafny"] = (args, config) => + new ShellLitCommand(config, Path.Join(dafnyReleaseDir, "dafny"), args, config.PassthroughEnvironmentVariables); + commands["%dafny"] = (args, config) => + new ShellLitCommand(config, Path.Join(dafnyReleaseDir, "dafny"), DefaultDafnyArguments.Concat(args), config.PassthroughEnvironmentVariables); + commands["%server"] = (args, config) => + new ShellLitCommand(config, Path.Join(dafnyReleaseDir, "DafnyServer"), args, config.PassthroughEnvironmentVariables); + substitutions["%z3"] = Path.Join(dafnyReleaseDir, "z3", "bin", "z3"); + } + + Config = new LitTestConfiguration(substitutions, commands, features, passthroughEnvironmentVariables); + } + + private readonly ITestOutputHelper output; + + public LitTests(ITestOutputHelper output) { + this.output = output; + } + + [FileTheory] + [FileData(Includes = new[] { "**/*.dfy", "**/*.transcript" }, + Excludes = new[] { "**/Inputs/**/*", "**/Output/**/*", "refman/examples/**/*" })] + public void LitTest(string path) { + LitTestCase.Run(path, Config, output); + } + } +} \ No newline at end of file diff --git a/Source/XUnitExtensions/FileDataAttribute.cs b/Source/XUnitExtensions/FileDataAttribute.cs new file mode 100644 index 00000000000..17752e13ef5 --- /dev/null +++ b/Source/XUnitExtensions/FileDataAttribute.cs @@ -0,0 +1,48 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Reflection; +using Microsoft.Extensions.FileSystemGlobbing; +using Microsoft.Extensions.FileSystemGlobbing.Abstractions; +using Xunit.Abstractions; +using Xunit.Sdk; + +namespace XUnitExtensions { + public class FileDataAttribute : DataAttribute { + public string? Directory { get; set; } + public string[]? Includes { get; set; } + public string[]? Excludes { get; set; } + + public override IEnumerable GetData(MethodInfo testMethod) { + var matcher = new Matcher(); + + if (Includes != null) { + foreach (var include in Includes) { + matcher.AddInclude(include); + } + } + + if (Excludes != null) { + foreach (var exclude in Excludes) { + matcher.AddExclude(exclude); + } + } + + var basePath = Directory ?? Path.Combine("TestFiles", testMethod.DeclaringType!.Name, testMethod.Name); + var result = matcher.Execute(new DirectoryInfoWrapper(new DirectoryInfo(basePath))); + if (!result.HasMatches) { + throw new ArgumentException("No matching files found: " + this); + } + + return result.Files.Select(file => { + var fullPath = Path.Join(basePath, file.Stem); + var row = new FileTheoryDataRow(fullPath) { + SourceInformation = new SourceInformation() { FileName = fullPath, LineNumber = 0 }, + TestDisplayName = file.Stem, + }; + return new[] { row }; + }); + } + } +} \ No newline at end of file diff --git a/Source/XUnitExtensions/FileTestCase.cs b/Source/XUnitExtensions/FileTestCase.cs new file mode 100644 index 00000000000..cf0d94cdc85 --- /dev/null +++ b/Source/XUnitExtensions/FileTestCase.cs @@ -0,0 +1,93 @@ +using System; +using System.Collections.Generic; +using System.ComponentModel; +using System.Threading; +using System.Threading.Tasks; +using Xunit; +using Xunit.Abstractions; +using Xunit.Sdk; + +namespace XUnitExtensions { + public class FileTestCase : LongLivedMarshalByRefObject, IXunitTestCase { + // This could use SkippableFactDiscoverer.GetSkippableExceptionNames(IAttributeInfo) + // but it doesn't seem to be worth the complexity here yet. + private static readonly string[] skippingExceptionNames = { typeof(SkipException).FullName! }; + + // Only nullable for the sake of the deserialization constructor + private XunitTestCase? innerTestCase; + + public string? DisplayName { get; protected set; } + public string? SkipReason { get; protected set; } + + public FileTestCase(IMessageSink diagnosticMessageSink, ITestMethod testMethod, IFileTheoryRowData rowData) { + var collection = new TestCollection(testMethod.TestClass.TestCollection.TestAssembly, + testMethod.TestClass.Class, "Test collection for " + rowData.TestDisplayName); + var testClassWithCollection = new TestClass(collection, testMethod.TestClass.Class); + var testMethodWithCollection = new TestMethod(testClassWithCollection, testMethod.Method); + + // This unsafe cast is necessary because the signature of the constructor we're passing arguments to + // is wrong: the type should be object?[] because arbitrary test method arguments can absolutely be null! + object[] data = (object[])rowData.GetData(); + innerTestCase = new SkippableFactTestCase(skippingExceptionNames, diagnosticMessageSink, TestMethodDisplay.Method, TestMethodDisplayOptions.All, + testMethodWithCollection, data); + if (rowData.Traits != null) { + foreach (var (key, value) in rowData.Traits) { + innerTestCase.Traits.Add(key, value); + } + } + + innerTestCase.SourceInformation = rowData.SourceInformation; + DisplayName = rowData.TestDisplayName; + SkipReason = rowData.Skip; + } + + [Obsolete("Called by the de-serializer", error: true)] + public FileTestCase() { } + + public void Deserialize(IXunitSerializationInfo info) { + innerTestCase = info.GetValue(nameof(innerTestCase)); + DisplayName = info.GetValue(nameof(DisplayName)); + SkipReason = info.GetValue(nameof(SkipReason)); + } + + public void Serialize(IXunitSerializationInfo info) { + info.AddValue(nameof(innerTestCase), innerTestCase); + info.AddValue(nameof(DisplayName), DisplayName); + info.AddValue(nameof(SkipReason), SkipReason); + } + + public ISourceInformation SourceInformation { + get => innerTestCase!.SourceInformation; + set => innerTestCase!.SourceInformation = value; + } + + public ITestMethod TestMethod => innerTestCase!.TestMethod; + public object[] TestMethodArguments => innerTestCase!.TestMethodArguments; + public Dictionary> Traits => innerTestCase!.Traits; + public string UniqueID => innerTestCase!.UniqueID; + public Exception InitializationException => innerTestCase!.InitializationException; + public IMethodInfo Method => innerTestCase!.Method; + public int Timeout => innerTestCase!.Timeout; + + public async Task RunAsync(IMessageSink diagnosticMessageSink, IMessageBus messageBus, object[] constructorArguments, + ExceptionAggregator aggregator, CancellationTokenSource cancellationTokenSource) { + + // This is the same thing SkippableFactTestCase.RunAsync does. + // support for dynamic test skipping is much cleaner in xUnit 3. + var messageBusInterceptor = new SkippableTestMessageBus(messageBus, skippingExceptionNames); + RunSummary result = await new XunitTestCaseRunner( + this, + DisplayName, + SkipReason, + constructorArguments, + TestMethodArguments, + messageBusInterceptor, + aggregator, + cancellationTokenSource + ).RunAsync(); + result.Failed -= messageBusInterceptor.SkippedCount; + result.Skipped += messageBusInterceptor.SkippedCount; + return result; + } + } +} \ No newline at end of file diff --git a/Source/XUnitExtensions/FileTheoryAttribute.cs b/Source/XUnitExtensions/FileTheoryAttribute.cs new file mode 100644 index 00000000000..daf006a0a85 --- /dev/null +++ b/Source/XUnitExtensions/FileTheoryAttribute.cs @@ -0,0 +1,10 @@ +using System; +using Xunit; +using Xunit.Sdk; + +namespace XUnitExtensions { + [AttributeUsage(AttributeTargets.Method)] + [XunitTestCaseDiscoverer("XUnitExtensions.FileTheoryDiscoverer", "XUnitExtensions")] + public class FileTheoryAttribute : TheoryAttribute { + } +} \ No newline at end of file diff --git a/Source/XUnitExtensions/FileTheoryDataRow.cs b/Source/XUnitExtensions/FileTheoryDataRow.cs new file mode 100644 index 00000000000..67a71cf4b4c --- /dev/null +++ b/Source/XUnitExtensions/FileTheoryDataRow.cs @@ -0,0 +1,39 @@ +using System.Collections.Generic; +using Xunit.Abstractions; + +namespace XUnitExtensions { + public class FileTheoryDataRow : IXunitSerializable, IFileTheoryRowData { + + private object[]? data; + + public FileTheoryDataRow() { + + } + + public FileTheoryDataRow(params object[] data) { + this.data = data; + } + + public ISourceInformation? SourceInformation { get; set; } + public string? Skip { get; set; } + public string? TestDisplayName { get; set; } + public Dictionary>? Traits { get; set; } + public object?[] GetData() => data!; + + public void Serialize(IXunitSerializationInfo info) { + info.AddValue(nameof(SourceInformation), SourceInformation); + info.AddValue(nameof(Skip), Skip); + info.AddValue(nameof(TestDisplayName), TestDisplayName); + info.AddValue(nameof(Traits), Traits); + info.AddValue(nameof(data), data); + } + + public void Deserialize(IXunitSerializationInfo info) { + SourceInformation = info.GetValue(nameof(SourceInformation)); + Skip = info.GetValue(nameof(Skip)); + TestDisplayName = info.GetValue(nameof(TestDisplayName)); + Traits = info.GetValue>>(nameof(Traits)); + data = info.GetValue(nameof(data)); + } + } +} \ No newline at end of file diff --git a/Source/XUnitExtensions/FileTheoryDiscoverer.cs b/Source/XUnitExtensions/FileTheoryDiscoverer.cs new file mode 100644 index 00000000000..09eebd2d668 --- /dev/null +++ b/Source/XUnitExtensions/FileTheoryDiscoverer.cs @@ -0,0 +1,28 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using Xunit.Abstractions; +using Xunit.Sdk; + +namespace XUnitExtensions { + public class FileTheoryDiscoverer : TheoryDiscoverer { + + public FileTheoryDiscoverer(IMessageSink diagnosticMessageSink) : base(diagnosticMessageSink) { + } + + public override IEnumerable Discover(ITestFrameworkDiscoveryOptions discoveryOptions, ITestMethod testMethod, IAttributeInfo factAttribute) { + // This discoverer requires pre-enumeration in order to assign a collection to each test case. + discoveryOptions.SetValue("xunit.discovery.PreEnumerateTheories", true); + return base.Discover(discoveryOptions, testMethod, factAttribute); + } + + protected override IEnumerable CreateTestCasesForDataRow(ITestFrameworkDiscoveryOptions discoveryOptions, ITestMethod testMethod, + IAttributeInfo theoryAttribute, object[] dataRow) { + if (dataRow.Length == 1 && dataRow[0] is IFileTheoryRowData theoryRowData) { + return new[] { new FileTestCase(DiagnosticMessageSink, testMethod, theoryRowData) }; + } + + return base.CreateTestCasesForDataRow(discoveryOptions, testMethod, theoryAttribute, dataRow); + } + } +} \ No newline at end of file diff --git a/Source/XUnitExtensions/ITheoryDataRow.cs b/Source/XUnitExtensions/ITheoryDataRow.cs new file mode 100644 index 00000000000..709a1971e4b --- /dev/null +++ b/Source/XUnitExtensions/ITheoryDataRow.cs @@ -0,0 +1,38 @@ +using System.Collections.Generic; +using Xunit; +using Xunit.Abstractions; +using Xunit.Sdk; + +namespace XUnitExtensions { + public interface IFileTheoryRowData { + + /// + /// Gets the source information for this row of data; if null is returned, then the location + /// of the test method is ussed. + /// + ISourceInformation? SourceInformation { get; } + + /// + /// Gets the reason for skipping this row of data; if null is returned, then the data + /// row isn't skipped. + /// + string? Skip { get; } + + /// + /// Gets the display name for the test (replacing the default behavior, which would be to use the DisplayName + /// from , or falling back to the class & method name). + /// + string? TestDisplayName { get; } + + /// + /// Gets the trait values associated with this theory data row. If there are none, you may either + /// return a null or empty dictionary. + /// + Dictionary>? Traits { get; } + + /// + /// Gets the theory data. + /// + object?[] GetData(); + } +} \ No newline at end of file diff --git a/Source/XUnitExtensions/Lit/ILitCommand.cs b/Source/XUnitExtensions/Lit/ILitCommand.cs new file mode 100644 index 00000000000..ac9aee86bc0 --- /dev/null +++ b/Source/XUnitExtensions/Lit/ILitCommand.cs @@ -0,0 +1,82 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Text; +using Microsoft.Extensions.FileSystemGlobbing; +using Microsoft.Extensions.FileSystemGlobbing.Abstractions; +using Xunit.Abstractions; + +namespace XUnitExtensions.Lit { + public interface ILitCommand { + + private static readonly Dictionary> CommandParsers = new(); + static ILitCommand() { + CommandParsers.Add("RUN:", RunCommand.Parse); + CommandParsers.Add("UNSUPPORTED:", UnsupportedCommand.Parse); + CommandParsers.Add("XFAIL:", XFailCommand.Parse); + } + + public static ILitCommand? Parse(string line, LitTestConfiguration config) { + foreach (var (keyword, parser) in CommandParsers) { + var index = line.IndexOf(keyword); + if (index >= 0) { + var arguments = line[(index + keyword.Length)..].Trim(); + return parser(arguments, config); + } + } + return null; + } + + public static string[] Tokenize(string line) { + var arguments = new List(); + var argument = new StringBuilder(); + var singleQuoted = false; + var doubleQuoted = false; + var hasGlobCharacters = false; + for (int i = 0; i < line.Length; i++) { + var c = line[i]; + if (c == '\'') { + singleQuoted = !singleQuoted; + } else if (c == '"') { + doubleQuoted = !doubleQuoted; + } else if (Char.IsWhiteSpace(c) && !(singleQuoted || doubleQuoted)) { + if (argument.Length != 0) { + if (hasGlobCharacters) { + arguments.AddRange(ExpandGlobs(argument.ToString())); + } else { + arguments.Add(argument.ToString()); + } + + argument.Clear(); + hasGlobCharacters = false; + } + } else { + if (c is '*' or '?' && !singleQuoted) { + hasGlobCharacters = true; + } + argument.Append(c); + } + } + + if (argument.Length != 0) { + if (hasGlobCharacters) { + arguments.AddRange(ExpandGlobs(argument.ToString())); + } else { + arguments.Add(argument.ToString()); + } + } + + return arguments.ToArray(); + } + + protected static IEnumerable ExpandGlobs(string chunk) { + var matcher = new Matcher(); + matcher.AddInclude(chunk); + var result = matcher.Execute(new DirectoryInfoWrapper(new DirectoryInfo("."))); + return result.Files.Select(f => f.Path); + } + + public (int, string, string) Execute(ITestOutputHelper outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter); + } +} \ No newline at end of file diff --git a/Source/XUnitExtensions/Lit/LitCommandWithRedirection.cs b/Source/XUnitExtensions/Lit/LitCommandWithRedirection.cs new file mode 100644 index 00000000000..be8b788d2f1 --- /dev/null +++ b/Source/XUnitExtensions/Lit/LitCommandWithRedirection.cs @@ -0,0 +1,94 @@ +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Text; +using System.Text.RegularExpressions; +using Microsoft.Extensions.FileSystemGlobbing; +using Microsoft.Extensions.FileSystemGlobbing.Abstractions; +using Xunit.Abstractions; + +namespace XUnitExtensions.Lit { + public class LitCommandWithRedirection : ILitCommand { + + public static LitCommandWithRedirection Parse(string[] tokens, LitTestConfiguration config) { + var commandSymbol = tokens[0]; + var argumentsList = tokens[1..].ToList(); + string? inputFile = null; + string? outputFile = null; + var appendOutput = false; + string? errorFile = null; + var redirectInIndex = argumentsList.IndexOf("<"); + if (redirectInIndex >= 0) { + inputFile = config.ApplySubstitutions(argumentsList[redirectInIndex + 1]); + argumentsList.RemoveRange(redirectInIndex, 2); + } + var redirectOutIndex = argumentsList.IndexOf(">"); + if (redirectOutIndex >= 0) { + outputFile = config.ApplySubstitutions(argumentsList[redirectOutIndex + 1]); + argumentsList.RemoveRange(redirectOutIndex, 2); + } + var redirectAppendIndex = argumentsList.IndexOf(">>"); + if (redirectAppendIndex >= 0) { + outputFile = config.ApplySubstitutions(argumentsList[redirectAppendIndex + 1]); + appendOutput = true; + argumentsList.RemoveRange(redirectAppendIndex, 2); + } + var redirectErrorIndex = argumentsList.IndexOf("2>"); + if (redirectErrorIndex >= 0) { + errorFile = config.ApplySubstitutions(argumentsList[redirectErrorIndex + 1]); + argumentsList.RemoveRange(redirectErrorIndex, 2); + } + + var arguments = argumentsList.Select(config.ApplySubstitutions); + + if (config.Commands.TryGetValue(commandSymbol, out var command)) { + return new LitCommandWithRedirection(command(arguments, config), inputFile, outputFile, appendOutput, errorFile); + } + + commandSymbol = config.ApplySubstitutions(commandSymbol); + + return new LitCommandWithRedirection( + new ShellLitCommand(config, commandSymbol, arguments, config.PassthroughEnvironmentVariables), + inputFile, outputFile, appendOutput, errorFile); + } + + private readonly ILitCommand command; + private readonly string? inputFile; + private readonly string? outputFile; + private readonly bool append; + private readonly string? errorFile; + + public LitCommandWithRedirection(ILitCommand command, string? inputFile, string? outputFile, bool append, string? errorFile) { + this.command = command; + this.inputFile = inputFile; + this.outputFile = outputFile; + this.append = append; + this.errorFile = errorFile; + } + + public (int, string, string) Execute(ITestOutputHelper outputHelper, TextReader? inReader, TextWriter? outWriter, TextWriter? errWriter) { + var inputReader = inputFile != null ? new StreamReader(inputFile) : null; + var outputWriter = outputFile != null ? new StreamWriter(outputFile, append) : null; + var errorWriter = errorFile != null ? new StreamWriter(errorFile, false) : null; + return command.Execute(outputHelper, inputReader, outputWriter, errorWriter); + } + + public override string ToString() { + var builder = new StringBuilder(); + builder.Append(command); + if (inputFile != null) { + builder.Append(" < "); + builder.Append(inputFile); + } + if (outputFile != null) { + builder.Append(append ? " >> " : " > "); + builder.Append(outputFile); + } + if (errorFile != null) { + builder.Append(" 2> "); + builder.Append(errorFile); + } + return builder.ToString(); + } + } +} \ No newline at end of file diff --git a/Source/XUnitExtensions/Lit/LitTestCase.cs b/Source/XUnitExtensions/Lit/LitTestCase.cs new file mode 100644 index 00000000000..a60e2a04a18 --- /dev/null +++ b/Source/XUnitExtensions/Lit/LitTestCase.cs @@ -0,0 +1,89 @@ +using System; +using System.Collections; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using Xunit; +using Xunit.Abstractions; + +namespace XUnitExtensions.Lit { + public class LitTestCase { + + private readonly string filePath; + private readonly IEnumerable commands; + private readonly bool expectFailure; + + public static LitTestCase Read(string filePath, LitTestConfiguration config) { + ILitCommand[] commands = File.ReadAllLines(filePath) + .Select(line => ILitCommand.Parse(line, config)) + .Where(c => c != null) + .Select(e => e!) + .ToArray(); + if (commands.Length == 0) { + throw new ArgumentException($"No lit commands found in test file: {filePath}"); + } + var xfail = commands.Any(c => c is XFailCommand); + foreach (var unsupported in commands.OfType()) { + foreach (var feature in config.Features) { + if (unsupported.Features.Contains(feature)) { + throw new SkipException($"Test case not supported: {feature}"); + } + } + } + return new LitTestCase(filePath, commands, xfail); + } + + public static void Run(string filePath, LitTestConfiguration config, ITestOutputHelper outputHelper) { + string fileName = Path.GetFileName(filePath); + string? directory = Path.GetDirectoryName(filePath); + if (directory == null) { + throw new ArgumentException("Couldn't get directory name for path: {}"); + } + string fullDirectoryPath = Path.GetFullPath(directory); + config = config.WithSubstitutions(new Dictionary { + { "%s", filePath }, + { "%S", fullDirectoryPath }, + { "%t", Path.Join(fullDirectoryPath, "Output", $"{fileName}.tmp")} + }); + + var testCase = Read(filePath, config); + testCase.Execute(outputHelper); + } + + public LitTestCase(string filePath, IEnumerable commands, bool expectFailure) { + this.filePath = filePath; + this.commands = commands; + this.expectFailure = expectFailure; + } + + public void Execute(ITestOutputHelper outputHelper) { + Directory.CreateDirectory(Path.Join(Path.GetDirectoryName(filePath), "Output")); + + foreach (var command in commands) { + int exitCode; + string output; + string error; + try { + outputHelper.WriteLine($"Executing command: {command}"); + (exitCode, output, error) = command.Execute(outputHelper, null, null, null); + } catch (Exception e) { + throw new Exception($"Exception thrown while executing command: {command}", e); + } + + if (expectFailure) { + if (exitCode != 0) { + throw new SkipException($"Command returned non-zero exit code ({exitCode}): {command}\nOutput:\n{output}\nError:\n{error}"); + } + } + + if (exitCode != 0) { + throw new Exception($"Command returned non-zero exit code ({exitCode}): {command}\nOutput:\n{output}\nError:\n{error}"); + } + } + + if (expectFailure) { + throw new Exception($"Test case passed but expected to fail: {filePath}"); + } + } + } +} \ No newline at end of file diff --git a/Source/XUnitExtensions/Lit/LitTestConfiguration.cs b/Source/XUnitExtensions/Lit/LitTestConfiguration.cs new file mode 100644 index 00000000000..46a6361d5a8 --- /dev/null +++ b/Source/XUnitExtensions/Lit/LitTestConfiguration.cs @@ -0,0 +1,45 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Reflection; +using Xunit.Abstractions; + +namespace XUnitExtensions.Lit { + + // TODO: Make safely immutable + public class LitTestConfiguration { + public readonly Dictionary Substitions; + + public readonly Dictionary, LitTestConfiguration, ILitCommand>> Commands; + + public readonly string[] Features; + + public readonly IEnumerable PassthroughEnvironmentVariables; + + public LitTestConfiguration(Dictionary substitions, + Dictionary, LitTestConfiguration, ILitCommand>> commands, + string[] features, + IEnumerable passthroughEnvironmentVariables) { + Substitions = substitions; + Commands = commands; + Features = features; + PassthroughEnvironmentVariables = passthroughEnvironmentVariables; + } + + public string ApplySubstitutions(string s) { + foreach (var (key, value) in Substitions) { + s = s.Replace(key, value); + } + return s; + } + + public LitTestConfiguration WithSubstitutions(Dictionary more) { + return new LitTestConfiguration( + Substitions.Concat(more).ToDictionary(pair => pair.Key, pair => pair.Value), + Commands, + Features, + PassthroughEnvironmentVariables + ); + } + } +} \ No newline at end of file diff --git a/Source/XUnitExtensions/Lit/MainMethodLitCommand.cs b/Source/XUnitExtensions/Lit/MainMethodLitCommand.cs new file mode 100644 index 00000000000..baf1bff8e32 --- /dev/null +++ b/Source/XUnitExtensions/Lit/MainMethodLitCommand.cs @@ -0,0 +1,53 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Reflection; +using System.Text; +using Xunit.Abstractions; + +namespace XUnitExtensions.Lit { + public class MainMethodLitCommand : ILitCommand { + private readonly Assembly assembly; + private readonly string[] arguments; + + private MainMethodLitCommand(Assembly assembly, string[] arguments) { + this.assembly = assembly; + this.arguments = arguments; + } + + public static ILitCommand Parse(Assembly assembly, IEnumerable arguments, LitTestConfiguration config, bool invokeDirectly) { + var result = new MainMethodLitCommand(assembly, arguments.ToArray()); + return invokeDirectly ? result : result.ToShellCommand(config); + } + + public (int, string, string) Execute(ITestOutputHelper outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { + if (inputReader != null) { + Console.SetIn(inputReader); + } + if (outputWriter != null) { + Console.SetOut(outputWriter); + } + if (errorWriter != null) { + Console.SetError(errorWriter); + } + + var exitCode = (int)assembly.EntryPoint!.Invoke(null, new object[] { arguments })!; + + return (exitCode, "", ""); + } + + public ILitCommand ToShellCommand(LitTestConfiguration config) { + var shellArguments = new[] { assembly.Location }.Concat(arguments); + return new ShellLitCommand(config, "dotnet", shellArguments, config.PassthroughEnvironmentVariables); + } + + public override string ToString() { + var builder = new StringBuilder(); + builder.Append(assembly.EntryPoint); + builder.Append(' '); + builder.AppendJoin(" ", arguments); + return builder.ToString(); + } + } +} \ No newline at end of file diff --git a/Source/XUnitExtensions/Lit/OrCommand.cs b/Source/XUnitExtensions/Lit/OrCommand.cs new file mode 100644 index 00000000000..885a8f75cf2 --- /dev/null +++ b/Source/XUnitExtensions/Lit/OrCommand.cs @@ -0,0 +1,26 @@ +using System.IO; +using Xunit.Abstractions; + +namespace XUnitExtensions.Lit { + public class OrCommand : ILitCommand { + private readonly ILitCommand lhs; + private readonly ILitCommand rhs; + + public OrCommand(ILitCommand lhs, ILitCommand rhs) { + this.lhs = lhs; + this.rhs = rhs; + } + + public (int, string, string) Execute(ITestOutputHelper outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { + var (exitCode, output, error) = lhs.Execute(outputHelper, inputReader, outputWriter, errorWriter); + if (exitCode == 0) { + return (exitCode, output, error); + } + return rhs.Execute(outputHelper, inputReader, outputWriter, errorWriter); + } + + public override string ToString() { + return $"{lhs} || {rhs}"; + } + } +} \ No newline at end of file diff --git a/Source/XUnitExtensions/Lit/RunCommand.cs b/Source/XUnitExtensions/Lit/RunCommand.cs new file mode 100644 index 00000000000..5afbbdc74a3 --- /dev/null +++ b/Source/XUnitExtensions/Lit/RunCommand.cs @@ -0,0 +1,22 @@ +using System; +using System.IO; +using Xunit.Abstractions; + +namespace XUnitExtensions.Lit { + public abstract class RunCommand { + public static ILitCommand Parse(string line, LitTestConfiguration config) { + return ParseArguments(ILitCommand.Tokenize(line), config); + } + + private static ILitCommand ParseArguments(string[] tokens, LitTestConfiguration config) { + // Just supporting || for now since it's a precise way to ignore an exit code + var seqOperatorIndex = Array.IndexOf(tokens, "||"); + if (seqOperatorIndex >= 0) { + var lhs = LitCommandWithRedirection.Parse(tokens[0..seqOperatorIndex], config); + var rhs = ParseArguments(tokens[(seqOperatorIndex + 1)..], config); + return new OrCommand(lhs, rhs); + } + return LitCommandWithRedirection.Parse(tokens, config); + } + } +} \ No newline at end of file diff --git a/Source/XUnitExtensions/Lit/ShellLitCommand.cs b/Source/XUnitExtensions/Lit/ShellLitCommand.cs new file mode 100644 index 00000000000..46da67974f8 --- /dev/null +++ b/Source/XUnitExtensions/Lit/ShellLitCommand.cs @@ -0,0 +1,70 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics; +using System.IO; +using System.Linq; +using System.Text; +using Xunit.Abstractions; + +namespace XUnitExtensions.Lit { + public class ShellLitCommand : ILitCommand { + private LitTestConfiguration config; + private string shellCommand; + private string[] arguments; + private string[] passthroughEnvironmentVariables; + + public ShellLitCommand(LitTestConfiguration config, string shellCommand, IEnumerable arguments, IEnumerable passthroughEnvironmentVariables) { + this.config = config; + this.shellCommand = shellCommand; + this.arguments = arguments.ToArray(); + this.passthroughEnvironmentVariables = passthroughEnvironmentVariables.ToArray(); + } + + public (int, string, string) Execute(ITestOutputHelper outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { + using var process = new Process(); + + process.StartInfo.FileName = shellCommand; + foreach (var argument in arguments) { + process.StartInfo.ArgumentList.Add(argument); + } + + // We avoid setting the current directory so that we maintain parity with + // MainMethodLitCommand, which can't change the current directory. + + process.StartInfo.UseShellExecute = false; + process.StartInfo.RedirectStandardInput = true; + process.StartInfo.RedirectStandardOutput = true; + process.StartInfo.RedirectStandardError = true; + process.StartInfo.CreateNoWindow = true; + + process.StartInfo.EnvironmentVariables.Clear(); + foreach (var passthrough in passthroughEnvironmentVariables) { + process.StartInfo.EnvironmentVariables.Add(passthrough, Environment.GetEnvironmentVariable(passthrough)); + } + + process.Start(); + if (inputReader != null) { + string input = inputReader.ReadToEnd(); + process.StandardInput.Write(input); + process.StandardInput.Close(); + } + string output = process.StandardOutput.ReadToEnd(); + outputWriter?.Write(output); + outputWriter?.Flush(); + string error = process.StandardError.ReadToEnd(); + errorWriter?.Write(error); + errorWriter?.Flush(); + process.WaitForExit(); + + return (process.ExitCode, output, error); + } + + public override string ToString() { + var builder = new StringBuilder(); + builder.Append(shellCommand); + builder.Append(' '); + builder.AppendJoin(" ", arguments); + return builder.ToString(); + } + } +} \ No newline at end of file diff --git a/Source/XUnitExtensions/Lit/UnsupportedCommand.cs b/Source/XUnitExtensions/Lit/UnsupportedCommand.cs new file mode 100644 index 00000000000..b9d392cb99d --- /dev/null +++ b/Source/XUnitExtensions/Lit/UnsupportedCommand.cs @@ -0,0 +1,26 @@ +using System; +using System.Collections; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using Xunit.Abstractions; + +namespace XUnitExtensions.Lit { + public class UnsupportedCommand : ILitCommand { + + public static UnsupportedCommand Parse(string line, LitTestConfiguration config) { + var features = line.Split(",", StringSplitOptions.RemoveEmptyEntries).Select(s => s.Trim()); + return new UnsupportedCommand(features); + } + + public IEnumerable Features { get; } + + public UnsupportedCommand(IEnumerable features) { + Features = features; + } + + public (int, string, string) Execute(ITestOutputHelper outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { + return (0, "", ""); + } + } +} \ No newline at end of file diff --git a/Source/XUnitExtensions/Lit/XFailCommand.cs b/Source/XUnitExtensions/Lit/XFailCommand.cs new file mode 100644 index 00000000000..7c438171036 --- /dev/null +++ b/Source/XUnitExtensions/Lit/XFailCommand.cs @@ -0,0 +1,21 @@ +using System; +using System.IO; +using Xunit.Abstractions; + +namespace XUnitExtensions.Lit { + public class XFailCommand : ILitCommand { + + public static ILitCommand Parse(string line, LitTestConfiguration config) { + // Only supporting * for now + if (line.Equals("*")) { + return new XFailCommand(); + } + + throw new ArgumentException($"Unrecognized arguments to XFAIL: {line}"); + } + + public (int, string, string) Execute(ITestOutputHelper outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { + return (0, "", ""); + } + } +} \ No newline at end of file diff --git a/Source/XUnitExtensions/TestCollectionShardFilter.cs b/Source/XUnitExtensions/TestCollectionShardFilter.cs new file mode 100644 index 00000000000..cf7c3c3f4c3 --- /dev/null +++ b/Source/XUnitExtensions/TestCollectionShardFilter.cs @@ -0,0 +1,38 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using Xunit; +using Xunit.Abstractions; + +namespace XUnitExtensions { + public class TestCollectionShardFilter : ITestCollectionOrderer { + public IEnumerable OrderTestCollections(IEnumerable testCollections) { + var sorted = testCollections.OrderBy(c => c.DisplayName); + + // Select the requested fraction of the test collections if using the XUNIT_SHARD[_COUNT] environment variables. + var shardEnvVar = Environment.GetEnvironmentVariable("XUNIT_SHARD"); + var numShardsEnvVar = Environment.GetEnvironmentVariable("XUNIT_SHARD_COUNT"); + if (shardEnvVar != null || numShardsEnvVar != null) { + if (shardEnvVar == null || numShardsEnvVar == null) { + throw new InvalidOperationException( + "The XUNIT_SHARD and XUNIT_SHARD_COUNT environment variables must both be provided."); + } + + var shard = Int32.Parse(shardEnvVar); + var numShards = Int32.Parse(numShardsEnvVar); + if (numShards <= 0) { + throw new InvalidOperationException( + "XUNIT_SHARD_COUNT must be greater than 0."); + } + if (shard <= 0 || shard > numShards) { + throw new InvalidOperationException( + "XUNIT_SHARD must be at least 1 and at most XUNIT_SHARD_COUNT."); + } + + return sorted.Where((_, index) => index % numShards == shard - 1); + } + + return sorted; + } + } +} \ No newline at end of file diff --git a/Source/XUnitExtensions/XUnitExtensions.csproj b/Source/XUnitExtensions/XUnitExtensions.csproj new file mode 100644 index 00000000000..c499739c8ee --- /dev/null +++ b/Source/XUnitExtensions/XUnitExtensions.csproj @@ -0,0 +1,25 @@ + + + + net5.0 + false + enable + + + + + + + + + runtime; build; native; contentfiles; analyzers; buildtransitive + all + + + runtime; build; native; contentfiles; analyzers; buildtransitive + all + + + + + diff --git a/Test/DafnyTestGeneration/TestGeneration.dfy b/Test/DafnyTestGeneration/TestGeneration.dfy index 1b405bf2b9c..9a979576227 100644 --- a/Test/DafnyTestGeneration/TestGeneration.dfy +++ b/Test/DafnyTestGeneration/TestGeneration.dfy @@ -1,17 +1,17 @@ // Generating tests: -// RUN: cp TestGeneration.dfy %t.dfy +// RUN: cp %S/TestGeneration.dfy %t.dfy // RUN: %dafny /definiteAssignment:3 /generateTestMode:Block %t.dfy > %t-tests.dfy // Compiling test to java: -// RUN: cd Output; %dafny /compileTarget:java %t-tests.dfy; cd ../ +// RUN: %dafny /compileTarget:java /out:%t-tests.dfy %t-tests.dfy // Adding reflection code that allows running the tests: -// RUN: perl -pe 's/import M_Compile.*;/`cat import.txt`/ge' -i %t-tests-java/TestGenerationUnitTests_Compile/__default.java -// RUN: perl -pe 's/public class __default \{/`cat reflectionCode.txt`/ge' -i %t-tests-java/TestGenerationUnitTests_Compile/__default.java +// RUN: perl -pe 's|import M_Compile.*;|`cat %S/import.txt`|ge' -i %t-tests-java/TestGenerationUnitTests_Compile/__default.java +// RUN: perl -pe 's|public class __default \{|`cat %S/reflectionCode.txt`|ge' -i %t-tests-java/TestGenerationUnitTests_Compile/__default.java // Compiling to bytecode and running the tests -// RUN: javac -cp %t-tests-java:../../Binaries/DafnyRuntime.jar %t-tests-java/TestGenerationUnitTests_Compile/__default.java -// RUN: java -cp %t-tests-java:../../Binaries/DafnyRuntime.jar TestGenerationUnitTests_Compile/__default > %t +// RUN: javac -cp %t-tests-java:%binaryDir/DafnyRuntime.jar %t-tests-java/TestGenerationUnitTests_Compile/__default.java +// RUN: java -cp %t-tests-java:%binaryDir/DafnyRuntime.jar TestGenerationUnitTests_Compile/__default > %t // RUN: %diff "%s.expect" "%t" module M { diff --git a/Test/DafnyTests/TestAttribute.dfy b/Test/DafnyTests/TestAttribute.dfy index 0f1858d9f80..9c08a160017 100644 --- a/Test/DafnyTests/TestAttribute.dfy +++ b/Test/DafnyTests/TestAttribute.dfy @@ -1,7 +1,7 @@ -// RUN: %dafny /out:Output/DafnyMain.cs TestAttribute.dfy /compile:0 /spillTargetCode:3 /noVerify -// RUN: dotnet test -v:q -noLogo 2>%t.raw || true +// RUN: %dafny /compileVerbose:1 /compile:0 /spillTargetCode:3 /noVerify "%s" > "%t" +// RUN: dotnet test -v:q -noLogo %S 2> %t.testresults.raw || true // Remove the timestamp prefixes on the expected errors -// RUN: sed 's/[^]]*\]//' "%t".raw > "%t" +// RUN: sed 's/[^]]*\]//' "%t".testresults.raw >> "%t" // RUN: %diff "%s.expect" "%t" include "../exceptions/VoidOutcomeDt.dfy" diff --git a/Test/DafnyTests/TestAttribute.dfy.expect b/Test/DafnyTests/TestAttribute.dfy.expect index 09066a94aa9..18bfb24f835 100644 --- a/Test/DafnyTests/TestAttribute.dfy.expect +++ b/Test/DafnyTests/TestAttribute.dfy.expect @@ -1,3 +1,6 @@ + +Dafny program verifier did not attempt verification +Wrote textual form of target program to TestAttribute.cs _module.__default.FailingTest_CheckForFailureForXunit [FAIL] _module.__default.FailingTestUsingExpectWithMessage [FAIL] _module.__default.FailingTestUsingExpect [FAIL] diff --git a/Test/comp/BranchCoverage.dfy b/Test/comp/BranchCoverage.dfy index 8b4206be84e..a0af1ea4d2c 100644 --- a/Test/comp/BranchCoverage.dfy +++ b/Test/comp/BranchCoverage.dfy @@ -1,7 +1,7 @@ -// RUN: %dafny /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:cs BranchCoverage2.cs "%s" > "%t" -// RUN: %dafny /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:js BranchCoverage3.js "%s" >> "%t" -// RUN: %dafny /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:go BranchCoverage4.go "%s" >> "%t" -// RUN: %dafny /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:java CodeCoverage.java "%s" >> "%t" +// RUN: %dafny /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:cs %S/BranchCoverage2.cs "%s" > "%t" +// RUN: %dafny /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:js %S/BranchCoverage3.js "%s" >> "%t" +// RUN: %dafny /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:go %S/BranchCoverage4.go "%s" >> "%t" +// RUN: %dafny /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:java %S/CodeCoverage.java "%s" >> "%t" // RUN: %diff "%s.expect" "%t" // The Main method is at the end of this file, because that makes it easier to maintain diff --git a/Test/comp/CSharpStyling.dfy b/Test/comp/CSharpStyling.dfy index 038eac22aef..584eac0b887 100644 --- a/Test/comp/CSharpStyling.dfy +++ b/Test/comp/CSharpStyling.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cs "%s" CSharpStyling2.cs > "%t" +// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cs "%s" %S/CSharpStyling2.cs > "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Test/comp/Extern.dfy b/Test/comp/Extern.dfy index f375937fe0a..52225810420 100644 --- a/Test/comp/Extern.dfy +++ b/Test/comp/Extern.dfy @@ -1,7 +1,7 @@ -// RUN: %dafny /compile:3 /compileTarget:cs "%s" Extern2.cs > "%t" -// RUN: %dafny /compile:3 /compileTarget:js "%s" Extern3.js >> "%t" -// RUN: %dafny /compile:3 /compileTarget:go "%s" Extern4.go >> "%t" -// RUN: %dafny /compile:3 /compileTarget:java "%s" LibClass.java OtherClass.java AllDafny.java Mixed.java AllExtern.java >> "%t" +// RUN: %dafny /compile:3 /compileTarget:cs "%s" %S/Extern2.cs > "%t" +// RUN: %dafny /compile:3 /compileTarget:js "%s" %S/Extern3.js >> "%t" +// RUN: %dafny /compile:3 /compileTarget:go "%s" %S/Extern4.go >> "%t" +// RUN: %dafny /compile:3 /compileTarget:java "%s" %S/LibClass.java %S/OtherClass.java %S/AllDafny.java %S/Mixed.java %S/AllExtern.java >> "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Test/comp/ExternCtors.dfy b/Test/comp/ExternCtors.dfy index 35b6112bab6..a9a0f9a897e 100644 --- a/Test/comp/ExternCtors.dfy +++ b/Test/comp/ExternCtors.dfy @@ -1,5 +1,5 @@ -// RUN: %dafny /compile:3 /compileTarget:cs "%s" ExternCtors-externs/Library.cs > "%t" -// RUN: %dafny /compile:3 /compileTarget:java "%s" ExternCtors-externs/Class.java >> "%t" +// RUN: %dafny /compile:3 /compileTarget:cs "%s" %S/ExternCtors-externs/Library.cs > "%t" +// RUN: %dafny /compile:3 /compileTarget:java "%s" %S/ExternCtors-externs/Class.java >> "%t" // RUN: %diff "%s.expect" "%t" // FIXME: Extern constructors are currently broken in Go and JavaScript, diff --git a/Test/comp/compile1quiet/CompileRunQuietly.dfy b/Test/comp/compile1quiet/CompileRunQuietly.dfy index e8b4149cea4..95b489e25fd 100644 --- a/Test/comp/compile1quiet/CompileRunQuietly.dfy +++ b/Test/comp/compile1quiet/CompileRunQuietly.dfy @@ -2,16 +2,16 @@ // RUN: dotnet CompileRunQuietly.dll >> "%t" // RUN: %dafny /compileTarget:js "%s" >> "%t" -// RUN: node CompileRunQuietly.js >> "%t" +// RUN: node %S/CompileRunQuietly.js >> "%t" // RUN: %dafny /compileTarget:go "%s" >> "%t" -// RUN: ./CompileRunQuietly >> "%t" +// RUN: %S/CompileRunQuietly >> "%t" // RUN: %dafny /compileTarget:java "%s" >> "%t" -// RUN: java CompileRunQuietly >> "%t" +// RUN: java -cp %binaryDir/DafnyRuntime.jar:%S/CompileRunQuietly-java CompileRunQuietly >> "%t" // RUN: %dafny /compileTarget:cpp "%s" >> "%t" -// RUN: ./CompileRunQuietly.exe >> "%t" +// RUN: CompileRunQuietly.exe >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/comp/compile1verbose/CompileAndThenRun.dfy b/Test/comp/compile1verbose/CompileAndThenRun.dfy index c14e80e257b..0db655f9129 100644 --- a/Test/comp/compile1verbose/CompileAndThenRun.dfy +++ b/Test/comp/compile1verbose/CompileAndThenRun.dfy @@ -2,16 +2,16 @@ // RUN: dotnet CompileAndThenRun.dll >> "%t" // RUN: %dafny /compileVerbose:1 /compileTarget:js "%s" >> "%t" -// RUN: node CompileAndThenRun.js >> "%t" +// RUN: node %S/CompileAndThenRun.js >> "%t" // RUN: %dafny /compileVerbose:1 /compileTarget:go "%s" >> "%t" -// RUN: ./CompileAndThenRun >> "%t" +// RUN: %S/CompileAndThenRun >> "%t" // RUN: %dafny /compileVerbose:1 /compileTarget:java "%s" >> "%t" -// RUN: java CompileAndThenRun >> "%t" +// RUN: java -cp %binaryDir/DafnyRuntime.jar:%S/CompileAndThenRun-java CompileAndThenRun >> "%t" // RUN: %dafny /compileVerbose:1 /compileTarget:cpp "%s" >> "%t" -// RUN: ./CompileAndThenRun.exe >> "%t" +// RUN: CompileAndThenRun.exe >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/comp/manualcompile/ManualCompile.dfy b/Test/comp/manualcompile/ManualCompile.dfy index 1d194078622..68255ca6431 100644 --- a/Test/comp/manualcompile/ManualCompile.dfy +++ b/Test/comp/manualcompile/ManualCompile.dfy @@ -1,20 +1,20 @@ // RUN: %dafny /compileVerbose:1 /compile:0 /spillTargetCode:2 /compileTarget:cs "%s" > "%t" -// RUN: dotnet build ManualCompile.csproj -// RUN: dotnet bin/Debug/net5.0/ManualCompile.dll >> "%t" +// RUN: dotnet build %S/ManualCompile.csproj +// RUN: dotnet %S/bin/Debug/net5.0/ManualCompile.dll >> "%t" // RUN: %dafny /compileVerbose:1 /compile:0 /spillTargetCode:2 /compileTarget:js "%s" >> "%t" -// RUN: node ManualCompile.js >> "%t" +// RUN: node %S/ManualCompile.js >> "%t" // RUN: %dafny /compileVerbose:1 /compile:0 /spillTargetCode:2 /compileTarget:go "%s" >> "%t" -// RUN: go run ManualCompile-go/src/ManualCompile.go >> "%t" +// RUN: env GOPATH=%S/ManualCompile-go go run %S/ManualCompile-go/src/ManualCompile.go >> "%t" // RUN: %dafny /compileVerbose:1 /compile:0 /spillTargetCode:2 /compileTarget:java "%s" >> "%t" -// RUN: javac ManualCompile-java/ManualCompile.java ManualCompile-java/*/*.java -// RUN: java ManualCompile >> "%t" +// RUN: javac -cp %binaryDir/DafnyRuntime.jar:%S/ManualCompile-java %S/ManualCompile-java/ManualCompile.java %S/ManualCompile-java/*/*.java +// RUN: java -cp %binaryDir/DafnyRuntime.jar:%S/ManualCompile-java ManualCompile >> "%t" // RUN: %dafny /compileVerbose:1 /compile:0 /spillTargetCode:2 /compileTarget:cpp "%s" >> "%t" -// RUN: g++ -g -Wall -Wextra -Wpedantic -Wno-unused-variable -std=c++17 -I %binaryDir -o ManualCompile.exe ManualCompile.cpp -// RUN: ./ManualCompile.exe >> "%t" +// RUN: g++ -g -Wall -Wextra -Wpedantic -Wno-unused-variable -std=c++17 -I %binaryDir -o ManualCompile.exe %S/ManualCompile.cpp +// RUN: ManualCompile.exe >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/comp/manualcompile/lit.local.cfg b/Test/comp/manualcompile/lit.local.cfg index f093c5c1e0b..8f63d146ca3 100644 --- a/Test/comp/manualcompile/lit.local.cfg +++ b/Test/comp/manualcompile/lit.local.cfg @@ -20,12 +20,4 @@ if lit.util.which('g++') == None: lit_config.note('g++ is unavailable, so cross-compilation tests are skipped\n') config.unsupported = True -binaryDir = config.dafnyBinaryDir -config.substitutions.append( ('%binaryDir', binaryDir) ) - current_dir = os.path.join(config.test_source_root, 'comp', 'manualcompile') - -config.environment['GOPATH'] = os.path.join(current_dir, 'ManualCompile-go') -config.environment['GO111MODULE'] = 'auto' - -config.environment['CLASSPATH'] = os.path.join(current_dir, 'ManualCompile-java') + ":" + os.path.join( binaryDir, "DafnyRuntime.jar" ) diff --git a/Test/dafny0/DafnyLibClient.dfy b/Test/dafny0/DafnyLibClient.dfy index 1a32d8cabc1..00e70143620 100644 --- a/Test/dafny0/DafnyLibClient.dfy +++ b/Test/dafny0/DafnyLibClient.dfy @@ -1,5 +1,5 @@ -// RUN: %dafny /spillTargetCode:1 DafnyLib.dfy DafnyLib-extern.cs /useRuntimeLib /out:Output/DafnyLib.dll /compileTarget:cs > "%t" -// RUN: %dafny /spillTargetCode:1 /compile:3 "%s" Output/DafnyLib.dll >> "%t" +// RUN: %dafny /spillTargetCode:1 %S/DafnyLib.dfy %S/DafnyLib-extern.cs /useRuntimeLib /out:%S/Output/DafnyLib.dll /compileTarget:cs > "%t" +// RUN: %dafny /spillTargetCode:1 /compile:3 "%s" %S/Output/DafnyLib.dll >> "%t" // RUN: %diff "%s.expect" "%t" module Client { diff --git a/Test/dafny0/Extern.dfy b/Test/dafny0/Extern.dfy index f5e66f416e3..b56ffaf35f4 100644 --- a/Test/dafny0/Extern.dfy +++ b/Test/dafny0/Extern.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:1 /compileTarget:cs /print:"%t.print" /dprint:"%t.dprint" "%s" Extern2.cs ExternHelloLibrary.dll > "%t" +// RUN: %dafny /compile:1 /compileTarget:cs /print:"%t.print" /dprint:"%t.dprint" "%s" %S/Extern2.cs %S/ExternHelloLibrary.dll > "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Test/dafny0/ExternCopyFromTrait.dfy b/Test/dafny0/ExternCopyFromTrait.dfy index 8ead0b18c8c..df15cf31368 100644 --- a/Test/dafny0/ExternCopyFromTrait.dfy +++ b/Test/dafny0/ExternCopyFromTrait.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:1 /compileTarget:cs /print:"%t.print" /dprint:"%t.dprint" "%s" ExternCopyFromTraitLibrary.cs > "%t" +// RUN: %dafny /compile:1 /compileTarget:cs /print:"%t.print" /dprint:"%t.dprint" "%s" %S/ExternCopyFromTraitLibrary.cs > "%t" // RUN: %diff "%s.expect" "%t" module {:extern "M"} M { trait {:extern} T1 { diff --git a/Test/dafny0/RuntimeTypeTests0.dfy b/Test/dafny0/RuntimeTypeTests0.dfy index bbce089d55d..5fcf21f53d0 100644 --- a/Test/dafny0/RuntimeTypeTests0.dfy +++ b/Test/dafny0/RuntimeTypeTests0.dfy @@ -4,8 +4,7 @@ // RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" -// RUN: sed -e 'sx\\x/x' < "%t" > "%t"2 -// RUN: %diff "%s.expect" "%t"2 +// RUN: %diff "%s.expect" "%t" // The code in this file demonstrates complications in sorting out covariance in some // compilation target languages. Compilation support is currently spotty, where C# and // Java only supports collection types (not datatypes), and only in the "upcast" direction. diff --git a/Test/dafny0/RuntimeTypeTests0.dfy.expect b/Test/dafny0/RuntimeTypeTests0.dfy.expect index ef718faea23..f415cb9699f 100644 --- a/Test/dafny0/RuntimeTypeTests0.dfy.expect +++ b/Test/dafny0/RuntimeTypeTests0.dfy.expect @@ -2,12 +2,12 @@ Dafny program verifier finished with 4 verified, 0 errors Dafny program verifier did not attempt verification -RuntimeTypeTests0.dfy(49,9): Error: compilation does not support trait types as a type parameter (got 'object'); consider introducing a ghost -RuntimeTypeTests0.dfy(58,9): Error: compilation does not support trait types as a type parameter (got 'object'); consider introducing a ghost +RuntimeTypeTests0.dfy(48,9): Error: compilation does not support trait types as a type parameter (got 'object'); consider introducing a ghost +RuntimeTypeTests0.dfy(57,9): Error: compilation does not support trait types as a type parameter (got 'object'); consider introducing a ghost Dafny program verifier did not attempt verification -RuntimeTypeTests0.dfy(49,9): Error: compilation does not support trait types as a type parameter (got 'object'); consider introducing a ghost -RuntimeTypeTests0.dfy(58,9): Error: compilation does not support trait types as a type parameter (got 'object'); consider introducing a ghost +RuntimeTypeTests0.dfy(48,9): Error: compilation does not support trait types as a type parameter (got 'object'); consider introducing a ghost +RuntimeTypeTests0.dfy(57,9): Error: compilation does not support trait types as a type parameter (got 'object'); consider introducing a ghost Wrote textual form of partial target program to RuntimeTypeTests0-java/RuntimeTypeTests0.java Dafny program verifier did not attempt verification diff --git a/Test/dafny0/ShowSnippets.dfy b/Test/dafny0/ShowSnippets.dfy index 9cf036cea60..c0a9f1f2ae5 100644 --- a/Test/dafny0/ShowSnippets.dfy +++ b/Test/dafny0/ShowSnippets.dfy @@ -1,4 +1,10 @@ -// RUN: %dafny /compile:0 /showSnippets:1 "%s" > "%t" +// There is a known bug in this feature where it can't find the original file if +// /useBaseNameForFileName is used and the file isn't in the current directory: +// https://github.com/dafny-lang/dafny/issues/1518. +// To work around this, we don't pass /useBaseNameForFileName and instead manually +// truncate the source paths to their base names using sed. +// RUN: %baredafny /countVerificationErrors:0 /errorTrace:0 /compile:0 /showSnippets:1 "%s" > "%t".raw +// RUN: sed 's/^.*\///' "%t".raw > "%t" // RUN: %diff "%s.expect" "%t" method Never() requires true && false {} diff --git a/Test/dafny0/ShowSnippets.dfy.expect b/Test/dafny0/ShowSnippets.dfy.expect index d3d72e1095d..a916e715643 100644 --- a/Test/dafny0/ShowSnippets.dfy.expect +++ b/Test/dafny0/ShowSnippets.dfy.expect @@ -1,17 +1,17 @@ -ShowSnippets.dfy(7,9): Error: assertion violation - | -7 | assert false; - | ^ here +ShowSnippets.dfy(13,9): Error: assertion violation + | +13 | assert false; + | ^ here -ShowSnippets.dfy(11,7): Error: A precondition for this call might not hold. +ShowSnippets.dfy(17,7): Error: A precondition for this call might not hold. | -11 | Never(); +17 | Never(); | ^ here -ShowSnippets.dfy(4,32): Related location: This is the precondition that might not hold. - | -4 | method Never() requires true && false {} - | ^ here +ShowSnippets.dfy(10,32): Related location: This is the precondition that might not hold. + | +10 | method Never() requires true && false {} + | ^ here Dafny program verifier finished with 0 verified, 2 errors diff --git a/Test/dafny0/snapshots/Snapshots0.run.dfy b/Test/dafny0/snapshots/Snapshots0.run.dfy index 4aeef2aae64..bd1c5c5df5e 100644 --- a/Test/dafny0/snapshots/Snapshots0.run.dfy +++ b/Test/dafny0/snapshots/Snapshots0.run.dfy @@ -1,2 +1,2 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 Inputs/Snapshots0.dfy > "%t" +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots0.dfy > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/Snapshots1.run.dfy b/Test/dafny0/snapshots/Snapshots1.run.dfy index 5e8a323f8ad..439b6681fce 100644 --- a/Test/dafny0/snapshots/Snapshots1.run.dfy +++ b/Test/dafny0/snapshots/Snapshots1.run.dfy @@ -1,2 +1,2 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 Inputs/Snapshots1.dfy > "%t" +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots1.dfy > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/Snapshots2.run.dfy b/Test/dafny0/snapshots/Snapshots2.run.dfy index 1658838a09e..36d8ae160af 100644 --- a/Test/dafny0/snapshots/Snapshots2.run.dfy +++ b/Test/dafny0/snapshots/Snapshots2.run.dfy @@ -1,2 +1,2 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 Inputs/Snapshots2.dfy > "%t" +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots2.dfy > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/Snapshots3.run.dfy b/Test/dafny0/snapshots/Snapshots3.run.dfy index 593a13ed18a..9a052948a11 100644 --- a/Test/dafny0/snapshots/Snapshots3.run.dfy +++ b/Test/dafny0/snapshots/Snapshots3.run.dfy @@ -1,2 +1,2 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 Inputs/Snapshots3.dfy > "%t" +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots3.dfy > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/Snapshots4.run.dfy b/Test/dafny0/snapshots/Snapshots4.run.dfy index 83443bca05f..8bde665646d 100644 --- a/Test/dafny0/snapshots/Snapshots4.run.dfy +++ b/Test/dafny0/snapshots/Snapshots4.run.dfy @@ -1,2 +1,2 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 Inputs/Snapshots4.dfy > "%t" +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots4.dfy > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/Snapshots5.run.dfy b/Test/dafny0/snapshots/Snapshots5.run.dfy index 2ca08b01a09..3948c29772a 100644 --- a/Test/dafny0/snapshots/Snapshots5.run.dfy +++ b/Test/dafny0/snapshots/Snapshots5.run.dfy @@ -1,2 +1,2 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 Inputs/Snapshots5.dfy > "%t" +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots5.dfy > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/Snapshots6.run.dfy b/Test/dafny0/snapshots/Snapshots6.run.dfy index 7eceec399be..f690cea5d0d 100644 --- a/Test/dafny0/snapshots/Snapshots6.run.dfy +++ b/Test/dafny0/snapshots/Snapshots6.run.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 Inputs/Snapshots6.dfy > "%t" +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots6.dfy > "%t" // RUN: %diff "%s.expect" "%t" // XFAIL: * // FIXME : Need to fix the snapshot diff --git a/Test/dafny0/snapshots/Snapshots7.run.dfy b/Test/dafny0/snapshots/Snapshots7.run.dfy index cabedf96d6e..ca6b8eed1d5 100644 --- a/Test/dafny0/snapshots/Snapshots7.run.dfy +++ b/Test/dafny0/snapshots/Snapshots7.run.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 Inputs/Snapshots7.dfy > "%t" +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots7.dfy > "%t" // RUN: %diff "%s.expect" "%t" // XFAIL: * // FIXME - need to regenerate the snapshots diff --git a/Test/dafny0/snapshots/Snapshots8.run.dfy b/Test/dafny0/snapshots/Snapshots8.run.dfy index c277023df73..5d7a84f5325 100644 --- a/Test/dafny0/snapshots/Snapshots8.run.dfy +++ b/Test/dafny0/snapshots/Snapshots8.run.dfy @@ -1,2 +1,2 @@ -// RUN: %dafny /compile:0 /verifySnapshots:3 /traceCaching:1 /errorTrace:0 Inputs/Snapshots8.dfy > "%t" +// RUN: %dafny /compile:0 /verifySnapshots:3 /traceCaching:1 /errorTrace:0 %S/Inputs/Snapshots8.dfy > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/Snapshots9.run.dfy b/Test/dafny0/snapshots/Snapshots9.run.dfy index de77de560cc..26b6d67312a 100644 --- a/Test/dafny0/snapshots/Snapshots9.run.dfy +++ b/Test/dafny0/snapshots/Snapshots9.run.dfy @@ -1,2 +1,2 @@ -// RUN: %dafny /compile:0 /verifySnapshots:3 /traceCaching:1 Inputs/Snapshots9.dfy > "%t" +// RUN: %dafny /compile:0 /verifySnapshots:3 /traceCaching:1 %S/Inputs/Snapshots9.dfy > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/git-issues/git-issue-1100.dfy b/Test/git-issues/git-issue-1100.dfy index 47af222b432..08126c15550 100644 --- a/Test/git-issues/git-issue-1100.dfy +++ b/Test/git-issues/git-issue-1100.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /compileTarget:cpp ../c++/arrays.dfy > "%t" +// RUN: %dafny /compile:3 /compileTarget:cpp %S/../c++/arrays.dfy > "%t" // RUN: %diff "%s.expect" "%t" // Test compilation of a file in another directory diff --git a/Test/git-issues/git-issue-1151.dfy b/Test/git-issues/git-issue-1151.dfy index a2ef5b9a45b..b58b4f21d12 100644 --- a/Test/git-issues/git-issue-1151.dfy +++ b/Test/git-issues/git-issue-1151.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 "%s" git-issue-1151-concrete.cs > "%t" +// RUN: %dafny /compile:3 "%s" %S/git-issue-1151-concrete.cs > "%t" // RUN: %diff "%s.expect" "%t" module {:extern "M"} M { diff --git a/Test/git-issues/git-issue-1199.dfy b/Test/git-issues/git-issue-1199.dfy index a6b5ec650b4..50c1a5c92ce 100644 --- a/Test/git-issues/git-issue-1199.dfy +++ b/Test/git-issues/git-issue-1199.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:1 /compileTarget:cs "%s" git-issue-1199-extern.cs > "%t" +// RUN: %dafny /compile:1 /compileTarget:cs "%s" %S/git-issue-1199-extern.cs > "%t" // RUN: %diff "%s.expect" "%t" module {:extern "Microsoft"} Microsoft { diff --git a/Test/git-issues/git-issue-1229.dfy b/Test/git-issues/git-issue-1229.dfy index a0f0f48b264..192f14ae3cd 100644 --- a/Test/git-issues/git-issue-1229.dfy +++ b/Test/git-issues/git-issue-1229.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:1 /compileTarget:cs "%s" git-issue-1229-extern.cs > "%t" +// RUN: %dafny /compile:1 /compileTarget:cs "%s" %S/git-issue-1229-extern.cs > "%t" // RUN: %diff "%s.expect" "%t" module {:extern "MyModule2"} MyModule2 { diff --git a/Test/git-issues/git-issue-289.dfy b/Test/git-issues/git-issue-289.dfy index 7dd84e07637..19c3d3076e9 100644 --- a/Test/git-issues/git-issue-289.dfy +++ b/Test/git-issues/git-issue-289.dfy @@ -1,6 +1,6 @@ -// RUN: %dafny /compile:1 "%s" > "%t" -// RUN: %dafny /compile:1 "%s" "git-issue-289b.dfy" >> "%t" -// RUN: %dafny /compile:1 "git-issue-289b.dfy" >> "%t" +// RUN: %dafny /compile:1 "%s" > "%t" +// RUN: %dafny /compile:1 "%s" %S/"git-issue-289b.dfy" >> "%t" +// RUN: %dafny /compile:1 %S/"git-issue-289b.dfy" >> "%t" // RUN: %diff "%s.expect" "%t" include "git-issue-289b.dfy" diff --git a/Test/git-issues/git-issue-314.dfy b/Test/git-issues/git-issue-314.dfy index 4426083f8bf..63624fcb076 100644 --- a/Test/git-issues/git-issue-314.dfy +++ b/Test/git-issues/git-issue-314.dfy @@ -3,8 +3,7 @@ // RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" -// RUN: sed -e 'sx\\x/x' < "%t" > "%t"2 -// RUN: %diff "%s.expect" "%t"2 +// RUN: %diff "%s.expect" "%t" datatype S = S(G: array) datatype T = T(F: array, ghost Repr: set) diff --git a/Test/git-issues/git-issue-374.dfy b/Test/git-issues/git-issue-374.dfy index d2df6a53f65..6357b6502b6 100644 --- a/Test/git-issues/git-issue-374.dfy +++ b/Test/git-issues/git-issue-374.dfy @@ -3,8 +3,7 @@ // RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" -// RUN: sed -e 'sx\\x/x' < "%t" > "%t"2 -// RUN: %diff "%s.expect" "%t"2 +// RUN: %diff "%s.expect" "%t" class C { constructor(ghost x: int) diff --git a/Test/git-issues/git-issue-633.dfy b/Test/git-issues/git-issue-633.dfy index b2081eb36ef..5d9b5aecf58 100644 --- a/Test/git-issues/git-issue-633.dfy +++ b/Test/git-issues/git-issue-633.dfy @@ -1,10 +1,9 @@ -// RUN: %dafny /compile:0 "%s" git-issue-633A.dfy > "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:cs /spillTargetCode:3 "%s" git-issue-633A.dfy >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:js /spillTargetCode:3 "%s" git-issue-633A.dfy >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go /spillTargetCode:3 "%s" git-issue-633A.dfy >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:java /spillTargetCode:3 "%s" git-issue-633A.dfy >> "%t" -// RUN: sed -e 'sx\\x/x' < "%t" > "%t"2 -// RUN: %diff "%s.expect" "%t"2 +// RUN: %dafny /compile:0 "%s" %S/git-issue-633A.dfy > "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:cs /spillTargetCode:3 "%s" %S/git-issue-633A.dfy >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:js /spillTargetCode:3 "%s" %S/git-issue-633A.dfy >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:go /spillTargetCode:3 "%s" %S/git-issue-633A.dfy >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:java /spillTargetCode:3 "%s" %S/git-issue-633A.dfy >> "%t" +// RUN: %diff "%s.expect" "%t" method m() { print "OK\n"; diff --git a/Test/git-issues/git-issue-684.dfy b/Test/git-issues/git-issue-684.dfy index 464554bbec4..43ab71ad447 100644 --- a/Test/git-issues/git-issue-684.dfy +++ b/Test/git-issues/git-issue-684.dfy @@ -3,8 +3,7 @@ // RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" -// RUN: sed -e 'sx\\x/x' < "%t" > "%t"2 -// RUN: %diff "%s.expect" "%t"2 +// RUN: %diff "%s.expect" "%t" datatype Level1 = Level1(u:int) datatype Level2 = Level2(u:int, l:Level1) diff --git a/Test/git-issues/git-issue-784.dfy b/Test/git-issues/git-issue-784.dfy index a11fba2c337..6ef11e09cce 100644 --- a/Test/git-issues/git-issue-784.dfy +++ b/Test/git-issues/git-issue-784.dfy @@ -3,8 +3,7 @@ // RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" -// RUN: sed -e 'sx\\x/x' < "%t" > "%t"2 -// RUN: %diff "%s.expect" "%t"2 +// RUN: %diff "%s.expect" "%t" datatype List = Nil | Cons(T, List) { function method App(ys: List): List { diff --git a/Test/git-issues/git-issue-801.dfy b/Test/git-issues/git-issue-801.dfy deleted file mode 100644 index 40c1d1737c7..00000000000 --- a/Test/git-issues/git-issue-801.dfy +++ /dev/null @@ -1,6 +0,0 @@ -// RUN: %dafny /compile:0 /verifyAllModules "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -// This tests that an example in the Reference Manual behaves as expected - -include "../../docs/DafnyRef/examples/Example-Old.dfy" diff --git a/Test/git-issues/git-issue-801.dfy.expect b/Test/git-issues/git-issue-801.dfy.expect deleted file mode 100644 index 823a60a105c..00000000000 --- a/Test/git-issues/git-issue-801.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 1 verified, 0 errors diff --git a/Test/git-issues/git-issue-801a.dfy b/Test/git-issues/git-issue-801a.dfy deleted file mode 100644 index 62db778a3c0..00000000000 --- a/Test/git-issues/git-issue-801a.dfy +++ /dev/null @@ -1,6 +0,0 @@ -// RUN: %dafny /compile:0 /verifyAllModules "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -// This tests that an example in the Reference Manual behaves as expected - -include "../../docs/DafnyRef/examples/Example-Old2.dfy" diff --git a/Test/git-issues/git-issue-801a.dfy.expect b/Test/git-issues/git-issue-801a.dfy.expect deleted file mode 100644 index ba00363fc08..00000000000 --- a/Test/git-issues/git-issue-801a.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 4 verified, 0 errors diff --git a/Test/git-issues/git-issue-801b.dfy b/Test/git-issues/git-issue-801b.dfy deleted file mode 100644 index fa4def880e6..00000000000 --- a/Test/git-issues/git-issue-801b.dfy +++ /dev/null @@ -1,6 +0,0 @@ -// RUN: %dafny /compile:0 /verifyAllModules "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -// This tests that an example in the Reference Manual behaves as expected - -include "../../docs/DafnyRef/examples/Example-Old3.dfy" diff --git a/Test/git-issues/git-issue-801b.dfy.expect b/Test/git-issues/git-issue-801b.dfy.expect deleted file mode 100644 index ebe2328e072..00000000000 --- a/Test/git-issues/git-issue-801b.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 2 verified, 0 errors diff --git a/Test/git-issues/git-issue-845.dfy b/Test/git-issues/git-issue-845.dfy index 0a3fe4963d1..3fe9a576338 100644 --- a/Test/git-issues/git-issue-845.dfy +++ b/Test/git-issues/git-issue-845.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /useBaseNameForFileName /compile:0 git-issue-845.dfy > "%t" +// RUN: %dafny /useBaseNameForFileName /compile:0 %S/git-issue-845.dfy > "%t" // RUN: %diff "%s.expect" "%t" /* blah blah /* blah */ diff --git a/Test/git-issues/git-issue-950.dfy b/Test/git-issues/git-issue-950.dfy index 12f3eada5c3..c16a1487d5b 100644 --- a/Test/git-issues/git-issue-950.dfy +++ b/Test/git-issues/git-issue-950.dfy @@ -1,6 +1,6 @@ // RUN: %dafny /compile:0 "%s" "%s" > "%t" -// RUN: %dafny /compile:0 "%s" git-issue-950.dfy >> "%t" -// RUN: %dafny /compile:0 "%s" ../git-issues/git-issue-950.dfy >> "%t" +// RUN: %dafny /compile:0 "%s" %S/git-issue-950.dfy >> "%t" +// RUN: %dafny /compile:0 "%s" %S/../git-issues/git-issue-950.dfy >> "%t" // RUN: %diff "%s.expect" "%t" module M { diff --git a/Test/git-issues/github-issue-305-b.dfy b/Test/git-issues/github-issue-305-b.dfy index 6520077a8f3..0ff3e7eb2df 100644 --- a/Test/git-issues/github-issue-305-b.dfy +++ b/Test/git-issues/github-issue-305-b.dfy @@ -1,6 +1,4 @@ -// UNSUPPORTED: windows -// RUN: %baredafny /countVerificationErrors:0 /compile:0 /spillTargetCode:2 "%s" > "%t.2" -// RUN: sed -e "s:%S:...:" -e 'sx\\x/x' < "%t.2" > "%t" +// RUN: %dafny /countVerificationErrors:0 /compile:0 /spillTargetCode:2 /useBaseNameForFileName "%s" > "%t" // RUN: %diff "%s".expect "%t" method hasNoBody() diff --git a/Test/git-issues/github-issue-305-b.dfy.expect b/Test/git-issues/github-issue-305-b.dfy.expect index 5900ae61de3..886f0b876f8 100644 --- a/Test/git-issues/github-issue-305-b.dfy.expect +++ b/Test/git-issues/github-issue-305-b.dfy.expect @@ -1,4 +1,4 @@ Dafny program verifier finished with 1 verified, 0 errors -.../github-issue-305-b.dfy(6,7): Error: Method _module._default.hasNoBody has no body +github-issue-305-b.dfy(4,7): Error: Method _module._default.hasNoBody has no body Wrote textual form of partial target program to github-issue-305-b.cs diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg index 79dfe84848d..6a4c61f5504 100644 --- a/Test/lit.site.cfg +++ b/Test/lit.site.cfg @@ -139,10 +139,12 @@ lit_config.note('%baredafny will expand to {}\n'.format(bareDafnyExecutable)) ver = "0" if os.name != "nt": ver = os.uname().version - + +config.substitutions.append( ('%binaryDir', binaryDir) ) config.substitutions.append( ('%dafny', dafnyExecutable) ) config.substitutions.append( ('%baredafny', bareDafnyExecutable) ) config.substitutions.append( ('%server', serverExecutable) ) +config.substitutions.append( ('%refmanexamples', os.path.join(repositoryRoot, 'docs', 'DafnyRef', 'examples')) ) config.substitutions.append( ('%os', os.name) ) config.substitutions.append( ('%ver', ver ) ) if os.name == "nt": diff --git a/Test/refman/Example-BV.dfy b/Test/refman/Example-BV.dfy index 3193a62ed35..3e9e45471be 100644 --- a/Test/refman/Example-BV.dfy +++ b/Test/refman/Example-BV.dfy @@ -1,4 +1,2 @@ -// RUN: %dafny /verifyAllModules /compile:0 "%s" > "%t" +// RUN: %dafny /compile:0 "%refmanexamples/Example-BV.dfy" > "%t" // RUN: %diff "%s.expect" "%t" - -include "../../docs/DafnyRef/examples/Example-BV.dfy" diff --git a/Test/refman/Example-BV.dfy.expect b/Test/refman/Example-BV.dfy.expect index 56c0f90a9ea..28c69a05cfa 100644 --- a/Test/refman/Example-BV.dfy.expect +++ b/Test/refman/Example-BV.dfy.expect @@ -1,3 +1,2 @@ -Example-BV.dfy(4,8): Error: the included file Example-BV.dfy contains error(s) Example-BV.dfy(3,16): Error: literal (5) is too large for the bitvector type bv2 -2 resolution/type errors detected in Example-BV.dfy +1 resolution/type errors detected in Example-BV.dfy diff --git a/Test/refman/Example-BV2.dfy b/Test/refman/Example-BV2.dfy index 33919883ffa..f66199c7cbc 100644 --- a/Test/refman/Example-BV2.dfy +++ b/Test/refman/Example-BV2.dfy @@ -1,4 +1,2 @@ -// RUN: %dafny /verifyAllModules /compile:0 "%s" > "%t" +// RUN: %dafny /compile:0 "%refmanexamples/Example-BV2.dfy" > "%t" // RUN: %diff "%s.expect" "%t" - -include "../../docs/DafnyRef/examples/Example-BV2.dfy" diff --git a/Test/refman/Example-BV3.dfy b/Test/refman/Example-BV3.dfy index 80ee757591e..80d51871b46 100644 --- a/Test/refman/Example-BV3.dfy +++ b/Test/refman/Example-BV3.dfy @@ -1,4 +1,2 @@ -// RUN: %dafny /verifyAllModules /compile:0 "%s" > "%t" +// RUN: %dafny /compile:0 "%refmanexamples/Example-BV3.dfy" > "%t" // RUN: %diff "%s.expect" "%t" - -include "../../docs/DafnyRef/examples/Example-BV3.dfy" diff --git a/Test/refman/Example-BV3.dfy.expect b/Test/refman/Example-BV3.dfy.expect index dc2aaf305b5..2ef059a5281 100644 --- a/Test/refman/Example-BV3.dfy.expect +++ b/Test/refman/Example-BV3.dfy.expect @@ -1,4 +1,3 @@ -Example-BV3.dfy(4,8): Error: the included file Example-BV3.dfy contains error(s) Example-BV3.dfy(5,15): Error: Ambiguous use of &, |, ^. Use parentheses to disambiguate. Example-BV3.dfy(5,17): Error: invalid AssertStmt 2 parse errors detected in Example-BV3.dfy diff --git a/Test/refman/Example-BV3a.dfy b/Test/refman/Example-BV3a.dfy index 73e8d30624f..0a15bdb54f2 100644 --- a/Test/refman/Example-BV3a.dfy +++ b/Test/refman/Example-BV3a.dfy @@ -1,4 +1,2 @@ -// RUN: %dafny /verifyAllModules /compile:0 "%s" > "%t" +// RUN: %dafny /compile:0 "%refmanexamples/Example-BV3a.dfy" > "%t" // RUN: %diff "%s.expect" "%t" - -include "../../docs/DafnyRef/examples/Example-BV3a.dfy" diff --git a/Test/refman/Example-BV3a.dfy.expect b/Test/refman/Example-BV3a.dfy.expect index fcb849d2383..3e13831ff2c 100644 --- a/Test/refman/Example-BV3a.dfy.expect +++ b/Test/refman/Example-BV3a.dfy.expect @@ -1,3 +1,2 @@ -Example-BV3a.dfy(4,8): Error: the included file Example-BV3a.dfy contains error(s) Example-BV3a.dfy(5,18): Error: arguments must have comparable types (got bv5 and bv6) -2 resolution/type errors detected in Example-BV3a.dfy +1 resolution/type errors detected in Example-BV3a.dfy diff --git a/Test/refman/Example-BV4.dfy b/Test/refman/Example-BV4.dfy index 2ea33e062b7..c43476b8a96 100644 --- a/Test/refman/Example-BV4.dfy +++ b/Test/refman/Example-BV4.dfy @@ -1,4 +1,2 @@ -// RUN: %dafny /verifyAllModules /compile:0 "%s" > "%t" +// RUN: %dafny /compile:0 "%refmanexamples/Example-BV4.dfy" > "%t" // RUN: %diff "%s.expect" "%t" - -include "../../docs/DafnyRef/examples/Example-BV4.dfy" diff --git a/Test/refman/Example-BV4a.dfy b/Test/refman/Example-BV4a.dfy index c9953f79088..3be99c692a9 100644 --- a/Test/refman/Example-BV4a.dfy +++ b/Test/refman/Example-BV4a.dfy @@ -1,4 +1,2 @@ -// RUN: %dafny /verifyAllModules /compile:0 "%s" > "%t" +// RUN: %dafny /compile:0 "%refmanexamples/Example-BV4a.dfy" > "%t" // RUN: %diff "%s.expect" "%t" - -include "../../docs/DafnyRef/examples/Example-BV4a.dfy" diff --git a/Test/refman/Example-BV4a.dfy.expect b/Test/refman/Example-BV4a.dfy.expect index 735287b4160..6f491b5f83d 100644 --- a/Test/refman/Example-BV4a.dfy.expect +++ b/Test/refman/Example-BV4a.dfy.expect @@ -1,3 +1,2 @@ -Example-BV4a.dfy(4,8): Error: the included file Example-BV4a.dfy contains error(s) Example-BV4a.dfy(4,14): Error: literal (25) is too large for the bitvector type bv4 -2 resolution/type errors detected in Example-BV4a.dfy +1 resolution/type errors detected in Example-BV4a.dfy diff --git a/Test/refman/Example-Fail1.dfy b/Test/refman/Example-Fail1.dfy index 6a554b6dc76..ffc862a059a 100644 --- a/Test/refman/Example-Fail1.dfy +++ b/Test/refman/Example-Fail1.dfy @@ -1,4 +1,2 @@ -// RUN: %dafny /verifyAllModules /compile:0 "%s" > "%t" +// RUN: %dafny /compile:0 "%refmanexamples/Example-Fail1.dfy" > "%t" // RUN: %diff "%s.expect" "%t" - -include "../../docs/DafnyRef/examples/Example-Fail1.dfy" diff --git a/Test/refman/Example-Fail2.dfy b/Test/refman/Example-Fail2.dfy index 2aeb6a61f50..46e02553270 100644 --- a/Test/refman/Example-Fail2.dfy +++ b/Test/refman/Example-Fail2.dfy @@ -1,4 +1,2 @@ -// RUN: %dafny /verifyAllModules /compile:0 "%s" > "%t" +// RUN: %dafny /compile:0 "%refmanexamples/Example-Fail2.dfy" > "%t" // RUN: %diff "%s.expect" "%t" - -include "../../docs/DafnyRef/examples/Example-Fail2.dfy" diff --git a/Test/refman/Example-Old.dfy b/Test/refman/Example-Old.dfy index c7885310028..70dc1cb3b13 100644 --- a/Test/refman/Example-Old.dfy +++ b/Test/refman/Example-Old.dfy @@ -1,4 +1,2 @@ -// RUN: %dafny /verifyAllModules /compile:0 "%s" > "%t" +// RUN: %dafny /compile:0 "%refmanexamples/Example-Old.dfy" > "%t" // RUN: %diff "%s.expect" "%t" - -include "../../docs/DafnyRef/examples/Example-Old.dfy" diff --git a/Test/refman/Example-Old2.dfy b/Test/refman/Example-Old2.dfy index f039906e3a1..49d5dba8fec 100644 --- a/Test/refman/Example-Old2.dfy +++ b/Test/refman/Example-Old2.dfy @@ -1,4 +1,2 @@ -// RUN: %dafny /verifyAllModules /compile:0 "%s" > "%t" +// RUN: %dafny /compile:0 "%refmanexamples/Example-Old2.dfy" > "%t" // RUN: %diff "%s.expect" "%t" - -include "../../docs/DafnyRef/examples/Example-Old2.dfy" diff --git a/Test/refman/Example-Old3.dfy b/Test/refman/Example-Old3.dfy index 21f3f15a2f6..3fc3d6a817c 100644 --- a/Test/refman/Example-Old3.dfy +++ b/Test/refman/Example-Old3.dfy @@ -1,4 +1,2 @@ -// RUN: %dafny /verifyAllModules /compile:0 "%s" > "%t" +// RUN: %dafny /compile:0 "%refmanexamples/Example-Old3.dfy" > "%t" // RUN: %diff "%s.expect" "%t" - -include "../../docs/DafnyRef/examples/Example-Old3.dfy" diff --git a/Test/refman/Example-RM.dfy b/Test/refman/Example-RM.dfy index 3ca112f5067..1868d4baa77 100644 --- a/Test/refman/Example-RM.dfy +++ b/Test/refman/Example-RM.dfy @@ -1,4 +1,2 @@ -// RUN: %dafny /verifyAllModules /compile:0 "%s" > "%t" +// RUN: %dafny /compile:0 "%refmanexamples/Example-RM.dfy" > "%t" // RUN: %diff "%s.expect" "%t" - -include "../../docs/DafnyRef/examples/Example-RM.dfy" diff --git a/Test/refman/Example-Refines1.dfy b/Test/refman/Example-Refines1.dfy index 803ab0cc2fc..6eea84e5f22 100644 --- a/Test/refman/Example-Refines1.dfy +++ b/Test/refman/Example-Refines1.dfy @@ -1,4 +1,2 @@ -// RUN: %dafny /verifyAllModules /compile:0 "%s" > "%t" +// RUN: %dafny /compile:0 "%refmanexamples/Example-Refines1.dfy" > "%t" // RUN: %diff "%s.expect" "%t" - -include "../../docs/DafnyRef/examples/Example-Refines1.dfy" diff --git a/Test/refman/Example-TP.dfy b/Test/refman/Example-TP.dfy index 436623cdc42..c60c1e9c4f1 100644 --- a/Test/refman/Example-TP.dfy +++ b/Test/refman/Example-TP.dfy @@ -1,4 +1,2 @@ -// RUN: %dafny /verifyAllModules /compile:0 "%s" > "%t" +// RUN: %dafny /compile:0 "%refmanexamples/Example-TP.dfy" > "%t" // RUN: %diff "%s.expect" "%t" - -include "../../docs/DafnyRef/examples/Example-TP.dfy" diff --git a/Test/refman/Example-TP.dfy.expect b/Test/refman/Example-TP.dfy.expect index 621e8e98509..fdcb26204e0 100644 --- a/Test/refman/Example-TP.dfy.expect +++ b/Test/refman/Example-TP.dfy.expect @@ -1,4 +1,3 @@ -Example-TP.dfy(4,8): Error: the included file Example-TP.dfy contains error(s) Example-TP.dfy(10,10): Error: type parameter (T) passed to type ResultN must support no references (got C) Example-TP.dfy(12,10): Error: type parameter (T) passed to type ResultN must support no references (got array) -3 resolution/type errors detected in Example-TP.dfy +2 resolution/type errors detected in Example-TP.dfy diff --git a/Test/refman/Example-TwoState.dfy b/Test/refman/Example-TwoState.dfy index 7a9cf0f3f8b..32fc5161de9 100644 --- a/Test/refman/Example-TwoState.dfy +++ b/Test/refman/Example-TwoState.dfy @@ -1,18 +1,2 @@ -// RUN: %dafny /verifyAllModules /compile:0 "%s" > "%t" +// RUN: %dafny /verifyAllModules /compile:0 "%refmanexamples/Example-TwoState.dfy" > "%t" // RUN: %diff "%s.expect" "%t" - -include "../../docs/DafnyRef/examples/Example-TwoState-Increasing.dfy" -include "../../docs/DafnyRef/examples/Example-TwoState-Caller.dfy" -include "../../docs/DafnyRef/examples/Example-TwoState-Diff.dfy" -include "../../docs/DafnyRef/examples/Example-TwoState-DiffAgain.dfy" -include "../../docs/DafnyRef/examples/Example-TwoState-SeqSum.dfy" -include "../../docs/DafnyRef/examples/Example-TwoState-EtaExample.dfy" - -class Cell { - var data: int - constructor (x: int) - ensures data == x - { - data := x; - } -} diff --git a/Test/wishlist/we-should-always-print-tooltips.dfy b/Test/wishlist/we-should-always-print-tooltips.dfy index e70f612062f..50540907a10 100644 --- a/Test/wishlist/we-should-always-print-tooltips.dfy +++ b/Test/wishlist/we-should-always-print-tooltips.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /printTooltips we-should-always-print-tooltips.dfy > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /printTooltips %S/we-should-always-print-tooltips.dfy > "%t" // RUN: %diff "%s.expect" "%t" // WISH it would be great to add /printTooltips to all tests diff --git a/customBoogie.patch b/customBoogie.patch index 2e3eff57ac5..a6f8e5c3b1b 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -2,7 +2,7 @@ diff --git a/Source/Dafny.sln b/Source/Dafny.sln index 3cc1738d..789c04ca 100644 --- a/Source/Dafny.sln +++ b/Source/Dafny.sln -@@ -26,6 +26,30 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyTestGeneration", "Dafn +@@ -30,6 +30,30 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyTestGeneration", "Dafn EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyTestGeneration.Test", "DafnyTestGeneration.Test\DafnyTestGeneration.Test.csproj", "{896E7F24-FD59-4B34-A1BF-53C51DDBC9E9}" EndProject @@ -33,7 +33,7 @@ index 3cc1738d..789c04ca 100644 Global GlobalSection(SolutionConfigurationPlatforms) = preSolution Debug|Any CPU = Debug|Any CPU -@@ -68,6 +92,64 @@ Global +@@ -80,6 +104,64 @@ Global {896E7F24-FD59-4B34-A1BF-53C51DDBC9E9}.Debug|Any CPU.Build.0 = Debug|Any CPU {896E7F24-FD59-4B34-A1BF-53C51DDBC9E9}.Release|Any CPU.ActiveCfg = Release|Any CPU {896E7F24-FD59-4B34-A1BF-53C51DDBC9E9}.Release|Any CPU.Build.0 = Release|Any CPU diff --git a/docs/DafnyRef/examples/Example-TwoState.dfy b/docs/DafnyRef/examples/Example-TwoState.dfy new file mode 100644 index 00000000000..98297f526d1 --- /dev/null +++ b/docs/DafnyRef/examples/Example-TwoState.dfy @@ -0,0 +1,18 @@ + +// This file only exists to include these examples as a test case. + +include "Example-TwoState-Increasing.dfy" +include "Example-TwoState-Caller.dfy" +include "Example-TwoState-Diff.dfy" +include "Example-TwoState-DiffAgain.dfy" +include "Example-TwoState-SeqSum.dfy" +include "Example-TwoState-EtaExample.dfy" + +class Cell { + var data: int + constructor (x: int) + ensures data == x + { + data := x; + } +}