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`

Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs

@@ -79,6 +79,11 @@ public class CsharpCompiler : SinglePassCompiler {
  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 @@ public class CsharpCompiler : SinglePassCompiler {
  EmitRuntimeSource("DafnyRuntimeCsharp", wr, false);
  }
 
+ if (Options.Get(CommonOptionBag.ExecutionCoverageReport) != null) {
+ EmitCoverageReportInstrumentation(program, wr);
+ }
  }
 
  /// <summary>
@@ -3435,5 +3443,30 @@ protected class ClassWriter : IClassWriter {
  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;
+ }
+ }
+}");
+ }
  }
 }

Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs

@@ -158,6 +158,10 @@ private class CSharpCompilationResult {
  return RunProcess(psi, outputWriter, errorWriter) == 0;
  }
 
+ public override void PopulateCoverageReport(CoverageReport coverageReport) {
+ compiler.Coverage.PopulateCoverageReport(coverageReport);
+ }
+
  public CsharpBackend(DafnyOptions options) : base(options) {
  }
 }

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 class CoverageInstrumenter {
  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 class CoverageInstrumenter {
  }
 
  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 class CoverageInstrumenter {
  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);
+ }
+ }
+ }
+
 }

Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs

@@ -56,7 +56,8 @@ class CppCompiler : SinglePassCompiler {
  Feature.MethodSynthesis,
  Feature.UnicodeChars,
  Feature.ConvertingValuesToStrings,
- Feature.BuiltinsInRuntime
+ Feature.BuiltinsInRuntime,
+ Feature.RuntimeCoverageReport
  };
 
  private List<DatatypeDecl> datatypeDecls = new();

Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs

@@ -91,7 +91,8 @@ class DafnyCompiler : SinglePassCompiler {
  Feature.SubtypeConstraintsInQuantifiers,
  Feature.TuplesWiderThan20,
  Feature.ForLoops,
- Feature.Traits
+ Feature.Traits,
+ Feature.RuntimeCoverageReport
  };
 
  private readonly List<string> Imports = new() { DafnyDefaultModule };

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;

Source/DafnyCore/Compilers/GoLang/Compiler-go.cs

@@ -27,7 +27,8 @@ class GoCompiler : SinglePassCompiler {
  Feature.MethodSynthesis,
  Feature.ExternalConstructors,
  Feature.SubsetTypeTests,
- Feature.AllUnderscoreExternalModuleNames
+ Feature.AllUnderscoreExternalModuleNames,
+ Feature.RuntimeCoverageReport
  };
 
  public override string ModuleSeparator => "_";

Source/DafnyCore/Compilers/Java/Compiler-java.cs

@@ -29,7 +29,8 @@ public class JavaCompiler : SinglePassCompiler {
  Feature.MethodSynthesis,
  Feature.TuplesWiderThan20,
  Feature.ArraysWithMoreThan16Dims,
- Feature.ArrowsWithMoreThan16Arguments
+ Feature.ArrowsWithMoreThan16Arguments,
+ Feature.RuntimeCoverageReport,
  };
 
  const string DafnySetClass = "dafny.DafnySet";

Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs

@@ -26,7 +26,8 @@ class JavaScriptCompiler : SinglePassCompiler {
  Feature.MethodSynthesis,
  Feature.ExternalConstructors,
  Feature.SubsetTypeTests,
- Feature.SeparateCompilation
+ Feature.SeparateCompilation,
+ Feature.RuntimeCoverageReport
  };
 
  public override string ModuleSeparator => "_";

Source/DafnyCore/Compilers/Library/LibraryBackend.cs

@@ -28,7 +28,8 @@ public class LibraryBackend : ExecutableBackend {
  public override bool SupportsInMemoryCompilation => false;
 
  public override IReadOnlySet<Feature> UnsupportedFeatures => new HashSet<Feature> {
- Feature.LegacyCLI
+ Feature.LegacyCLI,
+ Feature.RuntimeCoverageReport
  };
 
  // Necessary since Compiler is null

Source/DafnyCore/Compilers/Python/Compiler-python.cs

@@ -34,7 +34,8 @@ class PythonCompiler : SinglePassCompiler {
 
  public override IReadOnlySet<Feature> UnsupportedFeatures => new HashSet<Feature> {
  Feature.SubsetTypeTests,
- Feature.MethodSynthesis
+ Feature.MethodSynthesis,
+ Feature.RuntimeCoverageReport
  };
 
  public override string ModuleSeparator => "_";

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -6058,6 +6058,5 @@ private class ArrayLvalueImpl : ILvalue {
  }
 
  protected abstract void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody, ConcreteSyntaxTree wr);
-
  }
 }

Source/DafnyCore/CoverageReport/CoverageReport.cs

@@ -11,7 +11,7 @@ public class CoverageReport {
 
  private static int nextUniqueId = 0;
 
- private readonly Dictionary<string, List<CoverageSpan>> labelsByFile;
+ private readonly Dictionary<Uri, List<CoverageSpan>> 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 class CoverageReport {
  /// Assign a coverage label to the code indicated by the <param name="span"></param> range token.
  /// </summary>
  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<CoverageSpan> CoverageSpansForFile(string fileName) {
- return labelsByFile.GetOrDefault(fileName, () => new List<CoverageSpan>());
+ public IEnumerable<CoverageSpan> CoverageSpansForFile(Uri uri) {
+ return labelsByFile.GetOrDefault(uri, () => new List<CoverageSpan>());
  }
 
- public IEnumerable<string> AllFiles() {
+ public IEnumerable<Uri> AllFiles() {
  return labelsByFile.Keys;
  }
 
@@ -59,14 +59,14 @@ public class CoverageReport {
  }
 
  public void RegisterFile(Uri uri) {
- if (!labelsByFile.ContainsKey(uri.LocalPath)) {
- labelsByFile[uri.LocalPath] = new List<CoverageSpan>();
+ if (!labelsByFile.ContainsKey(uri)) {
+ labelsByFile[uri] = new List<CoverageSpan>();
  }
  }
 
  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<LiteralModuleDecl>()) {

Source/DafnyCore/Feature.cs

@@ -183,8 +183,11 @@ public enum Feature {
  [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 {

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -214,14 +214,18 @@ public enum GeneralTraitsOptions {
 May produce spurious warnings.") {
  IsHidden = true
  };
- public static readonly Option<string> 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<string> 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<bool> 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<string> ExecutionCoverageReport = new("--coverage-report",
+ "Emit execution coverage report to a given directory.") {
+ ArgumentHelpName = "directory"
+ };
 
  public static readonly Option<bool> IncludeRuntimeOption = new("--include-runtime",
  "Include the Dafny runtime as source in the target language.");
@@ -517,7 +521,8 @@ public enum DefaultFunctionOpacityOptions {
  UseStandardLibraries,
  OptimizeErasableDatatypeWrapper,
  AddCompileSuffix,
- SystemModule
+ SystemModule,
+ ExecutionCoverageReport
  );
  }
 

Source/DafnyCore/Options/DafnyCommands.cs

@@ -59,7 +59,8 @@ public static class DafnyCommands {
  public static IReadOnlyList<Option> ExecutionOptions = new Option[] {
  CommonOptionBag.Target,
  CommonOptionBag.SpillTranslation,
- CommonOptionBag.InternalIncludeRuntimeOptionForExecution
+ CommonOptionBag.InternalIncludeRuntimeOptionForExecution,
+ CommonOptionBag.ExecutionCoverageReport
  }.Concat(TranslationOptions).ToList();
 
  public static IReadOnlyList<Option> ConsoleOutputOptions = new List<Option>(new Option[] {

Source/DafnyCore/Plugins/IExecutableBackend.cs

@@ -8,6 +8,7 @@
 using System.IO;
 using System.Linq;
 using DafnyCore;
+using Microsoft.Dafny.Compilers;
 
 namespace Microsoft.Dafny.Plugins;
 
@@ -197,4 +198,8 @@ public abstract class IExecutableBackend {
  public virtual Command GetCommand() {
  return new Command(TargetId, $"Translate Dafny sources to {TargetName} source and build files.");
  }
+
+ public virtual void PopulateCoverageReport(CoverageReport coverageReport) {
+ throw new NotImplementedException();
+ }
 }

Source/DafnyDriver/CompilerDriver.cs

@@ -24,6 +24,7 @@
 using Bpl = Microsoft.Boogie;
 using System.Diagnostics;
 using JetBrains.Annotations;
+using Microsoft.Dafny.Compilers;
 using Microsoft.Dafny.LanguageServer.CounterExampleGeneration;
 using Microsoft.Dafny.Plugins;
 
@@ -492,6 +493,11 @@ private record TargetPaths(string Directory, string Filename) {
  options.Backend.InstrumentCompiler(compilerInstrumenter, dafnyProgram);
  }
 
+ if (options.Get(CommonOptionBag.ExecutionCoverageReport) != null
+ && options.Backend.UnsupportedFeatures.Contains(Feature.RuntimeCoverageReport)) {
+ throw new UnsupportedFeatureException(dafnyProgram.GetStartOfFirstFileToken(), Feature.RuntimeCoverageReport);
+ }
+
  var compiler = options.Backend;
 
  var hasMain = Compilers.SinglePassCompiler.HasMain(dafnyProgram, out var mainMethod);
@@ -559,6 +565,15 @@ private record TargetPaths(string Directory, string Filename) {
 
  compiledCorrectly = compiler.RunTargetProgram(dafnyProgramName, targetProgramText, callToMain,
  targetPaths.Filename, otherFileNames, compilationResult, outputWriter, errorWriter);
+
+ if (compiledCorrectly) {
+ var coverageReportDir = options.Get(CommonOptionBag.ExecutionCoverageReport);
+ if (coverageReportDir != null) {
+ var coverageReport = new CoverageReport("Execution Coverage", "Branches", "_tests_actual", dafnyProgram);
+ compiler.PopulateCoverageReport(coverageReport);
+ new CoverageReporter(options).SerializeCoverageReports(coverageReport, coverageReportDir);
+ }
+ }
  } else {
  // make sure to give some feedback to the user
  if (options.Verbose) {