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