diff --git a/.github/workflows/integration-tests-reusable.yml b/.github/workflows/integration-tests-reusable.yml index d9577e18813..803e8e3f37d 100644 --- a/.github/workflows/integration-tests-reusable.yml +++ b/.github/workflows/integration-tests-reusable.yml @@ -53,6 +53,7 @@ jobs: shard-list: ${{ steps.populate-shard-list.outputs.shard-list }} test: needs: populate-matrix-dimensions + timeout-minutes: 120 runs-on: ${{ matrix.os }} strategy: matrix: diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs index 8471cc0c43e..1fb46b2f3ea 100644 --- a/Source/DafnyCore/AST/Cloner.cs +++ b/Source/DafnyCore/AST/Cloner.cs @@ -232,9 +232,8 @@ public virtual Type CloneType(Type t) { } else if (t is MultiSetType) { var tt = (MultiSetType)t; 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)); + } else if (t is MapType mapType) { + return new MapType(this, mapType); } else if (t is ArrowType) { var tt = (ArrowType)t; return new ArrowType(Tok(tt.tok), tt.Args.ConvertAll(CloneType), CloneType(tt.Result)); diff --git a/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs b/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs index a654097ed53..0fe8374904f 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs @@ -1,5 +1,6 @@ using System; using System.Diagnostics.Contracts; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -86,7 +87,7 @@ public string AssignUniqueName(FreshIdGenerator generator) { } public abstract IToken NameToken { get; } - public DafnySymbolKind Kind => throw new NotImplementedException(); + public SymbolKind Kind => throw new NotImplementedException(); public string GetDescription(DafnyOptions options) { throw new NotImplementedException(); } diff --git a/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs b/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs index 754a03ded0e..f81d643d644 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs @@ -1,6 +1,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -134,7 +135,7 @@ public NonglobalVariable(IToken tok, string name, Type type, bool isGhost) { public IToken NameToken => tok; public override IEnumerable Children => IsTypeExplicit ? new List { Type } : Enumerable.Empty(); public override IEnumerable PreResolveChildren => IsTypeExplicit ? new List() { Type } : Enumerable.Empty(); - public DafnySymbolKind Kind => DafnySymbolKind.Variable; + public SymbolKind Kind => SymbolKind.Variable; public string GetDescription(DafnyOptions options) { return this.AsText(); } diff --git a/Source/DafnyCore/AST/Grammar/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer.cs index b40650701e7..5e8b2ec17c6 100644 --- a/Source/DafnyCore/AST/Grammar/Printer.cs +++ b/Source/DafnyCore/AST/Grammar/Printer.cs @@ -191,7 +191,9 @@ public static string ToStringWithoutNewline(System.IO.StringWriter wr) { } public void PrintProgramLargeStack(Program prog, bool afterResolver) { +#pragma warning disable VSTHRD002 DafnyMain.LargeStackFactory.StartNew(() => PrintProgram(prog, afterResolver)).Wait(); +#pragma warning restore VSTHRD002 } public void PrintProgram(Program prog, bool afterResolver) { diff --git a/Source/DafnyCore/AST/IHasUsages.cs b/Source/DafnyCore/AST/IHasUsages.cs index 982b55b01d2..090d2d39227 100644 --- a/Source/DafnyCore/AST/IHasUsages.cs +++ b/Source/DafnyCore/AST/IHasUsages.cs @@ -1,6 +1,7 @@ using System; using System.Collections.Generic; using System.Linq; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -53,7 +54,7 @@ public static string AsText(this IVariable variable) { } public interface ISymbol : IDeclarationOrUsage { - DafnySymbolKind Kind { get; } + SymbolKind Kind { get; } string GetDescription(DafnyOptions options); } @@ -79,38 +80,4 @@ public static ISet GetSymbolDescendants(ISymbol node) { } return result; } -} - -/// -/// This is a copy of OmniSharp.Extensions.LanguageServer.Protocol.Models.SymbolKind -/// In the future, we'll include that package in this project, and then this copy can be removed. -/// For now, adding that package reference is not worth its weight. -/// -public enum DafnySymbolKind { - File = 1, - Module = 2, - Namespace = 3, - Package = 4, - Class = 5, - Method = 6, - Property = 7, - Field = 8, - Constructor = 9, - Enum = 10, - Interface = 11, - Function = 12, - Variable = 13, - Constant = 14, - String = 15, - Number = 16, - Boolean = 17, - Array = 18, - Object = 19, - Key = 20, - Null = 21, - EnumMember = 22, - Struct = 23, - Event = 24, - Operator = 25, - TypeParameter = 26, } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Members/ConstantField.cs b/Source/DafnyCore/AST/Members/ConstantField.cs index c63e26d7de7..efc8668ad24 100644 --- a/Source/DafnyCore/AST/Members/ConstantField.cs +++ b/Source/DafnyCore/AST/Members/ConstantField.cs @@ -1,6 +1,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -46,7 +47,7 @@ public bool InferredDecreases { public bool AllowsAllocation => true; public override IEnumerable Children => base.Children.Concat(new[] { Rhs }.Where(x => x != null)); - public override DafnySymbolKind Kind => DafnySymbolKind.Constant; + public override SymbolKind Kind => SymbolKind.Constant; public override IEnumerable PreResolveChildren => Children; public ModuleDefinition ContainingModule => EnclosingModule; diff --git a/Source/DafnyCore/AST/Members/Constructor.cs b/Source/DafnyCore/AST/Members/Constructor.cs index 1a1d8093b85..7c8b2b7bb4e 100644 --- a/Source/DafnyCore/AST/Members/Constructor.cs +++ b/Source/DafnyCore/AST/Members/Constructor.cs @@ -1,5 +1,6 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -10,7 +11,7 @@ void ObjectInvariant() { Contract.Invariant(Body == null || Body is DividedBlockStmt); } - public override DafnySymbolKind Kind => DafnySymbolKind.Constructor; + public override SymbolKind Kind => SymbolKind.Constructor; protected override string GetQualifiedName() { return EnclosingClass.Name; } diff --git a/Source/DafnyCore/AST/Members/Field.cs b/Source/DafnyCore/AST/Members/Field.cs index c764d3279b8..eaf9aa29b1a 100644 --- a/Source/DafnyCore/AST/Members/Field.cs +++ b/Source/DafnyCore/AST/Members/Field.cs @@ -1,6 +1,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -95,7 +96,7 @@ public string GetTriviaContainingDocstring() { return GetTriviaContainingDocstringFromStartTokenOrNull(); } - public virtual DafnySymbolKind Kind => DafnySymbolKind.Field; + public virtual SymbolKind Kind => SymbolKind.Field; public string GetDescription(DafnyOptions options) { var prefix = IsMutable ? "var" : "const"; diff --git a/Source/DafnyCore/AST/Members/Function.cs b/Source/DafnyCore/AST/Members/Function.cs index 8eab61f6026..b60826f0862 100644 --- a/Source/DafnyCore/AST/Members/Function.cs +++ b/Source/DafnyCore/AST/Members/Function.cs @@ -5,6 +5,7 @@ using System.Numerics; using DafnyCore; using Microsoft.Dafny.Auditor; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -485,7 +486,7 @@ public string GetTriviaContainingDocstring() { return null; } - public DafnySymbolKind Kind => DafnySymbolKind.Function; + public SymbolKind Kind => SymbolKind.Function; public bool ShouldVerify => true; // This could be made more accurate public ModuleDefinition ContainingModule => EnclosingClass.EnclosingModuleDefinition; public string GetDescription(DafnyOptions options) { diff --git a/Source/DafnyCore/AST/Members/ICodeContext.cs b/Source/DafnyCore/AST/Members/ICodeContext.cs index 3515cb202a8..14d97610a87 100644 --- a/Source/DafnyCore/AST/Members/ICodeContext.cs +++ b/Source/DafnyCore/AST/Members/ICodeContext.cs @@ -1,5 +1,6 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -93,7 +94,7 @@ public bool InferredDecreases { public IEnumerable OwnedTokens => CwInner.OwnedTokens; public RangeToken RangeToken => CwInner.RangeToken; public IToken NameToken => CwInner.NameToken; - public DafnySymbolKind Kind => CwInner.Kind; + public SymbolKind Kind => CwInner.Kind; public string GetDescription(DafnyOptions options) { return CwInner.GetDescription(options); } @@ -127,7 +128,7 @@ public IEnumerable GetConcreteChildren() { public IEnumerable OwnedTokens => throw new cce.UnreachableException(); public RangeToken RangeToken => throw new cce.UnreachableException(); public IToken NameToken => throw new cce.UnreachableException(); - public DafnySymbolKind Kind => throw new cce.UnreachableException(); + public SymbolKind Kind => throw new cce.UnreachableException(); public string GetDescription(DafnyOptions options) { throw new cce.UnreachableException(); } diff --git a/Source/DafnyCore/AST/Members/Method.cs b/Source/DafnyCore/AST/Members/Method.cs index 2211521f03a..c35679b5b90 100644 --- a/Source/DafnyCore/AST/Members/Method.cs +++ b/Source/DafnyCore/AST/Members/Method.cs @@ -3,6 +3,7 @@ using System.Linq; using System.Numerics; using Microsoft.Dafny.Auditor; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -388,7 +389,7 @@ public string GetTriviaContainingDocstring() { return GetTriviaContainingDocstringFromStartTokenOrNull(); } - public virtual DafnySymbolKind Kind => DafnySymbolKind.Method; + public virtual SymbolKind Kind => SymbolKind.Method; public string GetDescription(DafnyOptions options) { var qualifiedName = GetQualifiedName(); var signatureWithoutReturn = $"{WhatKind} {qualifiedName}({string.Join(", ", Ins.Select(i => i.AsText()))})"; diff --git a/Source/DafnyCore/AST/Modules/ModuleDecl.cs b/Source/DafnyCore/AST/Modules/ModuleDecl.cs index 11531c54a34..588913b92a4 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDecl.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDecl.cs @@ -2,6 +2,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -80,7 +81,7 @@ public virtual string GetTriviaContainingDocstring() { return GetTriviaContainingDocstringFromStartTokenOrNull(); } - public DafnySymbolKind Kind => DafnySymbolKind.Namespace; + public SymbolKind Kind => SymbolKind.Namespace; public string GetDescription(DafnyOptions options) { return $"module {Name}"; } diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index 56228a4cf01..5ee071d9f9c 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs @@ -4,6 +4,7 @@ using System.Diagnostics.Contracts; using System.Linq; using Microsoft.Dafny.Auditor; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -1046,7 +1047,7 @@ bool InheritsFromObject(TraitDecl traitDecl) { return Enumerable.Empty(); }); - public DafnySymbolKind Kind => DafnySymbolKind.Namespace; + public SymbolKind Kind => SymbolKind.Namespace; public string GetDescription(DafnyOptions options) { return $"module {Name}"; } diff --git a/Source/DafnyCore/AST/Modules/ModuleQualifiedId.cs b/Source/DafnyCore/AST/Modules/ModuleQualifiedId.cs index b95c233309f..aa8686c5f07 100644 --- a/Source/DafnyCore/AST/Modules/ModuleQualifiedId.cs +++ b/Source/DafnyCore/AST/Modules/ModuleQualifiedId.cs @@ -95,6 +95,9 @@ public ModuleDecl ResolveTarget(ErrorReporter reporter) { } private ModuleDecl ResolveTargetUncached(ErrorReporter reporter) { + if (Root == null) { + return null; + } var decl = Root; for (int k = 1; k < Path.Count; k++) { ModuleSignature p; diff --git a/Source/DafnyCore/AST/Program.cs b/Source/DafnyCore/AST/Program.cs index 0c0734cde01..935290cce88 100644 --- a/Source/DafnyCore/AST/Program.cs +++ b/Source/DafnyCore/AST/Program.cs @@ -15,6 +15,7 @@ void ObjectInvariant() { Contract.Invariant(DefaultModule != null); } + public bool HasParseErrors { get; set; } public readonly string FullName; // Resolution essentially flattens the module hierarchy, for @@ -52,6 +53,7 @@ public Program(Cloner cloner, Program original) { SystemModuleManager = original.SystemModuleManager; Reporter = original.Reporter; Compilation = original.Compilation; + HasParseErrors = original.HasParseErrors; if (cloner.CloneResolvedFields) { throw new NotImplementedException(); diff --git a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs index 0505d4a1581..3ae978865a6 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs @@ -1,6 +1,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -130,7 +131,7 @@ public void MakeGhost() { (Attributes != null ? new List { Attributes } : Enumerable.Empty()).Concat( IsTypeExplicit ? new List() { OptionalType ?? type } : Enumerable.Empty()); - public DafnySymbolKind Kind => DafnySymbolKind.Variable; + public SymbolKind Kind => SymbolKind.Variable; public string GetDescription(DafnyOptions options) { return this.AsText(); } diff --git a/Source/DafnyCore/AST/Tokens.cs b/Source/DafnyCore/AST/Tokens.cs index d268539e3d9..96810cae6b7 100644 --- a/Source/DafnyCore/AST/Tokens.cs +++ b/Source/DafnyCore/AST/Tokens.cs @@ -56,8 +56,8 @@ string Boogie.IToken.filename { public class Token : IToken { public Token peekedTokens; // Used only internally by Coco when the scanner "peeks" tokens. Normally null at the end of parsing - public static readonly Token NoToken = new Token(); - public static readonly Token Cli = new Token(); + public static readonly Token NoToken = new(); + public static readonly Token Cli = new(); public Token() : this(0, 0) { } public Token(int linenum, int colnum) { @@ -218,6 +218,10 @@ public static RangeToken ToRange(this IToken token) { if (token is BoogieRangeToken boogieRangeToken) { return new RangeToken(boogieRangeToken.StartToken, boogieRangeToken.EndToken); } + + if (token is NestedToken nestedToken) { + return ToRange(nestedToken.Outer); + } return token as RangeToken ?? new RangeToken(token, token); } } diff --git a/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs b/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs index 0a779e080c9..660350c7749 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs @@ -1,6 +1,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -49,7 +50,7 @@ public string GetTriviaContainingDocstring() { return GetTriviaContainingDocstringFromStartTokenOrNull(); } - public DafnySymbolKind Kind => DafnySymbolKind.EnumMember; + public SymbolKind Kind => SymbolKind.EnumMember; public string GetDescription(DafnyOptions options) { var formals = string.Join(", ", Formals.Select(f => f.AsText())); return $"{EnclosingDatatype.Name}.{Name}({formals})"; diff --git a/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs index d0a69967c55..9a8cd46bb68 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs @@ -1,6 +1,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -81,7 +82,7 @@ public override bool IsEssentiallyEmpty() { } public override IEnumerable ChildSymbols => base.ChildSymbols.Concat(Ctors); - public override DafnySymbolKind Kind => DafnySymbolKind.Enum; + public override SymbolKind Kind => SymbolKind.Enum; public bool SetIndent(int indent, TokenNewIndentCollector formatter) { var indent2 = indent + formatter.SpaceTab; diff --git a/Source/DafnyCore/AST/TypeDeclarations/NonNullTypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/NonNullTypeDecl.cs index 0a2479e0c67..f17da2136b1 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/NonNullTypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/NonNullTypeDecl.cs @@ -1,5 +1,6 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -45,7 +46,7 @@ public override List ParentTypes(List typeArgs) { return result; } - public override DafnySymbolKind Kind => Class.Kind; + public override SymbolKind Kind => Class.Kind; public override string GetDescription(DafnyOptions options) { return Class.GetDescription(options); diff --git a/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs index 8d235f27085..3cf59abd0e8 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs @@ -1,6 +1,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -48,7 +49,7 @@ public override List ParentTypes(List typeArgs) { } public bool ShouldVerify => true; // This could be made more accurate public ModuleDefinition ContainingModule => EnclosingModuleDefinition; - public override DafnySymbolKind Kind => DafnySymbolKind.Class; + public override SymbolKind Kind => SymbolKind.Class; public override string GetDescription(DafnyOptions options) { return "subset type"; } diff --git a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs index 85810e98a47..f4c39e2863d 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs @@ -3,6 +3,7 @@ using System.Diagnostics.Contracts; using System.Linq; using Microsoft.Dafny.Auditor; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -266,7 +267,7 @@ public void RegisterMembers(ModuleResolver resolver, Dictionary ChildSymbols => Members.OfType(); - public virtual DafnySymbolKind Kind => DafnySymbolKind.Class; + public virtual SymbolKind Kind => SymbolKind.Class; public virtual string GetDescription(DafnyOptions options) { return $"{WhatKind} {Name}"; } diff --git a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDecl.cs index 5ca79f29643..b3687324a13 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDecl.cs @@ -1,4 +1,5 @@ using System.Collections.Generic; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -11,7 +12,7 @@ public TypeSynonymDecl(RangeToken rangeToken, Name name, TypeParameter.TypeParam } public TopLevelDecl AsTopLevelDecl => this; public TypeDeclSynonymInfo SynonymInfo { get; set; } - public override DafnySymbolKind Kind => DafnySymbolKind.Class; + public override SymbolKind Kind => SymbolKind.Class; public override string GetDescription(DafnyOptions options) { return "type synonym"; } @@ -23,7 +24,7 @@ public InternalTypeSynonymDecl(RangeToken rangeToken, Name name, TypeParameter.T : base(rangeToken, name, characteristics, typeArgs, module, rhs, attributes) { } - public override DafnySymbolKind Kind => DafnySymbolKind.Class; + public override SymbolKind Kind => SymbolKind.Class; public override string GetDescription(DafnyOptions options) { return "type synonym"; } diff --git a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs index 308b7f542f1..8812ba3ea56 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs @@ -2,6 +2,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -122,6 +123,6 @@ public string GetTriviaContainingDocstring() { return GetTriviaContainingDocstringFromStartTokenOrNull(); } - public abstract DafnySymbolKind Kind { get; } + public abstract SymbolKind Kind { get; } public abstract string GetDescription(DafnyOptions options); } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Types/MapType.cs b/Source/DafnyCore/AST/Types/MapType.cs index 5cc4d5c56d3..b5f6e7936bf 100644 --- a/Source/DafnyCore/AST/Types/MapType.cs +++ b/Source/DafnyCore/AST/Types/MapType.cs @@ -1,5 +1,6 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; +using System.Linq; namespace Microsoft.Dafny; @@ -23,6 +24,14 @@ public MapType(bool finite, Type domain, Type range) : base(domain, range) { this.finite = finite; this.range = range; } + + public MapType(Cloner cloner, MapType original) : base(cloner, original) { + Finite = original.Finite; + range = cloner.CloneType(original.Range); + var arg = HasTypeArg() ? Arg : null; + TypeArgs = new List() { arg, range }; + } + public Type Domain { get { return Arg; } } diff --git a/Source/DafnyCore/AST/Types/Types.cs b/Source/DafnyCore/AST/Types/Types.cs index 7cfa65790e3..a9323460a84 100644 --- a/Source/DafnyCore/AST/Types/Types.cs +++ b/Source/DafnyCore/AST/Types/Types.cs @@ -1998,6 +1998,10 @@ protected CollectionType(Type arg, Type other) { this.TypeArgs = new List { arg, other }; } + protected CollectionType(Cloner cloner, CollectionType original) { + this.arg = cloner.CloneType(original.arg); + } + public override bool ComputeMayInvolveReferences(ISet visitedDatatypes) { return Arg.ComputeMayInvolveReferences(visitedDatatypes); } diff --git a/Source/DafnyCore/Compilers/ExecutableBackend.cs b/Source/DafnyCore/Compilers/ExecutableBackend.cs index 4b8ef2096c4..f1ea26d03c0 100644 --- a/Source/DafnyCore/Compilers/ExecutableBackend.cs +++ b/Source/DafnyCore/Compilers/ExecutableBackend.cs @@ -135,7 +135,9 @@ public int WaitForExit(Process process, TextWriter outputWriter, TextWriter erro outputWriter.WriteLine("{0} Process exited with exit code {1}", errorMessage, process.ExitCode); } +#pragma warning disable VSTHRD002 errorProcessing.Wait(); +#pragma warning restore VSTHRD002 return process.ExitCode; } diff --git a/Source/DafnyCore/CoverageReport/CoverageReport.cs b/Source/DafnyCore/CoverageReport/CoverageReport.cs index d00f5a3a77d..de888236f44 100644 --- a/Source/DafnyCore/CoverageReport/CoverageReport.cs +++ b/Source/DafnyCore/CoverageReport/CoverageReport.cs @@ -19,7 +19,6 @@ public class CoverageReport { private readonly int uniqueId = Interlocked.Increment(ref nextUniqueId); public string UniqueSuffix => suffix + (uniqueId == 1 ? "" : ("_" + uniqueId)); - /// /// Generate a new empty coverage report for a given program. /// If not null, scan the for the list of files it consists of and populate the diff --git a/Source/DafnyCore/DafnyConsolePrinter.cs b/Source/DafnyCore/DafnyConsolePrinter.cs index 052b4fef298..c09d81c6661 100644 --- a/Source/DafnyCore/DafnyConsolePrinter.cs +++ b/Source/DafnyCore/DafnyConsolePrinter.cs @@ -4,6 +4,7 @@ using System.CommandLine; using System.IO; using System.Linq; +using System.Runtime.CompilerServices; using DafnyCore; using Microsoft.Boogie; using VC; @@ -19,7 +20,8 @@ public class DafnyConsolePrinter : ConsolePrinter { } } - private readonly ConcurrentDictionary> fsCache = new(); + private readonly static ConditionalWeakTable>> fsCaches = new(); + private DafnyOptions options; public record ImplementationLogEntry(string Name, Boogie.IToken Tok); @@ -64,7 +66,8 @@ public override void AdvisoryWriteLine(TextWriter output, string format, params } } - private string GetFileLine(Uri uri, int lineIndex) { + private static string GetFileLine(DafnyOptions options, Uri uri, int lineIndex) { + var fsCache = fsCaches.GetOrCreateValue(options)!; List lines = fsCache.GetOrAdd(uri, key => { try { // Note: This is not guaranteed to be the same file that Dafny parsed. To ensure that, Dafny should keep @@ -83,8 +86,8 @@ private string GetFileLine(Uri uri, int lineIndex) { return null; } - public void WriteSourceCodeSnippet(IToken tok, TextWriter tw) { - string line = GetFileLine(tok.Uri, tok.line - 1); + public static void WriteSourceCodeSnippet(DafnyOptions options, IToken tok, TextWriter tw) { + string line = GetFileLine(options, tok.Uri, tok.line - 1); if (line == null) { return; } @@ -139,7 +142,7 @@ public override void ReportBplError(Boogie.IToken tok, string message, bool erro if (Options.Get(ShowSnippets)) { if (tok is IToken dafnyTok) { - WriteSourceCodeSnippet(dafnyTok, tw); + WriteSourceCodeSnippet(Options, dafnyTok, tw); } else { ErrorWriteLine(tw, "No Dafny location information, so snippet can't be generated."); } diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 13cfdb24455..136dd72f1ce 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -29,9 +29,10 @@ + - + diff --git a/Source/DafnyCore/DafnyFile.cs b/Source/DafnyCore/DafnyFile.cs index 9c712ea9ad8..41c0c9c4f76 100644 --- a/Source/DafnyCore/DafnyFile.cs +++ b/Source/DafnyCore/DafnyFile.cs @@ -1,8 +1,6 @@ using System; using System.Collections.Generic; -using System.Diagnostics; using System.IO; -using System.Linq; using System.Reflection; using System.Reflection.Metadata; using System.Reflection.PortableExecutable; @@ -32,11 +30,11 @@ public static Uri ExposeInternalUri(string externalName, Uri internalUri) { } public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fileSystem, - DafnyOptions options, Uri uri, IToken origin) { + DafnyOptions options, Uri uri, IToken origin, string errorOnNotRecognized = null) { var embeddedFile = ExternallyVisibleEmbeddedFiles.GetValueOrDefault(uri); if (embeddedFile != null) { - var result = CreateAndValidate(reporter, fileSystem, options, embeddedFile, origin); + var result = CreateAndValidate(reporter, fileSystem, options, embeddedFile, origin, errorOnNotRecognized); if (result != null) { result.Uri = uri; } @@ -75,7 +73,7 @@ public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fi baseName = ""; } - var filePathForErrors = options.UseBaseNameForFileName ? Path.GetFileName(filePath) : filePath; + var filePathForErrors = options.GetPrintPath(filePath); if (getContent != null) { isPreverified = false; isPrecompiled = false; @@ -115,7 +113,16 @@ public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fi return null; } - dooFile = DooFile.Read(filePath); + try { + dooFile = DooFile.Read(filePath); + } catch (InvalidDataException) { + reporter.Error(MessageSource.Project, origin, $"malformed doo file {options.GetPrintPath(filePath)}"); + return null; + } catch (ArgumentException e) { + reporter.Error(MessageSource.Project, origin, e.Message); + return null; + } + } var validDooOptions = dooFile.Validate(reporter, filePathForErrors, options, origin); @@ -143,6 +150,9 @@ public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fi } getContent = () => new StringReader(sourceText); } else { + if (errorOnNotRecognized != null) { + reporter.Error(MessageSource.Project, Token.Cli, errorOnNotRecognized); + } return null; } diff --git a/Source/DafnyCore/DafnyMain.cs b/Source/DafnyCore/DafnyMain.cs index dd4d07fc369..2940e4b60ee 100644 --- a/Source/DafnyCore/DafnyMain.cs +++ b/Source/DafnyCore/DafnyMain.cs @@ -72,11 +72,11 @@ public static string Parse(IReadOnlyList files, string programName, D return null; } - private static readonly TaskScheduler largeThreadScheduler = + public static readonly CustomStackSizePoolTaskScheduler LargeThreadScheduler = CustomStackSizePoolTaskScheduler.Create(0x10000000, Environment.ProcessorCount); public static readonly TaskFactory LargeStackFactory = new(CancellationToken.None, - TaskCreationOptions.DenyChildAttach, TaskContinuationOptions.None, largeThreadScheduler); + TaskCreationOptions.DenyChildAttach, TaskContinuationOptions.None, LargeThreadScheduler); public static string Resolve(Program program) { if (program.Options.NoResolve || program.Options.NoTypecheck) { @@ -84,7 +84,9 @@ public static string Resolve(Program program) { } var programResolver = new ProgramResolver(program); +#pragma warning disable VSTHRD002 LargeStackFactory.StartNew(() => programResolver.Resolve(CancellationToken.None)).Wait(); +#pragma warning restore VSTHRD002 MaybePrintProgram(program, program.Options.DafnyPrintResolvedFile, true); if (program.Reporter.ErrorCountUntilResolver != 0) { @@ -113,7 +115,7 @@ to also include a directory containing the `z3` executable. var proverPath = options.ProverOptions.Find(o => o.StartsWith("PROVER_PATH=")); if (proverPath is null && options.Verify) { - options.OutputWriter.WriteLine(z3NotFoundMessage); + await options.OutputWriter.WriteLineAsync(z3NotFoundMessage); return (PipelineOutcome.FatalError, new PipelineStatistics()); } diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index 58e8e31cef7..c0bec6e11a4 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -36,6 +36,8 @@ public enum QuantifierSyntaxOptions { public record Options(IDictionary OptionArguments, IDictionary Arguments); public class DafnyOptions : Bpl.CommandLineOptions { + + public string GetPrintPath(string path) => UseBaseNameForFileName ? Path.GetFileName(path) : path; public TextWriter ErrorWriter { get; set; } public TextReader Input { get; } public static readonly DafnyOptions Default = new(TextReader.Null, TextWriter.Null, TextWriter.Null); diff --git a/Source/DafnyCore/Generic/ConsoleErrorReporter.cs b/Source/DafnyCore/Generic/ConsoleErrorReporter.cs index 30f681360cd..602ca2974d8 100644 --- a/Source/DafnyCore/Generic/ConsoleErrorReporter.cs +++ b/Source/DafnyCore/Generic/ConsoleErrorReporter.cs @@ -42,6 +42,12 @@ protected override bool MessageCore(MessageSource source, ErrorLevel level, stri errorLine += "\n"; } + if (Options.Get(DafnyConsolePrinter.ShowSnippets) && tok.Uri != null) { + var tw = new StringWriter(); + DafnyConsolePrinter.WriteSourceCodeSnippet(Options, tok.ToRange(), tw); + errorLine += tw.ToString(); + } + var innerToken = tok; while (innerToken is NestedToken nestedToken) { innerToken = nestedToken.Inner; @@ -59,17 +65,15 @@ protected override bool MessageCore(MessageSource source, ErrorLevel level, stri } errorLine += $"{innerToken.TokenToString(Options)}: {innerMessage}\n"; + if (Options.Get(DafnyConsolePrinter.ShowSnippets) && tok.Uri != null) { + var tw = new StringWriter(); + DafnyConsolePrinter.WriteSourceCodeSnippet(Options, innerToken.ToRange(), tw); + errorLine += tw.ToString(); + } } Options.OutputWriter.Write(errorLine); - - if (Options.Get(DafnyConsolePrinter.ShowSnippets) && tok.Uri != null) { - TextWriter tw = new StringWriter(); - new DafnyConsolePrinter(Options).WriteSourceCodeSnippet(tok.ToRange(), tw); - Options.OutputWriter.Write(tw.ToString()); - } - if (Options.OutputWriter == Console.Out) { Console.ForegroundColor = previousColor; } diff --git a/Source/DafnyCore/Generic/ErrorReporter.cs b/Source/DafnyCore/Generic/ErrorReporter.cs index c2351c70603..33fca572f82 100644 --- a/Source/DafnyCore/Generic/ErrorReporter.cs +++ b/Source/DafnyCore/Generic/ErrorReporter.cs @@ -14,7 +14,7 @@ protected ErrorReporter(DafnyOptions options) { public bool HasErrors => ErrorCount > 0; public int ErrorCount => Count(ErrorLevel.Error); - public bool HasErrorsUntilResolver => ErrorCountUntilResolver > 0; + public int ErrorCountUntilResolver => CountExceptVerifierAndCompiler(ErrorLevel.Error); public bool Message(MessageSource source, ErrorLevel level, string errorId, IToken tok, string msg) { diff --git a/Source/DafnyLanguageServer/Workspace/LazyConcurrentDictionary.cs b/Source/DafnyCore/Generic/LazyConcurrentDictionary.cs similarity index 97% rename from Source/DafnyLanguageServer/Workspace/LazyConcurrentDictionary.cs rename to Source/DafnyCore/Generic/LazyConcurrentDictionary.cs index accea09a69f..8d5971df2a6 100644 --- a/Source/DafnyLanguageServer/Workspace/LazyConcurrentDictionary.cs +++ b/Source/DafnyCore/Generic/LazyConcurrentDictionary.cs @@ -1,9 +1,10 @@ +#nullable enable using System; using System.Collections; using System.Collections.Concurrent; using System.Collections.Generic; -namespace Microsoft.Dafny.LanguageServer.Workspace; +namespace Microsoft.Dafny; /// /// System.Collections.Concurrent.ConcurrentDictionary does not allow you to lazily add a value if it is missing, diff --git a/Source/DafnyLanguageServer/Language/ReporterExtensions.cs b/Source/DafnyCore/Generic/ReporterExtensions.cs similarity index 79% rename from Source/DafnyLanguageServer/Language/ReporterExtensions.cs rename to Source/DafnyCore/Generic/ReporterExtensions.cs index a6106684ce8..8be46ca0bb2 100644 --- a/Source/DafnyLanguageServer/Language/ReporterExtensions.cs +++ b/Source/DafnyCore/Generic/ReporterExtensions.cs @@ -1,3 +1,4 @@ +#nullable enable using System.Collections.Generic; using System.Linq; using VCGeneration; @@ -6,10 +7,13 @@ namespace Microsoft.Dafny; public static class ErrorReporterExtensions { public static void ReportBoogieError(this ErrorReporter reporter, ErrorInformation error, bool useRange = true) { + var usingSnippets = reporter.Options.Get(DafnyConsolePrinter.ShowSnippets); var relatedInformation = new List(); foreach (var auxiliaryInformation in error.Aux) { - if (auxiliaryInformation.Category == RelatedLocationCategory) { - relatedInformation.AddRange(CreateDiagnosticRelatedInformationFor(BoogieGenerator.ToDafnyToken(true, auxiliaryInformation.Tok), auxiliaryInformation.Msg)); + if (auxiliaryInformation.Category == RelatedMessageCategory) { + error.Msg += "\n" + auxiliaryInformation.FullMsg; + } else if (auxiliaryInformation.Category == RelatedLocationCategory) { + relatedInformation.AddRange(CreateDiagnosticRelatedInformationFor(BoogieGenerator.ToDafnyToken(true, auxiliaryInformation.Tok), auxiliaryInformation.Msg, usingSnippets)); } else { // The execution trace is an additional auxiliary which identifies itself with // line=0 and character=0. These positions cause errors when exposing them, Furthermore, @@ -21,7 +25,7 @@ public static void ReportBoogieError(this ErrorReporter reporter, ErrorInformati } if (error.Tok is NestedToken { Inner: var innerToken, Message: var msg }) { - relatedInformation.AddRange(CreateDiagnosticRelatedInformationFor(innerToken, msg)); + relatedInformation.AddRange(CreateDiagnosticRelatedInformationFor(innerToken, msg, usingSnippets)); } var dafnyToken = BoogieGenerator.ToDafnyToken(useRange, error.Tok); @@ -36,18 +40,19 @@ public static void ReportBoogieError(this ErrorReporter reporter, ErrorInformati private const string RelatedLocationCategory = "Related location"; public const string RelatedLocationMessage = RelatedLocationCategory; + private const string RelatedMessageCategory = "Related message"; public static readonly string PostConditionFailingMessage = new ProofObligationDescription.EnsuresDescription(null, null).FailureDescription; private static string FormatRelated(string related) { return $"Could not prove: {related}"; } - public static IEnumerable CreateDiagnosticRelatedInformationFor(IToken token, string? message) { + public static IEnumerable CreateDiagnosticRelatedInformationFor(IToken token, string? message, bool usingSnippets) { var (tokenForMessage, inner, newMessage) = token is NestedToken nestedToken ? (nestedToken.Outer, nestedToken.Inner, nestedToken.Message) : (token, null, null); var dafnyToken = BoogieGenerator.ToDafnyToken(true, tokenForMessage); - if (dafnyToken is RangeToken rangeToken) { + if (!usingSnippets && dafnyToken is RangeToken rangeToken) { if (message == PostConditionFailingMessage) { var postcondition = rangeToken.PrintOriginal(); - message = $"This postcondition might not hold: {postcondition}"; + message = $"this postcondition might not hold: {postcondition}"; } else if (message == null || message == RelatedLocationMessage) { message = FormatRelated(rangeToken.PrintOriginal()); } @@ -55,7 +60,7 @@ public static IEnumerable CreateDiagnosticRelatedInform yield return new DafnyRelatedInformation(token, message); if (inner != null) { - foreach (var nestedInformation in CreateDiagnosticRelatedInformationFor(inner, newMessage)) { + foreach (var nestedInformation in CreateDiagnosticRelatedInformationFor(inner, newMessage, usingSnippets)) { yield return nestedInformation; } } diff --git a/Source/DafnyCore/Options/BoogieOptionBag.cs b/Source/DafnyCore/Options/BoogieOptionBag.cs index 5bbf99a944e..2e17ba5cfb7 100644 --- a/Source/DafnyCore/Options/BoogieOptionBag.cs +++ b/Source/DafnyCore/Options/BoogieOptionBag.cs @@ -116,6 +116,7 @@ static BoogieOptionBag() { DafnyOptions.RegisterLegacyBinding(SolverPath, (options, value) => { if (value != null) { + options.ProverOptions.RemoveAll(s => s.StartsWith("PROVER_PATH=")); options.ProverOptions.Add($"PROVER_PATH={value?.FullName}"); } }); diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index 34d7fb0bb25..d916645fb30 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -89,6 +89,23 @@ datatype with a single non-ghost constructor that has a single to prevent code from the bottom dependency from being generated more than once. The value may be a comma-separated list of files and folders.".TrimStart()); + public static IEnumerable SplitOptionValueIntoFiles(IEnumerable inputs) { + var result = new HashSet(); + foreach (var input in inputs) { + var values = input.Split(','); + foreach (var slice in values) { + var name = slice.Trim(); + if (Directory.Exists(name)) { + var files = Directory.GetFiles(name, "*.dfy", SearchOption.AllDirectories); + foreach (var file in files) { result.Add(file); } + } else { + result.Add(name); + } + } + } + return result; + } + public static readonly Option BuildFile = new(new[] { "--build", "-b" }, "Specify the filepath that determines where to place and how to name build files.") { ArgumentHelpName = "file", @@ -480,7 +497,7 @@ void ParsePrintMode(Option option, Boogie.CommandLineParseState ps, DafnyOptions.RegisterLegacyBinding(BuildFile, (options, value) => { options.DafnyPrintCompiledFile = value?.FullName; }); DafnyOptions.RegisterLegacyBinding(Libraries, - (options, value) => { options.LibraryFiles = value.Select(fi => fi.FullName).ToHashSet(); }); + (options, value) => { options.LibraryFiles = SplitOptionValueIntoFiles(value.Select(fi => fi.FullName)).ToHashSet(); }); DafnyOptions.RegisterLegacyBinding(Output, (options, value) => { options.DafnyPrintCompiledFile = value?.FullName; }); DafnyOptions.RegisterLegacyBinding(Verbose, (o, v) => o.Verbose = v); diff --git a/Source/DafnyCore/Options/DafnyProject.cs b/Source/DafnyCore/Options/DafnyProject.cs index a3c127d344d..e14d69b5e5d 100644 --- a/Source/DafnyCore/Options/DafnyProject.cs +++ b/Source/DafnyCore/Options/DafnyProject.cs @@ -19,7 +19,8 @@ namespace Microsoft.Dafny; public class DafnyProject : IEquatable { - public const string FileName = "dfyconfig.toml"; + public const string Extension = ".toml"; + public const string FileName = "dfyconfig" + Extension; public string ProjectName => Uri.ToString(); @@ -32,8 +33,9 @@ public class DafnyProject : IEquatable { public string[] Excludes { get; set; } public Dictionary Options { get; set; } public bool UsesProjectFile => Path.GetFileName(Uri.LocalPath) == FileName; + public bool ImplicitFromCli; - public IToken StartingToken => new Token { + public IToken StartingToken => ImplicitFromCli ? Token.Cli : new Token { Uri = Uri, line = 1, col = 1 @@ -57,7 +59,7 @@ public static async Task Open(IFileSystem fileSystem, DafnyOptions result = model; } catch (IOException e) { result = emptyProject; - result.Errors.Error(MessageSource.Parser, result.StartingToken, e.Message); + result.Errors.Error(MessageSource.Project, result.StartingToken, e.Message); } catch (TomlException tomlException) { var regex = new Regex( @$"\((\d+),(\d+)\) : error : The property `(\w+)` was not found on object type {typeof(DafnyProject).FullName}"); @@ -65,12 +67,12 @@ public static async Task Open(IFileSystem fileSystem, DafnyOptions match => $"({match.Groups[1].Value},{match.Groups[2].Value}): the property {match.Groups[3].Value} does not exist."); result = emptyProject; - var path = dafnyOptions.UseBaseNameForFileName ? Path.GetFileName(uri.LocalPath) : uri.LocalPath; - result.Errors.Error(MessageSource.Parser, result.StartingToken, $"The Dafny project file {path} contains the following errors: {newMessage}"); + var path = dafnyOptions.GetPrintPath(uri.LocalPath); + result.Errors.Error(MessageSource.Project, result.StartingToken, $"The Dafny project file {path} contains the following errors: {newMessage}"); } if (Path.GetFileName(uri.LocalPath) != FileName) { - result.Errors.Warning(MessageSource.Parser, (string)null, result.StartingToken, $"only Dafny project files named {FileName} are recognised by the Dafny IDE."); + result.Errors.Warning(MessageSource.Project, (string)null, result.StartingToken, $"only Dafny project files named {FileName} are recognised by the Dafny IDE."); } return result; @@ -153,7 +155,7 @@ public void Validate(TextWriter outputWriter, IEnumerable