Skip to content

Commit 29d265c

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 f81c761 commit 29d265c

File tree

3 files changed

+304
-0
lines changed

3 files changed

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

src/util/piped_process.h

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
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+
class piped_processt
9+
{
10+
public:
11+
/// Enumeration to keep track of child process state.
12+
enum class process_statet
13+
{
14+
NOT_CREATED,
15+
CREATED,
16+
STOPPED,
17+
ERROR
18+
};
19+
20+
enum class process_send_responset
21+
{
22+
SUCCEEDED,
23+
FAILED,
24+
ERROR
25+
};
26+
27+
/// Send a string message (command) to the child process.
28+
/// \param message The string message to be sent.
29+
process_send_responset send(const std::string &message);
30+
/// Read a string from the child process' output.
31+
std::string receive();
32+
/// Wait until a string is available and read a string from the child
33+
/// process' output.
34+
std::string wait_receive();
35+
36+
/// Get child process status.
37+
process_statet get_status();
38+
39+
/// See if this process can receive data from the other process.
40+
/// \param timeout Amount of time to wait before timing out and
41+
/// returning: -1 is infiniute, 0 is non-blocking immediate.
42+
bool can_receive(int timeout);
43+
44+
/// See if this process can receive data from the other process.
45+
/// Note this calls can_receive(0);
46+
bool can_receive();
47+
48+
/// Wait for the pipe to be ready, waiting specified time between
49+
/// checks. Will return when the pipe is ready or the other process
50+
/// is not in a process_statet::CREATED state (i.e. error has occured).
51+
/// \param wait_time Time spent in usleep() between checks of can_receive(0)
52+
void wait_receivable(int wait_time);
53+
54+
/// Initiate a new subprocess with pipes supporting communication
55+
/// between the parent (this process) and the child.
56+
/// \param command The command we want to run (binary + options)
57+
piped_processt(const std::string &command);
58+
59+
~piped_processt();
60+
61+
protected:
62+
// Child process ID.
63+
pid_t pid;
64+
FILE *command_stream;
65+
int pipe_input[2];
66+
int pipe_output[2];
67+
process_statet process_state;
68+
};
69+
70+
#endif

0 commit comments

Comments
 (0)