summaryrefslogtreecommitdiff
path: root/Source/DafnyExtension
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2013-06-07 18:53:40 -0700
committerGravatar wuestholz <unknown>2013-06-07 18:53:40 -0700
commit5b726294d6604001ec162edb4e95d17c0f32b5eb (patch)
tree1f1a4a4c99a2d3c6c1484660f93fa5392f202039 /Source/DafnyExtension
parent1ee9754513e8b4acc885384676df173af5fc0e42 (diff)
DafnyExtension: Worked on integrating the verification result caching.
Diffstat (limited to 'Source/DafnyExtension')
-rw-r--r--Source/DafnyExtension/DafnyDriver.cs21
-rw-r--r--Source/DafnyExtension/ProgressMargin.cs12
-rw-r--r--Source/DafnyExtension/ResolverTagger.cs18
3 files changed, 36 insertions, 15 deletions
diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 415bf996..93bb6f8c 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -1,7 +1,9 @@
using System;
+using System.Collections.Concurrent;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using Microsoft.Boogie;
+using Microsoft.VisualStudio.Text;
using VC;
using Bpl = Microsoft.Boogie;
using Dafny = Microsoft.Dafny;
@@ -104,17 +106,18 @@ namespace DafnyLanguage
class DafnyErrorInformationFactory : ErrorInformationFactory
{
- public override ErrorInformation CreateErrorInformation(IToken tok, string msg)
+ public override ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId)
{
- return new DafnyErrorInformation(tok, msg);
+ return new DafnyErrorInformation(tok, msg, requestId);
}
}
class DafnyErrorInformation : ErrorInformation
{
- public DafnyErrorInformation(IToken tok, string msg)
+ public DafnyErrorInformation(IToken tok, string msg, string requestId)
: base(tok, msg)
{
+ RequestId = requestId;
AddNestingsAsAux(tok);
}
@@ -147,12 +150,14 @@ namespace DafnyLanguage
#region Boogie interaction
- public static bool Verify(Dafny.Program dafnyProgram, ErrorReporterDelegate er) {
+ public static ConcurrentDictionary<string, ITextSnapshot> RequestIdToSnapshot = new ConcurrentDictionary<string, ITextSnapshot>();
+
+ public static bool Verify(Dafny.Program dafnyProgram, ITextSnapshot snapshot, ErrorReporterDelegate er) {
Dafny.Translator translator = new Dafny.Translator();
translator.InsertChecksums = true;
Bpl.Program boogieProgram = translator.Translate(dafnyProgram);
- PipelineOutcome oc = BoogiePipeline(boogieProgram, er);
+ PipelineOutcome oc = BoogiePipeline(boogieProgram, snapshot, er);
switch (oc) {
case PipelineOutcome.Done:
case PipelineOutcome.VerificationCompleted:
@@ -170,7 +175,7 @@ namespace DafnyLanguage
/// else. Hence, any resolution errors and type checking errors are due to errors in
/// the translation.
/// </summary>
- static PipelineOutcome BoogiePipeline(Bpl.Program/*!*/ program, ErrorReporterDelegate er) {
+ static PipelineOutcome BoogiePipeline(Bpl.Program/*!*/ program, ITextSnapshot snapshot, ErrorReporterDelegate er) {
Contract.Requires(program != null);
PipelineOutcome oc = BoogieResolveAndTypecheck(program);
@@ -178,7 +183,9 @@ namespace DafnyLanguage
ExecutionEngine.EliminateDeadVariablesAndInline(program);
ExecutionEngine.errorInformationFactory = new DafnyErrorInformationFactory();
int errorCount, verified, inconclusives, timeOuts, outOfMemories;
- return ExecutionEngine.InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories, er);
+ var requestId = (RequestIdToSnapshot.Count + 1).ToString();
+ RequestIdToSnapshot[requestId] = snapshot;
+ return ExecutionEngine.InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories, er, requestId);
}
return oc;
}
diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index 0a83bcc0..4eb150f5 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -273,10 +273,16 @@ namespace DafnyLanguage
// Run the verifier
var newErrors = new List<DafnyError>();
try {
- bool success = DafnyDriver.Verify(program, errorInfo => {
- newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg));
+ bool success = DafnyDriver.Verify(program, snapshot, errorInfo =>
+ {
+ ITextSnapshot ss = null;
+ if (errorInfo.RequestId != null)
+ {
+ ss = DafnyDriver.RequestIdToSnapshot[errorInfo.RequestId];
+ }
+ newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg, ss));
foreach (var aux in errorInfo.Aux) {
- newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg));
+ newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg, ss));
}
});
if (!success) {
diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index 4f8fa694..c7eba4c0 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -217,7 +217,10 @@ namespace DafnyLanguage
public void PopulateErrorList(List<DafnyError> newErrors, bool verificationErrors, ITextSnapshot snapshot) {
Contract.Requires(newErrors != null);
foreach (var err in newErrors) {
- err.FillInSnapshot(snapshot);
+ if (err.Snapshot == null)
+ {
+ err.FillInSnapshot(snapshot);
+ }
}
if (verificationErrors) {
_verificationErrors = newErrors;
@@ -228,12 +231,16 @@ namespace DafnyLanguage
_errorProvider.SuspendRefresh(); // reduce flickering
_errorProvider.Tasks.Clear();
foreach (var err in AllErrors()) {
+ var l = err.Snapshot.GetLineFromLineNumber(err.Line);
+ var c = l.Start.Add(err.Column);
+ c = c.TranslateTo(_buffer.CurrentSnapshot, PointTrackingMode.Negative);
+ l = c.GetContainingLine();
ErrorTask task = new ErrorTask() {
Category = TaskCategory.BuildCompile,
ErrorCategory = CategoryConversion(err.Category),
Text = err.Message,
- Line = err.Line,
- Column = err.Column
+ Line = l.LineNumber,
+ Column = l.Start.Difference(c)
};
if (_document != null) {
task.Document = _document.FilePath;
@@ -324,19 +331,20 @@ namespace DafnyLanguage
{
public readonly int Line; // 0 based
public readonly int Column; // 0 based
- ITextSnapshot Snapshot; // filled in during the FillInSnapshot call
+ public ITextSnapshot Snapshot; // filled in during the FillInSnapshot call
public readonly ErrorCategory Category;
public readonly string Message;
/// <summary>
/// "line" and "col" are expected to be 0-based
/// </summary>
- public DafnyError(int line, int col, ErrorCategory cat, string msg) {
+ public DafnyError(int line, int col, ErrorCategory cat, string msg, ITextSnapshot snapshot = null) {
Contract.Requires(0 <= line);
Contract.Requires(0 <= col);
Line = line;
Column = col;
Category = cat;
Message = msg;
+ Snapshot = snapshot;
}
public void FillInSnapshot(ITextSnapshot snapshot) {