From eaa507dad5904016694a0b019d1e2b8c6406c1c7 Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 17 Aug 2012 11:29:05 -0700 Subject: DafnyExtension: toward some fixes --- .../DafnyExtension/DafnyExtension/DafnyDriver.cs | 2 +- .../DafnyExtension/IdentifierTagger.cs | 26 +++++++----- .../DafnyExtension/OutliningTagger.cs | 28 ++++++++----- .../DafnyExtension/ProgressMargin.cs | 46 +++++++++++++--------- .../DafnyExtension/ResolverTagger.cs | 24 +++++++---- 5 files changed, 80 insertions(+), 46 deletions(-) (limited to 'Util') diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs index b7b2cd6d..79194d97 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs @@ -47,7 +47,7 @@ namespace DafnyLanguage } } - public Dafny.Program Process() { + public Dafny.Program ProcessResolution() { if (!ParseAndTypeCheck()) { return null; } diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs index db91cd92..4f414b91 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs @@ -89,16 +89,24 @@ namespace DafnyLanguage void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) { var r = sender as ResolverTagger; - if (r != null && r._program != null) { - if (!ComputeIdentifierRegions(r._program, r._snapshot)) - return; // no new regions + if (r != null) { + ITextSnapshot snap; + Microsoft.Dafny.Program prog; + lock (this) { + snap = r._snapshot; + prog = r._program; + } + if (prog != null) { + if (!ComputeIdentifierRegions(prog, snap)) + return; // no new regions - var chng = TagsChanged; - if (chng != null) { - NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot); - if (spans.Count > 0) { - SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End); - chng(this, new SnapshotSpanEventArgs(span)); + var chng = TagsChanged; + if (chng != null) { + NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot); + if (spans.Count > 0) { + SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End); + chng(this, new SnapshotSpanEventArgs(span)); + } } } } diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs index e51e9887..a47cdba7 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs @@ -91,16 +91,24 @@ namespace DafnyLanguage void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) { var r = sender as ResolverTagger; - if (r != null && r._program != null) { - if (!ComputeOutliningRegions(r._program, r._snapshot)) - return; // no new regions - - var chng = TagsChanged; - if (chng != null) { - NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot); - if (spans.Count > 0) { - SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End); - chng(this, new SnapshotSpanEventArgs(span)); + if (r != null) { + ITextSnapshot snap; + Microsoft.Dafny.Program prog; + lock (this) { + snap = r._snapshot; + prog = r._program; + } + if (prog != null) { + if (!ComputeOutliningRegions(prog, snap)) + return; // no new regions + + var chng = TagsChanged; + if (chng != null) { + NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot); + if (spans.Count > 0) { + SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End); + chng(this, new SnapshotSpanEventArgs(span)); + } } } } diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs index 34dcce3c..d8a60647 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs @@ -121,19 +121,22 @@ namespace DafnyLanguage // If r._program is null, then the current buffer contains a Dafny fragment that does not resolve. If it is non-null, // then r._program has been successfully resolved, so when things have been sufficiently idle, we're ready to verify it. resolver = r; - latestProgram = r._program; - latestSnapshot = latestProgram != null ? r._snapshot : null; + lock (r) { + latestProgram = r._program; + latestSnapshot = latestProgram != null ? r._snapshot : null; + } } } bool verificationInProgress; // this field is protected by "this" + bool verificationRequested; // this field is protected by "this". Invariant: verificationRequested ==> verificationInProgress public void DoTheVerification(object sender, EventArgs args) { var buffer = sender as ITextBuffer; if (buffer != null && latestProgram != null && resolver != null) { bool tagsChanged = false; lock (this) { if (verificationInProgress) { - // take no further action + verificationRequested = true; return; } verificationInProgress = true; @@ -185,25 +188,30 @@ namespace DafnyLanguage } public void Start() { - var newErrors = new List(); - bool success = DafnyDriver.Verify(program, errorInfo => { - newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg)); - foreach (var aux in errorInfo.Aux) { - newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg)); + bool verifySomeMore = true; + while (verifySomeMore) { + var newErrors = new List(); + bool success = DafnyDriver.Verify(program, errorInfo => { + newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg)); + foreach (var aux in errorInfo.Aux) { + newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg)); + } + }); + + lock (pt) { + verifySomeMore = pt.verificationRequested; + pt.verificationInProgress = verifySomeMore; + pt.verificationRequested = false; + if (pt.bufferChangesPreVerificationStart.Count != 0) { + pt.bufferChangesPreVerificationStart = new List(); + } + resolver.PopulateErrorList(newErrors, true, snapshot); // TODO: is this appropriate to do inside the monitor? } - }); - lock (pt) { - pt.verificationInProgress = false; - if (pt.bufferChangesPreVerificationStart.Count != 0) { - pt.bufferChangesPreVerificationStart = new List(); + var chng = pt.TagsChanged; + if (chng != null) { + chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length))); } - resolver.PopulateErrorList(newErrors, true, snapshot); // TODO: is this appropriate to do inside the monitor? - } - - var chng = pt.TagsChanged; - if (chng != null) { - chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length))); } } } diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs index 2017cfaa..398629ab 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs @@ -70,11 +70,12 @@ namespace DafnyLanguage { ITextBuffer _buffer; ITextDocument _document; + // 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(); ErrorListProvider _errorProvider; - public Dafny.Program _program; // non-null only if the snapshot contains a Dafny program that type checks internal ResolverTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITextDocumentFactoryService textDocumentFactory) { _buffer = buffer; @@ -138,15 +139,22 @@ namespace DafnyLanguage yield return new TagSpan(span, new DafnyErrorResolverTag(ty, err.Message)); } } - if (_program != null) { - yield return new TagSpan(new SnapshotSpan(_snapshot, 0, _snapshot.Length), new DafnySuccessResolverTag(_program)); + + ITextSnapshot snap; + Dafny.Program prog; + lock (this) { + snap = _snapshot; + prog = _program; + } + if (prog != null) { + yield return new TagSpan(new SnapshotSpan(snap, 0, snap.Length), new DafnySuccessResolverTag(prog)); } } public event EventHandler TagsChanged; /// - /// Calls the Dafny verifier on the program, updates the Error List accordingly. + /// Calls the Dafny parser/resolver/type checker on the program, updates the Error List accordingly. /// void ProcessFile(object sender, EventArgs args) { ITextSnapshot snapshot = _buffer.CurrentSnapshot; @@ -158,7 +166,7 @@ namespace DafnyLanguage List newErrors; Dafny.Program program; try { - program = driver.Process(); + program = driver.ProcessResolution(); newErrors = driver.Errors; } catch (Exception e) { newErrors = new List(); @@ -166,8 +174,10 @@ namespace DafnyLanguage program = null; } - _snapshot = snapshot; - _program = program; + lock (this) { + _snapshot = snapshot; + _program = program; + } PopulateErrorList(newErrors, false, snapshot); } -- cgit v1.2.3