From c5a1c58d3c89c55c31331cb419cd3c06e276b5dd Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 2 Oct 2015 14:46:50 -0700 Subject: Fixed latent crash of hovertext/outlining with include. (This also undoes two previous attempted fixes, which had accidentally disabled some outlining and hovertexts.) --- Source/DafnyExtension/IdentifierTagger.cs | 146 +++++++++++++++++------------- Source/DafnyExtension/OutliningTagger.cs | 30 +++--- 2 files changed, 103 insertions(+), 73 deletions(-) (limited to 'Source/DafnyExtension') diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs index d638cb6c..51f837f7 100644 --- a/Source/DafnyExtension/IdentifierTagger.cs +++ b/Source/DafnyExtension/IdentifierTagger.cs @@ -77,7 +77,7 @@ namespace DafnyLanguage int start = entire.Start; int end = entire.End; foreach (var r in _regions) { - if (0 <= r.Length && r.Start >= start && r.Start + r.Length <= end) { + if (0 <= r.Length && r.Start <= end && start <= r.Start + r.Length) { DafnyTokenKind kind; switch (r.Kind) { case IdRegion.OccurrenceKind.Use: @@ -136,7 +136,7 @@ namespace DafnyLanguage List newRegions = new List(); foreach (var info in program.reporter.AllMessages[ErrorLevel.Info]) { - IdRegion.Add(newRegions, info.token, info.message, info.token.val.Length); + IdRegion.Add(newRegions, program, info.token, info.message, info.token.val.Length); } foreach (var module in program.Modules) { @@ -149,29 +149,29 @@ namespace DafnyLanguage foreach (var ctor in dt.Ctors) { foreach (var dtor in ctor.Destructors) { if (dtor.CorrespondingFormal.HasName) { - IdRegion.Add(newRegions, dtor.tok, dtor, null, "destructor", true, module); + IdRegion.Add(newRegions, program, dtor.tok, dtor, null, "destructor", true, module); } } } } else if (d is IteratorDecl) { var iter = (IteratorDecl)d; foreach (var p in iter.Ins) { - IdRegion.Add(newRegions, p.tok, p, true, module); + IdRegion.Add(newRegions, program, p.tok, p, true, module); } foreach (var p in iter.Outs) { - IdRegion.Add(newRegions, p.tok, p, true, "yield-parameter", module); + IdRegion.Add(newRegions, program, p.tok, p, true, "yield-parameter", module); } - iter.Reads.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, module)); - iter.Modifies.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, module)); - iter.Requires.ForEach(e => ExprRegions(e.E, newRegions, module)); - iter.YieldRequires.ForEach(e => ExprRegions(e.E, newRegions, module)); - iter.YieldEnsures.ForEach(e => ExprRegions(e.E, newRegions, module)); - iter.Ensures.ForEach(e => ExprRegions(e.E, newRegions, module)); + iter.Reads.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, program, module)); + iter.Modifies.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, program, module)); + iter.Requires.ForEach(e => ExprRegions(e.E, newRegions, program, module)); + iter.YieldRequires.ForEach(e => ExprRegions(e.E, newRegions, program, module)); + iter.YieldEnsures.ForEach(e => ExprRegions(e.E, newRegions, program, module)); + iter.Ensures.ForEach(e => ExprRegions(e.E, newRegions, program, module)); if (!((ICallable)iter).InferredDecreases) { - iter.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, module)); + iter.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, program, module)); } if (iter.Body != null) { - StatementRegions(iter.Body, newRegions, module); + StatementRegions(iter.Body, newRegions, program, module); } } else if (d is ClassDecl) { @@ -182,42 +182,42 @@ namespace DafnyLanguage } else if (member is Function) { var f = (Function)member; foreach (var p in f.Formals) { - IdRegion.Add(newRegions, p.tok, p, true, module); + IdRegion.Add(newRegions, program, p.tok, p, true, module); } - f.Req.ForEach(e => ExprRegions(e, newRegions, module)); - f.Reads.ForEach(fe => FrameExprRegions(fe, newRegions, true, module)); - f.Ens.ForEach(e => ExprRegions(e, newRegions, module)); - f.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, module)); + f.Req.ForEach(e => ExprRegions(e, newRegions, program, module)); + f.Reads.ForEach(fe => FrameExprRegions(fe, newRegions, true, program, module)); + f.Ens.ForEach(e => ExprRegions(e, newRegions, program, module)); + f.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, program, module)); if (f.Body != null) { - ExprRegions(f.Body, newRegions, module); + ExprRegions(f.Body, newRegions, program, module); } } else if (member is Method) { var m = (Method)member; foreach (var p in m.Ins) { - IdRegion.Add(newRegions, p.tok, p, true, module); + IdRegion.Add(newRegions, program, p.tok, p, true, module); } foreach (var p in m.Outs) { - IdRegion.Add(newRegions, p.tok, p, true, module); + IdRegion.Add(newRegions, program, p.tok, p, true, module); } - m.Req.ForEach(e => ExprRegions(e.E, newRegions, module)); - m.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, module)); - m.Ens.ForEach(e => ExprRegions(e.E, newRegions, module)); - m.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, module)); + m.Req.ForEach(e => ExprRegions(e.E, newRegions, program, module)); + m.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, program, module)); + m.Ens.ForEach(e => ExprRegions(e.E, newRegions, program, module)); + m.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, program, module)); if (m.Body != null) { - StatementRegions(m.Body, newRegions, module); + StatementRegions(m.Body, newRegions, program, module); } } else if (member is SpecialField) { // do nothing } else if (member is Field) { var fld = (Field)member; - IdRegion.Add(newRegions, fld.tok, fld, null, "field", true, module); + IdRegion.Add(newRegions, program, fld.tok, fld, null, "field", true, module); } } } else if (d is NewtypeDecl) { var dd = (NewtypeDecl)d; if (dd.Var != null) { - IdRegion.Add(newRegions, dd.Var.tok, dd.Var, true, module); - ExprRegions(dd.Constraint, newRegions, module); + IdRegion.Add(newRegions, program, dd.Var.tok, dd.Var, true, module); + ExprRegions(dd.Constraint, newRegions, program, module); } } } @@ -228,54 +228,56 @@ namespace DafnyLanguage return true; } - static void FrameExprRegions(FrameExpression fe, List regions, bool descendIntoExpressions, ModuleDefinition module) { + static void FrameExprRegions(FrameExpression fe, List regions, bool descendIntoExpressions, Microsoft.Dafny.Program prog, ModuleDefinition module) { Contract.Requires(fe != null); Contract.Requires(regions != null); + Contract.Requires(prog != null); if (descendIntoExpressions) { - ExprRegions(fe.E, regions, module); + ExprRegions(fe.E, regions, prog, module); } if (fe.Field != null) { Microsoft.Dafny.Type showType = null; // TODO: if we had the instantiated type of this field, that would have been nice to use here (but the Resolver currently does not compute or store the instantiated type for a FrameExpression) - IdRegion.Add(regions, fe.tok, fe.Field, showType, "field", false, module); + IdRegion.Add(regions, prog, fe.tok, fe.Field, showType, "field", false, module); } } - static void ExprRegions(Microsoft.Dafny.Expression expr, List regions, ModuleDefinition module) { + static void ExprRegions(Microsoft.Dafny.Expression expr, List regions, Microsoft.Dafny.Program prog, ModuleDefinition module) { Contract.Requires(expr != null); Contract.Requires(regions != null); + Contract.Requires(prog != null); if (expr is AutoGeneratedExpression) { // do nothing return; } else if (expr is IdentifierExpr) { var e = (IdentifierExpr)expr; - IdRegion.Add(regions, e.tok, e.Var, false, module); + IdRegion.Add(regions, prog, e.tok, e.Var, false, module); } else if (expr is MemberSelectExpr) { var e = (MemberSelectExpr)expr; var field = e.Member as Field; if (field != null) { - IdRegion.Add(regions, e.tok, field, e.Type, "field", false, module); + IdRegion.Add(regions, prog, e.tok, field, e.Type, "field", false, module); } } else if (expr is LetExpr) { var e = (LetExpr)expr; foreach (var bv in e.BoundVars) { - IdRegion.Add(regions, bv.tok, bv, true, module); + IdRegion.Add(regions, prog, bv.tok, bv, true, module); } } else if (expr is ComprehensionExpr) { var e = (ComprehensionExpr)expr; foreach (var bv in e.BoundVars) { - IdRegion.Add(regions, bv.tok, bv, true, module); + IdRegion.Add(regions, prog, bv.tok, bv, true, module); } } else if (expr is MatchExpr) { var e = (MatchExpr)expr; foreach (var kase in e.Cases) { kase.Arguments.ForEach(bv => { - IdRegion.Add(regions, bv.tok, bv, true, module); + IdRegion.Add(regions, prog, bv.tok, bv, true, module); // if the arguments is an encapsulation of different boundvars from nested match cases, // add the boundvars so that they can show up in the IDE correctly if (bv.tok is MatchCaseToken) { MatchCaseToken mt = (MatchCaseToken)bv.tok; foreach(Tuple entry in mt.varList) { - IdRegion.Add(regions, entry.Item1, entry.Item2, entry.Item3, module); + IdRegion.Add(regions, prog, entry.Item1, entry.Item2, entry.Item3, module); } } }); @@ -283,22 +285,23 @@ namespace DafnyLanguage } else if (expr is ChainingExpression) { var e = (ChainingExpression)expr; // Do the subexpressions only once (that is, avoid the duplication that occurs in the desugared form of the ChainingExpression) - e.Operands.ForEach(ee => ExprRegions(ee, regions, module)); + e.Operands.ForEach(ee => ExprRegions(ee, regions, prog, module)); return; // return here, so as to avoid doing the subexpressions below } foreach (var ee in expr.SubExpressions) { - ExprRegions(ee, regions, module); + ExprRegions(ee, regions, prog, module); } } - static void StatementRegions(Statement stmt, List regions, ModuleDefinition module) { + static void StatementRegions(Statement stmt, List regions, Microsoft.Dafny.Program prog, ModuleDefinition module) { Contract.Requires(stmt != null); Contract.Requires(regions != null); + Contract.Requires(prog != null); if (stmt is VarDeclStmt) { var s = (VarDeclStmt)stmt; // Add the variables here, once, and then go directly to the RHS's (without letting the sub-statements re-do the LHS's) foreach (var local in s.Locals) { - IdRegion.Add(regions, local.Tok, local, true, module); + IdRegion.Add(regions, prog, local.Tok, local, true, module); } if (s.Update == null) { // the VarDeclStmt has no associated assignment @@ -306,29 +309,29 @@ namespace DafnyLanguage var upd = (UpdateStmt)s.Update; foreach (var rhs in upd.Rhss) { foreach (var ee in rhs.SubExpressions) { - ExprRegions(ee, regions, module); + ExprRegions(ee, regions, prog, module); } } } else { var upd = (AssignSuchThatStmt)s.Update; - ExprRegions(upd.Expr, regions, module); + ExprRegions(upd.Expr, regions, prog, module); } // we're done, so don't do the sub-statements/expressions again return; } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; - s.BoundVars.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module)); + s.BoundVars.ForEach(bv => IdRegion.Add(regions, prog, bv.tok, bv, true, module)); } else if (stmt is MatchStmt) { var s = (MatchStmt)stmt; foreach (var kase in s.Cases) { kase.Arguments.ForEach(bv => { - IdRegion.Add(regions, bv.tok, bv, true, module); + IdRegion.Add(regions, prog, bv.tok, bv, true, module); // if the arguments is an encapsulation of different boundvars from nested match cases, // add the boundvars so that they can show up in the IDE correctly if (bv.tok is MatchCaseToken) { MatchCaseToken mt = (MatchCaseToken)bv.tok; foreach (Tuple entry in mt.varList) { - IdRegion.Add(regions, entry.Item1, entry.Item2, entry.Item3, module); + IdRegion.Add(regions, prog, entry.Item1, entry.Item2, entry.Item3, module); } } }); @@ -336,28 +339,28 @@ namespace DafnyLanguage } else if (stmt is LoopStmt) { var s = (LoopStmt)stmt; if (s.Mod.Expressions != null) { - s.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, regions, false, module)); + s.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, regions, false, prog, module)); } } else if (stmt is CalcStmt) { var s = (CalcStmt)stmt; // skip the last line, which is just a duplicate anyway for (int i = 0; i < s.Lines.Count - 1; i++) { - ExprRegions(s.Lines[i], regions, module); + ExprRegions(s.Lines[i], regions, prog, module); } foreach (var ss in stmt.SubStatements) { - StatementRegions(ss, regions, module); + StatementRegions(ss, regions, prog, module); } return; } foreach (var ee in stmt.SubExpressions) { - ExprRegions(ee, regions, module); + ExprRegions(ee, regions, prog, module); } foreach (var ss in stmt.SubStatements) { - StatementRegions(ss, regions, module); + StatementRegions(ss, regions, prog, module); } } - class IdRegion + class IdRegion : DafnyRegion { public readonly int Start; public readonly int Length; @@ -366,31 +369,41 @@ namespace DafnyLanguage public readonly OccurrenceKind Kind; public readonly IVariable Variable; - public static void Add(List regions, Bpl.IToken tok, IVariable v, bool isDefinition, ModuleDefinition context) { + public static void Add(List regions, Microsoft.Dafny.Program prog, Bpl.IToken tok, IVariable v, bool isDefinition, ModuleDefinition context) { Contract.Requires(regions != null); + Contract.Requires(prog != null); Contract.Requires(tok != null); Contract.Requires(v != null); - Add(regions, tok, v, isDefinition, null, context); + Add(regions, prog, tok, v, isDefinition, null, context); } - public static void Add(List regions, Bpl.IToken tok, IVariable v, bool isDefinition, string kind, ModuleDefinition context) { + public static void Add(List regions, Microsoft.Dafny.Program prog, Bpl.IToken tok, IVariable v, bool isDefinition, string kind, ModuleDefinition context) { Contract.Requires(regions != null); + Contract.Requires(prog != null); Contract.Requires(tok != null); Contract.Requires(v != null); - regions.Add(new IdRegion(tok, v, isDefinition, kind, context)); + if (InMainFile(prog, tok)) { + regions.Add(new IdRegion(tok, v, isDefinition, kind, context)); + } } - public static void Add(List regions, Bpl.IToken tok, Field decl, Microsoft.Dafny.Type showType, string kind, bool isDefinition, ModuleDefinition context) { + public static void Add(List regions, Microsoft.Dafny.Program prog, Bpl.IToken tok, Field decl, Microsoft.Dafny.Type showType, string kind, bool isDefinition, ModuleDefinition context) { Contract.Requires(regions != null); + Contract.Requires(prog != null); Contract.Requires(tok != null); Contract.Requires(decl != null); Contract.Requires(kind != null); - regions.Add(new IdRegion(tok, decl, showType, kind, isDefinition, context)); + if (InMainFile(prog, tok)) { + regions.Add(new IdRegion(tok, decl, showType, kind, isDefinition, context)); + } } - public static void Add(List regions, Bpl.IToken tok, string text, int length) { + public static void Add(List regions, Microsoft.Dafny.Program prog, Bpl.IToken tok, string text, int length) { Contract.Requires(regions != null); + Contract.Requires(prog != null); Contract.Requires(tok != null); Contract.Requires(text != null); - regions.Add(new IdRegion(tok, OccurrenceKind.AdditionalInformation, text, length)); + if (InMainFile(prog, tok)) { + regions.Add(new IdRegion(tok, OccurrenceKind.AdditionalInformation, text, length)); + } } private IdRegion(Bpl.IToken tok, IVariable v, bool isDefinition, string kind, ModuleDefinition context) { @@ -442,6 +455,15 @@ namespace DafnyLanguage } } + public abstract class DafnyRegion + { + public static bool InMainFile(Microsoft.Dafny.Program prog, Bpl.IToken tok) { + Contract.Requires(prog != null); + Contract.Requires(tok != null); + return object.Equals(prog.FullName, tok.filename); + } + } + #endregion } diff --git a/Source/DafnyExtension/OutliningTagger.cs b/Source/DafnyExtension/OutliningTagger.cs index 85771e94..ea611594 100644 --- a/Source/DafnyExtension/OutliningTagger.cs +++ b/Source/DafnyExtension/OutliningTagger.cs @@ -80,7 +80,7 @@ namespace DafnyLanguage if (start == end) yield break; foreach (var r in _regions) { - if (0 <= r.Length && r.Start >= start && r.Start + r.Length <= end) { + if (0 <= r.Length && r.Start <= end && start <= r.Start + r.Length) { yield return new TagSpan( new SnapshotSpan(_snapshot, r.Start, r.Length), new OutliningRegionTag(false, false, "...", r.HoverText)); @@ -130,18 +130,18 @@ namespace DafnyLanguage if (module.IsAbstract) { nm = "abstract " + nm; } - newRegions.Add(new OutliningRegion(module, nm)); + OutliningRegion.Add(newRegions, program, module, nm); } foreach (Dafny.TopLevelDecl d in module.TopLevelDecls) { if (!HasBodyTokens(d) && !(d is Dafny.ClassDecl)) { continue; } if (d is Dafny.OpaqueTypeDecl) { - newRegions.Add(new OutliningRegion(d, "type")); + OutliningRegion.Add(newRegions, program, d, "type"); } else if (d is Dafny.CoDatatypeDecl) { - newRegions.Add(new OutliningRegion(d, "codatatype")); + OutliningRegion.Add(newRegions, program, d, "codatatype"); } else if (d is Dafny.DatatypeDecl) { - newRegions.Add(new OutliningRegion(d, "datatype")); + OutliningRegion.Add(newRegions, program, d, "datatype"); } else if (d is Dafny.ModuleDecl) { // do nothing here, since the outer loop handles modules } else { @@ -149,9 +149,9 @@ namespace DafnyLanguage if (cl.IsDefaultClass) { // do nothing } else if (cl is Dafny.IteratorDecl) { - newRegions.Add(new OutliningRegion(cl, "iterator")); + OutliningRegion.Add(newRegions, program, cl, "iterator"); } else { - newRegions.Add(new OutliningRegion(cl, "class")); + OutliningRegion.Add(newRegions, program, cl, "class"); } // do the class members (in particular, functions and methods) foreach (Dafny.MemberDecl m in cl.Members) { @@ -168,7 +168,7 @@ namespace DafnyLanguage if (!m.IsGhost) { nm += " method"; } - newRegions.Add(new OutliningRegion(m, nm)); + OutliningRegion.Add(newRegions, program, m, nm); } else if (m is Dafny.Method && ((Dafny.Method)m).Body != null) { var nm = m is Dafny.Constructor ? "constructor" : @@ -179,7 +179,7 @@ namespace DafnyLanguage if (m.IsGhost && !(m is Dafny.CoLemma)) { nm = "ghost " + nm; } - newRegions.Add(new OutliningRegion(m, nm)); + OutliningRegion.Add(newRegions, program, m, nm); } } } @@ -196,12 +196,20 @@ namespace DafnyLanguage return decl.BodyStartTok != Bpl.Token.NoToken && decl.BodyEndTok != Bpl.Token.NoToken; } - class OutliningRegion + class OutliningRegion : DafnyRegion { + public static void Add(List regions, Microsoft.Dafny.Program prog, Dafny.INamedRegion decl, string kind) { + Contract.Requires(regions != null); + Contract.Requires(prog != null); + if (InMainFile(prog, decl.BodyStartTok)) { + regions.Add(new OutliningRegion(decl, kind)); + } + } + public readonly int Start; public readonly int Length; public readonly string HoverText; - public OutliningRegion(Dafny.INamedRegion decl, string kind) { + private OutliningRegion(Dafny.INamedRegion decl, string kind) { int startPosition = decl.BodyStartTok.pos + 1; // skip the open-curly brace itself int length = decl.BodyEndTok.pos - startPosition; Start = startPosition; -- cgit v1.2.3