Verification coverage report (dafny-lang#4625)

# Description

Adds support for producing reports describing verification coverage in
the same format used for the expected test coverage reports that can be
produced from `dafny generate-tests`. Verification and test coverage
reports can be merged using `dafny merge-coverage-reports`.

# How has this been tested?

Includes a test of expected output in
`Test/logger/ProofDependencyLogging.dfy_verification.html.expect`.

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

---------

Co-authored-by: Aleksandr Fedchin <[email protected]>

Source/DafnyTestGeneration/CoverageReport/CoverageLabel.cs → Source/DafnyCore/CoverageReport/CoverageLabel.cs

@@ -3,9 +3,10 @@
 namespace Microsoft.Dafny;
 
 public enum CoverageLabel {
+  None,
   FullyCovered,
   NotCovered,
-  PartiallyCovered
+  PartiallyCovered,
 }
 
 public static class CoverageLabelExtension {
@@ -14,6 +15,12 @@ public static class CoverageLabelExtension {
   /// Combine coverage labels. E.g. FullyCovered + NotCovered = PartiallyCovered
   /// </summary>
   public static CoverageLabel Combine(CoverageLabel one, CoverageLabel two) {
+    if (one == CoverageLabel.None) {
+      return two;
+    }
+    if (two == CoverageLabel.None) {
+      return one;
+    }
     if (one == CoverageLabel.PartiallyCovered || two == CoverageLabel.PartiallyCovered || one != two) {
       return CoverageLabel.PartiallyCovered;
     }

Source/DafnyTestGeneration/CoverageReport/CoverageReport.cs → Source/DafnyCore/CoverageReport/CoverageReport.cs

@@ -11,7 +11,6 @@ public class CoverageReport {
 
   private static int nextUniqueId = 0;
 
-  // INVARIANT: CoverageSpans are sorted within each list by the position of the StartToken
   private readonly Dictionary<string, 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.
@@ -39,37 +38,12 @@ public CoverageReport(string name, string units, string suffix, Program program)
 
   /// <summary>
   /// Assign a coverage label to the code indicated by the <param name="span"></param> range token.
-  /// If the span intersects with existing coverage information, it will be merged according to
-  /// CoverageLabelExtension.Combine. 
   /// </summary>
   public void LabelCode(RangeToken span, CoverageLabel label) {
     Contract.Assert(labelsByFile.ContainsKey(span.ActualFilename));
-    if (span.StartToken.CompareTo(span.EndToken) == 0) {
-      return;
-    }
     var labeledFile = labelsByFile[span.ActualFilename];
     var coverageSpan = new CoverageSpan(span, label);
-    int index = labeledFile.BinarySearch(0, labeledFile.Count, coverageSpan, null);
-    if (index < 0) {
-      labeledFile.Insert(~index, coverageSpan);
-      return;
-    }
-    var overlappingSpan = labeledFile[index];
-    labeledFile.RemoveAt(index);
-    var combinedLabel = CoverageLabelExtension.Combine(label, overlappingSpan.Label);
-    switch (overlappingSpan.Span.EndToken.CompareTo(span.EndToken)) {
-      case 0:
-        labeledFile.Insert(index, new CoverageSpan(span, combinedLabel));
-        break;
-      case > 0:
-        labeledFile.Insert(index, new CoverageSpan(span, combinedLabel));
-        labeledFile.Insert(index + 1, new CoverageSpan(new RangeToken(span.EndToken, overlappingSpan.Span.EndToken), overlappingSpan.Label));
-        break;
-      default:
-        labeledFile.Insert(index, new CoverageSpan(overlappingSpan.Span, combinedLabel));
-        LabelCode(new RangeToken(overlappingSpan.Span.EndToken, span.EndToken), label);
-        break;
-    }
+    labeledFile.Add(coverageSpan);
   }
 
   public IEnumerable<CoverageSpan> CoverageSpansForFile(string fileName) {
@@ -92,8 +66,12 @@ private void RegisterFiles(Node astNode) {
     if (astNode.StartToken.ActualFilename != null) {
       labelsByFile[astNode.StartToken.ActualFilename] = new();
     }
+
     foreach (var declaration in astNode.Children.OfType<LiteralModuleDecl>()) {
       RegisterFiles(declaration);
     }
+    foreach (var declaration in astNode.Children.OfType<Declaration>()) {
+      RegisterFiles(declaration);
+    }
   }
 }

Source/DafnyTestGeneration/CoverageReport/CoverageSpan.cs → Source/DafnyCore/CoverageReport/CoverageSpan.cs

@@ -13,7 +13,6 @@ public CoverageSpan(RangeToken span, CoverageLabel label) {
     Contract.Assert(span.Uri != null);
     Contract.Assert(span.StartToken != null);
     Contract.Assert(span.EndToken != null);
-    Contract.Assert(span.StartToken.CompareTo(span.EndToken) != 0);
     Span = span;
     Label = label;
   }

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -209,6 +209,10 @@ May slow down verification slightly.
 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.") {
+    ArgumentHelpName = "directory"
+  };
 
   public static readonly Option<bool> IncludeRuntimeOption = new("--include-runtime",
     "Include the Dafny runtime as source in the target language.");
@@ -470,6 +474,7 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
       IncludeRuntimeOption,
       WarnContradictoryAssumptions,
       WarnRedundantAssumptions,
+      VerificationCoverageReport,
       DefaultFunctionOpacity
     );
   }

Source/DafnyCore/Options/DafnyCommands.cs

@@ -41,7 +41,8 @@ static DafnyCommands() {
     BoogieOptionBag.VerificationErrorLimit,
     CommonOptionBag.DefaultFunctionOpacity,
     CommonOptionBag.WarnContradictoryAssumptions,
-    CommonOptionBag.WarnRedundantAssumptions
+    CommonOptionBag.WarnRedundantAssumptions,
+    CommonOptionBag.VerificationCoverageReport
   }.ToList();
 
   public static IReadOnlyList<Option> TranslationOptions = new Option[] {

Source/DafnyCore/Verifier/ProofDependencyManager.cs

@@ -7,6 +7,7 @@
 //-----------------------------------------------------------------------------
 using System;
 using System.Collections.Generic;
+using System.Linq;
 using Dafny;
 using Bpl = Microsoft.Boogie;
 using BplParser = Microsoft.Boogie.Parser;
@@ -42,6 +43,10 @@ public IEnumerable<ProofDependency> GetPotentialDependenciesForDefinition(string
       return idsByMemberName[defName];
     }
 
+    public IEnumerable<ProofDependency> GetAllPotentialDependencies() {
+      return idsByMemberName.Values.SelectMany(deps => deps);
+    }
+
     // The "id" attribute on a Boogie AST node is used by Boogie to label
     // that AST node in the SMT-Lib formula when constructing a verification
     // condition.

Source/DafnyDriver/Commands/VerifyCommand.cs

@@ -15,6 +15,9 @@ public static Command Create() {
       result.AddOption(option);
     }
     DafnyCli.SetHandlerUsingDafnyOptionsContinuation(result, (options, _) => {
+      if (options.Get(CommonOptionBag.VerificationCoverageReport) != null) {
+        options.TrackVerificationCoverage = true;
+      }
       options.Compile = false;
       return CompilerDriver.RunCompiler(options);
     });

Source/DafnyDriver/CompilerDriver.cs

@@ -155,6 +155,13 @@ private async Task<ExitValue> ProcessFilesAsync(IReadOnlyList<DafnyFile/*!*/>/*!
 
         if (options.TrackVerificationCoverage) {
           ProofDependencyWarnings.WarnAboutSuspiciousDependencies(options, dafnyProgram.Reporter, depManager);
+          var coverageReportDir = options.Get(CommonOptionBag.VerificationCoverageReport);
+          if (coverageReportDir != null) {
+            new CoverageReporter(options).SerializeVerificationCoverageReport(
+              depManager, dafnyProgram,
+              boogiePrograms.SelectMany(tp => tp.Item2.AllCoveredElements),
+              coverageReportDir);
+          }
         }
 
         bool compiled;

Source/DafnyDriver/CoverageReporter.cs

@@ -4,6 +4,9 @@
 using System.Linq;
 using System.Text;
 using System.Text.RegularExpressions;
+using DafnyCore.Verifier;
+using Microsoft.Boogie;
+using Microsoft.Extensions.Primitives;
 
 namespace Microsoft.Dafny; 
 
@@ -22,7 +25,7 @@ public class CoverageReporter {
   private static readonly Regex TableFooterRegex = new(@"\{\{TABLE_FOOTER\}\}");
   private static readonly Regex TableBodyRegex = new(@"\{\{TABLE_BODY\}\}");
   private static readonly Regex IndexFileNameRegex = new(@"index(.*)\.html");
-  private static readonly Regex SpanRegexInverse = new("class=\"([a-z]+)\" id=\"line([0-9]+)col([0-9]+)-line([0-9]+)col([0-9]+)\"");
+  private static readonly Regex PosRegexInverse = new("class=\"([a-z]+)\" id=\"pos([0-9]+)\">");
   private const string CoverageReportTemplatePath = "coverage_report_template.html";
   private const string CoverageReportIndexTemplatePath = "coverage_report_index_template.html";
   private const string CoverageReportSupportingFilesPath = ".resources";
@@ -39,6 +42,28 @@ public CoverageReporter(DafnyOptions options) {
     this.options = options;
   }
 
+
+  public void SerializeVerificationCoverageReport(ProofDependencyManager depManager, Program dafnyProgram, IEnumerable<TrackedNodeComponent> usedComponents, string coverageReportDir) {
+    var usedDependencies =
+      usedComponents.Select(depManager.GetFullIdDependency).ToHashSet();
+    var allDependencies =
+      depManager
+        .GetAllPotentialDependencies()
+        .OrderBy(dep => dep.Range.StartToken);
+    var coverageReport = new CoverageReport("Verification coverage", "Lines", "_verification", dafnyProgram);
+    foreach (var dep in allDependencies) {
+      if (dep is FunctionDefinitionDependency) {
+        continue;
+      }
+      coverageReport.LabelCode(dep.Range,
+        usedDependencies.Contains(dep)
+          ? CoverageLabel.FullyCovered
+          : CoverageLabel.NotCovered);
+    }
+
+    SerializeCoverageReports(coverageReport, coverageReportDir);
+  }
+
   public void Merge(List<string> coverageReportsToMerge, string coverageReportOutDir) {
     // assume only one report in directory for now
     List<CoverageReport> reports = new();
@@ -80,16 +105,17 @@ private static CoverageReport ParseCoverageReport(string reportDir, string name,
         continue;
       }
       var uri = new Uri(uriMatch.Groups[1].Value);
+      var lastEndToken = new Token(1, 1);
       report.RegisterFile(uri);
-      foreach (var span in SpanRegexInverse.Matches(source).Where(match => match.Success)) {
-        if (int.TryParse(span.Groups[2].Value, out var startLine) &&
-            int.TryParse(span.Groups[3].Value, out var startCol) &&
-            int.TryParse(span.Groups[4].Value, out var endLine) &&
-            int.TryParse(span.Groups[5].Value, out var endCol)) {
-          var startToken = new Token(startLine, startCol);
-          startToken.Uri = uri;
-          var endToken = new Token(endLine, endCol);
+      foreach (var span in PosRegexInverse.Matches(source).Where(match => match.Success)) {
+        if (int.TryParse(span.Groups[2].Value, out var pos)) {
+          var startToken = new Token(1, 1);
           startToken.Uri = uri;
+          startToken.pos = pos;
+          lastEndToken.pos = pos;
+          var endToken = new Token(1, 1);
+          endToken.Uri = uri;
+          lastEndToken = endToken;
           var rangeToken = new RangeToken(startToken, endToken);
           rangeToken.Uri = uri;
           report.LabelCode(rangeToken, FromHtmlClass(span.Groups[1].Value));
@@ -125,7 +151,7 @@ private void SerializeCoverageReports(List<CoverageReport> reports, string repor
         .TakeWhile((c, i) => allFiles.All(s => s[i] == c)).ToArray()).Length;
     Dictionary<string, string> sourceFileToCoverageReport = new Dictionary<string, string>();
     foreach (var fileName in allFiles) {
-      var directoryForFile = Path.Combine(sessionDirectory, Path.GetDirectoryName(fileName)?[prefixLength..] ?? "");
+      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++) {
@@ -239,16 +265,31 @@ private void CopyStyleFiles(string baseDirectory) {
   private string HtmlReportForFile(CoverageReport report, string pathToSourceFile, string baseDirectory, string linksToOtherReports) {
     var source = new StreamReader(pathToSourceFile).ReadToEnd();
     var lines = source.Split("\n");
-    IToken lastToken = new Token(0, 0);
+    var characterLabels = new CoverageLabel[source.Length];
+    Array.Fill(characterLabels, CoverageLabel.None);
+    IToken lastToken = new Token(1, 1);
     var labeledCodeBuilder = new StringBuilder(source.Length);
     foreach (var span in report.CoverageSpansForFile(pathToSourceFile)) {
-      AppendCodeBetweenTokens(labeledCodeBuilder, lines, lastToken, span.Span.StartToken);
-      labeledCodeBuilder.Append(OpenHtmlTag(span));
-      AppendCodeBetweenTokens(labeledCodeBuilder, lines, span.Span.StartToken, span.Span.EndToken);
-      labeledCodeBuilder.Append(CloseHtmlTag(span));
-      lastToken = span.Span.EndToken;
+      for (var pos = span.Span.StartToken.pos; pos <= span.Span.EndToken.pos; pos++) {
+        characterLabels[pos] = CoverageLabelExtension.Combine(characterLabels[pos], span.Label);
+      }
     }
-    AppendCodeBetweenTokens(labeledCodeBuilder, lines, lastToken, null);
+
+    CoverageLabel lastLabel = CoverageLabel.None;
+    labeledCodeBuilder.Append(OpenHtmlTag(0, CoverageLabel.None));
+    for (var pos = 0; pos < source.Length; pos++) {
+      var thisLabel = characterLabels[pos];
+      if (thisLabel != lastLabel) {
+        labeledCodeBuilder.Append(CloseHtmlTag());
+        labeledCodeBuilder.Append(OpenHtmlTag(pos, thisLabel));
+      }
+
+      labeledCodeBuilder.Append(source[pos]);
+
+      lastLabel = thisLabel;
+    }
+    labeledCodeBuilder.Append(CloseHtmlTag());
+
     var assembly = System.Reflection.Assembly.GetCallingAssembly();
     var templateStream = assembly.GetManifestResourceStream(CoverageReportTemplatePath);
     var labeledCode = labeledCodeBuilder.ToString();
@@ -266,21 +307,6 @@ private string HtmlReportForFile(CoverageReport report, string pathToSourceFile,
     return LabeledCodeRegex.Replace(templateText, labeledCode);
   }
 
-  /// <summary>
-  /// Append code from <param name="lines"></param> that lies between <param name="start"></param> and
-  /// <param name="end"></param> tokens to the <param name="stringBuilder"></param>
-  /// </summary>
-  private static void AppendCodeBetweenTokens(StringBuilder stringBuilder, string[] lines, IToken start, IToken end) {
-    var currToken = new Token(start.line, start.col);
-    while (currToken.line < lines.Length && (end == null || currToken.line < end.line)) {
-      stringBuilder.Append(lines[currToken.line][currToken.col..] + "\n");
-      currToken.line += 1;
-    }
-    if (end != null && currToken.line < lines.Length) {
-      stringBuilder.Append(lines[currToken.line][currToken.col..end.col]);
-    }
-  }
-
   /// <summary>
   /// Return HTML class used to highlight lines in different colors depending on the coverage.
   /// Look at assets/.resources/coverage.css for the styles corresponding to these classes
@@ -290,6 +316,7 @@ private static string ToHtmlClass(CoverageLabel label) {
       CoverageLabel.FullyCovered => "fc",
       CoverageLabel.NotCovered => "nc",
       CoverageLabel.PartiallyCovered => "pc",
+      CoverageLabel.None => "none",
       _ => ""
     };
   }
@@ -304,13 +331,13 @@ private static CoverageLabel FromHtmlClass(string htmlClass) {
     return CoverageLabel.NotCovered; // this is a fallback in case the HTML has invalid classes
   }
 
-  private string OpenHtmlTag(CoverageSpan span) {
-    var id = $"id=\"line{span.Span.StartToken.line}col{span.Span.StartToken.col}-line{span.Span.EndToken.line}col{span.Span.EndToken.col}\"";
-    var classLabel = ToHtmlClass(span.Label);
+  private string OpenHtmlTag(int pos, CoverageLabel label) {
+    var id = $"id=\"pos{pos}\"";
+    var classLabel = ToHtmlClass(label);
     return $"<span class=\"{classLabel}\" {id}>";
   }
 
-  private string CloseHtmlTag(CoverageSpan span) {
+  private string CloseHtmlTag() {
     return "</span>";
   }
 }

Source/DafnyTestGeneration/Main.cs

@@ -115,6 +115,8 @@ private static void PopulateCoverageReport(CoverageReport coverageReport, Progra
       if (coverageReport == null) {
         return;
       }
+
+      var lineNumToPosCache = new Dictionary<Uri, int[]>();
       var lineRegex = new Regex("^(.*)\\(([0-9]+),[0-9]+\\)");
       HashSet<string> coveredStates = new(); // set of program states that are expected to be covered by tests
       foreach (var modification in cache.Values) {
@@ -133,7 +135,6 @@ private static void PopulateCoverageReport(CoverageReport coverageReport, Progra
           if (!int.TryParse(match.Groups[2].Value, out var lineNumber) || lineNumber == 0) {
             continue;
           }
-          lineNumber -= 1; // to zero-based
           Uri uri;
           try {
             uri = new Uri(
@@ -143,8 +144,12 @@ private static void PopulateCoverageReport(CoverageReport coverageReport, Progra
           } catch (ArgumentException) {
             continue;
           }
-          var rangeToken = new RangeToken(new Token(lineNumber, 0), new Token(lineNumber + 1, 0));
+          var linePos = Utils.GetPosFromLine(uri, lineNumber, lineNumToPosCache);
+          var lineLength = Utils.GetPosFromLine(uri, lineNumber + 1, lineNumToPosCache) - linePos - 1;
+          var rangeToken = new RangeToken(new Token(lineNumber, 1), new Token(lineNumber, lineLength));
           rangeToken.Uri = uri;
+          rangeToken.StartToken.pos = linePos;
+          rangeToken.EndToken.pos = linePos + lineLength;
           coverageReport.LabelCode(rangeToken,
             coveredStates.Contains(state)
               ? CoverageLabel.FullyCovered

Source/DafnyTestGeneration/Utils.cs

@@ -140,6 +140,28 @@ public static string GetBlockId(Block block, DafnyOptions options) {
       return state == null ? null : Regex.Replace(state, @"\s+", "") + uniqueId;
     }
 
+    /// <summary>
+    /// Given a file URI and a one-based line number, return the position of the character at the start of the line.
+    /// Use a cache to prevent reading the same file twice.
+    /// </summary>
+    public static int GetPosFromLine(Uri fileUri, int lineNum, Dictionary<Uri, int[]> cache) {
+      if (!cache.ContainsKey(fileUri)) {
+        var source = new StreamReader(fileUri.LocalPath).ReadToEnd();
+        var lines = source.Split("\n");
+        var pos = 0;
+        var line = 0;
+        var linePositions = new int[lines.Length + 1];
+        while (pos < source.Length) {
+          linePositions[line] = pos;
+          pos += lines[line].Length + 1;
+          line++;
+        }
+        linePositions[^1] = pos;
+        cache[fileUri] = linePositions;
+      }
+      return cache[fileUri][lineNum - 1]; // subtract one because lineNum is one-based
+    }
+
     public static IList<object> GetAttributeValue(Implementation implementation, string attribute) {
       var attributes = implementation.Attributes;
       while (attributes != null) {