Skip to content

Commit 93c3e14

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 c9ac965 commit 93c3e14

File tree

2 files changed

+273
-0
lines changed

2 files changed

+273
-0
lines changed

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.cpp \
124124
util/optional_utils.cpp \
125125
util/parse_options.cpp \
126+
util/piped_process.cpp \
126127
util/pointer_offset_size.cpp \
127128
util/prefix_filter.cpp \
128129
util/range.cpp \

unit/util/piped_process.cpp

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

0 commit comments

Comments
 (0)