blob: 8c94ad5b36ac52613f2365f7ae314c1da2d83818 (
plain)
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
|
using System;
using System.IO;
using System.Text;
using System.Collections.Generic;
using System.Runtime.Serialization;
using System.Runtime.Serialization.Json;
using Dafny = Microsoft.Dafny;
using Bpl = Microsoft.Boogie;
using Microsoft.Boogie;
namespace Microsoft.Dafny {
class Server {
private bool running;
static void Main(string[] args) {
Server server = new Server();
var hasArg = args.Length > 0;
var arg = hasArg ? args[0] : null;
if (hasArg && args[0] == "selftest") {
VerificationTask.SelfTest();
} else if (hasArg && File.Exists(arg)) {
Console.WriteLine("# Reading from {0}", Path.GetFileName(arg));
Console.SetIn(new StreamReader(arg, Encoding.UTF8));
server.Loop();
} else {
server.Loop();
}
}
private void SetupConsole() {
// Setting InputEncoding to UTF8 causes z3 to choke.
Console.OutputEncoding = new UTF8Encoding(false, true);
}
public Server() {
this.running = true;
ExecutionEngine.printer = new DafnyConsolePrinter();
SetupConsole();
}
bool EndOfPayload(out string line) {
line = Console.ReadLine();
return line == null || line == Interaction.CLIENT_EOM_TAG;
}
string ReadPayload() {
StringBuilder buffer = new StringBuilder();
string line = null;
while (!EndOfPayload(out line)) {
buffer.Append(line);
}
return buffer.ToString();
}
void Loop() {
for (int cycle = 0; running; cycle++) {
var line = Console.ReadLine() ?? "quit";
if (line != String.Empty && !line.StartsWith("#")) {
var command = line.Split();
Respond(command);
}
}
}
void Respond(string[] command) {
try {
if (command.Length == 0) {
throw new ServerException("Empty command");
}
var verb = command[0];
if (verb == "verify") {
ServerUtils.checkArgs(command, 0);
var payload = ReadPayload();
VerificationTask.ReadTask(payload).Run();
} else if (verb == "quit") {
ServerUtils.checkArgs(command, 0);
Exit();
} else {
throw new ServerException("Unknown verb '{0}'", verb);
}
Interaction.EOM(Interaction.SUCCESS, "Verification completed successfully!");
} catch (ServerException ex) {
Interaction.EOM(Interaction.FAILURE, ex);
} catch (Exception ex) {
Interaction.EOM(Interaction.FAILURE, ex, "[FATAL]");
running = false;
}
}
void Exit() {
this.running = false;
}
}
}
|
