Skip to content

Commit d96e719

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 80645ec commit d96e719

File tree

2 files changed

+271
-0
lines changed

2 files changed

+271
-0
lines changed

unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -127,6 +127,7 @@ SRC += analyses/ai/ai.cpp \
127127
util/optional.cpp \
128128
util/optional_utils.cpp \
129129
util/parse_options.cpp \
130+
util/piped_process.cpp \
130131
util/pointer_offset_size.cpp \
131132
util/prefix_filter.cpp \
132133
util/range.cpp \

unit/util/piped_process.cpp

Lines changed: 270 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,270 @@
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+
9+
# include <testing-utils/use_catch.h>
10+
# include <util/optional.h>
11+
# include <util/piped_process.h>
12+
# include <util/string_utils.h>
13+
14+
TEST_CASE(
15+
"Creating a sub process and reading its output.",
16+
"[core][util][piped_process]")
17+
{
18+
const std::string to_be_echoed = "The Jabberwocky";
19+
// Need to give path to avoid shell built-in invocation
20+
std::vector<std::string> commands;
21+
commands.push_back("/bin/echo");
22+
commands.push_back(to_be_echoed);
23+
piped_processt process = piped_processt(commands);
24+
25+
// This is an indirect way to detect when the pipe has something. This
26+
// could (in theory) also return when there is an error, but this unit
27+
// test is not doing error handling.
28+
process.can_receive(PIPED_PROCESS_INFINITE_TIMEOUT);
29+
std::string response = strip_string(process.receive());
30+
31+
REQUIRE(response == to_be_echoed);
32+
}
33+
34+
TEST_CASE(
35+
"Creating a sub process with a binary that doesn't exist.",
36+
"[core][util][piped_process]")
37+
{
38+
const std::string expected_error("Launching abcde failed");
39+
std::vector<std::string> commands;
40+
commands.push_back("abcde");
41+
piped_processt process = piped_processt(commands);
42+
43+
// This is an indirect way to detect when the pipe has something. This
44+
// could (in theory) also return when there is an error, but this unit
45+
// test is not doing error handling.
46+
process.can_receive(PIPED_PROCESS_INFINITE_TIMEOUT);
47+
std::string response = process.receive();
48+
// This tracks how many times we tried, if for some reason we are stuck
49+
// give up eventually for this test.
50+
int too_many_tries = 0;
51+
// The expected length of the output string is 6 characters, keep
52+
// trying up to the retry limit of 5 or the string is long enough
53+
while(too_many_tries < 5 && response.length() < 64)
54+
{
55+
// Wait a short amount of time to try and receive
56+
process.can_receive(10);
57+
response += process.receive();
58+
too_many_tries++;
59+
}
60+
61+
REQUIRE(response.find(expected_error) < response.length() - 5);
62+
}
63+
64+
TEST_CASE(
65+
"Creating a sub process of z3 and read a response from an echo command.",
66+
"[core][util][piped_process]")
67+
{
68+
std::vector<std::string> commands;
69+
commands.push_back("z3");
70+
commands.push_back("-in");
71+
piped_processt process = piped_processt(commands);
72+
73+
REQUIRE(
74+
process.send("(echo \"hi\")\n") ==
75+
piped_processt::send_responset::SUCCEEDED);
76+
77+
process.can_receive(PIPED_PROCESS_INFINITE_TIMEOUT);
78+
std::string response = strip_string(process.receive());
79+
REQUIRE(response == "hi");
80+
81+
REQUIRE(
82+
process.send("(exit)\n") == piped_processt::send_responset::SUCCEEDED);
83+
}
84+
85+
TEST_CASE(
86+
"Creating a sub process and interacting with it.",
87+
"[core][util][piped_process]")
88+
{
89+
std::vector<std::string> commands;
90+
commands.push_back("z3");
91+
commands.push_back("-in");
92+
const std::string termination_statement = "(exit)\n";
93+
piped_processt process = piped_processt(commands);
94+
95+
REQUIRE(
96+
process.send("(echo \"hi\")\n") ==
97+
piped_processt::send_responset::SUCCEEDED);
98+
99+
process.can_receive(PIPED_PROCESS_INFINITE_TIMEOUT);
100+
std::string response = strip_string(process.receive());
101+
REQUIRE(response == "hi");
102+
103+
std::string statement = std::string("(echo \"Second string\")\n");
104+
REQUIRE(process.send(statement) == piped_processt::send_responset::SUCCEEDED);
105+
106+
process.can_receive(PIPED_PROCESS_INFINITE_TIMEOUT);
107+
response = strip_string(process.receive());
108+
REQUIRE(response == "Second string");
109+
110+
REQUIRE(
111+
process.send(termination_statement) ==
112+
piped_processt::send_responset::SUCCEEDED);
113+
}
114+
115+
TEST_CASE(
116+
"Use a created piped process instance of z3 to solve a simple SMT problem",
117+
"[core][util][piped_process]")
118+
{
119+
std::vector<std::string> commands;
120+
commands.push_back("z3");
121+
commands.push_back("-in");
122+
commands.push_back("-smt2");
123+
piped_processt process = piped_processt(commands);
124+
125+
std::string message =
126+
"(set-logic QF_LIA) (declare-const x Int) (declare-const y Int) (assert (> "
127+
"(+ (mod x 4) (* 3 (div y 2))) (- x y))) (check-sat)\n";
128+
REQUIRE(process.send(message) == piped_processt::send_responset::SUCCEEDED);
129+
130+
process.can_receive(PIPED_PROCESS_INFINITE_TIMEOUT);
131+
std::string response = strip_string(process.receive());
132+
REQUIRE(response == "sat");
133+
134+
REQUIRE(
135+
process.send("(exit)\n") == piped_processt::send_responset::SUCCEEDED);
136+
}
137+
138+
TEST_CASE(
139+
"Use a created piped process instance of z3 to solve a simple SMT problem "
140+
"with wait_receive",
141+
"[core][util][piped_process]")
142+
{
143+
std::vector<std::string> commands;
144+
commands.push_back("z3");
145+
commands.push_back("-in");
146+
commands.push_back("-smt2");
147+
piped_processt process = piped_processt(commands);
148+
149+
std::string statement =
150+
"(set-logic QF_LIA) (declare-const x Int) (declare-const y Int) (assert (> "
151+
"(+ (mod x 4) (* 3 (div y 2))) (- x y))) (check-sat)\n";
152+
153+
REQUIRE(process.send(statement) == piped_processt::send_responset::SUCCEEDED);
154+
155+
std::string response = strip_string(process.wait_receive());
156+
REQUIRE(response == "sat");
157+
158+
REQUIRE(
159+
process.send("(exit)\n") == piped_processt::send_responset::SUCCEEDED);
160+
}
161+
162+
TEST_CASE(
163+
"Use a created piped process instance of z3 to test wait_receivable",
164+
"[core][util][piped_process]")
165+
{
166+
std::vector<std::string> commands;
167+
commands.push_back("z3");
168+
commands.push_back("-in");
169+
piped_processt process = piped_processt(commands);
170+
171+
REQUIRE(
172+
process.send("(echo \"hi\")\n") ==
173+
piped_processt::send_responset::SUCCEEDED);
174+
175+
process.wait_receivable(100);
176+
std::string response = strip_string(process.receive());
177+
REQUIRE(response == "hi");
178+
179+
std::string statement = std::string("(echo \"Second string\")\n");
180+
REQUIRE(process.send(statement) == piped_processt::send_responset::SUCCEEDED);
181+
182+
process.wait_receivable(100);
183+
response = strip_string(process.receive());
184+
REQUIRE(response == "Second string");
185+
186+
REQUIRE(
187+
process.send("(exit)\n") == piped_processt::send_responset::SUCCEEDED);
188+
}
189+
190+
TEST_CASE(
191+
"Use piped process instance of z3 to solve a simple SMT problem and get the "
192+
"model, with wait_receivable/can_receive",
193+
"[core][util][piped_process]")
194+
{
195+
std::vector<std::string> commands;
196+
commands.push_back("z3");
197+
commands.push_back("-in");
198+
commands.push_back("-smt2");
199+
piped_processt process = piped_processt(commands);
200+
201+
std::string statement =
202+
"(set-logic QF_LIA) (declare-const x Int) (declare-const y Int) (assert (> "
203+
"(+ (mod x 4) (* 3 (div y 2))) (- x y))) (check-sat)\n";
204+
REQUIRE(process.send(statement) == piped_processt::send_responset::SUCCEEDED);
205+
206+
process.can_receive(PIPED_PROCESS_INFINITE_TIMEOUT);
207+
std::string response = strip_string(process.receive());
208+
REQUIRE(response == "sat");
209+
210+
REQUIRE(
211+
process.send("(get-model)\n") == piped_processt::send_responset::SUCCEEDED);
212+
213+
process.can_receive(PIPED_PROCESS_INFINITE_TIMEOUT);
214+
// If we receive here we can get less than the full (expected) output.
215+
// The normal expectation is that the caller will handle parsing and
216+
// checking of the received data (i.e. it is not the responsibility
217+
// of the piped_process to know how big the response should be).
218+
// Therefore, we need to rebuild the string here.
219+
response = process.receive();
220+
// This tracks how many times we tried, if for some reason we are stuck
221+
// give up eventually for this test.
222+
int too_many_tries = 0;
223+
// The expected length of the output string is 74 characters, keep
224+
// trying up to the retry limit of 5 or the string is long enough
225+
while(too_many_tries < 5 && response.length() < 74)
226+
{
227+
// Wait a short amount of time to try and receive
228+
process.can_receive(10);
229+
response += process.receive();
230+
too_many_tries++;
231+
}
232+
// It would be nice to check then whole model, but this is non-deterministic
233+
// and so causes problems.
234+
// Note that the above loop would need to read 74 characters to safely check
235+
// the model commented out here.
236+
// const std::string expected_response = std::string(
237+
// "(model \n (define-fun y () Int\n 0)\n "
238+
// "(define-fun x () Int\n (- 4))\n)\n");
239+
// REQUIRE(response == expected_response);
240+
REQUIRE(response.find("(define-fun") != std::string::npos);
241+
242+
REQUIRE(
243+
process.send("(exit)\n") == piped_processt::send_responset::SUCCEEDED);
244+
}
245+
246+
TEST_CASE(
247+
"Use a created piped process instance of z3 to solve a simple SMT problem "
248+
"and get the model, using infinite wait can_receive(...)",
249+
"[core][util][piped_process]")
250+
{
251+
std::vector<std::string> commands;
252+
commands.push_back("z3");
253+
commands.push_back("-in");
254+
commands.push_back("-smt2");
255+
piped_processt process = piped_processt(commands);
256+
257+
std::string statement =
258+
"(set-logic QF_LIA) (declare-const x Int) (declare-const y Int) (assert (> "
259+
"(+ (mod x 4) (* 3 (div y 2))) (- x y))) (check-sat)\n";
260+
REQUIRE(process.send(statement) == piped_processt::send_responset::SUCCEEDED);
261+
262+
process.can_receive(PIPED_PROCESS_INFINITE_TIMEOUT);
263+
std::string response = strip_string(process.receive());
264+
REQUIRE(response == "sat");
265+
266+
REQUIRE(
267+
process.send("(exit)\n") == piped_processt::send_responset::SUCCEEDED);
268+
}
269+
270+
#endif

0 commit comments

Comments
 (0)