Merge pull request #6602 from thomasspriggs/tas/piped_process_windows_fix

Bug fix piped process on Windows

Author: thomasspriggs

.github/workflows/pull-request-checks.yaml

@@ -482,6 +482,7 @@ jobs:
       - name: Run CBMC and JBMC unit tests
         run: |
           make CXX=clcache BUILD_ENV=MSVC -C unit      test
+          make CXX=clcache BUILD_ENV=MSVC -C unit test TAGS="[z3]"
           make CXX=clcache BUILD_ENV=MSVC -C jbmc/unit test
       - name: Run CBMC regression tests
         run: make CXX=clcache BUILD_ENV=MSVC -C regression test

regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc

@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 control_flow.c
---incremental-smt2-solver "z3 --smt2 -in" --verbosity 10
+--incremental-smt2-solver 'z3 --smt2 -in' --verbosity 10
 Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
 Sending command to SMT2 solver - \(set-option :produce-models true\)
 Sending command to SMT2 solver - \(set-logic QF_UFBV\)

regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc

@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 test.c
---incremental-smt2-solver "z3 --smt2 -in" --verbosity 10
+--incremental-smt2-solver 'z3 --smt2 -in' --verbosity 10
 Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
 Sending command to SMT2 solver - \(set-option :produce-models true\)
 Sending command to SMT2 solver - \(set-logic QF_UFBV\)

regression/cbmc-incr-smt2/nondeterministic-int-assert/trace.desc

@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 trace.c
---incremental-smt2-solver "z3 --smt2 -in" --trace
+--incremental-smt2-solver 'z3 --smt2 -in' --trace
 Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
 Assert of inequality to 4\.: FAILURE
 Assert of inequality to 2\.: FAILURE

regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc

@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 valid_unsat.c
---incremental-smt2-solver "z3 --smt2 -in" --verbosity 10
+--incremental-smt2-solver 'z3 --smt2 -in' --verbosity 10
 Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
 Sending command to SMT2 solver - \(check-sat\)
 Solver response - unsat

src/solvers/smt2_incremental/smt_solver_process.cpp

@@ -28,7 +28,17 @@ void smt_piped_solver_processt::send(const smt_commandt &smt_command)
   const std::string command_string = smt_to_smt2_string(smt_command);
   log.debug() << "Sending command to SMT2 solver - " << command_string
               << messaget::eom;
-  process.send(command_string + "\n");
+  const auto response = process.send(command_string + "\n");
+  switch(response)
+  {
+  case piped_processt::send_responset::SUCCEEDED:
+    return;
+  case piped_processt::send_responset::FAILED:
+    throw analysis_exceptiont{"Sending to SMT solver sub process failed."};
+  case piped_processt::send_responset::ERRORED:
+    throw analysis_exceptiont{"SMT solver sub process is in error state."};
+  }
+  UNREACHABLE;
 }
 
 /// Log messages and throw exception.

src/util/piped_process.cpp

@@ -138,9 +138,9 @@ piped_processt::piped_processt(const std::vector<std::string> &commandvec)
   // Use process ID as a unique ID for this process at this time.
   base_name.append(std::to_string(GetCurrentProcessId()));
   const std::string in_name = base_name + "\\IN";
-  child_std_IN_Rd = CreateNamedPipe(
+  child_std_IN_Wr = CreateNamedPipe(
     in_name.c_str(),
-    PIPE_ACCESS_INBOUND,          // Reading for us
+    PIPE_ACCESS_OUTBOUND,         // Writing for us
     PIPE_TYPE_BYTE | PIPE_NOWAIT, // Bytes and non-blocking
     PIPE_UNLIMITED_INSTANCES,     // Probably doesn't matter
     BUFSIZE,
@@ -156,9 +156,9 @@ piped_processt::piped_processt(const std::vector<std::string> &commandvec)
     throw system_exceptiont("Input pipe creation failed for child_std_IN_Rd");
   }
   // Connect to the other side of the pipe
-  child_std_IN_Wr = CreateFileA(
+  child_std_IN_Rd = CreateFile(
     in_name.c_str(),
-    GENERIC_WRITE,                                  // Write side
+    GENERIC_READ,                                   // Read side
     FILE_SHARE_READ | FILE_SHARE_WRITE,             // Shared read/write
     &sec_attr,                                      // Need this for inherit
     OPEN_EXISTING,                                  // Opening other end
@@ -168,7 +168,8 @@ piped_processt::piped_processt(const std::vector<std::string> &commandvec)
   {
     throw system_exceptiont("Input pipe creation failed for child_std_IN_Wr");
   }
-  if(!SetHandleInformation(child_std_IN_Rd, HANDLE_FLAG_INHERIT, 0))
+  if(!SetHandleInformation(
+       child_std_IN_Rd, HANDLE_FLAG_INHERIT, HANDLE_FLAG_INHERIT))
   {
     throw system_exceptiont(
       "Input pipe creation failed on SetHandleInformation");
@@ -187,7 +188,7 @@ piped_processt::piped_processt(const std::vector<std::string> &commandvec)
   {
     throw system_exceptiont("Output pipe creation failed for child_std_OUT_Rd");
   }
-  child_std_OUT_Wr = CreateFileA(
+  child_std_OUT_Wr = CreateFile(
     out_name.c_str(),
     GENERIC_WRITE,                                  // Write side
     FILE_SHARE_READ | FILE_SHARE_WRITE,             // Shared read/write
@@ -233,6 +234,8 @@ piped_processt::piped_processt(const std::vector<std::string> &commandvec)
   // recognize that the child process has ended (but maybe we don't care).
   CloseHandle(child_std_OUT_Wr);
   CloseHandle(child_std_IN_Rd);
+  if(!success)
+    throw system_exceptiont("Process creation failed.");
 #  else
 
   if(pipe(pipe_input) == -1)
@@ -335,18 +338,25 @@ piped_processt::~piped_processt()
 #  endif
 }
 
+NODISCARD
 piped_processt::send_responset piped_processt::send(const std::string &message)
 {
   if(process_state != statet::RUNNING)
   {
     return send_responset::ERRORED;
   }
 #ifdef _WIN32
-  if(!WriteFile(child_std_IN_Wr, message.c_str(), message.size(), NULL, NULL))
+  const auto message_size = narrow<DWORD>(message.size());
+  DWORD bytes_written = 0;
+  if(!WriteFile(
+       child_std_IN_Wr, message.c_str(), message_size, &bytes_written, NULL))
   {
     // Error handling with GetLastError ?
     return send_responset::FAILED;
   }
+  INVARIANT(
+    message_size == bytes_written,
+    "Number of bytes written to sub process must match message size.");
 #else
   // send message to solver process
   int send_status = fputs(message.c_str(), command_stream);
@@ -415,15 +425,22 @@ bool piped_processt::can_receive(optionalt<std::size_t> wait_time)
   const int timeout = wait_time ? narrow<int>(*wait_time) : -1;
 #ifdef _WIN32
   int waited_time = 0;
-  // The next four need to be initialised for compiler warnings
-  DWORD buffer = 0;
-  LPDWORD nbytes = 0;
-  LPDWORD rbytes = 0;
-  LPDWORD rmbytes = 0;
+  DWORD total_bytes_available = 0;
   while(timeout < 0 || waited_time >= timeout)
   {
-    PeekNamedPipe(child_std_OUT_Rd, &buffer, 1, nbytes, rbytes, rmbytes);
-    if(buffer != 0)
+    const LPVOID lpBuffer = nullptr;
+    const DWORD nBufferSize = 0;
+    const LPDWORD lpBytesRead = nullptr;
+    const LPDWORD lpTotalBytesAvail = &total_bytes_available;
+    const LPDWORD lpBytesLeftThisMessage = nullptr;
+    PeekNamedPipe(
+      child_std_OUT_Rd,
+      lpBuffer,
+      nBufferSize,
+      lpBytesRead,
+      lpTotalBytesAvail,
+      lpBytesLeftThisMessage);
+    if(total_bytes_available > 0)
     {
       return true;
     }

src/util/piped_process.h

@@ -13,6 +13,7 @@ typedef struct _PROCESS_INFORMATION PROCESS_INFORMATION; // NOLINT
 typedef void *HANDLE;                                    // NOLINT
 #endif
 
+#include "nodiscard.h"
 #include "optional.h"
 #include <vector>
 
@@ -42,7 +43,7 @@ class piped_processt
   /// Send a string message (command) to the child process.
   /// \param message The string message to be sent.
   /// \return
-  send_responset send(const std::string &message);
+  NODISCARD send_responset send(const std::string &message);
   /// Read a string from the child process' output.
   /// \return a string containing data from the process, empty string if no data
   std::string receive();

unit/util/piped_process.cpp

@@ -107,8 +107,6 @@ TEST_CASE(
   REQUIRE(calc < 2);
 }
 
-#ifndef _WIN32
-// No Windows tests for z3 due to path and dependency issues.
 TEST_CASE(
   "Creating a sub process of z3 and read a response from an echo command.",
   "[core][util][piped_process][.z3]")
@@ -314,4 +312,3 @@ TEST_CASE(
   REQUIRE(
     process.send("(exit)\n") == piped_processt::send_responset::SUCCEEDED);
 }
-#endif