103 # define BUFSIZE (1024 * 64)
105 # define BUFSIZE 2048
115 prepare_windows_command_line(
const std::vector<std::string> &commandvec)
117 std::wstring result =
widen(commandvec[0]);
118 for(
int i = 1; i < commandvec.size(); i++)
121 result.append(quote_windows_arg(
widen(commandvec[i])));
128 const std::vector<std::string> &commandvec,
130 : log{message_handler}
134 SECURITY_ATTRIBUTES sec_attr;
135 sec_attr.nLength =
sizeof(SECURITY_ATTRIBUTES);
137 sec_attr.bInheritHandle =
TRUE;
141 sec_attr.lpSecurityDescriptor = NULL;
144 std::string base_name =
"\\\\.\\pipe\\cbmc\\child\\";
147 const std::string in_name = base_name +
"\\IN";
148 child_std_IN_Wr = CreateNamedPipe(
150 PIPE_ACCESS_OUTBOUND,
151 PIPE_TYPE_BYTE | PIPE_NOWAIT,
152 PIPE_UNLIMITED_INSTANCES,
161 if(child_std_IN_Rd == INVALID_HANDLE_VALUE)
166 child_std_IN_Rd = CreateFile(
169 FILE_SHARE_READ | FILE_SHARE_WRITE,
172 FILE_ATTRIBUTE_NORMAL | FILE_FLAG_NO_BUFFERING,
174 if(child_std_IN_Wr == INVALID_HANDLE_VALUE)
178 if(!SetHandleInformation(
179 child_std_IN_Rd, HANDLE_FLAG_INHERIT, HANDLE_FLAG_INHERIT))
182 "Input pipe creation failed on SetHandleInformation");
184 const std::string out_name = base_name +
"\\OUT";
185 child_std_OUT_Rd = CreateNamedPipe(
188 PIPE_TYPE_BYTE | PIPE_NOWAIT,
189 PIPE_UNLIMITED_INSTANCES,
194 if(child_std_OUT_Rd == INVALID_HANDLE_VALUE)
198 child_std_OUT_Wr = CreateFile(
201 FILE_SHARE_READ | FILE_SHARE_WRITE,
204 FILE_ATTRIBUTE_NORMAL | FILE_FLAG_NO_BUFFERING,
206 if(child_std_OUT_Wr == INVALID_HANDLE_VALUE)
210 if(!SetHandleInformation(child_std_OUT_Rd, HANDLE_FLAG_INHERIT, 0))
213 "Output pipe creation failed on SetHandleInformation");
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);
228 const BOOL success = CreateProcessW(
230 _wcsdup(cmdline.c_str()),
242 CloseHandle(child_std_OUT_Wr);
243 CloseHandle(child_std_IN_Rd);
248 if(pipe(pipe_input) == -1)
253 if(pipe(pipe_output) == -1)
259 if(fcntl(pipe_output[0], F_SETFL, O_NONBLOCK) < 0)
266 child_process_id = fork();
267 if(child_process_id == 0)
273 close(pipe_input[1]);
274 close(pipe_output[0]);
277 dup2(pipe_input[0], STDIN_FILENO);
278 dup2(pipe_output[1], STDOUT_FILENO);
279 dup2(pipe_output[1], STDERR_FILENO);
284 reinterpret_cast<char **
>(malloc((commandvec.size()) *
sizeof(
char *)));
287 while(i < commandvec.size())
289 args[i] = strdup(commandvec[i].c_str());
293 execvp(commandvec[0].c_str(), args);
306 std::cerr <<
"Launching " << commandvec[0]
307 <<
" failed with error: " << std::strerror(errno) << std::endl;
314 close(pipe_input[0]);
315 close(pipe_output[1]);
318 command_stream = fdopen(pipe_input[1],
"w");
321 process_state = statet::RUNNING;
327 TerminateProcess(proc_info->hProcess, 0);
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);
356 const auto message_size = narrow<DWORD>(message.size());
358 DWORD bytes_written = 0;
359 const int retry_limit = 10;
360 for(
int send_attempts = 0; send_attempts < retry_limit; ++send_attempts)
369 child_std_IN_Wr, message.c_str(), message_size, &bytes_written, NULL))
371 const DWORD error_code = GetLastError();
376 if(bytes_written != 0)
379 const auto wait_milliseconds = narrow<DWORD>(1 << send_attempts);
380 log.
debug() <<
"Zero bytes send to sub process. Retrying in "
382 FlushFileBuffers(child_std_IN_Wr);
383 Sleep(wait_milliseconds);
386 message_size == bytes_written,
387 "Number of bytes written to sub process must match message size."
390 " bytes were written.");
396 if(send_status == EOF)
408 "Can only receive() from a fully initialised process");
409 std::string response = std::string(
"");
420 success = ReadFile(child_std_OUT_Rd, buff,
BUFSIZE, &nbytes, NULL);
427 success = nbytes > 0;
431 "More bytes cannot be read at a time, than the size of the buffer");
434 response.append(buff, nbytes);
456 const int timeout = wait_time ? narrow<int>(*wait_time) : -1;
459 DWORD total_bytes_available = 0;
460 while(timeout < 0 || waited_time >= timeout)
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;
473 lpBytesLeftThisMessage);
474 if(total_bytes_available > 0)
479 # define WIN_POLL_WAIT 10
480 Sleep(WIN_POLL_WAIT);
481 waited_time += WIN_POLL_WAIT;
488 nfds_t nfds = POLLIN;
489 const int ready = poll(&fds, nfds, timeout);
505 if(fds.revents & POLLIN)