Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Allow filtering of combined coverage reports #4673

Merged
merged 3 commits into from
Oct 17, 2023
Merged

Allow filtering of combined coverage reports #4673

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
a273035
Allow filtering of combined coverage reports
atomb Oct 16, 2023
57482af
Add changelog entry
atomb Oct 16, 2023
06a55b6
Merge branch 'master' into only-label
atomb Oct 17, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions Source/DafnyDriver/Commands/CoverageReportCommand.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,20 +7,26 @@
using System.IO;
using System.Linq;
using System.Threading.Tasks;
using DafnyCore;

namespace Microsoft.Dafny;

static class CoverageReportCommand {

public static readonly Option<CoverageLabel?> OnlyLabelOption = new("--only-label",
"Skip coverage labels other than the given one, after merging labels from the input reports.");

public static IEnumerable<Option> Options =>
new Option[] {
CommonOptionBag.NoTimeStampForCoverageReport,
OnlyLabelOption
};

static CoverageReportCommand() {
ReportsArgument = new("reports", r => {
return r.Tokens.Where(t => !string.IsNullOrEmpty(t.Value)).Select(t => new FileInfo(t.Value)).ToList();
}, true, "directories with coverage reports to be merged");
DooFile.RegisterNoChecksNeeded(OnlyLabelOption);
}

// FilesArgument is intended for Dafny files, so CoverageReportCommand adds its own argument instead
Expand Down
6 changes: 5 additions & 1 deletion Source/DafnyDriver/CoverageReporter.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,11 +85,15 @@ public void Merge(List<string> coverageReportsToMerge, string coverageReportOutD
reports.Add(ParseCoverageReport(reportDir, $"{name} ({Path.GetFileName(reportDir)})", units, suffix));
}
}

var onlyLabel = options.Get(CoverageReportCommand.OnlyLabelOption);
foreach (var report in reports) {
foreach (var fileName in report.AllFiles()) {
foreach (var span in report.CoverageSpansForFile(fileName)) {
mergedReport.RegisterFile(span.Span.Uri);
mergedReport.LabelCode(span.Span, span.Label);
if ((onlyLabel ?? span.Label) == span.Label) {
mergedReport.LabelCode(span.Span, span.Label);
}
Comment on lines +94 to +96
Copy link
Collaborator

@Dargones Dargones Oct 16, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is the intent here to display locations where both reports have the same label (i.e. intersection)? If yes, then there should be an else branch here that labels the code with the NotApplicable label. The report merged using the present approach will display the union between the two original reports.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not quite. The point is to highlight only the locations that, after merging (with union semantics), have the label specified on the command line. The expected output I've checked in looks the way I'd expect it to. The key use case I want to support is for NotCovered: highlight all locations that are not covered by either verification or tests.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Alternatively, you could see this code as taking the merged report and removing all highlighting that isn't in the specified category. The conditional is arguably a bit confusing, given that it both checks whether the option has been specified and whether the current label matches the requested label in one expression.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, I see! So you can get the intersection if you don't use --only-label and the union if you do. This makes sense!

}
}
}
Expand Down
5 changes: 5 additions & 0 deletions Test/logger/CoverageReport.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,11 @@
// RUN: %baredafny merge-coverage-reports --no-timestamp-for-coverage-report "%t"/coverage_combined "%t"/coverage_testing "%t"/coverage_verification
// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_combined/ProofDependencyLogging.dfy_combined.html > "%t"/coverage_combined.html
// RUN: %diff "%S/ProofDependencyLogging.dfy_combined.html.expect" "%t/coverage_combined.html"
// Combined, limited coverage:
// RUN: rm -rf "%t"/coverage_combined
// RUN: %baredafny merge-coverage-reports --only-label NotCovered --no-timestamp-for-coverage-report "%t"/coverage_combined_limited "%t"/coverage_testing "%t"/coverage_verification
// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_combined_limited/ProofDependencyLogging.dfy_combined.html > "%t"/coverage_combined_limited.html
// RUN: %diff "%S/ProofDependencyLogging.dfy_combined_limited.html.expect" "%t/coverage_combined_limited.html"


include "ProofDependencyLogging.dfy"
Loading
Loading