From 6a39d5c1c6e50c9264a66d3683089e4ec7652d16 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 18 Nov 2021 23:16:08 +0100 Subject: [PATCH] fix: missing targetFilename leads to wrong location of generated files (#1598) * always generate targetFilename * test need to look at the correct location * refactor further * remove needless transformation * tune name --- Source/DafnyDriver/DafnyDriver.cs | 45 ++++++++++++------- Test/comp/compile1quiet/CompileRunQuietly.dfy | 2 +- .../compile1verbose/CompileAndThenRun.dfy | 2 +- 3 files changed, 30 insertions(+), 19 deletions(-) diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 0bc43884898..addf840c226 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -597,8 +597,14 @@ public override void ReportBplError(IToken tok, string message, bool error, Text #region Compilation - static string WriteDafnyProgramToFiles(Compiler compiler, string dafnyProgramName, bool targetProgramHasErrors, - string targetProgramText, string/*?*/ callToMain, Dictionary otherFiles, TextWriter outputWriter) { + private record TargetPaths(string Directory, string Filename) { + private Func DeleteDot = p => p == "." ? "" : p; + public string RelativeDirectory => DeleteDot(Path.GetRelativePath(Directory, Path.GetDirectoryName(Filename))); + public string RelativeFilename => DeleteDot(Path.GetRelativePath(Directory, Filename)); + public string SourceDirectory => Path.GetDirectoryName(Filename); + } + + private static TargetPaths GenerateTargetPaths(Compiler compiler, string dafnyProgramName) { string targetExtension; string baseName = Path.GetFileNameWithoutExtension(dafnyProgramName); string targetBaseDir = ""; @@ -633,34 +639,39 @@ static string WriteDafnyProgramToFiles(Compiler compiler, string dafnyProgramNam // Note that using Path.ChangeExtension here does the wrong thing when dafnyProgramName has multiple periods (e.g., a.b.dfy) string targetBaseName = baseName + "." + targetExtension; string targetDir = Path.Combine(Path.GetDirectoryName(dafnyProgramName), targetBaseDir); + + string targetFilename = Path.Combine(targetDir, targetBaseName); + + return new TargetPaths(Directory: Path.GetDirectoryName(dafnyProgramName), Filename: targetFilename); + } + + static void WriteDafnyProgramToFiles(TargetPaths paths, bool targetProgramHasErrors, string targetProgramText, + string/*?*/ callToMain, Dictionary otherFiles, TextWriter outputWriter) { // WARNING: Make sure that Directory.Delete is only called when the compilation target is Java. // If called during C# or JS compilation, you will lose your entire target directory. // Purpose is to delete the old generated folder with the Java compilation output and replace all contents. - if (DafnyOptions.O.CompileTarget is DafnyOptions.CompilationTarget.Java && Directory.Exists(targetDir)) { - Directory.Delete(targetDir, true); + if (DafnyOptions.O.CompileTarget is DafnyOptions.CompilationTarget.Java && Directory.Exists(paths.SourceDirectory)) { + Directory.Delete(paths.SourceDirectory, true); } - string targetFilename = Path.Combine(targetDir, targetBaseName); - WriteFile(targetFilename, targetProgramText, callToMain); - string relativeTarget = Path.Combine(targetBaseDir, targetBaseName); + WriteFile(paths.Filename, targetProgramText, callToMain); + if (targetProgramHasErrors) { // Something went wrong during compilation (e.g., the compiler may have found an "assume" statement). // As a courtesy, we're still printing the text of the generated target program. We print a message regardless // of the CompileVerbose settings. - outputWriter.WriteLine("Wrote textual form of partial target program to {0}", relativeTarget); + outputWriter.WriteLine("Wrote textual form of partial target program to {0}", paths.RelativeFilename); } else if (DafnyOptions.O.CompileVerbose) { - outputWriter.WriteLine("Wrote textual form of target program to {0}", relativeTarget); + outputWriter.WriteLine("Wrote textual form of target program to {0}", paths.RelativeFilename); } foreach (var entry in otherFiles) { var filename = entry.Key; - WriteFile(Path.Combine(targetDir, filename), entry.Value); + WriteFile(Path.Join(paths.SourceDirectory, filename), entry.Value); if (DafnyOptions.O.CompileVerbose) { - outputWriter.WriteLine("Additional target code written to {0}", Path.Combine(targetBaseDir, filename)); + outputWriter.WriteLine("Additional target code written to {0}", Path.Join(paths.RelativeDirectory, filename)); } } - - return targetFilename; } static void WriteFile(string filename, string text, string moreText = null) { @@ -750,10 +761,10 @@ public static bool CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyP compiler.Coverage.WriteLegendFile(); // blurt out the code to a file, if requested, or if other target-language files were specified on the command line. - string targetFilename = null; + var paths = GenerateTargetPaths(compiler, dafnyProgramName); if (DafnyOptions.O.SpillTargetCode > 0 || otherFileNames.Count > 0 || (invokeCompiler && !compiler.SupportsInMemoryCompilation) || (invokeCompiler && compiler.TextualTargetIsExecutable && !DafnyOptions.O.RunAfterCompile)) { - targetFilename = WriteDafnyProgramToFiles(compiler, dafnyProgramName, targetProgramHasErrors, targetProgramText, callToMain, otherFiles, outputWriter); + WriteDafnyProgramToFiles(paths, targetProgramHasErrors, targetProgramText, callToMain, otherFiles, outputWriter); } if (targetProgramHasErrors) { @@ -765,7 +776,7 @@ public static bool CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyP } // compile the program into an assembly - var compiledCorrectly = compiler.CompileTargetProgram(dafnyProgramName, targetProgramText, callToMain, targetFilename, otherFileNames, + var compiledCorrectly = compiler.CompileTargetProgram(dafnyProgramName, targetProgramText, callToMain, paths.Filename, otherFileNames, hasMain && DafnyOptions.O.RunAfterCompile, outputWriter, out var compilationResult); if (compiledCorrectly && DafnyOptions.O.RunAfterCompile) { if (hasMain) { @@ -773,7 +784,7 @@ public static bool CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyP outputWriter.WriteLine("Running..."); outputWriter.WriteLine(); } - compiledCorrectly = compiler.RunTargetProgram(dafnyProgramName, targetProgramText, callToMain, targetFilename, otherFileNames, compilationResult, outputWriter); + compiledCorrectly = compiler.RunTargetProgram(dafnyProgramName, targetProgramText, callToMain, paths.Filename, otherFileNames, compilationResult, outputWriter); } else { // make sure to give some feedback to the user if (DafnyOptions.O.CompileVerbose) { diff --git a/Test/comp/compile1quiet/CompileRunQuietly.dfy b/Test/comp/compile1quiet/CompileRunQuietly.dfy index 610c2545de1..64f50d91e71 100644 --- a/Test/comp/compile1quiet/CompileRunQuietly.dfy +++ b/Test/comp/compile1quiet/CompileRunQuietly.dfy @@ -1,5 +1,5 @@ // RUN: %dafny /compileTarget:cs "%s" > "%t" -// RUN: dotnet CompileRunQuietly.dll >> "%t" +// RUN: dotnet %S/CompileRunQuietly.dll >> "%t" // RUN: %dafny /compileTarget:js "%s" >> "%t" // RUN: node %S/CompileRunQuietly.js >> "%t" diff --git a/Test/comp/compile1verbose/CompileAndThenRun.dfy b/Test/comp/compile1verbose/CompileAndThenRun.dfy index a5d7fb7fe25..49ea197348b 100644 --- a/Test/comp/compile1verbose/CompileAndThenRun.dfy +++ b/Test/comp/compile1verbose/CompileAndThenRun.dfy @@ -1,5 +1,5 @@ // RUN: %dafny /compileVerbose:1 /compileTarget:cs "%s" > "%t" -// RUN: dotnet CompileAndThenRun.dll >> "%t" +// RUN: dotnet %S/CompileAndThenRun.dll >> "%t" // RUN: %dafny /compileVerbose:1 /compileTarget:js "%s" >> "%t" // RUN: node %S/CompileAndThenRun.js >> "%t"