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

@@ -79,7 +79,6 @@
 #  include "run.h"     // for Windows arg quoting
 #  include "unicode.h" // for widen function
 #  include <tchar.h>   // library for _tcscpy function
-#  include <util/make_unique.h>
 #  include <windows.h>
 #else
 #  include <fcntl.h>  // library for fcntl function
@@ -90,6 +89,7 @@
 
 #include <util/exception_utils.h>
 #include <util/invariant.h>
+#include <util/make_unique.h>
 #include <util/narrow.h>
 #include <util/optional.h>
 #include <util/piped_process.h>
@@ -124,7 +124,23 @@ prepare_windows_command_line(const std::vector<std::string> &commandvec)
 }
 #endif
 
-piped_processt::piped_processt(const std::vector<std::string> &commandvec)
+messaget piped_processt::make_log(message_handlert *message_handler)
+{
+  if(message_handler)
+  {
+    return messaget{*message_handler};
+  }
+  else
+  {
+    null_handler = util_make_unique<null_message_handlert>();
+    return messaget{*null_handler};
+  }
+}
+
+piped_processt::piped_processt(
+  const std::vector<std::string> &commandvec,
+  message_handlert *message_handler)
+  : log{make_log(message_handler)}
 {
 #  ifdef _WIN32
   // Security attributes for pipe creation
@@ -365,12 +381,17 @@ 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);
   }

src/util/piped_process.h

@@ -6,16 +6,17 @@
 #define CPROVER_UTIL_PIPED_PROCESS_H
 
 #ifdef _WIN32
-#  include <memory>
 // The below are forward declarations for Windows APIs
 struct _PROCESS_INFORMATION;                             // NOLINT
 typedef struct _PROCESS_INFORMATION PROCESS_INFORMATION; // NOLINT
 typedef void *HANDLE;                                    // NOLINT
 #endif
 
+#include <util/message.h>
 #include <util/nodiscard.h>
 #include <util/optional.h>
 
+#include <memory>
 #include <vector>
 
 #define PIPED_PROCESS_INFINITE_TIMEOUT                                         \
@@ -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 = nullptr);
 
   // Deleted due to declaring an explicit destructor and not wanting copy
   // constructors to be implemented.
@@ -109,6 +113,10 @@ class piped_processt
   int pipe_output[2];
 #endif
   statet process_state;
+
+  messaget make_log(message_handlert *message_handler);
+  std::unique_ptr<null_message_handlert> null_handler;
+  messaget log;
 };
 
 #endif // endifndef CPROVER_UTIL_PIPED_PROCESS_H