-
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
Verification coverage report #4625
Changes from all commits
10786bf
94e5829
e208197
efb99e4
0873a7f
b51fc59
ed001d7
6efb54a
18bc776
c9c5e16
1ce654f
1aa5258
ae43ffe
76d0938
43c2377
702e954
60cfa5b
5e699c8
652acb6
6fd0765
4ba4328
d6e8aa6
b48afa4
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 |
---|---|---|
|
@@ -4,6 +4,9 @@ | |
using System.Linq; | ||
using System.Text; | ||
using System.Text.RegularExpressions; | ||
using DafnyCore.Verifier; | ||
using Microsoft.Boogie; | ||
using Microsoft.Extensions.Primitives; | ||
|
||
namespace Microsoft.Dafny; | ||
|
||
|
@@ -22,7 +25,7 @@ public class CoverageReporter { | |
private static readonly Regex TableFooterRegex = new(@"\{\{TABLE_FOOTER\}\}"); | ||
private static readonly Regex TableBodyRegex = new(@"\{\{TABLE_BODY\}\}"); | ||
private static readonly Regex IndexFileNameRegex = new(@"index(.*)\.html"); | ||
private static readonly Regex SpanRegexInverse = new("class=\"([a-z]+)\" id=\"line([0-9]+)col([0-9]+)-line([0-9]+)col([0-9]+)\""); | ||
private static readonly Regex PosRegexInverse = new("class=\"([a-z]+)\" id=\"pos([0-9]+)\">"); | ||
private const string CoverageReportTemplatePath = "coverage_report_template.html"; | ||
private const string CoverageReportIndexTemplatePath = "coverage_report_index_template.html"; | ||
private const string CoverageReportSupportingFilesPath = ".resources"; | ||
|
@@ -39,6 +42,28 @@ public CoverageReporter(DafnyOptions options) { | |
this.options = options; | ||
} | ||
|
||
|
||
public void SerializeVerificationCoverageReport(ProofDependencyManager depManager, Program dafnyProgram, IEnumerable<TrackedNodeComponent> usedComponents, string coverageReportDir) { | ||
var usedDependencies = | ||
usedComponents.Select(depManager.GetFullIdDependency).ToHashSet(); | ||
var allDependencies = | ||
depManager | ||
.GetAllPotentialDependencies() | ||
.OrderBy(dep => dep.Range.StartToken); | ||
var coverageReport = new CoverageReport("Verification coverage", "Lines", "_verification", dafnyProgram); | ||
foreach (var dep in allDependencies) { | ||
if (dep is FunctionDefinitionDependency) { | ||
continue; | ||
} | ||
coverageReport.LabelCode(dep.Range, | ||
usedDependencies.Contains(dep) | ||
? CoverageLabel.FullyCovered | ||
: CoverageLabel.NotCovered); | ||
} | ||
|
||
SerializeCoverageReports(coverageReport, coverageReportDir); | ||
} | ||
|
||
public void Merge(List<string> coverageReportsToMerge, string coverageReportOutDir) { | ||
// assume only one report in directory for now | ||
List<CoverageReport> reports = new(); | ||
|
@@ -80,16 +105,17 @@ private static CoverageReport ParseCoverageReport(string reportDir, string name, | |
continue; | ||
} | ||
var uri = new Uri(uriMatch.Groups[1].Value); | ||
var lastEndToken = new Token(1, 1); | ||
report.RegisterFile(uri); | ||
foreach (var span in SpanRegexInverse.Matches(source).Where(match => match.Success)) { | ||
if (int.TryParse(span.Groups[2].Value, out var startLine) && | ||
int.TryParse(span.Groups[3].Value, out var startCol) && | ||
int.TryParse(span.Groups[4].Value, out var endLine) && | ||
int.TryParse(span.Groups[5].Value, out var endCol)) { | ||
var startToken = new Token(startLine, startCol); | ||
startToken.Uri = uri; | ||
var endToken = new Token(endLine, endCol); | ||
foreach (var span in PosRegexInverse.Matches(source).Where(match => match.Success)) { | ||
if (int.TryParse(span.Groups[2].Value, out var pos)) { | ||
var startToken = new Token(1, 1); | ||
startToken.Uri = uri; | ||
startToken.pos = pos; | ||
lastEndToken.pos = pos; | ||
var endToken = new Token(1, 1); | ||
endToken.Uri = uri; | ||
lastEndToken = endToken; | ||
var rangeToken = new RangeToken(startToken, endToken); | ||
rangeToken.Uri = uri; | ||
report.LabelCode(rangeToken, FromHtmlClass(span.Groups[1].Value)); | ||
|
@@ -125,7 +151,7 @@ private void SerializeCoverageReports(List<CoverageReport> reports, string repor | |
.TakeWhile((c, i) => allFiles.All(s => s[i] == c)).ToArray()).Length; | ||
Dictionary<string, string> sourceFileToCoverageReport = new Dictionary<string, string>(); | ||
foreach (var fileName in allFiles) { | ||
var directoryForFile = Path.Combine(sessionDirectory, Path.GetDirectoryName(fileName)?[prefixLength..] ?? ""); | ||
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++) { | ||
|
@@ -239,16 +265,31 @@ private void CopyStyleFiles(string baseDirectory) { | |
private string HtmlReportForFile(CoverageReport report, string pathToSourceFile, string baseDirectory, string linksToOtherReports) { | ||
var source = new StreamReader(pathToSourceFile).ReadToEnd(); | ||
var lines = source.Split("\n"); | ||
IToken lastToken = new Token(0, 0); | ||
var characterLabels = new CoverageLabel[source.Length]; | ||
Array.Fill(characterLabels, CoverageLabel.None); | ||
IToken lastToken = new Token(1, 1); | ||
var labeledCodeBuilder = new StringBuilder(source.Length); | ||
foreach (var span in report.CoverageSpansForFile(pathToSourceFile)) { | ||
AppendCodeBetweenTokens(labeledCodeBuilder, lines, lastToken, span.Span.StartToken); | ||
labeledCodeBuilder.Append(OpenHtmlTag(span)); | ||
AppendCodeBetweenTokens(labeledCodeBuilder, lines, span.Span.StartToken, span.Span.EndToken); | ||
labeledCodeBuilder.Append(CloseHtmlTag(span)); | ||
lastToken = span.Span.EndToken; | ||
for (var pos = span.Span.StartToken.pos; pos <= span.Span.EndToken.pos; pos++) { | ||
characterLabels[pos] = CoverageLabelExtension.Combine(characterLabels[pos], span.Label); | ||
} | ||
Comment on lines
+273
to
+275
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. Have just realized that this loop replaces about 30 lines of some binary search recursion madness I wrote... 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 originally started thinking about interval trees when I realized that I needed to deal with arbitrary types and degrees of overlap. And then I realized that just tracking the labels on a per-character basis was simpler and probably even more efficient. |
||
} | ||
AppendCodeBetweenTokens(labeledCodeBuilder, lines, lastToken, null); | ||
|
||
CoverageLabel lastLabel = CoverageLabel.None; | ||
labeledCodeBuilder.Append(OpenHtmlTag(0, CoverageLabel.None)); | ||
for (var pos = 0; pos < source.Length; pos++) { | ||
var thisLabel = characterLabels[pos]; | ||
if (thisLabel != lastLabel) { | ||
labeledCodeBuilder.Append(CloseHtmlTag()); | ||
labeledCodeBuilder.Append(OpenHtmlTag(pos, thisLabel)); | ||
} | ||
|
||
labeledCodeBuilder.Append(source[pos]); | ||
|
||
lastLabel = thisLabel; | ||
} | ||
labeledCodeBuilder.Append(CloseHtmlTag()); | ||
|
||
var assembly = System.Reflection.Assembly.GetCallingAssembly(); | ||
var templateStream = assembly.GetManifestResourceStream(CoverageReportTemplatePath); | ||
var labeledCode = labeledCodeBuilder.ToString(); | ||
|
@@ -266,21 +307,6 @@ private string HtmlReportForFile(CoverageReport report, string pathToSourceFile, | |
return LabeledCodeRegex.Replace(templateText, labeledCode); | ||
} | ||
|
||
/// <summary> | ||
/// Append code from <param name="lines"></param> that lies between <param name="start"></param> and | ||
/// <param name="end"></param> tokens to the <param name="stringBuilder"></param> | ||
/// </summary> | ||
private static void AppendCodeBetweenTokens(StringBuilder stringBuilder, string[] lines, IToken start, IToken end) { | ||
var currToken = new Token(start.line, start.col); | ||
while (currToken.line < lines.Length && (end == null || currToken.line < end.line)) { | ||
stringBuilder.Append(lines[currToken.line][currToken.col..] + "\n"); | ||
currToken.line += 1; | ||
} | ||
if (end != null && currToken.line < lines.Length) { | ||
stringBuilder.Append(lines[currToken.line][currToken.col..end.col]); | ||
} | ||
} | ||
|
||
/// <summary> | ||
/// Return HTML class used to highlight lines in different colors depending on the coverage. | ||
/// Look at assets/.resources/coverage.css for the styles corresponding to these classes | ||
|
@@ -290,6 +316,7 @@ private static string ToHtmlClass(CoverageLabel label) { | |
CoverageLabel.FullyCovered => "fc", | ||
CoverageLabel.NotCovered => "nc", | ||
CoverageLabel.PartiallyCovered => "pc", | ||
CoverageLabel.None => "none", | ||
_ => "" | ||
}; | ||
} | ||
|
@@ -304,13 +331,13 @@ private static CoverageLabel FromHtmlClass(string htmlClass) { | |
return CoverageLabel.NotCovered; // this is a fallback in case the HTML has invalid classes | ||
} | ||
|
||
private string OpenHtmlTag(CoverageSpan span) { | ||
var id = $"id=\"line{span.Span.StartToken.line}col{span.Span.StartToken.col}-line{span.Span.EndToken.line}col{span.Span.EndToken.col}\""; | ||
var classLabel = ToHtmlClass(span.Label); | ||
private string OpenHtmlTag(int pos, CoverageLabel label) { | ||
var id = $"id=\"pos{pos}\""; | ||
var classLabel = ToHtmlClass(label); | ||
return $"<span class=\"{classLabel}\" {id}>"; | ||
} | ||
|
||
private string CloseHtmlTag(CoverageSpan span) { | ||
private string CloseHtmlTag() { | ||
return "</span>"; | ||
} | ||
} |
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.
Is it worth explicitly initializing values with
None
so that the order of labels in theCoverageLabel
enum doesn't affect the behavior?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.
Yeah, good catch. I'll change that.