forked from dafny-lang/dafny
-
Notifications
You must be signed in to change notification settings - Fork 1
/
DafnyConsolePrinter.cs
157 lines (134 loc) · 5.36 KB
/
DafnyConsolePrinter.cs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
using System;
using System.Collections.Concurrent;
using System.Collections.Generic;
using System.CommandLine;
using System.IO;
using System.Linq;
using DafnyCore;
using Microsoft.Boogie;
using VC;
namespace Microsoft.Dafny;
public class DafnyConsolePrinter : ConsolePrinter {
public new DafnyOptions Options {
get => options;
set {
base.Options = value;
options = value;
}
}
private readonly ConcurrentDictionary<Uri, List<string>> fsCache = new();
private DafnyOptions options;
public record ImplementationLogEntry(string Name, Boogie.IToken Tok);
public record VCResultLogEntry(
int VCNum,
DateTime StartTime,
TimeSpan RunTime,
ProverInterface.Outcome Outcome,
List<(Boogie.IToken Tok, string Description)> Asserts,
IEnumerable<TrackedNodeComponent> CoveredElements,
int ResourceCount);
public record VerificationResultLogEntry(
ConditionGeneration.Outcome Outcome,
TimeSpan RunTime,
int ResourceCount,
List<VCResultLogEntry> VCResults,
List<Counterexample> Counterexamples);
public record ConsoleLogEntry(ImplementationLogEntry Implementation, VerificationResultLogEntry Result);
public static VerificationResultLogEntry DistillVerificationResult(VerificationResult verificationResult) {
return new VerificationResultLogEntry(
verificationResult.Outcome, verificationResult.End - verificationResult.Start,
verificationResult.ResourceCount, verificationResult.VCResults.Select(DistillVCResult).ToList(), verificationResult.Errors);
}
private static VCResultLogEntry DistillVCResult(VCResult r) {
return new VCResultLogEntry(r.vcNum, r.startTime, r.runTime, r.outcome,
r.asserts.Select(a => (a.tok, a.Description.SuccessDescription)).ToList(), r.coveredElements,
r.resourceCount);
}
public ConcurrentBag<ConsoleLogEntry> VerificationResults { get; } = new();
public override void AdvisoryWriteLine(TextWriter output, string format, params object[] args) {
if (output == Console.Out) {
int foregroundColor = (int)Console.ForegroundColor;
Console.ForegroundColor = ConsoleColor.Yellow;
output.WriteLine(format, args);
Console.ForegroundColor = (ConsoleColor)foregroundColor;
} else {
output.WriteLine(format, args);
}
}
private string GetFileLine(Uri uri, int lineIndex) {
List<string> lines = fsCache.GetOrAdd(uri, key => {
try {
// Note: This is not guaranteed to be the same file that Dafny parsed. To ensure that, Dafny should keep
// an in-memory version of each file it parses.
var file = DafnyFile.CreateAndValidate(new ErrorReporterSink(options), OnDiskFileSystem.Instance, options, uri, Token.NoToken);
using var reader = file.GetContent();
lines = Util.Lines(reader).ToList();
} catch (Exception) {
lines = new List<string>();
}
return lines;
});
if (0 <= lineIndex && lineIndex < lines.Count) {
return lines[lineIndex];
}
return null;
}
public void WriteSourceCodeSnippet(IToken tok, TextWriter tw) {
string line = GetFileLine(tok.Uri, tok.line - 1);
if (line == null) {
return;
}
string lineNumber = tok.line.ToString();
string lineNumberSpaces = new string(' ', lineNumber.Length);
string columnSpaces = new string(' ', tok.col - 1);
var lineStartPos = tok.pos - tok.col + 1;
var lineEndPos = lineStartPos + line.Length;
var tokEndPos = tok.pos + tok.val.Length;
if (tok is RangeToken rangeToken) {
tokEndPos = rangeToken.EndToken.pos + rangeToken.EndToken.val.Length;
}
var underlineLength = Math.Max(1, Math.Min(tokEndPos - tok.pos, lineEndPos - tok.pos));
string underline = new string('^', underlineLength);
tw.WriteLine($"{lineNumberSpaces} |");
tw.WriteLine($"{lineNumber} | {line}");
tw.WriteLine($"{lineNumberSpaces} | {columnSpaces}{underline}");
tw.WriteLine("");
}
public static readonly Option<bool> ShowSnippets = new("--show-snippets", () => true,
"Show a source code snippet for each Dafny message.");
static DafnyConsolePrinter() {
DooFile.RegisterNoChecksNeeded(ShowSnippets);
}
public DafnyConsolePrinter(DafnyOptions options) {
Options = options;
}
public override void ReportBplError(Boogie.IToken tok, string message, bool error, TextWriter tw, string category = null) {
if (Options.Verbosity == CoreOptions.VerbosityLevel.Silent) {
return;
}
if (category != null) {
message = $"{category}: {message}";
}
var dafnyToken = BoogieGenerator.ToDafnyToken(options.Get(ShowSnippets), tok);
message = $"{dafnyToken.TokenToString(Options)}: {message}";
if (error) {
ErrorWriteLine(tw, message);
} else {
tw.WriteLine(message);
}
if (Options.Get(ShowSnippets)) {
if (tok is IToken dafnyTok) {
WriteSourceCodeSnippet(dafnyTok, tw);
} else {
ErrorWriteLine(tw, "No Dafny location information, so snippet can't be generated.");
}
}
if (tok is NestedToken nestedToken) {
ReportBplError(nestedToken.Inner, "Related location", false, tw);
}
}
public override void ReportEndVerifyImplementation(Implementation implementation, VerificationResult result) {
var impl = new ImplementationLogEntry(implementation.VerboseName, implementation.tok);
VerificationResults.Add(new ConsoleLogEntry(impl, DistillVerificationResult(result)));
}
}