Skip to content

Commit 8b4b3bb

Browse files
NlightNFotisTGWDB
andcommitted
Add unit tests for the piped_processt class.
Add validation code for the `piped_processt` class, in the form of Catch unit tests, under `unit/util/`. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Thomas Given-Wilson <[email protected]>
1 parent 22e3d10 commit 8b4b3bb

File tree

4 files changed

+143
-11
lines changed

4 files changed

+143
-11
lines changed

src/util/piped_process.cpp

Lines changed: 43 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,23 @@
1+
#ifdef _WIN32
2+
// Windows includes go here
3+
#else
14
#include <cstring>
25
#include <iostream>
36
#include <unistd.h>
47
#include <errno.h>
8+
#include <fcntl.h> // library for fcntl function
9+
#endif
510

11+
#include "invariant.h"
612
#include "piped_process.h"
713

814

915
piped_processt::piped_processt(const std::string &command)
1016
{
11-
// piped_processt subp = piped_processt();
17+
#ifdef _WIN32
18+
// This should use the new error state from PR #6131 once that is done
19+
INVARIANT(false, "New SMT2 backend WIP: Windows piped_process constructor.");
20+
#else
1221
if (pipe(pipe_input) == -1) {
1322
throw std::runtime_error("Input pipe creation failed");
1423
}
@@ -19,6 +28,10 @@ piped_processt::piped_processt(const std::string &command)
1928
// Default state
2029
process_state = process_statet::NOT_CREATED;
2130

31+
if (fcntl(pipe_output[0], F_SETFL, O_NONBLOCK) < 0) {
32+
throw std::runtime_error("Setting pipe non-blocking failed");
33+
}
34+
2235
// Create a new process for the child that will execute the
2336
// command and receive information via pipes.
2437
pid_t pid = fork();
@@ -39,7 +52,7 @@ piped_processt::piped_processt(const std::string &command)
3952
char **args = split_command_args(command);
4053
// Execute the command
4154
execvp(args[0], args);
42-
// Only reachable if execpv failed
55+
// Only reachable if execvp failed
4356
throw std::runtime_error("Launching \"" + command +
4457
"\" failed with error: " + strerror(errno));
4558
} else {
@@ -48,14 +61,19 @@ piped_processt::piped_processt(const std::string &command)
4861
close(pipe_input[0]);
4962
close(pipe_output[1]);
5063

51-
// get stream for sending to the child process
64+
// Get stream for sending to the child process
5265
command_stream = fdopen(pipe_input[1], "w");
5366
process_state = process_statet::CREATED;
5467
}
68+
#endif
5569
}
5670

5771
bool piped_processt::send(const std::string &message)
5872
{
73+
#ifdef _WIN32
74+
// This should use the new error state from PR #6131 once that is done
75+
INVARIANT(false, "New SMT2 backend WIP: Windows piped_processt::send.");
76+
#else
5977
if(process_state != process_statet::CREATED)
6078
{
6179
return false;
@@ -70,10 +88,15 @@ bool piped_processt::send(const std::string &message)
7088
return false;
7189
}
7290
return true;
91+
#endif
7392
}
7493

7594
std::string piped_processt::receive()
7695
{
96+
#ifdef _WIN32
97+
// This should use the new error state from PR #6131 once that is done
98+
INVARIANT(false, "New SMT2 backend WIP: Windows piped_processt::receive.");
99+
#else
77100
if(process_state != process_statet::CREATED)
78101
return NULL;
79102
std::string response = std::string("");
@@ -82,12 +105,24 @@ std::string piped_processt::receive()
82105
while (true)
83106
{
84107
nbytes = read(pipe_output[0], buff, BUFSIZE);
85-
if (nbytes == 0)
86-
break;
87-
response.append(buff);
108+
switch (nbytes) {
109+
case -1:
110+
// Nothing more to read in the pipe
111+
return response;
112+
case 0:
113+
// Pipe is closed.
114+
process_state = process_statet::STOPPED;
115+
if (response == std::string("")) {
116+
return NULL;
117+
}
118+
return response;
119+
default:
120+
// Read some bytes, append them to the response and continue
121+
response.append(buff, nbytes);
122+
}
88123
}
89-
// assume nothing can go wrong for now! :D
90-
return response;
124+
UNREACHABLE;
125+
#endif
91126
}
92127

93128

src/util/piped_process.h

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
1-
#pragma once
1+
#ifndef CPROVER_UTIL_PIPED_PROCESS_H
2+
#define CPROVER_UTIL_PIPED_PROCESS_H
23

4+
// TODO: Revisit buffer size and storage location.
5+
// Note that this may impact number of characters correctly communicated
6+
// by the pipe, to check/fix.
37
#define BUFSIZE 2048
48

59
class piped_processt {
@@ -14,8 +18,6 @@ class piped_processt {
1418
protected:
1519
FILE *response_stream;
1620
FILE *command_stream;
17-
// TODO: Revisit buffer size and storage location
18-
// const int BUFSIZE = 2048;
1921
int pipe_input[2];
2022
int pipe_output[2];
2123
process_statet process_state;
@@ -31,3 +33,5 @@ class piped_processt {
3133
piped_processt(const std::string &command);
3234
// ~piped_processt();
3335
};
36+
37+
#endif

unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -123,6 +123,7 @@ SRC += analyses/ai/ai.cpp \
123123
util/optional_utils.cpp \
124124
util/parse_options.cpp \
125125
util/pointer_offset_size.cpp \
126+
util/piped_process.cpp \
126127
util/prefix_filter.cpp \
127128
util/range.cpp \
128129
util/replace_symbol.cpp \

unit/util/piped_process.cpp

Lines changed: 92 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,92 @@
1+
/// \file
2+
/// \author Diffblue Ltd.
3+
/// Unit tests for checking the piped process communication mechanism.
4+
5+
#ifdef _WIN32
6+
// No unit tests yet!
7+
#else
8+
#include <testing-utils/use_catch.h>
9+
#include <util/piped_process.h>
10+
#include <unistd.h>
11+
12+
TEST_CASE("We create a pipe and we can read from it", "[core][util][piped_process]")
13+
{
14+
std::string to_be_echoed = "The Jaberwocky";
15+
std::string binary = "/bin/echo";
16+
std::string command = binary + " " + to_be_echoed;
17+
piped_processt process = piped_processt(command);
18+
19+
sleep(1);
20+
21+
std::string response = process.receive();
22+
23+
// Trim newline from response string that causes match to fail.
24+
response.erase(
25+
std::remove(response.begin(), response.end(), '\n'), response.end());
26+
27+
REQUIRE(response == to_be_echoed);
28+
}
29+
30+
TEST_CASE("We create a pipe, send and receive from it", "[core][util][piped_process]")
31+
{
32+
std::string binary = "/usr/local/bin/z3 -in";
33+
std::string statement = "(echo \"hi\")";
34+
std::string termination_statement = "(exit)";
35+
piped_processt process = piped_processt(binary);
36+
// Wait a moment for z3 to start
37+
sleep(1);
38+
39+
bool res = process.send(statement);
40+
REQUIRE(res == true); // sending succeeded without problems
41+
42+
// Wait a moment for z3 to process the sent message
43+
sleep(1);
44+
std::string response = process.receive();
45+
// Trim newline from response string that causes match to fail.
46+
response.erase(
47+
std::remove(response.begin(), response.end(), '\n'), response.end());
48+
REQUIRE(response == std::string("hi"));
49+
REQUIRE(response.length() == 2);
50+
51+
// Tell z3 to terminate
52+
res = process.send(termination_statement);
53+
REQUIRE(res == true);
54+
}
55+
56+
TEST_CASE("We create a pipe, interact", "[core][util][piped_process]")
57+
{
58+
std::string binary = "/usr/local/bin/z3 -in";
59+
std::string statement = "(echo \"hi\")";
60+
std::string termination_statement = "(exit)";
61+
piped_processt process = piped_processt(binary);
62+
// Wait a moment for z3 to start
63+
sleep(1);
64+
65+
bool res = process.send(statement);
66+
REQUIRE(res == true); // sending succeeded without problems
67+
68+
// Wait a moment for z3 to process the sent message
69+
sleep(1);
70+
std::string response = process.receive();
71+
// Trim newline from response string that causes match to fail.
72+
response.erase(
73+
std::remove(response.begin(), response.end(), '\n'), response.end());
74+
REQUIRE(response == std::string("hi"));
75+
76+
statement = std::string("(echo \"Second string\")");
77+
res = process.send(statement);
78+
REQUIRE(res == true); // sending succeeded without problems
79+
80+
// Wait a moment for z3 to process the sent message
81+
sleep(1);
82+
response = process.receive();
83+
// Trim newline from response string that causes match to fail.
84+
response.erase(
85+
std::remove(response.begin(), response.end(), '\n'), response.end());
86+
REQUIRE(response == std::string("Second string"));
87+
88+
// Tell z3 to terminate
89+
res = process.send(termination_statement);
90+
REQUIRE(res == true);
91+
}
92+
#endif

0 commit comments

Comments
 (0)