Skip to content

Commit 80645ec

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 6397c1e commit 80645ec

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: 260 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,260 @@
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+
pid = fork();
58+
if(pid == 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+
std::cerr << "Launching " << commandvec[0]
96+
<< " failed with error: " << std::strerror(errno) << std::endl;
97+
abort();
98+
}
99+
else
100+
{
101+
// parent process here
102+
// Close pipes to be used by the child process
103+
close(pipe_input[0]);
104+
close(pipe_output[1]);
105+
106+
// Get stream for sending to the child process
107+
command_stream = fdopen(pipe_input[1], "w");
108+
process_state = statet::CREATED;
109+
}
110+
# endif
111+
}
112+
113+
piped_processt::~piped_processt()
114+
{
115+
# ifdef _WIN32
116+
UNIMPLEMENTED_FEATURE("Pipe IPC on windows: piped_processt constructor")
117+
# else
118+
// Close the parent side of the remaining pipes
119+
fclose(command_stream);
120+
// Note that the above will call close(pipe_input[1]);
121+
close(pipe_output[0]);
122+
// Send signal to the child process to terminate
123+
kill(pid, SIGTERM);
124+
# endif
125+
}
126+
127+
piped_processt::send_responset piped_processt::send(const std::string &message)
128+
{
129+
# ifdef _WIN32
130+
UNIMPLEMENTED_FEATURE("Pipe IPC on windows: send()")
131+
# else
132+
133+
if(process_state != statet::CREATED)
134+
{
135+
return send_responset::ERROR;
136+
}
137+
138+
// send message to solver process
139+
int send_status = fputs(message.c_str(), command_stream);
140+
fflush(command_stream);
141+
142+
if(send_status == EOF)
143+
{
144+
return send_responset::FAILED;
145+
}
146+
147+
return send_responset::SUCCEEDED;
148+
# endif
149+
}
150+
151+
std::string piped_processt::receive()
152+
{
153+
# ifdef _WIN32
154+
UNIMPLEMENTED_FEATURE("Pipe IPC on windows: receive()")
155+
# else
156+
157+
INVARIANT(
158+
process_state == statet::CREATED,
159+
"Can only receive() from a fully initialised process");
160+
161+
std::string response = std::string("");
162+
int nbytes;
163+
char buff[BUFSIZE];
164+
165+
while(true)
166+
{
167+
nbytes = read(pipe_output[0], buff, BUFSIZE);
168+
INVARIANT(
169+
nbytes < BUFSIZE,
170+
"More bytes cannot be read at a time, than the size of the buffer");
171+
switch(nbytes)
172+
{
173+
case -1:
174+
// Nothing more to read in the pipe
175+
return response;
176+
case 0:
177+
// Pipe is closed.
178+
process_state = statet::STOPPED;
179+
return response;
180+
default:
181+
// Read some bytes, append them to the response and continue
182+
response.append(buff, nbytes);
183+
}
184+
}
185+
186+
UNREACHABLE;
187+
# endif
188+
}
189+
190+
std::string piped_processt::wait_receive()
191+
{
192+
// can_receive(PIPED_PROCESS_INFINITE_TIMEOUT) waits an ubounded time until
193+
// there is some data
194+
can_receive(PIPED_PROCESS_INFINITE_TIMEOUT);
195+
return receive();
196+
}
197+
198+
piped_processt::statet piped_processt::get_status()
199+
{
200+
return process_state;
201+
}
202+
203+
bool piped_processt::can_receive(optionalt<std::size_t> wait_time)
204+
{
205+
# ifdef _WIN32
206+
UNIMPLEMENTED_FEATURE(
207+
"Pipe IPC on windows: can_receive(optionalt<std::size_t> wait_time)")
208+
# else
209+
// unwrap the optional argument here
210+
const int timeout = wait_time ? narrow<int>(*wait_time) : -1;
211+
struct pollfd fds // NOLINT
212+
{
213+
pipe_output[0], POLLIN, 0
214+
};
215+
nfds_t nfds = POLLIN;
216+
const int ready = poll(&fds, nfds, timeout);
217+
218+
switch(ready)
219+
{
220+
case -1:
221+
// Error case
222+
// Further error handling could go here
223+
process_state = statet::ERROR;
224+
// fallthrough intended
225+
case 0:
226+
// Timeout case
227+
// Do nothing for timeout and error fallthrough, default function behaviour
228+
// is to return false.
229+
break;
230+
default:
231+
// Found some events, check for POLLIN
232+
if(fds.revents & POLLIN)
233+
{
234+
// we can read from the pipe here
235+
return true;
236+
}
237+
// Some revent we did not ask for or check for, can't read though.
238+
}
239+
return false;
240+
# endif
241+
}
242+
243+
bool piped_processt::can_receive()
244+
{
245+
return can_receive(0);
246+
}
247+
248+
void piped_processt::wait_receivable(int wait_time)
249+
{
250+
# ifdef _WIN32
251+
UNIMPLEMENTED_FEATURE("Pipe IPC on windows: wait_stopped(int wait_time)")
252+
# else
253+
while(process_state == statet::CREATED && !can_receive(0))
254+
{
255+
usleep(wait_time);
256+
}
257+
# endif
258+
}
259+
260+
#endif

src/util/piped_process.h

Lines changed: 98 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,98 @@
1+
/// \file piped_process.h
2+
/// Subprocess communication with pipes
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+
// The member fields below are so named from the perspective of the
88+
// parent -> child process. So `pipe_input` is where we are feeding
89+
// commands to the child process, and `pipe_output` is where we read
90+
// the results of execution from.
91+
int pipe_input[2];
92+
int pipe_output[2];
93+
statet process_state;
94+
};
95+
96+
#endif // endif _WIN32
97+
98+
#endif // endifndef CPROVER_UTIL_PIPED_PROCESS_H

0 commit comments

Comments
 (0)