Partial work to handle implicit parent modules

(just capturing to come back to later)

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -9,7 +9,7 @@ namespace Microsoft.Dafny;
 
 public record PrefixNameModule(IReadOnlyList<IToken> Parts, LiteralModuleDecl Module);
 
-public class ModuleDefinition : RangeNode, IAttributeBearingDeclaration, ICloneable<ModuleDefinition>, IHasSymbolChildren {
+public class  ModuleDefinition : RangeNode, IAttributeBearingDeclaration, ICloneable<ModuleDefinition>, IHasSymbolChildren {
 
  public IToken BodyStartTok = Token.NoToken;
  public IToken TokenWithTrailingDocString = Token.NoToken;

Source/DafnyCore/CoverageReport/CoverageReport.cs

@@ -13,6 +13,7 @@ public class CoverageReport {
 
  private readonly Dictionary<Uri, List<CoverageSpan>> labelsByFile;
  private readonly Dictionary<Uri, HashSet<ModuleDefinition>> modulesByFile;
+
  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
@@ -72,14 +73,14 @@ public void RegisterFile(Uri uri) {
 
  private void RegisterFiles(Node astNode) {
  if (astNode.StartToken.ActualFilename != null) {
- var uri = astNode.StartToken.Uri;
-  labelsByFile.GetOrCreate(uri, () => new List<CoverageSpan>());
-  
-  if (astNode is LiteralModuleDecl moduleDecl) {
-  modulesByFile.GetOrCreate(uri, () => new HashSet<ModuleDefinition>()).Add(moduleDecl.ModuleDef);
-  
- RegisterFiles(moduleDecl.ModuleDef);
- }
+ labelsByFile.GetOrCreate(astNode.StartToken.Uri, () => new List<CoverageSpan>());
+ }
+
+ if (astNode is LiteralModuleDecl moduleDecl) {
+ // Uri may be null for implicit modules
+ modulesByFile.GetOrCreate(astNode.StartToken.Uri, () => new HashSet<ModuleDefinition>()).Add(moduleDecl.ModuleDef);
+
+ RegisterFiles(moduleDecl.ModuleDef);
  }
 
  foreach (var declaration in astNode.Children.OfType<LiteralModuleDecl>()) {

Source/DafnyDriver/CoverageReporter.cs

@@ -20,9 +20,12 @@ public class CoverageReporter {
  private static readonly Regex UriRegexInversed = new(@"<h1 hidden>([^\n]*)</h1>");
  private static readonly Regex IndexLinkRegex = new(@"\{\{INDEX_LINK\}\}");
  private static readonly Regex LinksToOtherReportsRegex = new(@"\{\{LINKS_TO_OTHER_REPORTS\}\}");
- private static readonly Regex TableHeaderRegex = new(@"\{\{TABLE_HEADER\}\}");
- private static readonly Regex TableFooterRegex = new(@"\{\{TABLE_FOOTER\}\}");
- private static readonly Regex TableBodyRegex = new(@"\{\{TABLE_BODY\}\}");
+ private static readonly Regex ByFileTableHeaderRegex = new(@"\{\{BY_FILE_TABLE_HEADER\}\}");
+ private static readonly Regex ByFileTableFooterRegex = new(@"\{\{BY_FILE_TABLE_FOOTER\}\}");
+ private static readonly Regex ByFileTableBodyRegex = new(@"\{\{BY_FILE_TABLE_BODY\}\}");
+ private static readonly Regex ByModuleTableHeaderRegex = new(@"\{\{BY_MODULE_TABLE_HEADER\}\}");
+ private static readonly Regex ByModuleTableFooterRegex = new(@"\{\{BY_MODULE_TABLE_FOOTER\}\}");
+ private static readonly Regex ByModuleTableBodyRegex = new(@"\{\{BY_MODULE_TABLE_BODY\}\}");
  private static readonly Regex IndexFileNameRegex = new(@"index(.*)\.html");
  private static readonly Regex PosRegexInverse = new("class=\"([a-z]+)\" id=\"([0-9]+):([0-9]+)\"");
  private const string CoverageReportTemplatePath = "coverage_report_template.html";
@@ -218,7 +221,7 @@ private void CreateIndexFile(CoverageReport report, Dictionary<Uri, string> sour
  return;
  }
  var coverageLabels = Enum.GetValues(typeof(CoverageLabel)).Cast<CoverageLabel>().ToList();
- List<object> header = new() { "File", "Module" };
+ List<object> header = new() { "File" };
  header.AddRange(coverageLabels
  .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable)
  .Select(label => $"{report.Units} {CoverageLabelExtension.ToString(label)}"));
@@ -229,8 +232,7 @@ private void CreateIndexFile(CoverageReport report, Dictionary<Uri, string> sour
 
  body.Add(new() {
  $"<a href = \"{relativePath}{report.UniqueSuffix}.html\"" +
- $"class = \"el_package\">{relativePath}</a>",
- "All modules"
+ $"class = \"el_package\">{relativePath}</a>"
  });
 
  body.Last().AddRange(coverageLabels
@@ -240,7 +242,6 @@ private void CreateIndexFile(CoverageReport report, Dictionary<Uri, string> sour
 
  foreach (var module in report.ModulesInFile(sourceFile).OrderBy(m => m.FullName)) {
  body.Add(new() {
- "",
  module.FullName
  });
 
@@ -255,7 +256,15 @@ private void CreateIndexFile(CoverageReport report, Dictionary<Uri, string> sour
  .Count(span => span.Label == label)).OfType<object>());
  }
  }
+
+ header = new() { "Module" };
+ header.AddRange(coverageLabels
+ .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable)
+ .Select(label => $"{report.Units} {CoverageLabelExtension.ToString(label)}"));
 
+ body = new();
+ PopulateByModuleTableBody(report, )
+
  List<object> footer = new() { "Total", "" };
  footer.AddRange(coverageLabels
  .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable)
@@ -265,12 +274,54 @@ private void CreateIndexFile(CoverageReport report, Dictionary<Uri, string> sour
  var templateText = new StreamReader(templateStream).ReadToEnd();
  templateText = LinksToOtherReportsRegex.Replace(templateText, linksToOtherReports);
  templateText = FileNameRegex.Replace(templateText, report.Name);
- templateText = TableHeaderRegex.Replace(templateText, MakeIndexFileTableRow(header));
- templateText = TableFooterRegex.Replace(templateText, MakeIndexFileTableRow(footer));
- templateText = TableBodyRegex.Replace(templateText, string.Join("\n", body.Select(MakeIndexFileTableRow)));
+
+ templateText = ByFileTableBodyRegex.Replace(templateText, MakeIndexFileTableRow(header));
+ templateText = ByFileTableFooterRegex.Replace(templateText, MakeIndexFileTableRow(footer));
+ templateText = ByFileTableBodyRegex.Replace(templateText, string.Join("\n", body.Select(MakeIndexFileTableRow)));
+
+ templateText = ByModuleTableBodyRegex.Replace(templateText, MakeIndexFileTableRow(header));
+ templateText = ByModuleTableFooterRegex.Replace(templateText, MakeIndexFileTableRow(footer));
+ templateText = ByModuleTableBodyRegex.Replace(templateText, string.Join("\n", body.Select(MakeIndexFileTableRow)));
+
  File.WriteAllText(Path.Combine(baseDirectory, $"index{report.UniqueSuffix}.html"), templateText);
  }
 
+ private static void PopulateByModuleTableBody(CoverageReport report, ModuleDefinition module, List<CoverageLabel> coverageLabels, List<List<object>> body) {
+ body.Add(CountsForModule(report, module, coverageLabels).OfType<object>().ToList());
+
+ foreach (var child in module.TopLevelDecls.OrderBy(decl => decl.Name)) {
+ if (child is LiteralModuleDecl moduleDecl) {
+ PopulateByModuleTableBody(report, moduleDecl.ModuleDef, coverageLabels, body);
+ }
+ }
+ }
+
+ private static List<int> CountsForModule(CoverageReport report, ModuleDefinition module, List<CoverageLabel> coverageLabels) {
+ if (module.StartToken.Uri != null) {
+ var moduleRange = module.RangeToken.ToDafnyRange();
+ return coverageLabels
+ .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable)
+ .Select(label => report.CoverageSpansForFile(module.StartToken.Uri)
+ // span.Span.Intersects(module.RangeToken) would be cleaner,
+ // but unfortunately coverage span tokens don't currently always
+ // have Token.pos set correctly. :(
+ .Where(span => moduleRange.Contains(span.Span.ToDafnyRange().Start))
+ .Count(span => span.Label == label)).ToList();
+ } else {
+ var sums = new int[coverageLabels.Count];
+ foreach (var child in module.TopLevelDecls) {
+ if (child is LiteralModuleDecl moduleDecl) {
+ var childModuleCounts = CountsForModule(report, moduleDecl.ModuleDef, coverageLabels);
+ for (var labelIndex = 0; labelIndex < coverageLabels.Count; labelIndex++) {
+ sums[labelIndex] += childModuleCounts[labelIndex];
+ }
+ }
+ }
+
+ return sums.ToList();
+ }
+ }
+
  /// <summary>
  /// Creates a set of links to be inserted in <param name="thisReport"></param> that point to corresponding
  /// report files for the same <param name="sourceFileName"></param>

Source/DafnyDriver/assets/coverage_report_index_template.html

@@ -14,13 +14,24 @@
 <h1>{{FILENAME}}</h1>
 <table class="coverage" cellspacing="0" id="coveragetable">
  <thead>
- {{TABLE_HEADER}}
+ {{BY_FILE_TABLE_HEADER}}
  </thead>
  <tfoot>
- {{TABLE_FOOTER}}
+ {{BY_FILE_TABLE_FOOTER}}
  </tfoot>
  <tbody>
- {{TABLE_BODY}}
+ {{BY_FILE_TABLE_BODY}}
+ </tbody>
+</table>
+<table class="coverage" cellspacing="0" id="coveragetable">
+ <thead>
+ {{BY_MODULE_TABLE_HEADER}}
+ </thead>
+ <tfoot>
+ {{BY_MODULE_TABLE_FOOTER}}
+ </tfoot>
+ <tbody>
+ {{BY_MODULE_TABLE_BODY}}
  </tbody>
 </table>
 <div class="footer">