Add debug logging for piped_process failures

Author: thomasspriggs

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

@@ -124,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
@@ -365,14 +368,19 @@ piped_processt::send_responset piped_processt::send(const std::string &message)
     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(1 << send_attempts);
+    Sleep(wait_milliseconds);
   }
   INVARIANT(
     message_size == bytes_written,

src/util/piped_process.h

@@ -13,6 +13,7 @@ typedef struct _PROCESS_INFORMATION PROCESS_INFORMATION; // NOLINT
 typedef void *HANDLE;                                    // NOLINT
 #endif
 
+#include "message.h"
 #include "nodiscard.h"
 #include "optional.h"
 
@@ -80,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.
@@ -109,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 (> "