Improve coverage report formatting, hook up to stdlibs, start to impr…

…ove stdlib coverage

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 {

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);
  }
  }
- 
+
 }

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>()) {

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
 }

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);

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,16 +292,17 @@ 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++) {
  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)) {
+ 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);
  }
 

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) {

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

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? {