Merge pull request #6675 from thomasspriggs/tas/windows_pipe_robustness

Improvements to robustness of piped process support on Windows

Author: thomasspriggs

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc

@@ -1,6 +1,6 @@
 CORE
 simple_equation.c
---incremental-smt2-solver 'z3 --smt2 -in' --trace
+--incremental-smt2-solver 'z3 --smt2 -in' --trace --verbosity 10
 \[main\.assertion\.1\] line \d+ a plus a always equals two times a: SUCCESS
 \[main\.assertion\.2\] line \d+ a minus a always equals 0: SUCCESS
 \[main\.assertion\.3\] line \d+ a plus its additive inverse equals 0: SUCCESS

src/solvers/smt2_incremental/smt_solver_process.cpp

@@ -13,7 +13,7 @@ smt_piped_solver_processt::smt_piped_solver_processt(
   std::string command_line,
   message_handlert &message_handler)
   : command_line_description{"\"" + command_line + "\""},
-    process{split_string(command_line, ' ', false, true)},
+    process{split_string(command_line, ' ', false, true), message_handler},
     log{message_handler}
 {
 }

src/util/piped_process.cpp

@@ -88,18 +88,22 @@
 #  include <unistd.h> // library for read/write/sleep/etc. functions
 #endif
 
-#  include <cstring> // library for strerror function (on linux)
-#  include <iostream>
-#  include <vector>
+#include "exception_utils.h"
+#include "invariant.h"
+#include "narrow.h"
+#include "optional.h"
+#include "piped_process.h"
+#include "string_utils.h"
 
-#  include "exception_utils.h"
-#  include "invariant.h"
-#  include "narrow.h"
-#  include "optional.h"
-#  include "piped_process.h"
-#  include "string_utils.h"
+#include <cstring> // library for strerror function (on linux)
+#include <iostream>
+#include <vector>
 
+#ifdef _WIN32
+#  define BUFSIZE (1024 * 64)
+#else
 #  define BUFSIZE 2048
+#endif
 
 #ifdef _WIN32
 /// This function prepares a single wide string for the windows command
@@ -120,7 +124,10 @@ prepare_windows_command_line(const std::vector<std::string> &commandvec)
 }
 #endif
 
-piped_processt::piped_processt(const std::vector<std::string> &commandvec)
+piped_processt::piped_processt(
+  const std::vector<std::string> &commandvec,
+  message_handlert &message_handler)
+  : log{message_handler}
 {
 #  ifdef _WIN32
   // Security attributes for pipe creation
@@ -347,34 +354,40 @@ piped_processt::send_responset piped_processt::send(const std::string &message)
   }
 #ifdef _WIN32
   const auto message_size = narrow<DWORD>(message.size());
+  PRECONDITION(message_size > 0);
   DWORD bytes_written = 0;
-  const auto write_file = [&]() {
-    return WriteFile(
-      child_std_IN_Wr, message.c_str(), message_size, &bytes_written, NULL);
-  };
-  if(!write_file())
+  const int retry_limit = 10;
+  for(int send_attempts = 0; send_attempts < retry_limit; ++send_attempts)
   {
-    // Error handling with GetLastError ?
-    return send_responset::FAILED;
-  }
-  // `WriteFile` can return a success status but write 0 bytes if we write
-  // messages quickly enough. This problem has been observed when using a
-  // release build, but resolved when using a debug build or `--verbosity 10`.
-  // Presumably this happens if cbmc gets too far ahead of the sub process.
-  // Flushing the buffer and retrying should then succeed to write the message
-  // in this case.
-  if(bytes_written == 0)
-  {
-    FlushFileBuffers(child_std_IN_Wr);
-    if(!write_file())
+    // `WriteFile` can return a success status but write 0 bytes if we write
+    // messages quickly enough. This problem has been observed when using a
+    // release build, but resolved when using a debug build or `--verbosity 10`.
+    // Presumably this happens if cbmc gets too far ahead of the sub process.
+    // Flushing the buffer and retrying should then succeed to write the message
+    // in this case.
+    if(!WriteFile(
+         child_std_IN_Wr, message.c_str(), message_size, &bytes_written, NULL))
     {
-      // Error handling with GetLastError ?
+      const DWORD error_code = GetLastError();
+      log.debug() << "Last error code is " + std::to_string(error_code)
+                  << messaget::eom;
       return send_responset::FAILED;
     }
+    if(bytes_written != 0)
+      break;
+    // Give the sub-process chance to read the waiting message(s).
+    const auto wait_milliseconds = narrow<DWORD>(1 << send_attempts);
+    log.debug() << "Zero bytes send to sub process. Retrying in "
+                << wait_milliseconds << " milliseconds." << messaget::eom;
+    FlushFileBuffers(child_std_IN_Wr);
+    Sleep(wait_milliseconds);
   }
   INVARIANT(
     message_size == bytes_written,
-    "Number of bytes written to sub process must match message size.");
+    "Number of bytes written to sub process must match message size."
+    "Message size is " +
+      std::to_string(message_size) + " but " + std::to_string(bytes_written) +
+      " bytes were written.");
 #else
   // send message to solver process
   int send_status = fputs(message.c_str(), command_stream);

src/util/piped_process.h

@@ -13,8 +13,10 @@ typedef struct _PROCESS_INFORMATION PROCESS_INFORMATION; // NOLINT
 typedef void *HANDLE;                                    // NOLINT
 #endif
 
+#include "message.h"
 #include "nodiscard.h"
 #include "optional.h"
+
 #include <vector>
 
 #define PIPED_PROCESS_INFINITE_TIMEOUT                                         \
@@ -79,7 +81,10 @@ class piped_processt
   /// Initiate a new subprocess with pipes supporting communication
   /// between the parent (this process) and the child.
   /// \param commandvec The command and arguments to create the process
-  explicit piped_processt(const std::vector<std::string> &commandvec);
+  /// \param message_handler Optional message handler for logging debug messages
+  explicit piped_processt(
+    const std::vector<std::string> &commandvec,
+    message_handlert &message_handler);
 
   // Deleted due to declaring an explicit destructor and not wanting copy
   // constructors to be implemented.
@@ -108,6 +113,7 @@ class piped_processt
   int pipe_output[2];
 #endif
   statet process_state;
+  messaget log;
 };
 
 #endif // endifndef CPROVER_UTIL_PIPED_PROCESS_H

unit/util/piped_process.cpp

@@ -2,10 +2,13 @@
 /// \author Diffblue Ltd.
 /// Unit tests for checking the piped process communication mechanism.
 
-#  include <testing-utils/use_catch.h>
-#  include <util/optional.h>
-#  include <util/piped_process.h>
-#  include <util/string_utils.h>
+#include <util/optional.h>
+#include <util/piped_process.h>
+#include <util/string_utils.h>
+
+#include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
+
 // Used for testing destructor/timing
 #include <chrono>
 
@@ -22,7 +25,7 @@ TEST_CASE(
   commands.push_back("/bin/echo");
   commands.push_back(to_be_echoed);
 #endif
-  piped_processt process(commands);
+  piped_processt process(commands, null_message_handler);
 
   // This is an indirect way to detect when the pipe has something. This
   // could (in theory) also return when there is an error, but this unit
@@ -45,7 +48,7 @@ TEST_CASE(
   const std::string expected_error("Launching abcde failed");
   commands.push_back("abcde");
 #endif
-  piped_processt process(commands);
+  piped_processt process(commands, null_message_handler);
 
   // This is an indirect way to detect when the pipe has something. This
   // could (in theory) also return when there is an error, but this unit
@@ -81,7 +84,7 @@ TEST_CASE(
     std::chrono::steady_clock::now();
   {
     // Scope restriction to cause destruction
-    piped_processt process(commands);
+    piped_processt process(commands, null_message_handler);
   }
   std::chrono::steady_clock::time_point end_time =
     std::chrono::steady_clock::now();
@@ -95,7 +98,7 @@ TEST_CASE(
 #  if 0
   commands.push_back("sleep 6");
   time_t calc = time(NULL);
-  piped_processt process(commands);
+  piped_processt process(commands, null_message_handler);
   process.~piped_processt();
   calc = time(NULL) - calc;
 #  else
@@ -114,7 +117,7 @@ TEST_CASE(
   std::vector<std::string> commands;
   commands.push_back("z3");
   commands.push_back("-in");
-  piped_processt process(commands);
+  piped_processt process(commands, null_message_handler);
 
   REQUIRE(
     process.send("(echo \"hi\")\n") ==
@@ -136,7 +139,7 @@ TEST_CASE(
   commands.push_back("z3");
   commands.push_back("-in");
   const std::string termination_statement = "(exit)\n";
-  piped_processt process(commands);
+  piped_processt process(commands, null_message_handler);
 
   REQUIRE(
     process.send("(echo \"hi\")\n") ==
@@ -166,7 +169,7 @@ TEST_CASE(
   commands.push_back("z3");
   commands.push_back("-in");
   commands.push_back("-smt2");
-  piped_processt process(commands);
+  piped_processt process(commands, null_message_handler);
 
   std::string message =
     "(set-logic QF_LIA) (declare-const x Int) (declare-const y Int) (assert (> "
@@ -190,7 +193,7 @@ TEST_CASE(
   commands.push_back("z3");
   commands.push_back("-in");
   commands.push_back("-smt2");
-  piped_processt process(commands);
+  piped_processt process(commands, null_message_handler);
 
   std::string statement =
     "(set-logic QF_LIA) (declare-const x Int) (declare-const y Int) (assert (> "
@@ -212,7 +215,7 @@ TEST_CASE(
   std::vector<std::string> commands;
   commands.push_back("z3");
   commands.push_back("-in");
-  piped_processt process(commands);
+  piped_processt process(commands, null_message_handler);
 
   REQUIRE(
     process.send("(echo \"hi\")\n") ==
@@ -242,7 +245,7 @@ TEST_CASE(
   commands.push_back("z3");
   commands.push_back("-in");
   commands.push_back("-smt2");
-  piped_processt process(commands);
+  piped_processt process(commands, null_message_handler);
 
   std::string statement =
     "(set-logic QF_LIA) (declare-const x Int) (declare-const y Int) (assert (> "
@@ -298,7 +301,7 @@ TEST_CASE(
   commands.push_back("z3");
   commands.push_back("-in");
   commands.push_back("-smt2");
-  piped_processt process(commands);
+  piped_processt process(commands, null_message_handler);
 
   std::string statement =
     "(set-logic QF_LIA) (declare-const x Int) (declare-const y Int) (assert (> "