diff --git a/.github/workflows/check-deep-tests-reusable.yml b/.github/workflows/check-deep-tests-reusable.yml index c2c6e23dcd2..41770e4c400 100644 --- a/.github/workflows/check-deep-tests-reusable.yml +++ b/.github/workflows/check-deep-tests-reusable.yml @@ -16,7 +16,7 @@ jobs: uses: actions/checkout@v3 with: path: dafny - submodules: recursive + submodules: true - uses: actions/github-script@v6 if: github.repository_owner == 'dafny-lang' with: diff --git a/.github/workflows/deep-tests.yml b/.github/workflows/deep-tests.yml index 16228a31723..abe08ca34c1 100644 --- a/.github/workflows/deep-tests.yml +++ b/.github/workflows/deep-tests.yml @@ -32,7 +32,6 @@ jobs: uses: actions/checkout@v3 with: ref: ${{ inputs.sha }} - submodules: recursive - name: Get short sha run: echo "sha_short=`git rev-parse --short HEAD`" >> $GITHUB_ENV diff --git a/.github/workflows/integration-tests-reusable.yml b/.github/workflows/integration-tests-reusable.yml index 759fdde00b4..434fd3a76b7 100644 --- a/.github/workflows/integration-tests-reusable.yml +++ b/.github/workflows/integration-tests-reusable.yml @@ -98,7 +98,7 @@ jobs: uses: actions/checkout@v3 with: path: dafny - submodules: true # Until the libraries work again + submodules: false # Until the libraries work again # - name: Clean up libraries for testing # run: | # rm dafny/Test/libraries/lit.site.cfg # we remove the lit configuration file in the library repo (a git submodule) to prevent override diff --git a/.github/workflows/msbuild.yml b/.github/workflows/msbuild.yml index 2bbbd0b8b19..91e8d18540b 100644 --- a/.github/workflows/msbuild.yml +++ b/.github/workflows/msbuild.yml @@ -32,7 +32,6 @@ jobs: uses: actions/checkout@v3 with: path: dafny - submodules: recursive - name: Restore tools working-directory: dafny run: dotnet tool restore @@ -87,7 +86,6 @@ jobs: uses: actions/checkout@v3 with: path: dafny - submodules: recursive - name: Setup dotnet uses: actions/setup-dotnet@v3 diff --git a/.github/workflows/runtime-tests.yml b/.github/workflows/runtime-tests.yml index ad927af4867..9f8a15f8d3b 100644 --- a/.github/workflows/runtime-tests.yml +++ b/.github/workflows/runtime-tests.yml @@ -24,8 +24,6 @@ jobs: steps: - name: Checkout Dafny uses: actions/checkout@v3 - with: - submodules: true - name: Set up JDK 18 uses: actions/setup-java@v3 with: diff --git a/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs b/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs index f71835f6ce2..ed0580e97fe 100644 --- a/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs +++ b/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs @@ -26,7 +26,7 @@ public override Expression CloneExpr(Expression expr) { var e = (FunctionCallExpr)expr; #if DEBUG_PRINT if (e.Function.Name.EndsWith("#") && Contract.Exists(focalPredicates, p => e.Function.Name == p.Name + "#")) { - Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(e)); + Console.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(e)); } #endif // Note, we don't actually ever get here, because all calls will have been parsed as ApplySuffix. @@ -37,7 +37,7 @@ public override Expression CloneExpr(Expression expr) { if (f != null && focalPredicates.Contains(f)) { #if DEBUG_PRINT var r = CloneCallAndAddK(e); - Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(r)); + Console.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(r)); return r; #else return CloneCallAndAddK(e); @@ -58,14 +58,14 @@ public override Expression CloneExpr(Expression expr) { if (fce != null) { #if DEBUG_PRINT if (fce.Function.Name.EndsWith("#") && Contract.Exists(focalPredicates, p => fce.Function.Name == p.Name + "#")) { - Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(fce)); + Console.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(fce)); } #endif var f = fce.Function as ExtremePredicate; if (f != null && focalPredicates.Contains(f)) { #if DEBUG_PRINT var r = CloneCallAndAddK(fce); - Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(r)); + Console.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(r)); return r; #else return CloneCallAndAddK(fce); diff --git a/Source/DafnyCore/AST/Grammar/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer.cs index 98f84801b44..d120d38f90e 100644 --- a/Source/DafnyCore/AST/Grammar/Printer.cs +++ b/Source/DafnyCore/AST/Grammar/Printer.cs @@ -194,10 +194,6 @@ public static string ToStringWithoutNewline(System.IO.StringWriter wr) { return sb.ToString(0, len); } - public void PrintProgramLargeStack(Program prog, bool afterResolver) { - DafnyMain.LargeStackFactory.StartNew(() => PrintProgram(prog, afterResolver)).Wait(); - } - public void PrintProgram(Program prog, bool afterResolver) { Contract.Requires(prog != null); this.afterResolver = afterResolver; diff --git a/Source/DafnyCore/AST/Types/Types.cs b/Source/DafnyCore/AST/Types/Types.cs index 6dd24bd0600..158f336d9fc 100644 --- a/Source/DafnyCore/AST/Types/Types.cs +++ b/Source/DafnyCore/AST/Types/Types.cs @@ -1285,7 +1285,7 @@ public static Type Join(Type a, Type b, BuiltIns builtIns) { Contract.Requires(builtIns != null); var j = JoinX(a, b, builtIns); if (builtIns.Options.Get(CommonOptionBag.TypeInferenceDebug)) { - builtIns.Options.OutputWriter.WriteLine("DEBUG: Join( {0}, {1} ) = {2}", a, b, j); + Console.WriteLine("DEBUG: Join( {0}, {1} ) = {2}", a, b, j); } return j; } @@ -1506,7 +1506,7 @@ public static Type Meet(Type a, Type b, BuiltIns builtIns) { } } if (builtIns.Options.Get(CommonOptionBag.TypeInferenceDebug)) { - builtIns.Options.OutputWriter.WriteLine("DEBUG: Meet( {0}, {1} ) = {2}", a, b, j); + Console.WriteLine("DEBUG: Meet( {0}, {1} ) = {2}", a, b, j); } return j; } diff --git a/Source/DafnyCore/Auditor/Auditor.cs b/Source/DafnyCore/Auditor/Auditor.cs index e67a2aa469e..020885ee5df 100644 --- a/Source/DafnyCore/Auditor/Auditor.cs +++ b/Source/DafnyCore/Auditor/Auditor.cs @@ -137,7 +137,7 @@ internal override void PostResolve(Program program) { _ => $"Internal error: unknown format {reportFormat}" }; if (reportFileName is null) { - Options.OutputWriter.Write(text); + Console.Write(text); } else { if (compareReport) { try { diff --git a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs index 3ae104e763b..9bcda7fd364 100644 --- a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs +++ b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs @@ -110,7 +110,7 @@ void EmitDafnySourceAttribute(Program program, ConcreteSyntaxTree wr) { stringWriter.NewLine = Environment.NewLine; var oldValue = Options.ShowEnv; Options.ShowEnv = ExecutionEngineOptions.ShowEnvironment.DuringPrint; - new Printer(stringWriter, Options, PrintModes.Serialization).PrintProgramLargeStack(program, true); + new Printer(stringWriter, Options, PrintModes.Serialization).PrintProgram(program, true); Options.ShowEnv = oldValue; var programString = stringWriter.GetStringBuilder().Replace("\"", "\"\"").ToString(); diff --git a/Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs b/Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs index b6cc80d8792..893ca63fed6 100644 --- a/Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs +++ b/Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs @@ -5,7 +5,6 @@ using System.Linq; using System.Reflection; using System.Runtime.Loader; -using System.Text; using System.Text.Json; using Microsoft.CodeAnalysis; using Microsoft.CodeAnalysis.CSharp; @@ -45,6 +44,7 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target MetadataReference.CreateFromFile(typeof(object).GetTypeInfo().Assembly.Location), MetadataReference.CreateFromFile(Assembly.Load("mscorlib").Location)); + var inMemory = runAfterCompile; compilation = compilation.WithOptions(compilation.Options.WithOutputKind(callToMain != null ? OutputKind.ConsoleApplication : OutputKind.DynamicallyLinkedLibrary)); var tempCompilationResult = new CSharpCompilationResult(); @@ -93,40 +93,54 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target var outputDir = targetFilename == null ? Directory.GetCurrentDirectory() : Path.GetDirectoryName(Path.GetFullPath(targetFilename)); var outputPath = Path.Join(outputDir, Path.GetFileNameWithoutExtension(Path.GetFileName(dafnyProgramName)) + ".dll"); var outputJson = Path.Join(outputDir, Path.GetFileNameWithoutExtension(Path.GetFileName(dafnyProgramName)) + ".runtimeconfig.json"); - var emitResult = compilation.Emit(outputPath); - - if (emitResult.Success) { - tempCompilationResult.CompiledAssembly = Assembly.LoadFile(outputPath); - if (Options.CompileVerbose) { - outputWriter.WriteLine("Compiled assembly into {0}.dll", compilation.AssemblyName); + if (inMemory) { + using var stream = new MemoryStream(); + var emitResult = compilation.Emit(stream); + if (emitResult.Success) { + tempCompilationResult.CompiledAssembly = Assembly.Load(stream.GetBuffer()); + } else { + outputWriter.WriteLine("Errors compiling program:"); + var errors = emitResult.Diagnostics.Where(d => d.Severity == DiagnosticSeverity.Error).ToList(); + foreach (var ce in errors) { + outputWriter.WriteLine(ce.ToString()); + outputWriter.WriteLine(); + } + return false; } + } else { + var emitResult = compilation.Emit(outputPath); - try { - var configuration = JsonSerializer.Serialize( - new { - runtimeOptions = new { - tfm = "net6.0", - framework = new { - name = "Microsoft.NETCore.App", - version = "6.0.0", - rollForward = "LatestMinor" + if (emitResult.Success) { + tempCompilationResult.CompiledAssembly = Assembly.LoadFile(outputPath); + if (Options.CompileVerbose) { + outputWriter.WriteLine("Compiled assembly into {0}.dll", compilation.AssemblyName); + } + try { + var configuration = JsonSerializer.Serialize( + new { + runtimeOptions = new { + tfm = "net6.0", + framework = new { + name = "Microsoft.NETCore.App", + version = "6.0.0", + rollForward = "LatestMinor" + } } - } - }, new JsonSerializerOptions() { WriteIndented = true }); - File.WriteAllText(outputJson, configuration + Environment.NewLine); - } catch (Exception e) { - outputWriter.WriteLine($"Error trying to write '{outputJson}': {e.Message}"); + }, new JsonSerializerOptions() { WriteIndented = true }); + File.WriteAllText(outputJson, configuration + Environment.NewLine); + } catch (Exception e) { + outputWriter.WriteLine($"Error trying to write '{outputJson}': {e.Message}"); + return false; + } + } else { + outputWriter.WriteLine("Errors compiling program into {0}", compilation.AssemblyName); + var errors = emitResult.Diagnostics.Where(d => d.Severity == DiagnosticSeverity.Error).ToList(); + foreach (var ce in errors) { + outputWriter.WriteLine(ce.ToString()); + outputWriter.WriteLine(); + } return false; } - } else { - outputWriter.WriteLine("Errors compiling program into {0}", compilation.AssemblyName); - var errors = emitResult.Diagnostics.Where(d => d.Severity == DiagnosticSeverity.Error).ToList(); - foreach (var ce in errors) { - outputWriter.WriteLine(ce.ToString()); - outputWriter.WriteLine(); - } - - return false; } compilationResult = tempCompilationResult; @@ -137,24 +151,37 @@ private class CSharpCompilationResult { public Assembly CompiledAssembly; } - public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, - string targetFilename /*?*/, ReadOnlyCollection otherFileNames, - object compilationResult, TextWriter outputWriter, TextWriter errorWriter) { + public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, string/*?*/ targetFilename, ReadOnlyCollection otherFileNames, + object compilationResult, TextWriter outputWriter) { var crx = (CSharpCompilationResult)compilationResult; foreach (var otherFileName in otherFileNames) { if (Path.GetExtension(otherFileName) == ".dll") { - var targetDirectory = Path.GetDirectoryName(crx.CompiledAssembly.Location); - File.Copy(otherFileName, Path.Combine(targetDirectory!, Path.GetFileName(otherFileName)), true); + AssemblyLoadContext.Default.LoadFromAssemblyPath(Path.GetFullPath(otherFileName)); } } if (crx.CompiledAssembly == null) { throw new Exception("Cannot call run target program on a compilation that failed"); } - var psi = PrepareProcessStartInfo("dotnet", new[] { crx.CompiledAssembly.Location }.Concat(Options.MainArgs)); - return RunProcess(psi, outputWriter, errorWriter) == 0; + var entry = crx.CompiledAssembly.EntryPoint; + if (entry == null) { + throw new Exception("Cannot call run target on a compilation whose assembly has no entry."); + } + try { + Console.OutputEncoding = System.Text.Encoding.UTF8; // Force UTF-8 output in dafny run (#2999) + object[] parameters = entry.GetParameters().Length == 0 ? new object[] { } : new object[] { Options.MainArgs.ToArray() }; + entry.Invoke(null, parameters); + return true; + } catch (System.Reflection.TargetInvocationException e) { + outputWriter.WriteLine("Error: Execution resulted in exception: {0}", e.Message); + outputWriter.WriteLine(e.InnerException.ToString()); + } catch (System.Exception e) { + outputWriter.WriteLine("Error: Execution resulted in exception: {0}", e.Message); + outputWriter.WriteLine(e.ToString()); + } + return false; } public CsharpBackend(DafnyOptions options) : base(options) { diff --git a/Source/DafnyCore/Compilers/CoverageInstrumenter.cs b/Source/DafnyCore/Compilers/CoverageInstrumenter.cs index 0167bae5816..0bf23bacfb8 100644 --- a/Source/DafnyCore/Compilers/CoverageInstrumenter.cs +++ b/Source/DafnyCore/Compilers/CoverageInstrumenter.cs @@ -72,7 +72,7 @@ public void WriteLegendFile() { if (legend != null) { var filename = compiler.Options.CoverageLegendFile; Contract.Assert(filename != null); - TextWriter wr = filename == "-" ? compiler.Options.OutputWriter : new StreamWriter(new FileStream(Path.GetFullPath(filename), System.IO.FileMode.Create)); + TextWriter wr = filename == "-" ? System.Console.Out : new StreamWriter(new FileStream(Path.GetFullPath(filename), System.IO.FileMode.Create)); { for (var i = 0; i < legend.Count; i++) { var e = legend[i]; @@ -82,4 +82,4 @@ public void WriteLegendFile() { legend = null; } } -} +} \ No newline at end of file diff --git a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs index f173a3772fe..4de1c249fea 100644 --- a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs +++ b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs @@ -905,7 +905,7 @@ protected override void EmitJumpToTailCallStart(ConcreteSyntaxTree wr) { } protected void Warn(string msg, IToken tok) { - Options.ErrorWriter.WriteLine("WARNING: {3} ({0}:{1}:{2})", tok.Filepath, tok.line, tok.col, msg); + Console.Error.WriteLine("WARNING: {3} ({0}:{1}:{2})", tok.Filepath, tok.line, tok.col, msg); } // Because we use reference counting (via shared_ptr), the TypeName of a class differs diff --git a/Source/DafnyCore/Compilers/Cplusplus/CppCompilerBackend.cs b/Source/DafnyCore/Compilers/Cplusplus/CppCompilerBackend.cs index 9a552d15c6b..f997667ab07 100644 --- a/Source/DafnyCore/Compilers/Cplusplus/CppCompilerBackend.cs +++ b/Source/DafnyCore/Compilers/Cplusplus/CppCompilerBackend.cs @@ -19,7 +19,7 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target bool runAfterCompile, TextWriter outputWriter, out object compilationResult) { var assemblyLocation = System.Reflection.Assembly.GetExecutingAssembly().Location; Contract.Assert(assemblyLocation != null); - var codebase = Path.GetDirectoryName(assemblyLocation); + var codebase = System.IO.Path.GetDirectoryName(assemblyLocation); Contract.Assert(codebase != null); compilationResult = null; var psi = PrepareProcessStartInfo("g++", new List { @@ -37,14 +37,13 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target "-o", ComputeExeName(targetFilename), targetFilename }); - return 0 == RunProcess(psi, outputWriter, outputWriter, "Error while compiling C++ files."); + return 0 == RunProcess(psi, outputWriter, "Error while compiling C++ files."); } - public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain /*?*/, - string targetFilename, ReadOnlyCollection otherFileNames, - object compilationResult, TextWriter outputWriter, TextWriter errorWriter) { + public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string targetFilename, ReadOnlyCollection otherFileNames, + object compilationResult, TextWriter outputWriter) { var psi = PrepareProcessStartInfo(ComputeExeName(targetFilename), Options.MainArgs); - return 0 == RunProcess(psi, outputWriter, errorWriter); + return 0 == RunProcess(psi, outputWriter); } public override IReadOnlySet SupportedExtensions => new HashSet { ".h" }; diff --git a/Source/DafnyCore/Compilers/Dafny/DafnyBackend.cs b/Source/DafnyCore/Compilers/Dafny/DafnyBackend.cs index 422e17ffa85..dce809d58c2 100644 --- a/Source/DafnyCore/Compilers/Dafny/DafnyBackend.cs +++ b/Source/DafnyCore/Compilers/Dafny/DafnyBackend.cs @@ -41,14 +41,13 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target * The Dafny backend is different from the other backends in that the output code needs to be compiled * by the Dafny compiler itself to another backend for execution. */ - public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, /*?*/ - string targetFilename, ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter, - TextWriter errorWriter) { + public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string /*?*/ callToMain, + string targetFilename, ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter) { Contract.Requires(targetFilename != null || otherFileNames.Count == 0); - return RunTargetDafnyProgram(targetFilename, outputWriter, errorWriter, false); + return RunTargetDafnyProgram(targetFilename, outputWriter, false); } public DafnyBackend(DafnyOptions options) : base(options) { } -} +} \ No newline at end of file diff --git a/Source/DafnyCore/Compilers/ExecutableBackend.cs b/Source/DafnyCore/Compilers/ExecutableBackend.cs index 1c5e4ebff8f..3197893b565 100644 --- a/Source/DafnyCore/Compilers/ExecutableBackend.cs +++ b/Source/DafnyCore/Compilers/ExecutableBackend.cs @@ -5,9 +5,6 @@ using System.Diagnostics.Contracts; using System.IO; using System.Linq; -using System.Text; -using System.Threading.Tasks; -using Microsoft.Win32; namespace Microsoft.Dafny.Compilers; @@ -54,7 +51,6 @@ public ProcessStartInfo PrepareProcessStartInfo(string programName, IEnumerable< var psi = new ProcessStartInfo(programName) { UseShellExecute = false, CreateNoWindow = false, // https://github.com/dotnet/runtime/issues/68259 - RedirectStandardOutput = true, }; foreach (var arg in args ?? Enumerable.Empty()) { psi.ArgumentList.Add(arg); @@ -62,44 +58,23 @@ public ProcessStartInfo PrepareProcessStartInfo(string programName, IEnumerable< return psi; } - public int RunProcess(ProcessStartInfo psi, - TextWriter outputWriter, - TextWriter errorWriter, - string errorMessage = null) { + public int RunProcess(ProcessStartInfo psi, TextWriter outputWriter, string errorMessage = null) { return StartProcess(psi, outputWriter) is { } process ? - WaitForExit(process, outputWriter, errorWriter, errorMessage) : -1; + WaitForExit(process, outputWriter, errorMessage) : -1; } - public int WaitForExit(Process process, TextWriter outputWriter, TextWriter errorWriter, string errorMessage = null) { - - var errorProcessing = Task.Run(() => { - PassthroughBuffer(process.StandardError, errorWriter); - }); - PassthroughBuffer(process.StandardOutput, outputWriter); + public int WaitForExit(Process process, TextWriter outputWriter, string errorMessage = null) { process.WaitForExit(); if (process.ExitCode != 0 && errorMessage != null) { outputWriter.WriteLine("{0} Process exited with exit code {1}", errorMessage, process.ExitCode); } - - errorProcessing.Wait(); return process.ExitCode; } - - // We read character by character because we did not find a way to ensure - // final newlines are kept when reading line by line - protected static void PassthroughBuffer(TextReader input, TextWriter output) { - int current; - while ((current = input.Read()) != -1) { - output.Write((char)current); - } - } - public Process StartProcess(ProcessStartInfo psi, TextWriter outputWriter) { string additionalInfo = ""; try { - psi.RedirectStandardError = true; if (Process.Start(psi) is { } process) { return process; } @@ -126,9 +101,8 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target return true; } - public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain /*?*/, - string targetFilename /*?*/, ReadOnlyCollection otherFileNames, - object compilationResult, TextWriter outputWriter, TextWriter errorWriter) { + public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string/*?*/ targetFilename, ReadOnlyCollection otherFileNames, + object compilationResult, TextWriter outputWriter) { Contract.Requires(dafnyProgramName != null); Contract.Requires(targetProgramText != null); Contract.Requires(otherFileNames != null); @@ -142,7 +116,7 @@ protected static void WriteFromFile(string inputFilename, TextWriter outputWrite SinglePassCompiler.WriteFromStream(rd, outputWriter); } - protected bool RunTargetDafnyProgram(string targetFilename, TextWriter outputWriter, TextWriter errorWriter, bool verify) { + protected bool RunTargetDafnyProgram(string targetFilename, TextWriter outputWriter, bool verify) { /* * In order to work for the continuous integration, we need to call the Dafny compiler using dotnet @@ -150,7 +124,7 @@ protected bool RunTargetDafnyProgram(string targetFilename, TextWriter outputWri */ var where = System.Reflection.Assembly.GetExecutingAssembly().Location; - where = Path.GetDirectoryName(where); + where = System.IO.Path.GetDirectoryName(where); var dafny = where + "/Dafny.dll"; var opt = Options; @@ -177,24 +151,16 @@ protected bool RunTargetDafnyProgram(string targetFilename, TextWriter outputWri var process = new Process(); process.StartInfo = psi; var outputBuilder = new List(); - var errorBuilder = new List(); process.OutputDataReceived += (sender, args) => outputBuilder.Add(args.Data); - process.ErrorDataReceived += (sender, args) => errorBuilder.Add(args.Data); try { process.Start(); process.BeginOutputReadLine(); - process.BeginErrorReadLine(); process.WaitForExit(); process.CancelOutputRead(); - process.CancelErrorRead(); for (int i = 2; i < outputBuilder.Count - 1; i++) { - outputWriter.WriteLine(outputBuilder[i]); - } - - for (int i = 0; i < errorBuilder.Count - 1; i++) { - errorWriter.WriteLine(errorBuilder[i]); + Console.WriteLine(outputBuilder[i]); } if (process.ExitCode != 0) { diff --git a/Source/DafnyCore/Compilers/GoLang/GoBackend.cs b/Source/DafnyCore/Compilers/GoLang/GoBackend.cs index 59746150c2e..da53450d233 100644 --- a/Source/DafnyCore/Compilers/GoLang/GoBackend.cs +++ b/Source/DafnyCore/Compilers/GoLang/GoBackend.cs @@ -22,8 +22,7 @@ protected override SinglePassCompiler CreateCompiler() { return new GoCompiler(Options, Reporter); } - public override bool CompileTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, - string/*?*/ targetFilename, ReadOnlyCollection otherFileNames, + public override bool CompileTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string/*?*/ targetFilename, ReadOnlyCollection otherFileNames, bool runAfterCompile, TextWriter outputWriter, out object compilationResult) { compilationResult = null; if (runAfterCompile) { @@ -34,21 +33,18 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target return true; } else { // compile now - return SendToNewGoProcess(dafnyProgramName, targetFilename, otherFileNames, - outputWriter, outputWriter, callToMain != null, run: false); + return SendToNewGoProcess(dafnyProgramName, targetFilename, otherFileNames, outputWriter, callToMain != null, run: false); } } - public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain /*?*/, - string targetFilename, ReadOnlyCollection otherFileNames, - object compilationResult, TextWriter outputWriter, TextWriter errorWriter) { + public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string targetFilename, ReadOnlyCollection otherFileNames, + object compilationResult, TextWriter outputWriter) { - return SendToNewGoProcess(dafnyProgramName, targetFilename, otherFileNames, outputWriter, errorWriter, hasMain: true, run: true); + return SendToNewGoProcess(dafnyProgramName, targetFilename, otherFileNames, outputWriter, hasMain: true, run: true); } - private bool SendToNewGoProcess(string dafnyProgramName, string targetFilename, - ReadOnlyCollection otherFileNames, - TextWriter outputWriter, TextWriter errorWriter, bool hasMain, bool run) { + private bool SendToNewGoProcess(string dafnyProgramName, string targetFilename, ReadOnlyCollection otherFileNames, + TextWriter outputWriter, bool hasMain, bool run) { Contract.Requires(targetFilename != null); foreach (var otherFileName in otherFileNames) { @@ -114,7 +110,7 @@ private bool SendToNewGoProcess(string dafnyProgramName, string targetFilename, // system. Until Dafny's Go compiler catches up, the GO111MODULE variable has to be set. psi.EnvironmentVariables["GO111MODULE"] = "auto"; - return 0 == RunProcess(psi, outputWriter, errorWriter); + return 0 == RunProcess(psi, outputWriter); } static string GoPath(string filename) { diff --git a/Source/DafnyCore/Compilers/Java/JavaBackend.cs b/Source/DafnyCore/Compilers/Java/JavaBackend.cs index 8361e906257..6c7cc5f23ab 100644 --- a/Source/DafnyCore/Compilers/Java/JavaBackend.cs +++ b/Source/DafnyCore/Compilers/Java/JavaBackend.cs @@ -74,7 +74,7 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target var compileProcess = PrepareProcessStartInfo("javac", new List { "-encoding", "UTF8" }.Concat(files)); compileProcess.WorkingDirectory = Path.GetFullPath(Path.GetDirectoryName(targetFilename)); compileProcess.EnvironmentVariables["CLASSPATH"] = GetClassPath(targetFilename); - if (0 != RunProcess(compileProcess, outputWriter, outputWriter, "Error while compiling Java files.")) { + if (0 != RunProcess(compileProcess, outputWriter, "Error while compiling Java files.")) { return false; } @@ -112,26 +112,24 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target public bool CreateJar(string/*?*/ entryPointName, string jarPath, string rootDirectory, List files, TextWriter outputWriter) { - Directory.CreateDirectory(Path.GetDirectoryName(jarPath)); + System.IO.Directory.CreateDirectory(Path.GetDirectoryName(jarPath)); var args = entryPointName == null ? // If null, then no entry point is added new List { "cf", jarPath } : new List { "cfe", jarPath, entryPointName }; var jarCreationProcess = PrepareProcessStartInfo("jar", args.Concat(files)); jarCreationProcess.WorkingDirectory = rootDirectory; - return 0 == RunProcess(jarCreationProcess, outputWriter, outputWriter, "Error while creating jar file: " + jarPath); + return 0 == RunProcess(jarCreationProcess, outputWriter, "Error while creating jar file: " + jarPath); } - public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, - string targetFilename, /*?*/ - ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter, - TextWriter errorWriter) { + public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, string /*?*/ targetFilename, + ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter) { string jarPath = Path.ChangeExtension(dafnyProgramName, ".jar"); // Must match that in CompileTargetProgram var psi = PrepareProcessStartInfo("java", new List { "-Dfile.encoding=UTF-8", "-jar", jarPath } .Concat(Options.MainArgs)); // Run the target program in the user's working directory and with the user's classpath psi.EnvironmentVariables["CLASSPATH"] = GetClassPath(null); - return 0 == RunProcess(psi, outputWriter, errorWriter); + return 0 == RunProcess(psi, outputWriter); } private string GetClassPath(string targetFilename) { diff --git a/Source/DafnyCore/Compilers/JavaScript/JavaScriptBackend.cs b/Source/DafnyCore/Compilers/JavaScript/JavaScriptBackend.cs index 13130440a40..90d5f4a2d8b 100644 --- a/Source/DafnyCore/Compilers/JavaScript/JavaScriptBackend.cs +++ b/Source/DafnyCore/Compilers/JavaScript/JavaScriptBackend.cs @@ -41,9 +41,8 @@ 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, TextWriter errorWriter) { + public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string targetFilename, ReadOnlyCollection otherFileNames, + object compilationResult, TextWriter outputWriter) { return SendToNewNodeProcess(dafnyProgramName, targetProgramText, callToMain, targetFilename, otherFileNames, outputWriter); } @@ -74,9 +73,9 @@ bool SendToNewNodeProcess(string dafnyProgramName, string targetProgramText, str nodeProcess.StandardInput.Close(); // Fixes a problem of Node on Windows, where Node does not prints to the parent console its standard outputs. var errorProcessing = Task.Run(() => { - PassthroughBuffer(nodeProcess.StandardError, Options.ErrorWriter); + PassthroughBuffer(nodeProcess.StandardError, Console.Error); }); - PassthroughBuffer(nodeProcess.StandardOutput, Options.OutputWriter); + PassthroughBuffer(nodeProcess.StandardOutput, Console.Out); nodeProcess.WaitForExit(); #pragma warning disable VSTHRD002 errorProcessing.Wait(); @@ -88,6 +87,15 @@ bool SendToNewNodeProcess(string dafnyProgramName, string targetProgramText, str } } + // We read character by character because we did not find a way to ensure + // final newlines are kept when reading line by line + private static void PassthroughBuffer(TextReader input, TextWriter output) { + int current; + while ((current = input.Read()) != -1) { + output.Write((char)current); + } + } + public JavaScriptBackend(DafnyOptions options) : base(options) { } -} +} \ No newline at end of file diff --git a/Source/DafnyCore/Compilers/Library/LibraryBackend.cs b/Source/DafnyCore/Compilers/Library/LibraryBackend.cs index a8e760e3496..344cdc3456c 100644 --- a/Source/DafnyCore/Compilers/Library/LibraryBackend.cs +++ b/Source/DafnyCore/Compilers/Library/LibraryBackend.cs @@ -80,8 +80,9 @@ 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, TextWriter errorWriter) { + ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter) { + var dooPath = DooFilePath(dafnyProgramName); - return RunTargetDafnyProgram(dooPath, outputWriter, errorWriter, true); + return RunTargetDafnyProgram(dooPath, outputWriter, true); } } \ No newline at end of file diff --git a/Source/DafnyCore/Compilers/Python/PythonBackend.cs b/Source/DafnyCore/Compilers/Python/PythonBackend.cs index ac224c8d1cb..88d36545999 100644 --- a/Source/DafnyCore/Compilers/Python/PythonBackend.cs +++ b/Source/DafnyCore/Compilers/Python/PythonBackend.cs @@ -63,14 +63,6 @@ bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram, TextW return true; } - public override void CleanSourceDirectory(string sourceDirectory) { - var cacheDirectory = Path.Combine(sourceDirectory, "__pycache__"); - try { - Directory.Delete(cacheDirectory, true); - } catch (DirectoryNotFoundException) { - } - } - public override bool CompileTargetProgram(string dafnyProgramName, string targetProgramText, string /*?*/ callToMain, string /*?*/ targetFilename, ReadOnlyCollection otherFileNames, bool runAfterCompile, TextWriter outputWriter, out object compilationResult) { @@ -87,13 +79,12 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target return true; } - public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, /*?*/ - string targetFilename, ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter, - TextWriter errorWriter) { + public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string /*?*/ callToMain, + string targetFilename, ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter) { Contract.Requires(targetFilename != null || otherFileNames.Count == 0); var psi = PrepareProcessStartInfo("python3", Options.MainArgs.Prepend(targetFilename)); psi.EnvironmentVariables["PYTHONIOENCODING"] = "utf8"; - return 0 == RunProcess(psi, outputWriter, errorWriter); + return 0 == RunProcess(psi, outputWriter); } public PythonBackend(DafnyOptions options) : base(options) { diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 83366cc694a..9e0804dc723 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -141,12 +141,12 @@ bool IsAssumeTypeKeyword(IToken la) { /// Returns the number of parsing errors encountered. /// Note: first initialize the Scanner. /// -public static int Parse (TextReader fileReaderOverride, Uri/*!*/ uri, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true, bool compileThisFile=true) /* throws System.IO.IOException */ { +public static int Parse (bool useStdin, Uri/*!*/ uri, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true, bool compileThisFile=true) /* throws System.IO.IOException */ { Contract.Requires(uri != null); Contract.Requires(module != null); string s; - if (fileReaderOverride != null) { - s = Microsoft.Dafny.SourcePreprocessor.ProcessDirectives(fileReaderOverride, new List(), Environment.NewLine); + if (useStdin) { + s = Microsoft.Dafny.SourcePreprocessor.ProcessDirectives(System.Console.In, new List(), Environment.NewLine); return Parse(s, uri, module, builtIns, errors, verifyThisFile, compileThisFile); } else { var newline = SourcePreprocessor.GetNewlineStyle(uri.LocalPath); diff --git a/Source/DafnyCore/DafnyConsolePrinter.cs b/Source/DafnyCore/DafnyConsolePrinter.cs index 8416cc6ddfd..cb9e429cba9 100644 --- a/Source/DafnyCore/DafnyConsolePrinter.cs +++ b/Source/DafnyCore/DafnyConsolePrinter.cs @@ -22,17 +22,6 @@ public class DafnyConsolePrinter : ConsolePrinter { private DafnyOptions options; public ConcurrentBag<(Implementation, VerificationResult)> VerificationResults { get; } = new(); - public override void AdvisoryWriteLine(TextWriter output, string format, params object[] args) { - if (output == Console.Out) { - int foregroundColor = (int)Console.ForegroundColor; - Console.ForegroundColor = ConsoleColor.Yellow; - output.WriteLine(format, args); - Console.ForegroundColor = (ConsoleColor)foregroundColor; - } else { - output.WriteLine(format, args); - } - } - private string GetFileLine(string filename, int lineIndex) { List lines = fsCache.GetOrAdd(filename, key => { try { diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 2143621793f..4a8b2f89b56 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -31,7 +31,7 @@ - + diff --git a/Source/DafnyCore/DafnyFile.cs b/Source/DafnyCore/DafnyFile.cs deleted file mode 100644 index cc44e667409..00000000000 --- a/Source/DafnyCore/DafnyFile.cs +++ /dev/null @@ -1,178 +0,0 @@ -using System; -using System.Collections.Generic; -using System.IO; -using System.Reflection.Metadata; -using System.Reflection.PortableExecutable; -using DafnyCore; - -namespace Microsoft.Dafny; - -public class DafnyFile { - public bool UseStdin { get; private set; } - public string FilePath => Uri.LocalPath; - public string CanonicalPath { get; private set; } - public string BaseName { get; private set; } - public bool IsPreverified { get; set; } - public bool IsPrecompiled { get; set; } - public string SourceFilePath { get; private set; } - public Uri Uri { get; private set; } - - // Returns a canonical string for the given file path, namely one which is the same - // for all paths to a given file and different otherwise. The best we can do is to - // make the path absolute -- detecting case and canonicalizing symbolic and hard - // links are difficult across file systems (which may mount parts of other filesystems, - // with different characteristics) and is not supported by .Net libraries - public static Uri Canonicalize(string filePath) { - if (filePath == null || !filePath.StartsWith("file:")) { - return new Uri(Path.GetFullPath(filePath)); - } - - if (Uri.IsWellFormedUriString(filePath, UriKind.RelativeOrAbsolute)) { - return new Uri(filePath); - } - - var potentialPrefixes = new List() { "file:\\", "file:/", "file:" }; - foreach (var potentialPrefix in potentialPrefixes) { - if (filePath.StartsWith(potentialPrefix)) { - var withoutPrefix = filePath.Substring(potentialPrefix.Length); - var tentativeURI = "file:///" + withoutPrefix.Replace("\\", "/"); - if (Uri.IsWellFormedUriString(tentativeURI, UriKind.RelativeOrAbsolute)) { - return new Uri(tentativeURI); - } - // Recovery mechanisms for the language server - return new Uri(filePath.Substring(potentialPrefix.Length)); - } - } - return new Uri(filePath.Substring("file:".Length)); - } - public static List FileNames(IList dafnyFiles) { - var sourceFiles = new List(); - foreach (DafnyFile f in dafnyFiles) { - sourceFiles.Add(f.FilePath); - } - return sourceFiles; - } - public DafnyFile(DafnyOptions options, string filePath, bool useStdin = false) { - UseStdin = useStdin; - Uri = useStdin ? new Uri("stdin:///") : new Uri(filePath); - BaseName = useStdin ? "" : Path.GetFileName(filePath); - - var extension = useStdin ? ".dfy" : Path.GetExtension(filePath); - if (extension != null) { extension = extension.ToLower(); } - - // Normalizing symbolic links appears to be not - // supported in .Net APIs, because it is very difficult in general - // So we will just use the absolute path, lowercased for all file systems. - // cf. IncludeComparer.CompareTo - CanonicalPath = !useStdin ? Canonicalize(filePath).LocalPath : ""; - filePath = CanonicalPath; - - if (extension == ".dfy" || extension == ".dfyi") { - IsPreverified = false; - IsPrecompiled = false; - SourceFilePath = filePath; - } else if (extension == ".doo") { - IsPreverified = true; - IsPrecompiled = false; - - var dooFile = DooFile.Read(filePath); - - var filePathForErrors = options.UseBaseNameForFileName ? Path.GetFileName(filePath) : filePath; - if (!dooFile.Validate(filePathForErrors, options, options.CurrentCommand)) { - throw new IllegalDafnyFile(true); - } - - // For now it's simpler to let the rest of the pipeline parse the - // program text back into the AST representation. - // At some point we'll likely want to serialize a program - // more efficiently inside a .doo file, at which point - // the DooFile class should encapsulate the serialization logic better - // and expose a Program instead of the program text. - SourceFilePath = Path.GetTempFileName(); - Uri = new Uri(SourceFilePath); - File.WriteAllText(SourceFilePath, dooFile.ProgramText); - - } else if (extension == ".dll") { - IsPreverified = true; - // Technically only for C#, this is for backwards compatability - IsPrecompiled = true; - - var sourceText = GetDafnySourceAttributeText(filePath); - if (sourceText == null) { throw new IllegalDafnyFile(); } - SourceFilePath = Path.GetTempFileName(); - Uri = new Uri(SourceFilePath); - File.WriteAllText(SourceFilePath, sourceText); - - } else { - throw new IllegalDafnyFile(); - } - } - - private static string GetDafnySourceAttributeText(string dllPath) { - if (!File.Exists(dllPath)) { - throw new IllegalDafnyFile(); - } - using var dllFs = new FileStream(dllPath, FileMode.Open, FileAccess.Read, FileShare.ReadWrite); - using var dllPeReader = new PEReader(dllFs); - var dllMetadataReader = dllPeReader.GetMetadataReader(); - - foreach (var attrHandle in dllMetadataReader.CustomAttributes) { - var attr = dllMetadataReader.GetCustomAttribute(attrHandle); - try { - /* The cast from EntityHandle to MemberReferenceHandle is overriden, uses private members, and throws - * an InvalidCastException if it fails. We have no other option than to use it and catch the exception. - */ - var constructor = dllMetadataReader.GetMemberReference((MemberReferenceHandle)attr.Constructor); - var attrType = dllMetadataReader.GetTypeReference((TypeReferenceHandle)constructor.Parent); - if (dllMetadataReader.GetString(attrType.Name) == "DafnySourceAttribute") { - var decoded = attr.DecodeValue(new StringOnlyCustomAttributeTypeProvider()); - return (string)decoded.FixedArguments[0].Value; - } - } catch (InvalidCastException) { - // Ignore - the Handle casts are handled as custom explicit operators, - // and there's no way I can see to test if the cases will succeed ahead of time. - } - } - - return null; - } - - // Dummy implementation of ICustomAttributeTypeProvider, providing just enough - // functionality to successfully decode a DafnySourceAttribute value. - private class StringOnlyCustomAttributeTypeProvider : ICustomAttributeTypeProvider { - public System.Type GetPrimitiveType(PrimitiveTypeCode typeCode) { - if (typeCode == PrimitiveTypeCode.String) { - return typeof(string); - } - throw new NotImplementedException(); - } - - public System.Type GetTypeFromDefinition(MetadataReader reader, TypeDefinitionHandle handle, byte rawTypeKind) { - throw new NotImplementedException(); - } - - public System.Type GetTypeFromReference(MetadataReader reader, TypeReferenceHandle handle, byte rawTypeKind) { - throw new NotImplementedException(); - } - - public System.Type GetSZArrayType(System.Type elementType) { - throw new NotImplementedException(); - } - - public System.Type GetSystemType() { - throw new NotImplementedException(); - } - - public System.Type GetTypeFromSerializedName(string name) { - throw new NotImplementedException(); - } - - public PrimitiveTypeCode GetUnderlyingEnumType(System.Type type) { - throw new NotImplementedException(); - } - - public bool IsSystemType(System.Type type) { - throw new NotImplementedException(); - } - } -} \ No newline at end of file diff --git a/Source/DafnyCore/DafnyMain.cs b/Source/DafnyCore/DafnyMain.cs index 3f0f5f98a16..4c268bf590d 100644 --- a/Source/DafnyCore/DafnyMain.cs +++ b/Source/DafnyCore/DafnyMain.cs @@ -10,7 +10,8 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; -using System.Threading; +using System.Reflection.Metadata; +using System.Reflection.PortableExecutable; using System.Threading.Tasks; using DafnyCore; using Microsoft.Boogie; @@ -25,26 +26,195 @@ public IllegalDafnyFile(bool processingError = false) { } } - public class DafnyMain { + public class DafnyFile { + public bool UseStdin { get; private set; } + public string FilePath => Uri.LocalPath; + public string CanonicalPath { get; private set; } + public string BaseName { get; private set; } + public bool IsPreverified { get; set; } + public bool IsPrecompiled { get; set; } + public string SourceFilePath { get; private set; } + public Uri Uri { get; private set; } + + // Returns a canonical string for the given file path, namely one which is the same + // for all paths to a given file and different otherwise. The best we can do is to + // make the path absolute -- detecting case and canonicalizing symbolic and hard + // links are difficult across file systems (which may mount parts of other filesystems, + // with different characteristics) and is not supported by .Net libraries + public static Uri Canonicalize(string filePath) { + if (filePath == null || !filePath.StartsWith("file:")) { + return new Uri(Path.GetFullPath(filePath)); + } + + if (Uri.IsWellFormedUriString(filePath, UriKind.RelativeOrAbsolute)) { + return new Uri(filePath); + } + + var potentialPrefixes = new List() { "file:\\", "file:/", "file:" }; + foreach (var potentialPrefix in potentialPrefixes) { + if (filePath.StartsWith(potentialPrefix)) { + var withoutPrefix = filePath.Substring(potentialPrefix.Length); + var tentativeURI = "file:///" + withoutPrefix.Replace("\\", "/"); + if (Uri.IsWellFormedUriString(tentativeURI, UriKind.RelativeOrAbsolute)) { + return new Uri(tentativeURI); + } + // Recovery mechanisms for the language server + return new Uri(filePath.Substring(potentialPrefix.Length)); + } + } + return new Uri(filePath.Substring("file:".Length)); + } + public static List FileNames(IList dafnyFiles) { + var sourceFiles = new List(); + foreach (DafnyFile f in dafnyFiles) { + sourceFiles.Add(f.FilePath); + } + return sourceFiles; + } + public DafnyFile(DafnyOptions options, string filePath, bool useStdin = false) { + UseStdin = useStdin; + Uri = useStdin ? new Uri("stdin:///") : new Uri(filePath); + BaseName = useStdin ? "" : Path.GetFileName(filePath); + + var extension = useStdin ? ".dfy" : Path.GetExtension(filePath); + if (extension != null) { extension = extension.ToLower(); } + + // Normalizing symbolic links appears to be not + // supported in .Net APIs, because it is very difficult in general + // So we will just use the absolute path, lowercased for all file systems. + // cf. IncludeComparer.CompareTo + CanonicalPath = !useStdin ? Canonicalize(filePath).LocalPath : ""; + filePath = CanonicalPath; + + if (extension == ".dfy" || extension == ".dfyi") { + IsPreverified = false; + IsPrecompiled = false; + SourceFilePath = filePath; + } else if (extension == ".doo") { + IsPreverified = true; + IsPrecompiled = false; + + var dooFile = DooFile.Read(filePath); + + var filePathForErrors = options.UseBaseNameForFileName ? Path.GetFileName(filePath) : filePath; + if (!dooFile.Validate(filePathForErrors, options, options.CurrentCommand)) { + throw new IllegalDafnyFile(true); + } + + // For now it's simpler to let the rest of the pipeline parse the + // program text back into the AST representation. + // At some point we'll likely want to serialize a program + // more efficiently inside a .doo file, at which point + // the DooFile class should encapsulate the serialization logic better + // and expose a Program instead of the program text. + SourceFilePath = Path.GetTempFileName(); + Uri = new Uri(SourceFilePath); + File.WriteAllText(SourceFilePath, dooFile.ProgramText); + + } else if (extension == ".dll") { + IsPreverified = true; + // Technically only for C#, this is for backwards compatability + IsPrecompiled = true; + + var sourceText = GetDafnySourceAttributeText(filePath); + if (sourceText == null) { throw new IllegalDafnyFile(); } + SourceFilePath = Path.GetTempFileName(); + Uri = new Uri(SourceFilePath); + File.WriteAllText(SourceFilePath, sourceText); + + } else { + throw new IllegalDafnyFile(); + } + } + + private static string GetDafnySourceAttributeText(string dllPath) { + if (!File.Exists(dllPath)) { + throw new IllegalDafnyFile(); + } + using var dllFs = new FileStream(dllPath, FileMode.Open, FileAccess.Read, FileShare.ReadWrite); + using var dllPeReader = new PEReader(dllFs); + var dllMetadataReader = dllPeReader.GetMetadataReader(); + + foreach (var attrHandle in dllMetadataReader.CustomAttributes) { + var attr = dllMetadataReader.GetCustomAttribute(attrHandle); + try { + /* The cast from EntityHandle to MemberReferenceHandle is overriden, uses private members, and throws + * an InvalidCastException if it fails. We have no other option than to use it and catch the exception. + */ + var constructor = dllMetadataReader.GetMemberReference((MemberReferenceHandle)attr.Constructor); + var attrType = dllMetadataReader.GetTypeReference((TypeReferenceHandle)constructor.Parent); + if (dllMetadataReader.GetString(attrType.Name) == "DafnySourceAttribute") { + var decoded = attr.DecodeValue(new StringOnlyCustomAttributeTypeProvider()); + return (string)decoded.FixedArguments[0].Value; + } + } catch (InvalidCastException) { + // Ignore - the Handle casts are handled as custom explicit operators, + // and there's no way I can see to test if the cases will succeed ahead of time. + } + } + + return null; + } + + // Dummy implementation of ICustomAttributeTypeProvider, providing just enough + // functionality to successfully decode a DafnySourceAttribute value. + private class StringOnlyCustomAttributeTypeProvider : ICustomAttributeTypeProvider { + public System.Type GetPrimitiveType(PrimitiveTypeCode typeCode) { + if (typeCode == PrimitiveTypeCode.String) { + return typeof(string); + } + throw new NotImplementedException(); + } + + public System.Type GetTypeFromDefinition(MetadataReader reader, TypeDefinitionHandle handle, byte rawTypeKind) { + throw new NotImplementedException(); + } + + public System.Type GetTypeFromReference(MetadataReader reader, TypeReferenceHandle handle, byte rawTypeKind) { + throw new NotImplementedException(); + } + + public System.Type GetSZArrayType(System.Type elementType) { + throw new NotImplementedException(); + } + + public System.Type GetSystemType() { + throw new NotImplementedException(); + } + + public System.Type GetTypeFromSerializedName(string name) { + throw new NotImplementedException(); + } + + public PrimitiveTypeCode GetUnderlyingEnumType(System.Type type) { + throw new NotImplementedException(); + } + + public bool IsSystemType(System.Type type) { + throw new NotImplementedException(); + } + } + } + + public class Main { public static void MaybePrintProgram(Program program, string filename, bool afterResolver) { if (filename == null) { return; } - var tw = filename == "-" ? program.Options.OutputWriter : new StreamWriter(filename); + var tw = filename == "-" ? Console.Out : new StreamWriter(filename); var pr = new Printer(tw, program.Options, program.Options.PrintMode); - pr.PrintProgramLargeStack(program, afterResolver); + pr.PrintProgram(program, afterResolver); } /// /// Returns null on success, or an error string otherwise. /// - public static string ParseCheck(TextReader stdIn, IList /*!*/ files, string /*!*/ programName, - DafnyOptions options, out Program program) + public static string ParseCheck(IList/*!*/ files, string/*!*/ programName, DafnyOptions options, out Program program) //modifies Bpl.options.XmlSink.*; { - string err = Parse(stdIn, files, programName, options, out program); + string err = Parse(files, programName, options, out program); if (err != null) { return err; } @@ -52,14 +222,12 @@ public static string ParseCheck(TextReader stdIn, IList /*!*/ f return Resolve(program); } - public static string Parse(TextReader stdIn, IList files, string programName, DafnyOptions options, - out Program program) { + public static string Parse(IList files, string programName, DafnyOptions options, out Program program) { Contract.Requires(programName != null); Contract.Requires(files != null); program = null; - var defaultModuleDefinition = - new DefaultModuleDefinition(files.Where(f => !f.IsPreverified).Select(f => f.Uri).ToList()); + var defaultModuleDefinition = new DefaultModuleDefinition(files.Where(f => !f.IsPreverified).Select(f => f.Uri).ToList()); ErrorReporter reporter = options.DiagnosticsFormat switch { DafnyOptions.DiagnosticsFormats.PlainText => new ConsoleErrorReporter(options, defaultModuleDefinition), DafnyOptions.DiagnosticsFormats.JSON => new JsonConsoleErrorReporter(options, defaultModuleDefinition), @@ -74,32 +242,26 @@ public static string Parse(TextReader stdIn, IList files, string prog if (options.XmlSink is { IsOpen: true } && !dafnyFile.UseStdin) { options.XmlSink.WriteFileFragment(dafnyFile.FilePath); } - if (options.Trace) { - options.OutputWriter.WriteLine("Parsing " + dafnyFile.FilePath); + Console.WriteLine("Parsing " + dafnyFile.FilePath); } - var include = dafnyFile.IsPrecompiled - ? new Include(new Token() { - Uri = dafnyFile.Uri, - col = 1, - line = 0 - }, null, dafnyFile.SourceFilePath, false) - : null; + var include = dafnyFile.IsPrecompiled ? new Include(new Token() { + Uri = dafnyFile.Uri, + col = 1, + line = 0 + }, null, dafnyFile.SourceFilePath, false) : null; if (include != null) { module.ModuleDef.Includes.Add(include); } - - var err = ParseFile(stdIn, dafnyFile, include, module, builtIns, new Errors(reporter), !dafnyFile.IsPreverified, - !dafnyFile.IsPrecompiled); + var err = ParseFile(dafnyFile, include, module, builtIns, new Errors(reporter), !dafnyFile.IsPreverified, !dafnyFile.IsPrecompiled); if (err != null) { return err; } } if (!(options.DisallowIncludes || options.PrintIncludesMode == DafnyOptions.IncludesModes.Immediate)) { - string errString = ParseIncludesDepthFirstNotCompiledFirst(stdIn, module, builtIns, - files.Select(f => f.SourceFilePath).ToHashSet(), new Errors(reporter)); + string errString = ParseIncludesDepthFirstNotCompiledFirst(module, builtIns, files.Select(f => f.SourceFilePath).ToHashSet(), new Errors(reporter)); if (errString != null) { return errString; } @@ -108,7 +270,7 @@ public static string Parse(TextReader stdIn, IList files, string prog if (options.PrintIncludesMode == DafnyOptions.IncludesModes.Immediate) { DependencyMap dmap = new DependencyMap(); dmap.AddIncludes(module.ModuleDef.Includes); - dmap.PrintMap(options); + dmap.PrintMap(); } program = new Program(programName, module, builtIns, reporter); @@ -118,27 +280,18 @@ public static string Parse(TextReader stdIn, IList files, string prog return null; // success } - private static readonly TaskScheduler largeThreadScheduler = - CustomStackSizePoolTaskScheduler.Create(0x10000000, Environment.ProcessorCount); - - public static readonly TaskFactory LargeStackFactory = new(CancellationToken.None, - TaskCreationOptions.DenyChildAttach, TaskContinuationOptions.None, largeThreadScheduler); - public static string Resolve(Program program) { - if (program.Options.NoResolve || program.Options.NoTypecheck) { - return null; - } + if (program.Options.NoResolve || program.Options.NoTypecheck) { return null; } var r = new Resolver(program); - LargeStackFactory.StartNew(() => r.ResolveProgram(program)).Wait(); + r.ResolveProgram(program); MaybePrintProgram(program, program.Options.DafnyPrintResolvedFile, true); if (program.Reporter.ErrorCountUntilResolver != 0) { - return string.Format("{0} resolution/type errors detected in {1}", program.Reporter.Count(ErrorLevel.Error), - program.Name); + return string.Format("{0} resolution/type errors detected in {1}", program.Reporter.Count(ErrorLevel.Error), program.Name); } - return null; // success + return null; // success } // Lower-case file names before comparing them, since Windows uses case-insensitive file names @@ -148,8 +301,7 @@ public int Compare(Include x, Include y) { } } - public static string ParseIncludesDepthFirstNotCompiledFirst(TextReader stdIn, ModuleDecl module, - BuiltIns builtIns, ISet excludeFiles, Errors errs) { + public static string ParseIncludesDepthFirstNotCompiledFirst(ModuleDecl module, BuiltIns builtIns, ISet excludeFiles, Errors errs) { var includesFound = new SortedSet(new IncludeComparer()); var allIncludes = ((LiteralModuleDecl)module).ModuleDef.Includes; var notCompiledRoots = allIncludes.Where(include => !include.CompileIncludedCode).ToList(); @@ -173,7 +325,7 @@ public static string ParseIncludesDepthFirstNotCompiledFirst(TextReader stdIn, M if (builtIns.Options.PrintIncludesMode != DafnyOptions.IncludesModes.None) { var dependencyMap = new DependencyMap(); dependencyMap.AddIncludes(allIncludes); - dependencyMap.PrintMap(builtIns.Options); + dependencyMap.PrintMap(); } return null; // Success @@ -187,7 +339,6 @@ string TraverseIncludesFrom(int startingIndex) { foreach (var addedItem in addedItems.Reverse()) { stack.Push(addedItem); } - includeIndex = allIncludes.Count; if (stack.Count == 0) { @@ -206,7 +357,7 @@ string TraverseIncludesFrom(int startingIndex) { return ($"Include of file \"{include.IncludedFilename}\" failed."); } - string result = ParseFile(stdIn, file, include, module, builtIns, errs, false, include.CompileIncludedCode); + string result = ParseFile(file, include, module, builtIns, errs, false, include.CompileIncludedCode); if (result != null) { return result; } @@ -216,12 +367,10 @@ string TraverseIncludesFrom(int startingIndex) { } } - private static string ParseFile(TextReader stdIn, DafnyFile dafnyFile, Include include, ModuleDecl module, - BuiltIns builtIns, Errors errs, bool verifyThisFile = true, bool compileThisFile = true) { + private static string ParseFile(DafnyFile dafnyFile, Include include, ModuleDecl module, BuiltIns builtIns, Errors errs, bool verifyThisFile = true, bool compileThisFile = true) { var fn = builtIns.Options.UseBaseNameForFileName ? Path.GetFileName(dafnyFile.FilePath) : dafnyFile.FilePath; try { - int errorCount = Dafny.Parser.Parse(dafnyFile.UseStdin ? stdIn : null, dafnyFile.Uri, module, builtIns, errs, - verifyThisFile, compileThisFile); + int errorCount = Dafny.Parser.Parse(dafnyFile.UseStdin, dafnyFile.Uri, module, builtIns, errs, verifyThisFile, compileThisFile); if (errorCount != 0) { return $"{errorCount} parse errors detected in {fn}"; } @@ -230,7 +379,6 @@ private static string ParseFile(TextReader stdIn, DafnyFile dafnyFile, Include i errs.SemErr(tok, "Unable to open included file"); return $"Error opening file \"{fn}\": {e.Message}"; } - return null; // Success } @@ -252,7 +400,7 @@ to also include a directory containing the `z3` executable. var proverPath = options.ProverOptions.Find(o => o.StartsWith("PROVER_PATH=")); if (proverPath is null && options.Verify) { - options.OutputWriter.WriteLine(z3NotFoundMessage); + Console.WriteLine(z3NotFoundMessage); return (PipelineOutcome.FatalError, new PipelineStatistics()); } @@ -281,11 +429,11 @@ public static string BoogieProgramSuffix(string printFile, string suffix) { public static bool IsBoogieVerified(PipelineOutcome outcome, PipelineStatistics statistics) { return (outcome == PipelineOutcome.Done || outcome == PipelineOutcome.VerificationCompleted) - && statistics.ErrorCount == 0 - && statistics.InconclusiveCount == 0 - && statistics.TimeoutCount == 0 - && statistics.OutOfResourceCount == 0 - && statistics.OutOfMemoryCount == 0; + && statistics.ErrorCount == 0 + && statistics.InconclusiveCount == 0 + && statistics.TimeoutCount == 0 + && statistics.OutOfResourceCount == 0 + && statistics.OutOfMemoryCount == 0; } /// @@ -298,8 +446,8 @@ public static bool IsBoogieVerified(PipelineOutcome outcome, PipelineStatistics /// private static async Task<(PipelineOutcome Outcome, PipelineStatistics Statistics)> BoogiePipelineWithRerun( DafnyOptions options, - TextWriter output, ExecutionEngine engine, Microsoft.Boogie.Program /*!*/ program, string /*!*/ bplFileName, - string programId) { + TextWriter output, ExecutionEngine engine, Microsoft.Boogie.Program/*!*/ program, string/*!*/ bplFileName, + string programId) { Contract.Requires(program != null); Contract.Requires(bplFileName != null); @@ -312,13 +460,12 @@ public static bool IsBoogieVerified(PipelineOutcome outcome, PipelineStatistics case PipelineOutcome.ResolutionError: case PipelineOutcome.TypeCheckingError: engine.PrintBplFile(bplFileName, program, false, false, options.PrettyPrint); - await options.OutputWriter.WriteLineAsync(); - await options.OutputWriter.WriteLineAsync( + Console.WriteLine(); + Console.WriteLine( "*** Encountered internal translation error - re-running Boogie to get better debug information"); - await options.OutputWriter.WriteLineAsync(); + Console.WriteLine(); - var /*!*/ - fileNames = new List { bplFileName }; + var /*!*/ fileNames = new List { bplFileName }; var reparsedProgram = engine.ParseBoogieProgram(fileNames, true); if (reparsedProgram != null) { engine.ResolveAndTypecheck(reparsedProgram, bplFileName, out _); @@ -335,8 +482,7 @@ await options.OutputWriter.WriteLineAsync( return (inferAndVerifyOutcome, stats); default: - Contract.Assert(false); - throw new cce.UnreachableException(); // unexpected outcome + Contract.Assert(false); throw new cce.UnreachableException(); // unexpected outcome } } diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index be262867127..a9c69578d56 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -35,12 +35,10 @@ public enum QuantifierSyntaxOptions { public record Options(IDictionary OptionArguments); public class DafnyOptions : Bpl.CommandLineOptions { - public TextWriter ErrorWriter { get; } - public TextReader Input { get; } - public static readonly DafnyOptions Default = new(TextReader.Null, TextWriter.Null, TextWriter.Null); public IList CliRootUris = new List(); + public static DafnyOptions Default = new DafnyOptions(); public ProjectFile ProjectFile { get; set; } public Command CurrentCommand { get; set; } public bool NonGhostsUseHeap => Allocated == 1 || Allocated == 2; @@ -208,11 +206,10 @@ public static void RegisterLegacyUi(Option option, } private static DafnyOptions defaultImmutableOptions; - public static DafnyOptions DefaultImmutableOptions => defaultImmutableOptions ??= Create(Console.Out, Console.In); + public static DafnyOptions DefaultImmutableOptions => defaultImmutableOptions ??= Create(); - public static DafnyOptions Create(TextWriter outputWriter, TextReader input = null, params string[] arguments) { - input ??= TextReader.Null; - var result = new DafnyOptions(input, outputWriter, outputWriter); + public static DafnyOptions Create(params string[] arguments) { + var result = new DafnyOptions(); result.Parse(arguments); return result; } @@ -232,10 +229,8 @@ public override bool Parse(string[] arguments) { return base.Parse(arguments.Take(i).ToArray()); } - public DafnyOptions(TextReader inputReader, TextWriter outputWriter, TextWriter errorWriter) - : base(outputWriter, "dafny", "Dafny program verifier", new Bpl.ConsolePrinter()) { - Input = inputReader; - ErrorWriter = errorWriter; + public DafnyOptions() + : base("dafny", "Dafny program verifier", new Bpl.ConsolePrinter()) { ErrorTrace = 0; Prune = true; NormalizeNames = true; @@ -403,7 +398,7 @@ private static string[] ParsePluginArguments(string argumentsString) { /// /// Automatic shallow-copy constructor /// - public DafnyOptions(DafnyOptions src) : this(src.Input, src.OutputWriter, src.ErrorWriter) { + public DafnyOptions(DafnyOptions src) : this() { src.CopyTo(this); } @@ -718,7 +713,7 @@ protected bool ParseDafnySpecificOption(string name, Bpl.CommandLineParseState p case "allocated": { ps.GetIntArgument(ref Allocated, 5); if (Allocated != 4) { - Printer.AdvisoryWriteLine(OutputWriter, "The /allocated: option is deprecated"); + Printer.AdvisoryWriteLine(Console.Out, "The /allocated: option is deprecated"); } return true; } @@ -1622,6 +1617,7 @@ Dafny generally accepts Boogie options and passes these on to Boogie. for a similar Boogie program. ".Replace("\n", "\n "); } + } class ErrorReportingCommandLineParseState : Bpl.CommandLineParseState { diff --git a/Source/DafnyCore/Generic/Reporting.cs b/Source/DafnyCore/Generic/Reporting.cs index 6bbea88f725..f6836d5b68a 100644 --- a/Source/DafnyCore/Generic/Reporting.cs +++ b/Source/DafnyCore/Generic/Reporting.cs @@ -189,9 +189,7 @@ public override bool Message(MessageSource source, ErrorLevel level, string erro msg = msg.Replace("\n", "\n "); ConsoleColor previousColor = Console.ForegroundColor; - if (Options.OutputWriter == Console.Out) { - Console.ForegroundColor = ColorForLevel(level); - } + Console.ForegroundColor = ColorForLevel(level); var errorLine = ErrorToString(level, tok, msg); while (tok is NestedToken nestedToken) { tok = nestedToken.Inner; @@ -210,15 +208,13 @@ public override bool Message(MessageSource source, ErrorLevel level, string erro errorLine += "\n" + info; } } - Options.OutputWriter.WriteLine(errorLine); + Console.WriteLine(errorLine); - if (Options.OutputWriter == Console.Out) { - Console.ForegroundColor = previousColor; - } + Console.ForegroundColor = previousColor; return true; + } else { + return false; } - - return false; } public ConsoleErrorReporter(DafnyOptions options, DefaultModuleDefinition outerModule) : base(options, outerModule) { diff --git a/Source/DafnyCore/Generic/Util.cs b/Source/DafnyCore/Generic/Util.cs index c80fa81dd3d..0b995224e7a 100644 --- a/Source/DafnyCore/Generic/Util.cs +++ b/Source/DafnyCore/Generic/Util.cs @@ -483,11 +483,11 @@ public static void PrintFunctionCallGraph(Dafny.Program program) { foreach (var vertex in functionCallGraph.GetVertices()) { var func = vertex.N; - program.Options.OutputWriter.Write("{0},{1}=", func.SanitizedName, func.EnclosingClass.EnclosingModuleDefinition.SanitizedName); + Console.Write("{0},{1}=", func.SanitizedName, func.EnclosingClass.EnclosingModuleDefinition.SanitizedName); foreach (var callee in vertex.Successors) { - program.Options.OutputWriter.Write("{0} ", callee.N.SanitizedName); + Console.Write("{0} ", callee.N.SanitizedName); } - program.Options.OutputWriter.Write("\n"); + Console.Write("\n"); } } @@ -581,9 +581,9 @@ public static void PrintStats(Dafny.Program program) { } // Print out the results, with some nice formatting - program.Options.OutputWriter.WriteLine(""); - program.Options.OutputWriter.WriteLine("Statistics"); - program.Options.OutputWriter.WriteLine("----------"); + Console.WriteLine(""); + Console.WriteLine("Statistics"); + Console.WriteLine("----------"); int max_key_length = 0; foreach (var key in stats.Keys) { @@ -594,7 +594,7 @@ public static void PrintStats(Dafny.Program program) { foreach (var keypair in stats) { string keyString = keypair.Key.PadRight(max_key_length + 2); - program.Options.OutputWriter.WriteLine("{0} {1,4}", keyString, keypair.Value); + Console.WriteLine("{0} {1,4}", keyString, keypair.Value); } } } @@ -625,20 +625,20 @@ public void AddIncludes(IEnumerable includes) { } } - public void PrintMap(DafnyOptions options) { + public void PrintMap() { SortedSet leaves = new SortedSet(); // Files that don't themselves include any files foreach (string target in dependencies.Keys) { - options.OutputWriter.Write(target); + System.Console.Write(target); foreach (string dependency in dependencies[target]) { - options.OutputWriter.Write(";" + dependency); + System.Console.Write(";" + dependency); if (!dependencies.ContainsKey(dependency)) { leaves.Add(dependency); } } - options.OutputWriter.WriteLine(); + System.Console.WriteLine(); } foreach (string leaf in leaves) { - options.OutputWriter.WriteLine(leaf); + System.Console.WriteLine(leaf); } } } diff --git a/Source/DafnyCore/JsonDiagnostics.cs b/Source/DafnyCore/JsonDiagnostics.cs index b3bedcffc41..73d553c4617 100644 --- a/Source/DafnyCore/JsonDiagnostics.cs +++ b/Source/DafnyCore/JsonDiagnostics.cs @@ -109,9 +109,9 @@ public DafnyJsonConsolePrinter(DafnyOptions options) : base(options) { } public class JsonConsoleErrorReporter : BatchErrorReporter { - public override bool Message(MessageSource source, ErrorLevel level, string errorID, Dafny.IToken tok, string msg) { - if (base.Message(source, level, errorID, tok, msg) && (Options is { PrintTooltips: true } || level != ErrorLevel.Info)) { - new DiagnosticMessageData(source, level, tok, null, msg, null).WriteJsonTo(Options.OutputWriter); + public override bool Message(MessageSource source, ErrorLevel level, string errorId, Dafny.IToken tok, string msg) { + if (base.Message(source, level, errorId, tok, msg) && (Options is { PrintTooltips: true } || level != ErrorLevel.Info)) { + new DiagnosticMessageData(source, level, tok, null, msg, null).WriteJsonTo(Console.Out); return true; } diff --git a/Source/DafnyCore/Plugins/IExecutableBackend.cs b/Source/DafnyCore/Plugins/IExecutableBackend.cs index 23f5316554a..bb9652fe09f 100644 --- a/Source/DafnyCore/Plugins/IExecutableBackend.cs +++ b/Source/DafnyCore/Plugins/IExecutableBackend.cs @@ -156,8 +156,6 @@ public abstract bool CompileTargetProgram(string dafnyProgramName, string target /// /// Returns true on success, false on error. Any errors are output to outputWriter. /// - public abstract bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, - string pathsFilename, - ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter, - TextWriter errorWriter); + public abstract bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, string pathsFilename, + ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter); } diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs index 333b9ff173c..8a5b73fe956 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs @@ -224,18 +224,18 @@ void PrintTypeConstraintState(int lbl) { if (!Options.Get(CommonOptionBag.TypeInferenceDebug)) { return; } - Options.OutputWriter.WriteLine("DEBUG: ---------- type constraints ---------- {0} {1}", lbl, lbl == 0 && currentMethod != null ? currentMethod.Name : ""); + Console.WriteLine("DEBUG: ---------- type constraints ---------- {0} {1}", lbl, lbl == 0 && currentMethod != null ? currentMethod.Name : ""); foreach (var constraint in AllTypeConstraints) { var super = constraint.Super.Normalize(); var sub = constraint.Sub.Normalize(); - Options.OutputWriter.WriteLine(" {0} :> {1}", super is IntVarietiesSupertype ? "int-like" : super is RealVarietiesSupertype ? "real-like" : super.ToString(), sub); + Console.WriteLine(" {0} :> {1}", super is IntVarietiesSupertype ? "int-like" : super is RealVarietiesSupertype ? "real-like" : super.ToString(), sub); } foreach (var xc in AllXConstraints) { - Options.OutputWriter.WriteLine(" {0}", xc); + Console.WriteLine(" {0}", xc); } - Options.OutputWriter.WriteLine(); + Console.WriteLine(); if (lbl % 2 == 1) { - Options.OutputWriter.WriteLine("DEBUG: --------------------------------------"); + Console.WriteLine("DEBUG: --------------------------------------"); } } @@ -1226,14 +1226,14 @@ private void ConstrainSubtypeRelation_Equal(Type a, Type b, TypeConstraint.Error var proxy = a.Normalize() as TypeProxy; if (proxy != null && proxy.T == null && !Reaches(b, proxy, 1, new HashSet())) { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine("DEBUG: (invariance) assigning proxy {0}.T := {1}", proxy, b); + Console.WriteLine("DEBUG: (invariance) assigning proxy {0}.T := {1}", proxy, b); } proxy.T = b; } proxy = b.Normalize() as TypeProxy; if (proxy != null && proxy.T == null && !Reaches(a, proxy, 1, new HashSet())) { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine("DEBUG: (invariance) assigning proxy {0}.T := {1}", proxy, a); + Console.WriteLine("DEBUG: (invariance) assigning proxy {0}.T := {1}", proxy, a); } proxy.T = a; } @@ -1452,7 +1452,7 @@ private bool AssignProxyAndHandleItsConstraints_aux(TypeProxy proxy, Type t, boo if (t != t.NormalizeExpand()) { // force the type to be a base type if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine("DEBUG: hijacking {0}.T := {1} to instead assign {2}", proxy, t, t.NormalizeExpand()); + Console.WriteLine("DEBUG: hijacking {0}.T := {1} to instead assign {2}", proxy, t, t.NormalizeExpand()); } t = t.NormalizeExpand(); followedRequestedAssignment = false; @@ -1460,7 +1460,7 @@ private bool AssignProxyAndHandleItsConstraints_aux(TypeProxy proxy, Type t, boo } else { // hijack the setting of proxy; to do that, we decide on a particular int variety now if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine("DEBUG: hijacking {0}.T := {1} to instead assign {2}", proxy, t, Type.Int); + Console.WriteLine("DEBUG: hijacking {0}.T := {1} to instead assign {2}", proxy, t, Type.Int); } t = Type.Int; followedRequestedAssignment = false; @@ -1473,7 +1473,7 @@ private bool AssignProxyAndHandleItsConstraints_aux(TypeProxy proxy, Type t, boo if (t != t.NormalizeExpand()) { // force the type to be a base type if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine("DEBUG: hijacking {0}.T := {1} to instead assign {2}", proxy, t, t.NormalizeExpand()); + Console.WriteLine("DEBUG: hijacking {0}.T := {1} to instead assign {2}", proxy, t, t.NormalizeExpand()); } t = t.NormalizeExpand(); followedRequestedAssignment = false; @@ -1481,7 +1481,7 @@ private bool AssignProxyAndHandleItsConstraints_aux(TypeProxy proxy, Type t, boo } else { // hijack the setting of proxy; to do that, we decide on a particular real variety now if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine("DEBUG: hijacking {0}.T := {1} to instead assign {2}", proxy, t, Type.Real); + Console.WriteLine("DEBUG: hijacking {0}.T := {1} to instead assign {2}", proxy, t, Type.Real); } t = Type.Real; followedRequestedAssignment = false; @@ -1491,7 +1491,7 @@ private bool AssignProxyAndHandleItsConstraints_aux(TypeProxy proxy, Type t, boo } // set proxy.T right away, so that we can freely recurse without having to worry about infinite recursion if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine("DEBUG: setting proxy {0}.T := {1}", proxy, t); + Console.WriteLine("DEBUG: setting proxy {0}.T := {1}", proxy, t); } proxy.T = t; @@ -2276,11 +2276,11 @@ Type FindCollectionType(DafnyOptions options, Type t, bool towardsSub, ISet rhss) { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { Console.Write("DEBUG: ProcessAssignable: {0} with rhss:", lhs); foreach (var rhs in rhss) { - Options.OutputWriter.Write(" {0}", rhs); + Console.Write(" {0}", rhs); } - Options.OutputWriter.Write(" subtypes:"); + Console.Write(" subtypes:"); foreach (var sub in lhs.SubtypesKeepConstraints) { - Options.OutputWriter.Write(" {0}", sub); + Console.Write(" {0}", sub); } - Options.OutputWriter.WriteLine(); + Console.WriteLine(); } Type join = null; foreach (var rhs in rhss) { @@ -2762,7 +2762,7 @@ private bool ProcessAssignable(TypeProxy lhs, List rhss) { return false; } else { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine("DEBUG: ProcessAssignable: assigning proxy {0}.T := {1}", lhs, join); + Console.WriteLine("DEBUG: ProcessAssignable: assigning proxy {0}.T := {1}", lhs, join); } lhs.T = join; return true; @@ -3042,7 +3042,7 @@ bool AssignKnownEndsFullstrength_SubDirection(TypeProxy proxy) { CloseOverAssignableRhss(proxySubs); if (HasApplicableNullableRefTypeConstraint(proxySubs)) { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine("DEBUG: Found join {0} for proxy {1}, but weakening it to {2}", joins[0], proxy, joins[0].NormalizeExpand()); + Console.WriteLine("DEBUG: Found join {0} for proxy {1}, but weakening it to {2}", joins[0], proxy, joins[0].NormalizeExpand()); } AssignProxyAndHandleItsConstraints(proxy, joins[0].NormalizeExpand(), true); return true; @@ -5169,14 +5169,14 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me var r = GetBaseTypeFromProxy((TypeProxy)t, new Dictionary()); if (r != null) { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine(" ----> found improvement through GetBaseTypeFromProxy: {0}", r); + Console.WriteLine(" ----> found improvement through GetBaseTypeFromProxy: {0}", r); } return r; } } if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine(" ----> found no improvement, giving up"); + Console.WriteLine(" ----> found no improvement, giving up"); } return t; } @@ -5189,7 +5189,7 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me return t; // simplification did the trick } if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine("DEBUG: Member selection{3}: {1} :> {0} :> {2}", t, + Console.WriteLine("DEBUG: Member selection{3}: {1} :> {0} :> {2}", t, Util.Comma(proxy.SupertypesKeepConstraints, su => su.ToString()), Util.Comma(proxy.SubtypesKeepConstraints, su => su.ToString()), memberName == null ? "" : " (" + memberName + ")"); @@ -5201,14 +5201,14 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me DetermineRootLeaf(joinType, out _, out _, out var headIsRoot, out _); if (joinType.IsDatatype) { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine(" ----> join is a datatype: {0}", joinType); + Console.WriteLine(" ----> join is a datatype: {0}", joinType); } ConstrainSubtypeRelation(t, joinType, tok, "Member selection requires a supertype of {0} (got something more like {1})", t, joinType); return joinType; } else if (headIsRoot) { // we're good to go -- by picking "join" (whose type parameters have been replaced by fresh proxies), we're not losing any generality if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine(" ----> improved to {0} through join", joinType); + Console.WriteLine(" ----> improved to {0} through join", joinType); } AssignProxyAndHandleItsConstraints(proxy, joinType, true); return proxy.NormalizeExpand(); // we return proxy.T instead of join, in case the assignment gets hijacked @@ -5217,7 +5217,7 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me if (generalArrowType != null) { // pick the supertype "generalArrowType" of "join" if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine(" ----> improved to {0} through join and function application", generalArrowType); + Console.WriteLine(" ----> improved to {0} through join and function application", generalArrowType); } ConstrainSubtypeRelation(generalArrowType, t, tok, "Function application requires a subtype of {0} (got something more like {1})", generalArrowType, t); return generalArrowType; @@ -5236,7 +5236,7 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me var mbr = plausibleMembers.First(); if (mbr.EnclosingClass == cl) { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine(" ----> improved to {0} through member-selection join", joinType); + Console.WriteLine(" ----> improved to {0} through member-selection join", joinType); } var joinRoot = joinType.NormalizeExpand(); // blow passed any constraints ConstrainSubtypeRelation(joinRoot, t, tok, "Member selection requires a subtype of {0} (got something more like {1})", joinRoot, t); @@ -5259,7 +5259,7 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me proxyTypeArgs = proxyTypeArgs.ConvertAll(t0 => t0.AsTypeParameter == null ? t0 : (Type)new InferredTypeProxy()); var pickItFromHere = new UserDefinedType(tok, mbr.EnclosingClass.Name, mbr.EnclosingClass, proxyTypeArgs); if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine(" ----> improved to {0} through join and member lookup", pickItFromHere); + Console.WriteLine(" ----> improved to {0} through join and member lookup", pickItFromHere); } ConstrainSubtypeRelation(pickItFromHere, t, tok, "Member selection requires a subtype of {0} (got something more like {1})", pickItFromHere, t); return pickItFromHere; @@ -5270,7 +5270,7 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me } } if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine(" ----> found no improvement, because join does not determine type enough"); + Console.WriteLine(" ----> found no improvement, because join does not determine type enough"); } } @@ -5285,12 +5285,12 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me if (proxy == meet.Normalize()) { // can this really ever happen? if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine(" ----> found no improvement (other than the proxy itself)"); + Console.WriteLine(" ----> found no improvement (other than the proxy itself)"); } return t; } else { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine(" ----> (merging, then trying to improve further) assigning proxy {0}.T := {1}", proxy, meet); + Console.WriteLine(" ----> (merging, then trying to improve further) assigning proxy {0}.T := {1}", proxy, meet); } Contract.Assert(proxy != meet); proxy.T = meet; @@ -5300,7 +5300,7 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me } if (!(meet is ArtificialType)) { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine(" ----> improved to {0} through meet", meet); + Console.WriteLine(" ----> improved to {0} through meet", meet); } if (memberName != null) { AssignProxyAndHandleItsConstraints(proxy, meet, true); @@ -5315,14 +5315,14 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me var artificialSuper = proxy.InClusterOfArtificial(AllXConstraints); if (artificialSuper != null) { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine(" ----> use artificial supertype: {0}", artificialSuper); + Console.WriteLine(" ----> use artificial supertype: {0}", artificialSuper); } return artificialSuper; } // we weren't able to do it if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine(" ----> found no improvement using simple things, trying harder once more"); + Console.WriteLine(" ----> found no improvement using simple things, trying harder once more"); } return PartiallyResolveTypeForMemberSelection(tok, t, memberName, strength + 1); } @@ -5418,7 +5418,7 @@ private void GetRelatedTypeProxies(Type t, ISet proxies) { return; } if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Options.OutputWriter.WriteLine("DEBUG: GetRelatedTypeProxies: finding {0} interesting", proxy); + Console.WriteLine("DEBUG: GetRelatedTypeProxies: finding {0} interesting", proxy); } proxies.Add(proxy); // close over interesting constraints diff --git a/Source/DafnyCore/Resolver/Resolver.cs b/Source/DafnyCore/Resolver/Resolver.cs index 7049daa9f6c..610ff2e90b6 100644 --- a/Source/DafnyCore/Resolver/Resolver.cs +++ b/Source/DafnyCore/Resolver/Resolver.cs @@ -52,7 +52,7 @@ private bool VisibleInScope(Declaration d) { return useCompileSignatures || d.IsVisibleInScope(moduleInfo.VisibilityScope); } - public FreshIdGenerator defaultTempVarIdGenerator = new FreshIdGenerator(); + public static FreshIdGenerator defaultTempVarIdGenerator = new FreshIdGenerator(); public string FreshTempVarName(string prefix, ICodeContext context) { var gen = context is Declaration decl ? decl.IdGenerator : defaultTempVarIdGenerator; @@ -448,7 +448,7 @@ public void ResolveProgram(Program prog) { rewriters.Add(new TimeLimitRewriter(reporter)); rewriters.Add(new ForallStmtRewriter(reporter)); rewriters.Add(new ProvideRevealAllRewriter(this.reporter)); - rewriters.Add(new MatchFlattener(this.reporter, defaultTempVarIdGenerator)); + rewriters.Add(new MatchFlattener(this.reporter, Resolver.defaultTempVarIdGenerator)); if (Options.AutoTriggers) { rewriters.Add(new QuantifierSplittingRewriter(reporter)); @@ -1192,7 +1192,7 @@ private void CheckModuleExportConsistency(ModuleDefinition m) { Cloner cloner = new ScopeCloner(scope); var exportView = cloner.CloneModuleDefinition(m, m.NameNode); if (Options.DafnyPrintExportedViews.Contains(exportDecl.FullName)) { - var wr = Options.OutputWriter; + var wr = Console.Out; wr.WriteLine("/* ===== export set {0}", exportDecl.FullName); var pr = new Printer(wr, Options); pr.PrintTopLevelDecls(exportView.TopLevelDecls, 0, null, null); diff --git a/Source/DafnyCore/Resolver/TypeConstraint.cs b/Source/DafnyCore/Resolver/TypeConstraint.cs index ada2c42af72..06eb2de36f7 100644 --- a/Source/DafnyCore/Resolver/TypeConstraint.cs +++ b/Source/DafnyCore/Resolver/TypeConstraint.cs @@ -29,7 +29,7 @@ public abstract class ErrorMsg { bool reported; public void FlagAsError(Resolver resolver) { if (resolver.Options.Get(CommonOptionBag.TypeInferenceDebug)) { - resolver.Options.OutputWriter.WriteLine($"DEBUG: flagging error: {ApproximateErrorMessage()}"); + Console.WriteLine($"DEBUG: flagging error: {ApproximateErrorMessage()}"); } resolver.TypeConstraintErrorsToBeReported.Add(this); } diff --git a/Source/DafnyCore/Rewriters/ForallStmtRewriter.cs b/Source/DafnyCore/Rewriters/ForallStmtRewriter.cs index de5e0203865..85a88402782 100644 --- a/Source/DafnyCore/Rewriters/ForallStmtRewriter.cs +++ b/Source/DafnyCore/Rewriters/ForallStmtRewriter.cs @@ -84,14 +84,14 @@ protected override bool VisitOneStmt(Statement stmt, ref bool st) { var range = Expression.CreateAnd(Resolver.GetImpliedTypeConstraint(i, i.Type), s.Range); var vals = InvertExpression(i, j, range, Fi); #if DEBUG_PRINT - resolve.Options.Writer.WriteLine("DEBUG: Trying to invert:"); - resolve.Options.Writer.WriteLine("DEBUG: " + Printer.ExprToString(s.Range) + " && " + j.Name + " == " + Printer.ExprToString(Fi)); + Console.WriteLine("DEBUG: Trying to invert:"); + Console.WriteLine("DEBUG: " + Printer.ExprToString(s.Range) + " && " + j.Name + " == " + Printer.ExprToString(Fi)); if (vals == null) { - resolve.Options.Writer.WriteLine("DEBUG: Can't"); + Console.WriteLine("DEBUG: Can't"); } else { - resolve.Options.Writer.WriteLine("DEBUG: The inverse is the disjunction of the following:"); + Console.WriteLine("DEBUG: The inverse is the disjunction of the following:"); foreach (var val in vals) { - resolve.Options.Writer.WriteLine("DEBUG: " + Printer.ExprToString(val.Range) + " && " + Printer.ExprToString(val.FInverse) + " == " + i.Name); + Console.WriteLine("DEBUG: " + Printer.ExprToString(val.Range) + " && " + Printer.ExprToString(val.FInverse) + " == " + i.Name); } } #endif diff --git a/Source/DafnyCore/Rewriters/IRewriter.cs b/Source/DafnyCore/Rewriters/IRewriter.cs index c919686f4bd..527bba5cec9 100644 --- a/Source/DafnyCore/Rewriters/IRewriter.cs +++ b/Source/DafnyCore/Rewriters/IRewriter.cs @@ -13,22 +13,6 @@ public abstract class IRewriter { /// protected ErrorReporter Reporter; - protected DafnyOptions Options => Reporter.Options; - - /// - /// Constructor that accepts an ErrorReporter - /// You can obtain an ErrorReporter two following ways: - /// * Extend a PluginConfiguration class, and override the method GetRewriters(), whose first argument is an ErrorReporter - /// * Have no PluginConfiguration class, and an ErrorReporter will be provided to your class's constructor. - /// - /// Then you can use the protected field "reporter" like the following: - /// - /// reporter.Error(MessageSource.Compiler, token, "[Your plugin] Your error message here"); - /// - /// The token is usually obtained on expressions and statements in the field `tok` - /// If you do not have access to them, use moduleDefinition.GetFirstTopLevelToken() - /// - /// The error reporter. Usually outputs automatically to IDE or command-line protected internal IRewriter(ErrorReporter reporter) { Contract.Requires(reporter != null); this.Reporter = reporter; diff --git a/Source/DafnyCore/Triggers/TriggerUtils.cs b/Source/DafnyCore/Triggers/TriggerUtils.cs index e168888bbb9..6f0c6f21c2c 100644 --- a/Source/DafnyCore/Triggers/TriggerUtils.cs +++ b/Source/DafnyCore/Triggers/TriggerUtils.cs @@ -188,8 +188,8 @@ internal string JoinStringsWithHeader(string header, IEnumerable lines) } [Conditional("DEBUG_AUTO_TRIGGERS")] - internal static void DebugTriggers(DafnyOptions options, string format, params object[] more) { - options.ErrorWriter.WriteLine(format, more); + internal static void DebugTriggers(string format, params object[] more) { + Console.Error.WriteLine(format, more); } internal static bool AllowsMatchingLoops(ComprehensionExpr quantifier) { diff --git a/Source/DafnyCore/Triggers/TriggersCollector.cs b/Source/DafnyCore/Triggers/TriggersCollector.cs index ac636e66c04..592024e7d30 100644 --- a/Source/DafnyCore/Triggers/TriggersCollector.cs +++ b/Source/DafnyCore/Triggers/TriggersCollector.cs @@ -234,7 +234,7 @@ expr is MultiSetFormingExpr || } } - TriggerUtils.DebugTriggers(options, "{0} ({1})\n{2}", Printer.ExprToString(options, expr), expr.GetType(), annotation); + TriggerUtils.DebugTriggers("{0} ({1})\n{2}", Printer.ExprToString(options, expr), expr.GetType(), annotation); cache.annotations[expr] = annotation; return annotation; } diff --git a/Source/DafnyCore/UndisposableTextWriter.cs b/Source/DafnyCore/UndisposableTextWriter.cs deleted file mode 100644 index 23d0c297b74..00000000000 --- a/Source/DafnyCore/UndisposableTextWriter.cs +++ /dev/null @@ -1,247 +0,0 @@ -using System; -using System.IO; -using System.Text; -using System.Threading; -using System.Threading.Tasks; - -namespace Microsoft.Dafny; - -public class UndisposableTextWriter : TextWriter { - public UndisposableTextWriter(TextWriter textWriterImplementation) { - this.textWriterImplementation = textWriterImplementation; - } - - public override void Close() { - textWriterImplementation.Close(); - } - - protected override void Dispose(bool disposing) { - WriteLine("Tried to Dispose the writer at: " + new Exception().StackTrace); - } - - public override ValueTask DisposeAsync() { - WriteLine("Tried to DisposeAsync the writer at: " + new Exception().StackTrace); - return ValueTask.CompletedTask; - } - - public override void Flush() { - textWriterImplementation.Flush(); - } - - public override Task FlushAsync() { - return textWriterImplementation.FlushAsync(); - } - - public override void Write(bool value) { - textWriterImplementation.Write(value); - } - - public override void Write(char value) { - textWriterImplementation.Write(value); - } - - public override void Write(char[] buffer) { - textWriterImplementation.Write(buffer); - } - - public override void Write(char[] buffer, int index, int count) { - textWriterImplementation.Write(buffer, index, count); - } - - public override void Write(decimal value) { - textWriterImplementation.Write(value); - } - - public override void Write(double value) { - textWriterImplementation.Write(value); - } - - public override void Write(int value) { - textWriterImplementation.Write(value); - } - - public override void Write(long value) { - textWriterImplementation.Write(value); - } - - public override void Write(object value) { - textWriterImplementation.Write(value); - } - - public override void Write(ReadOnlySpan buffer) { - textWriterImplementation.Write(buffer); - } - - public override void Write(float value) { - textWriterImplementation.Write(value); - } - - public override void Write(string value) { - textWriterImplementation.Write(value); - } - - public override void Write(string format, object arg0) { - textWriterImplementation.Write(format, arg0); - } - - public override void Write(string format, object arg0, object arg1) { - textWriterImplementation.Write(format, arg0, arg1); - } - - public override void Write(string format, object arg0, object arg1, object arg2) { - textWriterImplementation.Write(format, arg0, arg1, arg2); - } - - public override void Write(string format, params object[] arg) { - textWriterImplementation.Write(format, arg); - } - - public override void Write(StringBuilder value) { - textWriterImplementation.Write(value); - } - - public override void Write(uint value) { - textWriterImplementation.Write(value); - } - - public override void Write(ulong value) { - textWriterImplementation.Write(value); - } - - public override Task WriteAsync(char value) { - return textWriterImplementation.WriteAsync(value); - } - - public override Task WriteAsync(char[] buffer, int index, int count) { - return textWriterImplementation.WriteAsync(buffer, index, count); - } - - public override Task WriteAsync(ReadOnlyMemory buffer, CancellationToken cancellationToken = new CancellationToken()) { - return textWriterImplementation.WriteAsync(buffer, cancellationToken); - } - - public override Task WriteAsync(string value) { - return textWriterImplementation.WriteAsync(value); - } - - public override Task WriteAsync(StringBuilder value, CancellationToken cancellationToken = new CancellationToken()) { - return textWriterImplementation.WriteAsync(value, cancellationToken); - } - - public override void WriteLine() { - textWriterImplementation.WriteLine(); - } - - public override void WriteLine(bool value) { - textWriterImplementation.WriteLine(value); - } - - public override void WriteLine(char value) { - textWriterImplementation.WriteLine(value); - } - - public override void WriteLine(char[] buffer) { - textWriterImplementation.WriteLine(buffer); - } - - public override void WriteLine(char[] buffer, int index, int count) { - textWriterImplementation.WriteLine(buffer, index, count); - } - - public override void WriteLine(decimal value) { - textWriterImplementation.WriteLine(value); - } - - public override void WriteLine(double value) { - textWriterImplementation.WriteLine(value); - } - - public override void WriteLine(int value) { - textWriterImplementation.WriteLine(value); - } - - public override void WriteLine(long value) { - textWriterImplementation.WriteLine(value); - } - - public override void WriteLine(object value) { - textWriterImplementation.WriteLine(value); - } - - public override void WriteLine(ReadOnlySpan buffer) { - textWriterImplementation.WriteLine(buffer); - } - - public override void WriteLine(float value) { - textWriterImplementation.WriteLine(value); - } - - public override void WriteLine(string value) { - textWriterImplementation.WriteLine(value); - } - - public override void WriteLine(string format, object arg0) { - textWriterImplementation.WriteLine(format, arg0); - } - - public override void WriteLine(string format, object arg0, object arg1) { - textWriterImplementation.WriteLine(format, arg0, arg1); - } - - public override void WriteLine(string format, object arg0, object arg1, object arg2) { - textWriterImplementation.WriteLine(format, arg0, arg1, arg2); - } - - public override void WriteLine(string format, params object[] arg) { - textWriterImplementation.WriteLine(format, arg); - } - - public override void WriteLine(StringBuilder value) { - textWriterImplementation.WriteLine(value); - } - - public override void WriteLine(uint value) { - textWriterImplementation.WriteLine(value); - } - - public override void WriteLine(ulong value) { - textWriterImplementation.WriteLine(value); - } - - public override Task WriteLineAsync() { - return textWriterImplementation.WriteLineAsync(); - } - - public override Task WriteLineAsync(char value) { - return textWriterImplementation.WriteLineAsync(value); - } - - public override Task WriteLineAsync(char[] buffer, int index, int count) { - return textWriterImplementation.WriteLineAsync(buffer, index, count); - } - - public override Task WriteLineAsync(ReadOnlyMemory buffer, CancellationToken cancellationToken = new CancellationToken()) { - return textWriterImplementation.WriteLineAsync(buffer, cancellationToken); - } - - public override Task WriteLineAsync(string value) { - return textWriterImplementation.WriteLineAsync(value); - } - - public override Task WriteLineAsync(StringBuilder value, CancellationToken cancellationToken = new CancellationToken()) { - return textWriterImplementation.WriteLineAsync(value, cancellationToken); - } - - public override IFormatProvider FormatProvider => textWriterImplementation.FormatProvider; - - public override string NewLine { - get => textWriterImplementation.NewLine; - set => textWriterImplementation.NewLine = value; - } - - private TextWriter textWriterImplementation; - public override Encoding Encoding => textWriterImplementation.Encoding; - - - -} \ No newline at end of file diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs index 11e8c05b1d3..27abffcc08a 100644 --- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs +++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs @@ -906,7 +906,7 @@ private void AddFunctionOverrideCheckImpl(Function f) { var name = MethodName(f, MethodTranslationKind.OverrideCheck); var proc = new Boogie.Procedure(f.tok, name, new List(), Util.Concat(Util.Concat(typeInParams, inParams_Heap), inParams), outParams, - false, req, mod, ens, etran.TrAttributes(f.Attributes, null)); + req, mod, ens, etran.TrAttributes(f.Attributes, null)); AddVerboseName(proc, f.FullDafnyName, MethodTranslationKind.OverrideCheck); sink.AddTopLevelDeclaration(proc); var implInParams = Boogie.Formal.StripWhereClauses(inParams); @@ -1545,7 +1545,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { } var name = MethodName(m, kind); - var proc = new Boogie.Procedure(m.tok, name, new List(), inParams, outParams, false, req, mod, ens, etran.TrAttributes(m.Attributes, null)); + var proc = new Boogie.Procedure(m.tok, name, new List(), inParams, outParams, req, mod, ens, etran.TrAttributes(m.Attributes, null)); AddVerboseName(proc, m.FullDafnyName, kind); if (InsertChecksums) { diff --git a/Source/DafnyCore/Verifier/Translator.TrStatement.cs b/Source/DafnyCore/Verifier/Translator.TrStatement.cs index 4060cb34757..c4b724eeb14 100644 --- a/Source/DafnyCore/Verifier/Translator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/Translator.TrStatement.cs @@ -1577,7 +1577,7 @@ void TrLoop(LoopStmt s, Expression Guard, BodyTranslator/*?*/ bodyTr, } Bpl.StmtList body = loopBodyBuilder.Collect(s.Tok); - builder.Add(new Bpl.WhileCmd(s.Tok, Bpl.Expr.True, invariants, new List(), body)); + builder.Add(new Bpl.WhileCmd(s.Tok, Bpl.Expr.True, invariants, body)); } void InsertContinueTarget(LoopStmt loop, BoogieStmtListBuilder builder) { diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 70edf03a82a..eed2d64e6fe 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -434,7 +434,7 @@ public PredefinedDecls(Bpl.TypeCtorDecl charType, Bpl.TypeCtorDecl refType, Bpl. PredefinedDecls FindPredefinedDecls(Bpl.Program prog) { Contract.Requires(prog != null); if (prog.Resolve(options) != 0) { - options.OutputWriter.WriteLine("Error: resolution errors encountered in Dafny prelude"); + Console.WriteLine("Error: resolution errors encountered in Dafny prelude"); return null; } @@ -577,85 +577,85 @@ PredefinedDecls FindPredefinedDecls(Bpl.Program prog) { } } if (seqTypeCtor == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type Seq"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type Seq"); } else if (setTypeCtor == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type Set"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type Set"); } else if (isetTypeCtor == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type ISet"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type ISet"); } else if (multiSetTypeCtor == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type MultiSet"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type MultiSet"); } else if (mapTypeCtor == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type Map"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type Map"); } else if (imapTypeCtor == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type IMap"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type IMap"); } else if (arrayLength == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function _System.array.Length"); + Console.WriteLine("Error: Dafny prelude is missing declaration of function _System.array.Length"); } else if (realFloor == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function _System.real.Floor"); + Console.WriteLine("Error: Dafny prelude is missing declaration of function _System.real.Floor"); } else if (ORDINAL_isLimit == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function ORD#IsLimit"); + Console.WriteLine("Error: Dafny prelude is missing declaration of function ORD#IsLimit"); } else if (ORDINAL_isSucc == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function ORD#IsSucc"); + Console.WriteLine("Error: Dafny prelude is missing declaration of function ORD#IsSucc"); } else if (ORDINAL_offset == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function ORD#Offset"); + Console.WriteLine("Error: Dafny prelude is missing declaration of function ORD#Offset"); } else if (ORDINAL_isNat == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function ORD#IsNat"); + Console.WriteLine("Error: Dafny prelude is missing declaration of function ORD#IsNat"); } else if (mapDomain == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function Map#Domain"); + Console.WriteLine("Error: Dafny prelude is missing declaration of function Map#Domain"); } else if (imapDomain == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function IMap#Domain"); + Console.WriteLine("Error: Dafny prelude is missing declaration of function IMap#Domain"); } else if (mapValues == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function Map#Values"); + Console.WriteLine("Error: Dafny prelude is missing declaration of function Map#Values"); } else if (imapValues == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function IMap#Values"); + Console.WriteLine("Error: Dafny prelude is missing declaration of function IMap#Values"); } else if (mapItems == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function Map#Items"); + Console.WriteLine("Error: Dafny prelude is missing declaration of function Map#Items"); } else if (imapItems == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function IMap#Items"); + Console.WriteLine("Error: Dafny prelude is missing declaration of function IMap#Items"); } else if (tuple2Destructors0 == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function _System.Tuple2._0"); + Console.WriteLine("Error: Dafny prelude is missing declaration of function _System.Tuple2._0"); } else if (tuple2Destructors1 == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function _System.Tuple2._1"); + Console.WriteLine("Error: Dafny prelude is missing declaration of function _System.Tuple2._1"); } else if (tuple2Constructor == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function #_System._tuple#2._#Make2"); + Console.WriteLine("Error: Dafny prelude is missing declaration of function #_System._tuple#2._#Make2"); } else if (bv0TypeDecl == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type Bv0"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type Bv0"); } else if (fieldNameType == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type Field"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type Field"); } else if (classNameType == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type ClassName"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type ClassName"); } else if (tyType == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type Ty"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type Ty"); } else if (tyTagType == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type TyTag"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type TyTag"); } else if (tyTagFamilyType == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type TyTagFamily"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type TyTagFamily"); } else if (nameFamilyType == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type NameFamily"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type NameFamily"); } else if (datatypeType == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type DatatypeType"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type DatatypeType"); } else if (handleType == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type HandleType"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type HandleType"); } else if (layerType == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type LayerType"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type LayerType"); } else if (dtCtorId == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type DtCtorId"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type DtCtorId"); } else if (charType == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type char"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type char"); } else if (refType == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type ref"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type ref"); } else if (boxType == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type Box"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type Box"); } else if (tickType == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type TickType"); + Console.WriteLine("Error: Dafny prelude is missing declaration of type TickType"); } else if (heap == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of $Heap"); + Console.WriteLine("Error: Dafny prelude is missing declaration of $Heap"); } else if (allocField == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of constant alloc"); + Console.WriteLine("Error: Dafny prelude is missing declaration of constant alloc"); } else if (tuple2TypeConstructor == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of tuple2TypeConstructor"); + Console.WriteLine("Error: Dafny prelude is missing declaration of tuple2TypeConstructor"); } else if (objectTypeConstructor == null) { - options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of objectTypeConstructor"); + Console.WriteLine("Error: Dafny prelude is missing declaration of objectTypeConstructor"); } else { return new PredefinedDecls(charType, refType, boxType, tickType, setTypeCtor, isetTypeCtor, multiSetTypeCtor, @@ -1667,7 +1667,7 @@ Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) { } var name = MethodName(iter, kind); - var proc = new Bpl.Procedure(iter.tok, name, new List(), inParams, outParams, false, req, mod, ens, etran.TrAttributes(iter.Attributes, null)); + var proc = new Bpl.Procedure(iter.tok, name, new List(), inParams, outParams, req, mod, ens, etran.TrAttributes(iter.Attributes, null)); AddVerboseName(proc, iter.FullDafnyName, kind); currentModule = null; @@ -4301,7 +4301,7 @@ void AddWellformednessCheck(Function f) { } var proc = new Bpl.Procedure(f.tok, "CheckWellformed" + NameSeparator + f.FullSanitizedName, new List(), Concat(Concat(typeInParams, inParams_Heap), inParams), outParams, - false, req, mod, ens, etran.TrAttributes(f.Attributes, null)); + req, mod, ens, etran.TrAttributes(f.Attributes, null)); AddVerboseName(proc, f.FullDafnyName, MethodTranslationKind.SpecWellformedness); sink.AddTopLevelDeclaration(proc); @@ -4537,7 +4537,7 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { var name = MethodName(decl, MethodTranslationKind.SpecWellformedness); var proc = new Bpl.Procedure(decl.tok, name, new List(), inParams, new List(), - false, req, mod, new List(), etran.TrAttributes(decl.Attributes, null)); + req, mod, new List(), etran.TrAttributes(decl.Attributes, null)); AddVerboseName(proc, decl.Name, MethodTranslationKind.SpecWellformedness); sink.AddTopLevelDeclaration(proc); @@ -4690,7 +4690,7 @@ void AddWellformednessCheck(ConstantField decl) { var name = MethodName(decl, MethodTranslationKind.SpecWellformedness); var proc = new Bpl.Procedure(decl.tok, name, new List(), inParams, new List(), - false, req, varlist, new List(), etran.TrAttributes(decl.Attributes, null)); + req, varlist, new List(), etran.TrAttributes(decl.Attributes, null)); AddVerboseName(proc, decl.FullDafnyName, MethodTranslationKind.SpecWellformedness); sink.AddTopLevelDeclaration(proc); @@ -4761,7 +4761,7 @@ void AddWellformednessCheck(DatatypeCtor ctor) { var varlist = new List { heapVar, etran.Tick() }; var proc = new Bpl.Procedure(ctor.tok, "CheckWellformed" + NameSeparator + ctor.FullName, new List(), inParams, new List(), - false, req, varlist, new List(), etran.TrAttributes(ctor.Attributes, null)); + req, varlist, new List(), etran.TrAttributes(ctor.Attributes, null)); AddVerboseName(proc, ctor.FullName, MethodTranslationKind.SpecWellformedness); sink.AddTopLevelDeclaration(proc); diff --git a/Source/DafnyDriver/CSVTestLogger.cs b/Source/DafnyDriver/CSVTestLogger.cs index 6db93b18fb1..92d0f8c18fb 100644 --- a/Source/DafnyDriver/CSVTestLogger.cs +++ b/Source/DafnyDriver/CSVTestLogger.cs @@ -12,13 +12,8 @@ public class CSVTestLogger : ITestLoggerWithParameters { private readonly ConcurrentBag results = new(); private TextWriter writer; - private TextWriter logWriter; private string writerFilename; - public CSVTestLogger(TextWriter logWriter) { - this.logWriter = logWriter; - } - public void Initialize(TestLoggerEvents events, string testRunDirectory) { } @@ -77,7 +72,7 @@ private void TestRunCompleteHandler(object sender, TestRunCompleteEventArgs e) { } writer.Close(); - logWriter.WriteLine("Results File: " + Path.GetFullPath(writerFilename)); + Console.Out.WriteLine("Results File: " + Path.GetFullPath(writerFilename)); } } } diff --git a/Source/DafnyDriver/Commands/CommandRegistry.cs b/Source/DafnyDriver/Commands/CommandRegistry.cs index 4655d6d211b..66dae914255 100644 --- a/Source/DafnyDriver/Commands/CommandRegistry.cs +++ b/Source/DafnyDriver/Commands/CommandRegistry.cs @@ -17,13 +17,13 @@ namespace Microsoft.Dafny; -public interface ParseArgumentResult { +internal interface ParseArgumentResult { } -public record ParseArgumentSuccess(DafnyOptions DafnyOptions) : ParseArgumentResult; +record ParseArgumentSuccess(DafnyOptions DafnyOptions) : ParseArgumentResult; record ParseArgumentFailure(DafnyDriver.CommandLineArgumentsResult ExitResult) : ParseArgumentResult; -public static class CommandRegistry { +static class CommandRegistry { private const string ToolchainDebuggingHelpName = "--help-internal"; private static readonly HashSet Commands = new(); @@ -62,29 +62,12 @@ static CommandRegistry() { public static Argument FileArgument { get; } - class WritersConsole : IConsole { - private readonly TextWriter errWriter; - private readonly TextWriter outWriter; - - public WritersConsole(TextWriter outWriter, TextWriter errWriter) { - this.errWriter = errWriter; - this.outWriter = outWriter; - } - - public IStandardStreamWriter Out => StandardStreamWriter.Create(outWriter ?? TextWriter.Null); - - public bool IsOutputRedirected => outWriter != null; - public IStandardStreamWriter Error => StandardStreamWriter.Create(errWriter ?? TextWriter.Null); - public bool IsErrorRedirected => errWriter != null; - public bool IsInputRedirected => false; - } - [CanBeNull] - public static ParseArgumentResult Create(TextWriter outputWriter, TextWriter errorWriter, TextReader inputReader, string[] arguments) { + public static ParseArgumentResult Create(string[] arguments) { bool allowHidden = arguments.All(a => a != ToolchainDebuggingHelpName); - var console = new WritersConsole(outputWriter, errorWriter); + var wasInvoked = false; - var dafnyOptions = new DafnyOptions(inputReader, outputWriter, errorWriter); + var dafnyOptions = new DafnyOptions(); var optionValues = new Dictionary(); var options = new Options(optionValues); dafnyOptions.ShowEnv = ExecutionEngineOptions.ShowEnvironment.Never; @@ -117,11 +100,11 @@ public static ParseArgumentResult Create(TextWriter outputWriter, TextWriter err Union(new[] { "--version", "-h", ToolchainDebuggingHelpName, "--help", "[parse]", "[suggest]" }); if (!keywordForNewMode.Contains(first)) { if (first.Length > 0 && first[0] != '/' && first[0] != '-' && !File.Exists(first) && first.IndexOf('.') == -1) { - dafnyOptions.Printer.ErrorWriteLine(dafnyOptions.OutputWriter, + dafnyOptions.Printer.ErrorWriteLine(Console.Out, "*** Error: '{0}': The first input must be a command or a legacy option or file with supported extension", first); return new ParseArgumentFailure(DafnyDriver.CommandLineArgumentsResult.PREPROCESSING_ERROR); } - var oldOptions = new DafnyOptions(inputReader, outputWriter, errorWriter); + var oldOptions = new DafnyOptions(); if (oldOptions.Parse(arguments)) { return new ParseArgumentSuccess(oldOptions); } @@ -200,7 +183,7 @@ void CommandHandler(InvocationContext context) { builder = AddDeveloperHelp(rootCommand, builder); #pragma warning disable VSTHRD002 - var exitCode = builder.Build().InvokeAsync(arguments, console).Result; + var exitCode = builder.Build().InvokeAsync(arguments).Result; #pragma warning restore VSTHRD002 if (failedToProcessFile) { diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 1b8d2e85701..ee2a630b2f6 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -18,15 +18,12 @@ using System; using System.Collections.Generic; using System.Collections.ObjectModel; -using System.CommandLine; -using System.CommandLine.IO; using System.Diagnostics.Contracts; using System.IO; using System.Linq; using Microsoft.Boogie; using Bpl = Microsoft.Boogie; using System.Diagnostics; -using System.Threading; using DafnyCore; using Microsoft.Dafny.Plugins; @@ -100,29 +97,19 @@ static DafnyDriver() { }; public static int Main(string[] args) { - return MainWithWriters(Console.Out, Console.Error, Console.In, args); + int ret = 0; + var thread = new System.Threading.Thread( + new System.Threading.ThreadStart(() => { ret = ThreadMain(args); }), + 0x10000000); // 256MB stack size to prevent stack overflow + thread.Start(); + thread.Join(); + return ret; } - public static int MainWithWriters(TextWriter outputWriter, TextWriter errorWriter, TextReader inputReader, - string[] args) { - - // Code that shouldn't be needed, but prevents some exceptions when running the integration tests in parallel - // outputWriter = new UndisposableTextWriter(outputWriter); - // errorWriter = new UndisposableTextWriter(errorWriter); - // outputWriter = TextWriter.Synchronized(outputWriter); - // errorWriter = TextWriter.Synchronized(errorWriter); - -#pragma warning disable VSTHRD002 - return Task.Run(() => ThreadMain(outputWriter, errorWriter, inputReader, args)).Result; -#pragma warning restore VSTHRD002 - } - - private static int ThreadMain(TextWriter outputWriter, TextWriter errorWriter, TextReader inputReader, string[] args) { + public static int ThreadMain(string[] args) { Contract.Requires(cce.NonNullElements(args)); - - var cliArgumentsResult = ProcessCommandLineArguments(outputWriter, errorWriter, inputReader, - args, out var dafnyOptions, out var dafnyFiles, out var otherFiles); + var cliArgumentsResult = ProcessCommandLineArguments(args, out var dafnyOptions, out var dafnyFiles, out var otherFiles); ExitValue exitValue; switch (cliArgumentsResult) { @@ -153,7 +140,7 @@ private static int ThreadMain(TextWriter outputWriter, TextWriter errorWriter, T try { VerificationResultLogger.RaiseTestLoggerEvents(dafnyOptions); } catch (ArgumentException ae) { - dafnyOptions.Printer.ErrorWriteLine(dafnyOptions.OutputWriter, $"*** Error: {ae.Message}"); + dafnyOptions.Printer.ErrorWriteLine(Console.Out, $"*** Error: {ae.Message}"); exitValue = ExitValue.PREPROCESSING_ERROR; } } @@ -192,15 +179,12 @@ static HashSet SplitOptionValueIntoFiles(HashSet inputs) { return result; } - public static CommandLineArgumentsResult ProcessCommandLineArguments(TextWriter outputWriter, - TextWriter errorWriter, - TextReader inputReader, - string[] args, out DafnyOptions options, out List dafnyFiles, out List otherFiles) { + public static CommandLineArgumentsResult ProcessCommandLineArguments(string[] args, out DafnyOptions options, out List dafnyFiles, out List otherFiles) { dafnyFiles = new List(); otherFiles = new List(); try { - switch (CommandRegistry.Create(outputWriter, errorWriter, inputReader, args)) { + switch (CommandRegistry.Create(args)) { case ParseArgumentSuccess success: options = success.DafnyOptions; break; @@ -212,7 +196,7 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(TextWriter options.RunningBoogieFromCommandLine = true; } catch (ProverException pe) { - new DafnyConsolePrinter(DafnyOptions.Create(outputWriter)).ErrorWriteLine(outputWriter, "*** ProverException: {0}", pe.Message); + new DafnyConsolePrinter(DafnyOptions.Create()).ErrorWriteLine(Console.Out, "*** ProverException: {0}", pe.Message); options = null; return CommandLineArgumentsResult.PREPROCESSING_ERROR; } @@ -227,7 +211,7 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(TextWriter if (compiler == null) { if (nonOutOptions.CompilerName != null) { var known = String.Join(", ", compilers.Select(c => $"'{c.TargetId}' ({c.TargetName})")); - options.Printer.ErrorWriteLine(options.ErrorWriter, $"No compiler found for target \"{options.CompilerName}\"{(options.CompilerName.StartsWith("-t") || options.CompilerName.StartsWith("--") ? " (use just a target name, not a -t or --target option)" : "")}; expecting one of {known}"); + options.Printer.ErrorWriteLine(Console.Error, $"No compiler found for target \"{options.CompilerName}\"{(options.CompilerName.StartsWith("-t") || options.CompilerName.StartsWith("--") ? " (use just a target name, not a -t or --target option)" : "")}; expecting one of {known}"); return CommandLineArgumentsResult.PREPROCESSING_ERROR; } @@ -251,17 +235,17 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(TextWriter if (options.XmlSink != null) { string errMsg = options.XmlSink.Open(); if (errMsg != null) { - options.Printer.ErrorWriteLine(options.ErrorWriter, "*** Error: " + errMsg); + options.Printer.ErrorWriteLine(Console.Error, "*** Error: " + errMsg); return CommandLineArgumentsResult.PREPROCESSING_ERROR; } } if (options.ShowEnv == ExecutionEngineOptions.ShowEnvironment.Always) { - outputWriter.WriteLine("---Command arguments"); + Console.WriteLine("---Command arguments"); foreach (string arg in args) { Contract.Assert(arg != null); - outputWriter.WriteLine(arg); + Console.WriteLine(arg); } - outputWriter.WriteLine("--------------------"); + Console.WriteLine("--------------------"); } ISet filesSeen = new HashSet(); @@ -301,23 +285,23 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(TextWriter if (File.Exists(file) || extension == ".h") { otherFiles.Add(file); } else { - options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: file {nameToShow} not found"); + options.Printer.ErrorWriteLine(Console.Out, $"*** Error: file {nameToShow} not found"); return CommandLineArgumentsResult.PREPROCESSING_ERROR; } } else if (options.Format && Directory.Exists(file)) { options.FoldersToFormat.Add(file); } else if (!isDafnyFile) { if (options.UsingNewCli && string.IsNullOrEmpty(extension) && file.Length > 0) { - options.Printer.ErrorWriteLine(options.OutputWriter, + options.Printer.ErrorWriteLine(Console.Out, "*** Error: Command-line argument '{0}' is neither a recognized option nor a filename with a supported extension ({1}).", nameToShow, string.Join(", ", Enumerable.Repeat(".dfy", 1).Concat(supportedExtensions))); } else if (string.IsNullOrEmpty(extension) && file.Length > 0 && (file[0] == '/' || file[0] == '-')) { - options.Printer.ErrorWriteLine(options.OutputWriter, + options.Printer.ErrorWriteLine(Console.Out, "*** Error: Command-line argument '{0}' is neither a recognized option nor a filename with a supported extension ({1}).", nameToShow, string.Join(", ", Enumerable.Repeat(".dfy", 1).Concat(supportedExtensions))); } else { - options.Printer.ErrorWriteLine(options.OutputWriter, + options.Printer.ErrorWriteLine(Console.Out, "*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be Dafny programs (.dfy) or supported auxiliary files ({2})", nameToShow, extension, string.Join(", ", supportedExtensions)); } @@ -327,12 +311,12 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(TextWriter if (dafnyFiles.Count == 0) { if (!options.Format) { - options.Printer.ErrorWriteLine(options.OutputWriter, "*** Error: The command-line contains no .dfy files"); + options.Printer.ErrorWriteLine(Console.Out, "*** Error: The command-line contains no .dfy files"); return CommandLineArgumentsResult.PREPROCESSING_ERROR; } if (options.FoldersToFormat.Count == 0) { - options.Printer.ErrorWriteLine(options.OutputWriter, + options.Printer.ErrorWriteLine(Console.Out, "Usage:\ndafny format [--check] [--print] ...\nYou can use '.' for the current directory"); return CommandLineArgumentsResult.PREPROCESSING_ERROR; } @@ -340,13 +324,13 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(TextWriter if (dafnyFiles.Count > 1 && options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) { - options.Printer.ErrorWriteLine(options.OutputWriter, + options.Printer.ErrorWriteLine(Console.Out, "*** Error: Only one .dfy file can be specified for testing"); return CommandLineArgumentsResult.PREPROCESSING_ERROR; } if (options.ExtractCounterexample && options.ModelViewFile == null) { - options.Printer.ErrorWriteLine(options.OutputWriter, + options.Printer.ErrorWriteLine(Console.Out, "*** Error: ModelView file must be specified when attempting counterexample extraction"); return CommandLineArgumentsResult.PREPROCESSING_ERROR; } @@ -362,7 +346,7 @@ private async Task ProcessFilesAsync(IList/*!*/ dafny ExitValue exitValue = ExitValue.SUCCESS; if (options.TestGenOptions.WarnDeadCode) { await foreach (var line in DafnyTestGeneration.Main.GetDeadCodeStatistics(dafnyFileNames[0], options)) { - await options.OutputWriter.WriteLineAsync(line); + Console.WriteLine(line); } if (DafnyTestGeneration.Main.setNonZeroExitCode) { exitValue = ExitValue.DAFNY_ERROR; @@ -371,7 +355,7 @@ private async Task ProcessFilesAsync(IList/*!*/ dafny } if (options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) { await foreach (var line in DafnyTestGeneration.Main.GetTestClassForProgram(dafnyFileNames[0], options)) { - await options.OutputWriter.WriteLineAsync(line); + Console.WriteLine(line); } if (DafnyTestGeneration.Main.setNonZeroExitCode) { exitValue = ExitValue.DAFNY_ERROR; @@ -381,8 +365,8 @@ private async Task ProcessFilesAsync(IList/*!*/ dafny if (options.VerifySeparately && 1 < dafnyFiles.Count) { foreach (var f in dafnyFiles) { - await options.OutputWriter.WriteLineAsync(); - await options.OutputWriter.WriteLineAsync($"-------------------- {f} --------------------"); + Console.WriteLine(); + Console.WriteLine("-------------------- {0} --------------------", f); var ev = await ProcessFilesAsync(new List { f }, new List().AsReadOnly(), options, lookForSnapshots, f.FilePath); if (exitValue != ev && ev != ExitValue.SUCCESS) { exitValue = ev; @@ -408,27 +392,27 @@ private async Task ProcessFilesAsync(IList/*!*/ dafny } string programName = dafnyFileNames.Count == 1 ? dafnyFileNames[0] : "the_program"; + Program dafnyProgram; string err; if (Options.Format) { - return DoFormatting(dafnyFiles, Options, programName, options.ErrorWriter); + return DoFormatting(dafnyFiles, Options, programName); } - err = DafnyMain.ParseCheck(Options.Input, dafnyFiles, programName, options, out var dafnyProgram); + err = Dafny.Main.ParseCheck(dafnyFiles, programName, options, out dafnyProgram); if (err != null) { exitValue = ExitValue.DAFNY_ERROR; - options.Printer.ErrorWriteLine(options.OutputWriter, err); + options.Printer.ErrorWriteLine(Console.Out, err); } else if (dafnyProgram != null && !options.NoResolve && !options.NoTypecheck && options.DafnyVerify) { - var boogiePrograms = - await DafnyMain.LargeStackFactory.StartNew(() => Translate(engine.Options, dafnyProgram).ToList()); + var boogiePrograms = Translate(engine.Options, dafnyProgram).ToList(); string baseName = cce.NonNull(Path.GetFileName(dafnyFileNames[^1])); var (verified, outcome, moduleStats) = await BoogieAsync(options, baseName, boogiePrograms, programId); bool compiled; try { - compiled = await Compile(dafnyFileNames[0], otherFileNames, dafnyProgram, outcome, moduleStats, verified); + compiled = Compile(dafnyFileNames[0], otherFileNames, dafnyProgram, outcome, moduleStats, verified); } catch (UnsupportedFeatureException e) { if (!options.Backend.UnsupportedFeatures.Contains(e.Feature)) { throw new Exception($"'{e.Feature}' is not an element of the {options.Backend.TargetId} compiler's UnsupportedFeatures set"); @@ -452,7 +436,7 @@ private async Task ProcessFilesAsync(IList/*!*/ dafny return exitValue; } - private static ExitValue DoFormatting(IList dafnyFiles, DafnyOptions options, string programName, TextWriter errorWriter) { + private static ExitValue DoFormatting(IList dafnyFiles, DafnyOptions options, string programName) { var exitValue = ExitValue.SUCCESS; Contract.Assert(dafnyFiles.Count > 0 || options.FoldersToFormat.Count > 0); dafnyFiles = dafnyFiles.Concat(options.FoldersToFormat.SelectMany(folderPath => { @@ -469,7 +453,7 @@ private static ExitValue DoFormatting(IList dafnyFiles, DafnyOptions foreach (var file in dafnyFiles) { var dafnyFile = file; if (dafnyFile.UseStdin && !doCheck && !doPrint) { - errorWriter.WriteLine("Please use the --check and/or --print option as stdin cannot be formatted in place."); + Console.Error.WriteLine("Please use the --check and/or --print option as stdin cannot be formatted in place."); exitValue = ExitValue.PREPROCESSING_ERROR; continue; } @@ -482,13 +466,13 @@ private static ExitValue DoFormatting(IList dafnyFiles, DafnyOptions } // Might not be totally optimized but let's do that for now - var err = DafnyMain.Parse(options.Input, new List { dafnyFile }, programName, options, out var dafnyProgram); + var err = Dafny.Main.Parse(new List { dafnyFile }, programName, options, out var dafnyProgram); var originalText = dafnyFile.UseStdin ? Console.In.ReadToEnd() : File.Exists(dafnyFile.FilePath) ? File.ReadAllText(dafnyFile.FilePath) : null; if (err != null) { exitValue = ExitValue.DAFNY_ERROR; - errorWriter.WriteLine(err); + Console.Error.WriteLine(err); failedToParseFiles.Add(dafnyFile.BaseName); } else { var firstToken = dafnyProgram.GetFirstTopLevelToken(); @@ -503,10 +487,10 @@ private static ExitValue DoFormatting(IList dafnyFiles, DafnyOptions } if (doCheck && (!doPrint || options.CompileVerbose)) { - options.OutputWriter.WriteLine("The file " + - (options.UseBaseNameForFileName - ? Path.GetFileName(dafnyFile.FilePath) - : dafnyFile.FilePath) + " needs to be formatted"); + Console.Out.WriteLine("The file " + + (options.UseBaseNameForFileName + ? Path.GetFileName(dafnyFile.FilePath) + : dafnyFile.FilePath) + " needs to be formatted"); } if (!doCheck && !doPrint) { @@ -515,7 +499,7 @@ private static ExitValue DoFormatting(IList dafnyFiles, DafnyOptions } } else { if (options.CompileVerbose) { - options.ErrorWriter.WriteLine(dafnyFile.BaseName + " was empty."); + Console.Error.WriteLine(dafnyFile.BaseName + " was empty."); } emptyFiles.Add((options.UseBaseNameForFileName @@ -523,7 +507,7 @@ private static ExitValue DoFormatting(IList dafnyFiles, DafnyOptions : dafnyFile.FilePath)); } if (doPrint) { - options.OutputWriter.Write(result); + Console.Out.Write(result); } } @@ -551,12 +535,12 @@ string Files(int num) { reportMsg = filesNeedFormatting + reportMsg; if (doCheck) { - options.OutputWriter.WriteLine(neededFormatting > 0 + Console.Out.WriteLine(neededFormatting > 0 ? $"Error: {reportMsg}" : "All files are correctly formatted"); } else if (failedToParseFiles.Count > 0 || options.CompileVerbose) { // We don't display anything if we just format files without verbosity and there was no parse error - options.OutputWriter.WriteLine($"{reportMsg}"); + Console.Out.WriteLine($"{reportMsg}"); } return exitValue; @@ -570,14 +554,14 @@ string Files(int num) { /// the counterexample private static void PrintCounterexample(DafnyOptions options, string modelViewFile) { var model = DafnyModel.ExtractModel(options, File.ReadAllText(modelViewFile)); - options.OutputWriter.WriteLine("Counterexample for first failing assertion: "); + Console.WriteLine("Counterexample for first failing assertion: "); foreach (var state in model.States.Where(state => !state.IsInitialState)) { - options.OutputWriter.WriteLine(state.FullStateName + ":"); + Console.WriteLine(state.FullStateName + ":"); var vars = state.ExpandedVariableSet(-1); foreach (var variable in vars) { - options.OutputWriter.WriteLine($"\t{variable.ShortName} : " + - $"{DafnyModelTypeUtils.GetInDafnyFormat(variable.Type)} = " + - $"{variable.Value}"); + Console.WriteLine($"\t{variable.ShortName} : " + + $"{DafnyModelTypeUtils.GetInDafnyFormat(variable.Type)} = " + + $"{variable.Value}"); } } } @@ -597,7 +581,7 @@ private static string BoogieProgramSuffix(string printFile, string suffix) { if (options.PrintFile != null) { - var nm = nmodules > 1 ? Dafny.DafnyMain.BoogieProgramSuffix(options.PrintFile, prog.Item1) : options.PrintFile; + var nm = nmodules > 1 ? Dafny.Main.BoogieProgramSuffix(options.PrintFile, prog.Item1) : options.PrintFile; ExecutionEngine.PrintBplFile(options, nm, prog.Item2, false, false, options.PrettyPrint); } @@ -613,7 +597,7 @@ private static string BoogieProgramSuffix(string printFile, string suffix) { IEnumerable> boogiePrograms, string programId) { var concurrentModuleStats = new ConcurrentDictionary(); - var writerManager = new ConcurrentToSequentialWriteManager(options.OutputWriter); + var writerManager = new ConcurrentToSequentialWriteManager(Console.Out); var moduleTasks = boogiePrograms.Select(async program => { await using var moduleWriter = writerManager.AppendWriter(); @@ -625,12 +609,12 @@ private static string BoogieProgramSuffix(string printFile, string suffix) { }).ToList(); await Task.WhenAll(moduleTasks); - await options.OutputWriter.FlushAsync(); + await Console.Out.FlushAsync(); var outcome = moduleTasks.Select(t => t.Result.Outcome) .Aggregate(PipelineOutcome.VerificationCompleted, MergeOutcomes); var isVerified = moduleTasks.Select(t => - Dafny.DafnyMain.IsBoogieVerified(t.Result.Outcome, t.Result.Stats)).All(x => x); + Dafny.Main.IsBoogieVerified(t.Result.Outcome, t.Result.Stats)).All(x => x); return (isVerified, outcome, concurrentModuleStats); } @@ -647,7 +631,7 @@ private static string BoogieProgramSuffix(string printFile, string suffix) { } var result = - await Dafny.DafnyMain.BoogieOnce(options, output, engine, baseName, moduleName, program, programId); + await Dafny.Main.BoogieOnce(options, output, engine, baseName, moduleName, program, programId); watch.Stop(); @@ -721,24 +705,24 @@ private static void WriteModuleStats(DafnyOptions options, TextWriter output, ID } - public static async Task Compile(string fileName, ReadOnlyCollection otherFileNames, Program dafnyProgram, + public static bool Compile(string fileName, ReadOnlyCollection otherFileNames, Program dafnyProgram, PipelineOutcome oc, IDictionary moduleStats, bool verified) { var options = dafnyProgram.Options; var resultFileName = options.DafnyPrintCompiledFile ?? fileName; bool compiled = true; switch (oc) { case PipelineOutcome.VerificationCompleted: - WriteModuleStats(options, options.OutputWriter, moduleStats); + WriteModuleStats(options, Console.Out, moduleStats); if ((options.Compile && verified && !options.UserConstrainedProcsToCheck) || options.ForceCompile) { - compiled = await CompileDafnyProgram(dafnyProgram, resultFileName, otherFileNames, true); + compiled = CompileDafnyProgram(dafnyProgram, resultFileName, otherFileNames, true); } else if ((2 <= options.SpillTargetCode && verified && !options.UserConstrainedProcsToCheck) || 3 <= options.SpillTargetCode) { - compiled = await CompileDafnyProgram(dafnyProgram, resultFileName, otherFileNames, false); + compiled = CompileDafnyProgram(dafnyProgram, resultFileName, otherFileNames, false); } break; case PipelineOutcome.Done: - WriteModuleStats(options, options.OutputWriter, moduleStats); + WriteModuleStats(options, Console.Out, moduleStats); if (options.ForceCompile || 3 <= options.SpillTargetCode) { - compiled = await CompileDafnyProgram(dafnyProgram, resultFileName, otherFileNames, options.ForceCompile); + compiled = CompileDafnyProgram(dafnyProgram, resultFileName, otherFileNames, options.ForceCompile); } break; default: @@ -812,10 +796,11 @@ static void WriteFile(string filename, string text, string moreText = null) { } CheckFilenameIsLegal(filename); - using TextWriter target = new StreamWriter(new FileStream(filename, FileMode.Create)); - target.Write(text); - if (moreText != null) { - target.Write(moreText); + using (TextWriter target = new StreamWriter(new FileStream(filename, System.IO.FileMode.Create))) { + target.Write(text); + if (moreText != null) { + target.Write(moreText); + } } } @@ -841,13 +826,16 @@ private static void CheckFilenameIsLegal(string filename) { /// Generate a C# program from the Dafny program and, if "invokeCompiler" is "true", invoke /// the C# compiler to compile it. /// - public static async Task CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyProgramName, - ReadOnlyCollection otherFileNames, bool invokeCompiler) { + public static bool CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyProgramName, + ReadOnlyCollection otherFileNames, bool invokeCompiler, + TextWriter outputWriter = null) { Contract.Requires(dafnyProgram != null); Contract.Assert(dafnyProgramName != null); - var outputWriter = dafnyProgram.Options.OutputWriter; - var errorWriter = dafnyProgram.Options.ErrorWriter; + // TODO: `outputWriter` seems to always be passed in as `null`. Remove it? + if (outputWriter == null) { + outputWriter = Console.Out; + } // Compile the Dafny program into a string that contains the target program var oldErrorCount = dafnyProgram.Reporter.Count(ErrorLevel.Error); @@ -864,7 +852,7 @@ public static async Task CompileDafnyProgram(Dafny.Program dafnyProgram, s var otherFiles = new Dictionary(); { var output = new ConcreteSyntaxTree(); - await DafnyMain.LargeStackFactory.StartNew(() => compiler.Compile(dafnyProgram, output)); + compiler.Compile(dafnyProgram, output); var writerOptions = new WriterState(); var targetProgramTextWriter = new StringWriter(); var files = new Queue(); @@ -913,16 +901,15 @@ public static async Task CompileDafnyProgram(Dafny.Program dafnyProgram, s if (compiledCorrectly && options.RunAfterCompile) { if (hasMain) { if (options.CompileVerbose) { - await outputWriter.WriteLineAsync("Running..."); - await outputWriter.WriteLineAsync(); + outputWriter.WriteLine("Running..."); + outputWriter.WriteLine(); } - compiledCorrectly = compiler.RunTargetProgram(dafnyProgramName, targetProgramText, callToMain, - paths.Filename, otherFileNames, compilationResult, outputWriter, errorWriter); + compiledCorrectly = compiler.RunTargetProgram(dafnyProgramName, targetProgramText, callToMain, paths.Filename, otherFileNames, compilationResult, outputWriter); } else { // make sure to give some feedback to the user if (options.CompileVerbose) { - await outputWriter.WriteLineAsync("Program compiled successfully"); + outputWriter.WriteLine("Program compiled successfully"); } } } @@ -957,10 +944,8 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target throw new NotSupportedException(); } - public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, - string pathsFilename, - ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter, - TextWriter errorWriter) { + public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, string pathsFilename, + ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter) { throw new NotSupportedException(); } } diff --git a/Source/DafnyDriver/TextLogger.cs b/Source/DafnyDriver/TextLogger.cs index 76fe748c4aa..5d67f26f1af 100644 --- a/Source/DafnyDriver/TextLogger.cs +++ b/Source/DafnyDriver/TextLogger.cs @@ -8,14 +8,9 @@ namespace Microsoft.Dafny; public class TextLogger { private TextWriter tw; - private TextWriter outWriter; - - public TextLogger(TextWriter outWriter) { - this.outWriter = outWriter; - } public void Initialize(Dictionary parameters) { - tw = parameters.TryGetValue("LogFileName", out string filename) ? new StreamWriter(filename) : outWriter; + tw = parameters.TryGetValue("LogFileName", out string filename) ? new StreamWriter(filename) : Console.Out; } public void LogResults(List<(Implementation, VerificationResult)> verificationResults) { diff --git a/Source/DafnyDriver/VerificationResultLogger.cs b/Source/DafnyDriver/VerificationResultLogger.cs index 905a097c757..e30d5df7051 100644 --- a/Source/DafnyDriver/VerificationResultLogger.cs +++ b/Source/DafnyDriver/VerificationResultLogger.cs @@ -58,12 +58,12 @@ public static void RaiseTestLoggerEvents(DafnyOptions options) { var logger = new TrxLogger(); logger.Initialize(events, parameters); } else if (loggerName == "csv") { - var csvLogger = new CSVTestLogger(options.OutputWriter); + var csvLogger = new CSVTestLogger(); csvLogger.Initialize(events, parameters); } else if (loggerName == "text") { // This logger doesn't implement the ITestLogger interface because // it uses information that's tricky to encode in a TestResult. - var textLogger = new TextLogger(options.OutputWriter); + var textLogger = new TextLogger(); textLogger.Initialize(parameters); textLogger.LogResults(verificationResults); return; diff --git a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs index df093b57ad2..3f310d1c3cf 100644 --- a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs +++ b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs @@ -7,7 +7,6 @@ using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Xunit; -using Xunit.Abstractions; using XunitAssertMessages; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.CodeActions { @@ -309,9 +308,6 @@ private async Task TestCodeAction(string source) { } } - public CodeActionTest(ITestOutputHelper output) : base(output) { - } - private static List ApplyEdits(TextDocumentEdit textDocumentEdit, string output) { var inversedEdits = textDocumentEdit.Edits.ToList() .OrderByDescending(x => x.Range.Start.Line) diff --git a/Source/DafnyLanguageServer.Test/Completion/DotCompletionTest.cs b/Source/DafnyLanguageServer.Test/Completion/DotCompletionTest.cs index 048fb3d3b45..c54b132846b 100644 --- a/Source/DafnyLanguageServer.Test/Completion/DotCompletionTest.cs +++ b/Source/DafnyLanguageServer.Test/Completion/DotCompletionTest.cs @@ -6,7 +6,6 @@ using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Completion { public class DotCompletionTest : ClientBasedLanguageServerTest { @@ -218,8 +217,5 @@ method GetConstant() returns (c: int) { Assert.Equal(CompletionItemKind.Method, completionList[0].Kind); Assert.Equal("GetConstant", completionList[0].Label); } - - public DotCompletionTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs index e39ddaeaabc..1e7fb744a56 100644 --- a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs +++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs @@ -20,11 +20,9 @@ using Microsoft.Dafny.LanguageServer.IntegrationTest.Various; using Microsoft.Dafny.LanguageServer.Language; using OmniSharp.Extensions.LanguageServer.Client; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest { public class DafnyLanguageServerTestBase : LanguageServerTestBase { - protected readonly string SlowToVerify = @" lemma {:timeLimit 3} SquareRoot2NotRational(p: nat, q: nat) requires p > 0 && q > 0 @@ -49,16 +47,13 @@ ensures true public const string LanguageId = "dafny"; protected static int fileIndex; - protected readonly TextWriter output; public ILanguageServer Server { get; private set; } public IDocumentDatabase Documents => Server.GetRequiredService(); - public DafnyLanguageServerTestBase(ITestOutputHelper output) : base(new JsonRpcTestOptions(LoggerFactory.Create( - builder => builder.AddConsole().SetMinimumLevel(LogLevel.Warning)))) { - this.output = new WriterFromOutputHelper(output); - } + public DafnyLanguageServerTestBase() : base(new JsonRpcTestOptions(LoggerFactory.Create( + builder => builder.AddConsole().SetMinimumLevel(LogLevel.Warning)))) { } protected virtual IServiceCollection ServerOptionsAction(LanguageServerOptions serverOptions) { return serverOptions.Services.AddSingleton(serviceProvider => new SlowVerifier( @@ -70,7 +65,7 @@ protected virtual IServiceCollection ServerOptionsAction(LanguageServerOptions s protected virtual async Task InitializeClient( Action clientOptionsAction = null, Action modifyOptions = null) { - var dafnyOptions = DafnyOptions.Create(output); + var dafnyOptions = DafnyOptions.Create(); modifyOptions?.Invoke(dafnyOptions); void NewServerOptionsAction(LanguageServerOptions options) { diff --git a/Source/DafnyLanguageServer.Test/Formatting/FormattingTest.cs b/Source/DafnyLanguageServer.Test/Formatting/FormattingTest.cs index 12f64d43d90..382d9d63436 100644 --- a/Source/DafnyLanguageServer.Test/Formatting/FormattingTest.cs +++ b/Source/DafnyLanguageServer.Test/Formatting/FormattingTest.cs @@ -9,7 +9,6 @@ using OmniSharp.Extensions.LanguageServer.Protocol.Document; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.Formatting; public class FormattingTest : ClientBasedLanguageServerTest { @@ -163,7 +162,4 @@ private async Task FormattingWorksFor(string source, string target = null) { } Assert.Equal(target, finalText); } - - public FormattingTest(ITestOutputHelper output) : base(output) { - } } diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs index fbb005f8e46..ffdbba5c28e 100644 --- a/Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs @@ -1,5 +1,4 @@ using System.Threading.Tasks; -using Xunit.Abstractions; using Xunit; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics; @@ -41,7 +40,4 @@ await VerifyTrace(@" . S [S][ ][I][S][S][ ]: //Next: . S [S][ ][I][S][S][ ]:}"); } - - public CachedLinearVerificationGutterStatusTester(ITestOutputHelper output) : base(output) { - } } diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/ConcurrentLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/ConcurrentLinearVerificationGutterStatusTester.cs index 77ff734ed1b..94b372140e7 100644 --- a/Source/DafnyLanguageServer.Test/GutterStatus/ConcurrentLinearVerificationGutterStatusTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/ConcurrentLinearVerificationGutterStatusTester.cs @@ -4,7 +4,6 @@ using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Microsoft.Dafny.LanguageServer.Workspace.Notifications; using OmniSharp.Extensions.JsonRpc; -using Xunit.Abstractions; using Xunit; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics; @@ -59,6 +58,4 @@ public async Task EnsuresManyDocumentsCanBeVerifiedAtOnce() { } } - public ConcurrentLinearVerificationGutterStatusTester(ITestOutputHelper output) : base(output) { - } } diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs index 45a8055c424..655e9f7d37f 100644 --- a/Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs @@ -10,7 +10,6 @@ using OmniSharp.Extensions.JsonRpc; using OmniSharp.Extensions.LanguageServer.Client; using OmniSharp.Extensions.LanguageServer.Protocol.Models; -using Xunit.Abstractions; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics; @@ -285,7 +284,4 @@ public string AcceptQuestionMarks(string traceObtained, string expected) { var toReplaceRegex = new Regex(pattern); return toReplaceRegex.Replace(traceObtained, "?"); } - - protected LinearVerificationGutterStatusTester(ITestOutputHelper output) : base(output) { - } } diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/ReorderingVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/ReorderingVerificationGutterStatusTester.cs index 3fb5cff9f0f..d3b7d9e5b0e 100644 --- a/Source/DafnyLanguageServer.Test/GutterStatus/ReorderingVerificationGutterStatusTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/ReorderingVerificationGutterStatusTester.cs @@ -10,7 +10,6 @@ using Microsoft.Dafny.LanguageServer.Workspace; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; -using Xunit.Abstractions; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics; @@ -139,7 +138,7 @@ async Task CompareWithExpectation(List expectedSymbols) { $"Expected {string.Join(", ", expectedSymbols)} but got {string.Join(", ", orderAfterChangeSymbols)}." + $"\nOld to new history was: {verificationStatusReceiver.History.Stringify()}"); } catch (OperationCanceledException) { - await output.WriteLineAsync($"Operation cancelled for index {index} when expecting: {string.Join(", ", expectedSymbols)}"); + Console.WriteLine($"Operation cancelled for index {index} when expecting: {string.Join(", ", expectedSymbols)}"); throw; } @@ -232,7 +231,4 @@ public async IAsyncEnumerable> GetRunningOrder(SemaphoreSlim semapho yield return newlyReported.ToList(); } while (!started || foundStatus.NamedVerifiables.Any(v => v.Status < PublishedVerificationStatus.Error)); } - - public ReorderingVerificationGutterStatusTester(ITestOutputHelper output) : base(output) { - } } diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs index 5371dec112a..184ece94a38 100644 --- a/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs @@ -1,7 +1,6 @@ using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics; @@ -211,7 +210,4 @@ await VerifyTrace(@" . | | | : true . | | | :}"); } - - public SimpleLinearVerificationGutterStatusTester(ITestOutputHelper output) : base(output) { - } } diff --git a/Source/DafnyLanguageServer.Test/Lookup/DefinitionTest.cs b/Source/DafnyLanguageServer.Test/Lookup/DefinitionTest.cs index 659711bbfac..7b7566affc0 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/DefinitionTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/DefinitionTest.cs @@ -9,7 +9,6 @@ using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup { public class DefinitionTest : ClientBasedLanguageServerTest { @@ -463,8 +462,5 @@ method Q ... }".TrimStart(); await AssertPositionsLineUpWithRanges(source); } - - public DefinitionTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs b/Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs index d116e7b328f..6e1b7b8a03d 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs @@ -5,7 +5,6 @@ using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup { public class DocumentSymbolTest : ClientBasedLanguageServerTest { @@ -151,8 +150,5 @@ public async Task CanResolveSymbolsForFunctionWithoutBody() { Assert.Equal(new Range((0, 9), (0, 17)), methodSymbol.SelectionRange); Assert.Equal(SymbolKind.Function, methodSymbol.Kind); } - - public DocumentSymbolTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs index eb0c639f4f4..faa82646d0c 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs @@ -8,7 +8,6 @@ using System.Threading.Tasks; using JetBrains.Annotations; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; -using Xunit.Abstractions; using Xunit; using XunitAssertMessages; @@ -501,9 +500,6 @@ method test(opt: int) { "); } - public HoverTest(ITestOutputHelper output) : base(output) { - } - [Fact] public async Task HoverShouldDisplayComments() { await AssertHover(@" diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs index 875f772e10a..f3fb54a190e 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs @@ -10,7 +10,6 @@ using OmniSharp.Extensions.JsonRpc; using OmniSharp.Extensions.LanguageServer.Protocol.Document; using OmniSharp.Extensions.LanguageServer.Protocol.Models; -using Xunit.Abstractions; using Xunit; using XunitAssertMessages; @@ -492,8 +491,5 @@ private Task RequestHover(TextDocumentItem documentItem, Position positio CancellationToken ); } - - public HoverVerificationTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/Lookup/SignatureHelpTest.cs b/Source/DafnyLanguageServer.Test/Lookup/SignatureHelpTest.cs index 5004fd263ac..042bb2bdb87 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/SignatureHelpTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/SignatureHelpTest.cs @@ -5,7 +5,6 @@ using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup { public class SignatureHelpTest : ClientBasedLanguageServerTest { @@ -190,8 +189,5 @@ method GetProduct(x: int, y: int) returns (p: int) Assert.Equal(MarkupKind.Markdown, markup.Kind); Assert.Equal("```dafny\nfunction A.Multiply(n: int, m: int): int\n```", markup.Value); } - - public SignatureHelpTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs index 7037af3371c..984a601c35b 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs @@ -3,7 +3,6 @@ using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest; @@ -31,7 +30,4 @@ public async Task ProjectFileOverridesOptions() { Assert.Empty(diagnostics); } - - public ProjectFilesTest(ITestOutputHelper output) : base(output) { - } } \ No newline at end of file diff --git a/Source/DafnyLanguageServer.Test/StandaloneServerTest.cs b/Source/DafnyLanguageServer.Test/StandaloneServerTest.cs index ff6f881a7d4..11b04be4e46 100644 --- a/Source/DafnyLanguageServer.Test/StandaloneServerTest.cs +++ b/Source/DafnyLanguageServer.Test/StandaloneServerTest.cs @@ -1,49 +1,14 @@ -using System; -using System.IO; -using System.Text; using Microsoft.Dafny.LanguageServer.Workspace; -using Xunit.Abstractions; using Xunit; namespace Microsoft.Dafny.LanguageServer.IntegrationTest; public class StandaloneServerTest { - private readonly TextWriter output; - - public StandaloneServerTest(ITestOutputHelper output) { - this.output = new WriterFromOutputHelper(output); - } [Fact] public void OptionParsing() { var arguments = new[] { "--documents:verify=onsave", "--verifier:timelimit=3", "--ghost:markStatements=true" }; - var options = Program.GetOptionsFromArgs(output, TextReader.Null, arguments); + var options = Program.GetOptionsFromArgs(arguments); Assert.Equal(VerifyOnMode.Save, options.Get(ServerCommand.Verification)); } } - -public class WriterFromOutputHelper : TextWriter { - private readonly ITestOutputHelper output; - private bool failed = false; - - public WriterFromOutputHelper(ITestOutputHelper output) { - this.output = output; - } - - public override void Write(char value) { - if (!failed) { - failed = true; - WriteLine("Error: tried to write a single character, which WriterFromOutputHelper does not support."); - } - } - - public override Encoding Encoding => Encoding.Default; - - public override void WriteLine(string value) { - output.WriteLine(value); - } - - public override void WriteLine(string format, params object[] arg) { - output.WriteLine(format, arg); - } -} diff --git a/Source/DafnyLanguageServer.Test/Synchronization/CloseDocumentTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/CloseDocumentTest.cs index 7e9514183ac..cc33c64f470 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/CloseDocumentTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/CloseDocumentTest.cs @@ -4,7 +4,6 @@ using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System.Threading.Tasks; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { public class CloseDocumentTest : DafnyLanguageServerTestBase, IAsyncLifetime { @@ -47,8 +46,5 @@ function GetConstant(): int { await CloseDocumentAndWaitAsync(documentItem); Assert.Null(await Documents.GetResolvedDocumentAsync(documentItem.Uri)); } - - public CloseDocumentTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs index de051bdddc6..4a13e98f748 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs @@ -6,7 +6,6 @@ using System.Linq; using System.Threading.Tasks; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { public class DeclarationLocationMigrationTest : SynchronizationTestBase { @@ -325,8 +324,5 @@ public async Task PassingANullChangeRangePreservesForeignSymbols() { Assert.NotNull(document); Assert.False(TryFindSymbolDeclarationByName(document, "A", out var _)); } - - public DeclarationLocationMigrationTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs index ee7f1308961..89a7f0b19bb 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs @@ -9,7 +9,6 @@ using System.Threading; using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.Workspace.ChangeProcessors; -using Xunit.Abstractions; using Xunit; using XunitAssertMessages; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; @@ -1131,8 +1130,5 @@ method Foo() { var diagnostics2 = await GetLastDiagnostics(documentItem, CancellationToken); Assert.True(diagnostics2.Any()); } - - public DiagnosticsTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/GhostDiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/GhostDiagnosticsTest.cs index 2fb5eca0df8..cccd14fe4c0 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/GhostDiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/GhostDiagnosticsTest.cs @@ -4,7 +4,6 @@ using System.Linq; using System.Threading.Tasks; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { public class GhostDiagnosticsTest : ClientBasedLanguageServerTest { @@ -193,8 +192,5 @@ await SetUp(options => { Assert.Equal("Ghost statement", diagnostics[3].Message); Assert.Equal(new Range((15, 4), (15, 14)), diagnostics[3].Range); } - - public GhostDiagnosticsTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs index 5fcd1b575c8..975d8228f9d 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs @@ -2,7 +2,6 @@ using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System.Threading.Tasks; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { public class LookupMigrationTest : SynchronizationTestBase { @@ -304,8 +303,5 @@ function GetY(): int { Assert.True(document.SignatureAndCompletionTable.TryGetSymbolAt((12, 7), out var symbol)); Assert.Equal("x", symbol.Name); } - - public LookupMigrationTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs index fa8d704488f..c4fe5a4c245 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs @@ -6,7 +6,6 @@ using System.Threading.Tasks; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System.IO; -using Xunit.Abstractions; using Xunit; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { @@ -137,8 +136,5 @@ public async Task EmptyDocumentCanBeIncluded() { Assert.NotNull(document); Assert.True(!document.Diagnostics.Any()); } - - public OpenDocumentTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/SaveDocumentTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/SaveDocumentTest.cs index 6df0d4fd4ab..f590235261e 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/SaveDocumentTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/SaveDocumentTest.cs @@ -4,7 +4,6 @@ using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { public class SaveDocumentTest : ClientBasedLanguageServerTest { @@ -94,8 +93,5 @@ method DoIt() { var message = afterSaveDiagnostics.First(); Assert.Equal(MessageSource.Verifier.ToString(), message.Source); } - - public SaveDocumentTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/SymbolMigrationTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/SymbolMigrationTest.cs index a039523a411..55f799d8147 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/SymbolMigrationTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/SymbolMigrationTest.cs @@ -4,7 +4,6 @@ using System.Linq; using System.Threading.Tasks; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { public class SymbolMigrationTest : SynchronizationTestBase { @@ -100,8 +99,5 @@ await ApplyChangeAndWaitCompletionAsync( Assert.True(document.SignatureAndCompletionTable.Resolved); Assert.Single(document.SignatureAndCompletionTable.Locations.Keys.OfType()); } - - public SymbolMigrationTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/SynchronizationTestBase.cs b/Source/DafnyLanguageServer.Test/Synchronization/SynchronizationTestBase.cs index 3bc05daa08a..98ad629af14 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/SynchronizationTestBase.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/SynchronizationTestBase.cs @@ -4,13 +4,12 @@ using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System.Threading.Tasks; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { public class SynchronizationTestBase : DafnyLanguageServerTestBase, IAsyncLifetime { protected ILanguageClient Client { get; set; } - public virtual async Task InitializeAsync() { + public async virtual Task InitializeAsync() { Client = await InitializeClient(); } @@ -38,8 +37,5 @@ protected Task ApplyChangesAndWaitCompletionAsync(TextDocumentItem documentItem, }); return Client.WaitForNotificationCompletionAsync(documentItem.Uri, CancellationToken); } - - public SynchronizationTestBase(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/TextInsertionTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/TextInsertionTest.cs index b100816268e..4b5c0bd1c37 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/TextInsertionTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/TextInsertionTest.cs @@ -2,7 +2,6 @@ using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System.Threading.Tasks; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { public class TextInsertionTest : SynchronizationTestBase { @@ -200,8 +199,5 @@ function GetConstant(): int { 1 } }".TrimStart(); Assert.Equal(expected, document.TextDocumentItem.Text); } - - public TextInsertionTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/TextReplacementTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/TextReplacementTest.cs index b83f6b33b37..db9ff08fac9 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/TextReplacementTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/TextReplacementTest.cs @@ -2,7 +2,6 @@ using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System.Threading.Tasks; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { public class TextReplacementTest : SynchronizationTestBase { @@ -253,8 +252,5 @@ public async Task ReplaceCompleteDocumentContent() { Assert.NotNull(document); Assert.Equal(change, document.TextDocumentItem.Text); } - - public TextReplacementTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs index f339b395227..3c66308d45a 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs @@ -7,7 +7,6 @@ using Microsoft.Dafny.LanguageServer.Workspace; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; -using Xunit.Abstractions; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization; @@ -537,7 +536,4 @@ public async Task SymbolStatusIsMigrated() { var errorStatus = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); Assert.Equal(migratedRange, errorStatus.NamedVerifiables[0].NameRange); } - - public VerificationStatusTest(ITestOutputHelper output) : base(output) { - } } diff --git a/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs b/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs index e6ed3d57b10..78064d39e00 100644 --- a/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs @@ -9,7 +9,6 @@ using Microsoft.Extensions.Logging; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Unit; @@ -30,8 +29,8 @@ public IDisposable BeginScope(TState state) { } } - public GhostStateDiagnosticCollectorTest(ITestOutputHelper output) { - var options = new DafnyOptions(TextReader.Null, new WriterFromOutputHelper(output), new WriterFromOutputHelper(output)); + public GhostStateDiagnosticCollectorTest() { + var options = new DafnyOptions(); options.Set(ServerCommand.GhostIndicators, true); ghostStateDiagnosticCollector = new GhostStateDiagnosticCollector( options, diff --git a/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs b/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs index 99b23a347af..45549e7cc00 100644 --- a/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs @@ -1,12 +1,11 @@ using System; using System.Collections.Generic; using Microsoft.Dafny.LanguageServer.Language; -using System.IO; +using System.Threading; using Microsoft.Extensions.Logging; using OmniSharp.Extensions.LanguageServer.Protocol; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Unit { @@ -17,9 +16,9 @@ public class ParserExceptionTest { private DafnyLangParser parser; private LastDebugLogger lastDebugLogger; - public ParserExceptionTest(ITestOutputHelper output) { + public ParserExceptionTest() { lastDebugLogger = new LastDebugLogger(); - parser = DafnyLangParser.Create(DafnyOptions.Create(new WriterFromOutputHelper(output)), lastDebugLogger); + parser = DafnyLangParser.Create(DafnyOptions.Create(), lastDebugLogger); } [Fact(Timeout = MaxTestExecutionTimeMs)] diff --git a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs index 67d4097e263..09e446c2d1e 100644 --- a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs @@ -4,18 +4,14 @@ using Moq; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System; -using System.IO; using System.Threading; using System.Threading.Tasks; using Microsoft.Extensions.Logging; using OmniSharp.Extensions.LanguageServer.Protocol; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Unit { public class TextDocumentLoaderTest { - private readonly TextWriter output; - private Mock parser; private Mock symbolResolver; private Mock symbolTableFactory; @@ -25,8 +21,7 @@ public class TextDocumentLoaderTest { private Mock logger; private Mock diagnosticPublisher; - public TextDocumentLoaderTest(ITestOutputHelper output) { - this.output = new WriterFromOutputHelper(output); + public TextDocumentLoaderTest() { parser = new(); symbolResolver = new(); symbolTableFactory = new(); @@ -35,7 +30,7 @@ public TextDocumentLoaderTest(ITestOutputHelper output) { logger = new Mock(); diagnosticPublisher = new Mock(); textDocumentLoader = TextDocumentLoader.Create( - DafnyOptions.Create(this.output, TextReader.Null), + DafnyOptions.Create(), parser.Object, symbolResolver.Object, symbolTableFactory.Object, diff --git a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs index 84cfae5a31e..17f894f43a7 100644 --- a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs +++ b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs @@ -12,7 +12,6 @@ using OmniSharp.Extensions.LanguageServer.Protocol.Client; using OmniSharp.Extensions.LanguageServer.Protocol.Document; using OmniSharp.Extensions.LanguageServer.Protocol.Models; -using Xunit.Abstractions; using Xunit; using XunitAssertMessages; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; @@ -189,7 +188,4 @@ public async Task PopNextStatus() { Assert.Equal(1, nextNotification.NamedVerifiables.Count); return nextNotification.NamedVerifiables.Single().Status; } - - public ClientBasedLanguageServerTest(ITestOutputHelper output) : base(output) { - } } diff --git a/Source/DafnyLanguageServer.Test/Util/MarkupTestFileTest.cs b/Source/DafnyLanguageServer.Test/Util/MarkupTestFileTest.cs index d0370b9518d..987746a5d8c 100644 --- a/Source/DafnyLanguageServer.Test/Util/MarkupTestFileTest.cs +++ b/Source/DafnyLanguageServer.Test/Util/MarkupTestFileTest.cs @@ -4,6 +4,7 @@ using Xunit; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Util; + public class MarkupTestFileTest { [Fact] public void AnnotatedSpan() { diff --git a/Source/DafnyLanguageServer.Test/Various/CancelVerificationTest.cs b/Source/DafnyLanguageServer.Test/Various/CancelVerificationTest.cs index fcb5527a26b..8ec9c69175b 100644 --- a/Source/DafnyLanguageServer.Test/Various/CancelVerificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/CancelVerificationTest.cs @@ -6,7 +6,6 @@ using Microsoft.Dafny.LanguageServer.Workspace; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; -using Xunit.Abstractions; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various { @@ -101,8 +100,5 @@ private async Task AssertNothingIsQueued(TextDocumentItem documentItem) { status = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); } } - - public CancelVerificationTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs b/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs index e451437e480..9be08a7ede7 100644 --- a/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs @@ -9,7 +9,6 @@ using JetBrains.Annotations; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various { [Collection("Sequential Collection")] // Sequential because we saw test failures after switching to parallel execution @@ -199,8 +198,5 @@ lemma Something(i: int) await AssertProgress(documentItem, CompilationStatus.ResolutionStarted); await AssertProgress(documentItem, CompilationStatus.ParsingFailed); } - - public CompilationStatusNotificationTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/Various/ConcurrentInteractionsTest.cs b/Source/DafnyLanguageServer.Test/Various/ConcurrentInteractionsTest.cs index 749ede2ee50..214f8ff4526 100644 --- a/Source/DafnyLanguageServer.Test/Various/ConcurrentInteractionsTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/ConcurrentInteractionsTest.cs @@ -9,7 +9,6 @@ using System.Threading; using System.Threading.Tasks; using Xunit; -using Xunit.Abstractions; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various { @@ -179,8 +178,5 @@ decreases y } await AssertNoDiagnosticsAreComing(CancellationTokenWithHighTimeout); } - - public ConcurrentInteractionsTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs b/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs index 87623d8ab90..05212317711 100644 --- a/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs @@ -9,7 +9,6 @@ using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Microsoft.Dafny.LanguageServer.Workspace; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various { static class StringAssert { @@ -1161,8 +1160,5 @@ public void TestIsNegativeIndexedSeq() { Assert.True( IsNegativeIndexedSeq(new KeyValuePair("seq>", "(Length := 1123, [(- 12345)] := @12)"))); } - - public CounterExampleTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs b/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs index f5a043bb4b3..9a43eaebda6 100644 --- a/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs @@ -6,7 +6,6 @@ using OmniSharp.Extensions.LanguageServer.Protocol.Document; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; @@ -159,7 +158,4 @@ public async Task VerificationDiagnosticsDoNotShowUpTwice() { Assert.Equal(verificationDiagnostics[0].Message, verificationDiagnostics2[0].Message); await AssertNoDiagnosticsAreComing(CancellationToken); } - - public DiagnosticMigrationTest(ITestOutputHelper output) : base(output) { - } } diff --git a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs index 021f7e6e0f6..f18d1caf969 100644 --- a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs +++ b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs @@ -12,7 +12,6 @@ using Microsoft.Extensions.Logging; using OmniSharp.Extensions.LanguageServer.Server; using Xunit; -using Xunit.Abstractions; using LanguageServerExtensions = Microsoft.Dafny.LanguageServer.Workspace.LanguageServerExtensions; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; @@ -132,7 +131,4 @@ public Task LoadAsync(DafnyOptions options, DocumentTextBu return loader.LoadAsync(options, textDocument, cancellationToken); } } - - public ExceptionTests(ITestOutputHelper output) : base(output) { - } } diff --git a/Source/DafnyLanguageServer.Test/Various/IncludeFileTest.cs b/Source/DafnyLanguageServer.Test/Various/IncludeFileTest.cs index 36c1753d747..f92d6d5a8cc 100644 --- a/Source/DafnyLanguageServer.Test/Various/IncludeFileTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/IncludeFileTest.cs @@ -4,7 +4,6 @@ using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; @@ -41,7 +40,4 @@ ensures Foo(x) {{ Assert.Single(verificationDiagnostics); await AssertNoDiagnosticsAreComing(CancellationToken); } - - public IncludeFileTest(ITestOutputHelper output) : base(output) { - } } diff --git a/Source/DafnyLanguageServer.Test/Various/MultiFileTest.cs b/Source/DafnyLanguageServer.Test/Various/MultiFileTest.cs index 5004cda00e3..2a6d5497be4 100644 --- a/Source/DafnyLanguageServer.Test/Various/MultiFileTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/MultiFileTest.cs @@ -3,7 +3,6 @@ using System.IO; using System.Linq; using System.Threading.Tasks; -using Xunit.Abstractions; using Xunit; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various { @@ -54,8 +53,5 @@ method Test() { Assert.NotNull(document); Assert.Single(document.Diagnostics); } - - public MultiFileTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs index c33c3fae451..58ad75e2e9e 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs @@ -2,7 +2,6 @@ using System.Threading.Tasks; using System.Threading; using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; -using Xunit.Abstractions; using Xunit; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; @@ -39,7 +38,4 @@ public async Task EnsureErrorMessageCanBeComplexAndTakeIntoAccountConfiguration( Assert.Equal(new Range((3, 15), (3, 32)), related.Current.Location.Range); related.Dispose(); } - - public PluginsAdvancedTest(ITestOutputHelper output) : base(output) { - } } diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsCodeActionTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsCodeActionTest.cs index 2fd10d008f3..4e69346ccd9 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsCodeActionTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsCodeActionTest.cs @@ -3,7 +3,6 @@ using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; using OmniSharp.Extensions.LanguageServer.Protocol.Document; using OmniSharp.Extensions.LanguageServer.Protocol.Models; -using Xunit.Abstractions; using Xunit; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; @@ -33,7 +32,4 @@ method firstMethod() { Assert.Equal("Insert file header", codeAction.Title); // The rest is tested elsewhere } - - public PluginsDafnyCodeActionTest(ITestOutputHelper output) : base(output) { - } } diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs index d2872ba5fba..ae80698d523 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs @@ -2,7 +2,6 @@ using System.Threading.Tasks; using System.Threading; using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; -using Xunit.Abstractions; using Xunit; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; @@ -28,7 +27,4 @@ public async Task EnsureItIsPossibleToLoadAPluginWithArguments() { Assert.Equal("Impossible to continue because\\ \"whatever", diagnostics[0].Message); Assert.Equal(new Range((0, 0), (0, 8)), diagnostics[0].Range); } - - public PluginsTest(ITestOutputHelper output) : base(output) { - } } diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs index ece6f55460c..a894feb7d46 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs @@ -7,7 +7,6 @@ using Microsoft.CodeAnalysis; using Microsoft.CodeAnalysis.CSharp; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; -using Xunit.Abstractions; using Xunit; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; @@ -74,7 +73,4 @@ void ModifyOptions(DafnyOptions options) { } return base.SetUp(ModifyOptions); } - - protected PluginsTestBase(ITestOutputHelper output) : base(output) { - } } diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTestWithVerification.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTestWithVerification.cs index e536d99ca5f..9ba519fa654 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTestWithVerification.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTestWithVerification.cs @@ -3,7 +3,6 @@ using System.Threading; using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; using Xunit; -using Xunit.Abstractions; using XunitAssertMessages; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; @@ -33,7 +32,4 @@ public async Task EnsureItIsPossibleToLoadAPluginAndContinueVerification() { Assert.Equal("value does not satisfy the subset constraints of 'nat'", diagnostics[1].Message); Assert.Equal(new Range((0, 23), (0, 24)), diagnostics[1].Range); } - - public PluginsTestWithVerification(ITestOutputHelper output) : base(output) { - } } diff --git a/Source/DafnyLanguageServer.Test/Various/ResourceUsageTest.cs b/Source/DafnyLanguageServer.Test/Various/ResourceUsageTest.cs index b91e02ae970..4cfddb97031 100644 --- a/Source/DafnyLanguageServer.Test/Various/ResourceUsageTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/ResourceUsageTest.cs @@ -4,7 +4,6 @@ using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; @@ -31,7 +30,4 @@ method Foo() var processes3 = Process.GetProcessesByName(solverProcessName); Assert.Equal(processes2.Length, processes3.Length); } - - public ResourceUsageTest(ITestOutputHelper output) : base(output) { - } } diff --git a/Source/DafnyLanguageServer.Test/Various/StabilityTest.cs b/Source/DafnyLanguageServer.Test/Various/StabilityTest.cs index bbef0eb8d29..027317dae35 100644 --- a/Source/DafnyLanguageServer.Test/Various/StabilityTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/StabilityTest.cs @@ -4,7 +4,6 @@ using System.IO; using System.Threading.Tasks; using Xunit; -using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various { /// @@ -58,8 +57,5 @@ method NestedExpression() { await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); Assert.NotNull(await Documents.GetResolvedDocumentAsync(documentItem.Uri)); } - - public StabilityTest(ITestOutputHelper output) : base(output) { - } } } diff --git a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs index 7bd953f0ef0..6c61023d9e7 100644 --- a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs +++ b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs @@ -916,14 +916,14 @@ private List GetFieldNames(Model.Element elt) { if (i == 0) { dimTuple = fIndexField.AppWithResult(elt); if (dimTuple == null) { - options.OutputWriter.WriteLine(PleaseEnableModelCompressFalse); + Console.Out.WriteLine(PleaseEnableModelCompressFalse); continue; } indices[i] = dimTuple.Args[0]; } else { dimTuple = fMultiIndexField.AppWithResult(elt); if (dimTuple == null) { - options.OutputWriter.WriteLine(PleaseEnableModelCompressFalse); + Console.Out.WriteLine(PleaseEnableModelCompressFalse); continue; } indices[i] = dimTuple.Args[1]; diff --git a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs index ff342e00ee2..f8478a4b732 100644 --- a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs +++ b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs @@ -140,7 +140,7 @@ private bool TryParseInclude(Include include, ModuleDecl module, BuiltIns builtI try { var dafnyFile = new DafnyFile(builtIns.Options, include.IncludedFilename); int errorCount = Parser.Parse( - (TextReader)null!, + useStdin: false, dafnyFile.Uri, module, builtIns, diff --git a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs index 375fa7b3021..cff182d2f23 100644 --- a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs +++ b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs @@ -37,6 +37,7 @@ DafnyOptions options } private const int TranslatorMaxStackSize = 0x10000000; // 256MB + static readonly ThreadTaskScheduler TranslatorScheduler = new(TranslatorMaxStackSize); public async Task> GetVerificationTasksAsync(DocumentAfterResolution document, CancellationToken cancellationToken) { @@ -45,10 +46,10 @@ public async Task> GetVerificationTasksAsync( cancellationToken.ThrowIfCancellationRequested(); - var translated = await DafnyMain.LargeStackFactory.StartNew(() => Translator.Translate(program, errorReporter, new Translator.TranslatorFlags(errorReporter.Options) { + var translated = await Task.Factory.StartNew(() => Translator.Translate(program, errorReporter, new Translator.TranslatorFlags(errorReporter.Options) { InsertChecksums = true, ReportRanges = true - }).ToList(), cancellationToken); + }).ToList(), cancellationToken, TaskCreationOptions.None, TranslatorScheduler); cancellationToken.ThrowIfCancellationRequested(); diff --git a/Source/DafnyLanguageServer/StandaloneServerCli.cs b/Source/DafnyLanguageServer/StandaloneServerCli.cs index b4895fd62ee..cd898823a0c 100644 --- a/Source/DafnyLanguageServer/StandaloneServerCli.cs +++ b/Source/DafnyLanguageServer/StandaloneServerCli.cs @@ -16,15 +16,15 @@ namespace Microsoft.Dafny.LanguageServer { public class Program { public static async Task Main(string[] args) { - var dafnyOptions = GetOptionsFromArgs(Console.Out, Console.In, args); + var dafnyOptions = GetOptionsFromArgs(args); await Server.Start(dafnyOptions); } - public static DafnyOptions GetOptionsFromArgs(TextWriter outWriter, TextReader input, string[] args) { + public static DafnyOptions GetOptionsFromArgs(string[] args) { var configuration = CreateConfiguration(args); - var dafnyOptions = DafnyOptions.Create(outWriter, input); + var dafnyOptions = DafnyOptions.Create(); var verifierOptions = new VerifierOptions(); configuration.Bind(VerifierOptions.Section, verifierOptions); diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index ee70d061f4e..5c0fe1e00e8 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -21,6 +21,7 @@ namespace Microsoft.Dafny.LanguageServer.Workspace { /// public class TextDocumentLoader : ITextDocumentLoader { private const int ResolverMaxStackSize = 0x10000000; // 256MB + private static readonly ThreadTaskScheduler ResolverScheduler = new(ResolverMaxStackSize); private readonly IDafnyParser parser; private readonly ISymbolResolver symbolResolver; @@ -74,10 +75,10 @@ public IdeState CreateUnloaded(DocumentTextBuffer textDocument, CancellationToke public async Task LoadAsync(DafnyOptions options, DocumentTextBuffer textDocument, CancellationToken cancellationToken) { #pragma warning disable CS1998 - return await await DafnyMain.LargeStackFactory.StartNew( - async () => LoadInternal(options, textDocument, cancellationToken), cancellationToken + return await await Task.Factory.StartNew( + async () => LoadInternal(options, textDocument, cancellationToken), cancellationToken, #pragma warning restore CS1998 - ); + TaskCreationOptions.None, ResolverScheduler); } private DocumentAfterParsing LoadInternal(DafnyOptions options, DocumentTextBuffer textDocument, diff --git a/Source/DafnyLanguageServer/Workspace/ThreadTaskScheduler.cs b/Source/DafnyLanguageServer/Workspace/ThreadTaskScheduler.cs new file mode 100644 index 00000000000..bf3c67e48fa --- /dev/null +++ b/Source/DafnyLanguageServer/Workspace/ThreadTaskScheduler.cs @@ -0,0 +1,42 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Threading; +using System.Threading.Tasks; + +namespace Microsoft.Dafny.LanguageServer.Workspace; + +/// +/// Each queued task runs on a newly-created thread with the required +/// stack size. The default .NET task scheduler is built on the .NET +/// ThreadPool. Its policy allows it to create thousands of threads +/// if it chooses. +/// +public class ThreadTaskScheduler : TaskScheduler { + private readonly int stackSize; + + public ThreadTaskScheduler(int stackSize) { + Contract.Requires(stackSize >= 0); + + this.stackSize = stackSize; + } + + protected override IEnumerable GetScheduledTasks() { + // There is never a queue of scheduled, but not running, tasks. + // So return an empty list. + return new List(); + } + + protected override void QueueTask(Task task) { + Thread th = new Thread(TaskMain!, stackSize); + th.Start(task); + } + + protected override bool TryExecuteTaskInline(Task task, bool taskWasPreviouslyQueued) { + return false; + } + + private void TaskMain(object data) { + Task t = (Task)data; + TryExecuteTask(t); + } +} \ No newline at end of file diff --git a/Source/DafnyPipeline.Test/DocstringTest.cs b/Source/DafnyPipeline.Test/DocstringTest.cs index e0ac3d71d56..ed05e0cd6ef 100644 --- a/Source/DafnyPipeline.Test/DocstringTest.cs +++ b/Source/DafnyPipeline.Test/DocstringTest.cs @@ -8,7 +8,6 @@ using BplParser = Microsoft.Boogie.Parser; using Microsoft.Dafny; using Xunit; -using Xunit.Abstractions; namespace DafnyPipeline.Test { @@ -21,18 +20,12 @@ namespace DafnyPipeline.Test { // Every test is performed with all three newline styles // Every formatted program is formatted again to verify that it stays the same. public class DocstringTest { - private readonly ITestOutputHelper output; - enum Newlines { LF, CR, CRLF }; - public DocstringTest(ITestOutputHelper output) { - this.output = output; - } - private Newlines currentNewlines; [Fact] @@ -426,7 +419,7 @@ protected void DocstringWorksFor(string source, string nodeTokenValue, string? e } protected void DocstringWorksFor(string source, List<(string nodeTokenValue, string? expectedDocstring)> tests) { - var options = DafnyOptions.Create(new WriterFromOutputHelper(output)); + var options = DafnyOptions.Create(); var newlineTypes = Enum.GetValues(typeof(Newlines)); foreach (Newlines newLinesType in newlineTypes) { currentNewlines = newLinesType; @@ -461,4 +454,4 @@ private string AdjustNewlines(string programString) { }; } } -} \ No newline at end of file +} diff --git a/Source/DafnyPipeline.Test/FormatterBaseTest.cs b/Source/DafnyPipeline.Test/FormatterBaseTest.cs index aab142263fd..e93d7ecfa49 100644 --- a/Source/DafnyPipeline.Test/FormatterBaseTest.cs +++ b/Source/DafnyPipeline.Test/FormatterBaseTest.cs @@ -1,14 +1,18 @@ #nullable enable using System; +using System.Collections; using System.Collections.Generic; +using System.Linq; +using System.Diagnostics.Contracts; using System.IO; using System.Text.RegularExpressions; using DafnyTestGeneration; +using JetBrains.Annotations; using Bpl = Microsoft.Boogie; using BplParser = Microsoft.Boogie.Parser; using Microsoft.Dafny; using Xunit; -using Xunit.Abstractions; +using Main = Microsoft.Dafny.Main; namespace DafnyPipeline.Test { @@ -21,12 +25,6 @@ namespace DafnyPipeline.Test { // Every test is performed with all three newline styles // Every formatted program is formatted again to verify that it stays the same. public class FormatterBaseTest { - private readonly TextWriter output; - - public FormatterBaseTest(ITestOutputHelper output) { - this.output = new WriterFromOutputHelper(output); - } - enum Newlines { LF, CR, @@ -41,7 +39,7 @@ enum Newlines { protected void FormatterWorksFor(string testCase, string? expectedProgramString = null, bool expectNoToken = false, bool reduceBlockiness = true) { - var options = DafnyOptions.Create(output); + var options = DafnyOptions.Create(); var newlineTypes = Enum.GetValues(typeof(Newlines)); foreach (Newlines newLinesType in newlineTypes) { currentNewlines = newLinesType; @@ -83,13 +81,13 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString } // Formatting should work after resolution as well. - DafnyMain.Resolve(dafnyProgram); + Main.Resolve(dafnyProgram); reprinted = firstToken != null && firstToken.line > 0 ? Formatting.__default.ReindentProgramFromFirstToken(firstToken, IndentationFormatter.ForProgram(dafnyProgram, reduceBlockiness)) : programString; if (expectedProgram != reprinted) { - options.ErrorWriter.WriteLine("Formatting after resolution generates an error:"); + Console.Error.WriteLine("Formatting after resolution generates an error:"); Assert.Equal(expectedProgram, reprinted); } var initErrorCount = reporter.ErrorCount; diff --git a/Source/DafnyPipeline.Test/FormatterComprehensions.cs b/Source/DafnyPipeline.Test/FormatterComprehensions.cs index 1795182fad9..0e5108c9734 100644 --- a/Source/DafnyPipeline.Test/FormatterComprehensions.cs +++ b/Source/DafnyPipeline.Test/FormatterComprehensions.cs @@ -1,6 +1,4 @@ -using JetBrains.Annotations; -using Xunit; -using Xunit.Abstractions; +using Xunit; namespace DafnyPipeline.Test; @@ -210,6 +208,4 @@ function test(): int { } - public FormatterForComprehensions([NotNull] ITestOutputHelper output) : base(output) { - } -} +} \ No newline at end of file diff --git a/Source/DafnyPipeline.Test/FormatterForApplySuffixRelated.cs b/Source/DafnyPipeline.Test/FormatterForApplySuffixRelated.cs index dc47cd7e198..5839cde9692 100644 --- a/Source/DafnyPipeline.Test/FormatterForApplySuffixRelated.cs +++ b/Source/DafnyPipeline.Test/FormatterForApplySuffixRelated.cs @@ -1,6 +1,4 @@ -using JetBrains.Annotations; -using Xunit; -using Xunit.Abstractions; +using Xunit; namespace DafnyPipeline.Test; @@ -42,7 +40,4 @@ method Test() } "); } - - public FormatterForApplySuffixRelated([NotNull] ITestOutputHelper output) : base(output) { - } -} +} \ No newline at end of file diff --git a/Source/DafnyPipeline.Test/FormatterForAssignments.cs b/Source/DafnyPipeline.Test/FormatterForAssignments.cs index 25b53785b59..57a2d3ffe91 100644 --- a/Source/DafnyPipeline.Test/FormatterForAssignments.cs +++ b/Source/DafnyPipeline.Test/FormatterForAssignments.cs @@ -1,6 +1,4 @@ -using JetBrains.Annotations; -using Xunit; -using Xunit.Abstractions; +using Xunit; namespace DafnyPipeline.Test; @@ -181,7 +179,4 @@ method Test() { } ", reduceBlockiness: false); } - - public FormatterForAssignments([NotNull] ITestOutputHelper output) : base(output) { - } -} +} \ No newline at end of file diff --git a/Source/DafnyPipeline.Test/FormatterForCalcStmt.cs b/Source/DafnyPipeline.Test/FormatterForCalcStmt.cs index 16b74ec76d4..fb2b320a1b0 100644 --- a/Source/DafnyPipeline.Test/FormatterForCalcStmt.cs +++ b/Source/DafnyPipeline.Test/FormatterForCalcStmt.cs @@ -1,6 +1,4 @@ -using JetBrains.Annotations; -using Xunit; -using Xunit.Abstractions; +using Xunit; namespace DafnyPipeline.Test; @@ -29,7 +27,4 @@ assert true by { } "); } - - public FormatterForCalcStmt([NotNull] ITestOutputHelper output) : base(output) { - } -} +} \ No newline at end of file diff --git a/Source/DafnyPipeline.Test/FormatterForComments.cs b/Source/DafnyPipeline.Test/FormatterForComments.cs index b346ba1ba4d..2aba9ca3b10 100644 --- a/Source/DafnyPipeline.Test/FormatterForComments.cs +++ b/Source/DafnyPipeline.Test/FormatterForComments.cs @@ -1,6 +1,4 @@ -using JetBrains.Annotations; -using Xunit; -using Xunit.Abstractions; +using Xunit; namespace DafnyPipeline.Test; @@ -271,6 +269,4 @@ public void FormatterWorksForUtf8InComment() { "); } - public FormatterForComments([NotNull] ITestOutputHelper output) : base(output) { - } -} +} \ No newline at end of file diff --git a/Source/DafnyPipeline.Test/FormatterForDatatypeDeclarationTest.cs b/Source/DafnyPipeline.Test/FormatterForDatatypeDeclarationTest.cs index aa9ca091f33..2f3f37ae060 100644 --- a/Source/DafnyPipeline.Test/FormatterForDatatypeDeclarationTest.cs +++ b/Source/DafnyPipeline.Test/FormatterForDatatypeDeclarationTest.cs @@ -1,6 +1,4 @@ -using JetBrains.Annotations; -using Xunit; -using Xunit.Abstractions; +using Xunit; namespace DafnyPipeline.Test; @@ -146,6 +144,4 @@ public void FormatterWorksForSingleDatatypeConstructor() { ", reduceBlockiness: false); } - public FormatterForDatatypeDeclarationTest([NotNull] ITestOutputHelper output) : base(output) { - } -} +} \ No newline at end of file diff --git a/Source/DafnyPipeline.Test/FormatterForExpressions.cs b/Source/DafnyPipeline.Test/FormatterForExpressions.cs index 380062015cc..22973b02c56 100644 --- a/Source/DafnyPipeline.Test/FormatterForExpressions.cs +++ b/Source/DafnyPipeline.Test/FormatterForExpressions.cs @@ -1,6 +1,4 @@ -using JetBrains.Annotations; -using Xunit; -using Xunit.Abstractions; +using Xunit; namespace DafnyPipeline.Test; @@ -379,6 +377,4 @@ predicate Valid() FormatterWorksFor(testCase, testCase); } - public FormatterForExpressions([NotNull] ITestOutputHelper output) : base(output) { - } -} +} \ No newline at end of file diff --git a/Source/DafnyPipeline.Test/FormatterForMembers.cs b/Source/DafnyPipeline.Test/FormatterForMembers.cs index 7caa40515a3..1a0c260d39b 100644 --- a/Source/DafnyPipeline.Test/FormatterForMembers.cs +++ b/Source/DafnyPipeline.Test/FormatterForMembers.cs @@ -1,6 +1,4 @@ -using JetBrains.Annotations; -using Xunit; -using Xunit.Abstractions; +using Xunit; namespace DafnyPipeline.Test; @@ -264,6 +262,6 @@ method Main() { } - public FormatterForMembers([NotNull] ITestOutputHelper output) : base(output) { - } -} + + +} \ No newline at end of file diff --git a/Source/DafnyPipeline.Test/FormatterForSpecifications.cs b/Source/DafnyPipeline.Test/FormatterForSpecifications.cs index 91037888f1a..e715870ba40 100644 --- a/Source/DafnyPipeline.Test/FormatterForSpecifications.cs +++ b/Source/DafnyPipeline.Test/FormatterForSpecifications.cs @@ -1,6 +1,4 @@ -using JetBrains.Annotations; -using Xunit; -using Xunit.Abstractions; +using Xunit; namespace DafnyPipeline.Test; @@ -270,6 +268,4 @@ class TestClass { } - public FormatterForSpecifications([NotNull] ITestOutputHelper output) : base(output) { - } -} +} \ No newline at end of file diff --git a/Source/DafnyPipeline.Test/FormatterForStatements.cs b/Source/DafnyPipeline.Test/FormatterForStatements.cs index c04ea0500d8..9f1ef494b8f 100644 --- a/Source/DafnyPipeline.Test/FormatterForStatements.cs +++ b/Source/DafnyPipeline.Test/FormatterForStatements.cs @@ -1,6 +1,4 @@ -using JetBrains.Annotations; -using Xunit; -using Xunit.Abstractions; +using Xunit; namespace DafnyPipeline.Test; @@ -434,7 +432,4 @@ method Test() { "; FormatterWorksFor(test, test); } - - public FormatterForStatements([NotNull] ITestOutputHelper output) : base(output) { - } -} +} \ No newline at end of file diff --git a/Source/DafnyPipeline.Test/FormatterForTopLevelDeclarations.cs b/Source/DafnyPipeline.Test/FormatterForTopLevelDeclarations.cs index d5429cfed98..b0c423b0f91 100644 --- a/Source/DafnyPipeline.Test/FormatterForTopLevelDeclarations.cs +++ b/Source/DafnyPipeline.Test/FormatterForTopLevelDeclarations.cs @@ -1,6 +1,4 @@ -using JetBrains.Annotations; -using Xunit; -using Xunit.Abstractions; +using Xunit; namespace DafnyPipeline.Test; @@ -348,7 +346,4 @@ method M... } "); } - - public FormatterForTopLevelDeclarations([NotNull] ITestOutputHelper output) : base(output) { - } -} +} \ No newline at end of file diff --git a/Source/DafnyPipeline.Test/FormatterIssues.cs b/Source/DafnyPipeline.Test/FormatterIssues.cs index 73549f96ec2..41c2a2489c9 100644 --- a/Source/DafnyPipeline.Test/FormatterIssues.cs +++ b/Source/DafnyPipeline.Test/FormatterIssues.cs @@ -1,6 +1,4 @@ -using JetBrains.Annotations; -using Xunit; -using Xunit.Abstractions; +using Xunit; namespace DafnyPipeline.Test; @@ -129,7 +127,4 @@ public void FormatterWorksForEmptyDocument() { FormatterWorksFor(@" ", null, true); } - - public FormatterIssues([NotNull] ITestOutputHelper output) : base(output) { - } } diff --git a/Source/DafnyPipeline.Test/InterMethodVerificationStability.cs b/Source/DafnyPipeline.Test/InterMethodVerificationStability.cs index 0298cee3ede..bbd357c5a2f 100644 --- a/Source/DafnyPipeline.Test/InterMethodVerificationStability.cs +++ b/Source/DafnyPipeline.Test/InterMethodVerificationStability.cs @@ -8,15 +8,12 @@ using DiffPlex.DiffBuilder.Model; using Microsoft.VisualStudio.TestPlatform.PlatformAbstractions; using Xunit; -using Xunit.Abstractions; namespace DafnyPipeline.Test { // Main.Resolve has static shared state (TypeConstraint.ErrorsToBeReported for example) // so we can't execute tests that use it in parallel. [Collection("Singleton Test Collection - Resolution")] public class InterMethodVerificationStability { - private readonly ITestOutputHelper output; - [Fact] public void CreatingBoogieVariableNameCollisionsHasExpectedDiff() { var beforeChange = @" @@ -186,10 +183,6 @@ static InterMethodVerificationStability() { private static readonly string dafnyDirectory; - public InterMethodVerificationStability(ITestOutputHelper output) { - this.output = output; - } - private static string DafnyProjectFile => Path.Combine(dafnyDirectory, "Source", "Dafny", "Dafny.csproj"); private static string DefaultDafnyArgs => $"run --no-build --project {DafnyProjectFile} -- -useBaseNameForFileName -compileVerbose:0 /errorTrace:0"; @@ -208,10 +201,11 @@ string GetBoogie(string dafnyProgram, string optionalFileName = null) { dafnyProcess.WaitForExit(); if (dafnyProcess.ExitCode != 0) { - output.WriteLine("Arguments:", processStartInfo.Arguments); - output.WriteLine("Result:"); - output.WriteLine(result); - output.WriteLine(dafnyProcess.StandardError.ReadToEnd()); + Console.Out.WriteLine("Arguments:", processStartInfo.Arguments); + Console.Out.WriteLine("Result:"); + Console.Out.WriteLine(result); + Console.Out.WriteLine(dafnyProcess.StandardError.ReadToEnd()); + Console.Out.Flush(); } Assert.Equal(4, dafnyProcess.ExitCode); return result; diff --git a/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs b/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs index 3d5fd272f72..556183c4f0a 100644 --- a/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs +++ b/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs @@ -1,6 +1,8 @@ +using System; using System.Collections.Generic; using System.IO; using System.Linq; +using System.Threading; using System.Threading.Tasks; using DafnyTestGeneration; using Microsoft.Boogie; @@ -8,13 +10,14 @@ using Xunit; using Xunit.Abstractions; using BoogieProgram = Microsoft.Boogie.Program; +using Main = Microsoft.Dafny.Main; +using Parser = Microsoft.Dafny.Parser; namespace DafnyPipeline.Test { // Main.Resolve has static shared state (TypeConstraint.ErrorsToBeReported for example) // so we can't execute tests that use it in parallel. [Collection("Singleton Test Collection - Resolution")] public class IntraMethodVerificationStability { - private readonly ITestOutputHelper testOutputHelper; // All types of top level declarations. @@ -148,7 +151,7 @@ public IntraMethodVerificationStability(ITestOutputHelper testOutputHelper) { [Fact] public void NoUniqueLinesWhenConcatenatingUnrelatedPrograms() { - var options = DafnyOptions.Create(new WriterFromOutputHelper(testOutputHelper)); + var options = DafnyOptions.Create(); var regularBoogie = GetBoogie(options, originalProgram).ToList(); var renamedBoogie = GetBoogie(options, renamedProgram).ToList(); @@ -164,7 +167,7 @@ public void NoUniqueLinesWhenConcatenatingUnrelatedPrograms() { [Fact] public async Task EqualProverLogWhenReorderingProgram() { - var options = DafnyOptions.Create(new WriterFromOutputHelper(testOutputHelper)); + var options = DafnyOptions.Create(); options.ProcsToCheck.Add("SomeMethod*"); var reorderedProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, reorderedProgram)); @@ -174,7 +177,7 @@ public async Task EqualProverLogWhenReorderingProgram() { [Fact] public async Task EqualProverLogWhenRenamingProgram() { - var options = DafnyOptions.Create(new WriterFromOutputHelper(testOutputHelper)); + var options = DafnyOptions.Create(); options.ProcsToCheck.Add("*SomeMethod*"); var renamedProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, renamedProgram)); @@ -185,7 +188,7 @@ public async Task EqualProverLogWhenRenamingProgram() { [Fact] public async Task EqualProverLogWhenAddingUnrelatedProgram() { - var options = DafnyOptions.Create(new WriterFromOutputHelper(testOutputHelper)); + var options = DafnyOptions.Create(); options.ProcsToCheck.Add("*SomeMethod *"); var renamedProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, renamedProgram + originalProgram)); @@ -208,7 +211,7 @@ private async IAsyncEnumerable GetProverLogsForProgramAsync(DafnyOptions options.ProverLogFilePath = temp1; using (var engine = ExecutionEngine.CreateWithoutSharedCache(options)) { foreach (var boogieProgram in boogiePrograms) { - var (outcome, _) = await DafnyMain.BoogieOnce(options, options.OutputWriter, engine, "", "", boogieProgram, "programId"); + var (outcome, _) = await Main.BoogieOnce(options, Console.Out, engine, "", "", boogieProgram, "programId"); testOutputHelper.WriteLine("outcome: " + outcome); } } @@ -236,7 +239,7 @@ IEnumerable GetBoogie(DafnyOptions options, string dafnyProgramTe var dafnyProgram = Utils.Parse(options, dafnyProgramText, false); BatchErrorReporter reporter = (BatchErrorReporter)dafnyProgram.Reporter; Assert.NotNull(dafnyProgram); - DafnyMain.Resolve(dafnyProgram); + Main.Resolve(dafnyProgram); Assert.Equal(0, reporter.ErrorCount); return Translator.Translate(dafnyProgram, reporter).Select(t => t.Item2).ToList(); } diff --git a/Source/DafnyPipeline.Test/Issue1355.cs b/Source/DafnyPipeline.Test/Issue1355.cs index 8ac93cd5c8e..84dae7e1560 100644 --- a/Source/DafnyPipeline.Test/Issue1355.cs +++ b/Source/DafnyPipeline.Test/Issue1355.cs @@ -1,30 +1,28 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Diagnostics.Contracts; using System.IO; using DafnyTestGeneration; using Bpl = Microsoft.Boogie; using BplParser = Microsoft.Boogie.Parser; using Microsoft.Dafny; using Xunit; -using Xunit.Abstractions; +using Main = Microsoft.Dafny.Main; namespace DafnyPipeline.Test { // Main.Resolve has static shared state (TypeConstraint.ErrorsToBeReported for example) // so we can't execute tests that use it in parallel. [Collection("Singleton Test Collection - Resolution")] public class Issue1355 { - private readonly TextWriter output; - - public Issue1355(ITestOutputHelper output) { - this.output = new WriterFromOutputHelper(output); - } - [Fact] public void Test() { - var options = DafnyOptions.Create(output); + var options = DafnyOptions.Create(); options.DafnyPrelude = "../../../../../Binaries/DafnyPrelude.bpl"; var programString = @"trait Trait { }"; var dafnyProgram = Utils.Parse(options, programString, false); - DafnyMain.Resolve(dafnyProgram); + Main.Resolve(dafnyProgram); foreach (var prog in Translator.Translate(dafnyProgram, dafnyProgram.Reporter)) { var writer = new StringWriter(); var tokenWriter = new Bpl.TokenTextWriter("virtual", writer, true, options); diff --git a/Source/DafnyPipeline.Test/PluginsTest.cs b/Source/DafnyPipeline.Test/PluginsTest.cs index f324fd8362d..bdc421ef811 100644 --- a/Source/DafnyPipeline.Test/PluginsTest.cs +++ b/Source/DafnyPipeline.Test/PluginsTest.cs @@ -7,18 +7,12 @@ using Microsoft.CodeAnalysis.CSharp; using Xunit; using Microsoft.Dafny; -using Xunit.Abstractions; +using Main = Microsoft.Dafny.Main; namespace DafnyPipeline.Test; [Collection("Dafny plug-ins tests")] public class PluginsTest { - private readonly TextWriter output; - - public PluginsTest(ITestOutputHelper output) { - this.output = new WriterFromOutputHelper(output); - } - /// /// This method creates a library and returns the path to that library. /// The library extends a Rewriter so that we can verify that Dafny invokes it if provided in argument. @@ -57,13 +51,13 @@ private string GetLibrary(string name) { public void EnsurePluginIsExecuted() { var library = GetLibrary("rewriterPreventingVerificationWithArgument"); - var options = DafnyOptions.Create(output); + var options = DafnyOptions.Create(); options.Plugins.Add(AssemblyPlugin.Load(library, new string[] { "because whatever" })); var programString = "function test(): int { 1 }"; var dafnyProgram = Utils.Parse(options, programString, false); BatchErrorReporter reporter = (BatchErrorReporter)dafnyProgram.Reporter; - DafnyMain.Resolve(dafnyProgram); + Main.Resolve(dafnyProgram); Assert.Equal(1, reporter.Count(ErrorLevel.Error)); Assert.Equal("Impossible to continue because whatever", reporter.AllMessages[ErrorLevel.Error][0].Message); @@ -73,13 +67,13 @@ public void EnsurePluginIsExecuted() { public void EnsurePluginIsExecutedEvenWithoutConfiguration() { var library = GetLibrary("rewriterPreventingVerification"); - var options = DafnyOptions.Create(output); + var options = DafnyOptions.Create(); options.Plugins.Add(AssemblyPlugin.Load(library, new string[] { "ignored arguments" })); var programString = "function test(): int { 1 }"; var dafnyProgram = Utils.Parse(options, programString, false); BatchErrorReporter reporter = (BatchErrorReporter)dafnyProgram.Reporter; - DafnyMain.Resolve(dafnyProgram); + Main.Resolve(dafnyProgram); Assert.Equal(1, reporter.ErrorCount); Assert.Equal("Impossible to continue", reporter.AllMessages[ErrorLevel.Error][0].Message); } @@ -88,13 +82,13 @@ public void EnsurePluginIsExecutedEvenWithoutConfiguration() { public void EnsurePluginIsExecutedAndAllowsVerification() { var library = GetLibrary("rewriterAllowingVerification"); - var options = DafnyOptions.Create(output); + var options = DafnyOptions.Create(); options.Plugins.Add(AssemblyPlugin.Load(library, new string[] { "ignored arguments" })); var programString = "function test(): int { 1 }"; var dafnyProgram = Utils.Parse(options, programString, false); BatchErrorReporter reporter = (BatchErrorReporter)dafnyProgram.Reporter; - DafnyMain.Resolve(dafnyProgram); + Main.Resolve(dafnyProgram); Assert.Equal(0, reporter.ErrorCountUntilResolver); Assert.Equal(1, reporter.ErrorCount); } diff --git a/Source/DafnyPipeline.Test/RelativePaths.cs b/Source/DafnyPipeline.Test/RelativePaths.cs index 4d71cc07d1d..2bd258f6ce1 100644 --- a/Source/DafnyPipeline.Test/RelativePaths.cs +++ b/Source/DafnyPipeline.Test/RelativePaths.cs @@ -1,22 +1,14 @@ using System.IO; using Microsoft.Dafny; using Xunit; -using Xunit.Abstractions; namespace DafnyPipeline.Test { [Collection("Singleton Test Collection - Resolution")] public class RelativePaths { - private readonly TextWriter output; - - public RelativePaths(ITestOutputHelper output) { - this.output = new WriterFromOutputHelper(output); - } - [Fact] public void Test() { - Assert.Equal(0, DafnyDriver.MainWithWriters(output, output, - TextReader.Null, new[] { "/spillTargetCode:3", "warnings-as-errors.dfy" })); + Assert.Equal(0, DafnyDriver.ThreadMain(new string[] { "/spillTargetCode:3", "warnings-as-errors.dfy" })); } [Fact] diff --git a/Source/DafnyPipeline.Test/TranslatorTest.cs b/Source/DafnyPipeline.Test/TranslatorTest.cs index 93e6190a14c..f56f823039b 100644 --- a/Source/DafnyPipeline.Test/TranslatorTest.cs +++ b/Source/DafnyPipeline.Test/TranslatorTest.cs @@ -1,7 +1,9 @@ using System; using System.Collections.Generic; +using System.Diagnostics; using System.IO; using System.Linq; +using Microsoft.CodeAnalysis; using Bpl = Microsoft.Boogie; using Xunit; using Microsoft.Dafny; @@ -73,7 +75,7 @@ private void ShouldHaveImplicitCode(string program, string expected, DafnyOption } var expectedLine = program.Split("// Here")[0].Count(c => c == '\n') + 1; Microsoft.Dafny.Type.ResetScopes(); - options = options ?? new DafnyOptions(TextReader.Null, TextWriter.Null, TextWriter.Null); + options = options ?? new DafnyOptions(); var uri = new Uri("virtual:///virtual"); var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }); var module = new LiteralModuleDecl(defaultModuleDefinition, null); @@ -85,7 +87,7 @@ private void ShouldHaveImplicitCode(string program, string expected, DafnyOption var error = reporter.AllMessages[ErrorLevel.Error][0]; Assert.False(true, $"{error.Message}: line {error.Token.line} col {error.Token.col}"); } - DafnyMain.Resolve(dafnyProgram); + Main.Resolve(dafnyProgram); if (reporter.ErrorCount > 0) { var error = reporter.AllMessages[ErrorLevel.Error][0]; Assert.False(true, $"{error.Message}: line {error.Token.line} col {error.Token.col}"); diff --git a/Source/DafnyPipeline.Test/Trivia.cs b/Source/DafnyPipeline.Test/Trivia.cs index d67c093591b..3e92e11f53e 100644 --- a/Source/DafnyPipeline.Test/Trivia.cs +++ b/Source/DafnyPipeline.Test/Trivia.cs @@ -1,5 +1,7 @@ using System; using System.Collections.Generic; +using System.Linq; +using System.Diagnostics.Contracts; using System.IO; using System.Text.RegularExpressions; using DafnyTestGeneration; @@ -7,25 +9,17 @@ using BplParser = Microsoft.Boogie.Parser; using Microsoft.Dafny; using Xunit; -using Xunit.Abstractions; namespace DafnyPipeline.Test { [Collection("Singleton Test Collection - Trivia")] public class Trivia { - - private readonly TextWriter output; - - public Trivia(ITestOutputHelper output) { - this.output = new WriterFromOutputHelper(output); - } - enum Newlines { LF, CR, CRLF }; private Newlines currentNewlines; [Fact] public void TriviaSplitWorksOnLinuxMacAndWindows() { - var options = DafnyOptions.Create(output); + var options = DafnyOptions.Create(); foreach (Newlines newLinesType in Enum.GetValues(typeof(Newlines))) { currentNewlines = newLinesType; var programString = @" diff --git a/Source/DafnyPipeline.Test/WriterFromOutputHelper.cs b/Source/DafnyPipeline.Test/WriterFromOutputHelper.cs deleted file mode 100644 index c8159df29ef..00000000000 --- a/Source/DafnyPipeline.Test/WriterFromOutputHelper.cs +++ /dev/null @@ -1,30 +0,0 @@ -#nullable enable -using System.IO; -using System.Text; -using Xunit.Abstractions; - -public class WriterFromOutputHelper : TextWriter { - private readonly ITestOutputHelper output; - private bool failed = false; - - public WriterFromOutputHelper(ITestOutputHelper output) { - this.output = output; - } - - public override void Write(char value) { - if (!failed) { - failed = true; - WriteLine("Error: tried to write a single character, which WriterFromOutputHelper does not support."); - } - } - - public override Encoding Encoding => Encoding.Default; - - public override void WriteLine(string? value) { - output.WriteLine(value); - } - - public override void WriteLine(string format, params object?[] arg) { - output.WriteLine(format, arg); - } -} \ No newline at end of file diff --git a/Source/DafnyServer/CounterExampleProvider.cs b/Source/DafnyServer/CounterExampleProvider.cs index 2547adb2097..ca135d26e9d 100644 --- a/Source/DafnyServer/CounterExampleProvider.cs +++ b/Source/DafnyServer/CounterExampleProvider.cs @@ -12,13 +12,9 @@ using Microsoft.Dafny; namespace DafnyServer { - public sealed class CounterExampleProvider { + public class CounterExampleProvider { private const int maximumCounterexampleDepth = 5; - public readonly string ModelBvd; - - public CounterExampleProvider() { - ModelBvd = $"./model{GetHashCode()}.bvd"; - } + public const string ModelBvd = "./model.bvd"; public CounterExample LoadCounterModel(DafnyOptions options) { try { @@ -29,7 +25,7 @@ public CounterExample LoadCounterModel(DafnyOptions options) { } } - private List LoadModelFromFile(DafnyOptions options) { + private static List LoadModelFromFile(DafnyOptions options) { using var wr = new StreamReader(ModelBvd); var output = wr.ReadToEnd(); var models = ExtractModels(output); diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index 51ddc093398..013f0214eca 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -23,7 +23,6 @@ class DafnyHelper { private ErrorReporter reporter; private Program dafnyProgram; private IEnumerable> boogiePrograms; - private readonly CounterExampleProvider counterExampleProvider = new(); public DafnyHelper(DafnyOptions options, ExecutionEngine engine, string[] args, string fname, string source) { this.options = options; @@ -45,7 +44,7 @@ private bool Parse() { reporter = new ConsoleErrorReporter(options, defaultModuleDefinition); BuiltIns builtIns = new BuiltIns(options); var success = (Parser.Parse(source, uri, module, builtIns, new Errors(reporter)) == 0 && - DafnyMain.ParseIncludesDepthFirstNotCompiledFirst(Console.In, module, builtIns, new HashSet(), new Errors(reporter)) == null); + Main.ParseIncludesDepthFirstNotCompiledFirst(module, builtIns, new HashSet(), new Errors(reporter)) == null); if (success) { dafnyProgram = new Program(fname, module, builtIns, reporter); } @@ -72,7 +71,7 @@ private bool BoogieOnce(string moduleName, Bpl.Program boogieProgram) { engine.Inline(boogieProgram); //NOTE: We could capture errors instead of printing them (pass a delegate instead of null) - switch (engine.InferAndVerify(options.OutputWriter, boogieProgram, new PipelineStatistics(), + switch (engine.InferAndVerify(Console.Out, boogieProgram, new PipelineStatistics(), #pragma warning disable VSTHRD002 "ServerProgram_" + moduleName, null, DateTime.UtcNow.Ticks.ToString()).Result) { #pragma warning restore VSTHRD002 @@ -106,10 +105,11 @@ public void Symbols() { public void CounterExample() { var listArgs = args.ToList(); - listArgs.Add("/mv:" + counterExampleProvider.ModelBvd); + listArgs.Add("/mv:" + CounterExampleProvider.ModelBvd); ServerUtils.ApplyArgs(listArgs.ToArray(), options); try { if (Parse() && Resolve() && Translate()) { + var counterExampleProvider = new CounterExampleProvider(); foreach (var boogieProgram in boogiePrograms) { RemoveExistingModel(); BoogieOnce(boogieProgram.Item1, boogieProgram.Item2); @@ -123,8 +123,8 @@ public void CounterExample() { } private void RemoveExistingModel() { - if (File.Exists(counterExampleProvider.ModelBvd)) { - File.Delete(counterExampleProvider.ModelBvd); + if (File.Exists(CounterExampleProvider.ModelBvd)) { + File.Delete(CounterExampleProvider.ModelBvd); } } diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index fa19359990f..07dd05391d7 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -13,7 +13,7 @@ public class Server { private readonly ExecutionEngine engine; public static void Main(string[] args) { - var options = DafnyOptions.Create(Console.Out); + var options = DafnyOptions.Create(); ServerUtils.ApplyArgs(args, options); var engine = ExecutionEngine.CreateWithoutSharedCache(options); Server server = new Server(engine); @@ -231,4 +231,4 @@ void Exit() { } } -} +} \ No newline at end of file diff --git a/Source/DafnyTestGeneration.Test/BasicTypes.cs b/Source/DafnyTestGeneration.Test/BasicTypes.cs index fb0c12e5184..b0babd2db0d 100644 --- a/Source/DafnyTestGeneration.Test/BasicTypes.cs +++ b/Source/DafnyTestGeneration.Test/BasicTypes.cs @@ -1,18 +1,12 @@ -using System.IO; using System.Linq; using System.Text.RegularExpressions; using System.Threading.Tasks; using Microsoft.Dafny; using Xunit; -using Xunit.Abstractions; namespace DafnyTestGeneration.Test { - public class BasicTypes { - private readonly TextWriter output; - public BasicTypes(ITestOutputHelper output) { - this.output = new WriterFromOutputHelper(output); - } + public class BasicTypes { [Fact] public async Task Ints() { @@ -28,7 +22,7 @@ method compareToZero(i: int) returns (ret: int) { } } ".TrimStart(); - var options = Setup.GetDafnyOptions(output); + var options = Setup.GetDafnyOptions(); var program = Utils.Parse(options, source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Equal(3, methods.Count); @@ -57,7 +51,7 @@ method checkIfTrue(b: bool) returns (ret: bool) { } } ".TrimStart(); - var program = Utils.Parse(Setup.GetDafnyOptions(output), source); + var program = Utils.Parse(Setup.GetDafnyOptions(), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Equal(2, methods.Count); Assert.True(methods.All(m => m.MethodName == "SimpleTest.checkIfTrue")); @@ -91,7 +85,7 @@ method compareToZero(r: real) returns (ret: int) { } } ".TrimStart(); - var program = Utils.Parse(Setup.GetDafnyOptions(output), source); + var program = Utils.Parse(Setup.GetDafnyOptions(), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Equal(7, methods.Count); Assert.True( @@ -124,7 +118,7 @@ method compareToBase(r: bv10) returns (ret: int) { } } ".TrimStart(); - var program = Utils.Parse(DafnyOptions.Create(output), source); + var program = Utils.Parse(DafnyOptions.Create(), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Equal(3, methods.Count); Assert.True( @@ -155,7 +149,7 @@ method compareToB(c: char) returns (ret: int) { } } ".TrimStart(); - var program = Utils.Parse(Setup.GetDafnyOptions(output), source); + var program = Utils.Parse(Setup.GetDafnyOptions(), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Equal(3, methods.Count); Assert.True(methods.All(m => m.MethodName == "SimpleTest.compareToB")); @@ -186,7 +180,7 @@ method compareToB(c: char) returns (b:bool) { } } ".TrimStart(); - var program = Utils.Parse(Setup.GetDafnyOptions(output), source); + var program = Utils.Parse(Setup.GetDafnyOptions(), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Equal(2, methods.Count); Assert.True(methods.All(m => m.MethodName == "SimpleTest.compareToB")); diff --git a/Source/DafnyTestGeneration.Test/Collections.cs b/Source/DafnyTestGeneration.Test/Collections.cs index d00130ec6a4..f0a3f8e8993 100644 --- a/Source/DafnyTestGeneration.Test/Collections.cs +++ b/Source/DafnyTestGeneration.Test/Collections.cs @@ -1,3 +1,4 @@ +using System; using System.Linq; using System.Text.RegularExpressions; using System.Threading.Tasks; @@ -29,7 +30,7 @@ method compareStringLengthToOne(s: string) returns (ret: int) { } ".TrimStart(); - var program = Utils.Parse(Setup.GetDafnyOptions(new WriterFromOutputHelper(testOutputHelper)), source); + var program = Utils.Parse(Setup.GetDafnyOptions(), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Equal(3, methods.Count); Assert.True(methods.All(m => @@ -74,7 +75,7 @@ invariant i < |c| { } } ".TrimStart(); - var program = Utils.Parse(Setup.GetDafnyOptions(new WriterFromOutputHelper(testOutputHelper)), source); + var program = Utils.Parse(Setup.GetDafnyOptions(), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); if (methods.Count != 3) { // This sometimes occurs on Windows testOutputHelper.WriteLine("methods.Count != 3, printing methods"); diff --git a/Source/DafnyTestGeneration.Test/Setup.cs b/Source/DafnyTestGeneration.Test/Setup.cs index feaa0c55bd1..cd537450b48 100644 --- a/Source/DafnyTestGeneration.Test/Setup.cs +++ b/Source/DafnyTestGeneration.Test/Setup.cs @@ -1,4 +1,3 @@ -using System.IO; using Microsoft.Dafny; namespace DafnyTestGeneration.Test { @@ -6,8 +5,8 @@ namespace DafnyTestGeneration.Test { public class Setup { - public static DafnyOptions GetDafnyOptions(TextWriter writer, params string[] arguments) { - var options = DafnyOptions.Create(writer, TextReader.Null, arguments ?? System.Array.Empty()); + public static DafnyOptions GetDafnyOptions(params string[] arguments) { + var options = DafnyOptions.Create(arguments ?? System.Array.Empty()); options.DefiniteAssignmentLevel = 3; options.WarnShadowing = true; options.VerifyAllModules = true; @@ -20,4 +19,4 @@ public static DafnyOptions GetDafnyOptions(TextWriter writer, params string[] ar } } -} +} \ No newline at end of file diff --git a/Source/DafnyTestGeneration.Test/Various.cs b/Source/DafnyTestGeneration.Test/Various.cs index 0ff89fff7a9..4628aeb345c 100644 --- a/Source/DafnyTestGeneration.Test/Various.cs +++ b/Source/DafnyTestGeneration.Test/Various.cs @@ -1,19 +1,13 @@ -using System.IO; using System.Linq; using System.Text.RegularExpressions; using System.Threading.Tasks; using Microsoft.Dafny; using Xunit; -using Xunit.Abstractions; namespace DafnyTestGeneration.Test { public class Various { - private readonly TextWriter output; - public Various(ITestOutputHelper output) { - this.output = new WriterFromOutputHelper(output); - } [Fact] public async Task NoInlining() { @@ -33,7 +27,7 @@ method a (i:int) returns (r:int) { } } ".TrimStart(); - var program = Utils.Parse(Setup.GetDafnyOptions(output), source); + var program = Utils.Parse(Setup.GetDafnyOptions(), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Equal(3, methods.Count); Assert.Equal(2, methods.Count(m => m.MethodName == "M.Inlining.b")); @@ -66,7 +60,7 @@ method a (i:int) returns (r:int) { } } ".TrimStart(); - var options = Setup.GetDafnyOptions(output); + var options = Setup.GetDafnyOptions(); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "M.Inlining.a"; var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); @@ -97,7 +91,7 @@ method test (a:int, b:int) returns (r:int) { } } ".TrimStart(); - var options = Setup.GetDafnyOptions(output); + var options = Setup.GetDafnyOptions(); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "M.Inlining.test"; var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); @@ -121,7 +115,7 @@ method test(a:int, b:int) returns (r:int) { } } ".TrimStart(); - var options = Setup.GetDafnyOptions(output); + var options = Setup.GetDafnyOptions(); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "M.Inlining.test"; var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); @@ -150,7 +144,7 @@ method test(n:int) returns (r:int) } } ".TrimStart(); - var options = Setup.GetDafnyOptions(output); + var options = Setup.GetDafnyOptions(); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "M.Inlining.test"; var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); @@ -179,7 +173,7 @@ method test(n:int) returns (r:int) } } ".TrimStart(); - var options = Setup.GetDafnyOptions(output); + var options = Setup.GetDafnyOptions(); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "M.Inlining.test"; var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); @@ -211,7 +205,7 @@ method eightPaths (i:int) } } ".TrimStart(); - var options = Setup.GetDafnyOptions(output); + var options = Setup.GetDafnyOptions(); var program = Utils.Parse(options, source); options.TestGenOptions.Mode = TestGenerationOptions.Modes.Path; @@ -258,7 +252,7 @@ method eightPaths (i:int) returns (divBy2:bool, divBy3:bool, divBy5:bool) { } } ".TrimStart(); - var program = Utils.Parse(Setup.GetDafnyOptions(output), source); + var program = Utils.Parse(Setup.GetDafnyOptions(), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(methods.Count is >= 2 and <= 6); Assert.True(methods.All(m => m.MethodName == "Paths.eightPaths")); @@ -302,7 +296,7 @@ decreases 3 - counter { } } ".TrimStart(); - var options = Setup.GetDafnyOptions(output); + var options = Setup.GetDafnyOptions(); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "Objects.List.IsACircleOfLessThanThree"; @@ -356,7 +350,7 @@ static method Depth(node: Node) returns (i:int) { } } ".TrimStart(); - var options = Setup.GetDafnyOptions(output); + var options = Setup.GetDafnyOptions(); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "DataTypes.List.Depth"; @@ -394,7 +388,7 @@ method ignoreNonNullableObject(v:Value, b:bool) { } } ".TrimStart(); - var options = Setup.GetDafnyOptions(output); + var options = Setup.GetDafnyOptions(); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "Module.ignoreNonNullableObject"; @@ -422,7 +416,7 @@ requires a > 0 } } ".TrimStart(); - var options = Setup.GetDafnyOptions(output); + var options = Setup.GetDafnyOptions(); var program = Utils.Parse(options, source); options.TestGenOptions.WarnDeadCode = true; var stats = await Main.GetDeadCodeStatistics(program).ToListAsync(); @@ -441,7 +435,7 @@ method m(a:int) returns (b:int) return 1; } ".TrimStart(); - var options = Setup.GetDafnyOptions(output); + var options = Setup.GetDafnyOptions(); var program = Utils.Parse(options, source); options.TestGenOptions.WarnDeadCode = true; var stats = await Main.GetDeadCodeStatistics(program).ToListAsync(); @@ -462,7 +456,7 @@ method IsEvenLength(s: seq) returns (isEven: bool) } } ".TrimStart(); - var options = Setup.GetDafnyOptions(output); + var options = Setup.GetDafnyOptions(); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "Test.IsEvenLength"; options.TestGenOptions.SeqLengthLimit = 1; @@ -490,7 +484,7 @@ function Min(a:int, b:int):int { } } ".TrimStart(); - var options = Setup.GetDafnyOptions(output); + var options = Setup.GetDafnyOptions(); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "Math.Min"; var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); @@ -518,7 +512,7 @@ function Or(a:bool):bool { } } ".TrimStart(); - var options = Setup.GetDafnyOptions(output); + var options = Setup.GetDafnyOptions(); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "ShortCircuit.Or"; var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); @@ -548,7 +542,7 @@ module C { function m(r:real):real requires r == 0.0 { r } } ".TrimStart(); - var options = Setup.GetDafnyOptions(output); + var options = Setup.GetDafnyOptions(); var program = Utils.Parse(options, source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Equal(3, methods.Count); @@ -588,7 +582,7 @@ modifies this } } ".TrimStart(); - var program = Utils.Parse(Setup.GetDafnyOptions(output), source); + var program = Utils.Parse(Setup.GetDafnyOptions(), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Single(methods); Assert.True(methods.All(m => diff --git a/Source/DafnyTestGeneration.Test/WriterFromOutputHelper.cs b/Source/DafnyTestGeneration.Test/WriterFromOutputHelper.cs deleted file mode 100644 index 82c93646a14..00000000000 --- a/Source/DafnyTestGeneration.Test/WriterFromOutputHelper.cs +++ /dev/null @@ -1,31 +0,0 @@ -using System.IO; -using System.Text; -using Xunit.Abstractions; - -namespace DafnyTestGeneration.Test; - -public class WriterFromOutputHelper : TextWriter { - private readonly ITestOutputHelper output; - private bool failed; - - public WriterFromOutputHelper(ITestOutputHelper output) { - this.output = output; - } - - public override void Write(char value) { - if (!failed) { - failed = true; - WriteLine("Error: tried to write a single character, which WriterFromOutputHelper does not support."); - } - } - - public override Encoding Encoding => Encoding.Default; - - public override void WriteLine(string value) { - output.WriteLine(value); - } - - public override void WriteLine(string format, params object[] arg) { - output.WriteLine(format, arg); - } -} \ No newline at end of file diff --git a/Source/DafnyTestGeneration/DafnyInfo.cs b/Source/DafnyTestGeneration/DafnyInfo.cs index 70095f6b375..4aa2c7fc577 100644 --- a/Source/DafnyTestGeneration/DafnyInfo.cs +++ b/Source/DafnyTestGeneration/DafnyInfo.cs @@ -64,7 +64,7 @@ public IList GetReturnTypes(string callable) { return new List { Utils.UseFullName(functions[callable].ResultType) }; } - Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify callable {callable}"); + Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify callable {callable}"); SetNonZeroExitCode = true; return new List(); } @@ -76,7 +76,7 @@ public List GetTypeArgs(string callable) { if (functions.ContainsKey(callable)) { return functions[callable].TypeArgs; } - Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify callable {callable}"); + Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify callable {callable}"); SetNonZeroExitCode = true; return new List(); } @@ -91,7 +91,7 @@ public List GetTypeArgsWithParents(string callable) { result.AddRange(functions[callable].TypeArgs); clazz = functions[callable].EnclosingClass; } else { - Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify callable {callable}"); + Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify callable {callable}"); SetNonZeroExitCode = true; return result; } @@ -108,7 +108,7 @@ public IList GetFormalsTypes(string callable) { return functions[callable].Formals.Select(arg => Utils.UseFullName(arg.Type)).ToList(); ; } - Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify callable {callable}"); + Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify callable {callable}"); SetNonZeroExitCode = true; return new List(); } @@ -120,7 +120,7 @@ public bool IsStatic(string callable) { if (functions.ContainsKey(callable)) { return functions[callable].IsStatic; } - Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify callable {callable}"); + Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify callable {callable}"); SetNonZeroExitCode = true; return true; } @@ -240,7 +240,7 @@ public IEnumerable GetEnsures(List ins, List outs, s new ClonerWithSubstitution(this, subst, receiver).CloneValidOrNull(e.E)) .Where(e => e != null); } - Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify callable {callableName}"); + Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify callable {callableName}"); SetNonZeroExitCode = true; return new List(); } @@ -263,7 +263,7 @@ public IEnumerable GetRequires(List ins, string callableName new ClonerWithSubstitution(this, subst, receiver).CloneValidOrNull(e.E)) .Where(e => e != null); } - Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify callable {callableName}"); + Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify callable {callableName}"); SetNonZeroExitCode = true; return new List(); } @@ -281,7 +281,7 @@ public IEnumerable GetRequires(List ins, string callableName public List<(string name, Type type, bool mutable, string/*?*/ defValue)> GetNonGhostFields(UserDefinedType/*?*/ type) { if (type == null || !classes.ContainsKey(type.Name)) { - Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify type {type?.Name ?? " (null) "}"); + Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify type {type?.Name ?? " (null) "}"); SetNonZeroExitCode = true; return new List<(string name, Type type, bool mutable, string/*?*/ defValue)>(); } @@ -311,7 +311,7 @@ public IEnumerable GetRequires(List ins, string callableName public bool IsTrait(UserDefinedType/*?*/ type) { if (type == null || !classes.ContainsKey(type.Name)) { - Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify type {type?.Name ?? " (null) "}"); + Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify type {type?.Name ?? " (null) "}"); SetNonZeroExitCode = true; return true; } @@ -373,7 +373,7 @@ public List GetEnsuresForTrait(UserDefinedType/*?*/ type, string name, D } public bool IsExtern(UserDefinedType/*?*/ type) { if (type == null || !classes.ContainsKey(type.Name)) { - Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify type {type?.Name ?? " (null) "}"); + Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify type {type?.Name ?? " (null) "}"); SetNonZeroExitCode = true; return true; } @@ -382,7 +382,7 @@ public bool IsExtern(UserDefinedType/*?*/ type) { public Constructor/*?*/ GetConstructor(UserDefinedType/*?*/ type) { if (type == null || !classes.ContainsKey(type.Name)) { - Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify type {type?.Name ?? " (null) "}"); + Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify type {type?.Name ?? " (null) "}"); SetNonZeroExitCode = true; return null; } @@ -427,16 +427,15 @@ private void VisitUserDefinedTypeDeclaration(string newTypeName, if (witness != null) { info.witnessForType[newTypeName] = witness; if (info.Options.TestGenOptions.Verbose) { - info.Options.OutputWriter.WriteLine($"// Values of type {newTypeName} will be " + - $"assigned the default value of " + - $"{Printer.ExprToString(info.Options, info.witnessForType[newTypeName])}"); + Console.Out.WriteLine($"// Values of type {newTypeName} will be " + + $"assigned the default value of " + + $"{Printer.ExprToString(info.Options, info.witnessForType[newTypeName])}"); } } else if (info.Options.TestGenOptions.Verbose) { - var message = $@" -*** Error: Values of type {newTypeName} -will be assigned a default value of type {baseType}, -which may not match the associated condition, if any".TrimStart(); - info.Options.Printer.ErrorWriteLine(info.Options.ErrorWriter, message); + info.Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Values of type {newTypeName} " + + $"will be assigned a default value of type " + + $"{baseType}, which may not match the " + + $"associated condition, if any"); info.SetNonZeroExitCode = true; } info.subsetToSuperset[newTypeName] = (typeArgs, @@ -621,4 +620,4 @@ public override Expression CloneExpr(Expression expr) { } } } -} +} \ No newline at end of file diff --git a/Source/DafnyTestGeneration/GenerateTestsCommand.cs b/Source/DafnyTestGeneration/GenerateTestsCommand.cs index aa403791c77..8f115c72ea3 100644 --- a/Source/DafnyTestGeneration/GenerateTestsCommand.cs +++ b/Source/DafnyTestGeneration/GenerateTestsCommand.cs @@ -43,7 +43,7 @@ private enum Mode { /// because we have to modify ProcsToCheck list, which does not have a setter. /// internal static DafnyOptions CopyForProcedure(DafnyOptions options, string procedureToVerify) { - var copy = DafnyOptions.Create(options.OutputWriter, options.Input, new[] { "/proc:" + procedureToVerify }); + var copy = DafnyOptions.Create(new[] { "/proc:" + procedureToVerify }); // Options set by the user: copy.LoopUnrollCount = options.LoopUnrollCount; copy.TestGenOptions.SeqLengthLimit = options.TestGenOptions.SeqLengthLimit; diff --git a/Source/DafnyTestGeneration/Main.cs b/Source/DafnyTestGeneration/Main.cs index 7a8f7ed687a..c18f46d980c 100644 --- a/Source/DafnyTestGeneration/Main.cs +++ b/Source/DafnyTestGeneration/Main.cs @@ -85,7 +85,7 @@ private static IEnumerable GetModifications(Modifications c i.VerboseName.Split(" ")[0] == options.TestGenOptions.TargetMethod)); if (!targetFound) { - options.Printer.ErrorWriteLine(options.ErrorWriter, + options.Printer.ErrorWriteLine(Console.Error, "Error: Cannot find method " + options.TestGenOptions.TargetMethod + " (is this name fully-qualified?)"); @@ -135,6 +135,7 @@ public static async IAsyncEnumerable GetTestMethodsForProgram(Progra /// Return a Dafny class (list of lines) with tests for the given Dafny file /// public static async IAsyncEnumerable GetTestClassForProgram(string sourceFile, DafnyOptions options) { + options.PrintMode = PrintModes.Everything; TestMethod.ClearTypesToSynthesize(); var source = await new StreamReader(sourceFile).ReadToEndAsync(); @@ -179,7 +180,7 @@ string EscapeDafnyStringLiteral(string str) { yield return "}"; if (methodsGenerated == 0) { - options.Printer.ErrorWriteLine(options.ErrorWriter, + options.Printer.ErrorWriteLine(Console.Error, "Error: No tests were generated, because no code points could be " + "proven reachable (do you have a false assumption in the program?)"); setNonZeroExitCode = true; diff --git a/Source/DafnyTestGeneration/ProgramModification.cs b/Source/DafnyTestGeneration/ProgramModification.cs index f636d3894a1..f50efde0ec3 100644 --- a/Source/DafnyTestGeneration/ProgramModification.cs +++ b/Source/DafnyTestGeneration/ProgramModification.cs @@ -123,7 +123,7 @@ private static void SetupForCounterexamples(DafnyOptions options) { counterexampleLog = null; if (result is not Task) { if (Options.TestGenOptions.Verbose) { - await options.OutputWriter.WriteLineAsync( + Console.WriteLine( $"// No test can be generated for {uniqueId} " + "because the verifier timed out."); } @@ -140,22 +140,22 @@ await options.OutputWriter.WriteLineAsync( coversBlocks.Add(blockId); if (Options.TestGenOptions.Verbose && Options.TestGenOptions.Mode != TestGenerationOptions.Modes.Path) { - await options.OutputWriter.WriteLineAsync($"// Test {uniqueId} covers block {blockId}"); + Console.WriteLine($"// Test targeting block {uniqueId} also covers block {blockId}"); } } } if (Options.TestGenOptions.Verbose && counterexampleLog == null) { if (log == "") { - await options.OutputWriter.WriteLineAsync( + Console.WriteLine( $"// No test is generated for {uniqueId} " + "because the verifier proved that no inputs could cause this block to be visited."); } else if (log.Contains("MODEL") || log.Contains("anon0")) { - await options.OutputWriter.WriteLineAsync( + Console.WriteLine( $"// No test is generated for {uniqueId} " + "because there is no enhanced error trace. This can be caused " + "by a bug in boogie counterexample model parsing."); } else { - await options.OutputWriter.WriteLineAsync( + Console.WriteLine( $"// No test is generated for {uniqueId} " + "because the verifier timed out."); } @@ -165,7 +165,7 @@ await options.OutputWriter.WriteLineAsync( public async Task GetTestMethod(Modifications cache, DafnyInfo dafnyInfo, bool returnNullIfNotUnique = true) { if (Options.TestGenOptions.Verbose) { - await dafnyInfo.Options.OutputWriter.WriteLineAsync( + Console.WriteLine( $"// Extracting the test for {uniqueId} from the counterexample..."); } var log = await GetCounterExampleLog(cache); @@ -183,7 +183,7 @@ await dafnyInfo.Options.OutputWriter.WriteLineAsync( return testMethod; } if (Options.TestGenOptions.Verbose) { - await dafnyInfo.Options.OutputWriter.WriteLineAsync( + Console.WriteLine( $"// Test for {uniqueId} matches a test previously generated " + $"for {duplicate.uniqueId}. This happens when test generation tool " + $"does not know how to differentiate between counterexamples, " + diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs index 7f82b966cfd..63fd059e5f3 100644 --- a/Source/DafnyTestGeneration/Utils.cs +++ b/Source/DafnyTestGeneration/Utils.cs @@ -80,7 +80,7 @@ public static Type CopyWithReplacements(Type type, List from, List var builtIns = new BuiltIns(options); var reporter = new BatchErrorReporter(options, defaultModuleDefinition); var success = Parser.Parse(source, uri, module, builtIns, - new Errors(reporter)) == 0 && DafnyMain.ParseIncludesDepthFirstNotCompiledFirst(options.Input, module, builtIns, + new Errors(reporter)) == 0 && Microsoft.Dafny.Main.ParseIncludesDepthFirstNotCompiledFirst(module, builtIns, new HashSet(), new Errors(reporter)) == null; var program = new Program(uri.LocalPath, module, builtIns, reporter); diff --git a/Source/IntegrationTests/LitTests.cs b/Source/IntegrationTests/LitTests.cs index 4b15b47c0f0..2da0ae27fea 100644 --- a/Source/IntegrationTests/LitTests.cs +++ b/Source/IntegrationTests/LitTests.cs @@ -5,7 +5,6 @@ using System.Reflection; using System.Runtime.InteropServices; using Microsoft.Dafny; -using TestDafny; using Xunit; using Xunit.Abstractions; using XUnitExtensions; @@ -23,7 +22,7 @@ public class LitTests { private const bool InvokeMainMethodsDirectly = false; private static readonly Assembly DafnyDriverAssembly = typeof(Dafny.Dafny).Assembly; - private static readonly Assembly TestDafnyAssembly = typeof(TestDafny.MultiBackendTest).Assembly; + private static readonly Assembly TestDafnyAssembly = typeof(TestDafny.TestDafny).Assembly; private static readonly Assembly DafnyServerAssembly = typeof(Server).Assembly; private static readonly string RepositoryRoot = Path.GetFullPath("../../../../../"); // Up from Source/IntegrationTests/bin/Debug/net6.0/ @@ -67,36 +66,40 @@ IEnumerable AddExtraArgs(IEnumerable args, IEnumerable l var commands = new Dictionary, LitTestConfiguration, ILitCommand>> { { "%baredafny", (args, config) => - DafnyCommand(args, config, InvokeMainMethodsDirectly) + MainMethodLitCommand.Parse(DafnyDriverAssembly, args, config, InvokeMainMethodsDirectly) }, { "%resolve", (args, config) => - DafnyCommand(AddExtraArgs(defaultResolveArgs, args), config, InvokeMainMethodsDirectly) + MainMethodLitCommand.Parse(DafnyDriverAssembly, AddExtraArgs(defaultResolveArgs, args), + config, InvokeMainMethodsDirectly) }, { "%translate", (args, config) => - DafnyCommand(AddExtraArgs(new[]{"translate"}, args), config, InvokeMainMethodsDirectly) + MainMethodLitCommand.Parse(DafnyDriverAssembly, AddExtraArgs(new[]{"translate"}, args), + config, InvokeMainMethodsDirectly) }, { "%verify", (args, config) => - DafnyCommand(AddExtraArgs(defaultVerifyArgs, args), config, InvokeMainMethodsDirectly) + MainMethodLitCommand.Parse(DafnyDriverAssembly, AddExtraArgs(defaultVerifyArgs, args), + config, InvokeMainMethodsDirectly) }, { "%build", (args, config) => - DafnyCommand(AddExtraArgs(defaultBuildArgs, args), config, InvokeMainMethodsDirectly) + MainMethodLitCommand.Parse(DafnyDriverAssembly, AddExtraArgs(defaultBuildArgs, args), + config, InvokeMainMethodsDirectly) }, { "%run", (args, config) => - DafnyCommand(AddExtraArgs(defaultRunArgs, args), config, InvokeMainMethodsDirectly) + MainMethodLitCommand.Parse(DafnyDriverAssembly, AddExtraArgs(defaultRunArgs, args), + config, InvokeMainMethodsDirectly) }, { "%dafny", (args, config) => - DafnyCommand(AddExtraArgs(DafnyDriver.DefaultArgumentsForTesting, args), config, InvokeMainMethodsDirectly) + MainMethodLitCommand.Parse(DafnyDriverAssembly, AddExtraArgs(DafnyDriver.DefaultArgumentsForTesting, args), + config, InvokeMainMethodsDirectly) }, { "%testDafnyForEachCompiler", (args, config) => - MainMethodLitCommand.Parse(TestDafnyAssembly, new []{ "for-each-compiler" }.Concat(args), config, InvokeMainMethodsDirectly) + MainMethodLitCommand.Parse(TestDafnyAssembly, new []{ "for-each-compiler" }.Concat(args), config, + InvokeMainMethodsDirectly) }, { - "%server", (args, config) => // TODO - { - var shellArguments = new[] { DafnyServerAssembly.Location }.Concat(args); - return new ShellLitCommand("dotnet", shellArguments, config.PassthroughEnvironmentVariables); - } + "%server", (args, config) => + MainMethodLitCommand.Parse(DafnyServerAssembly, args, config, InvokeMainMethodsDirectly) }, { - "%boogie", (args, config) => // TODO + "%boogie", (args, config) => new DotnetToolCommand("boogie", args.Concat(DefaultBoogieArguments), config.PassthroughEnvironmentVariables) @@ -105,7 +108,8 @@ IEnumerable AddExtraArgs(IEnumerable args, IEnumerable l }, { "%sed", (args, config) => SedCommand.Parse(args.ToArray()) }, { - "%OutputCheck", OutputCheckCommand.Parse + "%OutputCheck", (args, config) => + OutputCheckCommand.Parse(args, config) } }; @@ -144,7 +148,8 @@ IEnumerable AddExtraArgs(IEnumerable args, IEnumerable l AddExtraArgs(DafnyDriver.DefaultArgumentsForTesting, args), config.PassthroughEnvironmentVariables); commands["%testDafnyForEachCompiler"] = (args, config) => MainMethodLitCommand.Parse(TestDafnyAssembly, - new[] { "for-each-compiler", "--dafny", dafnyCliPath }.Concat(args), config, false); + new[] { "for-each-compiler", "--dafny", dafnyCliPath }.Concat(args), config, + InvokeMainMethodsDirectly); commands["%server"] = (args, config) => new ShellLitCommand(Path.Join(dafnyReleaseDir, "DafnyServer"), args, config.PassthroughEnvironmentVariables); commands["%boogie"] = (args, config) => @@ -157,12 +162,6 @@ IEnumerable AddExtraArgs(IEnumerable args, IEnumerable l Config = new LitTestConfiguration(substitutions, commands, features, DafnyDriver.ReferencedEnvironmentVariables); } - public static ILitCommand DafnyCommand(IEnumerable arguments, LitTestConfiguration config, bool invokeDirectly) { - return invokeDirectly - ? new DafnyDriverLitCommand(arguments, config) - : new ShellLitCommand("dotnet", new[] { DafnyDriverAssembly.Location }.Concat(arguments), config.PassthroughEnvironmentVariables); - } - private readonly ITestOutputHelper output; public LitTests(ITestOutputHelper output) { @@ -177,39 +176,4 @@ public void LitTest(string path) { LitTestCase.Run(path, Config, output); } } - - class DafnyDriverLitCommand : ILitCommand { - private readonly string[] arguments; - - public DafnyDriverLitCommand(IEnumerable arguments, LitTestConfiguration config) { - this.arguments = arguments.ToArray(); - } - - public (int, string, string) Execute(TextReader inputReader, - TextWriter outputWriter, - TextWriter errorWriter) { - var exitCode = DafnyDriver.MainWithWriters(outputWriter, errorWriter, inputReader, arguments); - return (exitCode, "", ""); - } - - public override string ToString() { - return $"dafny {string.Join(" ", arguments)}"; - } - } - - class MultiBackendLitCommand : ILitCommand { - private readonly string[] arguments; - - public MultiBackendLitCommand(IEnumerable arguments, LitTestConfiguration config) { - this.arguments = arguments.ToArray(); - } - - public (int, string, string) Execute(TextReader inputReader, - TextWriter outputWriter, - TextWriter errorWriter) { - var exitCode = new MultiBackendTest(inputReader, outputWriter, errorWriter).Start(arguments.Prepend("for-each-compiler")); - return (exitCode, "", ""); - } - } } - diff --git a/Source/TestDafny/MultiBackendTest.cs b/Source/TestDafny/TestDafny.cs similarity index 59% rename from Source/TestDafny/MultiBackendTest.cs rename to Source/TestDafny/TestDafny.cs index db63b577e90..5f21c699d95 100644 --- a/Source/TestDafny/MultiBackendTest.cs +++ b/Source/TestDafny/TestDafny.cs @@ -5,6 +5,7 @@ using Microsoft.Dafny; using Microsoft.Dafny.Plugins; using XUnitExtensions; +using XUnitExtensions.Lit; namespace TestDafny; @@ -14,8 +15,10 @@ public class ForEachCompilerOptions { [Value(0, Required = true, MetaName = "Test file", HelpText = "The *.dfy file to test.")] public string? TestFile { get; set; } = null; - [Value(1, MetaName = "Dafny CLI arguments", HelpText = "Any arguments following '--' will be passed to the dafny CLI unaltered.")] - public IEnumerable OtherArgs { get; set; } = Array.Empty(); + [Option("dafny", HelpText = "The dafny CLI to test with. Defaults to the locally built DafnyDriver project.")] + public string? DafnyCliPath { get; set; } = null; + + [Value(1, MetaName = "Dafny CLI arguments", HelpText = "Any arguments following '--' will be passed to the dafny CLI unaltered.")] public IEnumerable OtherArgs { get; set; } = Array.Empty(); } [Verb("features", HelpText = "Print the Markdown content documenting feature support for each compiler.")] @@ -23,45 +26,37 @@ public class FeaturesOptions { [Value(1)] public IEnumerable OtherArgs { get; set; } = Array.Empty(); } -public class MultiBackendTest { +public class TestDafny { + private static readonly Assembly DafnyAssembly = typeof(Dafny.Dafny).Assembly; - private readonly TextReader input; - private readonly TextWriter output; - private readonly TextWriter errorWriter; - - public MultiBackendTest(TextReader input, TextWriter output, TextWriter errorWriter) { - this.input = input; - this.output = output; - this.errorWriter = errorWriter; - } public static int Main(string[] args) { - return new MultiBackendTest(Console.In, Console.Out, Console.Error).Start(args.ToList()); - } - - public int Start(IEnumerable args) { var result = -1; var parser = new CommandLine.Parser(with => { with.EnableDashDash = true; - with.HelpWriter = errorWriter; + with.HelpWriter = Console.Error; }); var parseResult = parser.ParseArguments(args); - parseResult.WithParsed(options => { result = ForEachCompiler(options); }) - .WithParsed(options => { result = GenerateCompilerTargetSupportTable(options); }); + parseResult.WithParsed(options => { + result = ForEachCompiler(options); + }).WithParsed(options => { + result = GenerateCompilerTargetSupportTable(options); + }); return result; } - private DafnyOptions? ParseDafnyOptions(IEnumerable dafnyArgs) { - var dafnyOptions = new DafnyOptions(input, output, errorWriter); + private static DafnyOptions? ParseDafnyOptions(IEnumerable dafnyArgs) { + var dafnyOptions = new DafnyOptions(); var success = dafnyOptions.Parse(dafnyArgs.ToArray()); return success ? dafnyOptions : null; } - private int ForEachCompiler(ForEachCompilerOptions options) { - var parseResult = CommandRegistry.Create(TextWriter.Null, TextWriter.Null, TextReader.Null, - new string[] { "verify", options.TestFile! }.Concat(options.OtherArgs).ToArray()); - var dafnyOptions = ((ParseArgumentSuccess)parseResult).DafnyOptions; + private static int ForEachCompiler(ForEachCompilerOptions options) { + var dafnyOptions = ParseDafnyOptions(options.OtherArgs); + if (dafnyOptions == null) { + return (int)DafnyDriver.CommandLineArgumentsResult.PREPROCESSING_ERROR; + } // First verify the file (and assume that verification should be successful). // Older versions of test files that now use %testDafnyForEachCompiler were sensitive to the number @@ -69,19 +64,19 @@ private int ForEachCompiler(ForEachCompilerOptions options) { // but this was never meaningful and only added maintenance burden. // Here we only ensure that the exit code is 0. - var dafnyArgs = new List() { - $"verify", + var dafnyArgs = new List(options.OtherArgs) { + $"/compile:0", options.TestFile! - }.Concat(options.OtherArgs).ToArray(); + }; - output.WriteLine("Verifying..."); + Console.Out.WriteLine("Verifying..."); - var (exitCode, outputString, error) = RunDafny(dafnyArgs); + var (exitCode, output, error) = RunDafny(options.DafnyCliPath, dafnyArgs); if (exitCode != 0) { - output.WriteLine("Verification failed. Output:"); - output.WriteLine(outputString); - output.WriteLine("Error:"); - output.WriteLine(error); + Console.Out.WriteLine("Verification failed. Output:"); + Console.Out.WriteLine(output); + Console.Out.WriteLine("Error:"); + Console.Out.WriteLine(error); return exitCode; } @@ -94,11 +89,6 @@ private int ForEachCompiler(ForEachCompilerOptions options) { var success = true; foreach (var plugin in dafnyOptions.Plugins) { foreach (var compiler in plugin.GetCompilers(dafnyOptions)) { - if (compiler.TargetId == "lib") { - // Some tests still fail when using the lib back-end, for example due to disallowed assumptions being present in the test, - // Such as empty constructors with ensures clauses, generated from iterators - continue; - } var result = RunWithCompiler(options, compiler, expectedOutput); if (result != 0) { success = false; @@ -107,7 +97,7 @@ private int ForEachCompiler(ForEachCompilerOptions options) { } if (success) { - output.WriteLine( + Console.Out.WriteLine( $"All executions were successful and matched the expected output (or reported errors for known unsupported features)!"); return 0; } else { @@ -115,55 +105,61 @@ private int ForEachCompiler(ForEachCompilerOptions options) { } } - private int RunWithCompiler(ForEachCompilerOptions options, IExecutableBackend backend, string expectedOutput) { - output.WriteLine($"Executing on {backend.TargetName}..."); - var dafnyArgs = new List() { - "run", - "--no-verify", - $"--target:{backend.TargetId}", - options.TestFile!, - }.Concat(options.OtherArgs); + private static int RunWithCompiler(ForEachCompilerOptions options, IExecutableBackend backend, string expectedOutput) { + Console.Out.WriteLine($"Executing on {backend.TargetName}..."); + var dafnyArgs = new List(options.OtherArgs) { + // Here we can pass /noVerify to save time since we already verified the program. + "/noVerify", + // /noVerify is interpreted pessimistically as "did not get verification success", + // so we have to force compiling and running despite this. + "/compile:4", + $"/compileTarget:{backend.TargetId}", + options.TestFile! + }; - var (exitCode, outputString, error) = RunDafny(dafnyArgs); + var (exitCode, output, error) = RunDafny(options.DafnyCliPath, dafnyArgs); if (exitCode == 0) { - var diffMessage = AssertWithDiff.GetDiffMessage(expectedOutput, outputString); + var diffMessage = AssertWithDiff.GetDiffMessage(expectedOutput, output); if (diffMessage == null) { return 0; } - output.WriteLine(diffMessage); + Console.Out.WriteLine(diffMessage); return 1; } // If we hit errors, check for known unsupported features for this compilation target - if (error == "" && OnlyUnsupportedFeaturesErrors(backend, outputString)) { + if (error == "" && OnlyUnsupportedFeaturesErrors(backend, output)) { return 0; } - output.WriteLine("Execution failed, for reasons other than known unsupported features. Output:"); - output.WriteLine(outputString); - output.WriteLine("Error:"); - output.WriteLine(error); + Console.Out.WriteLine("Execution failed, for reasons other than known unsupported features. Output:"); + Console.Out.WriteLine(output); + Console.Out.WriteLine("Error:"); + Console.Out.WriteLine(error); return exitCode; } - private static (int, string, string) RunDafny(IEnumerable arguments) { - var argumentsWithDefaults = arguments.Concat(DafnyDriver.NewDefaultArgumentsForTesting); - var outputWriter = new StringWriter(); - var errorWriter = new StringWriter(); - var exitCode = DafnyDriver.MainWithWriters(outputWriter, errorWriter, TextReader.Null, argumentsWithDefaults.ToArray()); - var outputString = outputWriter.ToString(); - var error = errorWriter.ToString(); - return (exitCode, outputString, error); + private static (int, string, string) RunDafny(string? dafnyCLIPath, IEnumerable arguments) { + var argumentsWithDefaults = arguments.Concat(DafnyDriver.DefaultArgumentsForTesting); + ILitCommand command; + if (dafnyCLIPath != null) { + command = new ShellLitCommand(dafnyCLIPath, argumentsWithDefaults, DafnyDriver.ReferencedEnvironmentVariables); + } else { + var dotnetArguments = new[] { DafnyAssembly.Location }.Concat(argumentsWithDefaults); + command = new ShellLitCommand("dotnet", dotnetArguments, DafnyDriver.ReferencedEnvironmentVariables); + } + return command.Execute(null, null, null, null); } private static bool OnlyUnsupportedFeaturesErrors(IExecutableBackend backend, string output) { - using StringReader sr = new StringReader(output); - string? line; - while ((line = sr.ReadLine()) != null) { - if (!IsAllowedOutputLine(backend, line)) { - return false; + using (StringReader sr = new StringReader(output)) { + string? line; + while ((line = sr.ReadLine()) != null) { + if (!IsAllowedOutputLine(backend, line)) { + return false; + } } } @@ -208,7 +204,7 @@ private static bool IsAllowedOutputLine(IExecutableBackend backend, string line) $"Compiler rejected feature '{feature}', which is not an element of its UnsupportedFeatures set"); } - private int GenerateCompilerTargetSupportTable(FeaturesOptions featuresOptions) { + private static int GenerateCompilerTargetSupportTable(FeaturesOptions featuresOptions) { var dafnyOptions = ParseDafnyOptions(featuresOptions.OtherArgs); if (dafnyOptions == null) { return (int)DafnyDriver.CommandLineArgumentsResult.PREPROCESSING_ERROR; @@ -220,20 +216,20 @@ private int GenerateCompilerTargetSupportTable(FeaturesOptions featuresOptions) .ToList(); // Header - output.Write("| Feature |"); + Console.Out.Write("| Feature |"); foreach (var compiler in allCompilers) { - output.Write($" {compiler.TargetName} |"); + Console.Out.Write($" {compiler.TargetName} |"); } - output.WriteLine(); + Console.Out.WriteLine(); // Horizontal rule ("|----|---|...") - output.Write("|-|"); + Console.Out.Write("|-|"); foreach (var _ in allCompilers) { - output.Write($"-|"); + Console.Out.Write($"-|"); } - output.WriteLine(); + Console.Out.WriteLine(); var footnotes = new StringBuilder(); foreach (var feature in Enum.GetValues(typeof(Feature)).Cast()) { @@ -245,19 +241,19 @@ private int GenerateCompilerTargetSupportTable(FeaturesOptions featuresOptions) footnotes.AppendLine(); } - output.Write($"| [{description.Description}](#{description.ReferenceManualSection}){footnoteLink} |"); + Console.Out.Write($"| [{description.Description}](#{description.ReferenceManualSection}){footnoteLink} |"); foreach (var compiler in allCompilers) { var supported = !compiler.UnsupportedFeatures.Contains(feature); var cell = supported ? " X " : ""; - output.Write($" {cell} |"); + Console.Out.Write($" {cell} |"); } - output.WriteLine(); + Console.Out.WriteLine(); } - output.WriteLine(); - output.WriteLine(footnotes); + Console.Out.WriteLine(); + Console.Out.WriteLine(footnotes); return 0; } -} +} \ No newline at end of file diff --git a/Source/TestDafny/TestDafny.csproj b/Source/TestDafny/TestDafny.csproj index 83f292e7923..03d2c3a702c 100644 --- a/Source/TestDafny/TestDafny.csproj +++ b/Source/TestDafny/TestDafny.csproj @@ -1,24 +1,22 @@ - Exe - net6.0 - enable - enable - false - - + Exe + net6.0 + enable + enable + false + + - - - + - + PreserveNewest diff --git a/Source/XUnitExtensions/Lit/DiffCommand.cs b/Source/XUnitExtensions/Lit/DiffCommand.cs index 281d1ffb72e..eee6070ed64 100644 --- a/Source/XUnitExtensions/Lit/DiffCommand.cs +++ b/Source/XUnitExtensions/Lit/DiffCommand.cs @@ -28,8 +28,7 @@ public static ILitCommand Parse(string[] args) { return new DiffCommand(expectedPath, actualPath); } - public (int, string, string) Execute(TextReader inputReader, - TextWriter outputWriter, TextWriter errorWriter) { + public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { var expected = File.ReadAllText(expectedPath); var actual = File.ReadAllText(actualPath); var diffMessage = AssertWithDiff.GetDiffMessage(expected, actual); diff --git a/Source/XUnitExtensions/Lit/ExitCommand.cs b/Source/XUnitExtensions/Lit/ExitCommand.cs index 793e224f6e3..e4499d7b1d7 100644 --- a/Source/XUnitExtensions/Lit/ExitCommand.cs +++ b/Source/XUnitExtensions/Lit/ExitCommand.cs @@ -12,9 +12,8 @@ public ExitCommand(int exitCode, ILitCommand operand) { this.operand = operand; } - public (int, string, string) Execute(TextReader inputReader, - TextWriter outputWriter, TextWriter errorWriter) { - var (exitCode, output, error) = operand.Execute(inputReader, outputWriter, errorWriter); + public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { + var (exitCode, output, error) = operand.Execute(outputHelper, inputReader, outputWriter, errorWriter); if (exitCode == expectedExitCode) { return (0, output, error); } else { diff --git a/Source/XUnitExtensions/Lit/ILitCommand.cs b/Source/XUnitExtensions/Lit/ILitCommand.cs index 83318221af4..da9cfabcac3 100644 --- a/Source/XUnitExtensions/Lit/ILitCommand.cs +++ b/Source/XUnitExtensions/Lit/ILitCommand.cs @@ -16,26 +16,15 @@ public enum Kind { Verbatim, MustGlob } class DelayedLitCommand : ILitCommand { private readonly Func factory; - private ILitCommand? command; public DelayedLitCommand(Func factory) { this.factory = factory; } - public (int, string, string) Execute(TextReader inputReader, - TextWriter outputWriter, - TextWriter errorWriter) { - if (command == null) { - command = factory(); - } - return command.Execute(inputReader, outputWriter, errorWriter); - } - - public override string? ToString() { - if (command == null) { - command = factory(); - } - return command!.ToString(); + public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, + TextWriter? errorWriter) { + var command = factory(); + return command.Execute(outputHelper, inputReader, outputWriter, errorWriter); } } public interface ILitCommand { @@ -91,6 +80,6 @@ public static Token[] Tokenize(string line) { return result.ToArray(); } - public (int, string, string) Execute(TextReader inputReader, TextWriter outputWriter, TextWriter errorWriter); + public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter); } } diff --git a/Source/XUnitExtensions/Lit/LitCommandWithRedirection.cs b/Source/XUnitExtensions/Lit/LitCommandWithRedirection.cs index 51a39441f97..962903e9f96 100644 --- a/Source/XUnitExtensions/Lit/LitCommandWithRedirection.cs +++ b/Source/XUnitExtensions/Lit/LitCommandWithRedirection.cs @@ -77,12 +77,11 @@ public LitCommandWithRedirection(ILitCommand command, string? inputFile, string? this.errorFile = errorFile; } - public (int, string, string) Execute(TextReader inReader, TextWriter outWriter, - TextWriter errWriter) { + public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inReader, TextWriter? outWriter, TextWriter? errWriter) { var inputReader = inputFile != null ? new StreamReader(inputFile) : inReader; var outputWriter = outputFile != null ? new StreamWriter(outputFile, append) : outWriter; var errorWriter = errorFile != null ? new StreamWriter(errorFile, append) : errWriter; - var result = command.Execute(inputReader, outputWriter, errorWriter); + var result = command.Execute(outputHelper, inputReader, outputWriter, errorWriter); inputReader?.Close(); outputWriter?.Close(); errorWriter?.Close(); @@ -117,25 +116,3 @@ public override string ToString() { } } } - -public class WriterFromOutputHelper : TextWriter { - private readonly ITestOutputHelper output; - - public WriterFromOutputHelper(ITestOutputHelper output) { - this.output = output; - } - - public override void Write(char value) { - - } - - public override Encoding Encoding => Encoding.Default; - - public override void WriteLine(string? value) { - output.WriteLine(value); - } - - public override void WriteLine(string format, params object?[] arg) { - output.WriteLine(format, arg); - } -} \ No newline at end of file diff --git a/Source/XUnitExtensions/Lit/LitTestCase.cs b/Source/XUnitExtensions/Lit/LitTestCase.cs index 9b3e96f66a9..1ed0680d6e3 100644 --- a/Source/XUnitExtensions/Lit/LitTestCase.cs +++ b/Source/XUnitExtensions/Lit/LitTestCase.cs @@ -61,7 +61,7 @@ public LitTestCase(string filePath, IEnumerable commands, bool expe this.expectFailure = expectFailure; } - public void Execute(ITestOutputHelper outputHelper) { + public void Execute(ITestOutputHelper? outputHelper) { Directory.CreateDirectory(Path.Join(Path.GetDirectoryName(filePath), "Output")); // For debugging. Only printed on failure in case the true cause is buried in an earlier command. List<(string, string)> results = new(); @@ -70,11 +70,9 @@ public void Execute(ITestOutputHelper outputHelper) { int exitCode; string output; string error; - var outputWriter = new StringWriter(); - var errorWriter = new StringWriter(); try { - outputHelper.WriteLine($"Executing command: {command}"); - (exitCode, output, error) = command.Execute(TextReader.Null, outputWriter, errorWriter); + 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); } @@ -82,7 +80,7 @@ public void Execute(ITestOutputHelper outputHelper) { if (expectFailure) { if (exitCode != 0) { throw new SkipException( - $"Command returned non-zero exit code ({exitCode}): {command}\nOutput:\n{output + outputWriter}\nError:\n{error + errorWriter}"); + $"Command returned non-zero exit code ({exitCode}): {command}\nOutput:\n{output}\nError:\n{error}"); } } @@ -94,7 +92,7 @@ public void Execute(ITestOutputHelper outputHelper) { } throw new Exception( - $"Command returned non-zero exit code ({exitCode}): {command}\nOutput:\n{output + outputWriter}\nError:\n{error + errorWriter}"); + $"Command returned non-zero exit code ({exitCode}): {command}\nOutput:\n{output}\nError:\n{error}"); } results.Add((output, error)); diff --git a/Source/XUnitExtensions/Lit/MainMethodLitCommand.cs b/Source/XUnitExtensions/Lit/MainMethodLitCommand.cs index c4412cc8bb7..19277f978c7 100644 --- a/Source/XUnitExtensions/Lit/MainMethodLitCommand.cs +++ b/Source/XUnitExtensions/Lit/MainMethodLitCommand.cs @@ -21,8 +21,7 @@ public static ILitCommand Parse(Assembly assembly, IEnumerable arguments return invokeDirectly ? result : result.ToShellCommand(config); } - public (int, string, string) Execute(TextReader inputReader, - TextWriter outputWriter, TextWriter errorWriter) { + public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { if (inputReader != null) { Console.SetIn(inputReader); } @@ -33,8 +32,8 @@ public static ILitCommand Parse(Assembly assembly, IEnumerable arguments Console.SetError(errorWriter); } - var result = assembly.EntryPoint!.Invoke(null, new object[] { arguments }); - var exitCode = result == null ? 0 : (int)result; + var entry = assembly.EntryPoint!; + var exitCode = (int)entry.Invoke(null, new object[] { arguments })!; return (exitCode, "", ""); } @@ -52,4 +51,4 @@ public override string ToString() { return builder.ToString(); } } -} +} \ No newline at end of file diff --git a/Source/XUnitExtensions/Lit/NotCommand.cs b/Source/XUnitExtensions/Lit/NotCommand.cs index bcf62f65ce2..f373ba765e5 100644 --- a/Source/XUnitExtensions/Lit/NotCommand.cs +++ b/Source/XUnitExtensions/Lit/NotCommand.cs @@ -10,9 +10,8 @@ public NotCommand(ILitCommand operand) { this.operand = operand; } - public (int, string, string) Execute(TextReader inputReader, - TextWriter outputWriter, TextWriter errorWriter) { - var (exitCode, output, error) = operand.Execute(inputReader, outputWriter, errorWriter); + public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { + var (exitCode, output, error) = operand.Execute(outputHelper, inputReader, outputWriter, errorWriter); return (exitCode == 0 ? 1 : 0, output, error); } diff --git a/Source/XUnitExtensions/Lit/OrCommand.cs b/Source/XUnitExtensions/Lit/OrCommand.cs index ee6d6afb911..02811594e07 100644 --- a/Source/XUnitExtensions/Lit/OrCommand.cs +++ b/Source/XUnitExtensions/Lit/OrCommand.cs @@ -11,14 +11,13 @@ public OrCommand(ILitCommand lhs, ILitCommand rhs) { this.rhs = rhs; } - public (int, string, string) Execute(TextReader inputReader, - TextWriter outputWriter, TextWriter errorWriter) { - var (leftExitCode, leftOutput, leftError) = lhs.Execute(inputReader, outputWriter, errorWriter); + public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { + var (leftExitCode, leftOutput, leftError) = lhs.Execute(outputHelper, inputReader, outputWriter, errorWriter); if (leftExitCode == 0) { return (leftExitCode, leftOutput, leftError); } - var (rightExitCode, rightOutput, rightError) = rhs.Execute(inputReader, outputWriter, errorWriter); + var (rightExitCode, rightOutput, rightError) = rhs.Execute(outputHelper, inputReader, outputWriter, errorWriter); return (rightExitCode, leftOutput + rightOutput, leftError + rightError); } diff --git a/Source/XUnitExtensions/Lit/OutputCheckCommand.cs b/Source/XUnitExtensions/Lit/OutputCheckCommand.cs index 3eba773e5a4..23ee3a8e391 100644 --- a/Source/XUnitExtensions/Lit/OutputCheckCommand.cs +++ b/Source/XUnitExtensions/Lit/OutputCheckCommand.cs @@ -185,8 +185,8 @@ public static ILitCommand Parse(IEnumerable args, LitTestConfiguration c return result!; } - public (int, string, string) Execute(TextReader inputReader, - TextWriter outputWriter, TextWriter errorWriter) { + public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, + TextWriter? outputWriter, TextWriter? errorWriter) { if (options.FileToCheck == null) { return (0, "", ""); } diff --git a/Source/XUnitExtensions/Lit/SedCommand.cs b/Source/XUnitExtensions/Lit/SedCommand.cs index 66846045055..8d47c9fe81a 100644 --- a/Source/XUnitExtensions/Lit/SedCommand.cs +++ b/Source/XUnitExtensions/Lit/SedCommand.cs @@ -39,8 +39,7 @@ public static ILitCommand Parse(string[] args) { return new SedCommand(regexp, replaceBy, file); } - public (int, string, string) Execute(TextReader inputReader, - TextWriter outputWriter, TextWriter errorWriter) { + public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { var fileContent = File.ReadAllText(file); try { var stdOutput = Regex.Replace(fileContent, "(?m)" + regexp, replaceBy); diff --git a/Source/XUnitExtensions/Lit/ShellLitCommand.cs b/Source/XUnitExtensions/Lit/ShellLitCommand.cs index c6dbd81136b..98fdcc19315 100644 --- a/Source/XUnitExtensions/Lit/ShellLitCommand.cs +++ b/Source/XUnitExtensions/Lit/ShellLitCommand.cs @@ -18,8 +18,7 @@ public ShellLitCommand(string shellCommand, IEnumerable arguments, IEnum this.passthroughEnvironmentVariables = passthroughEnvironmentVariables.ToArray(); } - public (int, string, string) Execute(TextReader inputReader, - TextWriter outputWriter, TextWriter errorWriter) { + public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { using var process = new Process(); process.StartInfo.FileName = shellCommand; diff --git a/Source/XUnitExtensions/Lit/StdInCommand.cs b/Source/XUnitExtensions/Lit/StdInCommand.cs index df1768cb800..3d10baf5577 100644 --- a/Source/XUnitExtensions/Lit/StdInCommand.cs +++ b/Source/XUnitExtensions/Lit/StdInCommand.cs @@ -13,10 +13,9 @@ public StdInCommand(string stdin, ILitCommand operand) { this.operand = operand; } - public (int, string, string) Execute(TextReader inputReader, - TextWriter outputWriter, TextWriter errorWriter) { + public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { inputReader = new StringReader(stdin); - return operand.Execute(inputReader, outputWriter, errorWriter); + return operand.Execute(outputHelper, inputReader, outputWriter, errorWriter); } public override string ToString() { diff --git a/Source/XUnitExtensions/Lit/UnsupportedCommand.cs b/Source/XUnitExtensions/Lit/UnsupportedCommand.cs index b5480d52724..6aa1e004c70 100644 --- a/Source/XUnitExtensions/Lit/UnsupportedCommand.cs +++ b/Source/XUnitExtensions/Lit/UnsupportedCommand.cs @@ -19,8 +19,7 @@ public UnsupportedCommand(IEnumerable features) { Features = features; } - public (int, string, string) Execute(TextReader inputReader, - TextWriter outputWriter, TextWriter errorWriter) { + public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { return (0, "", ""); } } diff --git a/Source/XUnitExtensions/Lit/XFailCommand.cs b/Source/XUnitExtensions/Lit/XFailCommand.cs index edad57bf4de..9310c84064b 100644 --- a/Source/XUnitExtensions/Lit/XFailCommand.cs +++ b/Source/XUnitExtensions/Lit/XFailCommand.cs @@ -14,8 +14,7 @@ public static ILitCommand Parse(string line, LitTestConfiguration config) { throw new ArgumentException($"Unrecognized arguments to XFAIL: {line}"); } - public (int, string, string) Execute(TextReader inputReader, - TextWriter outputWriter, TextWriter errorWriter) { + public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { return (0, "", ""); } } diff --git a/Test/comp/Iterators.dfy b/Test/comp/Iterators.dfy index 0512ddb93b0..663ade95863 100644 --- a/Test/comp/Iterators.dfy +++ b/Test/comp/Iterators.dfy @@ -8,8 +8,6 @@ class C { print "x is ", x, "\n"; Client(); RegressionClient(); - r := *; - s := *; } } diff --git a/Test/comp/UnicodeStrings.dfy b/Test/comp/UnicodeStrings.dfy index 30cde9aca69..fd512dd4510 100644 --- a/Test/comp/UnicodeStrings.dfy +++ b/Test/comp/UnicodeStrings.dfy @@ -1,4 +1,4 @@ -// RUN: %testDafnyForEachCompiler "%s" -- --unicode-char +// RUN: %testDafnyForEachCompiler "%s" -- /unicodeChar:1 method AssertAndExpect(p: bool) requires p diff --git a/Test/comp/Uninitialized.dfy b/Test/comp/Uninitialized.dfy index 1b69f1be4ec..220495ad5e1 100644 --- a/Test/comp/Uninitialized.dfy +++ b/Test/comp/Uninitialized.dfy @@ -140,16 +140,12 @@ module {:options "/functionSyntax:4"} EnumerationTests { method PickEnumValue() returns (r: Enum) { if e: Enum :| e.Is(13) { r := e; - } else { - r := *; } } method PickAllGhostValue() returns (r: AllGhost) { if ag: AllGhost :| ag.Is(13) { r := ag; - } else { - r := *; } } } diff --git a/Test/comp/compile3/JustRun.dfy.expect b/Test/comp/compile3/JustRun.dfy.expect index 95909991d55..06ceaa6e321 100644 --- a/Test/comp/compile3/JustRun.dfy.expect +++ b/Test/comp/compile3/JustRun.dfy.expect @@ -1,6 +1,5 @@ Dafny program verifier finished with 0 verified, 0 errors -Compiled assembly into JustRun.dll Running... hello, Dafny diff --git a/Test/dafny0/Strings.dfy b/Test/dafny0/Strings.dfy index 039c09a69aa..b0010970e6f 100644 --- a/Test/dafny0/Strings.dfy +++ b/Test/dafny0/Strings.dfy @@ -1,14 +1,12 @@ -// RUN: %testDafnyForEachCompiler "%s" -- --unicode-char=false +// RUN: %testDafnyForEachCompiler "%s" -- /unicodeChar:0 method Char(a: char, s: string, i: int) returns (b: char) { - var ch: char := *; + var ch: char; if a == ch { b := ch; } else if 0 <= i < |s| { b := s[i]; - } else { - b := *; } } @@ -20,8 +18,7 @@ method {:MyAttribute "hello", "hi" + "there", 57} AttrTest() method M(a: char, b: char) returns (s: string, t: seq) ensures |s| == 3 ==> t == [a, b, b]; -{ - s := *; +{ s := s + [a, b, b] + s; t := s; s := t[0..|s|]; @@ -35,7 +32,7 @@ method M(a: char, b: char) returns (s: string, t: seq) // strings rather than printing them and relying on the diff with the expect file. method Main() { - var ch: char := *; + var ch: char; var s, t := M(ch, ch); print "ch = ", ch, "\n"; print "The string is: " + s + "\n"; diff --git a/Test/git-issues/git-issue-1553.dfy b/Test/git-issues/git-issue-1553.dfy index 6267018c92d..530608808d9 100644 --- a/Test/git-issues/git-issue-1553.dfy +++ b/Test/git-issues/git-issue-1553.dfy @@ -1,11 +1,10 @@ // RUN: %dafny /compile:0 "%s" > "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" +// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" // RUN: %diff "%s.expect" "%t" -method Main() { } method Test() { var r: R; var s: seq; diff --git a/Test/git-issues/git-issue-374.dfy b/Test/git-issues/git-issue-374.dfy index 4c031b7d3ff..bdbc7099d31 100644 --- a/Test/git-issues/git-issue-374.dfy +++ b/Test/git-issues/git-issue-374.dfy @@ -1,7 +1,7 @@ // RUN: %dafny /compile:0 "%s" > "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" +// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" // RUN: %diff "%s.expect" "%t" @@ -13,7 +13,7 @@ class C { ghost function f() : int { 0 } -method Main() { +method main() { var c := new C(f()); } diff --git a/Test/git-issues/git-issue-3883.dfy b/Test/git-issues/git-issue-3883.dfy index 018dfcacf43..aaed6ae9512 100644 --- a/Test/git-issues/git-issue-3883.dfy +++ b/Test/git-issues/git-issue-3883.dfy @@ -46,14 +46,14 @@ type ST0 = x: int | x % 5 == 1 witness 16 type ST1 = x: int | (if var m: map := map[]; m == map[] then 0 else 8) <= x method DoIt() { - var t0: ST0 := *; - var t1: ST1 := *; + var t0: ST0; + var t1: ST1; Print(t0, " "); // 16-16 Print(t1, "\n"); // 0-0 } method Print(x: X, suffix: string) { - var y: X := *; + var y: X; print x, "-", y, suffix; } diff --git a/Test/git-issues/git-issue-610.dfy b/Test/git-issues/git-issue-610.dfy index 5e958f768ce..dc090e6ff6b 100644 --- a/Test/git-issues/git-issue-610.dfy +++ b/Test/git-issues/git-issue-610.dfy @@ -1,4 +1,4 @@ -// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment +// RUN: %testDafnyForEachCompiler "%s" type pos = i:int | i > 0 witness 1 diff --git a/Test/git-issues/git-issue-674.dfy b/Test/git-issues/git-issue-674.dfy index 30a22bd2f8f..d1643b53019 100644 --- a/Test/git-issues/git-issue-674.dfy +++ b/Test/git-issues/git-issue-674.dfy @@ -1,4 +1,4 @@ -// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment +// RUN: %testDafnyForEachCompiler "%s" type pos = i:int | i > 0 witness 1 diff --git a/Test/git-issues/git-issue-684.dfy b/Test/git-issues/git-issue-684.dfy index b1fbd7ab036..bf2983f1cdf 100644 --- a/Test/git-issues/git-issue-684.dfy +++ b/Test/git-issues/git-issue-684.dfy @@ -1,7 +1,7 @@ // RUN: %dafny /compile:0 "%s" > "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" +// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" // RUN: %diff "%s.expect" "%t" @@ -14,5 +14,3 @@ method TestNestedLet() { var Level2(u, Level1(v)) := x; } -method Main() {} - diff --git a/Test/git-issues/git-issue-784.dfy b/Test/git-issues/git-issue-784.dfy index 78b83f01064..ae71b0b8f47 100644 --- a/Test/git-issues/git-issue-784.dfy +++ b/Test/git-issues/git-issue-784.dfy @@ -1,7 +1,7 @@ // RUN: %dafny /compile:0 "%s" > "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" +// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" // RUN: %diff "%s.expect" "%t" @@ -31,5 +31,3 @@ datatype List = Nil | Cons(T, List) { x.AppAssoc(Concat(xs), Concat(l2)); } } - -method Main() {} diff --git a/Test/git-issues/git-issue-817.dfy b/Test/git-issues/git-issue-817.dfy index 006c718d256..e7ee0a13d6a 100644 --- a/Test/git-issues/git-issue-817.dfy +++ b/Test/git-issues/git-issue-817.dfy @@ -30,7 +30,6 @@ method m() returns (rr: Result) { assert d.v == 42; assert dd.v == 100; expect d.v == 42 && dd.v == 100; - rr := *; } method mm() returns (rr: Result) { @@ -46,7 +45,6 @@ method mm() returns (rr: Result) { print d[0], " ", dd[0], " ", d != dd, "\n"; // 42 100 true assert d[0] == 42 && dd[0] == 100; expect d[0] == 42 && dd[0] == 100; - rr := *; } method mmm() returns (rr: Result) { @@ -62,7 +60,6 @@ method mmm() returns (rr: Result) { print d[0,0], " ", dd[0,0], " ", d != dd, "\n"; // 42 100 true assert d[0,0] == 42 && dd[0,0] == 100; expect d[0,0] == 42 && dd[0,0] == 100; - rr := *; } class C { diff --git a/Test/git-issues/git-issue-817a.dfy b/Test/git-issues/git-issue-817a.dfy index 97826e1aea3..f4402a28f5e 100644 --- a/Test/git-issues/git-issue-817a.dfy +++ b/Test/git-issues/git-issue-817a.dfy @@ -35,7 +35,6 @@ method P() returns (r: Result){ assert a[7] == 200; assert c.data == 9; print c.data, " ", a[7], " ", a[9], "\n"; // 9 200 142 - r := *; } method Main() { diff --git a/Test/git-issues/git-issue-859.dfy b/Test/git-issues/git-issue-859.dfy index 461942b734d..991a447cd5e 100644 --- a/Test/git-issues/git-issue-859.dfy +++ b/Test/git-issues/git-issue-859.dfy @@ -6,9 +6,7 @@ datatype FailureCompatible = Make { function Extract(): (r: real) { 0.0 } } -method M() returns (r: FailureCompatible) { - r := *; -} +method M() returns (r: FailureCompatible) { } method N() returns (x: int) { var s: real :- M(); diff --git a/Test/libraries b/Test/libraries index 7c386fa0b4a..44f5891e7b5 160000 --- a/Test/libraries +++ b/Test/libraries @@ -1 +1 @@ -Subproject commit 7c386fa0b4a267715f9bd49948d1af68e1631e6b +Subproject commit 44f5891e7b5b21a5f13f139b22fb5559b46de36f diff --git a/Test/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect b/Test/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect index 67098a5e6cb..50785ca4277 100644 --- a/Test/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect +++ b/Test/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect @@ -6,8 +6,8 @@ Diff (changing expected into actual): Dafny program verifier did not attempt verification -System.Func`2[System.Numerics.BigInteger,System.Numerics.BigInteger] -+function (_3_x) { -+ return _3_x; ++function (_1_x) { ++ return _1_x; + } @@ -39,4 +39,5 @@ Diff (changing expected into actual): Executing on C++... +Executing on Dafny Library (.doo)... Executing on Simple Dafny... diff --git a/Test/unicodechars/comp/Arrays.dfy b/Test/unicodechars/comp/Arrays.dfy index e0aa3ea7b93..d206b7dc373 100644 --- a/Test/unicodechars/comp/Arrays.dfy +++ b/Test/unicodechars/comp/Arrays.dfy @@ -1,2 +1,2 @@ -// RUN: %testDafnyForEachCompiler "%s" -- --unicode-char +// RUN: %testDafnyForEachCompiler "%s" -- /unicodeChar:1 include "../../comp/Arrays.dfy" diff --git a/Test/unicodechars/git-issues/github-issue-2928.dfy b/Test/unicodechars/git-issues/github-issue-2928.dfy index 414164a8fe2..00d9026ba6a 100644 --- a/Test/unicodechars/git-issues/github-issue-2928.dfy +++ b/Test/unicodechars/git-issues/github-issue-2928.dfy @@ -1,3 +1,3 @@ -// RUN: %testDafnyForEachCompiler %s -- --unicode-char +// RUN: %testDafnyForEachCompiler %s -- /unicodeChar:1 include "../../git-issues/github-issue-2928.dfy" diff --git a/customBoogie.patch b/customBoogie.patch index af1c84b0564..897f7c4876a 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644 -- +- +