102 # define BUFSIZE 2048
111 prepare_windows_command_line(
const std::vector<std::string> &commandvec)
113 std::wstring result =
widen(commandvec[0]);
114 for(
int i = 1; i < commandvec.size(); i++)
117 result.append(quote_windows_arg(
widen(commandvec[i])));
127 SECURITY_ATTRIBUTES sec_attr;
128 sec_attr.nLength =
sizeof(SECURITY_ATTRIBUTES);
130 sec_attr.bInheritHandle =
TRUE;
134 sec_attr.lpSecurityDescriptor = NULL;
137 std::string base_name =
"\\\\.\\pipe\\cbmc\\child\\";
140 const std::string in_name = base_name +
"\\IN";
141 child_std_IN_Rd = CreateNamedPipe(
144 PIPE_TYPE_BYTE | PIPE_NOWAIT,
145 PIPE_UNLIMITED_INSTANCES,
154 if(child_std_IN_Rd == INVALID_HANDLE_VALUE)
159 child_std_IN_Wr = CreateFileA(
162 FILE_SHARE_READ | FILE_SHARE_WRITE,
165 FILE_ATTRIBUTE_NORMAL | FILE_FLAG_NO_BUFFERING,
167 if(child_std_IN_Wr == INVALID_HANDLE_VALUE)
171 if(!SetHandleInformation(child_std_IN_Rd, HANDLE_FLAG_INHERIT, 0))
174 "Input pipe creation failed on SetHandleInformation");
176 const std::string out_name = base_name +
"\\OUT";
177 child_std_OUT_Rd = CreateNamedPipe(
180 PIPE_TYPE_BYTE | PIPE_NOWAIT,
181 PIPE_UNLIMITED_INSTANCES,
186 if(child_std_OUT_Rd == INVALID_HANDLE_VALUE)
190 child_std_OUT_Wr = CreateFileA(
193 FILE_SHARE_READ | FILE_SHARE_WRITE,
196 FILE_ATTRIBUTE_NORMAL | FILE_FLAG_NO_BUFFERING,
198 if(child_std_OUT_Wr == INVALID_HANDLE_VALUE)
202 if(!SetHandleInformation(child_std_OUT_Rd, HANDLE_FLAG_INHERIT, 0))
205 "Output pipe creation failed on SetHandleInformation");
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);
220 const BOOL success = CreateProcessW(
222 _wcsdup(cmdline.c_str()),
234 CloseHandle(child_std_OUT_Wr);
235 CloseHandle(child_std_IN_Rd);
274 reinterpret_cast<char **
>(malloc((commandvec.size()) *
sizeof(
char *)));
277 while(i < commandvec.size())
279 args[i] = strdup(commandvec[i].c_str());
283 execvp(commandvec[0].c_str(), args);
296 std::cerr <<
"Launching " << commandvec[0]
297 <<
" failed with error: " << std::strerror(errno) << std::endl;
317 TerminateProcess(proc_info->hProcess, 0);
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);
345 if(!WriteFile(child_std_IN_Wr, message.c_str(), message.size(), NULL, NULL))
355 if(send_status == EOF)
367 "Can only receive() from a fully initialised process");
368 std::string response = std::string(
"");
379 success = ReadFile(child_std_OUT_Rd, buff,
BUFSIZE, &nbytes, NULL);
386 success = nbytes > 0;
390 "More bytes cannot be read at a time, than the size of the buffer");
393 response.append(buff, nbytes);
415 const int timeout = wait_time ? narrow<int>(*wait_time) : -1;
423 while(timeout < 0 || waited_time >= timeout)
425 PeekNamedPipe(child_std_OUT_Rd, &buffer, 1, nbytes, rbytes, rmbytes);
431 # define WIN_POLL_WAIT 10
432 Sleep(WIN_POLL_WAIT);
433 waited_time += WIN_POLL_WAIT;
440 nfds_t nfds = POLLIN;
441 const int ready = poll(&fds, nfds, timeout);
457 if(fds.revents & POLLIN)