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
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
|
# SPDX-FileCopyrightText: Copyright (c) 2021 Andrew T. Walter <me@atwalter.com>
# SPDX-License-Identifier: MIT
import time
import subprocess
import os
import socket
import struct
ACL2S_COMMAND_RUN_TIMEOUT_S = 20 # seconds in which the ACL2S process should start and run our command
class Acl2sServiceException(Exception):
pass
class InvalidHeaderException(Acl2sServiceException):
def __init__(self, actual_header):
self.message = f"Expected QK but got ${actual_header}."
class MessageSizeMismatchException(Acl2sServiceException):
def __init__(self, expected, actual):
self.message = f"Expected message length to be ${expected} bytes, but actually only recieved ${actual} bytes."
class ConnectionTestFailedException(Acl2sServiceException):
def __init__(self):
self.message = "Connection test failed - ensure that the service executes correctly and supports the E echo command"
class Acl2sService:
"""A class representing a an ACL2s service. Can either connect to an
existing ACL2s service with connect(), or start an ACL2s service
image in a subprocess and manage it.
"""
def __init__(self, run_timeout=ACL2S_COMMAND_RUN_TIMEOUT_S):
self.output_read_fd = None
self.output_write_fd = None
self.process = None
self.sock = None
self.run_timeout = run_timeout
# 1382728371 is the default random seed for ACL2s
# See books/acl2s/defdata/random-state-basis1.lisp.
def start(self, executable, seed=1382728371, debug=False):
"""Start the ACL2s service and connect to it.
Returns the port that the ACL2s service is listening on.
Note that the optional seed parameter must be a 63-bit unsigned
integer (per defdata).
The ACL2s service image must output the port number that it is
listening on to the file descriptor that it is passed in.
"""
# Create pipes for receiving data from acl2s.
self.output_read_fd, self.output_write_fd = os.pipe()
# TODO: preexec_fn does not work on windows. But this is probably
# true of most of the code in this file.
# Pipe stdout and stderr to /dev/null unless debug is True.
stdout = subprocess.DEVNULL
stderr = subprocess.DEVNULL
if debug:
stdout = None
stderr = None
self.process = subprocess.Popen(
[executable, str(self.output_write_fd), str(seed)],
stdin=subprocess.DEVNULL,
stdout=stdout,
stderr=stderr,
pass_fds=[self.output_write_fd],
# Ignore CTRL-C
preexec_fn=os.setpgrp)
d = os.read(self.output_read_fd, 5)
decoded = d.decode()
port = int(decoded)
self.connect(port, host="0.0.0.0")
return port
def connect(self, port, host="0.0.0.0"):
"""Connect to a running ACL2s service on the given port.
The `host` argument is optional, and by default is 0.0.0.0.
After connecting, this service will test whether the server
responds as expected to an E (echo) command. If this fails, a
`ConnectionTestFailedException `is raised but the socket remains
connected.
"""
self.sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
self.sock.connect((host, port))
self.sock.settimeout(self.run_timeout)
if not self.run_command("E", "test") == ("OK", "test"):
raise ConnectionTestFailedException()
def disconnect(self):
"""Disconnect from a running ACL2s service.
This will not stop the service, it will only close the TCP
connection.
"""
self.sock.close()
def stop(self):
"""Stop the running ACL2s service and disconnect from it.
If the ACL2s service was started in this Python instance using
the `start` method of Acl2sService, the process will also be
killed, and the file descriptors used to communicate with it at
initialization time will be closed.
The process kill and file descriptor cleanup will occur even if
the stop command fails to execute for some reason.
"""
try:
self.run_command("Q")
self.sock.close()
finally:
if self.process:
self.process.kill()
if self.output_write_fd:
os.close(self.output_write_fd)
if self.output_read_fd:
os.close(self.output_read_fd)
def write(self, body):
"""Send data to the ACL2s service."""
body_en = body.encode(encoding="utf-8")
nbytes = len(body_en)
return self.sock.send(b''.join([b'QK', struct.pack('>I', nbytes), body_en]))
def read(self):
"""Recieve data from the ACL2s service.
This method will raise a `socket.timeout` exception if no
message is received within the configured `run_timeout`
duration.
"""
header = self.sock.recv(6)
if not header[0:2] == b'QK':
raise InvalidHeaderException()
nbytes = struct.unpack('>I', header[2:])[0]
totbytes = 0
body = []
# Note that the message may come in as several TCP packets,
# so we need to make sure we wait for them all here
# TODO: add timeout or something
while totbytes < nbytes:
data = self.sock.recv(nbytes-totbytes)
body.append(data)
totbytes = totbytes + len(data)
if not totbytes == nbytes:
raise MessageSizeMismatchException(nbytes, totbytes)
return b''.join(body).decode(encoding="utf-8")
def run(self, data):
"""Send a data to the ACL2s service and wait for it to respond.
This method will raise a `socket.timeout` exception if the Lisp
command(s) take longer than the configured `run_timeout`
duration to evaluate.
"""
self.write(data)
return self.read()
def write_command(self, command, data=""):
if len(command) != 1:
raise ValueError("Command should be a single-character string.")
return self.write(command + str(data))
def read_command(self):
output = self.read()
return (output[0:2], output[2:])
def run_command(self, command, data=""):
"""Send a command to the ACL2s service with (optionally) some
data and wait for it to respond.
This method will raise a `socket.timeout` exception if the Lisp
command(s) take longer than the configured `run_timeout`
duration to evaluate.
"""
self.write_command(command, data)
return self.read_command()
if __name__ == "__main__":
# TODO: add better example
#p = Acl2sService()
#try:
# p.start()
# print(p.run_command("E", "foobar"))
#finally:
# p.stop()
pass
|
