DafnyExtension: Worked on integrating the verification result caching.

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) {