Skip to content

Commit 27b9337

Browse files
committed
Bugfix communication by keeping original input pipe in parent process
Prior to this commit, communication sent to the solver was not being received. Sending the data was reported as successful, but the subprocess could not read it from the standard input. The inherit flag is now set rather than cleared, so that the sub process is able to use the handle. This commit enables all piped_process unit tests on Windows, as these now work/pass.
1 parent 84396be commit 27b9337

File tree

2 files changed

+6
-8
lines changed

2 files changed

+6
-8
lines changed

src/util/piped_process.cpp

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -138,9 +138,9 @@ piped_processt::piped_processt(const std::vector<std::string> &commandvec)
138138
// Use process ID as a unique ID for this process at this time.
139139
base_name.append(std::to_string(GetCurrentProcessId()));
140140
const std::string in_name = base_name + "\\IN";
141-
child_std_IN_Rd = CreateNamedPipe(
141+
child_std_IN_Wr = CreateNamedPipe(
142142
in_name.c_str(),
143-
PIPE_ACCESS_INBOUND, // Reading for us
143+
PIPE_ACCESS_OUTBOUND, // Writing for us
144144
PIPE_TYPE_BYTE | PIPE_NOWAIT, // Bytes and non-blocking
145145
PIPE_UNLIMITED_INSTANCES, // Probably doesn't matter
146146
BUFSIZE,
@@ -156,9 +156,9 @@ piped_processt::piped_processt(const std::vector<std::string> &commandvec)
156156
throw system_exceptiont("Input pipe creation failed for child_std_IN_Rd");
157157
}
158158
// Connect to the other side of the pipe
159-
child_std_IN_Wr = CreateFile(
159+
child_std_IN_Rd = CreateFile(
160160
in_name.c_str(),
161-
GENERIC_WRITE, // Write side
161+
GENERIC_READ, // Read side
162162
FILE_SHARE_READ | FILE_SHARE_WRITE, // Shared read/write
163163
&sec_attr, // Need this for inherit
164164
OPEN_EXISTING, // Opening other end
@@ -168,7 +168,8 @@ piped_processt::piped_processt(const std::vector<std::string> &commandvec)
168168
{
169169
throw system_exceptiont("Input pipe creation failed for child_std_IN_Wr");
170170
}
171-
if(!SetHandleInformation(child_std_IN_Rd, HANDLE_FLAG_INHERIT, 0))
171+
if(!SetHandleInformation(
172+
child_std_IN_Rd, HANDLE_FLAG_INHERIT, HANDLE_FLAG_INHERIT))
172173
{
173174
throw system_exceptiont(
174175
"Input pipe creation failed on SetHandleInformation");

unit/util/piped_process.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -107,8 +107,6 @@ TEST_CASE(
107107
REQUIRE(calc < 2);
108108
}
109109

110-
#ifndef _WIN32
111-
// No Windows tests for z3 due to path and dependency issues.
112110
TEST_CASE(
113111
"Creating a sub process of z3 and read a response from an echo command.",
114112
"[core][util][piped_process][.z3]")
@@ -314,4 +312,3 @@ TEST_CASE(
314312
REQUIRE(
315313
process.send("(exit)\n") == piped_processt::send_responset::SUCCEEDED);
316314
}
317-
#endif

0 commit comments

Comments
 (0)