|
1 |
|
2 (****************************************************************) |
|
3 (****** Slightly modified version of sml Unix structure *********) |
|
4 (****************************************************************) |
|
5 |
|
6 type signal = Posix.Signal.signal |
|
7 datatype exit_status = datatype Posix.Process.exit_status |
|
8 |
|
9 val fromStatus = Posix.Process.fromStatus |
|
10 |
|
11 |
|
12 |
|
13 (* Internal function - inverse of Posix.Process.fromStatus. *) |
|
14 local |
|
15 val doCall = RunCall.run_call2 RuntimeCalls.POLY_SYS_os_specific |
|
16 in |
|
17 fun toStatus W_EXITED: OS.Process.status = doCall(16, (1, 0)) |
|
18 | toStatus(W_EXITSTATUS w) = doCall(16, (1, Word8.toInt w)) |
|
19 | toStatus(W_SIGNALED s) = |
|
20 doCall(16, (2, SysWord.toInt(Posix.Signal.toWord s))) |
|
21 | toStatus(W_STOPPED s) = |
|
22 doCall(16, (3, SysWord.toInt(Posix.Signal.toWord s))) |
|
23 end |
|
24 |
|
25 (* fun reap{pid, infd, outfd} = |
|
26 let |
|
27 val u = Posix.IO.close infd; |
|
28 val u = Posix.IO.close outfd; |
|
29 val (_, status) = |
|
30 Posix.Process.waitpid(Posix.Process.W_CHILD pid, []) |
|
31 in |
|
32 toStatus status |
|
33 end |
|
34 |
|
35 *) |
|
36 |
|
37 fun reap(pid, instr, outstr) = |
|
38 let |
|
39 val u = TextIO.closeIn instr; |
|
40 val u = TextIO.closeOut outstr; |
|
41 |
|
42 val (_, status) = |
|
43 Posix.Process.waitpid(Posix.Process.W_CHILD pid, []) |
|
44 in |
|
45 toStatus status |
|
46 end |
|
47 |
|
48 fun fdReader (name : string, fd : Posix.IO.file_desc) = |
|
49 Posix.IO.mkReader {initBlkMode = true,name = name,fd = fd }; |
|
50 |
|
51 fun fdWriter (name, fd) = |
|
52 Posix.IO.mkWriter { |
|
53 appendMode = false, |
|
54 initBlkMode = true, |
|
55 name = name, |
|
56 chunkSize=4096, |
|
57 fd = fd |
|
58 }; |
|
59 |
|
60 fun openOutFD (name, fd) = |
|
61 TextIO.mkOutstream ( |
|
62 TextIO.StreamIO.mkOutstream ( |
|
63 fdWriter (name, fd), IO.BLOCK_BUF)); |
|
64 |
|
65 fun openInFD (name, fd) = |
|
66 TextIO.mkInstream ( |
|
67 TextIO.StreamIO.mkInstream ( |
|
68 fdReader (name, fd), "")); |
|
69 |
|
70 |
|
71 |
|
72 |
|
73 |
|
74 (*****************************************) |
|
75 (* The result of calling createWatcher *) |
|
76 (*****************************************) |
|
77 |
|
78 datatype proc = PROC of { |
|
79 pid : Posix.Process.pid, |
|
80 instr : TextIO.instream, |
|
81 outstr : TextIO.outstream |
|
82 }; |
|
83 |
|
84 |
|
85 |
|
86 (*****************************************) |
|
87 (* The result of calling executeToList *) |
|
88 (*****************************************) |
|
89 |
|
90 datatype cmdproc = CMDPROC of { |
|
91 prover: string, (* Name of the resolution prover used, e.g. Vampire, SPASS *) |
|
92 cmd: string, (* The file containing the goal for res prover to prove *) |
|
93 thmstring: string, (* string representation of subgoal after negation, skolemization*) |
|
94 goalstring: string, (* string representation of subgoal*) |
|
95 pid : Posix.Process.pid, |
|
96 instr : TextIO.instream, (* Input stream to child process *) |
|
97 outstr : TextIO.outstream (* Output stream from child process *) |
|
98 }; |
|
99 |
|
100 |
|
101 |
|
102 fun killChild pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill); |
|
103 |
|
104 fun childInfo (PROC{pid,instr,outstr}) = ((pid, (instr,outstr))); |
|
105 |
|
106 fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr); |
|
107 |
|
108 fun cmdInStream (CMDPROC{instr,outstr,...}) = (instr); |
|
109 |
|
110 fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (prover,(cmd,(pid, (instr,outstr)))); |
|
111 |
|
112 fun cmdchildPid (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (pid); |
|
113 |
|
114 fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (prover); |
|
115 |
|
116 fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (thmstring); |
|
117 |
|
118 fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (goalstring); |
|
119 (***************************************************************************) |
|
120 (* Takes a command - e.g. 'vampire', a list of arguments for the command, *) |
|
121 (* and a list of currently running processes. Creates a new process for *) |
|
122 (* cmd and argv and adds it to procList *) |
|
123 (***************************************************************************) |
|
124 |
|
125 |
|
126 |
|
127 |
|
128 fun mySshExecuteToList (cmd, argv, procList) = let |
|
129 val p1 = Posix.IO.pipe () |
|
130 val p2 = Posix.IO.pipe () |
|
131 val prover = hd argv |
|
132 val thmstring = hd(tl argv) |
|
133 val goalstring = hd(tl(tl argv)) |
|
134 val argv = tl (tl argv) |
|
135 |
|
136 (* Turn the arguments into a single string. Perhaps we should quote the |
|
137 arguments. *) |
|
138 fun convArgs [] = [] |
|
139 | convArgs [s] = [s] |
|
140 | convArgs (hd::tl) = hd :: " " :: convArgs tl |
|
141 val cmd_args = concat(convArgs(cmd :: argv)) |
|
142 |
|
143 fun closep () = ( |
|
144 Posix.IO.close (#outfd p1); |
|
145 Posix.IO.close (#infd p1); |
|
146 Posix.IO.close (#outfd p2); |
|
147 Posix.IO.close (#infd p2) |
|
148 ) |
|
149 fun startChild () =(case Posix.Process.fork() |
|
150 of SOME pid => pid (* parent *) |
|
151 | NONE => let |
|
152 val oldchildin = #infd p1 |
|
153 val newchildin = Posix.FileSys.wordToFD 0w0 |
|
154 val oldchildout = #outfd p2 |
|
155 val newchildout = Posix.FileSys.wordToFD 0w1 |
|
156 (*val args = (["shep"]@([cmd]@argv)) |
|
157 val newcmd = "/usr/bin/ssh"*) |
|
158 |
|
159 in |
|
160 Posix.IO.close (#outfd p1); |
|
161 Posix.IO.close (#infd p2); |
|
162 Posix.IO.dup2{old = oldchildin, new = newchildin}; |
|
163 Posix.IO.close oldchildin; |
|
164 Posix.IO.dup2{old = oldchildout, new = newchildout}; |
|
165 Posix.IO.close oldchildout; |
|
166 (* Run the command. *) |
|
167 (* Run this as a shell command. The command and arguments have |
|
168 to be a single argument. *) |
|
169 Posix.Process.exec("/bin/sh", ["sh", "-c", cmd_args]) |
|
170 (*Posix.Process.exec(newcmd, args)*) |
|
171 end |
|
172 (* end case *)) |
|
173 val _ = TextIO.flushOut TextIO.stdOut |
|
174 val pid = (startChild ()) handle ex => (closep(); raise ex) |
|
175 val instr = openInFD ("_exec_in", #infd p2) |
|
176 val outstr = openOutFD ("_exec_out", #outfd p1) |
|
177 val cmd = hd (rev argv) |
|
178 in |
|
179 (* close the child-side fds *) |
|
180 Posix.IO.close (#outfd p2); |
|
181 Posix.IO.close (#infd p1); |
|
182 (* set the fds close on exec *) |
|
183 Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); |
|
184 Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); |
|
185 (((CMDPROC{ |
|
186 prover = prover, |
|
187 cmd = cmd, |
|
188 thmstring = thmstring, |
|
189 goalstring = goalstring, |
|
190 pid = pid, |
|
191 instr = instr, |
|
192 outstr = outstr |
|
193 })::procList)) |
|
194 end; |
|
195 |
|
196 |
|
197 fun myexecuteInEnv (cmd, argv, env) = let |
|
198 val p1 = Posix.IO.pipe () |
|
199 val p2 = Posix.IO.pipe () |
|
200 fun closep () = ( |
|
201 Posix.IO.close (#outfd p1); |
|
202 Posix.IO.close (#infd p1); |
|
203 Posix.IO.close (#outfd p2); |
|
204 Posix.IO.close (#infd p2) |
|
205 ) |
|
206 fun startChild () =(case Posix.Process.fork() |
|
207 of SOME pid => pid (* parent *) |
|
208 | NONE => let |
|
209 val oldchildin = #infd p1 |
|
210 val newchildin = Posix.FileSys.wordToFD 0w0 |
|
211 val oldchildout = #outfd p2 |
|
212 val newchildout = Posix.FileSys.wordToFD 0w1 |
|
213 in |
|
214 Posix.IO.close (#outfd p1); |
|
215 Posix.IO.close (#infd p2); |
|
216 Posix.IO.dup2{old = oldchildin, new = newchildin}; |
|
217 Posix.IO.close oldchildin; |
|
218 Posix.IO.dup2{old = oldchildout, new = newchildout}; |
|
219 Posix.IO.close oldchildout; |
|
220 Posix.Process.exece(cmd, argv, env) |
|
221 end |
|
222 (* end case *)) |
|
223 val _ = TextIO.flushOut TextIO.stdOut |
|
224 val pid = (startChild ()) handle ex => (closep(); raise ex) |
|
225 val instr = openInFD ("_exec_in", #infd p2) |
|
226 val outstr = openOutFD ("_exec_out", #outfd p1) |
|
227 in |
|
228 (* close the child-side fds *) |
|
229 Posix.IO.close (#outfd p2); |
|
230 Posix.IO.close (#infd p1); |
|
231 (* set the fds close on exec *) |
|
232 Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); |
|
233 Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); |
|
234 PROC{pid = pid, |
|
235 instr = instr, |
|
236 outstr = outstr |
|
237 } |
|
238 end; |
|
239 |
|
240 |
|
241 |
|
242 |
|
243 fun myexecuteToList (cmd, argv, procList) = let |
|
244 val p1 = Posix.IO.pipe () |
|
245 val p2 = Posix.IO.pipe () |
|
246 val prover = hd argv |
|
247 val thmstring = hd(tl argv) |
|
248 val goalstring = hd(tl(tl argv)) |
|
249 val argv = tl (tl (tl(argv))) |
|
250 |
|
251 fun closep () = ( |
|
252 Posix.IO.close (#outfd p1); |
|
253 Posix.IO.close (#infd p1); |
|
254 Posix.IO.close (#outfd p2); |
|
255 Posix.IO.close (#infd p2) |
|
256 ) |
|
257 fun startChild () =(case Posix.Process.fork() |
|
258 of SOME pid => pid (* parent *) |
|
259 | NONE => let |
|
260 val oldchildin = #infd p1 |
|
261 val newchildin = Posix.FileSys.wordToFD 0w0 |
|
262 val oldchildout = #outfd p2 |
|
263 val newchildout = Posix.FileSys.wordToFD 0w1 |
|
264 in |
|
265 Posix.IO.close (#outfd p1); |
|
266 Posix.IO.close (#infd p2); |
|
267 Posix.IO.dup2{old = oldchildin, new = newchildin}; |
|
268 Posix.IO.close oldchildin; |
|
269 Posix.IO.dup2{old = oldchildout, new = newchildout}; |
|
270 Posix.IO.close oldchildout; |
|
271 Posix.Process.exec(cmd, argv) |
|
272 end |
|
273 (* end case *)) |
|
274 val _ = TextIO.flushOut TextIO.stdOut |
|
275 val pid = (startChild ()) handle ex => (closep(); raise ex) |
|
276 val instr = openInFD ("_exec_in", #infd p2) |
|
277 val outstr = openOutFD ("_exec_out", #outfd p1) |
|
278 val cmd = hd (rev argv) |
|
279 in |
|
280 (* close the child-side fds *) |
|
281 Posix.IO.close (#outfd p2); |
|
282 Posix.IO.close (#infd p1); |
|
283 (* set the fds close on exec *) |
|
284 Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); |
|
285 Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); |
|
286 (((CMDPROC{ |
|
287 prover = prover, |
|
288 cmd = cmd, |
|
289 thmstring = thmstring, |
|
290 goalstring = goalstring, |
|
291 pid = pid, |
|
292 instr = instr, |
|
293 outstr = outstr |
|
294 })::procList)) |
|
295 end; |