Slightly hacky working first pass

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>
@@ -3434,6 +3442,31 @@ protected class ClassWriter : IClassWriter {
  catchBlock.WriteLine($"var {haltMessageVarName} = Dafny.Sequence<{CharTypeName}>.{CharMethodQualifier}FromString(e.Message);");
  TrStmt(recoveryBody, catchBlock);
  }
-
+
+ protected override 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/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,14 @@ public class CoverageInstrumenter {
  legend = null;
  }
  }
+
+ public void PopulateCoverageReport(CoverageReport report) {
+ var tallies = File.ReadLines(talliesFilePath).Select(int.Parse).ToArray();
+ foreach (var ((token, description), tally) in legend.Zip(tallies)) {
+ var label = tally == 0 ? CoverageLabel.NotCovered : CoverageLabel.FullyCovered;
+ // TODO: more intelligent conversion to range token
+ report.LabelCode(new RangeToken(token, token), label);
+ }
+ }
+
 }

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;
@@ -69,6 +70,10 @@ public abstract class ExecutableBackend : IExecutableBackend {
  Compiler.Coverage.WriteLegendFile();
  }
 
+ public override CoverageInstrumenter GetCoverageAfterRun() {
+ return Compiler.Coverage;
+ }
+
  protected abstract SinglePassCompiler CreateCompiler();
 
  public override string PublicIdProtect(string name) {

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -6062,5 +6062,8 @@ private class ArrayLvalueImpl : ILvalue {
 
  protected abstract void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody, ConcreteSyntaxTree wr);
 
+ protected virtual void EmitCoverageReportInstrumentation(Program program, ConcreteSyntaxTree wr) {
+ throw new UnsupportedFeatureException(program.GetStartOfFirstFileToken(), Feature.RuntimeCoverageReport);
+ }
  }
 }

Source/DafnyCore/Feature.cs

@@ -184,7 +184,10 @@ public enum Feature {
  SeparateCompilation,
 
  [FeatureDescription("All built-in types in runtime library", "#sec-compilation-built-ins")]
- BuiltinsInRuntime
+ BuiltinsInRuntime,
+
+ [FeatureDescription("Runtime coverage report", "#sec-compilation-built-ins")]
+ RuntimeCoverageReport
 }
 
 public class UnsupportedFeatureException : Exception {

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -215,13 +215,17 @@ public enum GeneralTraitsOptions {
  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.") {
+ "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("--test-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;
 
@@ -131,6 +132,8 @@ public abstract class IExecutableBackend {
  /// </summary>
  public virtual void OnPostCompile() { }
 
+ public abstract CoverageInstrumenter GetCoverageAfterRun();
+
  /// <summary>
  /// Remove previously generated source files. This is only applicable to compilers that put sources in a separate
  /// directory (e.g. Java). For other compilers, this method should do nothing.

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;
 
@@ -559,6 +560,16 @@ 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 coverage = compiler.GetCoverageAfterRun();
+ var coverageReport = new CoverageReport("Test Coverage", "Branches", "_tests_actual", dafnyProgram);
+ coverage.PopulateCoverageReport(coverageReport);
+ new CoverageReporter(options).SerializeCoverageReports(coverageReport, coverageReportDir);
+ }
+ }
  } else {
  // make sure to give some feedback to the user
  if (options.Verbose) {
@@ -614,6 +625,10 @@ class NoExecutableBackend : IExecutableBackend {
  throw new NotSupportedException();
  }
 
+ public override CoverageInstrumenter GetCoverageAfterRun() {
+ throw new NotImplementedException();
+ }
+
  public NoExecutableBackend([NotNull] DafnyOptions options) : base(options) {
  }
  }

Source/DafnyRuntime/DafnyRuntime.cs

@@ -1948,4 +1948,21 @@ public class HaltException : Exception {
  public HaltException(object message) : base(message.ToString()) {
  }
  }
+
+ public class CodeCoverage {
+ static uint[] tallies;
+ public static void Setup(int size) {
+ tallies = new uint[size];
+ }
+ public static void TearDown() {
+ for (var i = 0; i < tallies.Length; i++) {
+ Console.WriteLine("{0}: {1}", i, tallies[i]);
+ }
+ tallies = null;
+ }
+ public static bool Record(int id) {
+ tallies[id]++;
+ return true;
+ }
+ }
 }