Check that the timeout is correctly implemented for all the supported smt solvers

[ggrieco-tob]

The timeout option is very important to make sure the solver don't take forever. It's unclear if they work as expected.

[ggrieco-tob]

#2418 fixed the timeouts for the recently added solvers, however manticore still does not enforce timeouts if the it is blocked waiting for a solver result. That should be fixed in #2420 when solver uses a non-blocking call to read their results.

[ggrieco-tob]

The --smt.timeout seems to have no effect at all, the value used is always 120 seconds. I think @ekilmer was taking a look to that..

[ekilmer]

I tried testing this and it seems to propagate correctly:

    1 root       20   0 20356  3856  3344 S  0.0  0.0  0:00.25 /bin/bash
 9760 root       20   0  670M  380M 20164 S  0.7  0.9  1:16.37 └─ /usr/bin/python3 /usr/local/bin/manticore --smt.timeout 567 -v --core.procs 1 /bin/ls ++++
 9788 root       20   0  119M 19320 11876 S  0.0  0.0  0:00.80    ├─ z3 -t 567000 -memory 8192 -smt2 -in
 9789 root       20   0  119M 19320 11876 S  0.0  0.0  0:00.00    │  └─ z3 -t 567000 -memory 8192 -smt2 -in

Do you have an example where you see differently?

[ggrieco-tob]

The --smt.timeout seems to have no effect at all, the value used is always 120 seconds. I think @ekilmer was taking a look to that..

This is wrong in fact, only happens on one of my PRs (this should be fixed soon). However, it looks like global timeout is not enforced if the worker is busy waiting for a result here:

manticore/manticore/core/smtlib/solver.py

Lines 214 to 217 in 2e990ba

	def __readline_and_count(self):
	assert self._proc
	assert self._proc.stdout
	buf = self._proc.stdout.readline() # No timeout enforced here

This should be fixed in #2420 using a non-blocking read.