diff --git a/Source/DafnyCore/AST/Statements/SkeletonStatement.cs b/Source/DafnyCore/AST/Statements/SkeletonStatement.cs index 44033eacf5..f36c87d2a1 100644 --- a/Source/DafnyCore/AST/Statements/SkeletonStatement.cs +++ b/Source/DafnyCore/AST/Statements/SkeletonStatement.cs @@ -1,3 +1,5 @@ +#nullable enable + using System.Collections.Generic; using System.Diagnostics.Contracts; @@ -24,11 +26,11 @@ namespace Microsoft.Dafny; /// ConditionOmitted == true && BodyOmitted == false /// public class SkeletonStatement : Statement, ICloneable, ICanFormat { - public readonly Statement S; - public bool ConditionOmitted { get { return ConditionEllipsis != null; } } - public readonly IToken ConditionEllipsis; - public bool BodyOmitted { get { return BodyEllipsis != null; } } - public readonly IToken BodyEllipsis; + public readonly Statement? S; + public bool ConditionOmitted => ConditionEllipsis != null; + public readonly IToken? ConditionEllipsis; + public bool BodyOmitted => BodyEllipsis != null; + public readonly IToken? BodyEllipsis; public SkeletonStatement Clone(Cloner cloner) { return new SkeletonStatement(cloner, this); @@ -52,13 +54,14 @@ public SkeletonStatement(Statement s, IToken conditionEllipsis, IToken bodyEllip ConditionEllipsis = conditionEllipsis; BodyEllipsis = bodyEllipsis; } + public override IEnumerable SubStatements { get { // The SkeletonStatement is really a modification of its inner statement S. Therefore, // we don't consider S to be a substatement. Instead, the substatements of S are the // substatements of the SkeletonStatement. In the case the SkeletonStatement modifies // S by omitting its body (which is true only for loops), there are no substatements. - if (!BodyOmitted && S.SubStatements != null) { + if (!BodyOmitted && S?.SubStatements != null) { foreach (var s in S.SubStatements) { yield return s; } @@ -68,7 +71,9 @@ public override IEnumerable SubStatements { public override IEnumerable PreResolveSubStatements { get { - yield return S; + if (S != null) { + yield return S; + } } } diff --git a/Source/DafnyCore/AST/Types/Types.cs b/Source/DafnyCore/AST/Types/Types.cs index e920966389..22317360fd 100644 --- a/Source/DafnyCore/AST/Types/Types.cs +++ b/Source/DafnyCore/AST/Types/Types.cs @@ -1,6 +1,7 @@ #define TI_DEBUG_PRINT using System; using System.Collections.Generic; +using System.Diagnostics; using System.Diagnostics.Contracts; using System.Linq; using System.Threading; @@ -1946,19 +1947,21 @@ public bool HasTypeArg() { } public void SetTypeArg(Type arg) { Contract.Requires(arg != null); - Contract.Requires(1 <= this.TypeArgs.Count); // this is actually an invariant of all collection types Contract.Assume(this.arg == null); // Can only set it once. This is really a precondition. this.arg = arg; - this.TypeArgs[0] = arg; + + Debug.Assert(TypeArgs.Count == 0); + TypeArgs.Add(arg); } public virtual void SetTypeArgs(Type arg, Type other) { Contract.Requires(arg != null); Contract.Requires(other != null); - Contract.Requires(this.TypeArgs.Count == 2); Contract.Assume(this.arg == null); // Can only set it once. This is really a precondition. this.arg = arg; - this.TypeArgs[0] = arg; - this.TypeArgs[1] = other; + + Debug.Assert(TypeArgs.Count == 0); + TypeArgs.Add(arg); + TypeArgs.Add(other); } [ContractInvariantMethod] void ObjectInvariant() { @@ -1971,14 +1974,23 @@ void ObjectInvariant() { /// protected CollectionType(Type arg) { this.arg = arg; - this.TypeArgs = new List { arg }; + TypeArgs = new List(1); + if (arg != null) { + TypeArgs.Add(arg); + } } + /// /// This constructor is a collection types with 2 type arguments /// protected CollectionType(Type arg, Type other) { this.arg = arg; - this.TypeArgs = new List { arg, other }; + TypeArgs = new List(2); + if (arg != null && other != null) { + TypeArgs.Add(arg); + TypeArgs.Add(other); + } + Debug.Assert(arg == null && other == null || arg != null && other != null); } protected CollectionType(Cloner cloner, CollectionType original) { diff --git a/Source/DafnyLanguageServer.Test/Completion/DotCompletionTest.cs b/Source/DafnyLanguageServer.Test/Completion/DotCompletionTest.cs index f42e0127b6..aafde7cc3e 100644 --- a/Source/DafnyLanguageServer.Test/Completion/DotCompletionTest.cs +++ b/Source/DafnyLanguageServer.Test/Completion/DotCompletionTest.cs @@ -23,6 +23,16 @@ private async Task> RequestCompletionAsync(TextDocumentItem return completionList.OrderBy(completion => completion.Label).ToList(); } + [Fact] + public async Task CodeCompletionInIncompleteTypeArgumentList() { + var source = @" +function Foo(): seq<".TrimStart(); + var documentItem = CreateAndOpenTestDocument(source, "CompleteOnThisReturnsClassMembers.dfy"); + + var completionList = await RequestCompletionAsync(documentItem, (0, 23)); + Assert.Empty(completionList); + } + [Fact] public async Task CompleteOnThisReturnsClassMembers() { var source = @" diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs index 0cbfe64d02..cfe68398e5 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs @@ -85,6 +85,26 @@ await SetUp(o => { Assert.True(hovers.Count > 0, "No hover expression detected."); } + [Fact] + public async Task Crash() { + var source = @" +module M { + method m() +} +module P refines M { + method m ... { + while true { ...; } + } +}"; + + var document = CreateAndOpenTestDocument(source); + var hoverResult = await client.RequestHover(new HoverParams() { + Position = new Position(0, 20), + TextDocument = document + }, CancellationToken); + Assert.Null(hoverResult); + } + [Fact] public async Task RecoverableParseErrorTypeRhs() { var markup = @" diff --git a/Source/DafnyLanguageServer.Test/Synchronization/EditDocumentTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/EditDocumentTest.cs new file mode 100644 index 0000000000..13b1133ac9 --- /dev/null +++ b/Source/DafnyLanguageServer.Test/Synchronization/EditDocumentTest.cs @@ -0,0 +1,247 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Threading.Tasks; +using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; +using Microsoft.Dafny.LanguageServer.Workspace; +using Microsoft.Extensions.Logging; +using OmniSharp.Extensions.LanguageServer.Protocol.Document; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; +using Xunit; +using Xunit.Abstractions; +using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; + +namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization; + +[Collection("Sequential Collection")] +public class EditDocumentTest : ClientBasedLanguageServerTest { + + [Fact] + public async Task SlowlyTypeFile() { + var source = @"module NoTypeArgs0 { + datatype List<+T> = Nil | Cons(T, List) + datatype Tree<+A,+B> = Leaf(A, B) | Node(Tree, Tree) + + method DoAPrefix0(xs: List) returns (ys: List) + { + ys := xs; + } + + method DoAPrefix1(xs: List) returns (ys: List) + { + ys := xs; // error: List cannot be assign to a List + } + + method DoAPrefix2(xs: List) returns (ys: List) + { + ys := xs; // error: List cannot be assign to a List + } + + ghost function FTree0(t: Tree): Tree + { + match t + case Leaf(_,_) => t + case Node(x, y) => x + } + + ghost function FTree1(t: Tree): Tree + { + match t + case Leaf(_,_) => t + case Node(x, y) => y // error: y does not have the right type + } + + ghost function FTree2(t: Tree): Tree + { + t + } +} + +module NoTypeArgs1 { + datatype Tree = Leaf(A, B) | Node(Tree, Tree) + + ghost function FTree3(t: Tree): Tree // error: type of 't' does not have enough type parameters + { + t + } +} + +// ----------- let-such-that expressions ------------------------ + +module MiscMisc { + method LetSuchThat(ghost z: int, n: nat) + { + var x: int; + x := var y :| y < 0; y; // fine for the resolver (but would give a verification error for not being deterministic) + + x := var w :| w == 2*w; w; // fine (even for the verifier, this one) + x := var w := 2*w; w; // error: the 'w' in the RHS of the assignment is not in scope + ghost var xg := var w :| w == 2*w; w; + } +} + +// ------------ quantified variables whose types are not inferred ---------- + +module NonInferredType { + ghost predicate P(x: T) + + method InferredType(x: int) + { + var t; + assume forall z :: P(z) && z == t; + assume t == x; // this statement determines the type of t and z + } + + method NonInferredType(x: int) + { + var t; // error: the type of t is not determined + assume forall z :: P(z) && z == t; // error: the type of z is not determined + } +} + +// ------------ Here are some tests that lemma contexts don't allocate objects ------------- + +module GhostAllocationTests { + class G { } + iterator GIter() { } + class H { constructor () } + lemma GhostNew0() + ensures exists o: G :: fresh(o) + { + var p := new G; // error: lemma context is not allowed to allocate state + p := new G; // error: ditto + } + + method GhostNew1(n: nat, ghost g: int) returns (t: G, z: int) + { + if n < 0 { + z, t := 5, new G; // fine + } + if n < g { + var tt := new H(); // error: 'new' not allowed in ghost contexts + } + } + + method GhostNew2(ghost b: bool) + { + if (b) { + var y := new GIter(); // error: 'new' not allowed in ghost contexts (and a non-ghost method is not allowed to be called here either) + } + } +} +module MoreGhostAllocationTests { + class G { } + method GhostNew3(n: nat) { + var g := new G; + calc { + 5; + { var y := new G; } // error: 'new' not allowed in lemma contexts + 2 + 3; + } + } + ghost method GhostNew4(g: G) + modifies g + { + } +} + +module NewForallAssign { + class G { } + method NewForallTest(n: nat) { + var a := new G[n]; + forall i | 0 <= i < n { + a[i] := new G; // error: 'new' is currently not supported in forall statements + } } +} +module NewForallProof { + class G { } + method NewForallTest(n: nat) { var a := new G[n]; + forall i | 0 <= i < n ensures true { // this makes the whole 'forall' statement into a ghost statement + a[i] := new G; // error: proof-forall cannot update state (and 'new' not allowed in ghost contexts, but that's checked at a later stage) + } } +} + +// ------------------------- underspecified types ------------------------------ + +module UnderspecifiedTypes { + method M(S: set) { + var n, p, T0 :| 12 <= n && n in T0 && 10 <= p && p in T0 && T0 <= S && p % 2 != n % 2; + var T1 :| 12 in T1 && T1 <= S; + var T2 :| T2 <= S && 12 in T2; + + var T3'0: set :| 120 in T3'0; + var T3'1: multiset :| 120 in T3'1; + var T3'2: map :| 120 in T3'2; + var T3'3: seq :| 120 in T3'3; + var T3'4: bool :| 120 in T3'4; // error: second argument to 'in' cannot be bool + var T4 :| T4 <= S; + } +} + +module UnderspecifiedTypes' { + method M() { + var T3 :| 120 in T3; // error: underspecified type + } +} + +// ------------------------- lemmas ------------------------------ + +module MiscLemma { + class L { } + + // a lemma is allowed to have out-parameters, but not a modifies clause + lemma MyLemma(x: int, l: L) returns (y: int) + requires 0 <= x + modifies l + ensures 0 <= y + { + y := x; + } +} +"; + await SlowlyTypeInSource(source, 1000); + } + + private async Task SlowlyTypeInSource(string source, int steps) { + await SetUp(dafnyOptions => { + dafnyOptions.Set(ProjectManager.UpdateThrottling, ProjectManager.DefaultThrottleTime); + }); + var document = CreateAndOpenTestDocument(""); + + + var stepSize = (int)Math.Ceiling(source.Length / (double)steps); + for (var index = 0; index < source.Length; index += stepSize) { + var part = source.Substring(index, Math.Min(source.Length, index + stepSize) - index); + ApplyChange(ref document, new Range(0, index, 0, index), part); + var completionItems = await RequestCompletionAsync(document, new Position(0, index + stepSize)); + var hover = await RequestHover(document, new Position(0, index + stepSize)); + } + + return document; + } + + private Task RequestHover(TextDocumentItem documentItem, Position position) { + return client.RequestHover( + new HoverParams { + TextDocument = documentItem.Uri, + Position = position + }, + CancellationToken + ); + } + + private async Task> RequestCompletionAsync(TextDocumentItem documentItem, Position position) { + // TODO at this time we do not set the context since it appears that's also the case when used within VSCode. + var completionList = await client.RequestCompletion( + new CompletionParams { + TextDocument = documentItem.Uri, + Position = position + }, + CancellationToken + ).AsTask(); + return completionList.OrderBy(completion => completion.Label).ToList(); + } + + public EditDocumentTest(ITestOutputHelper output, LogLevel dafnyLogLevel = LogLevel.Information) : base(output, dafnyLogLevel) { + } +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer.Test/Unit/DafnyHoverHandlerTest.cs b/Source/DafnyLanguageServer.Test/Unit/DafnyHoverHandlerTest.cs index 5be278f196..a87144c032 100644 --- a/Source/DafnyLanguageServer.Test/Unit/DafnyHoverHandlerTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/DafnyHoverHandlerTest.cs @@ -4,6 +4,7 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Unit; public class DafnyHoverHandlerTest { + [Fact] public void FormatResourceUnitTest() { void OneTest(string expected, long input) { diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.cs b/Source/DafnyLanguageServer/DafnyLanguageServer.cs index 3a48010989..556b3682d2 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.cs +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.cs @@ -56,6 +56,10 @@ private static void PublishSolverPath(ILanguageServer server) { try { var proverOptions = new SMTLibSolverOptions(options); proverOptions.Parse(options.ProverOptions); + if (proverOptions.ProverName == "noop") { + telemetryPublisher.PublishSolverPath("noop solver"); + return; + } solverPath = proverOptions.ExecutablePath(); HandleZ3Version(telemetryPublisher, solverPath); } catch (Exception e) {