Skip to content

Commit 7601ad5

Browse files
authored
Merge pull request #6151 from NlightNFotis/pipes_infr
Piped process handler for CBMC/SMT solver IPC
2 parents d5c9ef8 + 814d951 commit 7601ad5

File tree

7 files changed

+661
-1
lines changed

7 files changed

+661
-1
lines changed

.github/workflows/pull-request-checks.yaml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -108,6 +108,7 @@ jobs:
108108
run: |
109109
make -C unit test
110110
make -C jbmc/unit test
111+
make TAGS="[z3]" -C unit test
111112
- name: Run expected failure unit tests
112113
run: |
113114
make TAGS="[!shouldfail]" -C unit test
@@ -332,7 +333,9 @@ jobs:
332333
- name: Print ccache stats
333334
run: ccache -s
334335
- name: Run unit tests
335-
run: cd unit; ./unit_tests
336+
run: |
337+
cd unit; ./unit_tests
338+
./unit_tests "[z3]"
336339
- name: Run JBMC unit tests
337340
run: cd jbmc/unit; ./unit_tests
338341
- name: Run regression tests

doc/API/util/piped_process.md

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
# `src/util/piped_process.{cpp, h}`
2+
3+
To utilise the `piped_process` API for interprocess communication with any binary:
4+
5+
* You need to initialise it by calling the construct `piped_processt("binary with args")`.
6+
* If IPC fails before child process creation, you will get a `system_exceptiont`.
7+
* If the `binary command` does not correspond to a binary in the `$PATH` or is
8+
not a path to a binary itself, you'll read a string `Launching <xyz> failed with error: <error>`
9+
when you attempt to `receive()` output from the child process.
10+
* The child process is automatically killed with SIGTERM when the destructor for
11+
the `piped_processt` object is called.
12+
* This will occur automatically when the `piped_processt` goes out of scope if
13+
it's locally scoped.
14+
* Use `send()` to send a string message to the child process' input.
15+
* This returns a `send_responset`, an enum that shows whether the
16+
sending of the message through the pipe succeeded or failed.
17+
* Use `receive()` to read a string message from the child process' output.
18+
* It's always a good idea to guard a call to `receive` with `can_receive()`,
19+
so that receiving is blocked until there's something to receive.
20+
* `can_receive` with no arguments will default to infinite wait time for piped
21+
process readiness.
22+
* Alternatively, you can guard the call to `receive` with `wait_receivable`.
23+
`wait_receivable` takes an integer value representing `microseconds` of waiting
24+
time between checks for pipe readiness.

src/util/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,7 @@ SRC = allocate_objects.cpp \
5858
options.cpp \
5959
parse_options.cpp \
6060
parser.cpp \
61+
piped_process.cpp \
6162
pointer_expr.cpp \
6263
pointer_offset_size.cpp \
6364
pointer_offset_sum.cpp \

src/util/piped_process.cpp

Lines changed: 262 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,262 @@
1+
/// \file piped_process.cpp
2+
/// Subprocess communication with pipes.
3+
/// \author Diffblue Ltd.
4+
5+
#ifdef _WIN32
6+
// Windows includes go here
7+
#else
8+
# include <fcntl.h> // library for fcntl function
9+
# include <poll.h> // library for poll function
10+
# include <signal.h> // library for kill function
11+
# include <unistd.h> // library for read/write/sleep/etc. functions
12+
#endif
13+
14+
#ifdef _WIN32
15+
// Unimplemented on windows for now...
16+
#else
17+
18+
# include <cstring> // library for strerror function (on linux)
19+
# include <iostream>
20+
# include <vector>
21+
22+
# include "exception_utils.h"
23+
# include "invariant.h"
24+
# include "narrow.h"
25+
# include "optional.h"
26+
# include "piped_process.h"
27+
# include "string_utils.h"
28+
29+
# define BUFSIZE 2048
30+
31+
piped_processt::piped_processt(const std::vector<std::string> commandvec)
32+
{
33+
# ifdef _WIN32
34+
UNIMPLEMENTED_FEATURE("Pipe IPC on windows.")
35+
# else
36+
37+
if(pipe(pipe_input) == -1)
38+
{
39+
throw system_exceptiont("Input pipe creation failed");
40+
}
41+
42+
if(pipe(pipe_output) == -1)
43+
{
44+
throw system_exceptiont("Output pipe creation failed");
45+
}
46+
47+
// Default state
48+
process_state = statet::NOT_CREATED;
49+
50+
if(fcntl(pipe_output[0], F_SETFL, O_NONBLOCK) < 0)
51+
{
52+
throw system_exceptiont("Setting pipe non-blocking failed");
53+
}
54+
55+
// Create a new process for the child that will execute the
56+
// command and receive information via pipes.
57+
child_process_id = fork();
58+
if(child_process_id == 0)
59+
{
60+
// child process here
61+
62+
// Close pipes that will be used by the parent so we do
63+
// not have our own copies and conflicts.
64+
close(pipe_input[1]);
65+
close(pipe_output[0]);
66+
67+
// Duplicate pipes so we have the ones we need.
68+
dup2(pipe_input[0], STDIN_FILENO);
69+
dup2(pipe_output[1], STDOUT_FILENO);
70+
dup2(pipe_output[1], STDERR_FILENO);
71+
72+
// Create a char** for the arguments (all the contents of commandvec
73+
// except the first element, i.e. the command itself).
74+
char **args =
75+
reinterpret_cast<char **>(malloc((commandvec.size()) * sizeof(char *)));
76+
// Add all the arguments to the args array of char *.
77+
unsigned long i = 0;
78+
while(i < commandvec.size())
79+
{
80+
args[i] = strdup(commandvec[i].c_str());
81+
i++;
82+
}
83+
args[i] = NULL;
84+
execvp(commandvec[0].c_str(), args);
85+
// The args variable will be handled by the OS if execvp succeeds, but
86+
// if execvp fails then we should free it here (just in case the runtime
87+
// error below continues execution.)
88+
while(i > 0)
89+
{
90+
i--;
91+
free(args[i]);
92+
}
93+
free(args);
94+
// Only reachable if execvp failed
95+
// Note that here we send to std::cerr since we are in the child process
96+
// here and this is received by the parent process.
97+
std::cerr << "Launching " << commandvec[0]
98+
<< " failed with error: " << std::strerror(errno) << std::endl;
99+
abort();
100+
}
101+
else
102+
{
103+
// parent process here
104+
// Close pipes to be used by the child process
105+
close(pipe_input[0]);
106+
close(pipe_output[1]);
107+
108+
// Get stream for sending to the child process
109+
command_stream = fdopen(pipe_input[1], "w");
110+
process_state = statet::CREATED;
111+
}
112+
# endif
113+
}
114+
115+
piped_processt::~piped_processt()
116+
{
117+
# ifdef _WIN32
118+
UNIMPLEMENTED_FEATURE("Pipe IPC on windows: piped_processt constructor")
119+
# else
120+
// Close the parent side of the remaining pipes
121+
fclose(command_stream);
122+
// Note that the above will call close(pipe_input[1]);
123+
close(pipe_output[0]);
124+
// Send signal to the child process to terminate
125+
kill(child_process_id, SIGTERM);
126+
# endif
127+
}
128+
129+
piped_processt::send_responset piped_processt::send(const std::string &message)
130+
{
131+
# ifdef _WIN32
132+
UNIMPLEMENTED_FEATURE("Pipe IPC on windows: send()")
133+
# else
134+
135+
if(process_state != statet::CREATED)
136+
{
137+
return send_responset::ERROR;
138+
}
139+
140+
// send message to solver process
141+
int send_status = fputs(message.c_str(), command_stream);
142+
fflush(command_stream);
143+
144+
if(send_status == EOF)
145+
{
146+
return send_responset::FAILED;
147+
}
148+
149+
return send_responset::SUCCEEDED;
150+
# endif
151+
}
152+
153+
std::string piped_processt::receive()
154+
{
155+
# ifdef _WIN32
156+
UNIMPLEMENTED_FEATURE("Pipe IPC on windows: receive()")
157+
# else
158+
159+
INVARIANT(
160+
process_state == statet::CREATED,
161+
"Can only receive() from a fully initialised process");
162+
163+
std::string response = std::string("");
164+
int nbytes;
165+
char buff[BUFSIZE];
166+
167+
while(true)
168+
{
169+
nbytes = read(pipe_output[0], buff, BUFSIZE);
170+
INVARIANT(
171+
nbytes < BUFSIZE,
172+
"More bytes cannot be read at a time, than the size of the buffer");
173+
switch(nbytes)
174+
{
175+
case -1:
176+
// Nothing more to read in the pipe
177+
return response;
178+
case 0:
179+
// Pipe is closed.
180+
process_state = statet::STOPPED;
181+
return response;
182+
default:
183+
// Read some bytes, append them to the response and continue
184+
response.append(buff, nbytes);
185+
}
186+
}
187+
188+
UNREACHABLE;
189+
# endif
190+
}
191+
192+
std::string piped_processt::wait_receive()
193+
{
194+
// can_receive(PIPED_PROCESS_INFINITE_TIMEOUT) waits an ubounded time until
195+
// there is some data
196+
can_receive(PIPED_PROCESS_INFINITE_TIMEOUT);
197+
return receive();
198+
}
199+
200+
piped_processt::statet piped_processt::get_status()
201+
{
202+
return process_state;
203+
}
204+
205+
bool piped_processt::can_receive(optionalt<std::size_t> wait_time)
206+
{
207+
# ifdef _WIN32
208+
UNIMPLEMENTED_FEATURE(
209+
"Pipe IPC on windows: can_receive(optionalt<std::size_t> wait_time)")
210+
# else
211+
// unwrap the optional argument here
212+
const int timeout = wait_time ? narrow<int>(*wait_time) : -1;
213+
struct pollfd fds // NOLINT
214+
{
215+
pipe_output[0], POLLIN, 0
216+
};
217+
nfds_t nfds = POLLIN;
218+
const int ready = poll(&fds, nfds, timeout);
219+
220+
switch(ready)
221+
{
222+
case -1:
223+
// Error case
224+
// Further error handling could go here
225+
process_state = statet::ERROR;
226+
// fallthrough intended
227+
case 0:
228+
// Timeout case
229+
// Do nothing for timeout and error fallthrough, default function behaviour
230+
// is to return false.
231+
break;
232+
default:
233+
// Found some events, check for POLLIN
234+
if(fds.revents & POLLIN)
235+
{
236+
// we can read from the pipe here
237+
return true;
238+
}
239+
// Some revent we did not ask for or check for, can't read though.
240+
}
241+
return false;
242+
# endif
243+
}
244+
245+
bool piped_processt::can_receive()
246+
{
247+
return can_receive(0);
248+
}
249+
250+
void piped_processt::wait_receivable(int wait_time)
251+
{
252+
# ifdef _WIN32
253+
UNIMPLEMENTED_FEATURE("Pipe IPC on windows: wait_stopped(int wait_time)")
254+
# else
255+
while(process_state == statet::CREATED && !can_receive(0))
256+
{
257+
usleep(wait_time);
258+
}
259+
# endif
260+
}
261+
262+
#endif

0 commit comments

Comments
 (0)