Add debug logging for piped_process failures

Author: thomasspriggs

src/solvers/smt2_incremental/smt_solver_process.cpp

@@ -13,7 +13,8 @@ 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,22 @@ 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 +380,16 @@ 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

@@ -15,6 +15,7 @@ typedef void *HANDLE;                                    // NOLINT
 
 #include "nodiscard.h"
 #include "optional.h"
+#include "message.h"
 #include <vector>
 
 #define PIPED_PROCESS_INFINITE_TIMEOUT                                         \
@@ -79,7 +80,9 @@ 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.
@@ -108,6 +111,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