feat: Execution branch coverage report #4755
Conversation
…ove stdlib coverage
robin-aws
changed the title
|
I've fixed the refman failure locally but don't want to push and trigger another CI run until I've also addressed any PR feedback |
| protected void EmitCoverageReportInstrumentation(Program program, ConcreteSyntaxTree wr) { | ||
| wr.WriteLine(@" | ||
| namespace DafnyProfiling { | ||
| public class CodeCoverage { |
There was a problem hiding this comment.
Not without breaking the existing /coverage option, since the idea is that you could provide your own implementation of DafnyProfilng.CodeCoverage as per the BranchCoverage.dfy test.
| 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.
This is nice because then merging actual and expected coverage would work well. The merge-coverage-reports command could perhaps use a --diff flag that would produce a report indicating where two coverage reports differed.
There was a problem hiding this comment.
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.
| 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.
You could call this --execution-coverage-report, since that term shows up in the variable name and the description text. :)
There was a problem hiding this comment.
I did consider that, but then it would feel weird to not further qualify dafny generate-tests --coverage-report as well, perhaps as --expected-execution-coverage-report. Given the generate-tests one is already released I'm more inclined to leave both with the simpler name.
| @@ -32,6 +32,20 @@ method {:test} TestMyMap() { | |||
| expect greeting == "Hello\nDafny\n"; | |||
| } | |||
|
|
|||
| method {:test} TestGetGreetingSuccess() { | |||
There was a problem hiding this comment.
The coverage reporting is already bearing dividends. :)
| @@ -1 +1 @@ | |||
| The new `--coverage-report` flag to `dafny verify` creates an HTML report highlighting which portions of the program were and were not necessary for verification. The format is the same as for `dafny generate-tests --coverage-report` and files from the two commands can be merged. | |||
| The new `--verification-coverage-report` flag to `dafny verify` creates an HTML report highlighting which portions of the program were and were not necessary for verification. The format is the same as for `dafny generate-tests --coverage-report` and files from the two commands can be merged. | |||
There was a problem hiding this comment.
Thanks for being thorough about where you change the name of this flag!
…time-coverage-report
### Description #4755 broke the nightly build because I neglected to escape a string literal properly. Works just fine as long as your directory separator is `/`, but then Windows had to go and be all different. :) ### How has this been tested? Existing tests with `run-deep-tests`. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Description
Implements an execution coverage report in the same format as the existing verification coverage and expected generated test coverage reports. Mainly this just meant using the existing low-level instrumentation provided by the old CLI
/coverageoption to write coverage data to a temporary file during execution, and then parsing this data and populating aCoverageReportobject. I've only implemented this for C# for now, since the execution coverage SHOULD generally be identical across languages (the instrumentation is emitted from the common SinglePassCompiler) but it wouldn't take much work to hook it up for the other backends.Also adds this to the
DafnyStandardLibrariesproject, and augments the existing coverage report generation to handle.doofiles and Uris somewhat better.Also renames the existing verification option
--coverage-reportto--verification-coverage-report, since this option is almost always in scope (since most commands run verification), and fordafny testanddafny run"coverage report" more naturally means execution coverage instead. The former hasn't been released yet so this won't break anyone. :)Resolves #4671
How has this been tested?
comp/CoverageReport.dfy, similar to the existinglogger/CoverageReport.dfyBy submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.