cprover
Loading...
Searching...
No Matches
piped_process.cpp
Go to the documentation of this file.
1
4
5// NOTES ON WINDOWS PIPES IMPLEMENTATION
6//
7// This is a note to explain the choices related to the Windows pipes
8// implementation and to serve as information for future work on the
9// Windows parts of this class.
10//
11// Windows supports two kinds of pipes: anonymous and named.
12//
13// Anonymous pipes can only operate in blocking mode. This is a problem for
14// this class because blocking mode pipes (on Windows) will not allow the
15// other end to read until the process providing the data has terminated.
16// (You might think that this is not necessary, but in practice this is
17// the case.) For example, if we ran
18// echo The Jabberwocky; ping 127.0.0.1 -n 6 >nul
19// on the command line in Windows we would see the string "The Jabberwocky"
20// immediately, and then the command would end about 6 seconds later after the
21// pings complete. However, a blocking pipe will see nothing until the ping
22// command has finished, even if the echo has completed and (supposedly)
23// written to the pipe.
24//
25// For the above reason, we NEED to be able to use non-blocking pipes. Since
26// anonymous pipes cannot be non-blocking (in theory they have a named pipe
27// underneath, but it's not clear you could hack this to be non-blocking
28// safely), we have to use named pipes.
29//
30// Named pipes can be non-blocking and this is how we create them.
31//
32// Aside on security:
33// Named pipes can be connected to by other processes and here we have NOT
34// gone deep into the security handling. The default used here is to allow
35// access from the same session token/permissions. This SHOULD be sufficient
36// for what we need.
37//
38// Non-blocking pipes allow immediate reading of any data on the pipe which
39// matches the Linux/MacOS pipe behaviour and also allows reading of the
40// string "The Jabberwocky" from the example above before waiting for the ping
41// command to terminate. This reading can be done with any of the usual pipe
42// read/peek functions, so we use those.
43//
44// There is one problem with the approach used here, that there is no Windows
45// function that can wait on a non-blocking pipe. There are a few options that
46// appear like they would work (or claim they work). Details on these and why
47// they don't work are over-viewed here:
48// - WaitCommEvent claims it can wait for events on a handle (e.g. char
49// written) which would be perfect. Unfortunately on a non-blocking pipe
50// this returns immediately. Using this on a blocking pipe fails to detect
51// that a character is written until the other process terminates in the
52// example above, making this ineffective for what we want.
53// - Setting the pipe timeout or changing blocking after creation. This is
54// theoretically possible, but in practice either has no effect, or can
55// cause a segmentation fault. This was attempted with the SetCommTimeouts
56// function and cause segfault.
57// - Using a wait for event function (e.g. WaitForMultipleObjects, also single
58// object, event, etc.). These can in theory wait until an event, but have
59// the problem that with non-blocking pipes, the wait will not happen since
60// they return immediately. One might think they can work with a blocking
61// pipe and a timeout (i.e. have a blocking read and a timeout thread and
62// wait for one of them to happen to see if there is something to read or
63// whether we could timeout). However, while this can create the right
64// wait and timeout behaviour, since the underlying pipe is blocking this
65// means the example above cannot read "The Jabberwocky" until the ping has
66// finished, again undoing the interactive behaviour desired.
67// Since none of the above work effectivley, the chosen approach is to use a
68// non-blocking peek to see if there is anthing to read, and use a sleep and
69// poll behaviour that might be much busier than we want. At the time of
70// writing this has not been made smart, just a first choice option for how
71// frequently to poll.
72//
73// Conclusion
74// The implementation is written this way to mitigate the problems with what
75// can and cannot be done with Windows pipes. It's not always pretty, but it
76// does work and handles what we want.
77
78#ifdef _WIN32
79# include "run.h" // for Windows arg quoting
80# include "unicode.h" // for widen function
81# include <tchar.h> // library for _tcscpy function
82# include <util/make_unique.h>
83# include <windows.h>
84#else
85# include <fcntl.h> // library for fcntl function
86# include <poll.h> // library for poll function
87# include <signal.h> // library for kill function
88# include <unistd.h> // library for read/write/sleep/etc. functions
89#endif
90
91#include "exception_utils.h"
92#include "invariant.h"
93#include "narrow.h"
94#include "optional.h"
95#include "piped_process.h"
96
97#include <cstring> // library for strerror function (on linux)
98#include <iostream>
99#include <vector>
100
101#ifdef _WIN32
102# define BUFSIZE (1024 * 64)
103#else
104# define BUFSIZE 2048
105#endif
106
107#ifdef _WIN32
113static std::wstring
114prepare_windows_command_line(const std::vector<std::string> &commandvec)
115{
116 std::wstring result = widen(commandvec[0]);
117 for(int i = 1; i < commandvec.size(); i++)
118 {
119 result.append(L" ");
120 result.append(quote_windows_arg(widen(commandvec[i])));
121 }
122 return result;
123}
124#endif
125
127 const std::vector<std::string> &commandvec,
128 message_handlert &message_handler)
129 : log{message_handler}
130{
131# ifdef _WIN32
132 // Security attributes for pipe creation
133 SECURITY_ATTRIBUTES sec_attr;
134 sec_attr.nLength = sizeof(SECURITY_ATTRIBUTES);
135 // Ensure pipes are inherited
136 sec_attr.bInheritHandle = TRUE;
137 // This sets the security to the default for the current session access token
138 // See following link for details
139 // https://docs.microsoft.com/en-us/previous-versions/windows/desktop/legacy/aa379560(v=vs.85) //NOLINT
140 sec_attr.lpSecurityDescriptor = NULL;
141 // Use named pipes to allow non-blocking read
142 // Build the base name for the pipes
143 std::string base_name = "\\\\.\\pipe\\cbmc\\child\\";
144 // Use process ID as a unique ID for this process at this time.
145 base_name.append(std::to_string(GetCurrentProcessId()));
146 const std::string in_name = base_name + "\\IN";
147 child_std_IN_Wr = CreateNamedPipe(
148 in_name.c_str(),
149 PIPE_ACCESS_OUTBOUND, // Writing for us
150 PIPE_TYPE_BYTE | PIPE_NOWAIT, // Bytes and non-blocking
151 PIPE_UNLIMITED_INSTANCES, // Probably doesn't matter
152 BUFSIZE,
153 BUFSIZE, // Output and input bufffer sizes
154 0, // Timeout in ms, 0 = use system default
155 // This is the timeout that WaitNamedPipe functions will wait to try
156 // and connect before aborting if no instance of the pipe is available.
157 // In practice this is not used since we connect immediately and only
158 // use one instance (no waiting for a free instance).
159 &sec_attr); // For inheritance by child
160 if(child_std_IN_Rd == INVALID_HANDLE_VALUE)
161 {
162 throw system_exceptiont("Input pipe creation failed for child_std_IN_Rd");
163 }
164 // Connect to the other side of the pipe
165 child_std_IN_Rd = CreateFile(
166 in_name.c_str(),
167 GENERIC_READ, // Read side
168 FILE_SHARE_READ | FILE_SHARE_WRITE, // Shared read/write
169 &sec_attr, // Need this for inherit
170 OPEN_EXISTING, // Opening other end
171 FILE_ATTRIBUTE_NORMAL | FILE_FLAG_NO_BUFFERING, // Normal, but don't buffer
172 NULL);
173 if(child_std_IN_Wr == INVALID_HANDLE_VALUE)
174 {
175 throw system_exceptiont("Input pipe creation failed for child_std_IN_Wr");
176 }
177 if(!SetHandleInformation(
178 child_std_IN_Rd, HANDLE_FLAG_INHERIT, HANDLE_FLAG_INHERIT))
179 {
180 throw system_exceptiont(
181 "Input pipe creation failed on SetHandleInformation");
182 }
183 const std::string out_name = base_name + "\\OUT";
184 child_std_OUT_Rd = CreateNamedPipe(
185 out_name.c_str(),
186 PIPE_ACCESS_INBOUND, // Reading for us
187 PIPE_TYPE_BYTE | PIPE_NOWAIT, // Bytes and non-blocking
188 PIPE_UNLIMITED_INSTANCES, // Probably doesn't matter
189 BUFSIZE,
190 BUFSIZE, // Output and input bufffer sizes
191 0, // Timeout in ms, 0 = use system default
192 &sec_attr); // For inheritance by child
193 if(child_std_OUT_Rd == INVALID_HANDLE_VALUE)
194 {
195 throw system_exceptiont("Output pipe creation failed for child_std_OUT_Rd");
196 }
197 child_std_OUT_Wr = CreateFile(
198 out_name.c_str(),
199 GENERIC_WRITE, // Write side
200 FILE_SHARE_READ | FILE_SHARE_WRITE, // Shared read/write
201 &sec_attr, // Need this for inherit
202 OPEN_EXISTING, // Opening other end
203 FILE_ATTRIBUTE_NORMAL | FILE_FLAG_NO_BUFFERING, // Normal, but don't buffer
204 NULL);
205 if(child_std_OUT_Wr == INVALID_HANDLE_VALUE)
206 {
207 throw system_exceptiont("Output pipe creation failed for child_std_OUT_Wr");
208 }
209 if(!SetHandleInformation(child_std_OUT_Rd, HANDLE_FLAG_INHERIT, 0))
210 {
211 throw system_exceptiont(
212 "Output pipe creation failed on SetHandleInformation");
213 }
214 // Create the child process
215 STARTUPINFOW start_info;
217 ZeroMemory(proc_info.get(), sizeof(PROCESS_INFORMATION));
218 ZeroMemory(&start_info, sizeof(STARTUPINFOW));
219 start_info.cb = sizeof(STARTUPINFOW);
220 start_info.hStdError = child_std_OUT_Wr;
221 start_info.hStdOutput = child_std_OUT_Wr;
222 start_info.hStdInput = child_std_IN_Rd;
223 start_info.dwFlags |= STARTF_USESTDHANDLES;
224 const std::wstring cmdline = prepare_windows_command_line(commandvec);
225 // Note that we do NOT free this since it becomes part of the child
226 // and causes heap corruption in Windows if we free!
227 const BOOL success = CreateProcessW(
228 NULL, // application name, we only use the command below
229 _wcsdup(cmdline.c_str()), // command line
230 NULL, // process security attributes
231 NULL, // primary thread security attributes
232 TRUE, // handles are inherited
233 0, // creation flags
234 NULL, // use parent's environment
235 NULL, // use parent's current directory
236 &start_info, // STARTUPINFO pointer
237 proc_info.get()); // receives PROCESS_INFORMATION
238 // Close handles to the stdin and stdout pipes no longer needed by the
239 // child process. If they are not explicitly closed, there is no way to
240 // recognize that the child process has ended (but maybe we don't care).
241 CloseHandle(child_std_OUT_Wr);
242 CloseHandle(child_std_IN_Rd);
243 if(!success)
244 throw system_exceptiont("Process creation failed.");
245# else
246
247 if(pipe(pipe_input) == -1)
248 {
249 throw system_exceptiont("Input pipe creation failed");
250 }
251
252 if(pipe(pipe_output) == -1)
253 {
254 throw system_exceptiont("Output pipe creation failed");
255 }
256
257
258 if(fcntl(pipe_output[0], F_SETFL, O_NONBLOCK) < 0)
259 {
260 throw system_exceptiont("Setting pipe non-blocking failed");
261 }
262
263 // Create a new process for the child that will execute the
264 // command and receive information via pipes.
265 child_process_id = fork();
266 if(child_process_id == 0)
267 {
268 // child process here
269
270 // Close pipes that will be used by the parent so we do
271 // not have our own copies and conflicts.
272 close(pipe_input[1]);
273 close(pipe_output[0]);
274
275 // Duplicate pipes so we have the ones we need.
276 dup2(pipe_input[0], STDIN_FILENO);
277 dup2(pipe_output[1], STDOUT_FILENO);
278 dup2(pipe_output[1], STDERR_FILENO);
279
280 // Create a char** for the arguments plus a NULL terminator (by convention,
281 // the first "argument" is the command itself)
282 char **args = reinterpret_cast<char **>(
283 malloc((commandvec.size() + 1) * sizeof(char *)));
284 // Add all the arguments to the args array of char *.
285 unsigned long i = 0;
286 while(i < commandvec.size())
287 {
288 args[i] = strdup(commandvec[i].c_str());
289 i++;
290 }
291 args[i] = NULL;
292 execvp(commandvec[0].c_str(), args);
293 // The args variable will be handled by the OS if execvp succeeds, but
294 // if execvp fails then we should free it here (just in case the runtime
295 // error below continues execution.)
296 while(i > 0)
297 {
298 i--;
299 free(args[i]);
300 }
301 free(args);
302 // Only reachable if execvp failed
303 // Note that here we send to std::cerr since we are in the child process
304 // here and this is received by the parent process.
305 std::cerr << "Launching " << commandvec[0]
306 << " failed with error: " << std::strerror(errno) << std::endl;
307 abort();
308 }
309 else
310 {
311 // parent process here
312 // Close pipes to be used by the child process
313 close(pipe_input[0]);
314 close(pipe_output[1]);
315
316 // Get stream for sending to the child process
317 command_stream = fdopen(pipe_input[1], "w");
318 }
319# endif
320 process_state = statet::RUNNING;
321}
322
324{
325# ifdef _WIN32
326 TerminateProcess(proc_info->hProcess, 0);
327 // Disconnecting the pipes also kicks the client off, it should be killed
328 // by now, but this will also force the client off.
329 // Note that pipes are cleaned up by Windows when all handles to the pipe
330 // are closed. Disconnect may be superfluous here.
331 DisconnectNamedPipe(child_std_OUT_Rd);
332 DisconnectNamedPipe(child_std_IN_Wr);
333 CloseHandle(child_std_OUT_Rd);
334 CloseHandle(child_std_IN_Wr);
335 CloseHandle(proc_info->hProcess);
336 CloseHandle(proc_info->hThread);
337# else
338 // Close the parent side of the remaining pipes
339 fclose(command_stream);
340 // Note that the above will call close(pipe_input[1]);
341 close(pipe_output[0]);
342 // Send signal to the child process to terminate
343 kill(child_process_id, SIGTERM);
344# endif
345}
346
349{
350 if(process_state != statet::RUNNING)
351 {
353 }
354#ifdef _WIN32
355 const auto message_size = narrow<DWORD>(message.size());
356 PRECONDITION(message_size > 0);
357 DWORD bytes_written = 0;
358 const int retry_limit = 10;
359 for(int send_attempts = 0; send_attempts < retry_limit; ++send_attempts)
360 {
361 // `WriteFile` can return a success status but write 0 bytes if we write
362 // messages quickly enough. This problem has been observed when using a
363 // release build, but resolved when using a debug build or `--verbosity 10`.
364 // Presumably this happens if cbmc gets too far ahead of the sub process.
365 // Flushing the buffer and retrying should then succeed to write the message
366 // in this case.
367 if(!WriteFile(
368 child_std_IN_Wr, message.c_str(), message_size, &bytes_written, NULL))
369 {
370 const DWORD error_code = GetLastError();
371 log.debug() << "Last error code is " + std::to_string(error_code)
372 << messaget::eom;
374 }
375 if(bytes_written != 0)
376 break;
377 // Give the sub-process chance to read the waiting message(s).
378 const auto wait_milliseconds = narrow<DWORD>(1 << send_attempts);
379 log.debug() << "Zero bytes send to sub process. Retrying in "
380 << wait_milliseconds << " milliseconds." << messaget::eom;
381 FlushFileBuffers(child_std_IN_Wr);
382 Sleep(wait_milliseconds);
383 }
384 INVARIANT(
385 message_size == bytes_written,
386 "Number of bytes written to sub process must match message size."
387 "Message size is " +
388 std::to_string(message_size) + " but " + std::to_string(bytes_written) +
389 " bytes were written.");
390#else
391 // send message to solver process
392 int send_status = fputs(message.c_str(), command_stream);
393 fflush(command_stream);
394
395 if(send_status == EOF)
396 {
398 }
399# endif
401}
402
404{
405 INVARIANT(
406 process_state == statet::RUNNING,
407 "Can only receive() from a fully initialised process");
408 std::string response = std::string("");
409 char buff[BUFSIZE];
410 bool success = true;
411#ifdef _WIN32
412 DWORD nbytes;
413#else
414 int nbytes;
415#endif
416 while(success)
417 {
418#ifdef _WIN32
419 success = ReadFile(child_std_OUT_Rd, buff, BUFSIZE, &nbytes, NULL);
420#else
421 nbytes = read(pipe_output[0], buff, BUFSIZE);
422 // Added the status back in here to keep parity with old implementation
423 // TODO: check which statuses are really used/needed.
424 if(nbytes == 0) // Update if the pipe is stopped
425 process_state = statet::ERRORED;
426 success = nbytes > 0;
427#endif
428 INVARIANT(
429 nbytes < BUFSIZE,
430 "More bytes cannot be read at a time, than the size of the buffer");
431 if(nbytes > 0)
432 {
433 response.append(buff, nbytes);
434 }
435 }
436 return response;
437}
438
440{
441 // can_receive(PIPED_PROCESS_INFINITE_TIMEOUT) waits an ubounded time until
442 // there is some data
444 return receive();
445}
446
451
453{
454 // unwrap the optional argument here
455 const int timeout = wait_time ? narrow<int>(*wait_time) : -1;
456#ifdef _WIN32
457 int waited_time = 0;
458 DWORD total_bytes_available = 0;
459 while(timeout < 0 || waited_time >= timeout)
460 {
461 const LPVOID lpBuffer = nullptr;
462 const DWORD nBufferSize = 0;
463 const LPDWORD lpBytesRead = nullptr;
464 const LPDWORD lpTotalBytesAvail = &total_bytes_available;
465 const LPDWORD lpBytesLeftThisMessage = nullptr;
466 PeekNamedPipe(
467 child_std_OUT_Rd,
468 lpBuffer,
469 nBufferSize,
470 lpBytesRead,
471 lpTotalBytesAvail,
472 lpBytesLeftThisMessage);
473 if(total_bytes_available > 0)
474 {
475 return true;
476 }
477// TODO make this define and choice better
478# define WIN_POLL_WAIT 10
479 Sleep(WIN_POLL_WAIT);
480 waited_time += WIN_POLL_WAIT;
481 }
482#else
483 struct pollfd fds // NOLINT
484 {
485 pipe_output[0], POLLIN, 0
486 };
487 nfds_t nfds = POLLIN;
488 const int ready = poll(&fds, nfds, timeout);
489
490 switch(ready)
491 {
492 case -1:
493 // Error case
494 // Further error handling could go here
495 process_state = statet::ERRORED;
496 // fallthrough intended
497 case 0:
498 // Timeout case
499 // Do nothing for timeout and error fallthrough, default function behaviour
500 // is to return false.
501 break;
502 default:
503 // Found some events, check for POLLIN
504 if(fds.revents & POLLIN)
505 {
506 // we can read from the pipe here
507 return true;
508 }
509 // Some revent we did not ask for or check for, can't read though.
510 }
511# endif
512 return false;
513}
514
516{
517 return can_receive(0);
518}
519
521{
522 while(process_state == statet::RUNNING && !can_receive(0))
523 {
524#ifdef _WIN32
525 Sleep(wait_time);
526#else
527 usleep(wait_time);
528#endif
529 }
530}
mstreamt & debug() const
Definition message.h:429
static eomt eom
Definition message.h:297
bool can_receive()
See if this process can receive data from the other process.
void wait_receivable(int wait_time)
Wait for the pipe to be ready, waiting specified time between checks.
std::string receive()
Read a string from the child process' output.
send_responset send(const std::string &message)
Send a string message (command) to the child process.
statet
Enumeration to keep track of child process state.
piped_processt(const std::vector< std::string > &commandvec, message_handlert &message_handler)
Initiate a new subprocess with pipes supporting communication between the parent (this process) and t...
statet get_status()
Get child process status.
send_responset
Enumeration for send response.
std::string wait_receive()
Wait until a string is available and read a string from the child process' output.
Thrown when some external system fails unexpectedly.
#define TRUE
Definition driver.h:7
#define BUFSIZE
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
output_type narrow(input_type input)
Run-time checked narrowing cast.
Definition narrow.h:34
#define NODISCARD
Definition nodiscard.h:22
nonstd::optional< T > optionalt
Definition optional.h:35
Subprocess communication with pipes.
#define PIPED_PROCESS_INFINITE_TIMEOUT
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
std::wstring widen(const char *s)
Definition unicode.cpp:49