From a70859f06ae78cc8551b6dad28ff0a4c23370fbf Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Tue, 7 Nov 2023 14:46:39 -0800
Subject: [PATCH 01/15] Slightly hacky working first pass

---
 .../Compilers/CSharp/Compiler-Csharp.cs       | 35 ++++++++++++++++++-
 .../Compilers/CoverageInstrumenter.cs         | 27 ++++++++++++--
 .../DafnyCore/Compilers/ExecutableBackend.cs  |  5 +++
 .../DafnyCore/Compilers/SinglePassCompiler.cs |  3 ++
 Source/DafnyCore/Feature.cs                   |  5 ++-
 Source/DafnyCore/Options/CommonOptionBag.cs   |  9 +++--
 Source/DafnyCore/Options/DafnyCommands.cs     |  3 +-
 .../DafnyCore/Plugins/IExecutableBackend.cs   |  3 ++
 Source/DafnyDriver/CompilerDriver.cs          | 15 ++++++++
 Source/DafnyRuntime/DafnyRuntime.cs           | 17 +++++++++
 10 files changed, 114 insertions(+), 8 deletions(-)

diff --git a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs
index fb15f0fbc33..7988d415f0b 100644
--- a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs
+++ b/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;
+    }
+  }
+}");
+    }
   }
 }
diff --git a/Source/DafnyCore/Compilers/CoverageInstrumenter.cs b/Source/DafnyCore/Compilers/CoverageInstrumenter.cs
index 0167bae5816..7caa8dae42d 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 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);
+    }
+  }
+  
 }
diff --git a/Source/DafnyCore/Compilers/ExecutableBackend.cs b/Source/DafnyCore/Compilers/ExecutableBackend.cs
index 7f2da678ec2..ce52879ccc2 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;
@@ -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) {
diff --git a/Source/DafnyCore/Compilers/SinglePassCompiler.cs b/Source/DafnyCore/Compilers/SinglePassCompiler.cs
index 6114aa8446e..c45459660b6 100644
--- a/Source/DafnyCore/Compilers/SinglePassCompiler.cs
+++ b/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);
+    }
   }
 }
diff --git a/Source/DafnyCore/Feature.cs b/Source/DafnyCore/Feature.cs
index 7130bc3dfe7..deae496f8c4 100644
--- a/Source/DafnyCore/Feature.cs
+++ b/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 {
diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
index 87962f5c921..a3d5161566e 100644
--- a/Source/DafnyCore/Options/CommonOptionBag.cs
+++ b/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
     );
   }
 
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 @@ 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[] {
diff --git a/Source/DafnyCore/Plugins/IExecutableBackend.cs b/Source/DafnyCore/Plugins/IExecutableBackend.cs
index e1ce320d2db..efd96c6bdfc 100644
--- a/Source/DafnyCore/Plugins/IExecutableBackend.cs
+++ b/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.
diff --git a/Source/DafnyDriver/CompilerDriver.cs b/Source/DafnyDriver/CompilerDriver.cs
index e636e5c54fc..61dfa7f7859 100644
--- a/Source/DafnyDriver/CompilerDriver.cs
+++ b/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) {
     }
   }
diff --git a/Source/DafnyRuntime/DafnyRuntime.cs b/Source/DafnyRuntime/DafnyRuntime.cs
index 557f781d1cb..06daa72c5b1 100755
--- a/Source/DafnyRuntime/DafnyRuntime.cs
+++ b/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;
+    }
+  }
 }

From 4bc558f219573ec970f56a79b765b8155c9bb7f0 Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Tue, 7 Nov 2023 16:31:51 -0800
Subject: [PATCH 02/15] =?UTF-8?q?Rename=20existing=20=E2=80=94coverage-rep?=
 =?UTF-8?q?ort=20to=20=E2=80=94verification-coverage-report?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Source/DafnyCore/Options/CommonOptionBag.cs | 4 ++--
 docs/DafnyRef/UserGuide.md                  | 4 ++--
 docs/dev/news/4625.feat                     | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
index a3d5161566e..3f23b1a1dc5 100644
--- a/Source/DafnyCore/Options/CommonOptionBag.cs
+++ b/Source/DafnyCore/Options/CommonOptionBag.cs
@@ -214,7 +214,7 @@ public enum GeneralTraitsOptions {
 May produce spurious warnings.") {
     IsHidden = true
   };
-  public static readonly Option<string> VerificationCoverageReport = new("--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"
   };
@@ -222,7 +222,7 @@ public enum GeneralTraitsOptions {
     "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",
+  public static readonly Option<string> ExecutionCoverageReport = new("--coverage-report",
     "Emit execution coverage report to a given directory.") {
     ArgumentHelpName = "directory"
   };
diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md
index c4a85cfcd98..6ca41f06b4e 100644
--- a/docs/DafnyRef/UserGuide.md
+++ b/docs/DafnyRef/UserGuide.md
@@ -1512,12 +1512,12 @@ included in the proof.
 These options can be specified in `dfyconfig.toml`, and this is typically the most convenient way to use them with the IDE.
 
 More detailed information is available using either the `--log-format
-text` or `--coverage-report` option to `dafny verify`. The former will
+text` or `--verification-coverage-report` option to `dafny verify`. The former will
 include a list of proof dependencies (including source location and
 description) alongside every assertion batch in the generated log
 whenever one of the two warning options above is also included. The
 latter will produce a highlighted HTML version of your source code, in
-the same format used by `dafny generate-tests --coverage-report`,
+the same format used by `dafny generate-tests --verification-coverage-report`,
 indicating which parts of the program were used, not used, or partly
 used in the verification of the entire program.
 
diff --git a/docs/dev/news/4625.feat b/docs/dev/news/4625.feat
index fc2354afce0..23ce498a469 100644
--- a/docs/dev/news/4625.feat
+++ b/docs/dev/news/4625.feat
@@ -1 +1 @@
-The new `--coverage-report` flag to `dafny verify` creates an HTML report highlighting which portions of the program were and were not necessary for verification. The format is the same as for `dafny generate-tests --coverage-report` and files from the two commands can be merged.
+The new `--verification-coverage-report` flag to `dafny verify` creates an HTML report highlighting which portions of the program were and were not necessary for verification. The format is the same as for `dafny generate-tests --coverage-report` and files from the two commands can be merged.

From b1254a48781a6ec7142182bd94d93518a5d6b0d8 Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Wed, 8 Nov 2023 12:10:00 -0800
Subject: [PATCH 03/15] Improve coverage report formatting, hook up to stdlibs,
 start to improve stdlib coverage

---
 .../Compilers/CSharp/Compiler-Csharp.cs       |  2 +-
 .../Compilers/CoverageInstrumenter.cs         | 13 +++++---
 .../CoverageReport/CoverageReport.cs          | 20 ++++++------
 Source/DafnyCore/Feature.cs                   |  2 +-
 Source/DafnyDriver/CompilerDriver.cs          |  2 +-
 Source/DafnyDriver/CoverageReporter.cs        | 31 +++++++++++--------
 Source/DafnyRuntime/DafnyRuntime.cs           |  2 +-
 Source/DafnyStandardLibraries/Makefile        |  2 +-
 .../examples/WrappersExamples.dfy             | 14 +++++++++
 9 files changed, 55 insertions(+), 33 deletions(-)

diff --git a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs
index 7988d415f0b..a39ac19314f 100644
--- a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs
+++ b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs
@@ -3442,7 +3442,7 @@ 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 {
diff --git a/Source/DafnyCore/Compilers/CoverageInstrumenter.cs b/Source/DafnyCore/Compilers/CoverageInstrumenter.cs
index 7caa8dae42d..b915e5158a2 100644
--- a/Source/DafnyCore/Compilers/CoverageInstrumenter.cs
+++ b/Source/DafnyCore/Compilers/CoverageInstrumenter.cs
@@ -12,7 +12,7 @@ public class CoverageInstrumenter {
 
   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)>();
     }
@@ -96,11 +96,14 @@ public class CoverageInstrumenter {
 
   public void PopulateCoverageReport(CoverageReport report) {
     var tallies = File.ReadLines(talliesFilePath).Select(int.Parse).ToArray();
-    foreach (var ((token, description), tally) in legend.Zip(tallies)) {
+    foreach (var ((token, _), 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);
+      // 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;
+      report.LabelCode(rangeToken, label);
     }
   }
-  
+
 }
diff --git a/Source/DafnyCore/CoverageReport/CoverageReport.cs b/Source/DafnyCore/CoverageReport/CoverageReport.cs
index 3593227fc5b..bccce063507 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<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>()) {
diff --git a/Source/DafnyCore/Feature.cs b/Source/DafnyCore/Feature.cs
index deae496f8c4..98e8ce5c683 100644
--- a/Source/DafnyCore/Feature.cs
+++ b/Source/DafnyCore/Feature.cs
@@ -185,7 +185,7 @@ public enum Feature {
 
   [FeatureDescription("All built-in types in runtime library", "#sec-compilation-built-ins")]
   BuiltinsInRuntime,
-  
+
   [FeatureDescription("Runtime coverage report", "#sec-compilation-built-ins")]
   RuntimeCoverageReport
 }
diff --git a/Source/DafnyDriver/CompilerDriver.cs b/Source/DafnyDriver/CompilerDriver.cs
index 61dfa7f7859..c63592c3534 100644
--- a/Source/DafnyDriver/CompilerDriver.cs
+++ b/Source/DafnyDriver/CompilerDriver.cs
@@ -564,7 +564,7 @@ private record TargetPaths(string Directory, string Filename) {
           if (compiledCorrectly) {
             var coverageReportDir = options.Get(CommonOptionBag.ExecutionCoverageReport);
             if (coverageReportDir != null) {
-              var coverage  = compiler.GetCoverageAfterRun();
+              var coverage = compiler.GetCoverageAfterRun();
               var coverageReport = new CoverageReport("Test Coverage", "Branches", "_tests_actual", dafnyProgram);
               coverage.PopulateCoverageReport(coverageReport);
               new CoverageReporter(options).SerializeCoverageReports(coverageReport, coverageReportDir);
diff --git a/Source/DafnyDriver/CoverageReporter.cs b/Source/DafnyDriver/CoverageReporter.cs
index dc170fc0d98..b2fee998554 100644
--- a/Source/DafnyDriver/CoverageReporter.cs
+++ b/Source/DafnyDriver/CoverageReporter.cs
@@ -160,26 +160,30 @@ public class CoverageReporter {
       sessionDirectory = Path.Combine(reportsDirectory, sessionName);
     }
     Directory.CreateDirectory(sessionDirectory);
-    HashSet<string> allFiles = new();
-    reports.ForEach(report => allFiles.UnionWith(report.AllFiles()));
-    if (allFiles.Count == 0) {
+    HashSet<Uri> allUris = new();
+    reports.ForEach(report => allUris.UnionWith(report.AllFiles()));
+    if (allUris.Count == 0) {
       reporter.Warning(MessageSource.Documentation, ErrorRegistry.NoneId, Token.NoToken,
         "No coverage data found in the reports.");
       return;
     }
     CopyStyleFiles(sessionDirectory);
+    // TODO: Handle arbitrary Uris better
+    var allFiles = allUris.Select(uri => uri.ToString());
     var prefixLength = new string(
       allFiles.First()[..allFiles.Min(s => Path.GetDirectoryName(s)?.Length ?? 0)]
         .TakeWhile((c, i) => allFiles.All(s => s[i] == c)).ToArray()).Length;
-    var sourceFileToCoverageReport = new Dictionary<string, string>();
-    foreach (var fileName in allFiles) {
+    var sourceFileToCoverageReport = new Dictionary<Uri, string>();
+    foreach (var uri in allUris) {
+      // TODO: Handle arbitrary Uris better
+      var fileName = uri.ToString();
       var directoryForFile = Path.Combine(sessionDirectory, Path.GetDirectoryName(fileName)?[prefixLength..].TrimStart('/') ?? "");
       var pathToRoot = Path.GetRelativePath(directoryForFile, sessionDirectory);
       Directory.CreateDirectory(directoryForFile);
       for (int i = 0; i < reports.Count; i++) {
         var linksToOtherReports = GetHtmlLinksToOtherReports(reports[i], Path.GetFileName(fileName), reports);
-        var reportForFile = HtmlReportForFile(reports[i], fileName, pathToRoot, linksToOtherReports);
-        sourceFileToCoverageReport[fileName] = Path.Combine(directoryForFile, Path.GetFileName(fileName));
+        var reportForFile = HtmlReportForFile(reports[i], uri, pathToRoot, linksToOtherReports);
+        sourceFileToCoverageReport[uri] = Path.Combine(directoryForFile, Path.GetFileName(fileName));
         File.WriteAllText(Path.Combine(directoryForFile, Path.GetFileName(fileName)) + $"{reports[i].UniqueSuffix}.html", reportForFile);
       }
     }
@@ -202,7 +206,7 @@ public class CoverageReporter {
   /// <summary>
   /// Creates an index file with program-wide statistics for a particular report
   /// </summary>
-  private void CreateIndexFile(CoverageReport report, Dictionary<string, string> sourceFileToCoverageReportFile, string baseDirectory, string linksToOtherReports) {
+  private void CreateIndexFile(CoverageReport report, Dictionary<Uri, string> sourceFileToCoverageReportFile, string baseDirectory, string linksToOtherReports) {
     var assembly = System.Reflection.Assembly.GetCallingAssembly();
     var templateStream = assembly.GetManifestResourceStream(CoverageReportIndexTemplatePath);
     if (templateStream is null) {
@@ -288,8 +292,9 @@ public class CoverageReporter {
     }
   }
 
-  private string HtmlReportForFile(CoverageReport report, string pathToSourceFile, string baseDirectory, string linksToOtherReports) {
-    var source = new StreamReader(pathToSourceFile).ReadToEnd();
+  private string HtmlReportForFile(CoverageReport report, Uri uri, string baseDirectory, string linksToOtherReports) {
+    var dafnyFile = new DafnyFile(options, uri);
+    var source = dafnyFile.GetContent().ReadToEnd();
     var lines = source.Split(new[] { Environment.NewLine }, StringSplitOptions.None);
     var characterLabels = new CoverageLabel[lines.Length][];
     for (int i = 0; i < lines.Length; i++) {
@@ -297,7 +302,7 @@ public class CoverageReporter {
       Array.Fill(characterLabels[i], CoverageLabel.None);
     }
     var labeledCodeBuilder = new StringBuilder(source.Length);
-    foreach (var span in report.CoverageSpansForFile(pathToSourceFile)) {
+    foreach (var span in report.CoverageSpansForFile(uri)) {
       var line = span.Span.StartToken.line - 1;
       var column = span.Span.StartToken.col - 1;
       while (true) {
@@ -345,8 +350,8 @@ public class CoverageReporter {
     templateText = PathToRootRegex.Replace(templateText, baseDirectory);
     templateText = LinksToOtherReportsRegex.Replace(templateText, linksToOtherReports);
     templateText = IndexLinkRegex.Replace(templateText, $"index{report.UniqueSuffix}.html");
-    templateText = FileNameRegex.Replace(templateText, $"{Path.GetFileName(pathToSourceFile)}, {report.Name}");
-    templateText = UriRegex.Replace(templateText, pathToSourceFile);
+    templateText = FileNameRegex.Replace(templateText, $"{uri.LocalPath}, {report.Name}");
+    templateText = UriRegex.Replace(templateText, uri.ToString());
     return LabeledCodeRegex.Replace(templateText, labeledCode);
   }
 
diff --git a/Source/DafnyRuntime/DafnyRuntime.cs b/Source/DafnyRuntime/DafnyRuntime.cs
index 06daa72c5b1..e20b9c69b26 100755
--- a/Source/DafnyRuntime/DafnyRuntime.cs
+++ b/Source/DafnyRuntime/DafnyRuntime.cs
@@ -1948,7 +1948,7 @@ public class HaltException : Exception {
     public HaltException(object message) : base(message.ToString()) {
     }
   }
-  
+
   public class CodeCoverage {
     static uint[] tallies;
     public static void Setup(int size) {
diff --git a/Source/DafnyStandardLibraries/Makefile b/Source/DafnyStandardLibraries/Makefile
index 6ff98d0d56b..44ef6df0162 100644
--- a/Source/DafnyStandardLibraries/Makefile
+++ b/Source/DafnyStandardLibraries/Makefile
@@ -23,7 +23,7 @@ update-binary: build-binary
 # with deeper coverage of module functionality.
 test:
 	$(DAFNY) build -t:lib examples/dfyconfig.toml --output:build/stdlibexamples.doo
-	$(DAFNY) test -t:cs build/stdlibexamples.doo examples/BoundedInts/NonDefault.cs --output:build/stdlibexamples
+	$(DAFNY) test -t:cs build/stdlibexamples.doo examples/BoundedInts/NonDefault.cs --output:build/stdlibexamples --coverage-report:build/testcoverage
 	$(DAFNY) test -t:java build/stdlibexamples.doo examples/BoundedInts/Externs/NonDefault.java --output:build/stdlibexamples
 	$(DAFNY) test -t:go build/stdlibexamples.doo examples/BoundedInts/NonDefault.go --output:build/stdlibexamples
 	$(DAFNY) test -t:py build/stdlibexamples.doo examples/BoundedInts/NonDefault.py --output:build/stdlibexamples
diff --git a/Source/DafnyStandardLibraries/examples/WrappersExamples.dfy b/Source/DafnyStandardLibraries/examples/WrappersExamples.dfy
index 9d9af1334a4..6587f2327fc 100644
--- a/Source/DafnyStandardLibraries/examples/WrappersExamples.dfy
+++ b/Source/DafnyStandardLibraries/examples/WrappersExamples.dfy
@@ -32,6 +32,20 @@ method {:test} TestMyMap() {
   expect greeting == "Hello\nDafny\n";
 }
 
+method {:test} TestGetGreetingSuccess() {
+  var m := new MyMap<string, string>();
+  m.Put("message", "Hello");
+  m.Put("name", "Dafny");
+  var greeting := GetGreeting(m);
+  expect greeting == Some("Hello Dafny");
+}
+
+method {:test} TestGetGreetingFailure() {
+  var m := new MyMap<string, string>();
+  var greeting := GetGreeting(m);
+  expect greeting == None;
+}
+
 method Greet(m: MyMap<string, string>) returns (greeting: string) {
   var o: Option<string> := m.Get("message");
   if o.Some? {

From fb55df8bca6220bbca0d3f2c74257e88955a9e58 Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Wed, 8 Nov 2023 13:09:05 -0800
Subject: [PATCH 04/15] Integration test mostly working

---
 .../LitTests/LitTest/comp/CoverageReport.dfy  |   9 +
 ...overageReport.dfy_tests_actual.html.expect | 228 ++++++++++++++++++
 .../LitTest/logger/CoverageReport.dfy         |   4 +-
 3 files changed, 239 insertions(+), 2 deletions(-)
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy_tests_actual.html.expect

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy
new file mode 100644
index 00000000000..b63bb066174
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy
@@ -0,0 +1,9 @@
+// Actual runtime test coverage
+// (See also logger/CoverageReport.dfy for verification coverage and expected coverage of generated tests)
+
+// RUN: rm -rf "%t"/execution_testing
+// RUN: %baredafny run %args -t:cs --no-timestamp-for-coverage-report --coverage-report "%t/execution_testing" %s
+// RUN: %sed 's/<h1 hidden.*//' "%t"/execution_testing/BranchCoverage.dfy_tests_actual.html > "%t"/coverage_tests_actual.html
+// RUN: %diff "%S/CoverageReport.dfy_tests_actual.html.expect" "%t/coverage_tests_actual.html"
+
+include "BranchCoverage.dfy"
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy_tests_actual.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy_tests_actual.html.expect
new file mode 100644
index 00000000000..3f4ef509947
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy_tests_actual.html.expect
@@ -0,0 +1,228 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html
+        xmlns="http://www.w3.org/1999/xhtml" lang="en">
+<head>
+    <meta http-equiv="Content-Type" content="text/html;charset=UTF-8"/>
+    <link rel="stylesheet" href="./.resources/coverage.css" type="text/css"/>
+    <title>/Users/salkeldr/Documents/GitHub/dafny/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/BranchCoverage.dfy, Test Coverage</title>
+</head>
+<body onload="window['PR_TAB_WIDTH']=4">
+<div class="menu" id="menu">
+    <a href="./index_tests_actual.html">Index</a>
+    
+</div>
+<h1>/Users/salkeldr/Documents/GitHub/dafny/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/BranchCoverage.dfy, Test Coverage</h1>
+
+<pre class="source lang-java linenums">
+<span class="na" id="1:1">// RUN: %dafny /useBaseNameForFileName /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:cs %S/BranchCoverage2.cs "%s" > "%t"
+// RUN: %dafny /useBaseNameForFileName /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:js %S/BranchCoverage3.js "%s" >> "%t"
+// RUN: %dafny /useBaseNameForFileName /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:go %S/BranchCoverage4.go "%s" >> "%t"
+// RUN: %dafny /useBaseNameForFileName /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:java %S/CodeCoverage.java "%s" >> "%t"
+// RUN: %dafny /useBaseNameForFileName /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:py %S/BranchCoverage.py "%s" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// The Main method is at the end of this file, because that makes it easier to maintain
+// this test file when adding more tests.
+
+// ---------- class constructor ----------
+    
+class MyClass {
+</span><span class="fc" id="14:1">  constructor () {  // 3 times
+</span><span class="na" id="15:1">  }
+}
+
+// ---------- routines that are never called ----------
+
+</span><span class="nc" id="20:1">method NeverCalled() {
+</span><span class="na" id="21:1">  // we get here 0 times
+}
+
+function FunctionNeverCalled(): int {
+  // we get here 0 times
+</span><span class="nc" id="26:1">  75
+</span><span class="na" id="27:1">}
+
+// ---------- if ----------
+
+</span><span class="fc" id="31:1">method M(x: int) returns (y: int) {
+</span><span class="na" id="32:1">  // we get here 3 times
+</span><span class="fc" id="33:1">  if x < 10 {
+</span><span class="na" id="34:1">    return x + 20;  // we get here 1 time
+</span><span class="nc" id="35:1">  } else if x < 20 {  // note: the location between th "else" and the "if" does not get recorded
+</span><span class="na" id="36:1">    return x + 20;  // we get here 0 times
+</span><span class="fc" id="37:1">  } else {
+</span><span class="na" id="38:1">    return 100;  // we get here 2 times
+  }
+}
+
+</span><span class="fc" id="42:1">method N(x: int) returns (y: int) {
+</span><span class="na" id="43:1">  // we get here 3 times
+  y := 100;
+</span><span class="fc" id="45:1">  if x < 10 {
+</span><span class="na" id="46:1">    return x + 20;  // we get here 1 time
+</span><span class="pc" id="47:1">  } else if x < 20 {  // note: the location between th "else" and the "if" does not get recorded
+</span><span class="na" id="48:1">    return x + 20;  // we get here 0 times
+  }  // we get to this implicit else 2 times
+}
+
+
+</span><span class="fc" id="53:1">method P(x: int) {
+</span><span class="na" id="54:1">  // we get here 1 time
+  var y := 100;
+</span><span class="pc" id="56:1">  if * {
+</span><span class="na" id="57:1">    // we get here 0 times, because the compiler picks the other branch, which is empty
+    y := y + 2;
+  }  // we get to the implicit else 1 time
+
+</span><span class="fc" id="61:1">  if * {
+</span><span class="na" id="62:1">    // we get here 1 time
+</span><span class="nc" id="63:1">  } else {
+</span><span class="na" id="64:1">    // we get here 0 times, because the compiler picks the other branch, which is empty
+    y := y + 2;
+  }
+
+  // the following if is all ghost, so there are no branch-coverage locations in it
+  if x < 2 {
+  } else if * {
+  }
+
+</span><span class="nc" id="73:1">  if x < 2 {
+</span><span class="na" id="74:1">    // get here 0 times
+</span><span class="pc" id="75:1">  } else if * {
+</span><span class="na" id="76:1">    // we get here 0 times
+    y := y + 1;
+  }  // implicit else: 1 time
+}
+
+// ---------- if case ----------
+
+</span><span class="fc" id="83:1">method Q(x: int) returns (y: int) {
+</span><span class="na" id="84:1">  // we get here 3 times
+
+  // the following statement is all ghost, so there are no coverage locations in it
+  if {
+    case x < 100 =>
+    case x < 1000 =>
+      assert x < 1_000_000;
+    case 50 <= x =>
+  }
+
+  if
+</span><span class="fc" id="95:1">  case x < 100 =>
+</span><span class="na" id="96:1">    // we get here 1 time
+</span><span class="fc" id="97:1">  case x < 1000 =>
+</span><span class="na" id="98:1">    // we get here 1 time, since the compiler lays down the cases in order
+    return 8;
+</span><span class="fc" id="100:1">  case 50 <= x =>
+</span><span class="na" id="101:1">    // we get here 1 time
+}
+
+// ---------- while ----------
+
+</span><span class="fc" id="106:1">method R(x: int) returns (y: int) {
+</span><span class="na" id="107:1">  // we get here 1 time
+  var i: nat := 0;
+</span><span class="fc" id="109:1">  while i < x {
+</span><span class="na" id="110:1">    // we get here 111 times
+    i := i + 1;
+  }
+
+</span><span class="nc" id="114:1">  while * {
+</span><span class="na" id="115:1">    // we get here 0 times
+    break;
+  }
+
+  while
+    decreases i
+  {
+</span><span class="fc" id="122:1">    case i % 2 == 0 =>
+</span><span class="na" id="123:1">      // we get here 56 times
+</span><span class="fc" id="124:1">      if i == 0 {
+</span><span class="na" id="125:1">        // we get here 1 time
+        break;
+      }  // implicit else: 55 times
+      i := i - 1;
+</span><span class="fc" id="129:1">    case i % 4 == 1 =>
+</span><span class="na" id="130:1">      // we get here 28 times
+      i := i - 1;
+</span><span class="fc" id="132:1">    case 0 < i =>
+</span><span class="na" id="133:1">      // we get here 28 times
+      i := i - 1;
+  }
+
+  return 40;
+}
+
+// ---------- top-level if-then-else ----------
+
+function Fib(n: nat): nat {
+  // we get here 465 times
+</span><span class="fc" id="144:1">  if n < 2 then  // then: 233 times
+    n
+</span><span class="na" id="146:1">  else if false then  // then: 0 times (else-if is omitted)
+</span><span class="pc" id="147:1">    8
+</span><span class="na" id="148:1">  else  // else: 232 times
+    Fib(n - 2) + Fib(n - 1)
+}
+
+// ---------- top-level match expression, match statement, and tail recursion ----------
+
+function {:tailrecursion} Factorial(n: nat): nat {
+  // 11 times
+</span><span class="fc" id="156:1">  match n
+  case 0 => 1  // 1 time
+</span><span class="na" id="158:1">  case _ => n * Factorial(n - 1)  // 10 times
+}
+
+method {:tailrecursion} ComputeFactorial(n: nat, acc: nat) returns (f: nat)
+  ensures f == Factorial(n) * acc
+</span><span class="fc" id="163:1">{
+</span><span class="na" id="164:1">  // 11 times
+  match n
+</span><span class="fc" id="166:1">  case 0 =>  // 1 time
+</span><span class="na" id="167:1">    return acc;
+</span><span class="fc" id="168:1">  case _ =>  // 10 times
+</span><span class="na" id="169:1">    f := ComputeFactorial(n - 1, acc * n);
+}
+
+// ---------- Main ----------
+
+</span><span class="fc" id="174:1">method Main() {
+</span><span class="na" id="175:1">  // we get here 1 time
+
+  var mc := new MyClass();
+  mc := new MyClass();
+  mc := new MyClass();
+
+  var y := M(5);
+  y := M(y);
+  y := M(y);
+
+  y := N(5);
+  y := N(y);
+  y := N(y);
+
+  P(5);
+
+  y := Q(50);
+  y := Q(101);
+  y := Q(1010);
+
+  y := R(111);
+
+  y := Fib(12);
+
+  y := Factorial(10);
+  y := ComputeFactorial(10, 1);
+}
+
+</span></pre>
+<div class="footer">
+    <span class="right">
+        Created with 
+        <a href="https://github.com/dafny-lang/dafny">Dafny</a>
+    </span>
+</div>
+</body>
+</html>
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/CoverageReport.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/CoverageReport.dfy
index dc530f4421e..eb76fc3925d 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/CoverageReport.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/CoverageReport.dfy
@@ -1,10 +1,10 @@
 // NONUNIFORM: Not a compiler test
 // Verification coverage:
 // RUN: rm -rf "%t"/coverage_verification
-// RUN: %baredafny verify --use-basename-for-filename --show-snippets false --verify-included-files --no-timestamp-for-coverage-report --coverage-report "%t/coverage_verification" %s
+// RUN: %baredafny verify --use-basename-for-filename --show-snippets false --verify-included-files --no-timestamp-for-coverage-report --verification-coverage-report "%t/coverage_verification" %s
 // RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_verification/ProofDependencyLogging.dfy_verification.html > "%t"/coverage_verification_actual.html
 // RUN: %diff "%S/ProofDependencyLogging.dfy_verification.html.expect" "%t/coverage_verification_actual.html"
-// Test coverage:
+// Expected test coverage:
 // RUN: rm -rf "%t"/coverage_testing
 // RUN: %baredafny generate-tests Block --no-timestamp-for-coverage-report --coverage-report "%t/coverage_testing" %s
 // RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_testing/ProofDependencyLogging.dfy_tests_expected.html > "%t"/coverage_testing_actual.html

From 99ff54b7ab4d6cefcc207a277b5f95105a92ea66 Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Wed, 8 Nov 2023 13:48:06 -0800
Subject: [PATCH 05/15] Fix regression in report naming

---
 Source/DafnyDriver/CoverageReporter.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Source/DafnyDriver/CoverageReporter.cs b/Source/DafnyDriver/CoverageReporter.cs
index b2fee998554..7cfe2157862 100644
--- a/Source/DafnyDriver/CoverageReporter.cs
+++ b/Source/DafnyDriver/CoverageReporter.cs
@@ -350,7 +350,7 @@ public class CoverageReporter {
     templateText = PathToRootRegex.Replace(templateText, baseDirectory);
     templateText = LinksToOtherReportsRegex.Replace(templateText, linksToOtherReports);
     templateText = IndexLinkRegex.Replace(templateText, $"index{report.UniqueSuffix}.html");
-    templateText = FileNameRegex.Replace(templateText, $"{uri.LocalPath}, {report.Name}");
+    templateText = FileNameRegex.Replace(templateText, $"{Path.GetFileName(uri.LocalPath)}, {report.Name}");
     templateText = UriRegex.Replace(templateText, uri.ToString());
     return LabeledCodeRegex.Replace(templateText, labeledCode);
   }

From b1f5da6bc0c84b0ea0966d0c41acbef58da78f8a Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Wed, 8 Nov 2023 13:53:15 -0800
Subject: [PATCH 06/15] Revert runtime change

---
 Source/DafnyRuntime/DafnyRuntime.cs | 17 -----------------
 1 file changed, 17 deletions(-)

diff --git a/Source/DafnyRuntime/DafnyRuntime.cs b/Source/DafnyRuntime/DafnyRuntime.cs
index e20b9c69b26..557f781d1cb 100755
--- a/Source/DafnyRuntime/DafnyRuntime.cs
+++ b/Source/DafnyRuntime/DafnyRuntime.cs
@@ -1948,21 +1948,4 @@ 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;
-    }
-  }
 }

From 084f92816793924d565a31a6ec6d48b49f26ee53 Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Wed, 8 Nov 2023 14:44:45 -0800
Subject: [PATCH 07/15] Nonuniform test

---
 .../TestFiles/LitTests/LitTest/comp/CoverageReport.dfy          | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy
index b63bb066174..c72374295a3 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy
@@ -1,3 +1,5 @@
+// NONUNIFORM: Out-of-band output (coverage reports) not easily testable via %testDafnyForEachCompiler
+
 // Actual runtime test coverage
 // (See also logger/CoverageReport.dfy for verification coverage and expected coverage of generated tests)
 

From ed93db2d4bf8c377cf311eedb56a160837a8abb1 Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Wed, 8 Nov 2023 14:45:28 -0800
Subject: [PATCH 08/15] Fix paths in expect file

---
 .../LitTest/comp/CoverageReport.dfy_tests_actual.html.expect  | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy_tests_actual.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy_tests_actual.html.expect
index 3f4ef509947..70ea2d7d1df 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy_tests_actual.html.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy_tests_actual.html.expect
@@ -5,14 +5,14 @@
 <head>
     <meta http-equiv="Content-Type" content="text/html;charset=UTF-8"/>
     <link rel="stylesheet" href="./.resources/coverage.css" type="text/css"/>
-    <title>/Users/salkeldr/Documents/GitHub/dafny/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/BranchCoverage.dfy, Test Coverage</title>
+    <title>BranchCoverage.dfy, Test Coverage</title>
 </head>
 <body onload="window['PR_TAB_WIDTH']=4">
 <div class="menu" id="menu">
     <a href="./index_tests_actual.html">Index</a>
     
 </div>
-<h1>/Users/salkeldr/Documents/GitHub/dafny/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/BranchCoverage.dfy, Test Coverage</h1>
+<h1>BranchCoverage.dfy, Test Coverage</h1>
 
 <pre class="source lang-java linenums">
 <span class="na" id="1:1">// RUN: %dafny /useBaseNameForFileName /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:cs %S/BranchCoverage2.cs "%s" > "%t"

From 46d7331297cd65886c7bcade87cae7a72ba76061 Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Wed, 8 Nov 2023 15:29:24 -0800
Subject: [PATCH 09/15] Test for unsupported feature too

---
 .../Compilers/CSharp/Compiler-Csharp.cs        |  2 +-
 .../Compilers/Cplusplus/Compiler-cpp.cs        |  3 ++-
 .../Compilers/Dafny/Compiler-dafny.cs          |  3 ++-
 .../DafnyCore/Compilers/GoLang/Compiler-go.cs  |  3 ++-
 .../DafnyCore/Compilers/Java/Compiler-java.cs  |  4 +++-
 .../Compilers/JavaScript/Compiler-js.cs        |  3 ++-
 .../Compilers/Python/Compiler-python.cs        |  3 ++-
 .../DafnyCore/Compilers/SinglePassCompiler.cs  |  4 ----
 Source/DafnyCore/Feature.cs                    |  2 +-
 Source/DafnyDriver/CompilerDriver.cs           |  7 ++++++-
 .../LitTests/LitTest/comp/CoverageReport.dfy   | 15 ++++++++++++---
 .../LitTest/comp/CoverageReport.dfy.expect     | 18 ++++++++++++++++++
 ...CoverageReport.dfy_tests_actual.html.expect |  4 ++--
 13 files changed, 53 insertions(+), 18 deletions(-)
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy.expect

diff --git a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs
index a39ac19314f..c0dcd391747 100644
--- a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs
+++ b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs
@@ -3443,7 +3443,7 @@ protected class ClassWriter : IClassWriter {
       TrStmt(recoveryBody, catchBlock);
     }
 
-    protected override void EmitCoverageReportInstrumentation(Program program, ConcreteSyntaxTree wr) {
+    protected void EmitCoverageReportInstrumentation(Program program, ConcreteSyntaxTree wr) {
       wr.WriteLine(@"
 namespace DafnyProfiling {
   public class CodeCoverage {
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 @@ class CppCompiler : SinglePassCompiler {
       Feature.MethodSynthesis,
       Feature.UnicodeChars,
       Feature.ConvertingValuesToStrings,
-      Feature.BuiltinsInRuntime
+      Feature.BuiltinsInRuntime,
+      Feature.RuntimeCoverageReport
     };
 
     private List<DatatypeDecl> 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 @@ class DafnyCompiler : SinglePassCompiler {
       Feature.SubtypeConstraintsInQuantifiers,
       Feature.TuplesWiderThan20,
       Feature.ForLoops,
-      Feature.Traits
+      Feature.Traits,
+      Feature.RuntimeCoverageReport
     };
 
     private readonly List<string> Imports = new() { DafnyDefaultModule };
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 @@ class GoCompiler : SinglePassCompiler {
       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..2b1a39558ac 100644
--- a/Source/DafnyCore/Compilers/Java/Compiler-java.cs
+++ b/Source/DafnyCore/Compilers/Java/Compiler-java.cs
@@ -29,7 +29,9 @@ public class JavaCompiler : SinglePassCompiler {
       Feature.MethodSynthesis,
       Feature.TuplesWiderThan20,
       Feature.ArraysWithMoreThan16Dims,
-      Feature.ArrowsWithMoreThan16Arguments
+      Feature.ArrowsWithMoreThan16Arguments,
+      Feature.RuntimeCoverageReport,
+      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 @@ class JavaScriptCompiler : SinglePassCompiler {
       Feature.MethodSynthesis,
       Feature.ExternalConstructors,
       Feature.SubsetTypeTests,
-      Feature.SeparateCompilation
+      Feature.SeparateCompilation,
+      Feature.RuntimeCoverageReport
     };
 
     public override string ModuleSeparator => "_";
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 @@ class PythonCompiler : SinglePassCompiler {
 
     public override IReadOnlySet<Feature> UnsupportedFeatures => new HashSet<Feature> {
       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 c45459660b6..1ddf0facbb3 100644
--- a/Source/DafnyCore/Compilers/SinglePassCompiler.cs
+++ b/Source/DafnyCore/Compilers/SinglePassCompiler.cs
@@ -6061,9 +6061,5 @@ 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);
-    }
   }
 }
diff --git a/Source/DafnyCore/Feature.cs b/Source/DafnyCore/Feature.cs
index 98e8ce5c683..33b45e180fb 100644
--- a/Source/DafnyCore/Feature.cs
+++ b/Source/DafnyCore/Feature.cs
@@ -186,7 +186,7 @@ public enum Feature {
   [FeatureDescription("All built-in types in runtime library", "#sec-compilation-built-ins")]
   BuiltinsInRuntime,
 
-  [FeatureDescription("Runtime coverage report", "#sec-compilation-built-ins")]
+  [FeatureDescription("Execution coverage report", "#sec-compilation-built-ins")]
   RuntimeCoverageReport
 }
 
diff --git a/Source/DafnyDriver/CompilerDriver.cs b/Source/DafnyDriver/CompilerDriver.cs
index c63592c3534..d4b7e7ba2d5 100644
--- a/Source/DafnyDriver/CompilerDriver.cs
+++ b/Source/DafnyDriver/CompilerDriver.cs
@@ -492,6 +492,11 @@ private record TargetPaths(string Directory, string Filename) {
       foreach (var compilerInstrumenter in options.Plugins.SelectMany(p => p.GetCompilerInstrumenters(dafnyProgram.Reporter))) {
         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;
 
@@ -565,7 +570,7 @@ private record TargetPaths(string Directory, string Filename) {
             var coverageReportDir = options.Get(CommonOptionBag.ExecutionCoverageReport);
             if (coverageReportDir != null) {
               var coverage = compiler.GetCoverageAfterRun();
-              var coverageReport = new CoverageReport("Test Coverage", "Branches", "_tests_actual", dafnyProgram);
+              var coverageReport = new CoverageReport("Execution Coverage", "Branches", "_tests_actual", dafnyProgram);
               coverage.PopulateCoverageReport(coverageReport);
               new CoverageReporter(options).SerializeCoverageReports(coverageReport, coverageReportDir);
             }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy
index c72374295a3..c8f941667b3 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy
@@ -4,8 +4,17 @@
 // (See also logger/CoverageReport.dfy for verification coverage and expected coverage of generated tests)
 
 // RUN: rm -rf "%t"/execution_testing
-// RUN: %baredafny run %args -t:cs --no-timestamp-for-coverage-report --coverage-report "%t/execution_testing" %s
-// RUN: %sed 's/<h1 hidden.*//' "%t"/execution_testing/BranchCoverage.dfy_tests_actual.html > "%t"/coverage_tests_actual.html
-// RUN: %diff "%S/CoverageReport.dfy_tests_actual.html.expect" "%t/coverage_tests_actual.html"
+// RUN: %baredafny run %args -t:cs --no-timestamp-for-coverage-report --coverage-report "%t_coverage_reports/execution_testing" %s
+// RUN: %sed 's/<h1 hidden.*//' "%t_coverage_reports"/execution_testing/BranchCoverage.dfy_tests_actual.html > "%t_coverage_reports"/coverage_tests_actual.html
+// RUN: %diff "%S/CoverageReport.dfy_tests_actual.html.expect" "%t_coverage_reports/coverage_tests_actual.html"
+
+// Manually assert the other backends cleanly report they don't support this feature yet
+// RUN: %exits-with 3 %baredafny run %args -t:java --no-timestamp-for-coverage-report --coverage-report "%t_coverage_reports/execution_testing" %s > "%t"
+// RUN: %exits-with 3 %baredafny run %args -t:js --no-timestamp-for-coverage-report --coverage-report "%t_coverage_reports/execution_testing" %s >> "%t"
+// RUN: %exits-with 3 %baredafny run %args -t:go --no-timestamp-for-coverage-report --coverage-report "%t_coverage_reports/execution_testing" %s >> "%t"
+// RUN: %exits-with 3 %baredafny run %args -t:py --no-timestamp-for-coverage-report --coverage-report "%t_coverage_reports/execution_testing" %s >> "%t"
+// RUN: %exits-with 3 %baredafny run %args -t:cpp --no-timestamp-for-coverage-report --coverage-report "%t_coverage_reports/execution_testing" %s >> "%t"
+// RUN: %exits-with 3 %baredafny run %args -t:rs --no-timestamp-for-coverage-report --coverage-report "%t_coverage_reports/execution_testing" %s >> "%t"
+// RUN: %diff "%s.expect" "%t"
 
 include "BranchCoverage.dfy"
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy.expect
new file mode 100644
index 00000000000..050212ee153
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy.expect
@@ -0,0 +1,18 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
+CoverageReport.dfy(20,0): Error: Feature not supported for this compilation target: Execution coverage report
+
+Dafny program verifier finished with 0 verified, 0 errors
+CoverageReport.dfy(20,0): Error: Feature not supported for this compilation target: Execution coverage report
+
+Dafny program verifier finished with 0 verified, 0 errors
+CoverageReport.dfy(20,0): Error: Feature not supported for this compilation target: Execution coverage report
+
+Dafny program verifier finished with 0 verified, 0 errors
+CoverageReport.dfy(20,0): Error: Feature not supported for this compilation target: Execution coverage report
+
+Dafny program verifier finished with 0 verified, 0 errors
+CoverageReport.dfy(20,0): Error: Feature not supported for this compilation target: Execution coverage report
+
+Dafny program verifier finished with 0 verified, 0 errors
+CoverageReport.dfy(20,0): Error: Feature not supported for this compilation target: Execution coverage report
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy_tests_actual.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy_tests_actual.html.expect
index 70ea2d7d1df..50b452d2ad2 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy_tests_actual.html.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy_tests_actual.html.expect
@@ -5,14 +5,14 @@
 <head>
     <meta http-equiv="Content-Type" content="text/html;charset=UTF-8"/>
     <link rel="stylesheet" href="./.resources/coverage.css" type="text/css"/>
-    <title>BranchCoverage.dfy, Test Coverage</title>
+    <title>BranchCoverage.dfy, Execution Coverage</title>
 </head>
 <body onload="window['PR_TAB_WIDTH']=4">
 <div class="menu" id="menu">
     <a href="./index_tests_actual.html">Index</a>
     
 </div>
-<h1>BranchCoverage.dfy, Test Coverage</h1>
+<h1>BranchCoverage.dfy, Execution Coverage</h1>
 
 <pre class="source lang-java linenums">
 <span class="na" id="1:1">// RUN: %dafny /useBaseNameForFileName /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:cs %S/BranchCoverage2.cs "%s" > "%t"

From 6f2a5d400ebe73254623250cc270dbaa340941de Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Wed, 8 Nov 2023 15:37:08 -0800
Subject: [PATCH 10/15] =?UTF-8?q?Mention=20=E2=80=94coverage-report=20for?=
 =?UTF-8?q?=20dafny=20test?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Source/DafnyCore/Feature.cs | 2 +-
 docs/DafnyRef/UserGuide.md  | 5 ++++-
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/Source/DafnyCore/Feature.cs b/Source/DafnyCore/Feature.cs
index 33b45e180fb..5d8ad4a0a99 100644
--- a/Source/DafnyCore/Feature.cs
+++ b/Source/DafnyCore/Feature.cs
@@ -186,7 +186,7 @@ public enum Feature {
   [FeatureDescription("All built-in types in runtime library", "#sec-compilation-built-ins")]
   BuiltinsInRuntime,
 
-  [FeatureDescription("Execution coverage report", "#sec-compilation-built-ins")]
+  [FeatureDescription("Execution coverage report", "#sec-dafny-test")]
   RuntimeCoverageReport
 }
 
diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md
index 6ca41f06b4e..5b4d20ad5ed 100644
--- a/docs/DafnyRef/UserGuide.md
+++ b/docs/DafnyRef/UserGuide.md
@@ -479,6 +479,8 @@ In particular, it accepts the `--target` option that specifies the programming l
 - `--output` - gives the folder and filename root for compilation artifacts
 - `--methods-to-test` - the value is a (.NET) regular expression that is matched against the fully
   qualified name of the method; only those methods that match are tested
+- `--coverage-report` - the value is a directory in which Dafny will save an html coverage report highlighting parts of
+  the program that execution of the tests covered.
 
 The order in which the tests are run is not specified.
 
@@ -1517,7 +1519,8 @@ include a list of proof dependencies (including source location and
 description) alongside every assertion batch in the generated log
 whenever one of the two warning options above is also included. The
 latter will produce a highlighted HTML version of your source code, in
-the same format used by `dafny generate-tests --verification-coverage-report`,
+the same format used by `dafny test --coverage-report`
+and `dafny generate-tests --verification-coverage-report`,
 indicating which parts of the program were used, not used, or partly
 used in the verification of the entire program.
 

From b0b7fc5f1fb83146504b90ec8d6bea73269689ad Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Wed, 8 Nov 2023 15:38:39 -0800
Subject: [PATCH 11/15] Update features table

---
 docs/DafnyRef/Features.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/docs/DafnyRef/Features.md b/docs/DafnyRef/Features.md
index f0b5c1a51ee..f4679ac7cbb 100644
--- a/docs/DafnyRef/Features.md
+++ b/docs/DafnyRef/Features.md
@@ -45,6 +45,7 @@
 | [Legacy CLI without commands](#sec-dafny-commands) |  X  |  X  |  X  |  X  |  X  |  X  |  |
 | [Separate compilation](#sec-compilation) |  X  |  |  X  |  X  |  X  |  X  |  X  |
 | [All built-in types in runtime library](##sec-compilation-built-ins) |  X  |  X  |  X  |  X  |  X  |  |  X  |
+| [Runtime coverage report](##sec-compilation-built-ins) |  X  |  |  |  |  |  |  |
 
 [^compiler-feature-forall-note]: 'Sequentializing' a `forall` statement refers to compiling it directly to a series of nested loops
     with the statement's body directly inside. The alternative, default compilation strategy

From e40be50f48843706f65290ec00c2d4b2245abf6d Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Wed, 8 Nov 2023 15:50:12 -0800
Subject: [PATCH 12/15] Improve encapsulation

---
 .../Compilers/CSharp/CsharpBackend.cs         |  4 ++++
 .../Compilers/CoverageInstrumenter.cs         | 21 +++++++++++--------
 .../DafnyCore/Compilers/ExecutableBackend.cs  |  4 ----
 .../DafnyCore/Plugins/IExecutableBackend.cs   |  6 ++++--
 Source/DafnyDriver/CompilerDriver.cs          |  7 +------
 5 files changed, 21 insertions(+), 21 deletions(-)

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 @@ 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) {
   }
 }
diff --git a/Source/DafnyCore/Compilers/CoverageInstrumenter.cs b/Source/DafnyCore/Compilers/CoverageInstrumenter.cs
index b915e5158a2..dc02c7786f1 100644
--- a/Source/DafnyCore/Compilers/CoverageInstrumenter.cs
+++ b/Source/DafnyCore/Compilers/CoverageInstrumenter.cs
@@ -94,15 +94,18 @@ public class CoverageInstrumenter {
     }
   }
 
-  public void PopulateCoverageReport(CoverageReport report) {
-    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;
-      report.LabelCode(rangeToken, label);
+  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/ExecutableBackend.cs b/Source/DafnyCore/Compilers/ExecutableBackend.cs
index ce52879ccc2..322c0fc6ebf 100644
--- a/Source/DafnyCore/Compilers/ExecutableBackend.cs
+++ b/Source/DafnyCore/Compilers/ExecutableBackend.cs
@@ -70,10 +70,6 @@ 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) {
diff --git a/Source/DafnyCore/Plugins/IExecutableBackend.cs b/Source/DafnyCore/Plugins/IExecutableBackend.cs
index efd96c6bdfc..13f42750e96 100644
--- a/Source/DafnyCore/Plugins/IExecutableBackend.cs
+++ b/Source/DafnyCore/Plugins/IExecutableBackend.cs
@@ -132,8 +132,6 @@ 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.
@@ -200,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();
+  }
 }
diff --git a/Source/DafnyDriver/CompilerDriver.cs b/Source/DafnyDriver/CompilerDriver.cs
index d4b7e7ba2d5..ffbaa794888 100644
--- a/Source/DafnyDriver/CompilerDriver.cs
+++ b/Source/DafnyDriver/CompilerDriver.cs
@@ -569,9 +569,8 @@ private record TargetPaths(string Directory, string Filename) {
           if (compiledCorrectly) {
             var coverageReportDir = options.Get(CommonOptionBag.ExecutionCoverageReport);
             if (coverageReportDir != null) {
-              var coverage = compiler.GetCoverageAfterRun();
               var coverageReport = new CoverageReport("Execution Coverage", "Branches", "_tests_actual", dafnyProgram);
-              coverage.PopulateCoverageReport(coverageReport);
+              compiler.PopulateCoverageReport(coverageReport);
               new CoverageReporter(options).SerializeCoverageReports(coverageReport, coverageReportDir);
             }
           }
@@ -630,10 +629,6 @@ class NoExecutableBackend : IExecutableBackend {
       throw new NotSupportedException();
     }
 
-    public override CoverageInstrumenter GetCoverageAfterRun() {
-      throw new NotImplementedException();
-    }
-
     public NoExecutableBackend([NotNull] DafnyOptions options) : base(options) {
     }
   }

From 06a90688986d7b7f66a898d19147c0d81297ac45 Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Wed, 8 Nov 2023 16:03:42 -0800
Subject: [PATCH 13/15] Release note, typo, whitespace

---
 Source/DafnyCore/Compilers/Java/Compiler-java.cs | 1 -
 Source/DafnyDriver/CompilerDriver.cs             | 4 ++--
 docs/dev/news/4755.feat                          | 1 +
 3 files changed, 3 insertions(+), 3 deletions(-)
 create mode 100644 docs/dev/news/4755.feat

diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs
index 2b1a39558ac..f41a92e9196 100644
--- a/Source/DafnyCore/Compilers/Java/Compiler-java.cs
+++ b/Source/DafnyCore/Compilers/Java/Compiler-java.cs
@@ -31,7 +31,6 @@ public class JavaCompiler : SinglePassCompiler {
       Feature.ArraysWithMoreThan16Dims,
       Feature.ArrowsWithMoreThan16Arguments,
       Feature.RuntimeCoverageReport,
-      Feature.RuntimeCoverageReport
     };
 
     const string DafnySetClass = "dafny.DafnySet";
diff --git a/Source/DafnyDriver/CompilerDriver.cs b/Source/DafnyDriver/CompilerDriver.cs
index ffbaa794888..ac06e8fea31 100644
--- a/Source/DafnyDriver/CompilerDriver.cs
+++ b/Source/DafnyDriver/CompilerDriver.cs
@@ -492,8 +492,8 @@ private record TargetPaths(string Directory, string Filename) {
       foreach (var compilerInstrumenter in options.Plugins.SelectMany(p => p.GetCompilerInstrumenters(dafnyProgram.Reporter))) {
         options.Backend.InstrumentCompiler(compilerInstrumenter, dafnyProgram);
       }
-      
-      if (options.Get(CommonOptionBag.ExecutionCoverageReport) != null 
+
+      if (options.Get(CommonOptionBag.ExecutionCoverageReport) != null
           && options.Backend.UnsupportedFeatures.Contains(Feature.RuntimeCoverageReport)) {
         throw new UnsupportedFeatureException(dafnyProgram.GetStartOfFirstFileToken(), Feature.RuntimeCoverageReport);
       }
diff --git a/docs/dev/news/4755.feat b/docs/dev/news/4755.feat
new file mode 100644
index 00000000000..5e5021687d5
--- /dev/null
+++ b/docs/dev/news/4755.feat
@@ -0,0 +1 @@
+The new `--coverage-report` flag to `dafny run` and `dafny test` creates an HTML report highlighting which portions of the program were executed at runtime.

From 87aa06899bfd0853a8fbb247e6da3713e8b96e2f Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Wed, 8 Nov 2023 16:07:46 -0800
Subject: [PATCH 14/15] Typo and library backend

---
 Source/DafnyCore/Compilers/Library/LibraryBackend.cs | 3 ++-
 docs/DafnyRef/Features.md                            | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/Source/DafnyCore/Compilers/Library/LibraryBackend.cs b/Source/DafnyCore/Compilers/Library/LibraryBackend.cs
index 0874a382949..9bcbbf9f865 100644
--- a/Source/DafnyCore/Compilers/Library/LibraryBackend.cs
+++ b/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
diff --git a/docs/DafnyRef/Features.md b/docs/DafnyRef/Features.md
index f4679ac7cbb..148a967fa80 100644
--- a/docs/DafnyRef/Features.md
+++ b/docs/DafnyRef/Features.md
@@ -45,7 +45,7 @@
 | [Legacy CLI without commands](#sec-dafny-commands) |  X  |  X  |  X  |  X  |  X  |  X  |  |
 | [Separate compilation](#sec-compilation) |  X  |  |  X  |  X  |  X  |  X  |  X  |
 | [All built-in types in runtime library](##sec-compilation-built-ins) |  X  |  X  |  X  |  X  |  X  |  |  X  |
-| [Runtime coverage report](##sec-compilation-built-ins) |  X  |  |  |  |  |  |  |
+| [Execution coverage report](##sec-compilation-built-ins) |  X  |  |  |  |  |  |  |
 
 [^compiler-feature-forall-note]: 'Sequentializing' a `forall` statement refers to compiling it directly to a series of nested loops
     with the statement's body directly inside. The alternative, default compilation strategy

From 9262299ba6846f5b34073d6318334e4c27cca0f5 Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Thu, 9 Nov 2023 08:28:02 -0800
Subject: [PATCH 15/15] Fix feature support table

---
 Source/DafnyCore/Feature.cs | 4 ++--
 docs/DafnyRef/Features.md   | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Source/DafnyCore/Feature.cs b/Source/DafnyCore/Feature.cs
index 5d8ad4a0a99..82958d87c81 100644
--- a/Source/DafnyCore/Feature.cs
+++ b/Source/DafnyCore/Feature.cs
@@ -183,10 +183,10 @@ public enum Feature {
   [FeatureDescription("Separate compilation", "sec-compilation")]
   SeparateCompilation,
 
-  [FeatureDescription("All built-in types in runtime library", "#sec-compilation-built-ins")]
+  [FeatureDescription("All built-in types in runtime library", "sec-compilation-built-ins")]
   BuiltinsInRuntime,
 
-  [FeatureDescription("Execution coverage report", "#sec-dafny-test")]
+  [FeatureDescription("Execution coverage report", "sec-dafny-test")]
   RuntimeCoverageReport
 }
 
diff --git a/docs/DafnyRef/Features.md b/docs/DafnyRef/Features.md
index 148a967fa80..c09e18d0d67 100644
--- a/docs/DafnyRef/Features.md
+++ b/docs/DafnyRef/Features.md
@@ -44,8 +44,8 @@
 | [Converting values to strings](#sec-print-statement) |  X  |  X  |  X  |  X  |  X  |  |  X  |
 | [Legacy CLI without commands](#sec-dafny-commands) |  X  |  X  |  X  |  X  |  X  |  X  |  |
 | [Separate compilation](#sec-compilation) |  X  |  |  X  |  X  |  X  |  X  |  X  |
-| [All built-in types in runtime library](##sec-compilation-built-ins) |  X  |  X  |  X  |  X  |  X  |  |  X  |
-| [Execution coverage report](##sec-compilation-built-ins) |  X  |  |  |  |  |  |  |
+| [All built-in types in runtime library](#sec-compilation-built-ins) |  X  |  X  |  X  |  X  |  X  |  |  X  |
+| [Execution coverage report](#sec-dafny-test) |  X  |  |  |  |  |  |  |
 
 [^compiler-feature-forall-note]: 'Sequentializing' a `forall` statement refers to compiling it directly to a series of nested loops
     with the statement's body directly inside. The alternative, default compilation strategy