Skip to content

Commit 22e3d10

Browse files
NlightNFotisTGWDB
andcommitted
Add pipe_processt 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 shown to be working, it was refactored and integrated into CBMC. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Thomas Given-Wilson <[email protected]>
1 parent 66d9d17 commit 22e3d10

File tree

3 files changed

+153
-0
lines changed

3 files changed

+153
-0
lines changed

src/util/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,7 @@ SRC = allocate_objects.cpp \
6262
pointer_offset_size.cpp \
6363
pointer_offset_sum.cpp \
6464
pointer_predicates.cpp \
65+
piped_process.cpp \
6566
prefix_filter.cpp \
6667
rational.cpp \
6768
rational_tools.cpp \

src/util/piped_process.cpp

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
1+
#include <cstring>
2+
#include <iostream>
3+
#include <unistd.h>
4+
#include <errno.h>
5+
6+
#include "piped_process.h"
7+
8+
9+
piped_processt::piped_processt(const std::string &command)
10+
{
11+
// piped_processt subp = piped_processt();
12+
if (pipe(pipe_input) == -1) {
13+
throw std::runtime_error("Input pipe creation failed");
14+
}
15+
16+
if (pipe(pipe_output) == -1) {
17+
throw std::runtime_error("Output pipe creation failed");
18+
}
19+
// Default state
20+
process_state = process_statet::NOT_CREATED;
21+
22+
// Create a new process for the child that will execute the
23+
// command and receive information via pipes.
24+
pid_t pid = fork();
25+
if (pid == 0) {
26+
// child process here
27+
28+
// Close pipes that will be used by the parent so we do
29+
// not have our own copies and conflicts.
30+
close(pipe_input[1]);
31+
close(pipe_output[0]);
32+
33+
// Duplicate pipes so we have the ones we need.
34+
dup2(pipe_input[0], STDIN_FILENO);
35+
dup2(pipe_output[1], STDOUT_FILENO);
36+
dup2(pipe_output[1], STDERR_FILENO);
37+
38+
// Create the arguments to execvp from the construction string
39+
char **args = split_command_args(command);
40+
// Execute the command
41+
execvp(args[0], args);
42+
// Only reachable if execpv failed
43+
throw std::runtime_error("Launching \"" + command +
44+
"\" failed with error: " + strerror(errno));
45+
} else {
46+
// parent process here
47+
// Close pipes to be used by the child process
48+
close(pipe_input[0]);
49+
close(pipe_output[1]);
50+
51+
// get stream for sending to the child process
52+
command_stream = fdopen(pipe_input[1], "w");
53+
process_state = process_statet::CREATED;
54+
}
55+
}
56+
57+
bool piped_processt::send(const std::string &message)
58+
{
59+
if(process_state != process_statet::CREATED)
60+
{
61+
return false;
62+
}
63+
// send message to solver process
64+
int send_status = fputs(message.c_str(), command_stream);
65+
fflush(command_stream);
66+
if(send_status == EOF)
67+
{
68+
// Some kind of error occured, maybe we should update the
69+
// solver status here?
70+
return false;
71+
}
72+
return true;
73+
}
74+
75+
std::string piped_processt::receive()
76+
{
77+
if(process_state != process_statet::CREATED)
78+
return NULL;
79+
std::string response = std::string("");
80+
int nbytes;
81+
char buff[BUFSIZE];
82+
while (true)
83+
{
84+
nbytes = read(pipe_output[0], buff, BUFSIZE);
85+
if (nbytes == 0)
86+
break;
87+
response.append(buff);
88+
}
89+
// assume nothing can go wrong for now! :D
90+
return response;
91+
}
92+
93+
94+
char ** piped_processt::split_command_args(const std::string &command)
95+
{
96+
char ** res = NULL;
97+
int n_spaces = 0;
98+
char *p = strtok(strdup(command.c_str()), " ");
99+
while(p)
100+
{
101+
res = (char **)realloc(res, sizeof (char*) * ++n_spaces);
102+
if (res == NULL)
103+
exit (-1); /* memory allocation failed */
104+
res[n_spaces-1] = p;
105+
p = strtok (NULL, " ");
106+
}
107+
res = (char **)realloc (res, sizeof (char*) * (n_spaces+1));
108+
res[n_spaces] = 0;
109+
return res;
110+
}
111+
112+
// Below is simple testing code to see that things (mostly) work.
113+
// int main(int argc, char *argv[])
114+
// {
115+
// piped_processt subp = piped_processt("/usr/local/bin/z3 --help");
116+
// std::string data = subp.receive();
117+
// std::cout << data << std::endl;
118+
// return 0;
119+
// }

src/util/piped_process.h

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
#pragma once
2+
3+
#define BUFSIZE 2048
4+
5+
class piped_processt {
6+
enum class process_statet {
7+
NOT_CREATED,
8+
CREATED,
9+
STOPPED
10+
};
11+
12+
char **split_command_args(const std::string &command);
13+
14+
protected:
15+
FILE *response_stream;
16+
FILE *command_stream;
17+
// TODO: Revisit buffer size and storage location
18+
// const int BUFSIZE = 2048;
19+
int pipe_input[2];
20+
int pipe_output[2];
21+
process_statet process_state;
22+
public:
23+
bool send(const std::string &message);
24+
std::string receive();
25+
26+
process_statet get_status()
27+
{
28+
return process_state;
29+
}
30+
31+
piped_processt(const std::string &command);
32+
// ~piped_processt();
33+
};

0 commit comments

Comments
 (0)