forked from dafny-lang/dafny
-
Notifications
You must be signed in to change notification settings - Fork 0
/
DafnyLanguageServerTestBase.cs
169 lines (146 loc) · 6.49 KB
/
DafnyLanguageServerTestBase.cs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
using System;
using System.Collections.Generic;
using System.CommandLine;
using Microsoft.Dafny.LanguageServer.Workspace;
using Microsoft.Extensions.DependencyInjection;
using Microsoft.Extensions.Logging;
using OmniSharp.Extensions.JsonRpc.Testing;
using OmniSharp.Extensions.LanguageProtocol.Testing;
using OmniSharp.Extensions.LanguageServer.Protocol;
using OmniSharp.Extensions.LanguageServer.Protocol.Client;
using OmniSharp.Extensions.LanguageServer.Protocol.Document;
using OmniSharp.Extensions.LanguageServer.Protocol.Models;
using OmniSharp.Extensions.LanguageServer.Protocol.Server;
using OmniSharp.Extensions.LanguageServer.Server;
using System.IO;
using System.Linq;
using System.Threading;
using System.Threading.Tasks;
using DafnyCore.Test;
using Microsoft.Dafny.LanguageServer.IntegrationTest.Various;
using Microsoft.Dafny.LanguageServer.Language;
using OmniSharp.Extensions.LanguageServer.Client;
using Xunit.Abstractions;
namespace Microsoft.Dafny.LanguageServer.IntegrationTest {
public class DafnyLanguageServerTestBase : LanguageProtocolTestBase {
protected readonly string SlowToVerify = @"
lemma {:rlimit 100} SquareRoot2NotRational(p: nat, q: nat)
requires p > 0 && q > 0
ensures (p * p) != 2 * (q * q)
{
if (p * p) == 2 * (q * q) {
calc == {
(2 * q - p) * (2 * q - p);
4 * q * q + p * p - 4 * p * q;
{assert 2 * q * q == p * p;}
2 * q * q + 2 * p * p - 4 * p * q;
2 * (p - q) * (p - q);
}
}
}".TrimStart();
protected string SlowToVerifyNoLimit => SlowToVerify.Replace(" {:rlimit 100}", "");
protected readonly string NeverVerifies = @"
lemma {:neverVerify} HasNeverVerifyAttribute(p: nat, q: nat)
ensures true
{
}".TrimStart();
public const string LanguageId = "dafny";
protected static int fileIndex;
protected readonly TextWriter output;
public ILanguageServer Server { get; protected set; }
public IProjectDatabase Projects => Server.GetRequiredService<IProjectDatabase>();
protected DafnyLanguageServerTestBase(ITestOutputHelper output, LogLevel dafnyLogLevel = LogLevel.Information)
: base(new JsonRpcTestOptions(LoggerFactory.Create(
builder => {
builder.AddFilter("OmniSharp.Extensions.JsonRpc", LogLevel.None);
builder.AddFilter("OmniSharp", LogLevel.Warning);
builder.AddFilter("Microsoft.Dafny", dafnyLogLevel);
builder.AddConsole();
}))) {
this.output = new WriterFromOutputHelper(output);
}
protected virtual void ServerOptionsAction(LanguageServerOptions serverOptions) {
}
protected Task<(ILanguageClient client, ILanguageServer server)> Initialize(Action<LanguageClientOptions> clientOptionsAction, Action<DafnyOptions> serverOptionsAction) {
/*
* I would rather use LanguageServerOptions.RegisterForDisposal, but it doesn't seem to work
* Alternatively one can do Disposable.Add((IDisposable)Server.Services), but we've seen many
* ObjectDisposedExceptions in tests that might relate to this, so let's be more specific and only dispose
* IProjectDatabase
*/
Disposable.Add(new AnonymousDisposable(() => {
var database = Server.Services.GetRequiredService<IProjectDatabase>();
database.Dispose();
}));
return base.Initialize(clientOptionsAction, GetServerOptionsAction(serverOptionsAction));
}
private sealed class AnonymousDisposable : IDisposable {
private Action action;
public AnonymousDisposable(Action action) {
this.action = action;
}
public void Dispose() => Interlocked.Exchange(ref action, null)?.Invoke();
}
private Action<LanguageServerOptions> GetServerOptionsAction(Action<DafnyOptions> modifyOptions) {
var dafnyOptions = DafnyOptions.Create(output);
dafnyOptions.Set(ServerCommand.UpdateThrottling, 0);
modifyOptions?.Invoke(dafnyOptions);
ServerCommand.ConfigureDafnyOptionsForServer(dafnyOptions);
ApplyDefaultOptionValues(dafnyOptions);
return options => {
options.WithDafnyLanguageServer(() => { });
options.Services.AddSingleton(dafnyOptions);
options.Services.AddSingleton<IProgramVerifier>(serviceProvider => new SlowVerifier(
serviceProvider.GetRequiredService<ILogger<DafnyProgramVerifier>>()
));
ServerOptionsAction(options);
};
}
private static void ApplyDefaultOptionValues(DafnyOptions dafnyOptions) {
var testCommand = new System.CommandLine.Command("test");
foreach (var serverOption in ServerCommand.Instance.Options) {
testCommand.AddOption(serverOption);
}
var result = testCommand.Parse("test");
foreach (var option in ServerCommand.Instance.Options) {
if (!dafnyOptions.Options.OptionArguments.ContainsKey(option)) {
var value = result.GetValueForOption(option);
dafnyOptions.SetUntyped(option, value);
}
dafnyOptions.ApplyBinding(option);
}
}
protected static TextDocumentItem CreateTestDocument(string source, string filePath = null, int version = 1) {
if (filePath == null) {
var index = Interlocked.Increment(ref fileIndex);
filePath = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName(), $"testFile{index}.dfy");
}
if (string.IsNullOrEmpty(Path.GetDirectoryName(filePath))) {
filePath = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName(), filePath);
}
filePath = Path.GetFullPath(filePath);
return new TextDocumentItem {
LanguageId = LanguageId,
Text = source,
Uri = filePath.StartsWith("untitled:") ? DocumentUri.Parse(filePath) : DocumentUri.FromFileSystemPath(filePath),
Version = version
};
}
protected static void OpenDocument(ILanguageClient client, TextDocumentItem document) {
client.DidOpenTextDocument(new DidOpenTextDocumentParams {
TextDocument = document
});
}
public static string PrintDiagnostics(IEnumerable<Diagnostic> items) {
return PrintEnumerable(items.Select(PrintDiagnostic));
}
public static string PrintDiagnostic(Diagnostic diagnostic) {
var relatedPrint = string.Join(", ", diagnostic.RelatedInformation?.
Select(r => $"at {r.Location} saying '{r.Message}'") ?? Array.Empty<string>());
return $"Diagnostic at {diagnostic.Range} saying '{diagnostic.Message}', related: {relatedPrint}";
}
public static string PrintEnumerable(IEnumerable<object> items) {
return "[" + string.Join(", ", items.Select(o => o.ToString())) + "]";
}
}
}