Add additional retries in piped_processt::send on Windows

Author: thomasspriggs

src/util/piped_process.cpp

@@ -351,30 +351,27 @@ 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())
-  {
-    // 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)
+  const int retry_limit = 10;
+  for(int send_attempts = 0; send_attempts < retry_limit; ++send_attempts)
   {
-    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 ?
       return send_responset::FAILED;
     }
+    if(bytes_written != 0)
+      break;
+    // Give the sub-process chance to read the waiting message(s).
+    FlushFileBuffers(child_std_IN_Wr);
   }
   INVARIANT(
     message_size == bytes_written,