Did some refactoring of the interaction with the Boogie execution engine.

4 files changed, 41 insertions, 30 deletions

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 43aa6971..81662b5d 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -163,7 +163,8 @@ namespace Microsoft.Dafny
       Contract.Ensures(0 <= Contract.ValueAtReturn(out stats).InconclusiveCount && 0 <= Contract.ValueAtReturn(out stats).TimeoutCount);

 

       stats = new PipelineStatistics();

-      PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(program, bplFileName);

+      LinearTypechecker ltc;

+      PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(program, bplFileName, out ltc);

       switch (oc) {

         case PipelineOutcome.Done:

           return oc;

@@ -180,7 +181,7 @@ namespace Microsoft.Dafny
             fileNames.Add(bplFileName);

             Bpl.Program reparsedProgram = ExecutionEngine.ParseBoogieProgram(fileNames, true);

             if (reparsedProgram != null) {

-              ExecutionEngine.ResolveAndTypecheck(reparsedProgram, bplFileName);

+              ExecutionEngine.ResolveAndTypecheck(reparsedProgram, bplFileName, out ltc);

             }

           }

           return oc;

@@ -190,7 +191,7 @@ namespace Microsoft.Dafny
           return ExecutionEngine.InferAndVerify(program, stats);

 

         default:

-          Contract.Assert(false);throw new cce.UnreachableException();  // unexpected outcome

+          Contract.Assert(false); throw new cce.UnreachableException();  // unexpected outcome

       }

     }

 

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index b5629b96..479816a6 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -40,6 +40,7 @@ namespace DafnyLanguage
         options.ApplyDefaultOptions();

 

         ExecutionEngine.printer = new DummyPrinter();

+        ExecutionEngine.errorInformationFactory = new DafnyErrorInformationFactory();

       }

     }

 

@@ -230,8 +231,7 @@ namespace DafnyLanguage
 

       PipelineOutcome oc = BoogieResolveAndTypecheck(program);

       if (oc == PipelineOutcome.ResolvedAndTypeChecked) {

-        ExecutionEngine.EliminateDeadVariablesAndInline(program);

-        ExecutionEngine.errorInformationFactory = new DafnyErrorInformationFactory();

+        ExecutionEngine.EliminateDeadVariablesAndInline(program);        

         return ExecutionEngine.InferAndVerify(program, new PipelineStatistics(), er, requestId);

       }

       return oc;

diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index 584d57fc..8500117a 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -134,8 +134,14 @@ namespace DafnyLanguage
           {

             Microsoft.Boogie.ExecutionEngine.CancelRequest(lastRequestId);

           }

+          if (_document.FilePath != null)

+          {

+            ProgressTaggers.Remove(_document.FilePath);

+          }

           _buffer.Changed -= buffer_Changed;

+          timer.Tick -= UponIdle;

           _errorProvider.Dispose();

+          _errorProvider = null;

           ClearCachedVerificationResults();

           if (resolver != null)

           {

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index 33baf3b5..578b9ce2 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -87,7 +87,7 @@ namespace DafnyLanguage
   {

     readonly ITextBuffer _buffer;

     readonly ITextDocument _document;

-    readonly ErrorListProvider _errorProvider;

+    ErrorListProvider _errorProvider;

 

     // The 'Snapshot' and 'Program' fields should be updated and read together, so they are protected by "this"

     public ITextSnapshot Snapshot;  // may be null

@@ -207,6 +207,7 @@ namespace DafnyLanguage
               // this may occur if the SVsServiceProvider somehow has been uninstalled before our Dispose method is called

             }

             _errorProvider.Dispose();

+            _errorProvider = null;

           }

           BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ResolveBuffer);

         }

@@ -307,35 +308,38 @@ namespace DafnyLanguage
 

     public void UpdateErrorList(ITextSnapshot snapshot)

     {

-      lock (this)

+      lock (this) 

       {

-        _errorProvider.SuspendRefresh();  // reduce flickering

-        _errorProvider.Tasks.Clear();

-        foreach (var err in AllErrors)

+        if (_errorProvider != null)

         {

-          var span = err.Span.GetSpan(snapshot);

-          var lineNum = snapshot.GetLineNumberFromPosition(span.Start.Position);

-          var line = snapshot.GetLineFromPosition(span.Start.Position);

-          var columnNum = span.Start - line.Start;

-          ErrorTask task = new ErrorTask()

-          {

-            Category = TaskCategory.BuildCompile,

-            ErrorCategory = CategoryConversion(err.Category),

-            Text = err.Message,

-            Line = lineNum,

-            Column = columnNum

-          };

-          if (_document != null)

+          _errorProvider.SuspendRefresh();  // reduce flickering

+          _errorProvider.Tasks.Clear();

+          foreach (var err in AllErrors)

           {

-            task.Document = _document.FilePath;

-          }

-          if (err.Category != ErrorCategory.ProcessError && err.Category != ErrorCategory.InternalError)

-          {

-            task.Navigate += new EventHandler(NavigateHandler);

+            var span = err.Span.GetSpan(snapshot);

+            var lineNum = snapshot.GetLineNumberFromPosition(span.Start.Position);

+            var line = snapshot.GetLineFromPosition(span.Start.Position);

+            var columnNum = span.Start - line.Start;

+            ErrorTask task = new ErrorTask()

+            {

+              Category = TaskCategory.BuildCompile,

+              ErrorCategory = CategoryConversion(err.Category),

+              Text = err.Message,

+              Line = lineNum,

+              Column = columnNum

+            };

+            if (_document != null)

+            {

+              task.Document = _document.FilePath;

+            }

+            if (err.Category != ErrorCategory.ProcessError && err.Category != ErrorCategory.InternalError)

+            {

+              task.Navigate += new EventHandler(NavigateHandler);

+            }

+            _errorProvider.Tasks.Add(task);

           }

-          _errorProvider.Tasks.Add(task);

+          _errorProvider.ResumeRefresh();

         }

-        _errorProvider.ResumeRefresh();

       }

       var chng = TagsChanged;

       if (chng != null)