Piped communication on Windows #6180

TGWDB · 2021-06-15T15:50:05Z

Piped inter-process communication for Windows.

Old text below.

This is a PR to test CI and see how the piped communication progresses on Windows. This started based on #6151 and so will need to either wait for that to be merged and rebased, or supersede that PR.

Note that this is part of the larger SMT plan available at #6134 .

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2021-06-15T17:32:54Z

Codecov Report

Merging #6180 (e530e4a) into develop (4c039ba) will increase coverage by 0.00%.
The diff coverage is 79.48%.

@@            Coverage Diff            @@
##           develop    #6180    +/-   ##
=========================================
  Coverage    75.98%   75.98%            
=========================================
  Files         1507     1512     +5     
  Lines       163237   163458   +221     
=========================================
+ Hits        124032   124208   +176     
- Misses       39205    39250    +45

Impacted Files	Coverage Δ
unit/util/piped_process.cpp	`30.65% <57.14%> (+2.08%)`	⬆️
src/util/piped_process.cpp	`76.92% <83.33%> (+1.92%)`	⬆️
src/goto-instrument/contracts/contracts.cpp	`92.59% <100.00%> (ø)`
src/goto-instrument/loop_utils.cpp	`90.62% <0.00%> (-3.93%)`	⬇️
src/solvers/flattening/arrays.cpp	`80.45% <0.00%> (-2.84%)`	⬇️
...sensitivity/variable_sensitivity_configuration.cpp	`80.95% <0.00%> (-2.07%)`	⬇️
...nsitivity/three_way_merge_abstract_interpreter.cpp	`93.02% <0.00%> (-1.32%)`	⬇️
src/solvers/smt2/smt2_parser.cpp	`77.00% <0.00%> (-0.91%)`	⬇️
src/solvers/flattening/boolbv_floatbv_op.cpp	`60.21% <0.00%> (-0.84%)`	⬇️
src/analyses/ai.h	`57.36% <0.00%> (-0.78%)`	⬇️
... and 59 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update d6fe178...e530e4a. Read the comment docs.

kroening · 2021-06-16T07:43:54Z

src/util/piped_process.cpp

+  sec_attr.nLength = sizeof(SECURITY_ATTRIBUTES);
+  sec_attr.bInheritHandle = TRUE;
+  sec_attr.lpSecurityDescriptor = NULL;
+  // Use named pipes to allow non-blocking read


What access rights does this security descriptor grant? The default one for named pipes gives read access to the EVERYONE group.

If I read the documentation here correctly then by defining the security attributes for null for lpSecurityDescriptor (sec_attr approx line 30 of src/util/piped_process.cpp) this sets the security to be the default for the current session access token. In particular this is NOT available to all users.

That said, I'll add comment about this to the code.

Added comment to code as well.

kroening · 2021-06-16T07:44:38Z

src/util/piped_process.cpp

+  // Use named pipes to allow non-blocking read
+  child_std_IN_Rd = CreateNamedPipe(
+      TEXT("\\\\.\\pipe\\cbmc\\SMT2\\child\\IN"),
+      PIPE_ACCESS_INBOUND,          // Reading for us


What happens when there are multiple instances of CBMC running simultaneously? Do they all try to talk over the same named pipe?

Fixed with use of random number.

rand isn't random, but produces a deterministic sequence unless you change the seed.
Consider using something you know to be unique, say a process ID.

It was seeded, but process ID is better - done.

kroening · 2021-06-16T07:48:03Z

src/util/piped_process.cpp

+  for(int i = 0; i < commandvec.size(); i++)
+  {
+    cmdline.append(commandvec[i].c_str());
+    cmdline.append(" ");


This will require quoting. Use quote_windows_arg from util/run.cpp

I'd prefer to leave this to the calling code to properly ensure the handling of quotations (also this breaks unit tests and makes for messy dependencies for now).

This is a no-go, since it has security implications.

Added quoting here.

kroening · 2021-06-16T07:59:12Z

src/util/piped_process.cpp

+    }
+// TODO, make this define and choice better
+#  define WIN_POLL_WAIT 10
+    Sleep(WIN_POLL_WAIT);


There is no better option than polling? This will heat a lot of CPUs!

I haven't found evidence of one that works nicely with our asynchronous reading from named pipes. The options available for waiting appear to work with blocking pipes, but this does not work with our interactive approach (at least at the moment).

If someone who knows Windows better can suggest an alternative I'll look into it.

I'd say this is a blocker for using this.

MsgWaitForMultipleObjectsEx might do the right thing.

WaitForMultipleObjects (and similar ones) rely upon the events they wait on being synchronous. This (so far in testing and from what I've read) means we have to wait for the child process to finish before we can read from the pipe. I saw some example code that used this approach with asynchronous pipes, but then used a busy loop with peek in the same way I've implemented currently.

I'll keep looking, and play around more now I've sorted out most of the other quirks.

See comment/discussion at the top of the file for more on why this is done this way.

kroening · 2021-06-16T13:14:45Z

src/util/piped_process.cpp

+  TCHAR *szCmdline =
+    reinterpret_cast<TCHAR *>(malloc(sizeof(TCHAR) * cmdline.size()));
+  _tcscpy(szCmdline, cmdline.c_str());
+  success = CreateProcess(


This should use CreateProcessW, and widen(cmdline)

Done, along with quoting.

kroening · 2021-06-16T13:15:13Z

src/util/piped_process.cpp

+  TerminateProcess(proc_info.hProcess, 0);
+  CloseHandle(proc_info.hProcess);
+  CloseHandle(proc_info.hThread);
+#else


Does this clean up the named pipe?

According to the docs when all handles are closed/released then Windows cleans up the pipe. I've pushed some more aggressive killing and disconnecting of the child process, but it probably makes no difference in practice.

kroening · 2021-06-16T15:57:49Z

src/util/piped_process.cpp

+  // and causes heap corruption in Windows if we free!
+  WCHAR *szCmdline =
+    reinterpret_cast<WCHAR *>(malloc(sizeof(WCHAR) * cmdline.size()));
+  wcscpy(szCmdline, cmdline.c_str());


You need to add one WCHAR to the size of the allocated buffer for the terminating zero.
To avoid this problem altogether, use _wcsdup.

kroening · 2021-06-16T15:59:35Z

src/util/piped_process.cpp

+    while(i < commandvec.size())
+    {
+      args[i] = strdup(commandvec[i].c_str());
+      i++;


No need for the strdup, and the subsequent free.

The child process wants to be able to modify the arguments (i.e. non const) while the commandvec with c_str()can only provide const instances.

This memory is not shared with the child; the child gets a copy. const is fine.

Please add the const to the type of args. There is then no need for the const_cast.

TGWDB · 2021-08-11T13:53:27Z

Now rebased on develop after merging of #6151 .

thomasspriggs

Great to see some more progress on this, but there are some 🚫 issues which we should address before merging this.

src/util/piped_process.cpp

thomasspriggs · 2021-08-11T16:00:48Z

src/util/piped_process.cpp

  if(process_state != statet::CREATED)
  {
-    return send_responset::ERROR;
+    return send_responset::ERRORED;


⛏️ I would have kept this rename in a separate commit, in order to keep the commits smaller and restricted to a single change. I consider this something to consider for next time, rather than something worth editing the commit history to fix.

src/util/piped_process.cpp

thomasspriggs · 2021-08-11T16:45:34Z

src/util/piped_process.cpp

+  LPDWORD nbytes = 0;
+  LPDWORD rbytes = 0;
+  LPDWORD rmbytes = 0;
+  while(timeout < 0 || waited_time >= timeout)


⛏️ The magic value of -1 for timeout is set due to the unix API being used. I suggest the "unwrap" is moved into the non-Windows code and this line be written as while(!wait_time || waited_time >= *wait_time)

src/util/piped_process.h

unit/util/piped_process.cpp

peterschrammel · 2021-08-12T09:56:12Z

src/util/piped_process.cpp

+// access from the same session token/permissions. This SHOULD be sufficient
+// for what we need.
+//
+// Non-blocking pipes allow immediate reading of any data on the pipre which


peterschrammel · 2021-08-12T09:56:27Z

src/util/piped_process.cpp

+// for what we need.
+//
+// Non-blocking pipes allow immediate reading of any data on the pipre which
+// matches the Linux/MasOC pipe behvariour and also allows reading of the


Also: MacOS

peterschrammel · 2021-08-12T09:58:08Z

src/util/piped_process.cpp

+//    finished, again undoing the interactive behaviour desired.
+// Since none of the above work effectivley, the chosen approach is to use a
+// non-blocking peek to see if there is anthing to read, and use a sleep and
+// poll behaviour that might be puch busier than we want. At the time of


peterschrammel · 2021-08-12T10:04:25Z

src/util/piped_process.cpp

+//    means the example above cannot read "The Jabberwocky" until the ping has
+//    finished, again undoing the interactive behaviour desired.
+// Since none of the above work effectivley, the chosen approach is to use a
+// non-blocking peek to see if there is anthing to read, and use a sleep and


Would something like this work instead of sleep or is this no better but just with more overhead?

do { // check whether there's something new } while (WaitForSingleObject(hEvent, 100) == WAIT_TIMEOUT)

Those don't work on non-blocking pipes, they immediately return and so would not actually sleep.

peterschrammel · 2021-08-12T10:11:14Z

src/util/piped_process.cpp

-  UNIMPLEMENTED_FEATURE("Pipe IPC on windows.")
+  // Security attributes for pipe creation
+  SECURITY_ATTRIBUTES sec_attr;
+  // Ensure pipes are inherited


comment should be one line further down

peterschrammel · 2021-08-12T10:18:04Z

src/util/piped_process.cpp

+    PIPE_UNLIMITED_INSTANCES,     // Probably doesn't matter
+    BUFSIZE,
+    BUFSIZE,    // Output and input bufffer sizes
+    0,          // Timeout in ms, 0 = use system default


This is the timeout to detect that the other side hasn't connected, I guess?

Any insights on this? Would be good to explain to save follow-ups the time for investigating how the API works.

peterschrammel · 2021-08-12T10:22:06Z

src/util/piped_process.cpp

+    &sec_attr); // For inheritance by child
+  if(child_std_IN_Rd == INVALID_HANDLE_VALUE)
+  {
+    throw std::runtime_error("Input pipe creation failed for child_std_IN_Rd");


I think we have exception types in util/exception_util.h that are more suitable.

peterschrammel · 2021-08-12T10:23:13Z

src/util/piped_process.cpp

@@ -30,8 +101,127 @@

 piped_processt::piped_processt(const std::vector<std::string> commandvec)
 {
+  // Default state


Would it be possible to split up this mega-function a bit?

Split out a small helper function, but the function is pretty straightforward, just many lines due to many arguments to function calls to create Windows processes/pipes (also lots of commends/explanation).

tautschnig · 2021-08-12T13:29:56Z

src/util/piped_process.cpp

+// for what we need.
+//
+// Non-blocking pipes allow immediate reading of any data on the pipre which
+// matches the Linux/MasOC pipe behvariour and also allows reading of the


Also: MacOS

tautschnig · 2021-08-12T13:32:18Z

src/util/piped_process.cpp

@@ -30,8 +101,127 @@

 piped_processt::piped_processt(const std::vector<std::string> commandvec)


I recognise this was here before, but any insight as to why this isn't being passed as a reference? The const doesn't seem terribly useful at present.

No insight, but fixed now.

tautschnig · 2021-08-12T13:33:23Z

src/util/piped_process.cpp

+  sec_attr.lpSecurityDescriptor = NULL;
+  // Use named pipes to allow non-blocking read
+  // Build the base name for the pipes
+  std::string base_name = "\\\\.\\pipe\\cbmc\\SMT2\\child\\";


This is generic code in util, I don't think it should hard-code SMT2.

Make the quote_windows_arg function available for use

This adds in windows versions of the piped_process communication functions.

Adds unit tests for Windows piped process communication. These duplicate the Linux/MacOS ones in most cases. There is also a termination one that does not have a working Linux/MacOS version. (Also z3 is not tested on Windows).

This removes the copy operations from the piped_process class since we do not want to implement these. Also fix unit tests that used these.

This fixes the unit tests to use the std::chrono library insead of windows.h for timing information.

Instead of calling the destructor explicitly, use braces to scope and use implicit destructor calling.

This fixes the including of windows.h to limited scope. Requires some forward definition and uses unique_ptr.

Replace std::* exceptions in Windows code with system_exceptiont

Split out a helper function to process an array of strings into a single wide string for use in Windows commands.

Reduce the number of possible states for the piped_process statet since we only really need to know if it's running or has an error for now.

src/util/piped_process.cpp

This changes to pass the vector of strings for the piped_process command by reference instead of by value. Also add some doxygen and static keyword

thomasspriggs

👍

peterschrammel · 2021-08-23T09:09:43Z

src/util/piped_process.cpp

+    PIPE_UNLIMITED_INSTANCES,     // Probably doesn't matter
+    BUFSIZE,
+    BUFSIZE,    // Output and input bufffer sizes
+    0,          // Timeout in ms, 0 = use system default


Any insights on this? Would be good to explain to save follow-ups the time for investigating how the API works.

peterschrammel · 2021-08-23T09:13:54Z

unit/util/piped_process.cpp

  std::vector<std::string> commands;
+#ifdef _WIN32
+  const std::string expected_error("'abcde' is not recogni");


Suggested change

const std::string expected_error("'abcde' is not recogni");

const std::string expected_error("'abcde' is not recognized");

peterschrammel · 2021-08-23T09:14:10Z

unit/util/piped_process.cpp

+      end_time - start_time);
+  size_t calc = time_span.count();
+#else
+  // Currently not working under Linxu/MacOS?!


Suggested change

// Currently not working under Linxu/MacOS?!

// Currently not working under Linux/MacOS?!

peterschrammel · 2021-08-23T09:14:39Z

unit/util/piped_process.cpp

+  size_t calc = time_span.count();
+#else
+  // Currently not working under Linxu/MacOS?!
+  // commands.push_back("sleep 6");


Put in #if 0 rather than commenting.

Add comment on timeout in windows.

Tidy up unit test code to have cleaner string in windows failed command test, and useful #if for non-working code.

TGWDB added SMT Backend Interface do not merge work in progress dependent - do not merge labels Jun 15, 2021

kroening reviewed Jun 16, 2021

View reviewed changes

TGWDB force-pushed the pipes_infr_win branch 2 times, most recently from 498108c to 1ef5767 Compare June 17, 2021 11:07

tautschnig assigned TGWDB Aug 11, 2021

TGWDB force-pushed the pipes_infr_win branch from 92a9a42 to f86ea58 Compare August 11, 2021 13:51

TGWDB marked this pull request as ready for review August 11, 2021 13:52

TGWDB requested review from peterschrammel and tautschnig as code owners August 11, 2021 13:52

TGWDB removed do not merge work in progress dependent - do not merge labels Aug 11, 2021

TGWDB changed the title ~~Piped communication on Windows [DRAFT and RFC]~~ Piped communication on Windows Aug 11, 2021

thomasspriggs suggested changes Aug 11, 2021

View reviewed changes

peterschrammel reviewed Aug 12, 2021

View reviewed changes

tautschnig reviewed Aug 12, 2021

View reviewed changes

TGWDB force-pushed the pipes_infr_win branch 2 times, most recently from 3ce4876 to 9cc1d5a Compare August 16, 2021 15:20

Expose quote_windows_arg

ffacdea

Make the quote_windows_arg function available for use

TGWDB force-pushed the pipes_infr_win branch from 1ebad86 to d2b629b Compare August 17, 2021 08:55

TGWDB added 9 commits August 17, 2021 09:56

Add in Windows version of piped_process functions

20c51db

This adds in windows versions of the piped_process communication functions.

Add unit tests for Windows piped process IPC

fab21fe

Adds unit tests for Windows piped process communication. These duplicate the Linux/MacOS ones in most cases. There is also a termination one that does not have a working Linux/MacOS version. (Also z3 is not tested on Windows).

Fix missing copy operations (delete them)

c90b2fe

This removes the copy operations from the piped_process class since we do not want to implement these. Also fix unit tests that used these.

Fix unit tests to use std::chrono not Windows.h

803de49

This fixes the unit tests to use the std::chrono library insead of windows.h for timing information.

Fix destructor scope to fix termination test

dfd28af

Instead of calling the destructor explicitly, use braces to scope and use implicit destructor calling.

Fix include scoping and use unique_ptr

3f9fe4a

This fixes the including of windows.h to limited scope. Requires some forward definition and uses unique_ptr.

Fix to use system_exceptiont

c62310f

Replace std::* exceptions in Windows code with system_exceptiont

Split out helper function for Windows string construction

8510283

Split out a helper function to process an array of strings into a single wide string for use in Windows commands.

Reduce unecessary states for piped process statet

f60acac

Reduce the number of possible states for the piped_process statet since we only really need to know if it's running or has an error for now.

thomasspriggs reviewed Aug 17, 2021

View reviewed changes

src/util/piped_process.cpp Outdated Show resolved Hide resolved

src/util/piped_process.cpp Outdated Show resolved Hide resolved

src/util/piped_process.cpp Outdated Show resolved Hide resolved

src/util/piped_process.cpp Outdated Show resolved Hide resolved

TGWDB force-pushed the pipes_infr_win branch from d2b629b to cec11e1 Compare August 17, 2021 13:30

Pass commandvec by reference and small fixes

cec11e1

This changes to pass the vector of strings for the piped_process command by reference instead of by value. Also add some doxygen and static keyword

thomasspriggs approved these changes Aug 17, 2021

View reviewed changes

TGWDB requested review from peterschrammel and tautschnig August 17, 2021 13:49

peterschrammel approved these changes Aug 23, 2021

View reviewed changes

TGWDB added 2 commits August 23, 2021 10:40

Update comment on timeout in windows

f7e4440

Add comment on timeout in windows.

Tidy up unit test code

e530e4a

Tidy up unit test code to have cleaner string in windows failed command test, and useful #if for non-working code.

TGWDB merged commit dfa3810 into diffblue:develop Aug 23, 2021

		@@ -30,8 +101,127 @@

		piped_processt::piped_processt(const std::vector<std::string> commandvec)

	const std::string expected_error("'abcde' is not recogni");
	const std::string expected_error("'abcde' is not recognized");

	// Currently not working under Linxu/MacOS?!
	// Currently not working under Linux/MacOS?!

Piped communication on Windows #6180

Piped communication on Windows #6180

Uh oh!

Conversation

TGWDB commented Jun 15, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

codecov bot commented Jun 15, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Choose a reason for hiding this comment

Uh oh!

TGWDB Jun 16, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

TGWDB commented Aug 11, 2021

Uh oh!

thomasspriggs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

TGWDB commented Jun 15, 2021 •

edited

Loading

codecov bot commented Jun 15, 2021 •

edited

Loading

TGWDB Jun 16, 2021 •

edited

Loading