Improve encapsulation

Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs

@@ -158,6 +158,10 @@ private class CSharpCompilationResult {
  return RunProcess(psi, outputWriter, errorWriter) == 0;
  }
 
+ public override void PopulateCoverageReport(CoverageReport coverageReport) {
+ compiler.Coverage.PopulateCoverageReport(coverageReport);
+ }
+
  public CsharpBackend(DafnyOptions options) : base(options) {
  }
 }

Source/DafnyCore/Compilers/CoverageInstrumenter.cs

@@ -94,15 +94,18 @@ public class CoverageInstrumenter {
  }
  }
 
- public void PopulateCoverageReport(CoverageReport report) {
- var tallies = File.ReadLines(talliesFilePath).Select(int.Parse).ToArray();
- foreach (var ((token, _), tally) in legend.Zip(tallies)) {
- var label = tally == 0 ? CoverageLabel.NotCovered : CoverageLabel.FullyCovered;
- // 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);
+ public void PopulateCoverageReport(CoverageReport coverageReport) {
+ var coverageReportDir = compiler.Options?.Get(CommonOptionBag.ExecutionCoverageReport);
+ if (coverageReportDir != null) {
+ var tallies = File.ReadLines(talliesFilePath).Select(int.Parse).ToArray();
+ foreach (var ((token, _), tally) in legend.Zip(tallies)) {
+ var label = tally == 0 ? CoverageLabel.NotCovered : CoverageLabel.FullyCovered;
+ // 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;
+ coverageReport.LabelCode(rangeToken, label);
+ }
  }
  }
 

Source/DafnyCore/Compilers/ExecutableBackend.cs

@@ -70,10 +70,6 @@ public abstract class ExecutableBackend : IExecutableBackend {
  Compiler.Coverage.WriteLegendFile();
  }
 
- public override CoverageInstrumenter GetCoverageAfterRun() {
- return Compiler.Coverage;
- }
-
  protected abstract SinglePassCompiler CreateCompiler();
 
  public override string PublicIdProtect(string name) {

Source/DafnyCore/Plugins/IExecutableBackend.cs

@@ -132,8 +132,6 @@ public abstract class IExecutableBackend {
  /// </summary>
  public virtual void OnPostCompile() { }
 
- public abstract CoverageInstrumenter GetCoverageAfterRun();
-
  /// <summary>
  /// Remove previously generated source files. This is only applicable to compilers that put sources in a separate
  /// directory (e.g. Java). For other compilers, this method should do nothing.
@@ -200,4 +198,8 @@ public abstract class IExecutableBackend {
  public virtual Command GetCommand() {
  return new Command(TargetId, $"Translate Dafny sources to {TargetName} source and build files.");
  }
+
+ public virtual void PopulateCoverageReport(CoverageReport coverageReport) {
+ throw new NotImplementedException();
+ }
 }

Source/DafnyDriver/CompilerDriver.cs

@@ -569,9 +569,8 @@ private record TargetPaths(string Directory, string Filename) {
  if (compiledCorrectly) {
  var coverageReportDir = options.Get(CommonOptionBag.ExecutionCoverageReport);
  if (coverageReportDir != null) {
- var coverage = compiler.GetCoverageAfterRun();
  var coverageReport = new CoverageReport("Execution Coverage", "Branches", "_tests_actual", dafnyProgram);
- coverage.PopulateCoverageReport(coverageReport);
+ compiler.PopulateCoverageReport(coverageReport);
  new CoverageReporter(options).SerializeCoverageReports(coverageReport, coverageReportDir);
  }
  }
@@ -630,10 +629,6 @@ class NoExecutableBackend : IExecutableBackend {
  throw new NotSupportedException();
  }
 
- public override CoverageInstrumenter GetCoverageAfterRun() {
- throw new NotImplementedException();
- }
-
  public NoExecutableBackend([NotNull] DafnyOptions options) : base(options) {
  }
  }