1 package acl2s.lib.session;
2
3 import java.io.BufferedWriter;
4 import java.io.File;
5 import java.io.IOException;
6 import java.io.InputStream;
7 import java.io.InputStreamReader;
8 import java.io.OutputStreamWriter;
9 import java.io.Writer;
10 import java.util.LinkedList;
11
12 import org.peterd.util.ExceptionHandler;
13 import org.peterd.util.Misc;
14 import org.peterd.util.io.AsyncLineReader;
15 import org.peterd.util.io.AsyncWriter;
16 import org.peterd.util.process.KillableProcess;
17
18 public class BatchSession {
19 protected final BatchSessionConfig config;
20 protected final File workingDir;
21
22 protected KillableProcess proc;
23 protected AsyncWriter acl2Input;
24 protected OutputHandler outputHandler;
25 protected long secret;
26 protected String[] cmdLine;
27
28 public BatchSession(BatchSessionConfig config, File workingDir) {
29 proc = null;
30 this.config = config;
31 this.workingDir = workingDir;
32 }
33
34 public synchronized void init() throws IOException, IllegalStateException {
35 if (proc != null) throw new IllegalStateException();
36 cmdLine = config.getBaseConfig().getCmdLine();
37 proc = KillableProcess.exec(cmdLine, workingDir, config.getBaseConfig(), true);
38 acl2Input = new AsyncWriter(new OutputStreamWriter(proc.getStdin())).fork();
39 secret = Misc.random.nextLong() & 0xfffffffffffffffL;
40
41 // All input
42 String[] input = config.getStartup(secret);
43 if (input != null) {
44 for (int i = 0; i < input.length; i++) {
45 acl2Input.write(input[i]);
46 }
47 }
48 acl2Input.close(); // after all input, of course
49 notifyAll();
50 }
51
52 public class OutputHandler extends Thread {
53 protected final Writer dst;
54
55 // access must be lock-protected
56 protected ExceptionHandler<IOException> ioeh;
57 protected IOException ioe = null;
58 protected boolean snip = true;
59 protected StringBuilder snippedOutput = null;
60 protected LinkedList<Runnable> postEOFhooks = new LinkedList<Runnable>();
61
62 OutputHandler(Writer dst) {
63 if (!(dst instanceof BufferedWriter)) {
64 dst = new BufferedWriter(dst);
65 }
66 this.dst = dst;
67 }
68
69 public Writer getDst() {
70 return dst;
71 }
72
73 public synchronized void setExceptionHandler(ExceptionHandler<IOException> ioeh) {
74 this.ioeh = ioeh;
75 }
76
77 public synchronized void setSnipEnabled(boolean snip) {
78 this.snip = snip;
79 }
80
81 public synchronized void setSnipCaptureEnabled(boolean snipCapture) {
82 if (snipCapture && snippedOutput == null) {
83 snippedOutput = new StringBuilder();
84 } else if (snippedOutput != null) {
85 snippedOutput = null;
86 }
87 }
88
89 public synchronized String getSnippedOutput() {
90 if (snippedOutput == null) throw new IllegalStateException();
91 return snippedOutput.toString();
92 }
93
94 public synchronized IOException getIOException() {
95 return ioe;
96 }
97
98 void handleIOException(IOException ioe) {
99 if (ioe == null) return;
100 ExceptionHandler<IOException> h;
101 synchronized (this) {
102 this.ioe = ioe;
103 h = ioeh;
104 }
105 if (h != null) {
106 h.handleException(ioe);
107 }
108 }
109
110 synchronized void handleSnippedOutputLine(String line) {
111 if (snippedOutput != null) {
112 snippedOutput.append(line);
113 snippedOutput.append('\n');
114 }
115 }
116
117 public synchronized void appendCloseOnEOFhook() {
118 appendPostEOFhook(new Runnable() {
119 public void run() {
120 try {
121 dst.close();
122 } catch (IOException ioe) {
123 handleIOException(ioe);
124 }
125 }
126 });
127 }
128
129 public synchronized void appendPostEOFhook(Runnable r) {
130 if (postEOFhooks == null) throw new IllegalStateException();
131 postEOFhooks.addLast(r);
132 }
133
134 protected AsyncLineReader in = null; // only accessed by this thread
135 public void run() {
136 try {
137 KillableProcess p;
138 synchronized (BatchSession.this) {
139 while (proc == null) {
140 try {
141 BatchSession.this.wait();
142 } catch (InterruptedException e) {
143 // ignore
144 }
145 }
146 p = proc;
147 }
|
Event do_not_call: |
"java.io.InputStreamReader(java.io.InputStream arg1)" implicitly uses the environment's default character set, which might lead to unexpected behavior. Consider using InputStreamReader(InputStream in, String charsetName). |
148 in = new AsyncLineReader(new InputStreamReader(p.getStdout())).fork();
149 boolean snip;
150 synchronized (this) {
151 snip = this.snip;
152 }
153 if (snip) {
154 goWithSnip();
155 } else {
156 goNoSnip();
157 }
158 synchronized (BatchSession.this) {
159 updateAlive();
160 p = proc;
161 }
162 dst.write("//end of output\n");
163 if (p != null) {
164 p.waitFor2();
165 synchronized (BatchSession.this) {
166 proc = null; // make sure :)
167 }
168 }
169 dst.write("//session terminated\n");
170 } catch (IOException ioe) {
171 handleIOException(ioe);
172 kill();
173 }
174
175 LinkedList<Runnable> hooks;
176 synchronized (this) {
177 hooks = postEOFhooks;
178 postEOFhooks = null;
179 }
180 for (Runnable r : hooks) {
181 try {
182 r.run();
183 } catch (Throwable t) {
184 // ignore
185 }
186 }
187 }
188
189 String readLine() throws IOException {
190 try {
191 // return a line if available
192 String maybeLine = in.maybeReadLine();
193 if (maybeLine != null) return maybeLine;
194 // otherwise, flush output and wait (or return null)
195 dst.flush();
196 return in.readLine2();
197 } catch (IOException ioe) {
198 if (isAlive()) {
199 dst.write("Error reading ACL2 output: " + ioe.getMessage());
200 kill();
201 }
202 return null;
203 }
204 }
205
206 public void goWithSnip() throws IOException {
207 String line;
208 for (;;) {
209 line = readLine();
210 if (line == null) return;
211 dst.write(line);
212 dst.write(newline);
213 if (line.indexOf("ACL2 Version ") >= 0) {
214 break;
215 }
216 }
217 for (;;) {
218 line = readLine();
219 if (line == null) return;
220 dst.write(line);
221 dst.write(newline);
222 if (line.length() < 2) {
223 break;
224 }
225 }
226 for (;;) {
227 for (;;) {
228 line = readLine();
229 if (line == null) return;
230 handleSnippedOutputLine(line);
231 if (line.endsWith("${NoMoReSnIp}$")) {
232 break;
233 }
234 }
235 for (;;) {
236 line = readLine();
237 if (line == null) return;
238 if (line.endsWith("${SnIpMeHeRe}$")) {
239 handleSnippedOutputLine(line);
240 break;
241 }
242 dst.write(line);
243 dst.write(newline);
244 }
245 }
246 }
247
248 public void goNoSnip() throws IOException {
249 String line;
250 for (;;) {
251 line = readLine();
252 if (line == null) return;
253 dst.write(line);
254 dst.write(newline);
255 }
256 }
257 }
258
259 public synchronized OutputHandler createOutputHandler(Writer dst) {
260 if (outputHandler != null) throw new IllegalStateException();
261 outputHandler = new OutputHandler(dst);
262 return outputHandler;
263 }
264
265
266
267 static final String newline = "\n";
268
269 public void dispose() {
270 kill();
271 }
272
273 public synchronized boolean isAlive() {
274 updateAlive();
275 return proc != null;
276 }
277
278 synchronized void updateAlive() {
279 if (proc != null && !proc.isAlive()) {
280 proc = null;
281 notifyAll();
282 }
283 }
284
285 public synchronized void kill() {
286 if (proc != null) {
287 proc.kill();
288 proc = null;
289 }
290 }
291
292 public long getSecret() { return secret; }
293
294 public String[] getCmdLine() {
295 return cmdLine;
296 }
297
298 public ISessionConfig getConfig() {
299 return config;
300 }
301
302 public synchronized InputStream getRawOutput() throws IllegalStateException {
303 if (outputHandler != null) throw new IllegalStateException();
304 return proc.getStdout();
305 }
306 }