Allow filtering of combined coverage reports (dafny-lang#4673)

Add a new `--only-label` option to `merge-coverage-reports` to include
only one category of highlighting in the output. For example, merging
coverage reports from test generation and verification using the option
`--only-label NotCovered` will highlight only the regions not covered by
either testing or verification.

By submitting this pull request, I confirm that my contribution
is made under the terms of the MIT license.

Source/DafnyDriver/Commands/CoverageReportCommand.cs

@@ -7,20 +7,26 @@
 using System.IO;
 using System.Linq;
 using System.Threading.Tasks;
+using DafnyCore;
 
 namespace Microsoft.Dafny; 
 
 static class CoverageReportCommand {
 
+  public static readonly Option<CoverageLabel?> OnlyLabelOption = new("--only-label",
+    "Skip coverage labels other than the given one, after merging labels from the input reports.");
+
   public static IEnumerable<Option> Options =>
     new Option[] {
       CommonOptionBag.NoTimeStampForCoverageReport,
+      OnlyLabelOption
     };
 
   static CoverageReportCommand() {
     ReportsArgument = new("reports", r => {
       return r.Tokens.Where(t => !string.IsNullOrEmpty(t.Value)).Select(t => new FileInfo(t.Value)).ToList();
     }, true, "directories with coverage reports to be merged");
+    DooFile.RegisterNoChecksNeeded(OnlyLabelOption);
   }
 
   // FilesArgument is intended for Dafny files, so CoverageReportCommand adds its own argument instead

Source/DafnyDriver/CoverageReporter.cs

@@ -85,11 +85,15 @@ public void Merge(List<string> coverageReportsToMerge, string coverageReportOutD
         reports.Add(ParseCoverageReport(reportDir, $"{name} ({Path.GetFileName(reportDir)})", units, suffix));
       }
     }
+
+    var onlyLabel = options.Get(CoverageReportCommand.OnlyLabelOption);
     foreach (var report in reports) {
       foreach (var fileName in report.AllFiles()) {
         foreach (var span in report.CoverageSpansForFile(fileName)) {
           mergedReport.RegisterFile(span.Span.Uri);
-          mergedReport.LabelCode(span.Span, span.Label);
+          if ((onlyLabel ?? span.Label) == span.Label) {
+            mergedReport.LabelCode(span.Span, span.Label);
+          }
         }
       }
     }

Test/logger/CoverageReport.dfy

@@ -14,6 +14,11 @@
 // RUN: %baredafny merge-coverage-reports --no-timestamp-for-coverage-report "%t"/coverage_combined "%t"/coverage_testing "%t"/coverage_verification
 // RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_combined/ProofDependencyLogging.dfy_combined.html > "%t"/coverage_combined.html
 // RUN: %diff "%S/ProofDependencyLogging.dfy_combined.html.expect" "%t/coverage_combined.html"
+// Combined, limited coverage:
+// RUN: rm -rf "%t"/coverage_combined
+// RUN: %baredafny merge-coverage-reports --only-label NotCovered --no-timestamp-for-coverage-report "%t"/coverage_combined_limited "%t"/coverage_testing "%t"/coverage_verification
+// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_combined_limited/ProofDependencyLogging.dfy_combined.html > "%t"/coverage_combined_limited.html
+// RUN: %diff "%S/ProofDependencyLogging.dfy_combined_limited.html.expect" "%t/coverage_combined_limited.html"
 
 
 include "ProofDependencyLogging.dfy"