-
Notifications
You must be signed in to change notification settings - Fork 260
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat: Execution branch coverage report #4755
Changes from 15 commits
a70859f
4bc558f
b1254a4
fb55df8
99ff54b
b1f5da6
084f928
ed93db2
46d7331
6f2a5d4
b0b7fc5
e40be50
06a9068
87aa068
55616a1
9262299
64ac12d
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,18 +1,25 @@ | ||
using System.Collections.Generic; | ||
using System.Diagnostics.Contracts; | ||
using System.IO; | ||
using System.Linq; | ||
|
||
namespace Microsoft.Dafny.Compilers; | ||
|
||
public class CoverageInstrumenter { | ||
private readonly SinglePassCompiler compiler; | ||
private List<(IToken, string)>/*?*/ legend; // non-null implies options.CoverageLegendFile is non-null | ||
private string talliesFilePath; | ||
|
||
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)>(); | ||
} | ||
|
||
if (compiler.Options?.Get(CommonOptionBag.ExecutionCoverageReport) != null) { | ||
talliesFilePath = Path.GetTempFileName(); | ||
} | ||
} | ||
|
||
public bool IsRecording { | ||
|
@@ -55,7 +62,11 @@ public void InstrumentExpr(IToken tok, string description, bool resultValue, Con | |
public void EmitSetup(ConcreteSyntaxTree wr) { | ||
Contract.Requires(wr != null); | ||
if (legend != null) { | ||
wr.Write("DafnyProfiling.CodeCoverage.Setup({0})", legend.Count); | ||
wr.Write("DafnyProfiling.CodeCoverage.Setup({0}", legend.Count); | ||
if (talliesFilePath != null) { | ||
wr.Write($", \"{talliesFilePath}\""); | ||
} | ||
wr.Write(")"); | ||
compiler.EndStmt(wr); | ||
} | ||
} | ||
|
@@ -69,7 +80,7 @@ public void EmitTearDown(ConcreteSyntaxTree wr) { | |
} | ||
|
||
public void WriteLegendFile() { | ||
if (legend != null) { | ||
if (compiler.Options?.CoverageLegendFile != null) { | ||
var filename = compiler.Options.CoverageLegendFile; | ||
Contract.Assert(filename != null); | ||
TextWriter wr = filename == "-" ? compiler.Options.OutputWriter : new StreamWriter(new FileStream(Path.GetFullPath(filename), System.IO.FileMode.Create)); | ||
|
@@ -82,4 +93,20 @@ public void WriteLegendFile() { | |
legend = null; | ||
} | ||
} | ||
|
||
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. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This is nice because then merging actual and expected coverage would work well. The There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. My thoughts exactly, and although I do suspect that the actual and expected coverage don't 100% agree on coverable things yet, I don't think it will take much to align them in the future. |
||
var rangeToken = new RangeToken(new Token(token.line, 1), new Token(token.line + 1, 0)); | ||
rangeToken.Uri = token.Uri; | ||
coverageReport.LabelCode(rangeToken, label); | ||
} | ||
} | ||
} | ||
|
||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -214,14 +214,18 @@ 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.") { | ||
public static readonly Option<string> VerificationCoverageReport = new("--verification-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> 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<string> ExecutionCoverageReport = new("--coverage-report", | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. You could call this There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I did consider that, but then it would feel weird to not further qualify |
||
"Emit execution coverage report to a given directory.") { | ||
ArgumentHelpName = "directory" | ||
}; | ||
|
||
public static readonly Option<bool> IncludeRuntimeOption = new("--include-runtime", | ||
"Include the Dafny runtime as source in the target language."); | ||
|
@@ -517,7 +521,8 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps, | |
UseStandardLibraries, | ||
OptimizeErasableDatatypeWrapper, | ||
AddCompileSuffix, | ||
SystemModule | ||
SystemModule, | ||
ExecutionCoverageReport | ||
); | ||
} | ||
|
||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could we put this in the runtime?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not without breaking the existing
/coverage
option, since the idea is that you could provide your own implementation ofDafnyProfilng.CodeCoverage
as per theBranchCoverage.dfy
test.