Parity for Test Coverage and Proof Dependency Coverage Reports (dafny…

…-lang#4670)

# Description

This PR makes changes to how coverage reports produced using test
generation and proof dependency analysis can be merged together. In
particular:

- Calling `dafny merge-coverage-reports` now produces a 'combined
coverage' file that only labels code that is also labeled in all
original coverage reports. So, for example, code labeled in red would
have to not be covered both by the proof dependency analysis and by
tests.
- Code is now labeled using line and column numbers. This should lead to
identical outputs on Windows vs Unix.
- Test coverage reports now highlight more lines as opposed to only
labeling the last line associated with a given basic block in Boogie.
This is achieved by adding more `:captureState` assumptions in the
translator (only in translation passes that happen as part of test
generation)
- There is now a hidden `--no-timestamp-for-coverage-report` option
which disables the creation of a new timestamped directory for each
coverage report -- this allows testing of combined coverage reports

# How has this been tested?
I have run test generation on a file previously used to test proof
dependency reporting and added a test that checks the resulting test
coverage and combined coverage reports.

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]>
Co-authored-by: Aaron Tomb <[email protected]>

Source/DafnyCore/CoverageReport/CoverageLabel.cs

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

Source/DafnyCore/CoverageReport/CoverageReport.cs

@@ -59,11 +59,13 @@ public void RegisterFiles(Program program) {
   }
 
   public void RegisterFile(Uri uri) {
-    labelsByFile[uri.LocalPath] = new List<CoverageSpan>();
+    if (!labelsByFile.ContainsKey(uri.LocalPath)) {
+      labelsByFile[uri.LocalPath] = new List<CoverageSpan>();
+    }
   }
 
   private void RegisterFiles(Node astNode) {
-    if (astNode.StartToken.ActualFilename != null) {
+    if (astNode.StartToken.ActualFilename != null && !labelsByFile.ContainsKey(astNode.StartToken.ActualFilename)) {
       labelsByFile[astNode.StartToken.ActualFilename] = new();
     }
 

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -213,6 +213,10 @@ May slow down verification slightly.
     "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<bool> IncludeRuntimeOption = new("--include-runtime",
     "Include the Dafny runtime as source in the target language.");
@@ -475,6 +479,7 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
       WarnContradictoryAssumptions,
       WarnRedundantAssumptions,
       VerificationCoverageReport,
+      NoTimeStampForCoverageReport,
       DefaultFunctionOpacity
     );
   }

Source/DafnyCore/Options/DafnyCommands.cs

@@ -42,6 +42,7 @@ static DafnyCommands() {
     CommonOptionBag.DefaultFunctionOpacity,
     CommonOptionBag.WarnContradictoryAssumptions,
     CommonOptionBag.WarnRedundantAssumptions,
+    CommonOptionBag.NoTimeStampForCoverageReport,
     CommonOptionBag.VerificationCoverageReport
   }.ToList();
 

Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs

@@ -612,6 +612,9 @@ private void TrPredicateStmt(PredicateStmt stmt, BoogieStmtListBuilder builder,
           builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Expr, "assume statement", true));
           stmtContext = StmtType.NONE;
         }
+        if (options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) {
+          builder.AddCaptureState(stmt);
+        }
       } else if (stmt is ExpectStmt) {
         AddComment(builder, stmt, "expect statement");
         var s = (ExpectStmt)stmt;
@@ -639,6 +642,9 @@ private void TrPredicateStmt(PredicateStmt stmt, BoogieStmtListBuilder builder,
         TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);
         builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, s.Expr, "assume statement", true, etran.TrAttributes(stmt.Attributes, null)));
         stmtContext = StmtType.NONE; // done with translating assume stmt.
+        if (options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) {
+          builder.AddCaptureState(s);
+        }
       }
       this.fuelContext = FuelSetting.PopFuelContext();
     }

Source/DafnyDriver/Commands/CoverageReportCommand.cs

@@ -4,7 +4,6 @@
 #nullable disable
 using System.Collections.Generic;
 using System.CommandLine;
-using System.CommandLine.Invocation;
 using System.IO;
 using System.Linq;
 using System.Threading.Tasks;
@@ -13,6 +12,11 @@ namespace Microsoft.Dafny;
 
 static class CoverageReportCommand {
 
+  public static IEnumerable<Option> Options =>
+    new Option[] {
+      CommonOptionBag.NoTimeStampForCoverageReport,
+    };
+
   static CoverageReportCommand() {
     ReportsArgument = new("reports", r => {
       return r.Tokens.Where(t => !string.IsNullOrEmpty(t.Value)).Select(t => new FileInfo(t.Value)).ToList();
@@ -29,6 +33,9 @@ public static Command Create() {
       "Merge several previously generated coverage reports together.");
     result.AddArgument(OutDirArgument);
     result.AddArgument(ReportsArgument);
+    foreach (var option in Options) {
+      result.AddOption(option);
+    }
 
     DafnyCli.SetHandlerUsingDafnyOptionsContinuation(result, (options, _) => {
       var coverageReporter = new CoverageReporter(options);

Source/DafnyDriver/Commands/GenerateTestsCommand.cs

@@ -26,6 +26,7 @@ static class GenerateTestsCommand {
       BoogieOptionBag.VerificationTimeLimit,
       PrintBpl,
       CoverageReport,
+      CommonOptionBag.NoTimeStampForCoverageReport,
       ForcePrune
     }.Concat(DafnyCommands.ConsoleOutputOptions).
       Concat(DafnyCommands.ResolverOptions);

Source/DafnyDriver/CoverageReporter.cs

@@ -6,7 +6,6 @@
 using System.Text.RegularExpressions;
 using DafnyCore.Verifier;
 using Microsoft.Boogie;
-using Microsoft.Extensions.Primitives;
 
 namespace Microsoft.Dafny; 
 
@@ -25,7 +24,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 PosRegexInverse = new("class=\"([a-z]+)\" id=\"pos([0-9]+)\">");
+  private static readonly Regex PosRegexInverse = new("class=\"([a-z]+)\" id=\"([0-9]+):([0-9]+)\"");
   private const string CoverageReportTemplatePath = "coverage_report_template.html";
   private const string CoverageReportIndexTemplatePath = "coverage_report_index_template.html";
   private const string CoverageReportSupportingFilesPath = ".resources";
@@ -50,7 +49,7 @@ public void SerializeVerificationCoverageReport(ProofDependencyManager depManage
       depManager
         .GetAllPotentialDependencies()
         .OrderBy(dep => dep.Range.StartToken);
-    var coverageReport = new CoverageReport("Verification coverage", "Lines", "_verification", dafnyProgram);
+    var coverageReport = new CoverageReport("Verification coverage", "Proof Dependencies", "_verification", dafnyProgram);
     foreach (var dep in allDependencies) {
       if (dep is FunctionDefinitionDependency) {
         continue;
@@ -65,8 +64,8 @@ public void SerializeVerificationCoverageReport(ProofDependencyManager depManage
   }
 
   public void Merge(List<string> coverageReportsToMerge, string coverageReportOutDir) {
-    // assume only one report in directory for now
     List<CoverageReport> reports = new();
+    var mergedReport = new CoverageReport("Combined Coverage Report", "Locations", "_combined", null);
     foreach (var reportDir in coverageReportsToMerge) {
       if (!Directory.Exists(reportDir)) {
         reporter.Warning(MessageSource.Documentation, ErrorRegistry.NoneId, Token.NoToken,
@@ -77,8 +76,7 @@ public void Merge(List<string> coverageReportsToMerge, string coverageReportOutD
         var indexFileName = Path.GetFileName(pathToIndexFile);
         var indexFileMatch = IndexFileNameRegex.Match(indexFileName);
         if (!indexFileMatch.Success) {
-          reporter.Warning(MessageSource.Documentation, ErrorRegistry.NoneId, Token.NoToken,
-            $"Directory {reportDir} contains file {indexFileName} which is not part of a coverage report");
+          continue;
         }
         var suffix = indexFileMatch.Groups[1].Value;
         var index = new StreamReader(pathToIndexFile).ReadToEnd();
@@ -87,6 +85,15 @@ public void Merge(List<string> coverageReportsToMerge, string coverageReportOutD
         reports.Add(ParseCoverageReport(reportDir, $"{name} ({Path.GetFileName(reportDir)})", units, suffix));
       }
     }
+    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);
+        }
+      }
+    }
+    reports.Add(mergedReport);
     SerializeCoverageReports(reports, coverageReportOutDir);
   }
 
@@ -104,23 +111,31 @@ private static CoverageReport ParseCoverageReport(string reportDir, string name,
       if (!uriMatch.Success) {
         continue;
       }
+
       var uri = new Uri(uriMatch.Groups[1].Value);
       var lastEndToken = new Token(1, 1);
+      lastEndToken.Uri = uri;
+      var lastLabel = CoverageLabel.NotApplicable;
       report.RegisterFile(uri);
       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);
+        if (int.TryParse(span.Groups[2].Value, out var line) &&
+            int.TryParse(span.Groups[3].Value, out var col)) {
+          var nextToken = new Token(line, col);
+          nextToken.Uri = uri;
+          var precedingToken = new Token(line, col - 1);
+          precedingToken.Uri = uri;
+          var rangeToken = new RangeToken(lastEndToken, precedingToken);
           rangeToken.Uri = uri;
-          report.LabelCode(rangeToken, FromHtmlClass(span.Groups[1].Value));
+          report.LabelCode(rangeToken, lastLabel);
+          lastLabel = FromHtmlClass(span.Groups[1].Value);
+          lastEndToken = nextToken;
         }
       }
+
+      var lastToken = new Token(source.Count(c => c == '\n') + 2, 0);
+      lastToken.Uri = uri;
+      var lastRangeToken = new RangeToken(lastEndToken, lastToken);
+      report.LabelCode(lastRangeToken, lastLabel);
     }
     return report;
   }
@@ -135,8 +150,11 @@ public void SerializeCoverageReports(CoverageReport report, string directory) {
   /// will have links to each other to make comparison easier
   /// </summary>
   private void SerializeCoverageReports(List<CoverageReport> reports, string reportsDirectory) {
-    var sessionName = DateTime.Now.ToString("yyyy-dd-M--HH-mm-ss");
-    var sessionDirectory = Path.Combine(reportsDirectory, sessionName);
+    var sessionDirectory = reportsDirectory;
+    if (!options.Get(CommonOptionBag.NoTimeStampForCoverageReport)) {
+      var sessionName = DateTime.Now.ToString("yyyy-dd-M--HH-mm-ss");
+      sessionDirectory = Path.Combine(reportsDirectory, sessionName);
+    }
     Directory.CreateDirectory(sessionDirectory);
     HashSet<string> allFiles = new();
     reports.ForEach(report => allFiles.UnionWith(report.AllFiles()));
@@ -149,7 +167,7 @@ private void SerializeCoverageReports(List<CoverageReport> reports, string repor
     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;
-    Dictionary<string, string> sourceFileToCoverageReport = new Dictionary<string, string>();
+    var sourceFileToCoverageReport = new Dictionary<string, string>();
     foreach (var fileName in allFiles) {
       var directoryForFile = Path.Combine(sessionDirectory, Path.GetDirectoryName(fileName)?[prefixLength..].TrimStart('/') ?? "");
       var pathToRoot = Path.GetRelativePath(directoryForFile, sessionDirectory);
@@ -190,7 +208,9 @@ private void CreateIndexFile(CoverageReport report, Dictionary<string, string> s
     }
     var coverageLabels = Enum.GetValues(typeof(CoverageLabel)).Cast<CoverageLabel>().ToList();
     List<object> header = new() { "File" };
-    header.AddRange(coverageLabels.Select(label => $"{report.Units} {CoverageLabelExtension.ToString(label)}"));
+    header.AddRange(coverageLabels
+      .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable)
+      .Select(label => $"{report.Units} {CoverageLabelExtension.ToString(label)}"));
 
     List<List<object>> body = new();
     foreach (var sourceFile in sourceFileToCoverageReportFile.Keys) {
@@ -199,13 +219,15 @@ private void CreateIndexFile(CoverageReport report, Dictionary<string, string> s
         $"<a href = \"{relativePath}{report.UniqueSuffix}.html\"" +
         $"class = \"el_package\">{relativePath}</a>"
       });
-      body.Last().AddRange(coverageLabels.Select(label =>
-        report.CoverageSpansForFile(sourceFile).Count(span => span.Label == label)).OfType<object>());
+      body.Last().AddRange(coverageLabels
+        .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable)
+        .Select(label => report.CoverageSpansForFile(sourceFile).Count(span => span.Label == label)).OfType<object>());
     }
 
     List<object> footer = new() { "Total" };
-    footer.AddRange(coverageLabels.Select(label =>
-      report.AllFiles().Select(sourceFile =>
+    footer.AddRange(coverageLabels
+      .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable)
+      .Select(label => report.AllFiles().Select(sourceFile =>
         report.CoverageSpansForFile(sourceFile).Count(span => span.Label == label)).Sum()).OfType<object>());
 
     var templateText = new StreamReader(templateStream).ReadToEnd();
@@ -264,29 +286,46 @@ 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");
-    var characterLabels = new CoverageLabel[source.Length];
-    Array.Fill(characterLabels, CoverageLabel.None);
-    IToken lastToken = new Token(1, 1);
+    var lines = source.Split(new[] { Environment.NewLine }, StringSplitOptions.None);
+    var characterLabels = new CoverageLabel[lines.Length][];
+    for (int i = 0; i < lines.Length; i++) {
+      characterLabels[i] = new CoverageLabel[lines[i].Length];
+      Array.Fill(characterLabels[i], CoverageLabel.None);
+    }
     var labeledCodeBuilder = new StringBuilder(source.Length);
     foreach (var span in report.CoverageSpansForFile(pathToSourceFile)) {
-      for (var pos = span.Span.StartToken.pos; pos <= span.Span.EndToken.pos; pos++) {
-        characterLabels[pos] = CoverageLabelExtension.Combine(characterLabels[pos], span.Label);
+      var line = span.Span.StartToken.line - 1;
+      var column = span.Span.StartToken.col - 1;
+      while (true) {
+        if (characterLabels[line].Length <= column) {
+          do { line++; }
+          while (line < characterLabels.Length && characterLabels[line].Length == 0);
+          column = 0;
+          if (characterLabels.Length == line) {
+            break;
+          }
+        }
+        if (line > span.Span.EndToken.line - 1 || (line == span.Span.EndToken.line - 1 && column > span.Span.EndToken.col - 1)) {
+          break;
+        }
+        characterLabels[line][column] = CoverageLabelExtension.Combine(characterLabels[line][column], span.Label);
+        column++;
       }
     }
 
-    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));
+    var lastLabel = CoverageLabel.NotApplicable;
+    labeledCodeBuilder.Append(OpenHtmlTag(1, 1, CoverageLabel.NotApplicable));
+    for (var line = 0; line < lines.Length; line++) {
+      for (var col = 0; col < lines[line].Length; col++) {
+        var thisLabel = characterLabels[line][col] == CoverageLabel.None ? CoverageLabel.NotApplicable : characterLabels[line][col];
+        if (thisLabel != lastLabel) {
+          labeledCodeBuilder.Append(CloseHtmlTag());
+          labeledCodeBuilder.Append(OpenHtmlTag(line + 1, col + 1, thisLabel));
+        }
+        labeledCodeBuilder.Append(lines[line][col]);
+        lastLabel = thisLabel;
       }
-
-      labeledCodeBuilder.Append(source[pos]);
-
-      lastLabel = thisLabel;
+      labeledCodeBuilder.Append(Environment.NewLine);
     }
     labeledCodeBuilder.Append(CloseHtmlTag());
 
@@ -317,6 +356,7 @@ private static string ToHtmlClass(CoverageLabel label) {
       CoverageLabel.NotCovered => "nc",
       CoverageLabel.PartiallyCovered => "pc",
       CoverageLabel.None => "none",
+      CoverageLabel.NotApplicable => "na",
       _ => ""
     };
   }
@@ -331,8 +371,8 @@ private static CoverageLabel FromHtmlClass(string htmlClass) {
     return CoverageLabel.NotCovered; // this is a fallback in case the HTML has invalid classes
   }
 
-  private string OpenHtmlTag(int pos, CoverageLabel label) {
-    var id = $"id=\"pos{pos}\"";
+  private string OpenHtmlTag(int line, int col, CoverageLabel label) {
+    var id = $"id=\"{line}:{col}\"";
     var classLabel = ToHtmlClass(label);
     return $"<span class=\"{classLabel}\" {id}>";
   }

Source/DafnyTestGeneration/BlockBasedModifier.cs

@@ -72,7 +72,7 @@ private IEnumerable<ProgramModification> VisitImplementation(
           twinBlock.cmds.Add(new AssertCmd(new Token(), new LiteralExpr(new Token(), false)));
         }
         var record = modifications.GetProgramModification(program, implementation,
-          new HashSet<string>() { state },
+          Utils.AllBlockIds(block, DafnyInfo.Options).ToHashSet(),
           testEntryNames, $"{implementation.VerboseName.Split(" ")[0]} ({state})");
         if (record.IsCovered(modifications)) {
           foreach (var twinBlock in stateToBlocksMap[state]) {

Source/DafnyTestGeneration/Main.cs

@@ -116,7 +116,6 @@ private static void PopulateCoverageReport(CoverageReport coverageReport, Progra
         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) {
@@ -144,12 +143,8 @@ private static void PopulateCoverageReport(CoverageReport coverageReport, Progra
           } catch (ArgumentException) {
             continue;
           }
-          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));
+          var rangeToken = new RangeToken(new Token(lineNumber, 1), new Token(lineNumber + 1, 0));
           rangeToken.Uri = uri;
-          rangeToken.StartToken.pos = linePos;
-          rangeToken.EndToken.pos = linePos + lineLength;
           coverageReport.LabelCode(rangeToken,
             coveredStates.Contains(state)
               ? CoverageLabel.FullyCovered