feat: Execution branch coverage report

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) {