Line data Source code
1 : // Author(s): Thomas Neele
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file child_process.cpp
10 :
11 : #include "mcrl2/smt/child_process.h"
12 : #include "mcrl2/utilities/exception.h"
13 : #include "mcrl2/utilities/platform.h"
14 :
15 : #ifdef MCRL2_PLATFORM_WINDOWS
16 : #include <windows.h>
17 : #include <tchar.h>
18 : #include <cstdio>
19 : #include <strsafe.h>
20 : #else
21 : #include <unistd.h>
22 : #include <sys/select.h>
23 : #include <sys/wait.h>
24 : #endif // MCRL2_PLATFORM_WINDOWS
25 :
26 : #include <cstring>
27 : #include <csignal>
28 : #include <cerrno>
29 :
30 :
31 : namespace mcrl2
32 : {
33 : namespace smt
34 : {
35 :
36 : #ifdef MCRL2_PLATFORM_WINDOWS
37 :
38 : struct child_process::platform_impl
39 : {
40 : HANDLE g_hChildStd_IN_Rd = NULL;
41 : HANDLE g_hChildStd_IN_Wr = NULL;
42 : HANDLE g_hChildStd_OUT_Rd = NULL;
43 : HANDLE g_hChildStd_OUT_Wr = NULL;
44 : };
45 :
46 : void child_process::write(const std::string& command) const
47 : {
48 : DWORD dwWritten;
49 : BOOL bSuccess = FALSE;
50 :
51 : bSuccess = WriteFile(m_pimpl->g_hChildStd_IN_Wr, command.c_str(), static_cast<DWORD>(command.size()), &dwWritten, NULL);
52 : if(!bSuccess || dwWritten != command.size())
53 : {
54 : throw mcrl2::runtime_error("Failed to write SMT problem to the solver.\n" + command);
55 : }
56 : }
57 :
58 :
59 : std::string child_process::read() const
60 : {
61 : DWORD dwRead, totalRead;
62 : CHAR output[512];
63 : BOOL bSuccess = FALSE;
64 :
65 : totalRead = 0;
66 : do
67 : {
68 : bSuccess = ReadFile( m_pimpl->g_hChildStd_OUT_Rd, output + totalRead, 512 - totalRead, &dwRead, NULL);
69 : totalRead += dwRead;
70 : } while(bSuccess && output[totalRead-1] != '\n');
71 : if(!bSuccess || totalRead == 0 )
72 : {
73 : throw mcrl2::runtime_error("Reading from child process " + m_name + " failed.");
74 : }
75 : return std::string(output, totalRead);
76 : }
77 :
78 : std::string child_process::read(const std::chrono::microseconds& timeout) const
79 : {
80 : // Not implemented on Windows
81 : return read();
82 : }
83 :
84 : void child_process::send_sigint() const
85 : {
86 : // Not implemented on Windows
87 : }
88 :
89 : void child_process::initialize()
90 : {
91 : m_pimpl = std::make_shared<child_process::platform_impl>();
92 : SECURITY_ATTRIBUTES saAttr;
93 : // Set the bInheritHandle flag so pipe handles are inherited.
94 : saAttr.nLength = sizeof(SECURITY_ATTRIBUTES);
95 : saAttr.bInheritHandle = TRUE;
96 : saAttr.lpSecurityDescriptor = NULL;
97 :
98 : // Create a pipe for the child process's STDOUT.
99 : if (!CreatePipe(&m_pimpl->g_hChildStd_OUT_Rd, &m_pimpl->g_hChildStd_OUT_Wr, &saAttr, 0))
100 : {
101 : throw mcrl2::runtime_error("Could not connect to SMT solver: failed to create pipe Stdout");
102 : }
103 : // Ensure the read handle to the pipe for STDOUT is not inherited.
104 : if(!SetHandleInformation(m_pimpl->g_hChildStd_OUT_Rd, HANDLE_FLAG_INHERIT, 0))
105 : {
106 : throw mcrl2::runtime_error("Could not modify SMT solver handle: SetHandleInformation Stdout");
107 : }
108 : // Create a pipe for the child process's STDIN.
109 : if(!CreatePipe(&m_pimpl->g_hChildStd_IN_Rd, &m_pimpl->g_hChildStd_IN_Wr, &saAttr, 0))
110 : {
111 : throw mcrl2::runtime_error("Could not connect to SMT solver: failed to create pipe Stdin");
112 : }
113 : // Ensure the write handle to the pipe for STDIN is not inherited.
114 : if(!SetHandleInformation(m_pimpl->g_hChildStd_IN_Wr, HANDLE_FLAG_INHERIT, 0))
115 : {
116 : throw mcrl2::runtime_error("Could not modify SMT solver handle: SetHandleInformation Stdin");
117 : }
118 : // Create the child process.
119 : TCHAR szCmdline[] = TEXT("z3.exe -smt2 -in");
120 : PROCESS_INFORMATION piProcInfo;
121 : STARTUPINFO siStartInfo;
122 : BOOL bSuccess = FALSE;
123 :
124 : // Set up members of the PROCESS_INFORMATION structure.
125 : ZeroMemory(&piProcInfo, sizeof(PROCESS_INFORMATION));
126 :
127 : // Set up members of the STARTUPINFO structure.
128 : // This structure specifies the STDIN and STDOUT handles for redirection.
129 : ZeroMemory(&siStartInfo, sizeof(STARTUPINFO));
130 : siStartInfo.cb = sizeof(STARTUPINFO);
131 : siStartInfo.hStdError = m_pimpl->g_hChildStd_OUT_Wr;
132 : siStartInfo.hStdOutput = m_pimpl->g_hChildStd_OUT_Wr;
133 : siStartInfo.hStdInput = m_pimpl->g_hChildStd_IN_Rd;
134 : siStartInfo.dwFlags |= STARTF_USESTDHANDLES;
135 :
136 : // Create the child process.
137 : bSuccess = CreateProcess(NULL,
138 : szCmdline, // command line
139 : NULL, // process security attributes
140 : NULL, // primary thread security attributes
141 : TRUE, // handles are inherited
142 : 0, // creation flags
143 : NULL, // use parent's environment
144 : NULL, // use parent's current directory
145 : &siStartInfo, // STARTUPINFO pointer
146 : &piProcInfo); // receives PROCESS_INFORMATION
147 :
148 : // If an error occurs, exit the application.
149 : if(!bSuccess)
150 : {
151 : throw mcrl2::runtime_error("Problem occurred while creating SMT solver process.\nIs " + m_name + " in your path?");
152 : }
153 : else
154 : {
155 : // Close handles to the child process and its primary thread.
156 : // Some applications might keep these handles to monitor the status
157 : // of the child process, for example.
158 : CloseHandle(piProcInfo.hProcess);
159 : CloseHandle(piProcInfo.hThread);
160 : }
161 : }
162 :
163 : child_process::~child_process()
164 : {
165 : // Clean up the child process
166 : // It terminates when we close its stdin
167 : CloseHandle(m_pimpl->g_hChildStd_IN_Wr);
168 : }
169 :
170 :
171 : #else // MCRL2_PLATFORM_WINDOWS
172 :
173 : struct child_process::platform_impl
174 : {
175 : pid_t child_pid;
176 : int pipe_stdin[2];
177 : int pipe_stdout[2];
178 : int pipe_stderr[2];
179 : };
180 :
181 0 : void child_process::write(const std::string& command) const
182 : {
183 0 : if(::write(m_pimpl->pipe_stdin[1], command.c_str(), command.size()) < 0)
184 : {
185 0 : throw mcrl2::runtime_error("Failed to write to " + m_name + ".\n" + command);
186 : }
187 0 : }
188 :
189 0 : std::string child_process::read() const
190 : {
191 : char output[512];
192 : // check return value
193 0 : int count = ::read(m_pimpl->pipe_stdout[0], output, 512);
194 0 : if(count > 0)
195 : {
196 0 : return std::string(output, count);
197 : }
198 : else
199 : {
200 0 : std::string message;
201 :
202 0 : while(int i = ::read(m_pimpl->pipe_stderr[0], output, 512))
203 : {
204 0 : message.append(output, 0, i);
205 0 : }
206 :
207 0 : throw mcrl2::runtime_error("Reading from child process " + m_name + " failed: " + message);
208 0 : }
209 : }
210 :
211 0 : std::string child_process::read(const std::chrono::microseconds& timeout) const
212 : {
213 : struct timeval tv;
214 0 : tv.tv_sec = 0;
215 0 : tv.tv_usec = timeout.count();
216 :
217 : fd_set readfds;
218 0 : FD_ZERO(&readfds);
219 0 : FD_SET(m_pimpl->pipe_stdout[0], &readfds);
220 :
221 0 : int result = ::select(m_pimpl->pipe_stdout[0] + 1, &readfds, NULL, NULL, &tv);
222 :
223 0 : if(result == -1)
224 : {
225 0 : throw mcrl2::runtime_error("Error while waiting for input from " + m_name);
226 : }
227 0 : else if(result == 0)
228 : {
229 0 : send_sigint();
230 : }
231 0 : return read();
232 : }
233 :
234 0 : void child_process::send_sigint() const
235 : {
236 0 : ::kill(m_pimpl->child_pid, SIGINT);
237 0 : }
238 :
239 0 : void child_process::initialize()
240 : {
241 0 : signal(SIGPIPE, SIG_IGN);
242 0 : m_pimpl = std::make_shared<child_process::platform_impl>();
243 : // Create pipes (two pairs r/w)
244 0 : if (::pipe(&m_pimpl->pipe_stdin[0]) < 0)
245 : {
246 0 : throw mcrl2::runtime_error("failed to create pipe");
247 : }
248 :
249 0 : if (::pipe(&m_pimpl->pipe_stdout[0]) < 0)
250 : {
251 0 : throw mcrl2::runtime_error("failed to create pipe");
252 : }
253 :
254 0 : if (::pipe(&m_pimpl->pipe_stderr[0]) < 0)
255 : {
256 0 : throw mcrl2::runtime_error("failed to create pipe");
257 : }
258 :
259 : // fork process
260 0 : pid_t pid = ::fork();
261 0 : if (pid == 0)
262 : {
263 : // Forked process keeps waiting for input
264 0 : ::dup2(m_pimpl->pipe_stdin[0], STDIN_FILENO);
265 0 : ::dup2(m_pimpl->pipe_stdout[1], STDOUT_FILENO);
266 0 : ::dup2(m_pimpl->pipe_stderr[1], STDERR_FILENO);
267 :
268 0 : ::close(m_pimpl->pipe_stdin[1]);
269 0 : ::close(m_pimpl->pipe_stdout[0]);
270 0 : ::close(m_pimpl->pipe_stderr[0]);
271 :
272 0 : ::execlp("z3", "z3", "-smt2", "-in", (char*) nullptr);
273 :
274 0 : ::_exit(errno);
275 : }
276 0 : else if (pid < 0)
277 : {
278 0 : ::close(m_pimpl->pipe_stdin[0]);
279 0 : ::close(m_pimpl->pipe_stdin[1]);
280 0 : ::close(m_pimpl->pipe_stdout[0]);
281 0 : ::close(m_pimpl->pipe_stdout[1]);
282 0 : ::close(m_pimpl->pipe_stderr[0]);
283 0 : ::close(m_pimpl->pipe_stderr[1]);
284 :
285 0 : throw mcrl2::runtime_error("Problem occurred while forking SMT solver process: " + std::string(strerror(errno)) + ".\nIs " + m_name + " in your path?");
286 : }
287 : else
288 : {
289 0 : m_pimpl->child_pid = pid;
290 0 : ::close(m_pimpl->pipe_stdin[0]);
291 0 : ::close(m_pimpl->pipe_stdout[1]);
292 0 : ::close(m_pimpl->pipe_stderr[1]);
293 : }
294 0 : }
295 :
296 0 : child_process::~child_process()
297 : {
298 : // Clean up the child process
299 : // It terminates when we close its stdin
300 0 : ::close(m_pimpl->pipe_stdin[1]);
301 0 : ::close(m_pimpl->pipe_stdout[0]);
302 0 : ::close(m_pimpl->pipe_stderr[0]);
303 :
304 : int return_status;
305 0 : ::wait(&return_status);
306 0 : }
307 :
308 : #endif // MCRL2_PLATFORM_WINDOWS
309 :
310 :
311 : } // namespace smt
312 : } // namespace mcrl2
|
