diff --git a/Source/DafnyCore.Test/DooFileTest.cs b/Source/DafnyCore.Test/DooFileTest.cs index f62657c7279..98705c6a52b 100644 --- a/Source/DafnyCore.Test/DooFileTest.cs +++ b/Source/DafnyCore.Test/DooFileTest.cs @@ -1,4 +1,6 @@ using Microsoft.Dafny; +using Microsoft.Extensions.Logging; +using Microsoft.Extensions.Logging.Abstractions; using Tomlyn; namespace DafnyCore.Test; @@ -33,7 +35,7 @@ private static Program ParseProgram(string dafnyProgramText, DafnyOptions option var rootUri = new Uri(fullFilePath); Microsoft.Dafny.Type.ResetScopes(); var errorReporter = new ConsoleErrorReporter(options); - var program = ParseUtils.Parse(dafnyProgramText, rootUri, errorReporter); + var program = new ProgramParser().Parse(dafnyProgramText, rootUri, errorReporter); Assert.Equal(0, errorReporter.ErrorCount); return program; } diff --git a/Source/DafnyCore/AST/BuiltIns.cs b/Source/DafnyCore/AST/BuiltIns.cs index 8ca1bbf6dfb..4862ae8aa35 100644 --- a/Source/DafnyCore/AST/BuiltIns.cs +++ b/Source/DafnyCore/AST/BuiltIns.cs @@ -64,6 +64,9 @@ public static Attributes AxiomAttribute() { return new Attributes("axiom", new List(), null); } + /// + /// Ensures this instance contains the requested type + /// public UserDefinedType ArrayType(int dims, Type arg, bool allowCreationOfNewClass) { Contract.Requires(1 <= dims); Contract.Requires(arg != null); diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs index f5f0dd90aef..a13929060a1 100644 --- a/Source/DafnyCore/AST/Cloner.cs +++ b/Source/DafnyCore/AST/Cloner.cs @@ -5,6 +5,7 @@ using System.Collections.Generic; using System.Numerics; using System.Diagnostics.Contracts; +using System.Linq; using System.Xml; namespace Microsoft.Dafny { @@ -14,50 +15,72 @@ interface ICloneable { } public class Cloner { + public bool CloneResolvedFields { get; } private readonly Dictionary statementClones = new(); private readonly Dictionary clones = new(); private readonly Dictionary memberClones = new(); + private readonly bool cloneLiteralModuleDefinition; public void AddStatementClone(Statement original, Statement clone) { statementClones.Add(original, clone); } - public Cloner(bool cloneResolvedFields = false) { - this.CloneResolvedFields = cloneResolvedFields; + public Cloner(bool cloneLiteralModuleDefinition = false, bool cloneResolvedFields = false) { + this.cloneLiteralModuleDefinition = cloneLiteralModuleDefinition; + CloneResolvedFields = cloneResolvedFields; } - public virtual ModuleDefinition CloneModuleDefinition(ModuleDefinition m, Name name) { + public virtual ModuleDefinition CloneModuleDefinition(ModuleDefinition m, ModuleDefinition newParent) { if (m is DefaultModuleDefinition defaultModuleDefinition) { - return new DefaultModuleDefinition(this, defaultModuleDefinition); + var result = new DefaultModuleDefinition(this, defaultModuleDefinition) { + EnclosingModule = newParent + }; + return result; } - return new ModuleDefinition(this, m, name); + return new ModuleDefinition(this, m) { + EnclosingModule = newParent + }; } - public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) { + public virtual ModuleDefinition CloneModuleDefinition(ModuleDefinition m, ModuleDefinition newParent, Name name) { + if (m is DefaultModuleDefinition defaultModuleDefinition) { + var result = new DefaultModuleDefinition(this, defaultModuleDefinition) { + EnclosingModule = newParent + }; + return result; + } + + return new ModuleDefinition(this, m, name) { + EnclosingModule = newParent + }; + + } + + public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition parent) { Contract.Requires(d != null); - Contract.Requires(m != null); + Contract.Requires(parent != null); if (d is AbstractTypeDecl) { var dd = (AbstractTypeDecl)d; - return new AbstractTypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), m, CloneTPChar(dd.Characteristics), dd.TypeArgs.ConvertAll(CloneTypeParam), dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining); + return new AbstractTypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), parent, CloneTPChar(dd.Characteristics), dd.TypeArgs.ConvertAll(CloneTypeParam), dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining); } else if (d is SubsetTypeDecl) { Contract.Assume(!(d is NonNullTypeDecl)); // don't clone the non-null type declaration; close the class, which will create a new non-null type declaration var dd = (SubsetTypeDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); - return new SubsetTypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), CloneTPChar(dd.Characteristics), tps, m, CloneBoundVar(dd.Var, false), CloneExpr(dd.Constraint), dd.WitnessKind, CloneExpr(dd.Witness), CloneAttributes(dd.Attributes)); + return new SubsetTypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), CloneTPChar(dd.Characteristics), tps, parent, CloneBoundVar(dd.Var, false), CloneExpr(dd.Constraint), dd.WitnessKind, CloneExpr(dd.Witness), CloneAttributes(dd.Attributes)); } else if (d is TypeSynonymDecl) { var dd = (TypeSynonymDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); - return new TypeSynonymDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), CloneTPChar(dd.Characteristics), tps, m, CloneType(dd.Rhs), CloneAttributes(dd.Attributes)); + return new TypeSynonymDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), CloneTPChar(dd.Characteristics), tps, parent, CloneType(dd.Rhs), CloneAttributes(dd.Attributes)); } else if (d is NewtypeDecl) { var dd = (NewtypeDecl)d; if (dd.Var == null) { - return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), m, CloneType(dd.BaseType), + return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), parent, CloneType(dd.BaseType), dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining); } else { - return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), m, CloneBoundVar(dd.Var, false), + return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), parent, CloneBoundVar(dd.Var, false), CloneExpr(dd.Constraint), dd.WitnessKind, CloneExpr(dd.Witness), dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining); } @@ -69,13 +92,13 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) var dd = (IndDatatypeDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); var ctors = dd.Ctors.ConvertAll(CloneCtor); - var dt = new IndDatatypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), m, tps, ctors, dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining); + var dt = new IndDatatypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), parent, tps, ctors, dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining); return dt; } else if (d is CoDatatypeDecl) { var dd = (CoDatatypeDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); var ctors = dd.Ctors.ConvertAll(CloneCtor); - var dt = new CoDatatypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), m, tps, ctors, dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining); + var dt = new CoDatatypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), parent, tps, ctors, dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining); return dt; } else if (d is IteratorDecl) { var dd = (IteratorDecl)d; @@ -90,7 +113,7 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) var ens = dd.Ensures.ConvertAll(CloneAttributedExpr); var yens = dd.YieldEnsures.ConvertAll(CloneAttributedExpr); var body = CloneBlockStmt(dd.Body); - var iter = new IteratorDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), m, + var iter = new IteratorDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), parent, tps, ins, outs, reads, mod, decr, req, ens, yreq, yens, body, CloneAttributes(dd.Attributes), dd.SignatureEllipsis); @@ -99,32 +122,34 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) var dd = (TraitDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); var mm = dd.Members.ConvertAll(member => CloneMember(member, false)); - var cl = new TraitDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), m, tps, mm, CloneAttributes(dd.Attributes), dd.IsRefining, dd.ParentTraits.ConvertAll(CloneType)); + var cl = new TraitDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), parent, tps, mm, CloneAttributes(dd.Attributes), dd.IsRefining, dd.ParentTraits.ConvertAll(CloneType)); return cl; } else if (d is DefaultClassDecl) { var dd = (DefaultClassDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); var mm = dd.Members.ConvertAll(member => CloneMember(member, false)); - return new DefaultClassDecl(m, mm); + return new DefaultClassDecl(parent, mm); } else if (d is ClassDecl) { var dd = (ClassDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); var mm = dd.Members.ConvertAll(member => CloneMember(member, false)); - return new ClassDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), m, tps, mm, CloneAttributes(dd.Attributes), dd.IsRefining, dd.ParentTraits.ConvertAll(CloneType)); + return new ClassDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), parent, tps, mm, CloneAttributes(dd.Attributes), dd.IsRefining, dd.ParentTraits.ConvertAll(CloneType)); } else if (d is ModuleDecl) { if (d is LiteralModuleDecl moduleDecl) { - return new LiteralModuleDecl(moduleDecl.ModuleDef, m) { + //var newModuleDefinition = moduleDecl.ModuleDef; + var newModuleDefinition = this.cloneLiteralModuleDefinition ? CloneModuleDefinition(moduleDecl.ModuleDef, parent) : moduleDecl.ModuleDef; + return new LiteralModuleDecl(newModuleDefinition, parent) { DefaultExport = moduleDecl.DefaultExport }; } else if (d is AliasModuleDecl) { var a = (AliasModuleDecl)d; - return new AliasModuleDecl(Range(a.RangeToken), a.TargetQId?.Clone(false), a.NameNode.Clone(this), m, a.Opened, a.Exports); + return new AliasModuleDecl(Range(a.RangeToken), a.TargetQId?.Clone(false), a.NameNode.Clone(this), parent, a.Opened, a.Exports); } else if (d is AbstractModuleDecl) { var a = (AbstractModuleDecl)d; - return new AbstractModuleDecl(Range(a.RangeToken), a.QId?.Clone(false), a.NameNode.Clone(this), m, a.Opened, a.Exports); + return new AbstractModuleDecl(Range(a.RangeToken), a.QId?.Clone(false), a.NameNode.Clone(this), parent, a.Opened, a.Exports); } else if (d is ModuleExportDecl) { var a = (ModuleExportDecl)d; - return new ModuleExportDecl(Range(a.RangeToken), a.NameNode.Clone(this), m, a.Exports, a.Extends, a.ProvideAll, a.RevealAll, a.IsDefault, a.IsRefining); + return new ModuleExportDecl(Range(a.RangeToken), a.NameNode.Clone(this), parent, a.Exports, a.Extends, a.ProvideAll, a.RevealAll, a.IsDefault, a.IsRefining); } else { Contract.Assert(false); // unexpected declaration return null; // to please compiler @@ -180,13 +205,13 @@ public virtual Type CloneType(Type t) { return t; } else if (t is SetType) { var tt = (SetType)t; - return new SetType(tt.Finite, CloneType(tt.Arg)); + return new SetType(tt.Finite, tt.HasTypeArg() ? CloneType(tt.Arg) : null); } else if (t is SeqType) { var tt = (SeqType)t; - return new SeqType(CloneType(tt.Arg)); + return new SeqType(tt.HasTypeArg() ? CloneType(tt.Arg) : null); } else if (t is MultiSetType) { var tt = (MultiSetType)t; - return new MultiSetType(CloneType(tt.Arg)); + return new MultiSetType(tt.HasTypeArg() ? CloneType(tt.Arg) : null); } else if (t is MapType) { var tt = (MapType)t; return new MapType(tt.Finite, CloneType(tt.Domain), CloneType(tt.Range)); @@ -306,120 +331,7 @@ public virtual Expression CloneExpr(Expression expr) { return cloneableExpression.Clone(this); } - var result = CloneExprInner(expr); - if (CloneResolvedFields && expr.Type != null) { - result.Type = expr.Type; - } - return result; - } - - private Expression CloneExprInner(Expression expr) { - if (expr is LiteralExpr) { - var e = (LiteralExpr)expr; - if (e is StaticReceiverExpr) { - var ee = (StaticReceiverExpr)e; - return new StaticReceiverExpr(Tok(e.tok), CloneType(ee.UnresolvedType), ee.IsImplicit); - } else if (e.Value == null) { - return new LiteralExpr(Tok(e.tok)); - } else if (e.Value is bool) { - return new LiteralExpr(Tok(e.tok), (bool)e.Value); - } else if (e is CharLiteralExpr) { - return new CharLiteralExpr(Tok(e.tok), (string)e.Value); - } else if (e is StringLiteralExpr) { - var str = (StringLiteralExpr)e; - return new StringLiteralExpr(Tok(e.tok), (string)e.Value, str.IsVerbatim); - } else if (e.Value is BaseTypes.BigDec) { - return new LiteralExpr(Tok(e.tok), (BaseTypes.BigDec)e.Value); - } else { - return new LiteralExpr(Tok(e.tok), (BigInteger)e.Value); - } - - } else if (expr is ThisExpr) { - if (expr is ImplicitThisExpr_ConstructorCall) { - return new ImplicitThisExpr_ConstructorCall(Tok(expr.tok)); - } else if (expr is ImplicitThisExpr) { - return new ImplicitThisExpr(Tok(expr.tok)); - } else { - return new ThisExpr(Tok(expr.tok)); - } - } else if (expr is AutoGhostIdentifierExpr) { - var e = (AutoGhostIdentifierExpr)expr; - return new AutoGhostIdentifierExpr(this, e); - } else if (expr is DisplayExpression) { - DisplayExpression e = (DisplayExpression)expr; - if (expr is SetDisplayExpr) { - return new SetDisplayExpr(Tok(e.tok), ((SetDisplayExpr)expr).Finite, e.Elements.ConvertAll(CloneExpr)); - } else if (expr is MultiSetDisplayExpr) { - return new MultiSetDisplayExpr(Tok(e.tok), e.Elements.ConvertAll(CloneExpr)); - } else { - Contract.Assert(expr is SeqDisplayExpr); - return new SeqDisplayExpr(Tok(e.tok), e.Elements.ConvertAll(CloneExpr)); - } - - } else if (expr is MapDisplayExpr) { - MapDisplayExpr e = (MapDisplayExpr)expr; - List pp = new List(); - foreach (ExpressionPair p in e.Elements) { - pp.Add(new ExpressionPair(CloneExpr(p.A), CloneExpr(p.B))); - } - return new MapDisplayExpr(Tok(expr.tok), e.Finite, pp); - - } else if (expr is SeqSelectExpr) { - var e = (SeqSelectExpr)expr; - return new SeqSelectExpr(Tok(e.tok), e.SelectOne, CloneExpr(e.Seq), CloneExpr(e.E0), CloneExpr(e.E1), - Tok(e.CloseParen)); - } else if (expr is MultiSelectExpr) { - var e = (MultiSelectExpr)expr; - return new MultiSelectExpr(Tok(e.tok), CloneExpr(e.Array), e.Indices.ConvertAll(CloneExpr)); - - } else if (expr is SeqUpdateExpr) { - var e = (SeqUpdateExpr)expr; - return new SeqUpdateExpr(Tok(e.tok), CloneExpr(e.Seq), CloneExpr(e.Index), CloneExpr(e.Value)); - - } else if (expr is ApplyExpr) { - var e = (ApplyExpr)expr; - return new ApplyExpr(Tok(e.tok), CloneExpr(e.Function), e.Args.ConvertAll(CloneExpr), Tok(e.CloseParen)); - - } else if (expr is SeqConstructionExpr) { - var e = (SeqConstructionExpr)expr; - var elemType = e.ExplicitElementType == null ? null : CloneType(e.ExplicitElementType); - return new SeqConstructionExpr(Tok(e.tok), elemType, CloneExpr(e.N), CloneExpr(e.Initializer)); - - } else if (expr is MultiSetFormingExpr) { - var e = (MultiSetFormingExpr)expr; - return new MultiSetFormingExpr(Tok(e.tok), CloneExpr(e.E)); - } else if (expr is UnaryOpExpr) { - var e = (UnaryOpExpr)expr; - return new UnaryOpExpr(Tok(e.tok), e.Op, CloneExpr(e.E)); - - } else if (expr is ConversionExpr) { - var e = (ConversionExpr)expr; - return new ConversionExpr(Tok(e.tok), CloneExpr(e.E), CloneType(e.ToType)); - - } else if (expr is TypeTestExpr) { - var e = (TypeTestExpr)expr; - return new TypeTestExpr(Tok(e.tok), CloneExpr(e.E), CloneType(e.ToType)); - } else if (expr is TernaryExpr) { - var e = (TernaryExpr)expr; - return new TernaryExpr(Tok(e.tok), e.Op, CloneExpr(e.E0), CloneExpr(e.E1), CloneExpr(e.E2)); - } else if (expr is WildcardExpr) { - return new WildcardExpr(Tok(expr.tok)); - } else if (expr is StmtExpr) { - var e = (StmtExpr)expr; - return new StmtExpr(Tok(e.tok), CloneStmt(e.S), CloneExpr(e.E)); - } else if (expr is ITEExpr) { - var e = (ITEExpr)expr; - return new ITEExpr(Tok(e.tok), e.IsBindingGuard, CloneExpr(e.Test), CloneExpr(e.Thn), CloneExpr(e.Els)); - } else if (expr is ParensExpression) { - var e = (ParensExpression)expr; - return CloneExpr(e.E); // skip the parentheses in the clone - } - if (expr is Resolver_IdentifierExpr resolverIdentifierExpr) { - return new Resolver_IdentifierExpr(Tok(resolverIdentifierExpr.tok), resolverIdentifierExpr.Decl, resolverIdentifierExpr.TypeArgs); - } else { - Contract.Assert(false); - throw new cce.UnreachableException(); // unexpected expression - } + throw new Exception($"No clone implementation found for {expr.GetType()}"); // unexpected expression } public MatchCaseExpr CloneMatchCaseExpr(MatchCaseExpr c) { @@ -633,7 +545,7 @@ public virtual Method CloneMethod(Method m) { req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null); } else { return new Method(Range(m.RangeToken), m.NameNode.Clone(this), m.HasStaticKeyword, m.IsGhost, tps, ins, m.Outs.ConvertAll(o => CloneFormal(o, false)), - req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null, m.IsByMethod); + req, mod, ens, decreases, body, CloneAttributes(m.Attributes), m.SignatureEllipsis, m.IsByMethod); } } @@ -681,7 +593,7 @@ public override Expression CloneExpr(Expression expr) { /// This cloner copies the origin module signatures to their cloned declarations /// class DeepModuleSignatureCloner : Cloner { - public DeepModuleSignatureCloner(bool cloneResolvedFields = false) : base(cloneResolvedFields) { + public DeepModuleSignatureCloner(bool cloneResolvedFields = false) : base(false, cloneResolvedFields) { } public override TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) { diff --git a/Source/DafnyCore/AST/Expressions/Expressions.cs b/Source/DafnyCore/AST/Expressions/Expressions.cs index d96841b4645..425cb99bf6e 100644 --- a/Source/DafnyCore/AST/Expressions/Expressions.cs +++ b/Source/DafnyCore/AST/Expressions/Expressions.cs @@ -93,6 +93,7 @@ public Expression(IToken tok) { protected Expression(Cloner cloner, Expression original) { tok = cloner.Tok(original.tok); + RangeToken = cloner.Range(original.RangeToken); if (cloner.CloneResolvedFields && original.Type != null) { Type = original.Type; @@ -772,7 +773,7 @@ public static MatchCaseExpr CreateMatchCase(MatchCaseExpr old_case, Expression n Contract.Requires(new_body != null); Contract.Ensures(Contract.Result() != null); - var cloner = new Cloner(true); + var cloner = new Cloner(false, true); var newVars = old_case.Arguments.ConvertAll(bv => cloner.CloneBoundVar(bv, false)); new_body = VarSubstituter(old_case.Arguments.ConvertAll(x => (NonglobalVariable)x), newVars, new_body); @@ -801,7 +802,7 @@ public static Expression CreateLet(IToken tok, List> LHSs, Contract.Requires(LHSs.Count == RHSs.Count); Contract.Requires(body != null); - var cloner = new Cloner(true); + var cloner = new Cloner(false, true); var newLHSs = LHSs.ConvertAll(cloner.CloneCasePattern); var oldVars = new List(); @@ -822,7 +823,7 @@ public static Expression CreateLet(IToken tok, List> LHSs, public static Expression CreateQuantifier(QuantifierExpr expr, bool forall, Expression body = null) { Contract.Requires(expr != null); - var cloner = new Cloner(true); + var cloner = new Cloner(false, true); var newVars = expr.BoundVars.ConvertAll(bv => cloner.CloneBoundVar(bv, false)); if (body == null) { @@ -886,7 +887,7 @@ public string AsStringLiteral() { public override IEnumerable PreResolveChildren => Children; } -public class LiteralExpr : Expression { +public class LiteralExpr : Expression, ICloneable { /// /// One of the following: /// * 'null' for the 'null' literal (a special case of which is the subclass StaticReceiverExpr) @@ -974,22 +975,45 @@ protected LiteralExpr(IToken tok, string s) Contract.Requires(s != null); this.Value = s; } + + public LiteralExpr(Cloner cloner, LiteralExpr original) : base(cloner, original) { + Value = original.Value; + } + + public LiteralExpr Clone(Cloner cloner) { + return new LiteralExpr(cloner, this); + } } -public class CharLiteralExpr : LiteralExpr { +public class CharLiteralExpr : LiteralExpr, ICloneable { public CharLiteralExpr(IToken tok, string s) : base(tok, s) { Contract.Requires(s != null); } + + public CharLiteralExpr(Cloner cloner, CharLiteralExpr original) : base(cloner, original) { + } + + public new CharLiteralExpr Clone(Cloner cloner) { + return new CharLiteralExpr(cloner, this); + } } -public class StringLiteralExpr : LiteralExpr { +public class StringLiteralExpr : LiteralExpr, ICloneable { public readonly bool IsVerbatim; public StringLiteralExpr(IToken tok, string s, bool isVerbatim) : base(tok, s) { Contract.Requires(s != null); IsVerbatim = isVerbatim; } + + public StringLiteralExpr(Cloner cloner, StringLiteralExpr original) : base(cloner, original) { + IsVerbatim = original.IsVerbatim; + } + + public new StringLiteralExpr Clone(Cloner cloner) { + return new StringLiteralExpr(cloner, this); + } } public class DatatypeValue : Expression, IHasUsages, ICloneable, ICanFormat { @@ -1063,7 +1087,10 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { } } -public class ThisExpr : Expression { +public class ThisExpr : Expression, ICloneable { + public ThisExpr(Cloner cloner, ThisExpr original) : base(cloner, original) { + } + public ThisExpr(IToken tok) : base(tok) { Contract.Requires(tok != null); @@ -1094,6 +1121,10 @@ public ThisExpr(TopLevelDeclWithMembers cl) Contract.Requires(cl.tok != null); Type = Resolver.GetThisType(cl.tok, cl); } + + public ThisExpr Clone(Cloner cloner) { + return new ThisExpr(cloner, this); + } } public class ExpressionPair { public Expression A, B; @@ -1105,7 +1136,10 @@ public ExpressionPair(Expression a, Expression b) { } } -public class ImplicitThisExpr : ThisExpr { +public class ImplicitThisExpr : ThisExpr, ICloneable { + public ImplicitThisExpr(Cloner cloner, ImplicitThisExpr original) : base(cloner, original) { + } + public ImplicitThisExpr(IToken tok) : base(tok) { Contract.Requires(tok != null); @@ -1114,6 +1148,10 @@ public ImplicitThisExpr(IToken tok) public override bool IsImplicit { get { return true; } } + + public new ImplicitThisExpr Clone(Cloner cloner) { + return new ImplicitThisExpr(cloner, this); + } } /// @@ -1122,11 +1160,18 @@ public override bool IsImplicit { /// gives a way to distinguish this receiver from other receivers, which /// plays a role in checking the restrictions on divided block statements. /// -public class ImplicitThisExpr_ConstructorCall : ImplicitThisExpr { +public class ImplicitThisExpr_ConstructorCall : ImplicitThisExpr, ICloneable { + public ImplicitThisExpr_ConstructorCall(Cloner cloner, ImplicitThisExpr_ConstructorCall original) : base(cloner, original) { + } + public ImplicitThisExpr_ConstructorCall(IToken tok) : base(tok) { Contract.Requires(tok != null); } + + public new ImplicitThisExpr_ConstructorCall Clone(Cloner cloner) { + return new ImplicitThisExpr_ConstructorCall(cloner, this); + } } public class IdentifierExpr : Expression, IHasUsages, ICloneable { @@ -1223,7 +1268,7 @@ public AutoGhostIdentifierExpr(Cloner cloner, AutoGhostIdentifierExpr original) /// /// This class is used only inside the resolver itself. It gets hung in the AST in uncompleted name segments. /// -class Resolver_IdentifierExpr : Expression, IHasUsages { +class Resolver_IdentifierExpr : Expression, IHasUsages, ICloneable { public readonly TopLevelDecl Decl; public readonly List TypeArgs; [ContractInvariantMethod] @@ -1234,6 +1279,11 @@ void ObjectInvariant() { Contract.Invariant(Type is ResolverType_Module || Type is ResolverType_Type); } + public Resolver_IdentifierExpr(Cloner cloner, Resolver_IdentifierExpr original) : base(cloner, original) { + Decl = original.Decl; + TypeArgs = original.TypeArgs; + } + public override IEnumerable Children => TypeArgs.SelectMany(ta => ta.Nodes); public abstract class ResolverType : Type { @@ -1290,6 +1340,9 @@ public IEnumerable GetResolvedDeclarations() { } public IToken NameToken => tok; + public Resolver_IdentifierExpr Clone(Cloner cloner) { + return new Resolver_IdentifierExpr(cloner, this); + } } public abstract class DisplayExpression : Expression { @@ -1299,6 +1352,10 @@ void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(Elements)); } + protected DisplayExpression(Cloner cloner, DisplayExpression original) : base(cloner, original) { + Elements = original.Elements.ConvertAll(cloner.CloneExpr); + } + public DisplayExpression(IToken tok, List elements) : base(tok) { Contract.Requires(cce.NonNullElements(elements)); @@ -1308,7 +1365,7 @@ public DisplayExpression(IToken tok, List elements) public override IEnumerable SubExpressions => Elements; } -public class SetDisplayExpr : DisplayExpression, ICanFormat { +public class SetDisplayExpr : DisplayExpression, ICanFormat, ICloneable { public bool Finite; public SetDisplayExpr(IToken tok, bool finite, List elements) : base(tok, elements) { @@ -1320,18 +1377,39 @@ public SetDisplayExpr(IToken tok, bool finite, List elements) public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { return formatter.SetIndentParensExpression(indentBefore, OwnedTokens); } + + public SetDisplayExpr(Cloner cloner, SetDisplayExpr original) : base(cloner, original) { + Finite = original.Finite; + } + + public SetDisplayExpr Clone(Cloner cloner) { + return new SetDisplayExpr(cloner, this); + } } -public class MultiSetDisplayExpr : DisplayExpression { +public class MultiSetDisplayExpr : DisplayExpression, ICloneable { + public MultiSetDisplayExpr(Cloner cloner, MultiSetDisplayExpr original) : base(cloner, original) { + } + public MultiSetDisplayExpr(IToken tok, List elements) : base(tok, elements) { Contract.Requires(tok != null); Contract.Requires(cce.NonNullElements(elements)); } + + public MultiSetDisplayExpr Clone(Cloner cloner) { + return new MultiSetDisplayExpr(cloner, this); + } } -public class MapDisplayExpr : Expression, ICanFormat { +public class MapDisplayExpr : Expression, ICanFormat, ICloneable { public bool Finite; public List Elements; + + public MapDisplayExpr(Cloner cloner, MapDisplayExpr original) : base(cloner, original) { + Finite = original.Finite; + Elements = original.Elements.Select(p => new ExpressionPair(cloner.CloneExpr(p.A), cloner.CloneExpr(p.B))).ToList(); + } + public MapDisplayExpr(IToken tok, bool finite, List elements) : base(tok) { Contract.Requires(tok != null); @@ -1351,8 +1429,12 @@ public override IEnumerable SubExpressions { public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { return formatter.SetIndentParensExpression(indentBefore, OwnedTokens); } + + public MapDisplayExpr Clone(Cloner cloner) { + return new MapDisplayExpr(cloner, this); + } } -public class SeqDisplayExpr : DisplayExpression, ICanFormat { +public class SeqDisplayExpr : DisplayExpression, ICanFormat, ICloneable { public SeqDisplayExpr(IToken tok, List elements) : base(tok, elements) { Contract.Requires(cce.NonNullElements(elements)); @@ -1362,15 +1444,30 @@ public SeqDisplayExpr(IToken tok, List elements) public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { return formatter.SetIndentParensExpression(indentBefore, OwnedTokens); } + + public SeqDisplayExpr(Cloner cloner, SeqDisplayExpr original) : base(cloner, original) { + } + + public SeqDisplayExpr Clone(Cloner cloner) { + return new SeqDisplayExpr(cloner, this); + } } -public class SeqSelectExpr : Expression { +public class SeqSelectExpr : Expression, ICloneable { public readonly bool SelectOne; // false means select a range public readonly Expression Seq; public readonly Expression E0; public readonly Expression E1; public readonly IToken CloseParen; + public SeqSelectExpr(Cloner cloner, SeqSelectExpr original) : base(cloner, original) { + SelectOne = original.SelectOne; + Seq = cloner.CloneExpr(original.Seq); + E0 = cloner.CloneExpr(original.E0); + E1 = cloner.CloneExpr(original.E1); + CloseParen = cloner.Tok(original.CloseParen); + } + [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Seq != null); @@ -1405,9 +1502,13 @@ public override IEnumerable SubExpressions { } } } + + public SeqSelectExpr Clone(Cloner cloner) { + return new SeqSelectExpr(cloner, this); + } } -public class MultiSelectExpr : Expression { +public class MultiSelectExpr : Expression, ICloneable { public readonly Expression Array; public readonly List Indices; [ContractInvariantMethod] @@ -1417,6 +1518,11 @@ void ObjectInvariant() { Contract.Invariant(1 <= Indices.Count); } + public MultiSelectExpr(Cloner cloner, MultiSelectExpr original) : base(cloner, original) { + Indices = original.Indices.Select(cloner.CloneExpr).ToList(); + Array = cloner.CloneExpr(original.Array); + } + public MultiSelectExpr(IToken tok, Expression array, List indices) : base(tok) { Contract.Requires(tok != null); @@ -1435,6 +1541,10 @@ public override IEnumerable SubExpressions { } } } + + public MultiSelectExpr Clone(Cloner cloner) { + return new MultiSelectExpr(cloner, this); + } } /// @@ -1447,7 +1557,7 @@ public override IEnumerable SubExpressions { /// /// Datatype updates are represented by DatatypeUpdateExpr nodes. /// -public class SeqUpdateExpr : Expression { +public class SeqUpdateExpr : Expression, ICloneable { public readonly Expression Seq; public readonly Expression Index; public readonly Expression Value; @@ -1458,6 +1568,12 @@ void ObjectInvariant() { Contract.Invariant(Value != null); } + public SeqUpdateExpr(Cloner cloner, SeqUpdateExpr original) : base(cloner, original) { + Seq = cloner.CloneExpr(original.Seq); + Index = cloner.CloneExpr(original.Index); + Value = cloner.CloneExpr(original.Value); + } + public SeqUpdateExpr(IToken tok, Expression seq, Expression index, Expression val) : base(tok) { Contract.Requires(tok != null); @@ -1476,9 +1592,13 @@ public override IEnumerable SubExpressions { yield return Value; } } + + public SeqUpdateExpr Clone(Cloner cloner) { + return new SeqUpdateExpr(cloner, this); + } } -public class ApplyExpr : Expression { +public class ApplyExpr : Expression, ICloneable { // The idea is that this apply expression does not need a type argument substitution, // since lambda functions and anonymous functions are never polymorphic. // Make a FunctionCallExpr otherwise, to call a resolvable anonymous function. @@ -1496,6 +1616,12 @@ public override IEnumerable SubExpressions { public IToken CloseParen; + public ApplyExpr(Cloner cloner, ApplyExpr original) : base(cloner, original) { + Function = cloner.CloneExpr(original.Function); + Args = original.Args.ConvertAll(cloner.CloneExpr); + CloseParen = cloner.Tok(original.CloseParen); + } + public ApplyExpr(IToken tok, Expression fn, List args, IToken closeParen) : base(tok) { Function = fn; @@ -1503,6 +1629,10 @@ public ApplyExpr(IToken tok, Expression fn, List args, IToken closeP CloseParen = closeParen; FormatTokens = closeParen != null ? new[] { closeParen } : null; } + + public ApplyExpr Clone(Cloner cloner) { + return new ApplyExpr(cloner, this); + } } public class FunctionCallExpr : Expression, IHasUsages, ICloneable { @@ -1655,10 +1785,18 @@ public IEnumerable GetResolvedDeclarations() { public IToken NameToken => tok; } -public class SeqConstructionExpr : Expression { +public class SeqConstructionExpr : Expression, ICloneable { public Type/*?*/ ExplicitElementType; public Expression N; public Expression Initializer; + + public SeqConstructionExpr(Cloner cloner, SeqConstructionExpr original) : base(cloner, original) { + var elemType = original.ExplicitElementType == null ? null : cloner.CloneType(original.ExplicitElementType); + N = cloner.CloneExpr(original.N); + Initializer = cloner.CloneExpr(original.Initializer); + ExplicitElementType = elemType; + } + public SeqConstructionExpr(IToken tok, Type/*?*/ elementType, Expression length, Expression initializer) : base(tok) { Contract.Requires(tok != null); @@ -1682,9 +1820,13 @@ public override IEnumerable ComponentTypes { } } } + + public SeqConstructionExpr Clone(Cloner cloner) { + return new SeqConstructionExpr(cloner, this); + } } -public class MultiSetFormingExpr : Expression { +public class MultiSetFormingExpr : Expression, ICloneable { [Peer] public readonly Expression E; [ContractInvariantMethod] @@ -1692,6 +1834,10 @@ void ObjectInvariant() { Contract.Invariant(E != null); } + public MultiSetFormingExpr(Cloner cloner, MultiSetFormingExpr original) : base(cloner, original) { + E = cloner.CloneExpr(original.E); + } + [Captured] public MultiSetFormingExpr(IToken tok, Expression expr) : base(tok) { @@ -1704,6 +1850,10 @@ public MultiSetFormingExpr(IToken tok, Expression expr) public override IEnumerable SubExpressions { get { yield return E; } } + + public MultiSetFormingExpr Clone(Cloner cloner) { + return new MultiSetFormingExpr(cloner, this); + } } public abstract class UnaryExpr : Expression, ICanFormat { @@ -1733,7 +1883,7 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { } } -public class UnaryOpExpr : UnaryExpr { +public class UnaryOpExpr : UnaryExpr, ICloneable { public enum Opcode { Not, // boolean negation or bitwise negation Cardinality, @@ -1800,6 +1950,9 @@ public UnaryOpExpr(Cloner cloner, UnaryOpExpr original) : base(cloner, original) } public override bool IsImplicit => Op == Opcode.Lit; + public UnaryOpExpr Clone(Cloner cloner) { + return new UnaryOpExpr(cloner, this); + } } public class FreshExpr : UnaryOpExpr, ICloneable { @@ -1820,12 +1973,17 @@ public FreshExpr(Cloner cloner, FreshExpr original) : base(cloner, original) { } } - public FreshExpr Clone(Cloner cloner) { return new FreshExpr(cloner, this); } + public new FreshExpr Clone(Cloner cloner) { return new FreshExpr(cloner, this); } } public abstract class TypeUnaryExpr : UnaryExpr { public readonly Type ToType; - public TypeUnaryExpr(IToken tok, Expression expr, Type toType) + + protected TypeUnaryExpr(Cloner cloner, TypeUnaryExpr original) : base(cloner, original) { + ToType = cloner.CloneType(original.ToType); + } + + protected TypeUnaryExpr(IToken tok, Expression expr, Type toType) : base(tok, expr) { Contract.Requires(tok != null); Contract.Requires(expr != null); @@ -1842,8 +2000,13 @@ public override IEnumerable ComponentTypes { } } -public class ConversionExpr : TypeUnaryExpr { +public class ConversionExpr : TypeUnaryExpr, ICloneable { public readonly string messagePrefix; + + public ConversionExpr(Cloner cloner, ConversionExpr original) : base(cloner, original) { + messagePrefix = original.messagePrefix; + } + public ConversionExpr(IToken tok, Expression expr, Type toType, string messagePrefix = "") : base(tok, expr, toType) { Contract.Requires(tok != null); @@ -1851,15 +2014,26 @@ public ConversionExpr(IToken tok, Expression expr, Type toType, string messagePr Contract.Requires(toType != null); this.messagePrefix = messagePrefix; } + + public ConversionExpr Clone(Cloner cloner) { + return new ConversionExpr(cloner, this); + } } -public class TypeTestExpr : TypeUnaryExpr { +public class TypeTestExpr : TypeUnaryExpr, ICloneable { + public TypeTestExpr(Cloner cloner, TypeTestExpr original) : base(cloner, original) { + } + public TypeTestExpr(IToken tok, Expression expr, Type toType) : base(tok, expr, toType) { Contract.Requires(tok != null); Contract.Requires(expr != null); Contract.Requires(toType != null); } + + public TypeTestExpr Clone(Cloner cloner) { + return new TypeTestExpr(cloner, this); + } } public class BinaryExpr : Expression, ICloneable, ICanFormat { @@ -2392,13 +2566,21 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { } } -public class TernaryExpr : Expression { +public class TernaryExpr : Expression, ICloneable { public readonly Opcode Op; public readonly Expression E0; public readonly Expression E1; public readonly Expression E2; public enum Opcode { /*SOON: IfOp,*/ PrefixEqOp, PrefixNeqOp } public static readonly bool PrefixEqUsesNat = false; // "k" is either a "nat" or an "ORDINAL" + + public TernaryExpr(Cloner cloner, TernaryExpr original) : base(cloner, original) { + Op = original.Op; + E0 = cloner.CloneExpr(original.E0); + E1 = cloner.CloneExpr(original.E1); + E2 = cloner.CloneExpr(original.E2); + } + public TernaryExpr(IToken tok, Opcode op, Expression e0, Expression e1, Expression e2) : base(tok) { Contract.Requires(tok != null); @@ -2418,6 +2600,10 @@ public override IEnumerable SubExpressions { yield return E2; } } + + public TernaryExpr Clone(Cloner cloner) { + return new TernaryExpr(cloner, this); + } } public class LetOrFailExpr : ConcreteSyntaxExpression, ICloneable, ICanFormat { @@ -2701,11 +2887,19 @@ public override bool SetIndent(int indentBefore, TokenNewIndentCollector formatt } } -public class WildcardExpr : Expression { // a WildcardExpr can occur only in reads clauses and a loop's decreases clauses (with different meanings) +public class WildcardExpr : Expression, ICloneable { // a WildcardExpr can occur only in reads clauses and a loop's decreases clauses (with different meanings) + + public WildcardExpr(Cloner cloner, WildcardExpr original) : base(cloner, original) { + } + public WildcardExpr(IToken tok) : base(tok) { Contract.Requires(tok != null); } + + public WildcardExpr Clone(Cloner cloner) { + return new WildcardExpr(cloner, this); + } } /// @@ -2713,7 +2907,7 @@ public WildcardExpr(IToken tok) /// The expression S;E evaluates to whatever E evaluates to, but its well-formedness comes down to /// executing S (which itself must be well-formed) and then checking the well-formedness of E. /// -public class StmtExpr : Expression, ICanFormat { +public class StmtExpr : Expression, ICanFormat, ICloneable { public readonly Statement S; public readonly Expression E; [ContractInvariantMethod] @@ -2722,6 +2916,11 @@ void ObjectInvariant() { Contract.Invariant(E != null); } + public StmtExpr(Cloner cloner, StmtExpr original) : base(cloner, original) { + E = cloner.CloneExpr(original.E); + S = cloner.CloneStmt(original.S); + } + public override IEnumerable Children => new Node[] { S, E }; public StmtExpr(IToken tok, Statement stmt, Expression expr) @@ -2776,14 +2975,25 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { formatter.Visit(E, indentBefore); return false; } + + public StmtExpr Clone(Cloner cloner) { + return new StmtExpr(cloner, this); + } } -public class ITEExpr : Expression, ICanFormat { +public class ITEExpr : Expression, ICanFormat, ICloneable { public readonly bool IsBindingGuard; public readonly Expression Test; public readonly Expression Thn; public readonly Expression Els; + public ITEExpr(Cloner cloner, ITEExpr original) : base(cloner, original) { + IsBindingGuard = original.IsBindingGuard; + Test = cloner.CloneExpr(original.Test); + Thn = cloner.CloneExpr(original.Thn); + Els = cloner.CloneExpr(original.Els); + } + public enum ITECompilation { CompileBothBranches, CompileJustThenBranch, @@ -2882,6 +3092,10 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { return false; } + + public ITEExpr Clone(Cloner cloner) { + return new ITEExpr(cloner, this); + } } @@ -3198,7 +3412,7 @@ public override IEnumerable TerminalExpressions { public override IEnumerable ComponentTypes => ResolvedExpression.ComponentTypes; } -public class ParensExpression : ConcreteSyntaxExpression, ICanFormat { +public class ParensExpression : ConcreteSyntaxExpression, ICanFormat, ICloneable { public readonly Expression E; public ParensExpression(IToken tok, Expression e) : base(tok) { @@ -3228,6 +3442,10 @@ public override IEnumerable PreResolveSubExpressions { public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { return formatter.SetIndentParensExpression(indentBefore, OwnedTokens); } + + public ParensExpression Clone(Cloner cloner) { + return new ParensExpression(cloner, this); + } } public class DatatypeUpdateExpr : ConcreteSyntaxExpression, IHasUsages, ICloneable { @@ -3311,7 +3529,7 @@ public AutoGeneratedExpression(IToken tok, Expression e) Contract.Requires(e != null); } - public AutoGeneratedExpression Clone(Cloner cloner) { + public new AutoGeneratedExpression Clone(Cloner cloner) { return new AutoGeneratedExpression(cloner, this); } diff --git a/Source/DafnyCore/AST/Expressions/StaticReceiverExpr.cs b/Source/DafnyCore/AST/Expressions/StaticReceiverExpr.cs index 2467cc56135..97505695fb1 100644 --- a/Source/DafnyCore/AST/Expressions/StaticReceiverExpr.cs +++ b/Source/DafnyCore/AST/Expressions/StaticReceiverExpr.cs @@ -8,7 +8,7 @@ namespace Microsoft.Dafny; /// Instances of this class are introduced during resolution to indicate that a static method or function has /// been invoked without specifying a receiver (that is, by just giving the name of the enclosing class). /// -public class StaticReceiverExpr : LiteralExpr { +public class StaticReceiverExpr : LiteralExpr, ICloneable { public readonly Type UnresolvedType; /// /// A static member can be invoked through an object, in which case the object is not used for the call. @@ -29,6 +29,11 @@ public StaticReceiverExpr(IToken tok, Type t, bool isImplicit) IsImplicit = isImplicit; } + public StaticReceiverExpr(Cloner cloner, StaticReceiverExpr original) : base(cloner, original) { + UnresolvedType = cloner.CloneType(original.UnresolvedType); + IsImplicit = original.IsImplicit; + } + /// /// Constructs a resolved LiteralExpr representing the fictitious static-receiver literal whose type is /// "cl" parameterized by the type arguments of "cl" itself. @@ -94,4 +99,8 @@ public override IEnumerable SubExpressions { public override IEnumerable Children => new[] { ObjectToDiscard, ContainerExpression }.Where(x => x != null).Concat(Type.Nodes); + + public new StaticReceiverExpr Clone(Cloner cloner) { + return new StaticReceiverExpr(cloner, this); + } } diff --git a/Source/DafnyCore/AST/FileModuleDefinition.cs b/Source/DafnyCore/AST/FileModuleDefinition.cs index d5aa4572b1f..2b61b4843d4 100644 --- a/Source/DafnyCore/AST/FileModuleDefinition.cs +++ b/Source/DafnyCore/AST/FileModuleDefinition.cs @@ -17,4 +17,9 @@ public FileModuleDefinition() : { } } + + public FileModuleDefinition(Cloner cloner, FileModuleDefinition original) + : base(cloner, original) { + Includes = original.Includes; + } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Grammar/ParseUtils.cs b/Source/DafnyCore/AST/Grammar/ProgramParser.cs similarity index 88% rename from Source/DafnyCore/AST/Grammar/ParseUtils.cs rename to Source/DafnyCore/AST/Grammar/ProgramParser.cs index 1962f379572..1148b94f1ac 100644 --- a/Source/DafnyCore/AST/Grammar/ParseUtils.cs +++ b/Source/DafnyCore/AST/Grammar/ProgramParser.cs @@ -5,16 +5,29 @@ using System.Linq; using System.Text; using System.Threading; +using Microsoft.Extensions.Logging; +using Microsoft.Extensions.Logging.Abstractions; using static Microsoft.Dafny.ParseErrors; namespace Microsoft.Dafny; -public record DfyParseResult(BatchErrorReporter ErrorReporter, FileModuleDefinition Module, - IReadOnlyList> ModifyBuiltins); +public record DfyParseResult( + BatchErrorReporter ErrorReporter, + FileModuleDefinition Module, + IReadOnlyList> ModifyBuiltins + ); -public class ParseUtils { +public class ProgramParser { + protected readonly ILogger logger; - public static Program ParseFiles(string programName, IReadOnlyList files, ErrorReporter errorReporter, + public ProgramParser() : this(NullLogger.Instance) { + } + + public ProgramParser(ILogger logger) { + this.logger = logger; + } + + public Program ParseFiles(string programName, IReadOnlyList files, ErrorReporter errorReporter, CancellationToken cancellationToken) { var options = errorReporter.Options; var builtIns = new BuiltIns(options); @@ -44,6 +57,9 @@ public static Program ParseFiles(string programName, IReadOnlyList fi dafnyFile.Content, dafnyFile.Uri ); + if (parseResult.ErrorReporter.ErrorCount != 0) { + logger.LogDebug($"encountered {parseResult.ErrorReporter.ErrorCount} errors while parsing {dafnyFile.Uri}"); + } AddParseResultToProgram(parseResult, program); if (defaultModule.RangeToken.StartToken.Uri == null) { @@ -51,6 +67,7 @@ public static Program ParseFiles(string programName, IReadOnlyList fi } } catch (Exception e) { + logger.LogDebug(e, $"encountered an exception while parsing {dafnyFile.Uri}"); var internalErrorDummyToken = new Token { Uri = dafnyFile.Uri, line = 1, @@ -130,7 +147,7 @@ public static void AddParseResultToProgram(DfyParseResult parseResult, Program p defaultModule.DefaultClass.SetMembersBeforeResolution(); } - public static IList TryParseIncludes( + public IList TryParseIncludes( IReadOnlyList files, IEnumerable roots, BuiltIns builtIns, @@ -199,7 +216,7 @@ private static DafnyFile IncludeToDafnyFile(BuiltIns builtIns, ErrorReporter err /// Returns the number of parsing errors encountered. /// Note: first initialize the Scanner. /// - private static DfyParseResult ParseFile(DafnyOptions options, TextReader reader, Uri uri) /* throws System.IO.IOException */ { + protected virtual DfyParseResult ParseFile(DafnyOptions options, TextReader reader, Uri uri) /* throws System.IO.IOException */ { Contract.Requires(uri != null); var text = SourcePreprocessor.ProcessDirectives(reader, new List()); try { @@ -255,7 +272,7 @@ private static Parser SetupParser(string /*!*/ s, Uri /*!*/ uri, ErrorReporter / return new Parser(errorReporter.Options, scanner, errors); } - public static Program Parse(string source, Uri uri, ErrorReporter reporter) { + public Program Parse(string source, Uri uri, ErrorReporter reporter) { var files = new[] { new DafnyFile(reporter.Options, uri, new StringReader(source)) }; return ParseFiles(uri.ToString(), files, reporter, CancellationToken.None); } diff --git a/Source/DafnyCore/AST/Modules/AbstractSignatureCloner.cs b/Source/DafnyCore/AST/Modules/AbstractSignatureCloner.cs index e59b028b471..e6d0797e1df 100644 --- a/Source/DafnyCore/AST/Modules/AbstractSignatureCloner.cs +++ b/Source/DafnyCore/AST/Modules/AbstractSignatureCloner.cs @@ -6,8 +6,8 @@ public AbstractSignatureCloner(VisibilityScope scope) : base(scope) { } - public override ModuleDefinition CloneModuleDefinition(ModuleDefinition m, Name name) { - var basem = base.CloneModuleDefinition(m, name); + public override ModuleDefinition CloneModuleDefinition(ModuleDefinition m, ModuleDefinition newParent, Name name) { + var basem = base.CloneModuleDefinition(m, newParent, name); basem.SourceDecls.RemoveAll(t => t is ModuleExportDecl); basem.ResolvedPrefixNamedModules.RemoveAll(t => t is ModuleExportDecl); return basem; diff --git a/Source/DafnyCore/AST/Modules/ScopeCloner.cs b/Source/DafnyCore/AST/Modules/ScopeCloner.cs index c83221777bc..9c14866cd7d 100644 --- a/Source/DafnyCore/AST/Modules/ScopeCloner.cs +++ b/Source/DafnyCore/AST/Modules/ScopeCloner.cs @@ -27,8 +27,8 @@ private bool VisibleInScope(Declaration d) { return d.IsVisibleInScope(scope); } - public override ModuleDefinition CloneModuleDefinition(ModuleDefinition m, Name name) { - var basem = base.CloneModuleDefinition(m, name); + public override ModuleDefinition CloneModuleDefinition(ModuleDefinition m, ModuleDefinition newParent, Name name) { + var basem = base.CloneModuleDefinition(m, newParent, name); //Merge signatures for imports which point to the same module //This makes the consistency check understand that the same element diff --git a/Source/DafnyCore/AST/Modules/TopLevelDeclarations.cs b/Source/DafnyCore/AST/Modules/TopLevelDeclarations.cs index f06f15bea82..6edbd835674 100644 --- a/Source/DafnyCore/AST/Modules/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/Modules/TopLevelDeclarations.cs @@ -70,8 +70,8 @@ public virtual bool CanBeRevealed() { public bool ScopeIsInherited { get { return scopeIsInherited; } } - public void AddVisibilityScope(VisibilityScope scope, bool IsOpaque) { - if (IsOpaque) { + public void AddVisibilityScope(VisibilityScope scope, bool isOpaque) { + if (isOpaque) { opaqueScope.Augment(scope); } else { revealScope.Augment(scope); @@ -816,7 +816,7 @@ public IEnumerable GetResolvedDeclarations() { } } -public class ModuleDefinition : RangeNode, IDeclarationOrUsage, IAttributeBearingDeclaration { +public class ModuleDefinition : RangeNode, IDeclarationOrUsage, IAttributeBearingDeclaration, ICloneable { public IToken BodyStartTok = Token.NoToken; public IToken TokenWithTrailingDocString = Token.NoToken; public string DafnyName => NameNode.StartToken.val; // The (not-qualified) name as seen in Dafny source code @@ -892,15 +892,20 @@ void ObjectInvariant() { Contract.Invariant(CallGraph != null); } - public ModuleDefinition(Cloner cloner, ModuleDefinition original, Name name) : base(cloner, original) { + public ModuleDefinition(Cloner cloner, ModuleDefinition original, Name name) : this(cloner, original) { NameNode = name; IsBuiltinName = true; + } + + public ModuleDefinition(Cloner cloner, ModuleDefinition original) : base(cloner, original) { + IsBuiltinName = original.IsBuiltinName; + NameNode = original.NameNode; PrefixIds = original.PrefixIds.Select(cloner.Tok).ToList(); + IsFacade = original.IsFacade; Attributes = original.Attributes; IsAbstract = original.IsAbstract; RefinementQId = original.RefinementQId; - EnclosingModule = original.EnclosingModule; defaultClassFirst = original.defaultClassFirst; foreach (var d in original.SourceDecls) { SourceDecls.Add(cloner.CloneDeclaration(d, this)); @@ -1167,9 +1172,13 @@ public void PreResolveSnapshotForFormatter() { public override IEnumerable Assumptions(Declaration decl) { return TopLevelDecls.SelectMany(m => m.Assumptions(decl)); } + + public ModuleDefinition Clone(Cloner cloner) { + return new ModuleDefinition(cloner, this); + } } -public class DefaultModuleDefinition : ModuleDefinition { +public class DefaultModuleDefinition : ModuleDefinition, ICloneable { public List Includes { get; } = new(); public IList RootSourceUris { get; } @@ -1186,6 +1195,9 @@ public DefaultModuleDefinition(IList rootSourceUris, bool defaultClassFirst public override bool IsDefaultModule => true; public override IEnumerable PreResolveChildren => Includes.Concat(base.PreResolveChildren); + public new DefaultModuleDefinition Clone(Cloner cloner) { + return new DefaultModuleDefinition(cloner, this); + } } public abstract class TopLevelDecl : Declaration, TypeParameter.ParentType { diff --git a/Source/DafnyCore/AST/Statements/CalcStmt.cs b/Source/DafnyCore/AST/Statements/CalcStmt.cs index 7e0fb0834b8..c0c19327d0f 100644 --- a/Source/DafnyCore/AST/Statements/CalcStmt.cs +++ b/Source/DafnyCore/AST/Statements/CalcStmt.cs @@ -199,8 +199,9 @@ public CalcOp GetInferredDefaultOp() { public readonly List Lines; // Last line is dummy, in order to form a proper step with the dangling hint public readonly List Hints; // Hints[i] comes after line i; block statement is used as a container for multiple sub-hints public readonly CalcOp UserSuppliedOp; // may be null, if omitted by the user - public CalcOp Op; // main operator of the calculation (either UserSuppliedOp or (after resolution) an inferred CalcOp) public readonly List StepOps; // StepOps[i] comes after line i + [FilledInDuringResolution] + public CalcOp Op; // main operator of the calculation (either UserSuppliedOp or (after resolution) an inferred CalcOp) [FilledInDuringResolution] public readonly List Steps; // expressions li op l (last step is dummy) [FilledInDuringResolution] public Expression Result; // expression l0 ResultOp ln diff --git a/Source/DafnyCore/AST/Statements/Statements.cs b/Source/DafnyCore/AST/Statements/Statements.cs index 4df7da0cdaf..140602abdb7 100644 --- a/Source/DafnyCore/AST/Statements/Statements.cs +++ b/Source/DafnyCore/AST/Statements/Statements.cs @@ -813,6 +813,7 @@ public LocalVariable(Cloner cloner, LocalVariable original) : base(cloner, original) { name = original.Name; OptionalType = cloner.CloneType(original.OptionalType); + IsTypeExplicit = original.IsTypeExplicit; IsGhost = original.IsGhost; if (cloner.CloneResolvedFields) { diff --git a/Source/DafnyCore/AST/SubstitutingCloner.cs b/Source/DafnyCore/AST/SubstitutingCloner.cs index 0e0bc79c29f..d1d7f18abb3 100644 --- a/Source/DafnyCore/AST/SubstitutingCloner.cs +++ b/Source/DafnyCore/AST/SubstitutingCloner.cs @@ -6,7 +6,7 @@ class SubstitutingCloner : Cloner { private readonly Dictionary substitutions; public SubstitutingCloner(Dictionary substitutions, bool cloneResolvedFields) - : base(cloneResolvedFields) { + : base(false, cloneResolvedFields) { this.substitutions = substitutions; } diff --git a/Source/DafnyCore/AST/Types/Types.cs b/Source/DafnyCore/AST/Types/Types.cs index 0f8f4b39aaf..2ae8b27a8a6 100644 --- a/Source/DafnyCore/AST/Types/Types.cs +++ b/Source/DafnyCore/AST/Types/Types.cs @@ -1962,7 +1962,10 @@ public Type Arg { return arg; } } // denotes the Domain type for a Map + + [FilledInDuringResolution] private Type arg; + // The following methods, HasTypeArg and SetTypeArg/SetTypeArgs, are to be called during resolution to make sure that "arg" becomes set. public bool HasTypeArg() { return arg != null; diff --git a/Source/DafnyCore/AST/VisibilityScope.cs b/Source/DafnyCore/AST/VisibilityScope.cs index 5dd73fb3663..9876211cff0 100644 --- a/Source/DafnyCore/AST/VisibilityScope.cs +++ b/Source/DafnyCore/AST/VisibilityScope.cs @@ -3,15 +3,21 @@ using System.Diagnostics.Contracts; namespace Microsoft.Dafny { + /// + /// A scope consists of a set of identifiers. + /// Two scopes overlap if the intersections of their identifiers is not empty + /// public class VisibilityScope { - private static uint maxScopeID = 0; + private static uint maxScopeId; - private SortedSet scopeTokens = new SortedSet(); + private readonly SortedSet scopeTokens = new(); // Only for debugging - private SortedSet scopeIds = new SortedSet(); + private readonly SortedSet scopeIds = new(); - private bool overlaps(SortedSet set1, SortedSet set2) { + private static bool Overlaps(SortedSet set1, SortedSet set2) { + // This conditional implements a performance optimization, + // since there is an iteration over the second argument to Overlaps if (set1.Count < set2.Count) { return set2.Overlaps(set1); } else { @@ -19,23 +25,26 @@ private bool overlaps(SortedSet set1, SortedSet set2) { } } - private Dictionary> cached = new Dictionary>(); + private Dictionary> cached = new(); - //By convention, the "null" scope sees all + // By convention, the "null" scope sees all public bool VisibleInScope(VisibilityScope other) { if (other != null) { if (cached.TryGetValue(other, out var result)) { if (result.Item1 == other.scopeTokens.Count) { + // If the second scope did not change, then we can use the cached result. + // If this scoped changed, the cache would have been cleared. return result.Item2; } else { + // If the scoped used to overlap, they still do, since scopes only grow. if (result.Item2) { return true; } } } - var isoverlap = overlaps(other.scopeTokens, this.scopeTokens); - cached[other] = new Tuple(other.scopeTokens.Count, isoverlap); - return isoverlap; + var overlaps = Overlaps(other.scopeTokens, scopeTokens); + cached[other] = new Tuple(other.scopeTokens.Count, overlaps); + return overlaps; } return true; @@ -56,16 +65,15 @@ public void Augment(VisibilityScope other) { } public VisibilityScope(string name) { - scopeTokens.Add(maxScopeID); + scopeTokens.Add(maxScopeId); scopeIds.Add(name); - if (maxScopeID == uint.MaxValue) { + if (maxScopeId == uint.MaxValue) { Contract.Assert(false); } - maxScopeID++; + maxScopeId++; } public VisibilityScope() { } - } } \ No newline at end of file diff --git a/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs b/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs index f0529d74b5c..f059a3c2901 100644 --- a/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs +++ b/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs @@ -124,7 +124,7 @@ private Expression CompileNestedMatchExpr(NestedMatchExpr nestedMatchExpr) { private Statement CompileNestedMatchStmt(NestedMatchStmt nestedMatchStmt) { var cases = nestedMatchStmt.Cases.SelectMany(FlattenNestedMatchCaseStmt) - .Select(nms => nms.Clone(new Cloner(true))) + .Select(nms => nms.Clone(new Cloner(false, true))) .ToList(); var state = new MatchCompilationState(nestedMatchStmt, cases, resolutionContext.WithGhost(nestedMatchStmt.IsGhost), nestedMatchStmt.Attributes); @@ -422,7 +422,7 @@ private CaseBody CompileHeadsContainingConstructor(MatchCompilationState mti, Ma private MatchCase CreateMatchCase(IToken tok, DatatypeCtor ctor, List freshPatBV, CaseBody bodyContainer, bool fromBoundVar) { MatchCase newMatchCase; - var cloner = new Cloner(true); + var cloner = new Cloner(false, true); if (bodyContainer.Node is Statement statement) { var body = UnboxStmt(statement).Select(cloner.CloneStmt).ToList(); newMatchCase = new MatchCaseStmt(tok.ToRange(), ctor, fromBoundVar, freshPatBV, body, bodyContainer.Attributes); diff --git a/Source/DafnyCore/Compilers/CSharp/Synthesizer-Csharp.cs b/Source/DafnyCore/Compilers/CSharp/Synthesizer-Csharp.cs index abb1348da9f..a988b09608a 100644 --- a/Source/DafnyCore/Compilers/CSharp/Synthesizer-Csharp.cs +++ b/Source/DafnyCore/Compilers/CSharp/Synthesizer-Csharp.cs @@ -286,7 +286,7 @@ private void SynthesizeExpression(ConcreteSyntaxTree wr, ForallExpr forallExpr, wr.Write("\treturn "); wr.Append(compiler.Expr(binaryExpr.E0, false, wStmts)); wr.WriteLine(";"); - binaryExpr = (BinaryExpr)binaryExpr.E1; + binaryExpr = (BinaryExpr)binaryExpr.E1.Resolved; break; case BinaryExpr.Opcode.Eq: wr.WriteLine("\treturn true;"); diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 2143621793f..827fe95c272 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -28,6 +28,7 @@ + diff --git a/Source/DafnyCore/DafnyMain.cs b/Source/DafnyCore/DafnyMain.cs index e0593db8527..4c0ca249d31 100644 --- a/Source/DafnyCore/DafnyMain.cs +++ b/Source/DafnyCore/DafnyMain.cs @@ -14,6 +14,8 @@ using System.Threading.Tasks; using DafnyCore; using Microsoft.Boogie; +using Microsoft.Extensions.Logging; +using Microsoft.Extensions.Logging.Abstractions; namespace Microsoft.Dafny { @@ -59,15 +61,13 @@ public static string Parse(IReadOnlyList files, string programName, D program = null; var defaultClassFirst = options.VerifyAllModules; - var defaultModuleDefinition = - new DefaultModuleDefinition(files.Where(f => !f.IsPreverified).Select(f => f.Uri).ToList(), defaultClassFirst); ErrorReporter reporter = options.DiagnosticsFormat switch { DafnyOptions.DiagnosticsFormats.PlainText => new ConsoleErrorReporter(options), DafnyOptions.DiagnosticsFormats.JSON => new JsonConsoleErrorReporter(options), _ => throw new ArgumentOutOfRangeException() }; - program = ParseUtils.ParseFiles(programName, files, reporter, CancellationToken.None); + program = new ProgramParser().ParseFiles(programName, files, reporter, CancellationToken.None); var errorCount = program.Reporter.ErrorCount; if (errorCount != 0) { return $"{errorCount} parse errors detected in {program.Name}"; diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs index fbff94789b0..6336c3ccbd8 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs @@ -57,7 +57,7 @@ void ResolveNamesAndInferTypesForOneDeclarationInitial(TopLevelDecl topd) { AddXConstraint(newtypeDecl.tok, "NumericType", newtypeDecl.BaseType, "newtypes must be based on some numeric type (got {0})"); // type check the constraint, if any if (newtypeDecl.Var != null) { - Contract.Assert(object.ReferenceEquals(newtypeDecl.Var.Type, newtypeDecl.BaseType)); // follows from NewtypeDecl invariant + Contract.Assert(object.ReferenceEquals(newtypeDecl.Var.Type, newtypeDecl.BaseType.NormalizeExpand(true))); // follows from NewtypeDecl invariant Contract.Assert(newtypeDecl.Constraint != null); // follows from NewtypeDecl invariant scope.PushMarker(); diff --git a/Source/DafnyCore/Resolver/Resolver.cs b/Source/DafnyCore/Resolver/Resolver.cs index e677fdfea65..ef82f38eb5e 100644 --- a/Source/DafnyCore/Resolver/Resolver.cs +++ b/Source/DafnyCore/Resolver/Resolver.cs @@ -560,7 +560,7 @@ public void ResolveProgram(Program prog) { // compilation should only proceed if everything is good, including the signature (which preResolveErrorCount does not include); CompilationCloner cloner = new CompilationCloner(compilationModuleClones); var compileName = new Name(m.NameNode.RangeToken, m.GetCompileName(Options) + "_Compile"); - var nw = cloner.CloneModuleDefinition(m, compileName); + var nw = cloner.CloneModuleDefinition(m, m.EnclosingModule, compileName); compilationModuleClones.Add(m, nw); var oldErrorsOnly = reporter.ErrorsOnly; reporter.ErrorsOnly = true; // turn off warning reporting for the clone @@ -1190,7 +1190,7 @@ private void CheckModuleExportConsistency(Program program, ModuleDefinition m) { var scope = exportDecl.Signature.VisibilityScope; Cloner cloner = new ScopeCloner(scope); - var exportView = cloner.CloneModuleDefinition(m, m.NameNode); + var exportView = cloner.CloneModuleDefinition(m, m.EnclosingModule, m.NameNode); if (Options.DafnyPrintExportedViews.Contains(exportDecl.FullName)) { var wr = Options.OutputWriter; wr.WriteLine("/* ===== export set {0}", exportDecl.FullName); diff --git a/Source/DafnyCore/Rewriters/AutoReqFunctionRewriter.cs b/Source/DafnyCore/Rewriters/AutoReqFunctionRewriter.cs index c90308222a8..90190a46981 100644 --- a/Source/DafnyCore/Rewriters/AutoReqFunctionRewriter.cs +++ b/Source/DafnyCore/Rewriters/AutoReqFunctionRewriter.cs @@ -279,7 +279,7 @@ List GenerateAutoReqs(Expression expr) { reqs.AddRange(GenerateAutoReqs(e.E0)); foreach (var req in GenerateAutoReqs(e.E1)) { // We only care about this req if E0 is true, since And short-circuits - var cloner = new Cloner(true); + var cloner = new Cloner(false, true); var e0 = cloner.CloneExpr(e.E0); reqs.Add(Expression.CreateImplies(e0, req)); } @@ -289,7 +289,7 @@ List GenerateAutoReqs(Expression expr) { reqs.AddRange(GenerateAutoReqs(e.E0)); foreach (var req in GenerateAutoReqs(e.E1)) { // We only care about this req if E0 is false, since Or short-circuits - var cloner = new Cloner(true); + var cloner = new Cloner(false, true); var e0 = cloner.CloneExpr(e.E0); reqs.Add(Expression.CreateImplies(Expression.CreateNot(e.E1.tok, e0), req)); } diff --git a/Source/DafnyCore/Rewriters/RefinementTransformer.cs b/Source/DafnyCore/Rewriters/RefinementTransformer.cs index eae5f30d07b..7e358d57978 100644 --- a/Source/DafnyCore/Rewriters/RefinementTransformer.cs +++ b/Source/DafnyCore/Rewriters/RefinementTransformer.cs @@ -253,14 +253,14 @@ void PreResolveWorker(ModuleDefinition m) { var clone = refinementCloner.CloneDeclaration(d, m); m.SourceDecls.Add(clone); } else { - var nw = nwPointer.Get(); - if (d.Name == "_default" || nw.IsRefining || d is AbstractTypeDecl) { + var neww = nwPointer.Get(); + if (d.Name == "_default" || neww.IsRefining || d is AbstractTypeDecl) { MergeTopLevelDecls(m, nwPointer, d); - } else if (nw is TypeSynonymDecl) { - var msg = $"a type synonym ({nw.Name}) is not allowed to replace a {d.WhatKind} from the refined module ({m.RefinementQId}), even if it denotes the same type"; - Error(ErrorId.ref_refinement_type_must_match_base, nw.tok, msg); + } else if (neww is TypeSynonymDecl) { + var msg = $"a type synonym ({neww.Name}) is not allowed to replace a {d.WhatKind} from the refined module ({m.RefinementQId}), even if it denotes the same type"; + Error(ErrorId.ref_refinement_type_must_match_base, neww.tok, msg); } else if (!(d is AbstractModuleDecl)) { - Error(ErrorId.ref_refining_notation_needed, nw.tok, $"to redeclare and refine declaration '{d.Name}' from module '{m.RefinementQId}', you must use the refining (`...`) notation"); + Error(ErrorId.ref_refining_notation_needed, neww.tok, $"to redeclare and refine declaration '{d.Name}' from module '{m.RefinementQId}', you must use the refining (`...`) notation"); } } } diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj index e270e4be9d5..a61deb155f0 100644 --- a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj +++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj @@ -12,6 +12,7 @@ + @@ -83,6 +84,9 @@ Always + + PreserveNewest + diff --git a/Source/DafnyLanguageServer.Test/Synchronization/CachingTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/CachingTest.cs new file mode 100644 index 00000000000..a985981eb9d --- /dev/null +++ b/Source/DafnyLanguageServer.Test/Synchronization/CachingTest.cs @@ -0,0 +1,127 @@ +using System.IO; +using System.Linq; +using System.Threading.Tasks; +using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; +using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; +using Microsoft.Extensions.DependencyInjection; +using Microsoft.Extensions.DependencyInjection.Extensions; +using Microsoft.Extensions.Logging; +using OmniSharp.Extensions.LanguageServer.Server; +using Serilog; +using Serilog.Sinks.InMemory; +using Xunit; +using Xunit.Abstractions; + +namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization; + +public class CachingTest : ClientBasedLanguageServerTest { + private InMemorySink sink; + + protected override IServiceCollection ServerOptionsAction(LanguageServerOptions serverOptions) { + sink = InMemorySink.Instance; + var logger = new LoggerConfiguration().MinimumLevel.Debug() + .WriteTo.InMemory().CreateLogger(); + var factory = LoggerFactory.Create(b => b.AddSerilog(logger)); + return base.ServerOptionsAction(serverOptions.WithServices(c => c.Replace(new ServiceDescriptor(typeof(ILoggerFactory), factory)))); + } + + [Fact] + public async Task ParsingIsCachedAndCacheIsPruned() { + var source = @" +include ""./A.dfy"" +include ""./B.dfy"" +module ModC { + lemma Lem() ensures false {} +} +".TrimStart(); + var documentItem = CreateTestDocument(source, Path.Combine(Directory.GetCurrentDirectory(), "Synchronization/TestFiles/test.dfy")); + await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var hits0 = await WaitAndCountHits(); + Assert.Equal(0, hits0); + + async Task WaitAndCountHits() { + await client.WaitForNotificationCompletionAsync(documentItem.Uri, CancellationToken); + return sink.Snapshot().LogEvents.Count(le => le.MessageTemplate.Text.Contains("Parse cache hit")); + } + + ApplyChange(ref documentItem, ((0, 0), (0, 0)), "// Pointless comment that triggers a reparse\n"); + var hitCount1 = await WaitAndCountHits(); + Assert.Equal(2, hitCount1); + + // Removes the comment and the include of B.dfy, which will prune the cache for B.dfy + ApplyChange(ref documentItem, ((2, 0), (3, 0)), ""); + var hitCount2 = await WaitAndCountHits(); + Assert.Equal(hitCount1 + 1, hitCount2); + + ApplyChange(ref documentItem, ((0, 0), (0, 0)), @"include ""./B.dfy""\n"); + var hitCount3 = await WaitAndCountHits(); + // No hit for B.dfy, since it was previously pruned + Assert.Equal(hitCount2 + 1, hitCount3); + } + + /// + /// This test uses a file larger than the chunkSize used by CachingParser when chunking files. + /// + [Fact] + public async Task CachingDetectsStartAndEndAndUriChanges() { + var source = @" +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +// Make the file larger +".TrimStart(); + + var firstFile = CreateTestDocument(source, "firstFile"); + await client.OpenDocumentAndWaitAsync(firstFile, CancellationToken); + + async Task WaitAndCountHits() { + await client.WaitForNotificationCompletionAsync(firstFile.Uri, CancellationToken); + return sink.Snapshot().LogEvents.Count(le => le.MessageTemplate.Text.Contains("Parse cache hit")); + } + + var secondFile = CreateTestDocument(source, "secondFile"); + await client.OpenDocumentAndWaitAsync(secondFile, CancellationToken); + // No hit because Uri has changed + Assert.Equal(0, await WaitAndCountHits()); + + ApplyChange(ref secondFile, ((0, 0), (0, 0)), "// Make the file larger\n"); + // No hit because start of the file has changed + Assert.Equal(0, await WaitAndCountHits()); + + // No hit because end of file has changed + ApplyChange(ref secondFile, ((19, 0), (19, 0)), "// Make the file larger\n"); + Assert.Equal(0, await WaitAndCountHits()); + } + + public CachingTest(ITestOutputHelper output) : base(output) { + } +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer.Test/Synchronization/TestFiles/includesSyntaxError.dfy b/Source/DafnyLanguageServer.Test/Synchronization/TestFiles/includesSyntaxError.dfy new file mode 100644 index 00000000000..cdbf20a6d4d --- /dev/null +++ b/Source/DafnyLanguageServer.Test/Synchronization/TestFiles/includesSyntaxError.dfy @@ -0,0 +1,2 @@ +include "./syntaxError.dfy" +module IncludesSyntaxError {} diff --git a/Source/DafnyLanguageServer.Test/Unit/ByteArrayEqualityTest.cs b/Source/DafnyLanguageServer.Test/Unit/ByteArrayEqualityTest.cs new file mode 100644 index 00000000000..509f942eebe --- /dev/null +++ b/Source/DafnyLanguageServer.Test/Unit/ByteArrayEqualityTest.cs @@ -0,0 +1,27 @@ +using System; +using Microsoft.Dafny.LanguageServer.Language; +using Xunit; + +namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Unit; + +public class ByteArrayEqualityTest { + [Fact] + public void EqualsMethod() { + var oneToSeven = new byte[] { 0, 1, 2, 3, 4, 5, 6, 7 }; + var twoIsThree = new byte[] { 0, 1, 3, 3, 4, 5, 6, 7 }; + var oneToSevenAgain = new byte[] { 0, 1, 2, 3, 4, 5, 6, 7 }; + var equality = new HashEquality(); + Assert.False(equality.Equals(twoIsThree, oneToSeven)); + Assert.True(equality.Equals(oneToSevenAgain, oneToSeven)); + } + + [Fact] + public void TestHashCode() { + var equality = new HashEquality(); + var hashCodeOne = equality.GetHashCode(new byte[] { 1, 0, 0, 0, 1, 1 }); + Assert.Equal(1, hashCodeOne); + + var hashCode2Power24 = equality.GetHashCode(new byte[] { 0, 0, 0, 1, 1, 1, 1 }); + Assert.Equal(Math.Pow(2, 24), hashCode2Power24); + } +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs b/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs index 8d4696b3caf..f2f6c948f76 100644 --- a/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs @@ -2,10 +2,14 @@ using System.Collections.Generic; using Microsoft.Dafny.LanguageServer.Language; using System.IO; +using System.Linq; using Microsoft.Dafny.LanguageServer.Workspace; using Microsoft.Extensions.Logging; +using Moq; using OmniSharp.Extensions.LanguageServer.Protocol; using OmniSharp.Extensions.LanguageServer.Protocol.Models; +using Serilog; +using Serilog.Sinks.InMemory; using Xunit; using Xunit.Abstractions; @@ -16,11 +20,16 @@ public class ParserExceptionTest { private const string LanguageId = "dafny"; private const int MaxTestExecutionTimeMs = 10_000; private DafnyLangParser parser; - private LastDebugLogger lastDebugLogger; + private readonly InMemorySink sink; public ParserExceptionTest(ITestOutputHelper output) { - lastDebugLogger = new LastDebugLogger(); - parser = DafnyLangParser.Create(DafnyOptions.Create(new WriterFromOutputHelper(output)), lastDebugLogger); + + sink = InMemorySink.Instance; + var logger = new LoggerConfiguration().MinimumLevel.Debug() + .WriteTo.InMemory().CreateLogger(); + var factory = LoggerFactory.Create(b => b.AddSerilog(logger)); + + parser = DafnyLangParser.Create(DafnyOptions.Create(new WriterFromOutputHelper(output)), Mock.Of(), factory); } [Fact(Timeout = MaxTestExecutionTimeMs)] @@ -31,6 +40,7 @@ public void DocumentWithParserExceptionDisplaysIt() { var uri = new Uri("file:///" + TestFilePath); var errorReporter = new ParserExceptionSimulatingErrorReporter(options); parser.Parse(new DocumentTextBuffer(documentItem), errorReporter, default); + Assert.Contains(sink.LogEvents, le => le.MessageTemplate.Text.Contains($"encountered an exception while parsing {uri}")); Assert.Equal($"/{TestFilePath}(1,0): Error: [internal error] Parser exception: Simulated parser internal error", errorReporter.LastMessage); } @@ -66,33 +76,6 @@ public ParserExceptionSimulatingErrorReporter(DafnyOptions options) : base(optio } } - // Helpers and definitions - - /// - /// Retains the last debug logged message - /// - private class LastDebugLogger : ILogger { - public string LastDebugMessage = ""; - public void Log(LogLevel logLevel, EventId eventId, TState state, Exception exception, Func formatter) { - if (logLevel is LogLevel.Debug) { - LastDebugMessage = formatter(state, exception); - return; - } - if (logLevel is LogLevel.Trace or LogLevel.Information or LogLevel.Warning) { - return; - } - throw new NotImplementedException(); - } - - public bool IsEnabled(LogLevel logLevel) { - return true; - } - - public IDisposable BeginScope(TState state) { - throw new NotImplementedException(); - } - } - private static TextDocumentItem CreateTestDocument(string source, string filePath, int version = 1) { return new TextDocumentItem { LanguageId = LanguageId, diff --git a/Source/DafnyLanguageServer.Test/Unit/TextReaderFromCharArraysTest.cs b/Source/DafnyLanguageServer.Test/Unit/TextReaderFromCharArraysTest.cs new file mode 100644 index 00000000000..4049b445c23 --- /dev/null +++ b/Source/DafnyLanguageServer.Test/Unit/TextReaderFromCharArraysTest.cs @@ -0,0 +1,61 @@ +using System.Linq; +using Microsoft.Dafny.LanguageServer.Language; +using Xunit; + +namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Unit; + +public class TextReaderFromCharArraysTest { + + [Fact] + public void ReadBlockEmptyMiddle() { + var fourAs = new[] { 'a', 'a', 'a', 'a' }; + var chunks = new[] { fourAs, new char[] { }, fourAs }; + var emptyMiddleReader = new TextReaderFromCharArrays(chunks); + var end = emptyMiddleReader.ReadToEnd(); + Assert.Equal("aaaaaaaa", end); + } + + [Fact] + public void ReadPeekEmptyStart() { + var emptyStart = new[] { new char[] { }, new[] { 'a', 'b', 'c', 'd' } }; + var emptyStartReader = new TextReaderFromCharArrays(emptyStart); + var firstPeek = emptyStartReader.Peek(); + var firstRead = emptyStartReader.Read(); + Assert.Equal('a', firstPeek); + Assert.Equal('a', firstRead); + } + + [Fact] + public void ReadEmptyMiddle() { + var emptyMiddleReader = new TextReaderFromCharArrays(new[] { new[] { 'a' }, new char[] { }, new[] { 'b' } }); + var a = emptyMiddleReader.Read(); + var b = emptyMiddleReader.Read(); + Assert.Equal('a', a); + Assert.Equal('b', b); + } + + [Fact] + public void ReadMoreThanContent() { + var abcd = new[] { 'a', 'b', 'c', 'd' }; + var chunks = new[] { abcd, abcd }; + var reader = new TextReaderFromCharArrays(chunks); + var buffer = new char[1024]; + var readCount = reader.Read(buffer, 0, buffer.Length); + Assert.Equal(8, readCount); + Assert.Equal("abcdabcd", new string(buffer.Take(8).ToArray())); + } + + [Fact] + public void ReadPerChar() { + var ab = new[] { 'a', 'b' }; + var chunks = new[] { ab }; + var reader = new TextReaderFromCharArrays(chunks); + var first = reader.Read(); + var second = reader.Read(); + var third = reader.Read(); + + Assert.Equal('a', first); + Assert.Equal('b', second); + Assert.Equal(-1, third); + } +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer.Test/Various/IncludeFileTest.cs b/Source/DafnyLanguageServer.Test/Various/IncludeFileTest.cs index 36c1753d747..a15cc544779 100644 --- a/Source/DafnyLanguageServer.Test/Various/IncludeFileTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/IncludeFileTest.cs @@ -1,5 +1,6 @@ using System; using System.IO; +using System.Threading; using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; @@ -10,6 +11,32 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; public class IncludeFileTest : ClientBasedLanguageServerTest { + [Fact] + public async Task DirectlyIncludedFileFails() { + var source = @" +include ""./syntaxError.dfy"" +".TrimStart(); + var documentItem = CreateTestDocument(source, Path.Combine(Directory.GetCurrentDirectory(), "Synchronization/TestFiles/test.dfy")); + await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + Assert.Single(diagnostics); + Assert.Contains("the included file", diagnostics[0].Message); + Assert.Contains("syntaxError.dfy", diagnostics[0].Message); + } + + [Fact] + public async Task IndirectlyIncludedFileFails() { + var source = @" +include ""./includesSyntaxError.dfy"" +".TrimStart(); + var documentItem = CreateTestDocument(source, Path.Combine(Directory.GetCurrentDirectory(), "Synchronization/TestFiles/test.dfy")); + await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + Assert.Single(diagnostics); + Assert.Contains("the included file", diagnostics[0].Message); + Assert.Contains("syntaxError.dfy", diagnostics[0].Message); + } + [Fact] public async Task MutuallyRecursiveIncludes() { string rootFile = Path.Combine(Directory.GetCurrentDirectory(), "Various", "TestFiles", "includesBincludesA.dfy"); diff --git a/Source/DafnyLanguageServer/Caching/HashEquality.cs b/Source/DafnyLanguageServer/Caching/HashEquality.cs new file mode 100644 index 00000000000..05e6f3e54a7 --- /dev/null +++ b/Source/DafnyLanguageServer/Caching/HashEquality.cs @@ -0,0 +1,32 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Security.Policy; + +namespace Microsoft.Dafny.LanguageServer.Language; + +/// +/// Useful for using hashes as keys in dictionaries +/// +public class HashEquality : IEqualityComparer { + public bool Equals(byte[]? x, byte[]? y) { + return (x, y) switch { + (null, null) => true, + (null, _) => false, + (_, null) => false, + _ => x.SequenceEqual(y) + }; + } + + /// + /// Since the bytes themselves are already a hash, + /// we don't expect ot gain a benefit from hashing those bytes into 32 bits + /// over simply taking the first 32 bits of the original hash. + /// + public int GetHashCode(byte[] obj) { + if (obj.Length == 0) { + return 0; + } + return BitConverter.ToInt32(obj, 0); + } +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer/Caching/PruneIfNotUsedSinceLastPruneCache.cs b/Source/DafnyLanguageServer/Caching/PruneIfNotUsedSinceLastPruneCache.cs new file mode 100644 index 00000000000..2f2598d2ea6 --- /dev/null +++ b/Source/DafnyLanguageServer/Caching/PruneIfNotUsedSinceLastPruneCache.cs @@ -0,0 +1,54 @@ +using System; +using System.Collections.Concurrent; +using System.Collections.Generic; +using System.Linq; + +namespace Microsoft.Dafny; + +public class PruneIfNotUsedSinceLastPruneCache + where TValue : class + where TKey : notnull { + class Item { + public Item(TValue value) { + Value = value; + Accessed = true; + } + + public bool Accessed { get; set; } + public TValue Value { get; } + } + + private readonly ConcurrentDictionary items; + + public PruneIfNotUsedSinceLastPruneCache(IEqualityComparer comparer) { + items = new(comparer); + } + + public void Prune() { + var keys = items.Keys.ToList(); + foreach (var key in keys) { + var item = items[key]; + if (!item.Accessed) { + items.TryRemove(key, out _); + } + + item.Accessed = false; + } + } + + public void Set(TKey key, TValue value) { + items.TryAdd(key, new Item(value)); + } + + public bool TryGet(TKey key, out TValue? value) { + var result = items.TryGetValue(key, out var item); + if (result) { + value = item!.Value; + item.Accessed = true; + } else { + value = null; + } + + return result; + } +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer/Caching/TextReaderFromCharArrays.cs b/Source/DafnyLanguageServer/Caching/TextReaderFromCharArrays.cs new file mode 100644 index 00000000000..843f23bd099 --- /dev/null +++ b/Source/DafnyLanguageServer/Caching/TextReaderFromCharArrays.cs @@ -0,0 +1,80 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Text; +using System.Threading.Tasks.Dataflow; + +namespace Microsoft.Dafny.LanguageServer.Language; + +public class TextReaderFromCharArrays : TextReader { + private readonly IReadOnlyList arrays; + private int arrayIndex; + private int elementIndex; + + public TextReaderFromCharArrays(IReadOnlyList arrays) { + this.arrays = arrays; + UpdateIndices(); + } + + public string Text { + get { + var size = arrays.Sum(a => a.Length); + var result = new char[size]; + var offset = 0; + foreach (var array in arrays) { + Array.Copy(array, 0, result, offset, array.Length); + offset += array.Length; + } + return new string(result); + } + } + + public override int Peek() { + if (arrayIndex == arrays.Count) { + return -1; + } + var array = arrays[arrayIndex]; + if (elementIndex == array.Length) { + return -1; + } + return array[elementIndex]; + } + + public override int Read() { + if (arrayIndex == arrays.Count) { + return -1; + } + + var array = arrays[arrayIndex]; + if (elementIndex == array.Length) { + return -1; + } + var result = array[elementIndex++]; + UpdateIndices(); + return result; + } + + public override int Read(char[] buffer, int index, int count) { + var remainingCount = count; + while (remainingCount > 0 && arrayIndex < arrays.Count) { + var currentArray = arrays[arrayIndex]; + var currentRemainder = currentArray.Length - elementIndex; + var readCount = Math.Min(currentRemainder, remainingCount); + Array.Copy(currentArray, elementIndex, buffer, index, readCount); + elementIndex += readCount; + index += readCount; + remainingCount -= readCount; + UpdateIndices(); + } + + return count - remainingCount; + } + + private void UpdateIndices() { + while (arrayIndex < arrays.Count && elementIndex == arrays[arrayIndex].Length) { + arrayIndex++; + elementIndex = 0; + } + } +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs index 4fd55561390..0c1121e7a4a 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs @@ -235,7 +235,7 @@ string GetDescription(Boogie.ProofObligationDescription? description) { string information = ""; - string CouldProveOrNotPrefix = (assertionNode?.StatusVerification) switch { + string couldProveOrNotPrefix = (assertionNode?.StatusVerification) switch { GutterVerificationStatus.Verified => "Did prove: ", GutterVerificationStatus.Error => "Could not prove: ", GutterVerificationStatus.Inconclusive => "Not able to prove: ", @@ -257,7 +257,7 @@ string MoreInformation(Boogie.IToken? token, bool hoveringPostcondition) { // however, nested postconditions should be displayed if (errorToken is BoogieRangeToken rangeToken && !hoveringPostcondition) { var originalText = rangeToken.PrintOriginal(); - deltaInformation += " \n" + CouldProveOrNotPrefix + originalText; + deltaInformation += " \n" + couldProveOrNotPrefix + originalText; } hoveringPostcondition = false; diff --git a/Source/DafnyLanguageServer/Language/CachingParser.cs b/Source/DafnyLanguageServer/Language/CachingParser.cs new file mode 100644 index 00000000000..e57fa0f6b3b --- /dev/null +++ b/Source/DafnyLanguageServer/Language/CachingParser.cs @@ -0,0 +1,70 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Security.Cryptography; +using System.Security.Policy; +using System.Text; +using Microsoft.Extensions.Logging; + +namespace Microsoft.Dafny.LanguageServer.Language; + +public class CachingParser : ProgramParser { + private readonly PruneIfNotUsedSinceLastPruneCache parseCache = new(new HashEquality()); + + public CachingParser(ILogger logger) : base(logger) { + } + + public void Prune() { + parseCache.Prune(); + } + + protected override DfyParseResult ParseFile(DafnyOptions options, TextReader reader, Uri uri) { + var (newReader, hash) = ComputeHashFromReader(uri, reader, HashAlgorithm.Create("SHA256")!); + if (!parseCache.TryGet(hash, out var result)) { + logger.LogDebug($"Parse cache miss for {uri}"); + result = base.ParseFile(options, newReader, uri); + parseCache.Set(hash, result); + } else { + logger.LogDebug($"Parse cache hit for {uri}"); + } + + // Clone declarations before returning them, since they are mutable and we don't want to mutate the one in the cache. + // We should cache an immutable version of the AST instead: https://github.com/dafny-lang/dafny/issues/4086 + var cloner = new Cloner(true, false); + var clonedResult = result! with { + Module = new FileModuleDefinition(cloner, result.Module) + }; + return clonedResult; + } + + /// + /// We read the contents of the reader and store them in memory using chunks + /// to prevent allocating a large array of memory. + /// + private static (TextReader reader, byte[] hash) ComputeHashFromReader(Uri uri, TextReader reader, HashAlgorithm hashAlgorithm) { + var result = new List(); + const int chunkSize = 1024; + hashAlgorithm.Initialize(); + // Add NUL delimiter to avoid collisions (otherwise hash("A" + "BC") == hash("AB" + "C")) + var uriBytes = Encoding.UTF8.GetBytes(uri.ToString() + "\0"); + + // We need to include the uri as part of the hash, because the parsed AST contains tokens that refer to the filename. + hashAlgorithm.TransformBlock(uriBytes, 0, uriBytes.Length, null, 0); + while (true) { + var chunk = new char[chunkSize]; + var readCount = reader.ReadBlock(chunk, 0, chunk.Length); + if (readCount < chunk.Length) { + var shortenedChunk = new char[readCount]; + Array.Copy(chunk, 0, shortenedChunk, 0, readCount); + result.Add(shortenedChunk); + var charArray = Encoding.UTF8.GetBytes(shortenedChunk); + hashAlgorithm.TransformFinalBlock(charArray, 0, charArray.Length); + return (new TextReaderFromCharArrays(result), hashAlgorithm.Hash!); + } else { + var charArray = Encoding.UTF8.GetBytes(chunk); + hashAlgorithm.TransformBlock(charArray, 0, charArray.Length, null, 0); + } + result.Add(chunk); + } + } +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs index 958d4e249e7..360469eef54 100644 --- a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs +++ b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs @@ -1,14 +1,11 @@ -using Microsoft.Dafny.LanguageServer.Util; -using Microsoft.Extensions.Logging; +using Microsoft.Extensions.Logging; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System; using System.Collections.Generic; -using System.IO; -using System.Linq; using System.Threading; -using Microsoft.Boogie; using Microsoft.Dafny.LanguageServer.Workspace; -using OmniSharp.Extensions.LanguageServer.Protocol; +using OmniSharp.Extensions.LanguageServer.Protocol.Server; +using OmniSharp.Extensions.LanguageServer.Protocol.Window; namespace Microsoft.Dafny.LanguageServer.Language { /// @@ -21,12 +18,16 @@ namespace Microsoft.Dafny.LanguageServer.Language { /// public sealed class DafnyLangParser : IDafnyParser, IDisposable { private readonly DafnyOptions options; + private readonly ITelemetryPublisher telemetryPublisher; private readonly ILogger logger; private readonly SemaphoreSlim mutex = new(1); + private readonly CachingParser cachingParser; - private DafnyLangParser(DafnyOptions options, ILogger logger) { + private DafnyLangParser(DafnyOptions options, ITelemetryPublisher telemetryPublisher, ILoggerFactory loggerFactory) { this.options = options; - this.logger = logger; + this.telemetryPublisher = telemetryPublisher; + logger = loggerFactory.CreateLogger(); + cachingParser = new CachingParser(loggerFactory.CreateLogger()); } /// @@ -34,8 +35,8 @@ private DafnyLangParser(DafnyOptions options, ILogger logger) { /// /// A logger instance that may be used by this parser instance. /// A safely created dafny parser instance. - public static DafnyLangParser Create(DafnyOptions options, ILogger logger) { - return new DafnyLangParser(options, logger); + public static DafnyLangParser Create(DafnyOptions options, ITelemetryPublisher telemetryPublisher, ILoggerFactory loggerFactory) { + return new DafnyLangParser(options, telemetryPublisher, loggerFactory); } public Dafny.Program CreateUnparsed(TextDocumentItem document, ErrorReporter errorReporter, CancellationToken cancellationToken) { @@ -52,19 +53,23 @@ public Dafny.Program Parse(DocumentTextBuffer document, ErrorReporter errorRepor mutex.Wait(cancellationToken); try { - return ParseUtils.ParseFiles(document.Uri.ToString(), + var beforeParsing = DateTime.Now; + var result = cachingParser.ParseFiles(document.Uri.ToString(), new DafnyFile[] { new(errorReporter.Options, document.Uri.ToUri(), document.Content) }, errorReporter, cancellationToken); + telemetryPublisher.PublishTime("Parse", document.Uri.ToString(), DateTime.Now - beforeParsing); + return result; } finally { + cachingParser.Prune(); mutex.Release(); } } - private Dafny.Program NewDafnyProgram(TextDocumentItem document, ErrorReporter errorReporter) { + private static Dafny.Program NewDafnyProgram(TextDocumentItem document, ErrorReporter errorReporter) { // Ensure that the statically kept scopes are empty when parsing a new document. Type.ResetScopes(); return new Dafny.Program( diff --git a/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs b/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs index 5a8029ace2f..95413e87458 100644 --- a/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs +++ b/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs @@ -28,7 +28,8 @@ private static IServiceCollection WithDafnyLanguage(this IServiceCollection serv return services .AddSingleton(serviceProvider => DafnyLangParser.Create( serviceProvider.GetRequiredService(), - serviceProvider.GetRequiredService>())) + serviceProvider.GetRequiredService(), + serviceProvider.GetRequiredService())) .AddSingleton() .AddSingleton(CreateVerifier) .AddSingleton() diff --git a/Source/DafnyLanguageServer/Workspace/ITelemetryPublisher.cs b/Source/DafnyLanguageServer/Workspace/ITelemetryPublisher.cs index fac20b59671..ec0f504f6a8 100644 --- a/Source/DafnyLanguageServer/Workspace/ITelemetryPublisher.cs +++ b/Source/DafnyLanguageServer/Workspace/ITelemetryPublisher.cs @@ -1,4 +1,5 @@ using System; +using System.Collections.Immutable; using Microsoft.Dafny.LanguageServer.Language; using Microsoft.Extensions.Logging; using OmniSharp.Extensions.LanguageServer.Protocol.Models; @@ -13,15 +14,15 @@ protected enum TelemetryEventKind { UpdateComplete, UnhandledException, SolverPath, - Z3Version + Z3Version, + Time } - /// - /// Publish a telemetry event. - /// - /// The kind of this telemetry event. - /// The payload of this telemetry event. - protected void PublishTelemetry(TelemetryEventKind kind, object? payload); + protected void PublishTelemetry(TelemetryEventKind kind, object? payload) { + PublishTelemetry(kind.ToString(), ImmutableDictionary.Create().Add("payload", payload!)); + } + + protected void PublishTelemetry(string kind, ImmutableDictionary payload); /// /// Signal the completion of a document update. @@ -39,6 +40,11 @@ public void PublishSolverPath(string solverPath) { PublishTelemetry(TelemetryEventKind.SolverPath, solverPath); } + public void PublishTime(string activity, string resource, TimeSpan span) { + PublishTelemetry(TelemetryEventKind.Time, ImmutableDictionary.Create(). + Add("activity", activity).Add("resource", resource).Add("time", span.TotalMilliseconds)); + } + public void PublishZ3Version(string z3Version) { PublishTelemetry(TelemetryEventKind.Z3Version, z3Version); } diff --git a/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs b/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs index 948d4606c87..ee490f6a057 100644 --- a/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs +++ b/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs @@ -29,7 +29,8 @@ private static IServiceCollection WithDafnyWorkspace(this IServiceCollection ser .AddSingleton(serviceProvider => { var options = serviceProvider.GetRequiredService(); return DafnyLangParser.Create(options, - serviceProvider.GetRequiredService>()); + serviceProvider.GetRequiredService(), + serviceProvider.GetRequiredService()); }) .AddSingleton(CreateTextDocumentLoader) .AddSingleton() diff --git a/Source/DafnyLanguageServer/Workspace/TelemetryPublisher.cs b/Source/DafnyLanguageServer/Workspace/TelemetryPublisher.cs index 8903d51df87..928a558a26d 100644 --- a/Source/DafnyLanguageServer/Workspace/TelemetryPublisher.cs +++ b/Source/DafnyLanguageServer/Workspace/TelemetryPublisher.cs @@ -1,11 +1,7 @@ using System; -using Microsoft.Dafny.LanguageServer.Util; -using Microsoft.Dafny.LanguageServer.Workspace.Notifications; -using OmniSharp.Extensions.LanguageServer.Protocol.Document; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using OmniSharp.Extensions.LanguageServer.Protocol.Server; -using System.Collections.Generic; -using System.Linq; +using System.Collections.Immutable; using Microsoft.Extensions.Logging; using OmniSharp.Extensions.LanguageServer.Protocol.Window; @@ -21,19 +17,14 @@ public TelemetryPublisher(ILanguageServerFacade languageServer, ILogger().Add("payload", e.ToString())); } - void ITelemetryPublisher.PublishTelemetry(ITelemetryPublisher.TelemetryEventKind kind, object? payload) { - PublishTelemetry(kind, payload); - } - - private void PublishTelemetry(ITelemetryPublisher.TelemetryEventKind kind, object? payload) { + public void PublishTelemetry(string kind, ImmutableDictionary payload) { + var data = payload.Add("kind", kind); languageServer.Window.SendTelemetryEvent(new TelemetryEventParams { - ExtensionData = new Dictionary { - {"kind", kind.ToString()}, - {"payload", payload ?? new Dictionary()} - } + ExtensionData = data }); } } diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index c4faf0d1373..2f1334673e9 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -66,7 +66,8 @@ public IdeState CreateUnloaded(DocumentTextBuffer textDocument, CancellationToke // This diagnostic never gets sent to the client, // instead it forces the first computed diagnostics for a document to always be sent. // The message here describes the implicit client state before the first diagnostics have been sent. - Message = "Resolution diagnostics have not been computed yet." + Message = "Resolution diagnostics have not been computed yet.", + Range = new OmniSharp.Extensions.LanguageServer.Protocol.Models.Range(0, 0, 0,0) }} ); } diff --git a/Source/DafnyPipeline.Test/FormatterBaseTest.cs b/Source/DafnyPipeline.Test/FormatterBaseTest.cs index bae70c73ef9..44b167e1c80 100644 --- a/Source/DafnyPipeline.Test/FormatterBaseTest.cs +++ b/Source/DafnyPipeline.Test/FormatterBaseTest.cs @@ -7,6 +7,8 @@ using Bpl = Microsoft.Boogie; using BplParser = Microsoft.Boogie.Parser; using Microsoft.Dafny; +using Microsoft.Extensions.Logging; +using Microsoft.Extensions.Logging.Abstractions; using Xunit; using Xunit.Abstractions; @@ -58,7 +60,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString var reporter = new BatchErrorReporter(options); Microsoft.Dafny.Type.ResetScopes(); - var dafnyProgram = ParseUtils.Parse(programNotIndented, uri, reporter); + var dafnyProgram = new ProgramParser().Parse(programNotIndented, uri, reporter); if (reporter.ErrorCount > 0) { var error = reporter.AllMessagesByLevel[ErrorLevel.Error][0]; @@ -95,7 +97,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString // Verify that the formatting is stable. Microsoft.Dafny.Type.ResetScopes(); var newReporter = new BatchErrorReporter(options); - dafnyProgram = ParseUtils.Parse(reprinted, uri, newReporter); ; + dafnyProgram = new ProgramParser().Parse(reprinted, uri, newReporter); ; Assert.Equal(initErrorCount, reporter.ErrorCount + newReporter.ErrorCount); firstToken = dafnyProgram.GetFirstTopLevelToken(); diff --git a/Source/DafnyPipeline.Test/TranslatorTest.cs b/Source/DafnyPipeline.Test/TranslatorTest.cs index 747d8baffa1..a06b558ac10 100644 --- a/Source/DafnyPipeline.Test/TranslatorTest.cs +++ b/Source/DafnyPipeline.Test/TranslatorTest.cs @@ -6,6 +6,8 @@ using Xunit; using Microsoft.Dafny; using Microsoft.Dafny.ProofObligationDescription; +using Microsoft.Extensions.Logging; +using Microsoft.Extensions.Logging.Abstractions; namespace DafnyPipeline.Test; @@ -76,7 +78,7 @@ private void ShouldHaveImplicitCode(string program, string expected, DafnyOption options = options ?? new DafnyOptions(TextReader.Null, TextWriter.Null, TextWriter.Null); var uri = new Uri("virtual:///virtual"); BatchErrorReporter reporter = new BatchErrorReporter(options); - var dafnyProgram = ParseUtils.Parse(program, uri, reporter); + var dafnyProgram = new ProgramParser().Parse(program, uri, reporter); if (reporter.ErrorCount > 0) { var error = reporter.AllMessagesByLevel[ErrorLevel.Error][0]; Assert.False(true, $"{error.Message}: line {error.Token.line} col {error.Token.col}"); diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index d09a242aadc..59cd5eb2908 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -10,6 +10,8 @@ using System.Threading; using Microsoft.Boogie; using DafnyServer; +using Microsoft.Extensions.Logging; +using Microsoft.Extensions.Logging.Abstractions; using Bpl = Microsoft.Boogie; namespace Microsoft.Dafny { @@ -42,7 +44,7 @@ public bool Verify() { private bool Parse() { var uri = new Uri("transcript:///" + fname); reporter = new ConsoleErrorReporter(options); - var program = ParseUtils.ParseFiles(fname, new DafnyFile[] { new(reporter.Options, uri, new StringReader(source)) }, + var program = new ProgramParser().ParseFiles(fname, new DafnyFile[] { new(reporter.Options, uri, new StringReader(source)) }, reporter, CancellationToken.None); var success = reporter.ErrorCount == 0; diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs index e9491d8fd80..e8bc42f3068 100644 --- a/Source/DafnyTestGeneration/Utils.cs +++ b/Source/DafnyTestGeneration/Utils.cs @@ -7,6 +7,8 @@ using DafnyServer.CounterexampleGeneration; using Microsoft.Boogie; using Microsoft.Dafny; +using Microsoft.Extensions.Logging; +using Microsoft.Extensions.Logging.Abstractions; using Errors = Microsoft.Dafny.Errors; using Function = Microsoft.Dafny.Function; using Parser = Microsoft.Dafny.Parser; @@ -80,7 +82,7 @@ public static Type CopyWithReplacements(Type type, List from, List uri ??= new Uri(Path.GetTempPath()); var reporter = new BatchErrorReporter(options); - var program = ParseUtils.ParseFiles(uri.LocalPath, new DafnyFile[] { new(reporter.Options, uri, new StringReader(source)) }, + var program = new ProgramParser().ParseFiles(uri.LocalPath, new DafnyFile[] { new(reporter.Options, uri, new StringReader(source)) }, reporter, CancellationToken.None); if (!resolve) { diff --git a/docs/dev/news/4083.feat b/docs/dev/news/4083.feat new file mode 100644 index 00000000000..2f522e09c09 --- /dev/null +++ b/docs/dev/news/4083.feat @@ -0,0 +1 @@ +When using the Dafny CLI, error messages of the form "the included file contains error(s)" are no longer reported, since the actual errors for these included files are shown as well. When using the Dafny server, errors like these are still shown, since the Dafny server only shows errors for currently opened files. In addition, such errors are now also shown for files that are indirectly included by an opened file. \ No newline at end of file diff --git a/docs/dev/news/4085.feat b/docs/dev/news/4085.feat new file mode 100644 index 00000000000..14a5c1778a1 --- /dev/null +++ b/docs/dev/news/4085.feat @@ -0,0 +1 @@ +When using the Dafny IDE, parsing is now cached in order to improve performance when making changes in multi-file projects.