cprover
piped_process.cpp
Go to the documentation of this file.
1 
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 <cstring> // library for strerror function (on linux)
92 # include <iostream>
93 # include <vector>
94 
95 # include "exception_utils.h"
96 # include "invariant.h"
97 # include "narrow.h"
98 # include "optional.h"
99 # include "piped_process.h"
100 # include "string_utils.h"
101 
102 # define BUFSIZE 2048
103 
104 #ifdef _WIN32
110 static std::wstring
111 prepare_windows_command_line(const std::vector<std::string> &commandvec)
112 {
113  std::wstring result = widen(commandvec[0]);
114  for(int i = 1; i < commandvec.size(); i++)
115  {
116  result.append(L" ");
117  result.append(quote_windows_arg(widen(commandvec[i])));
118  }
119  return result;
120 }
121 #endif
122 
123 piped_processt::piped_processt(const std::vector<std::string> &commandvec)
124 {
125 # ifdef _WIN32
126  // Security attributes for pipe creation
127  SECURITY_ATTRIBUTES sec_attr;
128  sec_attr.nLength = sizeof(SECURITY_ATTRIBUTES);
129  // Ensure pipes are inherited
130  sec_attr.bInheritHandle = TRUE;
131  // This sets the security to the default for the current session access token
132  // See following link for details
133  // https://docs.microsoft.com/en-us/previous-versions/windows/desktop/legacy/aa379560(v=vs.85) //NOLINT
134  sec_attr.lpSecurityDescriptor = NULL;
135  // Use named pipes to allow non-blocking read
136  // Build the base name for the pipes
137  std::string base_name = "\\\\.\\pipe\\cbmc\\child\\";
138  // Use process ID as a unique ID for this process at this time.
139  base_name.append(std::to_string(GetCurrentProcessId()));
140  const std::string in_name = base_name + "\\IN";
141  child_std_IN_Rd = CreateNamedPipe(
142  in_name.c_str(),
143  PIPE_ACCESS_INBOUND, // Reading for us
144  PIPE_TYPE_BYTE | PIPE_NOWAIT, // Bytes and non-blocking
145  PIPE_UNLIMITED_INSTANCES, // Probably doesn't matter
146  BUFSIZE,
147  BUFSIZE, // Output and input bufffer sizes
148  0, // Timeout in ms, 0 = use system default
149  // This is the timeout that WaitNamedPipe functions will wait to try
150  // and connect before aborting if no instance of the pipe is available.
151  // In practice this is not used since we connect immediately and only
152  // use one instance (no waiting for a free instance).
153  &sec_attr); // For inheritance by child
154  if(child_std_IN_Rd == INVALID_HANDLE_VALUE)
155  {
156  throw system_exceptiont("Input pipe creation failed for child_std_IN_Rd");
157  }
158  // Connect to the other side of the pipe
159  child_std_IN_Wr = CreateFileA(
160  in_name.c_str(),
161  GENERIC_WRITE, // Write side
162  FILE_SHARE_READ | FILE_SHARE_WRITE, // Shared read/write
163  &sec_attr, // Need this for inherit
164  OPEN_EXISTING, // Opening other end
165  FILE_ATTRIBUTE_NORMAL | FILE_FLAG_NO_BUFFERING, // Normal, but don't buffer
166  NULL);
167  if(child_std_IN_Wr == INVALID_HANDLE_VALUE)
168  {
169  throw system_exceptiont("Input pipe creation failed for child_std_IN_Wr");
170  }
171  if(!SetHandleInformation(child_std_IN_Rd, HANDLE_FLAG_INHERIT, 0))
172  {
173  throw system_exceptiont(
174  "Input pipe creation failed on SetHandleInformation");
175  }
176  const std::string out_name = base_name + "\\OUT";
177  child_std_OUT_Rd = CreateNamedPipe(
178  out_name.c_str(),
179  PIPE_ACCESS_INBOUND, // Reading for us
180  PIPE_TYPE_BYTE | PIPE_NOWAIT, // Bytes and non-blocking
181  PIPE_UNLIMITED_INSTANCES, // Probably doesn't matter
182  BUFSIZE,
183  BUFSIZE, // Output and input bufffer sizes
184  0, // Timeout in ms, 0 = use system default
185  &sec_attr); // For inheritance by child
186  if(child_std_OUT_Rd == INVALID_HANDLE_VALUE)
187  {
188  throw system_exceptiont("Output pipe creation failed for child_std_OUT_Rd");
189  }
190  child_std_OUT_Wr = CreateFileA(
191  out_name.c_str(),
192  GENERIC_WRITE, // Write side
193  FILE_SHARE_READ | FILE_SHARE_WRITE, // Shared read/write
194  &sec_attr, // Need this for inherit
195  OPEN_EXISTING, // Opening other end
196  FILE_ATTRIBUTE_NORMAL | FILE_FLAG_NO_BUFFERING, // Normal, but don't buffer
197  NULL);
198  if(child_std_OUT_Wr == INVALID_HANDLE_VALUE)
199  {
200  throw system_exceptiont("Output pipe creation failed for child_std_OUT_Wr");
201  }
202  if(!SetHandleInformation(child_std_OUT_Rd, HANDLE_FLAG_INHERIT, 0))
203  {
204  throw system_exceptiont(
205  "Output pipe creation failed on SetHandleInformation");
206  }
207  // Create the child process
208  STARTUPINFOW start_info;
209  proc_info = util_make_unique<PROCESS_INFORMATION>();
210  ZeroMemory(proc_info.get(), sizeof(PROCESS_INFORMATION));
211  ZeroMemory(&start_info, sizeof(STARTUPINFOW));
212  start_info.cb = sizeof(STARTUPINFOW);
213  start_info.hStdError = child_std_OUT_Wr;
214  start_info.hStdOutput = child_std_OUT_Wr;
215  start_info.hStdInput = child_std_IN_Rd;
216  start_info.dwFlags |= STARTF_USESTDHANDLES;
217  const std::wstring cmdline = prepare_windows_command_line(commandvec);
218  // Note that we do NOT free this since it becomes part of the child
219  // and causes heap corruption in Windows if we free!
220  const BOOL success = CreateProcessW(
221  NULL, // application name, we only use the command below
222  _wcsdup(cmdline.c_str()), // command line
223  NULL, // process security attributes
224  NULL, // primary thread security attributes
225  TRUE, // handles are inherited
226  0, // creation flags
227  NULL, // use parent's environment
228  NULL, // use parent's current directory
229  &start_info, // STARTUPINFO pointer
230  proc_info.get()); // receives PROCESS_INFORMATION
231  // Close handles to the stdin and stdout pipes no longer needed by the
232  // child process. If they are not explicitly closed, there is no way to
233  // recognize that the child process has ended (but maybe we don't care).
234  CloseHandle(child_std_OUT_Wr);
235  CloseHandle(child_std_IN_Rd);
236 # else
237 
238  if(pipe(pipe_input) == -1)
239  {
240  throw system_exceptiont("Input pipe creation failed");
241  }
242 
243  if(pipe(pipe_output) == -1)
244  {
245  throw system_exceptiont("Output pipe creation failed");
246  }
247 
248 
249  if(fcntl(pipe_output[0], F_SETFL, O_NONBLOCK) < 0)
250  {
251  throw system_exceptiont("Setting pipe non-blocking failed");
252  }
253 
254  // Create a new process for the child that will execute the
255  // command and receive information via pipes.
256  child_process_id = fork();
257  if(child_process_id == 0)
258  {
259  // child process here
260 
261  // Close pipes that will be used by the parent so we do
262  // not have our own copies and conflicts.
263  close(pipe_input[1]);
264  close(pipe_output[0]);
265 
266  // Duplicate pipes so we have the ones we need.
267  dup2(pipe_input[0], STDIN_FILENO);
268  dup2(pipe_output[1], STDOUT_FILENO);
269  dup2(pipe_output[1], STDERR_FILENO);
270 
271  // Create a char** for the arguments (all the contents of commandvec
272  // except the first element, i.e. the command itself).
273  char **args =
274  reinterpret_cast<char **>(malloc((commandvec.size()) * sizeof(char *)));
275  // Add all the arguments to the args array of char *.
276  unsigned long i = 0;
277  while(i < commandvec.size())
278  {
279  args[i] = strdup(commandvec[i].c_str());
280  i++;
281  }
282  args[i] = NULL;
283  execvp(commandvec[0].c_str(), args);
284  // The args variable will be handled by the OS if execvp succeeds, but
285  // if execvp fails then we should free it here (just in case the runtime
286  // error below continues execution.)
287  while(i > 0)
288  {
289  i--;
290  free(args[i]);
291  }
292  free(args);
293  // Only reachable if execvp failed
294  // Note that here we send to std::cerr since we are in the child process
295  // here and this is received by the parent process.
296  std::cerr << "Launching " << commandvec[0]
297  << " failed with error: " << std::strerror(errno) << std::endl;
298  abort();
299  }
300  else
301  {
302  // parent process here
303  // Close pipes to be used by the child process
304  close(pipe_input[0]);
305  close(pipe_output[1]);
306 
307  // Get stream for sending to the child process
308  command_stream = fdopen(pipe_input[1], "w");
309  }
310 # endif
312 }
313 
315 {
316 # ifdef _WIN32
317  TerminateProcess(proc_info->hProcess, 0);
318  // Disconnecting the pipes also kicks the client off, it should be killed
319  // by now, but this will also force the client off.
320  // Note that pipes are cleaned up by Windows when all handles to the pipe
321  // are closed. Disconnect may be superfluous here.
322  DisconnectNamedPipe(child_std_OUT_Rd);
323  DisconnectNamedPipe(child_std_IN_Wr);
324  CloseHandle(child_std_OUT_Rd);
325  CloseHandle(child_std_IN_Wr);
326  CloseHandle(proc_info->hProcess);
327  CloseHandle(proc_info->hThread);
328 # else
329  // Close the parent side of the remaining pipes
330  fclose(command_stream);
331  // Note that the above will call close(pipe_input[1]);
332  close(pipe_output[0]);
333  // Send signal to the child process to terminate
334  kill(child_process_id, SIGTERM);
335 # endif
336 }
337 
339 {
341  {
343  }
344 #ifdef _WIN32
345  if(!WriteFile(child_std_IN_Wr, message.c_str(), message.size(), NULL, NULL))
346  {
347  // Error handling with GetLastError ?
348  return send_responset::FAILED;
349  }
350 #else
351  // send message to solver process
352  int send_status = fputs(message.c_str(), command_stream);
353  fflush(command_stream);
354 
355  if(send_status == EOF)
356  {
357  return send_responset::FAILED;
358  }
359 # endif
361 }
362 
364 {
365  INVARIANT(
367  "Can only receive() from a fully initialised process");
368  std::string response = std::string("");
369  char buff[BUFSIZE];
370  bool success = true;
371 #ifdef _WIN32
372  DWORD nbytes;
373 #else
374  int nbytes;
375 #endif
376  while(success)
377  {
378 #ifdef _WIN32
379  success = ReadFile(child_std_OUT_Rd, buff, BUFSIZE, &nbytes, NULL);
380 #else
381  nbytes = read(pipe_output[0], buff, BUFSIZE);
382  // Added the status back in here to keep parity with old implementation
383  // TODO: check which statuses are really used/needed.
384  if(nbytes == 0) // Update if the pipe is stopped
386  success = nbytes > 0;
387 #endif
388  INVARIANT(
389  nbytes < BUFSIZE,
390  "More bytes cannot be read at a time, than the size of the buffer");
391  if(nbytes > 0)
392  {
393  response.append(buff, nbytes);
394  }
395  }
396  return response;
397 }
398 
400 {
401  // can_receive(PIPED_PROCESS_INFINITE_TIMEOUT) waits an ubounded time until
402  // there is some data
404  return receive();
405 }
406 
408 {
409  return process_state;
410 }
411 
413 {
414  // unwrap the optional argument here
415  const int timeout = wait_time ? narrow<int>(*wait_time) : -1;
416 #ifdef _WIN32
417  int waited_time = 0;
418  // The next four need to be initialised for compiler warnings
419  DWORD buffer = 0;
420  LPDWORD nbytes = 0;
421  LPDWORD rbytes = 0;
422  LPDWORD rmbytes = 0;
423  while(timeout < 0 || waited_time >= timeout)
424  {
425  PeekNamedPipe(child_std_OUT_Rd, &buffer, 1, nbytes, rbytes, rmbytes);
426  if(buffer != 0)
427  {
428  return true;
429  }
430 // TODO make this define and choice better
431 # define WIN_POLL_WAIT 10
432  Sleep(WIN_POLL_WAIT);
433  waited_time += WIN_POLL_WAIT;
434  }
435 #else
436  struct pollfd fds // NOLINT
437  {
438  pipe_output[0], POLLIN, 0
439  };
440  nfds_t nfds = POLLIN;
441  const int ready = poll(&fds, nfds, timeout);
442 
443  switch(ready)
444  {
445  case -1:
446  // Error case
447  // Further error handling could go here
449  // fallthrough intended
450  case 0:
451  // Timeout case
452  // Do nothing for timeout and error fallthrough, default function behaviour
453  // is to return false.
454  break;
455  default:
456  // Found some events, check for POLLIN
457  if(fds.revents & POLLIN)
458  {
459  // we can read from the pipe here
460  return true;
461  }
462  // Some revent we did not ask for or check for, can't read though.
463  }
464 # endif
465  return false;
466 }
467 
469 {
470  return can_receive(0);
471 }
472 
474 {
475  while(process_state == statet::RUNNING && !can_receive(0))
476  {
477 #ifdef _WIN32
478  Sleep(wait_time);
479 #else
480  usleep(wait_time);
481 #endif
482  }
483 }
pid_t child_process_id
statet process_state
bool can_receive()
See if this process can receive data from the other process.
piped_processt(const std::vector< std::string > &commandvec)
Initiate a new subprocess with pipes supporting communication between the parent (this process) and t...
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.
FILE * command_stream
statet
Enumeration to keep track of child process state.
Definition: piped_process.h:29
statet get_status()
Get child process status.
send_responset
Enumeration for send response.
Definition: piped_process.h:36
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.
nonstd::optional< T > optionalt
Definition: optional.h:35
#define BUFSIZE
Subprocess communication with pipes.
#define PIPED_PROCESS_INFINITE_TIMEOUT
Definition: piped_process.h:19
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::wstring widen(const char *s)
Definition: unicode.cpp:48