100 # define BUFSIZE (1024 * 64)
102 # define BUFSIZE 2048
112 prepare_windows_command_line(
const std::vector<std::string> &commandvec)
114 std::wstring result =
widen(commandvec[0]);
115 for(
int i = 1; i < commandvec.size(); i++)
118 result.append(quote_windows_arg(
widen(commandvec[i])));
125 const std::vector<std::string> &commandvec,
127 :
log{message_handler}
131 SECURITY_ATTRIBUTES sec_attr;
132 sec_attr.nLength =
sizeof(SECURITY_ATTRIBUTES);
134 sec_attr.bInheritHandle =
TRUE;
138 sec_attr.lpSecurityDescriptor = NULL;
141 std::string base_name =
"\\\\.\\pipe\\cbmc\\child\\";
144 const std::string in_name = base_name +
"\\IN";
145 child_std_IN_Wr = CreateNamedPipe(
147 PIPE_ACCESS_OUTBOUND,
148 PIPE_TYPE_BYTE | PIPE_NOWAIT,
149 PIPE_UNLIMITED_INSTANCES,
158 if(child_std_IN_Rd == INVALID_HANDLE_VALUE)
163 child_std_IN_Rd = CreateFile(
166 FILE_SHARE_READ | FILE_SHARE_WRITE,
169 FILE_ATTRIBUTE_NORMAL | FILE_FLAG_NO_BUFFERING,
171 if(child_std_IN_Wr == INVALID_HANDLE_VALUE)
175 if(!SetHandleInformation(
176 child_std_IN_Rd, HANDLE_FLAG_INHERIT, HANDLE_FLAG_INHERIT))
179 "Input pipe creation failed on SetHandleInformation");
181 const std::string out_name = base_name +
"\\OUT";
182 child_std_OUT_Rd = CreateNamedPipe(
185 PIPE_TYPE_BYTE | PIPE_NOWAIT,
186 PIPE_UNLIMITED_INSTANCES,
191 if(child_std_OUT_Rd == INVALID_HANDLE_VALUE)
195 child_std_OUT_Wr = CreateFile(
198 FILE_SHARE_READ | FILE_SHARE_WRITE,
201 FILE_ATTRIBUTE_NORMAL | FILE_FLAG_NO_BUFFERING,
203 if(child_std_OUT_Wr == INVALID_HANDLE_VALUE)
207 if(!SetHandleInformation(child_std_OUT_Rd, HANDLE_FLAG_INHERIT, 0))
210 "Output pipe creation failed on SetHandleInformation");
213 STARTUPINFOW start_info;
214 proc_info = std::make_unique<PROCESS_INFORMATION>();
215 ZeroMemory(proc_info.get(),
sizeof(PROCESS_INFORMATION));
216 ZeroMemory(&start_info,
sizeof(STARTUPINFOW));
217 start_info.cb =
sizeof(STARTUPINFOW);
218 start_info.hStdError = child_std_OUT_Wr;
219 start_info.hStdOutput = child_std_OUT_Wr;
220 start_info.hStdInput = child_std_IN_Rd;
221 start_info.dwFlags |= STARTF_USESTDHANDLES;
222 const std::wstring cmdline = prepare_windows_command_line(commandvec);
225 const BOOL success = CreateProcessW(
227 _wcsdup(cmdline.c_str()),
239 CloseHandle(child_std_OUT_Wr);
240 CloseHandle(child_std_IN_Rd);
280 char **args =
reinterpret_cast<char **
>(
281 malloc((commandvec.size() + 1) *
sizeof(
char *)));
284 while(i < commandvec.size())
286 args[i] =
strdup(commandvec[i].c_str());
290 execvp(commandvec[0].c_str(), args);
303 std::cerr <<
"Launching " << commandvec[0]
304 <<
" failed with error: " <<
std::strerror(errno) << std::endl;
324 TerminateProcess(proc_info->hProcess, 0);
329 DisconnectNamedPipe(child_std_OUT_Rd);
330 DisconnectNamedPipe(child_std_IN_Wr);
331 CloseHandle(child_std_OUT_Rd);
332 CloseHandle(child_std_IN_Wr);
333 CloseHandle(proc_info->hProcess);
334 CloseHandle(proc_info->hThread);
353 const auto message_size = narrow<DWORD>(message.size());
355 DWORD bytes_written = 0;
356 const int retry_limit = 10;
357 for(
int send_attempts = 0; send_attempts < retry_limit; ++send_attempts)
366 child_std_IN_Wr, message.c_str(), message_size, &bytes_written, NULL))
368 const DWORD error_code = GetLastError();
373 if(bytes_written != 0)
376 const auto wait_milliseconds = narrow<DWORD>(1 << send_attempts);
377 log.
debug() <<
"Zero bytes send to sub process. Retrying in "
379 FlushFileBuffers(child_std_IN_Wr);
380 Sleep(wait_milliseconds);
383 message_size == bytes_written,
384 "Number of bytes written to sub process must match message size."
387 " bytes were written.");
393 if(send_status == EOF)
405 "Can only receive() from a fully initialised process");
406 std::string response = std::string(
"");
417 success = ReadFile(child_std_OUT_Rd, buff,
BUFSIZE, &nbytes, NULL);
424 success = nbytes > 0;
428 "More bytes cannot be read at a time, than the size of the buffer");
431 response.append(buff, nbytes);
453 const int timeout = wait_time ? narrow<int>(*wait_time) : -1;
456 DWORD total_bytes_available = 0;
457 while(timeout < 0 || waited_time >= timeout)
459 const LPVOID lpBuffer =
nullptr;
460 const DWORD nBufferSize = 0;
461 const LPDWORD lpBytesRead =
nullptr;
462 const LPDWORD lpTotalBytesAvail = &total_bytes_available;
463 const LPDWORD lpBytesLeftThisMessage =
nullptr;
470 lpBytesLeftThisMessage);
471 if(total_bytes_available > 0)
476 # define WIN_POLL_WAIT 10
477 Sleep(WIN_POLL_WAIT);
478 waited_time += WIN_POLL_WAIT;
485 nfds_t nfds = POLLIN;
486 const int ready = poll(&fds, nfds, timeout);
502 if(fds.revents & POLLIN)
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.
int fcntl(int fd, int cmd,...)
int __CPROVER_ID java::java io InputStream read
Subprocess communication with pipes.
#define PIPED_PROCESS_INFINITE_TIMEOUT
int kill(pid_t pid, int sig)
#define PRECONDITION(CONDITION)
FILE * fdopen(int handle, const char *mode)
int fputs(const char *s, FILE *stream)
void * malloc(__CPROVER_size_t malloc_size)
char * strdup(const char *str)
char * strerror(int errnum)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::wstring widen(const char *s)
int usleep(unsigned int usec)