Skip to content

Commit 1523354

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 1523354

File tree

3 files changed

+352
-0
lines changed

3 files changed

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