Skip to content

Commit b44b0f6

Browse files
NlightNFotisTGWDB
andcommitted
Add piped_processt handler to CBMC.
Integration of our piped-process handling class into CBMC. A prototype of this was developed as a standalone executable, and after the proof of concept was validated, it was refactored and integrated into CBMC. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Thomas Given-Wilson <[email protected]>
1 parent 9539a51 commit b44b0f6

File tree

3 files changed

+359
-0
lines changed

3 files changed

+359
-0
lines changed

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

src/util/piped_process.h

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
/// \file Subprocess communication with pipes
2+
///
3+
/// \author Diffblue Ltd.
4+
5+
#ifndef CPROVER_UTIL_PIPED_PROCESS_H
6+
#define CPROVER_UTIL_PIPED_PROCESS_H
7+
8+
#ifdef _WIN32
9+
// TODO: Windows definitions go here
10+
#else
11+
12+
# include <vector>
13+
14+
# include "optional.h"
15+
16+
# define PIPED_PROCESS_INFINITE_TIMEOUT \
17+
optionalt<std::size_t> \
18+
{ \
19+
}
20+
21+
class piped_processt
22+
{
23+
public:
24+
/// Enumeration to keep track of child process state.
25+
enum class statet
26+
{
27+
NOT_CREATED,
28+
CREATED,
29+
STOPPED,
30+
ERROR
31+
};
32+
33+
/// Enumeration for send response.
34+
enum class send_responset
35+
{
36+
SUCCEEDED,
37+
FAILED,
38+
ERROR
39+
};
40+
41+
/// Send a string message (command) to the child process.
42+
/// \param message The string message to be sent.
43+
/// \return
44+
send_responset send(const std::string &message);
45+
/// Read a string from the child process' output.
46+
/// \return a string containing data from the process, empty string if no data
47+
std::string receive();
48+
/// Wait until a string is available and read a string from the child
49+
/// process' output.
50+
/// \return a string containing data from the process, empty string if no data
51+
std::string wait_receive();
52+
53+
/// Get child process status.
54+
/// \return a statet representing the status of the child process
55+
statet get_status();
56+
57+
/// See if this process can receive data from the other process.
58+
/// \param wait_time Amount of time to wait before timing out, with:
59+
/// * positive integer being wait time in milli-seconds,
60+
/// * 0 signifying non-blocking immediate return, and
61+
/// * an empty optional representing infinite wait time.
62+
/// \return true is there is data to read from process, false otherwise
63+
bool can_receive(optionalt<std::size_t> wait_time);
64+
65+
/// See if this process can receive data from the other process.
66+
/// Note this calls can_receive(0);
67+
/// \return true if there is data to read from process, false otherwise.
68+
bool can_receive();
69+
70+
/// Wait for the pipe to be ready, waiting specified time between
71+
/// checks. Will return when the pipe is ready or the other process
72+
/// is not in a process_statet::CREATED state (i.e. error has occured).
73+
/// \param wait_time Time spent in usleep() between checks of can_receive(0)
74+
void wait_receivable(int wait_time);
75+
76+
/// Initiate a new subprocess with pipes supporting communication
77+
/// between the parent (this process) and the child.
78+
/// \param commandvec The command and arguments to create the process
79+
explicit piped_processt(const std::vector<std::string> commandvec);
80+
81+
~piped_processt();
82+
83+
protected:
84+
// Child process ID.
85+
pid_t pid;
86+
FILE *command_stream;
87+
int pipe_input[2];
88+
int pipe_output[2];
89+
statet process_state;
90+
};
91+
92+
#endif // endif _WIN32
93+
94+
#endif // endifndef CPROVER_UTIL_PIPED_PROCESS_H

0 commit comments

Comments
 (0)