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
|
using System;
using System.Collections.Generic;
using System.IO;
using System.Linq;
using System.Text;
using System.Threading.Tasks;
using Microsoft.Boogie;
using Bpl = Microsoft.Boogie;
namespace Microsoft.Dafny {
// FIXME: This should not be duplicated here
class DafnyConsolePrinter : ConsolePrinter {
public override void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null) {
// Dafny has 0-indexed columns, but Boogie counts from 1
var realigned_tok = new Token(tok.line, tok.col - 1);
realigned_tok.kind = tok.kind;
realigned_tok.pos = tok.pos;
realigned_tok.val = tok.val;
realigned_tok.filename = tok.filename;
base.ReportBplError(realigned_tok, message, error, tw, category);
if (tok is Dafny.NestedToken) {
var nt = (Dafny.NestedToken)tok;
ReportBplError(nt.Inner, "Related location", false, tw);
}
}
}
class DafnyHelper {
private string fname;
private string source;
private string[] args;
private readonly Dafny.ErrorReporter reporter;
private Dafny.Program dafnyProgram;
private Bpl.Program boogieProgram;
public DafnyHelper(string[] args, string fname, string source) {
this.args = args;
this.fname = fname;
this.source = source;
this.reporter = new Dafny.ConsoleErrorReporter();
}
public bool Verify() {
ServerUtils.ApplyArgs(args, reporter);
return Parse() && Resolve() && Translate() && Boogie();
}
private bool Parse() {
Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null);
Dafny.BuiltIns builtIns = new Dafny.BuiltIns();
var success = (Dafny.Parser.Parse(source, fname, fname, module, builtIns, new Dafny.Errors(reporter)) == 0 &&
Dafny.Main.ParseIncludes(module, builtIns, new List<string>(), new Dafny.Errors(reporter)) == null);
if (success) {
dafnyProgram = new Dafny.Program(fname, module, builtIns, reporter);
}
return success;
}
private bool Resolve() {
var resolver = new Dafny.Resolver(dafnyProgram);
resolver.ResolveProgram(dafnyProgram);
return reporter.Count(ErrorLevel.Error) == 0;
}
private bool Translate() {
var translator = new Dafny.Translator(reporter) { InsertChecksums = true, UniqueIdPrefix = fname };
boogieProgram = translator.Translate(dafnyProgram); // FIXME how are translation errors reported?
return true;
}
private bool Boogie() {
if (boogieProgram.Resolve() == 0 && boogieProgram.Typecheck() == 0) { //FIXME ResolveAndTypecheck?
ExecutionEngine.EliminateDeadVariables(boogieProgram);
ExecutionEngine.CollectModSets(boogieProgram);
ExecutionEngine.CoalesceBlocks(boogieProgram);
ExecutionEngine.Inline(boogieProgram);
//NOTE: We could capture errors instead of printing them (pass a delegate instead of null)
switch (ExecutionEngine.InferAndVerify(boogieProgram, new PipelineStatistics(), "ServerProgram", null, DateTime.UtcNow.Ticks.ToString())) {
case PipelineOutcome.Done:
case PipelineOutcome.VerificationCompleted:
return true;
}
}
return false;
}
}
}
|
