search

tweag / smtlib-backends

A Haskell library providing low-level functions for SMTLIB-based interaction with SMT solvers.
https://hackage.haskell.org/package/smtlib-backends
MIT License
17 stars 1 forks source link

`Backends.Process`: the test-suite may fail randomly #15

Closed qaristote closed 1 year ago

qaristote commented 1 year ago

Describe the bug When running the test suite of smtlib-backends, one of the assertions for the process backend may sometimes fail with the error Exception: waitForProcess: does not exist (No child processes). This doesn't happen too often so it shouldn't be too much of a problem but it can cause the CI checks to fail on correct code.

To Reproduce Unknown.

Expected behavior The tests shouldn't fail.

facundominguez commented 1 year ago

It is the process backend that fails, the Z3 backend doesn't use waitForProcess as far as I can tell. Here's the output of a failure: https://github.com/tweag/smtlib-backends/actions/runs/3685039572/jobs/6235500281

facundominguez commented 1 year ago

stopProcess makes some complicated things, and sometimes it may call to waitForProcess.

I think waitForProcess is terminating with an IOException, where ioe_errno is set to eCHILD.

Assuming a bug in stopProcess, one solution could be to catch and silence this kind of exceptions.

qaristote commented 1 year ago

It is the process backend that fails, the Z3 backend doesn't use waitForProcess as far as I can tell.

Indeed, my bad. I'll edit the issue accordingly.

qaristote commented 1 year ago

Oh this probably just happens because the sources all use ackCommand solver "(exit)", so the process stops itself before we can actually do it.

facundominguez commented 1 year ago

Sounds like a good conjecture.

qaristote commented 1 year ago

one solution could be to catch and silence this kind of exceptions

Do you think we should do that regardless of whether it's useful for our test-suite ? I'd say no because it would only allow unsafe uses of the Process backend, but maybe you disagree ?

facundominguez commented 1 year ago

Silencing exceptions is not ideal because it could mask other problems. But we don't need to do it now that we have something reasonable to try.

The documentation of the process backend should warn not to use close or with if the SMT solver is terminated with "(exit)".

facundominguez commented 1 year ago

Tests are still failing after #17: https://github.com/tweag/smtlib-backends/actions/runs/3688466600/jobs/6243305111

qaristote commented 1 year ago

This seems like it's still an issue in https://github.com/ucsd-progsys/liquid-fixpoint/pull/641. The origin of the bug seems to lie in the implementation of stopProcess which is used in Process.kill: https://github.com/fpco/typed-process/issues/38.