Skip to content

Commit 48e3a22

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 fd515f1 commit 48e3a22

File tree

3 files changed

+303
-0
lines changed

3 files changed

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

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)