From 4d7bdf582e6a9c1b05063dac6130f65f196001a0 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 9 Nov 2023 15:36:44 -0800 Subject: [PATCH] feat: Execution branch coverage report (#4755) ### Description Implements an execution coverage report in the same format as the existing verification coverage and expected generated test coverage reports. Mainly this just meant using the existing low-level instrumentation provided by the old CLI `/coverage` option to write coverage data to a temporary file during execution, and then parsing this data and populating a `CoverageReport` object. I've only implemented this for C# for now, since the execution coverage SHOULD generally be identical across languages (the instrumentation is emitted from the common SinglePassCompiler) but it wouldn't take much work to hook it up for the other backends. Also adds this to the `DafnyStandardLibraries` project, and augments the existing coverage report generation to handle `.doo` files and Uris somewhat better. Also renames the existing verification option `--coverage-report` to `--verification-coverage-report`, since this option is almost always in scope (since most commands run verification), and for `dafny test` and `dafny run` "coverage report" more naturally means execution coverage instead. The former hasn't been released yet so this won't break anyone. :) Resolves #4671 ### How has this been tested? `comp/CoverageReport.dfy`, similar to the existing `logger/CoverageReport.dfy` --- .../Compilers/CSharp/Compiler-Csharp.cs | 33 +++ .../Compilers/CSharp/CsharpBackend.cs | 4 + .../Compilers/CoverageInstrumenter.cs | 33 ++- .../Compilers/Cplusplus/Compiler-cpp.cs | 3 +- .../Compilers/Dafny/Compiler-dafny.cs | 3 +- .../DafnyCore/Compilers/ExecutableBackend.cs | 1 + .../DafnyCore/Compilers/GoLang/Compiler-go.cs | 3 +- .../DafnyCore/Compilers/Java/Compiler-java.cs | 3 +- .../Compilers/JavaScript/Compiler-js.cs | 3 +- .../Compilers/Library/LibraryBackend.cs | 3 +- .../Compilers/Python/Compiler-python.cs | 3 +- .../DafnyCore/Compilers/SinglePassCompiler.cs | 1 - .../CoverageReport/CoverageReport.cs | 20 +- Source/DafnyCore/Feature.cs | 7 +- Source/DafnyCore/Options/CommonOptionBag.cs | 11 +- Source/DafnyCore/Options/DafnyCommands.cs | 3 +- .../DafnyCore/Plugins/IExecutableBackend.cs | 5 + Source/DafnyDriver/CompilerDriver.cs | 15 ++ Source/DafnyDriver/CoverageReporter.cs | 31 ++- Source/DafnyStandardLibraries/Makefile | 2 +- .../examples/WrappersExamples.dfy | 14 ++ .../LitTests/LitTest/comp/CoverageReport.dfy | 20 ++ .../LitTest/comp/CoverageReport.dfy.expect | 18 ++ ...overageReport.dfy_tests_actual.html.expect | 228 ++++++++++++++++++ .../LitTest/logger/CoverageReport.dfy | 4 +- docs/DafnyRef/Features.md | 3 +- docs/DafnyRef/UserGuide.md | 7 +- docs/dev/news/4625.feat | 2 +- docs/dev/news/4755.feat | 1 + 29 files changed, 437 insertions(+), 47 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy_tests_actual.html.expect create mode 100644 docs/dev/news/4755.feat diff --git a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs index fb15f0fbc33..c0dcd391747 100644 --- a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs +++ b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs @@ -79,6 +79,11 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) { wr.WriteLine("using System;"); wr.WriteLine("using System.Numerics;"); wr.WriteLine("using System.Collections;"); + + if (Options.Get(CommonOptionBag.ExecutionCoverageReport) != null) { + wr.WriteLine("using System.IO;"); + } + if (program.Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.OmitAllOtherModules) { wr.WriteLine("#endif"); } @@ -95,6 +100,9 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) { EmitRuntimeSource("DafnyRuntimeCsharp", wr, false); } + if (Options.Get(CommonOptionBag.ExecutionCoverageReport) != null) { + EmitCoverageReportInstrumentation(program, wr); + } } /// @@ -3435,5 +3443,30 @@ protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageV TrStmt(recoveryBody, catchBlock); } + protected void EmitCoverageReportInstrumentation(Program program, ConcreteSyntaxTree wr) { + wr.WriteLine(@" +namespace DafnyProfiling { + public class CodeCoverage { + static uint[] tallies; + static string talliesFileName; + public static void Setup(int size, string theTalliesFileName) { + tallies = new uint[size]; + talliesFileName = theTalliesFileName; + } + public static void TearDown() { + using TextWriter talliesWriter = new StreamWriter( + new FileStream(talliesFileName, FileMode.Create)); + for (var i = 0; i < tallies.Length; i++) { + talliesWriter.WriteLine(""{0}"", tallies[i]); + } + tallies = null; + } + public static bool Record(int id) { + tallies[id]++; + return true; + } + } +}"); + } } } diff --git a/Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs b/Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs index 23fd88722f8..a8e66b2e186 100644 --- a/Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs +++ b/Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs @@ -158,6 +158,10 @@ public override bool RunTargetProgram(string dafnyProgramName, string targetProg return RunProcess(psi, outputWriter, errorWriter) == 0; } + public override void PopulateCoverageReport(CoverageReport coverageReport) { + compiler.Coverage.PopulateCoverageReport(coverageReport); + } + public CsharpBackend(DafnyOptions options) : base(options) { } } diff --git a/Source/DafnyCore/Compilers/CoverageInstrumenter.cs b/Source/DafnyCore/Compilers/CoverageInstrumenter.cs index 0167bae5816..dc02c7786f1 100644 --- a/Source/DafnyCore/Compilers/CoverageInstrumenter.cs +++ b/Source/DafnyCore/Compilers/CoverageInstrumenter.cs @@ -1,18 +1,25 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.IO; +using System.Linq; namespace Microsoft.Dafny.Compilers; public class CoverageInstrumenter { private readonly SinglePassCompiler compiler; private List<(IToken, string)>/*?*/ legend; // non-null implies options.CoverageLegendFile is non-null + private string talliesFilePath; public CoverageInstrumenter(SinglePassCompiler compiler) { this.compiler = compiler; - if (compiler.Options?.CoverageLegendFile != null) { + if (compiler.Options?.CoverageLegendFile != null + || compiler.Options?.Get(CommonOptionBag.ExecutionCoverageReport) != null) { legend = new List<(IToken, string)>(); } + + if (compiler.Options?.Get(CommonOptionBag.ExecutionCoverageReport) != null) { + talliesFilePath = Path.GetTempFileName(); + } } public bool IsRecording { @@ -55,7 +62,11 @@ public void InstrumentExpr(IToken tok, string description, bool resultValue, Con public void EmitSetup(ConcreteSyntaxTree wr) { Contract.Requires(wr != null); if (legend != null) { - wr.Write("DafnyProfiling.CodeCoverage.Setup({0})", legend.Count); + wr.Write("DafnyProfiling.CodeCoverage.Setup({0}", legend.Count); + if (talliesFilePath != null) { + wr.Write($", \"{talliesFilePath}\""); + } + wr.Write(")"); compiler.EndStmt(wr); } } @@ -69,7 +80,7 @@ public void EmitTearDown(ConcreteSyntaxTree wr) { } public void WriteLegendFile() { - if (legend != null) { + if (compiler.Options?.CoverageLegendFile != 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)); @@ -82,4 +93,20 @@ public void WriteLegendFile() { legend = null; } } + + public void PopulateCoverageReport(CoverageReport coverageReport) { + var coverageReportDir = compiler.Options?.Get(CommonOptionBag.ExecutionCoverageReport); + if (coverageReportDir != null) { + var tallies = File.ReadLines(talliesFilePath).Select(int.Parse).ToArray(); + foreach (var ((token, _), tally) in legend.Zip(tallies)) { + var label = tally == 0 ? CoverageLabel.NotCovered : CoverageLabel.FullyCovered; + // For now we only identify branches at the line granularity, + // which matches what `dafny generate-tests ... --coverage-report` does as well. + var rangeToken = new RangeToken(new Token(token.line, 1), new Token(token.line + 1, 0)); + rangeToken.Uri = token.Uri; + coverageReport.LabelCode(rangeToken, label); + } + } + } + } diff --git a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs index 22e5264b7eb..7f7b64650c1 100644 --- a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs +++ b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs @@ -56,7 +56,8 @@ public CppCompiler(DafnyOptions options, ErrorReporter reporter, ReadOnlyCollect Feature.MethodSynthesis, Feature.UnicodeChars, Feature.ConvertingValuesToStrings, - Feature.BuiltinsInRuntime + Feature.BuiltinsInRuntime, + Feature.RuntimeCoverageReport }; private List datatypeDecls = new(); diff --git a/Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs b/Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs index 24d642317a9..2e5c9d44227 100644 --- a/Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs +++ b/Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs @@ -91,7 +91,8 @@ public static void throwGeneralUnsupported() { Feature.SubtypeConstraintsInQuantifiers, Feature.TuplesWiderThan20, Feature.ForLoops, - Feature.Traits + Feature.Traits, + Feature.RuntimeCoverageReport }; private readonly List Imports = new() { DafnyDefaultModule }; diff --git a/Source/DafnyCore/Compilers/ExecutableBackend.cs b/Source/DafnyCore/Compilers/ExecutableBackend.cs index 7f2da678ec2..322c0fc6ebf 100644 --- a/Source/DafnyCore/Compilers/ExecutableBackend.cs +++ b/Source/DafnyCore/Compilers/ExecutableBackend.cs @@ -1,6 +1,7 @@ using System; using System.Collections.Generic; using System.Collections.ObjectModel; +using System.CommandLine; using System.Data.SqlTypes; using System.Diagnostics; using System.Diagnostics.Contracts; diff --git a/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs b/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs index 4afc2b63b91..43aae8a70ce 100644 --- a/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs +++ b/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs @@ -27,7 +27,8 @@ public GoCompiler(DafnyOptions options, ErrorReporter reporter) : base(options, Feature.MethodSynthesis, Feature.ExternalConstructors, Feature.SubsetTypeTests, - Feature.AllUnderscoreExternalModuleNames + Feature.AllUnderscoreExternalModuleNames, + Feature.RuntimeCoverageReport }; public override string ModuleSeparator => "_"; diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs index ea0375dd708..f41a92e9196 100644 --- a/Source/DafnyCore/Compilers/Java/Compiler-java.cs +++ b/Source/DafnyCore/Compilers/Java/Compiler-java.cs @@ -29,7 +29,8 @@ public JavaCompiler(DafnyOptions options, ErrorReporter reporter) : base(options Feature.MethodSynthesis, Feature.TuplesWiderThan20, Feature.ArraysWithMoreThan16Dims, - Feature.ArrowsWithMoreThan16Arguments + Feature.ArrowsWithMoreThan16Arguments, + Feature.RuntimeCoverageReport, }; const string DafnySetClass = "dafny.DafnySet"; diff --git a/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs b/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs index 55e9b81b114..8d08c2cdd32 100644 --- a/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs +++ b/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs @@ -26,7 +26,8 @@ public JavaScriptCompiler(DafnyOptions options, ErrorReporter reporter) : base(o Feature.MethodSynthesis, Feature.ExternalConstructors, Feature.SubsetTypeTests, - Feature.SeparateCompilation + Feature.SeparateCompilation, + Feature.RuntimeCoverageReport }; public override string ModuleSeparator => "_"; diff --git a/Source/DafnyCore/Compilers/Library/LibraryBackend.cs b/Source/DafnyCore/Compilers/Library/LibraryBackend.cs index bb10038713e..d245ce4941a 100644 --- a/Source/DafnyCore/Compilers/Library/LibraryBackend.cs +++ b/Source/DafnyCore/Compilers/Library/LibraryBackend.cs @@ -28,7 +28,8 @@ public override string TargetBaseDir(string dafnyProgramName) => public override bool SupportsInMemoryCompilation => false; public override IReadOnlySet UnsupportedFeatures => new HashSet { - Feature.LegacyCLI + Feature.LegacyCLI, + Feature.RuntimeCoverageReport }; // Necessary since Compiler is null diff --git a/Source/DafnyCore/Compilers/Python/Compiler-python.cs b/Source/DafnyCore/Compilers/Python/Compiler-python.cs index 7ed0d05a1da..ba5e59ed0ae 100644 --- a/Source/DafnyCore/Compilers/Python/Compiler-python.cs +++ b/Source/DafnyCore/Compilers/Python/Compiler-python.cs @@ -34,7 +34,8 @@ public PythonCompiler(DafnyOptions options, ErrorReporter reporter) : base(optio public override IReadOnlySet UnsupportedFeatures => new HashSet { Feature.SubsetTypeTests, - Feature.MethodSynthesis + Feature.MethodSynthesis, + Feature.RuntimeCoverageReport }; public override string ModuleSeparator => "_"; diff --git a/Source/DafnyCore/Compilers/SinglePassCompiler.cs b/Source/DafnyCore/Compilers/SinglePassCompiler.cs index 322523494c6..85f90102a1d 100644 --- a/Source/DafnyCore/Compilers/SinglePassCompiler.cs +++ b/Source/DafnyCore/Compilers/SinglePassCompiler.cs @@ -6058,6 +6058,5 @@ private bool IsComparisonWithZeroOnRight( } protected abstract void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody, ConcreteSyntaxTree wr); - } } diff --git a/Source/DafnyCore/CoverageReport/CoverageReport.cs b/Source/DafnyCore/CoverageReport/CoverageReport.cs index e8b1532e420..3e2bb0c5cce 100644 --- a/Source/DafnyCore/CoverageReport/CoverageReport.cs +++ b/Source/DafnyCore/CoverageReport/CoverageReport.cs @@ -11,7 +11,7 @@ public class CoverageReport { private static int nextUniqueId = 0; - private readonly Dictionary> labelsByFile; + private readonly Dictionary> labelsByFile; public readonly string Name; // the name to assign to this coverage report public readonly string Units; // the units of coverage (plural). This will be written in the coverage report table. private readonly string suffix; // user-provided suffix to add to filenames that are part of this report @@ -40,17 +40,17 @@ public CoverageReport(string name, string units, string suffix, Program program) /// Assign a coverage label to the code indicated by the range token. /// public void LabelCode(RangeToken span, CoverageLabel label) { - Contract.Assert(labelsByFile.ContainsKey(span.ActualFilename)); - var labeledFile = labelsByFile[span.ActualFilename]; + Contract.Assert(labelsByFile.ContainsKey(span.Uri)); + var labeledFile = labelsByFile[span.Uri]; var coverageSpan = new CoverageSpan(span, label); labeledFile.Add(coverageSpan); } - public IEnumerable CoverageSpansForFile(string fileName) { - return labelsByFile.GetOrDefault(fileName, () => new List()); + public IEnumerable CoverageSpansForFile(Uri uri) { + return labelsByFile.GetOrDefault(uri, () => new List()); } - public IEnumerable AllFiles() { + public IEnumerable AllFiles() { return labelsByFile.Keys; } @@ -59,14 +59,14 @@ public void RegisterFiles(Program program) { } public void RegisterFile(Uri uri) { - if (!labelsByFile.ContainsKey(uri.LocalPath)) { - labelsByFile[uri.LocalPath] = new List(); + if (!labelsByFile.ContainsKey(uri)) { + labelsByFile[uri] = new List(); } } private void RegisterFiles(Node astNode) { - if (astNode.StartToken.ActualFilename != null && !labelsByFile.ContainsKey(astNode.StartToken.ActualFilename)) { - labelsByFile[astNode.StartToken.ActualFilename] = new(); + if (astNode.StartToken.ActualFilename != null && !labelsByFile.ContainsKey(astNode.StartToken.Uri)) { + labelsByFile[astNode.StartToken.Uri] = new(); } foreach (var declaration in astNode.Children.OfType()) { diff --git a/Source/DafnyCore/Feature.cs b/Source/DafnyCore/Feature.cs index 7130bc3dfe7..82958d87c81 100644 --- a/Source/DafnyCore/Feature.cs +++ b/Source/DafnyCore/Feature.cs @@ -183,8 +183,11 @@ and where at least one variable has potentially infinite bounds. [FeatureDescription("Separate compilation", "sec-compilation")] SeparateCompilation, - [FeatureDescription("All built-in types in runtime library", "#sec-compilation-built-ins")] - BuiltinsInRuntime + [FeatureDescription("All built-in types in runtime library", "sec-compilation-built-ins")] + BuiltinsInRuntime, + + [FeatureDescription("Execution coverage report", "sec-dafny-test")] + RuntimeCoverageReport } public class UnsupportedFeatureException : Exception { diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index 87962f5c921..3f23b1a1dc5 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -214,14 +214,18 @@ May slow down verification slightly. May produce spurious warnings.") { IsHidden = true }; - public static readonly Option VerificationCoverageReport = new("--coverage-report", - "Emit verification coverage report to a given directory, in the same format as a test coverage report.") { + public static readonly Option VerificationCoverageReport = new("--verification-coverage-report", + "Emit verification coverage report to a given directory, in the same format as a test coverage report.") { ArgumentHelpName = "directory" }; public static readonly Option NoTimeStampForCoverageReport = new("--no-timestamp-for-coverage-report", "Write coverage report directly to the specified folder instead of creating a timestamped subdirectory.") { IsHidden = true }; + public static readonly Option ExecutionCoverageReport = new("--coverage-report", + "Emit execution coverage report to a given directory.") { + ArgumentHelpName = "directory" + }; public static readonly Option IncludeRuntimeOption = new("--include-runtime", "Include the Dafny runtime as source in the target language."); @@ -517,7 +521,8 @@ void ParsePrintMode(Option option, Boogie.CommandLineParseState ps, UseStandardLibraries, OptimizeErasableDatatypeWrapper, AddCompileSuffix, - SystemModule + SystemModule, + ExecutionCoverageReport ); } diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs index 1becf3d1e49..28edb04304f 100644 --- a/Source/DafnyCore/Options/DafnyCommands.cs +++ b/Source/DafnyCore/Options/DafnyCommands.cs @@ -59,7 +59,8 @@ static DafnyCommands() { public static IReadOnlyList