From 7a9c9cfb6bf69f2ed8c5c8d8ad0e7780266338d8 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Thu, 20 Jun 2013 17:50:13 -0700 Subject: DafnyExtension: Made it display verification errors incrementally. --- Source/DafnyExtension/ResolverTagger.cs | 160 ++++++++++++++++++++++---------- 1 file changed, 113 insertions(+), 47 deletions(-) (limited to 'Source/DafnyExtension/ResolverTagger.cs') diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs index 349bc09f..54e29070 100644 --- a/Source/DafnyExtension/ResolverTagger.cs +++ b/Source/DafnyExtension/ResolverTagger.cs @@ -38,7 +38,8 @@ namespace DafnyLanguage [Import] ITextDocumentFactoryService _textDocumentFactory = null; - public ITagger CreateTagger(ITextBuffer buffer) where T : ITag { + public ITagger CreateTagger(ITextBuffer buffer) where T : ITag + { // create a single tagger for each buffer. Func> sc = delegate() { return new ResolverTagger(buffer, _serviceProvider, _textDocumentFactory) as ITagger; }; return buffer.Properties.GetOrCreateSingletonProperty>(sc); @@ -60,7 +61,8 @@ namespace DafnyLanguage { public readonly string Typ; public readonly string Msg; - public DafnyErrorResolverTag(string typ, string msg) { + public DafnyErrorResolverTag(string typ, string msg) + { Typ = typ; Msg = msg; } @@ -69,7 +71,8 @@ namespace DafnyLanguage public class DafnySuccessResolverTag : DafnyResolverTag { public readonly Dafny.Program Program; - public DafnySuccessResolverTag(Dafny.Program program) { + public DafnySuccessResolverTag(Dafny.Program program) + { Program = program; } } @@ -86,24 +89,66 @@ namespace DafnyLanguage readonly ITextDocument _document; readonly 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 - public Dafny.Program _program; // non-null only if the snapshot contains a Dafny program that type checks + // The 'Snapshot' and 'Program' fields should be updated and read together, so they are protected by "this" + public ITextSnapshot Snapshot; // may be null + public Dafny.Program Program; // non-null only if the snapshot contains a Dafny program that type checks List _resolutionErrors = new List(); // if nonempty, then _snapshot is the snapshot from which the errors were produced - List _verificationErrors = new List(); - public List VerificationErrors + internal void AddError(DafnyError error, string unitId, string requestId) { - get + ErrorContainer entry; + if (_verificationErrors.TryGetValue(unitId, out entry)) { - return _verificationErrors; + lock (entry) + { + if (entry.RequestId == null || new DateTime(long.Parse(entry.RequestId)) < new DateTime(long.Parse(requestId))) + { + entry.Errors.Clear(); + entry.RequestId = requestId; + } + } + entry.Errors.Push(error); } - set + } + + string MostRecentRequestId; + + internal void ReInitializeVerificationErrors(string mostRecentRequestId, List units) + { + var implNames = units.OfType().Select(impl => impl.Name); + lock (this) { - Contract.Requires(value != null); + MostRecentRequestId = mostRecentRequestId; + var outOfDatekeys = _verificationErrors.Keys.Except(implNames); + foreach (var key in outOfDatekeys) + { + ErrorContainer oldError; + _verificationErrors.TryRemove(key, out oldError); + } - _verificationErrors = value; + var newKeys = implNames.Except(_verificationErrors.Keys).ToList(); + newKeys.Add("$$program$$"); + foreach (var key in newKeys) + { + _verificationErrors.TryAdd(key, new ErrorContainer()); + } + } + } + + public class ErrorContainer + { + internal string RequestId; + internal ConcurrentStack Errors = new ConcurrentStack(); + } + + public readonly ConcurrentDictionary _verificationErrors = new ConcurrentDictionary(); + + public IEnumerable VerificationErrors + { + get + { + return _verificationErrors.Values.Where(ec => ec.RequestId == MostRecentRequestId).SelectMany(ec => ec.Errors); } } @@ -127,11 +172,12 @@ namespace DafnyLanguage public static readonly IDictionary Programs = new ConcurrentDictionary(); - internal ResolverTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITextDocumentFactoryService textDocumentFactory) { + internal ResolverTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITextDocumentFactoryService textDocumentFactory) + { _buffer = buffer; if (!textDocumentFactory.TryGetTextDocument(_buffer, out _document)) _document = null; - _snapshot = null; // this makes sure the next snapshot will look different + Snapshot = null; // this makes sure the next snapshot will look different _errorProvider = new ErrorListProvider(serviceProvider); BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, ResolveBuffer); @@ -171,14 +217,18 @@ namespace DafnyLanguage /// /// Find the Error tokens in the set of all tokens and create an ErrorTag for each /// - public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { + public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) + { if (spans.Count == 0) yield break; var currentSnapshot = spans[0].Snapshot; - foreach (var err in AllErrors) { - if (err.Category != ErrorCategory.ProcessError) { + foreach (var err in AllErrors) + { + if (err.Category != ErrorCategory.ProcessError) + { var span = err.Span.TranslateTo(currentSnapshot, SpanTrackingMode.EdgeExclusive); string ty; // the COLORs below indicate what I see on my machine - switch (err.Category) { + switch (err.Category) + { default: // unexpected category case ErrorCategory.ParseError: case ErrorCategory.ParseWarning: @@ -198,11 +248,13 @@ namespace DafnyLanguage ITextSnapshot snap; Dafny.Program prog; - lock (this) { - snap = _snapshot; - prog = _program; + lock (this) + { + snap = Snapshot; + prog = Program; } - if (prog != null) { + if (prog != null) + { yield return new TagSpan(new SnapshotSpan(snap, 0, snap.Length), new DafnySuccessResolverTag(prog)); } } @@ -213,25 +265,30 @@ namespace DafnyLanguage /// /// Calls the Dafny parser/resolver/type checker on the contents of the buffer, updates the Error List accordingly. /// - void ResolveBuffer(object sender, EventArgs args) { + void ResolveBuffer(object sender, EventArgs args) + { ITextSnapshot snapshot = _buffer.CurrentSnapshot; - if (snapshot == _snapshot) + if (snapshot == Snapshot) return; // we've already done this snapshot var driver = new DafnyDriver(snapshot, _document != null ? _document.FilePath : ""); List newErrors; Dafny.Program program; - try { + try + { program = driver.ProcessResolution(); newErrors = driver.Errors; - } catch (Exception e) { + } + catch (Exception e) + { newErrors = new List { new DafnyError(0, 0, ErrorCategory.InternalError, "internal Dafny error: " + e.Message, snapshot) }; program = null; } - lock (this) { - _snapshot = snapshot; - _program = program; + lock (this) + { + Snapshot = snapshot; + Program = program; } if (program != null && _document != null) @@ -244,28 +301,34 @@ namespace DafnyLanguage } _resolutionErrors = newErrors; + UpdateErrorList(snapshot); } - public void UpdateErrorList(ITextSnapshot snapshot) { + public void UpdateErrorList(ITextSnapshot snapshot) + { _errorProvider.SuspendRefresh(); // reduce flickering _errorProvider.Tasks.Clear(); - foreach (var err in AllErrors) { - var span = err.Span.TranslateTo(snapshot, SpanTrackingMode.EdgeExclusive); + foreach (var err in AllErrors) + { + var span = err.Span.TranslateTo(snapshot, SpanTrackingMode.EdgeInclusive); var lineNum = snapshot.GetLineNumberFromPosition(span.Start.Position); var line = snapshot.GetLineFromPosition(span.Start.Position); var columnNum = span.Start - line.Start; - ErrorTask task = new ErrorTask() { + ErrorTask task = new ErrorTask() + { Category = TaskCategory.BuildCompile, ErrorCategory = CategoryConversion(err.Category), Text = err.Message, Line = lineNum, Column = columnNum }; - if (_document != null) { + if (_document != null) + { task.Document = _document.FilePath; } - if (err.Category != ErrorCategory.ProcessError && err.Category != ErrorCategory.InternalError) { + if (err.Category != ErrorCategory.ProcessError && err.Category != ErrorCategory.InternalError) + { task.Navigate += new EventHandler(NavigateHandler); } _errorProvider.Tasks.Add(task); @@ -276,8 +339,10 @@ namespace DafnyLanguage chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length))); } - static TaskErrorCategory CategoryConversion(ErrorCategory cat) { - switch (cat) { + static TaskErrorCategory CategoryConversion(ErrorCategory cat) + { + switch (cat) + { case ErrorCategory.ParseError: case ErrorCategory.ResolveError: case ErrorCategory.VerificationError: @@ -293,7 +358,8 @@ namespace DafnyLanguage } } - void NavigateHandler(object sender, EventArgs arguments) { + void NavigateHandler(object sender, EventArgs arguments) + { var task = sender as ErrorTask; if (task == null || task.Document == null) return; @@ -321,9 +387,11 @@ namespace DafnyLanguage // Get the VsTextBuffer VsTextBuffer buffer = docData as VsTextBuffer; - if (buffer == null) { + if (buffer == null) + { IVsTextBufferProvider bufferProvider = docData as IVsTextBufferProvider; - if (bufferProvider != null) { + if (bufferProvider != null) + { IVsTextLines lines; Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(bufferProvider.GetTextBuffer(out lines)); buffer = lines as VsTextBuffer; @@ -339,7 +407,6 @@ namespace DafnyLanguage // Finally, move the cursor Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(textManager.NavigateToLineAndColumn(buffer, ref logicalView, task.Line, task.Column, task.Line, task.Column)); } - } @@ -361,11 +428,10 @@ namespace DafnyLanguage /// /// "line" and "col" are expected to be 0-based /// - public DafnyError(int line, int col, ErrorCategory cat, string msg, ITextSnapshot snapshot) { - Contract.Requires(0 <= line); - Contract.Requires(0 <= col); - Line = line; - Column = col; + public DafnyError(int line, int col, ErrorCategory cat, string msg, ITextSnapshot snapshot) + { + Line = Math.Max(0, line); + Column = Math.Max(0, col); Category = cat; Message = msg; Snapshot = snapshot; -- cgit v1.2.3