From a6cf67873c2fce7bfe07e8ff57ee6b279ffbbb2c Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 8 Aug 2012 18:42:57 -0700 Subject: Dafny: the DafnyExtension mode for Visual Studio now calls the verifier and visually indicates a non-verified buffer --- Source/Core/CommandLineOptions.cs | 4 ++-- Source/Dafny/Dafny.atg | 2 ++ Source/Dafny/DafnyOptions.cs | 2 +- Source/Dafny/Parser.cs | 2 ++ 4 files changed, 7 insertions(+), 3 deletions(-) (limited to 'Source') diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index ff1a0eb1..4e134b3c 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -254,7 +254,7 @@ namespace Microsoft.Boogie { /// /// This method is called after all parsing is done, if no parse errors were encountered. /// - protected virtual void ApplyDefaultOptions() { + public virtual void ApplyDefaultOptions() { } /// @@ -1244,7 +1244,7 @@ namespace Microsoft.Boogie { return base.ParseOption(name, ps); // defer to superclass } - protected override void ApplyDefaultOptions() { + public override void ApplyDefaultOptions() { Contract.Ensures(TheProverFactory != null); Contract.Ensures(vcVariety != VCVariety.Unspecified); diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index ce0ccf16..ebf01c4c 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1031,6 +1031,8 @@ WhileStmt stmt = new WhileStmt(x, guard, invariants, new Specification(decreases, decAttrs), new Specification(null, null), body); stmt = new SkeletonStatement(stmt, guardOmitted, bodyOmitted); } else { + // The following statement protects against crashes in case of parsing errors + body = body ?? new BlockStmt(x, new List()); stmt = new WhileStmt(x, guard, invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), body); } .) diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 34fa0487..d5057017 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -97,7 +97,7 @@ namespace Microsoft.Dafny return base.ParseOption(name, ps); } - protected override void ApplyDefaultOptions() { + public override void ApplyDefaultOptions() { base.ApplyDefaultOptions(); // expand macros in filenames, now that LogPrefix is fully determined diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index a7de690e..d01fe161 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -1515,6 +1515,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo stmt = new WhileStmt(x, guard, invariants, new Specification(decreases, decAttrs), new Specification(null, null), body); stmt = new SkeletonStatement(stmt, guardOmitted, bodyOmitted); } else { + // The following statement protects against crashes in case of parsing errors + body = body ?? new BlockStmt(x, new List()); stmt = new WhileStmt(x, guard, invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), body); } -- cgit v1.2.3 From cd6ffa2c7166a5ddb2052cade723de11daf0452a Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 8 Aug 2012 22:46:20 -0700 Subject: DafnyExtension: improvements --- Source/Dafny/DafnyAst.cs | 2 +- .../DafnyExtension/DafnyExtension.csproj | 1 - .../DafnyExtension/DafnyExtension/Outlining.cs | 222 --------------------- .../DafnyExtension/OutliningTagger.cs | 2 +- .../DafnyExtension/ResolverTagger.cs | 23 ++- 5 files changed, 18 insertions(+), 232 deletions(-) delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/Outlining.cs (limited to 'Source') diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 8ea17a52..98319473 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -20,7 +20,7 @@ namespace Microsoft.Dafny { public readonly string Name; public List/*!*/ Modules; // filled in during resolution. - // Resolution essentially flattens the module heirarchy, for + // Resolution essentially flattens the module hierarchy, for // purposes of translation and compilation. public List CompileModules; // filled in during resolution. // Contains the definitions to be used for compilation. diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj index 62413d03..cfa7a070 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj +++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj @@ -135,7 +135,6 @@ - diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/Outlining.cs b/Util/VS2010/DafnyExtension/DafnyExtension/Outlining.cs deleted file mode 100644 index 3e64e43d..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/Outlining.cs +++ /dev/null @@ -1,222 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using System.Text.RegularExpressions; -using System.Windows.Threading; -using System.ComponentModel.Composition; -using Microsoft.VisualStudio.Text.Outlining; -using Microsoft.VisualStudio.Text.Tagging; -using Microsoft.VisualStudio.Utilities; -using Microsoft.VisualStudio.Text; - -namespace DafnyLanguage -{ -#if THIS_IS_THE_PAST - [Export(typeof(ITaggerProvider))] - [ContentType("dafny")] - [TagType(typeof(IOutliningRegionTag))] - internal sealed class OutliningTaggerProvider : ITaggerProvider - { - public ITagger CreateTagger(ITextBuffer buffer) where T : ITag { - // create a single tagger for each buffer. - Func> sc = delegate() { return new OutlineTagger(buffer) as ITagger; }; - return buffer.Properties.GetOrCreateSingletonProperty>(sc); - } - } - - /// - /// Data about one outline region - /// - internal class OutlineRegion - { - public SnapshotPoint Start { get; set; } - public SnapshotPoint End { get; set; } - public SnapshotSpan Span { - get { return new SnapshotSpan(Start, End); } - } - - public string HoverText { get; set; } - public string Label { get; set; } - } - - internal sealed class OutlineTagger : ITagger - { - ITextBuffer _buffer; - ITextSnapshot _snapshot; - List _regions; - - public OutlineTagger(ITextBuffer buffer) { - _buffer = buffer; - _snapshot = buffer.CurrentSnapshot; - _regions = new List(); - - ReparseFile(null, EventArgs.Empty); - - // listen for changes to the buffer, but don't process until the user stops typing - BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, ReparseFile); - } - - public void Dispose() { - BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ReparseFile); - } - - public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { - if (spans.Count == 0) - yield break; - - List currentRegions = _regions; - ITextSnapshot currentSnapshot = _snapshot; - - // create a new SnapshotSpan for the entire region encompassed by the span collection - SnapshotSpan entire = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End).TranslateTo(currentSnapshot, SpanTrackingMode.EdgeExclusive); - int startLineNumber = entire.Start.GetContainingLine().LineNumber; - int endLineNumber = entire.End.GetContainingLine().LineNumber; - - // return outline tags for any regions that fall within that span - foreach (var region in currentRegions) { - if (entire.IntersectsWith(region.Span)) { - //the region starts at the beginning of the "{", and goes until the *end* of the line that contains the "}". - yield return new TagSpan(new SnapshotSpan(region.Start, region.End), - new OutliningRegionTag(false, false, region.Label, region.HoverText)); - } - } - } - - public event EventHandler TagsChanged; - - static string ellipsis = "..."; //the characters that are displayed when the region is collapsed - static Regex matchKey = new Regex("^\\s*(datatype|method|function)"); - static int MaxHiddenLines = 15; - static char[] eitherBrace = { '{', '}' }; - - /// - /// Find all of the outline sections in the snapshot - /// - private List ParseOutlineSections(ITextSnapshot newSnapshot) { - List newRegions = new List(); - - // We care about three states: - // (0) looking for an outlineable declaration - // (1) have found an outlineable declaration, looking for an open curly - // (2) looking for a close curly - // The search used here is not at all exact, and it would be easy to get it to - // do the wrong thing; however, in common cases, it will do the right thing. - int state = 0; - SnapshotPoint start = new SnapshotPoint(); // the value of "start" matters only if state==2 - int braceImbalance = 0; // used only if state==2 - string hoverText = ""; // used only if state==2 - int hoverLineCount = 0; // used only if state==2 - string prevLineBreak = ""; // used only if state==2 - foreach (ITextSnapshotLine line in newSnapshot.Lines) { - string txt = line.GetText(); - if (state == 0) { - MatchCollection matches = matchKey.Matches(txt); - if (matches.Count != 0) - state = 1; - } - int startPos = 0; - if (state == 1) { - startPos = txt.IndexOf('{'); - if (startPos != -1) { - start = new SnapshotPoint(newSnapshot, line.Start.Position + startPos + 1); - startPos++; - state = 2; - braceImbalance = 1; - hoverText = txt.Substring(startPos).Trim(); - hoverLineCount = hoverText.Length == 0 ? 0 : 1; - prevLineBreak = line.GetLineBreakText(); - } - } - if (state == 2) { - int endPos = startPos; - while (braceImbalance != 0) { - endPos = txt.IndexOfAny(eitherBrace, endPos); - if (endPos == -1) break; - char ch = txt[endPos]; - if (ch == '{') { - braceImbalance++; - } else { - braceImbalance--; - if (braceImbalance == 0) break; - } - endPos++; - } - - if (endPos == -1) { - // not there yet - if (startPos == 0 && hoverLineCount < MaxHiddenLines) { - string h = txt.Trim(); - if (h.Length != 0) { - if (hoverText.Length != 0) - hoverText += prevLineBreak; - hoverText += h; - hoverLineCount++; - prevLineBreak = line.GetLineBreakText(); - } - } - } else { - // we found the end - if (startPos != 0) { - hoverText = txt.Substring(startPos, endPos - startPos).Trim(); - } else if (hoverLineCount < MaxHiddenLines) { - string h = txt.Substring(0, endPos).Trim(); - if (h.Length != 0) { - if (hoverText.Length != 0) - hoverText += prevLineBreak; - hoverText += h; - } - } - SnapshotPoint end = new SnapshotPoint(newSnapshot, line.Start.Position + endPos); - newRegions.Add(new OutlineRegion() { - Start = start, End = end, Label = ellipsis, - HoverText = hoverText - }); - state = 0; - } - } - } - - return newRegions; - } - - /// - /// Find all of the outline regions in the document (snapshot) and notify - /// listeners of any that changed - /// - void ReparseFile(object sender, EventArgs args) { - ITextSnapshot snapshot = _buffer.CurrentSnapshot; - - // get all of the outline regions in the snapshot - List newRegions = ParseOutlineSections(snapshot); - - // determine the changed span, and send a changed event with the new spans - List oldSpans = new List(_regions.Select(r => - r.Span.TranslateTo(snapshot, SpanTrackingMode.EdgeExclusive))); - - List newSpans = new List(newRegions.Select(r => r.Span)); - - NormalizedSnapshotSpanCollection oldSpanCollection = new NormalizedSnapshotSpanCollection(oldSpans); - NormalizedSnapshotSpanCollection newSpanCollection = new NormalizedSnapshotSpanCollection(newSpans); - - NormalizedSnapshotSpanCollection difference = SymmetricDifference(oldSpanCollection, newSpanCollection); - - // save the new baseline - _snapshot = snapshot; - _regions = newRegions; - - foreach (var span in difference) { - var chng = TagsChanged; - if (chng != null) - chng(this, new SnapshotSpanEventArgs(span)); - } - } - - NormalizedSnapshotSpanCollection SymmetricDifference(NormalizedSnapshotSpanCollection first, NormalizedSnapshotSpanCollection second) { - return NormalizedSnapshotSpanCollection.Union( - NormalizedSnapshotSpanCollection.Difference(first, second), - NormalizedSnapshotSpanCollection.Difference(second, first)); - } - } -#endif -} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs index 8cbdb9f6..86a53460 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs @@ -119,7 +119,7 @@ namespace DafnyLanguage newRegions.Add(new ORegion(module, "module")); } foreach (Dafny.TopLevelDecl d in module.TopLevelDecls) { - if (!HasBodyTokens(d)) { + if (!HasBodyTokens(d) && !(d is Dafny.ClassDecl)) { continue; } if (d is Dafny.ArbitraryTypeDecl) { diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs index fcc31a3c..10bb36e1 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs @@ -102,6 +102,10 @@ namespace DafnyLanguage foreach (var err in _resolutionErrors) { yield return err; } + if (_resolutionErrors.Count != 0) { + // we're done + yield break; + } foreach (var err in _verificationErrors) { yield return err; } @@ -112,14 +116,10 @@ namespace DafnyLanguage /// 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) { - Contract.Assert(0 <= err.Line); - var line = _snapshot.GetLineFromLineNumber(err.Line); - Contract.Assert(err.Column <= line.Length); - var length = line.Length - err.Column; - if (5 < length) length = 5; - var span = new SnapshotSpan(new SnapshotPoint(_snapshot, line.Start.Position + err.Column), length); + var span = err.Span().TranslateTo(currentSnapshot, SpanTrackingMode.EdgeExclusive); string ty; // the COLORs below indicate what I see on my machine switch (err.Category) { default: // unexpected category @@ -282,13 +282,15 @@ namespace DafnyLanguage { public readonly int Line; // 0 based public readonly int Column; // 0 based - public ITextSnapshot Snapshot; // filled in during the FillInSnapshot call + ITextSnapshot Snapshot; // filled in during the FillInSnapshot call public readonly ErrorCategory Category; public readonly string Message; /// /// "line" and "col" are expected to be 0-based /// public DafnyError(int line, int col, ErrorCategory cat, string msg) { + Contract.Requires(0 <= line); + Contract.Requires(0 <= col); Line = line; Column = col; Category = cat; @@ -299,5 +301,12 @@ namespace DafnyLanguage Contract.Requires(snapshot != null); Snapshot = snapshot; } + public SnapshotSpan Span() { + Contract.Requires(Snapshot != null); // requires that Snapshot has been filled in + var line = Snapshot.GetLineFromLineNumber(Line); + Contract.Assume(Column <= line.Length); // this is really a precondition of the constructor + FillInSnapshot + var length = Math.Min(line.Length - Column, 5); + return new SnapshotSpan(line.Start + Column, length); + } } } -- cgit v1.2.3