You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Since making the threading model the default form of multiprocessing (#1779), we've been encountering occasional worker crashes when performing long-running tasks due to SMTLib errors.
OS / Environment
Tested on Ubuntu 20.04 using Python 3.8.2
Behavior
The exceptions seem to fall into three broad categories:
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 356, in __getvalue_bv
expr, value = m.group("expr"), m.group("value") # type: ignore
AttributeError: 'NoneType' object has no attribute 'group'
m here is a regex match on the output of the SMT Solver. In other words, it's returning without finding the expected results. This is presumably due to invalid constraints being passed to it.
"Unknown Constant" means we asked the solver to use a variable without providing a definition for it. This could mean that some of our SMTLib constraints are not getting sent to the solver. Then again, the unknown constant is sometimes simply named a_, so it may be that we're just getting the numbering incorrect here.
We're getting the internal string "(BV #x0000555555556020)" as a response from (check-sat), which is not correct. Perhaps some sort of communication issue between the various Manticore threads and the solver process.
Any relevant logs
The following exceptions killed all 10 workers when running a sample script under Manticore:
; declare- line: 7043 position: 30
2020-10-06 16:22:18,701: [71691] m.c.worker:ERROR: Exception in state 1: AttributeError("'NoneType' object has no attribute 'group'")
Traceback (most recent call last):
File "/home/ehennenfent/manticore/manticore/core/worker.py", line 121, in run
current_state.execute()
File "/home/ehennenfent/manticore/manticore/native/state.py", line 192, in execute
result = self._platform.execute()
File "/home/ehennenfent/manticore/manticore/platforms/linux.py", line 2910, in execute
self.current.execute()
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 1017, in execute
implementation(*insn.operands)
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 1160, in new_method
return old_method(cpu, *args, **kw_args)
File "/home/ehennenfent/manticore/manticore/native/cpu/x86.py", line 5516, in MOVZX
op0.write(Operators.ZEXTEND(op1.read(), op0.size))
File "/home/ehennenfent/manticore/manticore/native/cpu/x86.py", line 778, in read
value = cpu.read_int(self.address(), self.size)
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 733, in read_int
data = self._memory.read(where, size // 8, force)
File "/home/ehennenfent/manticore/manticore/native/memory.py", line 1195, in read
solutions = self._try_get_solutions(address, size, "r", force=force)
File "/home/ehennenfent/manticore/manticore/native/memory.py", line 1338, in _try_get_solutions
solutions = solver.get_all_values(
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 535, in get_all_values
value = self._getvalue(var)
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 384, in _getvalue
return self.__getvalue_bv(expression.name)
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 356, in __getvalue_bv
expr, value = m.group("expr"), m.group("value") # type: ignore
AttributeError: 'NoneType' object has no attribute 'group'
2020-10-06 16:22:19,059: [71691] m.c.worker:ERROR: Exception in state 9: SolverError('(error "line 7043 column 42: unknown constant a_518854")')
Traceback (most recent call last):
File "/home/ehennenfent/manticore/manticore/core/worker.py", line 121, in run
current_state.execute()
File "/home/ehennenfent/manticore/manticore/native/state.py", line 192, in execute
result = self._platform.execute()
File "/home/ehennenfent/manticore/manticore/platforms/linux.py", line 2910, in execute
self.current.execute()
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 1017, in execute
implementation(*insn.operands)
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 1160, in new_method
return old_method(cpu, *args, **kw_args)
File "/home/ehennenfent/manticore/manticore/native/cpu/x86.py", line 5516, in MOVZX
op0.write(Operators.ZEXTEND(op1.read(), op0.size))
File "/home/ehennenfent/manticore/manticore/native/cpu/x86.py", line 778, in read
value = cpu.read_int(self.address(), self.size)
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 733, in read_int
data = self._memory.read(where, size // 8, force)
File "/home/ehennenfent/manticore/manticore/native/memory.py", line 1195, in read
solutions = self._try_get_solutions(address, size, "r", force=force)
File "/home/ehennenfent/manticore/manticore/native/memory.py", line 1338, in _try_get_solutions
solutions = solver.get_all_values(
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 534, in get_all_values
while self._is_sat():
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 338, in _is_sat
raise SolverError(status)
manticore.exceptions.SolverError: (error "line 7043 column 42: unknown constant a_518854")
2020-10-06 16:22:19,136: [71691] m.c.worker:ERROR: Exception in state 4: SolverError('(error "line 7045 column 74: unknown constant a_518854")')
Traceback (most recent call last):
File "/home/ehennenfent/manticore/manticore/core/worker.py", line 121, in run
current_state.execute()
File "/home/ehennenfent/manticore/manticore/native/state.py", line 192, in execute
result = self._platform.execute()
File "/home/ehennenfent/manticore/manticore/platforms/linux.py", line 2910, in execute
self.current.execute()
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 1017, in execute
implementation(*insn.operands)
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 1160, in new_method
return old_method(cpu, *args, **kw_args)
File "/home/ehennenfent/manticore/manticore/native/cpu/x86.py", line 5516, in MOVZX
op0.write(Operators.ZEXTEND(op1.read(), op0.size))
File "/home/ehennenfent/manticore/manticore/native/cpu/x86.py", line 778, in read
value = cpu.read_int(self.address(), self.size)
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 733, in read_int
data = self._memory.read(where, size // 8, force)
File "/home/ehennenfent/manticore/manticore/native/memory.py", line 1195, in read
solutions = self._try_get_solutions(address, size, "r", force=force)
File "/home/ehennenfent/manticore/manticore/native/memory.py", line 1338, in _try_get_solutions
solutions = solver.get_all_values(
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 534, in get_all_values
while self._is_sat():
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 338, in _is_sat
raise SolverError(status)
manticore.exceptions.SolverError: (error "line 7045 column 74: unknown constant a_518854")
==============
2020-10-06 16:22:26,164: [71691] m.c.worker:ERROR: Exception in state 8: SolverError('(error "line 7053 column 74: unknown constant a_518854")')
Traceback (most recent call last):
File "/home/ehennenfent/manticore/manticore/core/worker.py", line 121, in run
current_state.execute()
File "/home/ehennenfent/manticore/manticore/native/state.py", line 192, in execute
result = self._platform.execute()
File "/home/ehennenfent/manticore/manticore/platforms/linux.py", line 2910, in execute
self.current.execute()
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 1017, in execute
implementation(*insn.operands)
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 1160, in new_method
return old_method(cpu, *args, **kw_args)
File "/home/ehennenfent/manticore/manticore/native/cpu/x86.py", line 5516, in MOVZX
op0.write(Operators.ZEXTEND(op1.read(), op0.size))
File "/home/ehennenfent/manticore/manticore/native/cpu/x86.py", line 778, in read
value = cpu.read_int(self.address(), self.size)
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 733, in read_int
data = self._memory.read(where, size // 8, force)
File "/home/ehennenfent/manticore/manticore/native/memory.py", line 1195, in read
solutions = self._try_get_solutions(address, size, "r", force=force)
File "/home/ehennenfent/manticore/manticore/native/memory.py", line 1338, in _try_get_solutions
solutions = solver.get_all_values(
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 534, in get_all_values
while self._is_sat():
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 338, in _is_sat
raise SolverError(status)
manticore.exceptions.SolverError: (error "line 7053 column 74: unknown constant a_518854")
==============
2020-10-06 16:22:36,907: [71691] m.c.worker:ERROR: Exception in state 7: SolverError('(error "line 11489 column 66: unknown constant a_")')
Traceback (most recent call last):
File "/home/ehennenfent/manticore/manticore/core/worker.py", line 121, in run
current_state.execute()
File "/home/ehennenfent/manticore/manticore/native/state.py", line 192, in execute
result = self._platform.execute()
File "/home/ehennenfent/manticore/manticore/platforms/linux.py", line 2910, in execute
self.current.execute()
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 1017, in execute
implementation(*insn.operands)
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 1160, in new_method
return old_method(cpu, *args, **kw_args)
File "/home/ehennenfent/manticore/manticore/native/cpu/x86.py", line 5516, in MOVZX
op0.write(Operators.ZEXTEND(op1.read(), op0.size))
File "/home/ehennenfent/manticore/manticore/native/cpu/x86.py", line 778, in read
value = cpu.read_int(self.address(), self.size)
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 733, in read_int
data = self._memory.read(where, size // 8, force)
File "/home/ehennenfent/manticore/manticore/native/memory.py", line 1195, in read
solutions = self._try_get_solutions(address, size, "r", force=force)
File "/home/ehennenfent/manticore/manticore/native/memory.py", line 1338, in _try_get_solutions
solutions = solver.get_all_values(
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 534, in get_all_values
while self._is_sat():
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 338, in _is_sat
raise SolverError(status)
manticore.exceptions.SolverError: (error "line 11489 column 66: unknown constant a_")
================
2020-10-06 16:22:41,221: [71691] m.c.worker:ERROR: Exception in state 5: AttributeError("'NoneType' object has no attribute 'group'")
Traceback (most recent call last):
File "/home/ehennenfent/manticore/manticore/core/worker.py", line 121, in run
current_state.execute()
File "/home/ehennenfent/manticore/manticore/native/state.py", line 192, in execute
result = self._platform.execute()
File "/home/ehennenfent/manticore/manticore/platforms/linux.py", line 2910, in execute
self.current.execute()
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 1017, in execute
implementation(*insn.operands)
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 1160, in new_method
return old_method(cpu, *args, **kw_args)
File "/home/ehennenfent/manticore/manticore/native/cpu/x86.py", line 5516, in MOVZX
op0.write(Operators.ZEXTEND(op1.read(), op0.size))
File "/home/ehennenfent/manticore/manticore/native/cpu/x86.py", line 778, in read
value = cpu.read_int(self.address(), self.size)
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 733, in read_int
data = self._memory.read(where, size // 8, force)
File "/home/ehennenfent/manticore/manticore/native/memory.py", line 1195, in read
solutions = self._try_get_solutions(address, size, "r", force=force)
File "/home/ehennenfent/manticore/manticore/native/memory.py", line 1338, in _try_get_solutions
solutions = solver.get_all_values(
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 535, in get_all_values
value = self._getvalue(var)
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 384, in _getvalue
return self.__getvalue_bv(expression.name)
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 356, in __getvalue_bv
expr, value = m.group("expr"), m.group("value") # type: ignore
AttributeError: 'NoneType' object has no attribute 'group'
=================
2020-10-06 16:22:41,569: [71691] m.c.worker:ERROR: Exception in state 6: AttributeError("'NoneType' object has no attribute 'group'")
Traceback (most recent call last):
File "/home/ehennenfent/manticore/manticore/core/worker.py", line 121, in run
current_state.execute()
File "/home/ehennenfent/manticore/manticore/native/state.py", line 192, in execute
result = self._platform.execute()
File "/home/ehennenfent/manticore/manticore/platforms/linux.py", line 2910, in execute
self.current.execute()
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 1017, in execute
implementation(*insn.operands)
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 1160, in new_method
return old_method(cpu, *args, **kw_args)
File "/home/ehennenfent/manticore/manticore/native/cpu/x86.py", line 5516, in MOVZX
op0.write(Operators.ZEXTEND(op1.read(), op0.size))
File "/home/ehennenfent/manticore/manticore/native/cpu/x86.py", line 778, in read
value = cpu.read_int(self.address(), self.size)
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 733, in read_int
data = self._memory.read(where, size // 8, force)
File "/home/ehennenfent/manticore/manticore/native/memory.py", line 1195, in read
solutions = self._try_get_solutions(address, size, "r", force=force)
File "/home/ehennenfent/manticore/manticore/native/memory.py", line 1338, in _try_get_solutions
solutions = solver.get_all_values(
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 535, in get_all_values
value = self._getvalue(var)
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 384, in _getvalue
return self.__getvalue_bv(expression.name)
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 356, in __getvalue_bv
expr, value = m.group("expr"), m.group("value") # type: ignore
AttributeError: 'NoneType' object has no attribute 'group'
===================
2020-10-06 16:22:46,044: [71691] m.c.worker:ERROR: Exception in state 2: SolverError('((BV #x0000555555556020))')
Traceback (most recent call last):
File "/home/ehennenfent/manticore/manticore/core/worker.py", line 121, in run
current_state.execute()
File "/home/ehennenfent/manticore/manticore/native/state.py", line 192, in execute
result = self._platform.execute()
File "/home/ehennenfent/manticore/manticore/platforms/linux.py", line 2910, in execute
self.current.execute()
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 1017, in execute
implementation(*insn.operands)
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 1160, in new_method
return old_method(cpu, *args, **kw_args)
File "/home/ehennenfent/manticore/manticore/native/cpu/x86.py", line 5516, in MOVZX
op0.write(Operators.ZEXTEND(op1.read(), op0.size))
File "/home/ehennenfent/manticore/manticore/native/cpu/x86.py", line 778, in read
value = cpu.read_int(self.address(), self.size)
File "/home/ehennenfent/manticore/manticore/native/cpu/abstractcpu.py", line 733, in read_int
data = self._memory.read(where, size // 8, force)
File "/home/ehennenfent/manticore/manticore/native/memory.py", line 1195, in read
solutions = self._try_get_solutions(address, size, "r", force=force)
File "/home/ehennenfent/manticore/manticore/native/memory.py", line 1338, in _try_get_solutions
solutions = solver.get_all_values(
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 534, in get_all_values
while self._is_sat():
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 338, in _is_sat
raise SolverError(status)
manticore.exceptions.SolverError: ((BV #x0000555555556020))
2020-10-06 16:22:46,158: [71691] m.c.manticore:INFO: Generated testcase No. 0 - Program finished with exit status: 1
Traceback (most recent call last):
File "solve.py", line 51, in <module>
m.finalize()
File "/home/ehennenfent/manticore/manticore/native/manticore.py", line 345, in finalize
super().finalize()
File "/home/ehennenfent/manticore/manticore/core/manticore.py", line 1174, in finalize
self.generate_testcase(state)
File "/home/ehennenfent/manticore/manticore/native/manticore.py", line 29, in generate_testcase
self._output.save_testcase(state, testcase, message)
File "/home/ehennenfent/manticore/manticore/core/workspace.py", line 608, in save_testcase
self.save_input_symbols(testcase, state)
File "/home/ehennenfent/manticore/manticore/core/workspace.py", line 663, in save_input_symbols
buf = state.solve_one(symbol)
File "/home/ehennenfent/manticore/manticore/core/state.py", line 452, in solve_one
return self.solve_one_n(expr, constrain=constrain)[0]
File "/home/ehennenfent/manticore/manticore/core/state.py", line 470, in solve_one_n
value = self._solver.get_value(self._constraints, expr)
File "/home/ehennenfent/manticore/manticore/core/state.py", line 135, in get_value
solved = self._solver.get_value(constraints, expression, *args, **kwargs)
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 619, in get_value
result.append(self.__getvalue_bv(var[i].name))
File "/home/ehennenfent/manticore/manticore/core/smtlib/solver.py", line 356, in __getvalue_bv
expr, value = m.group("expr"), m.group("value") # type: ignore
AttributeError: 'NoneType' object has no attribute 'group'
The text was updated successfully, but these errors were encountered:
Summary of the problem
Since making the threading model the default form of multiprocessing (#1779), we've been encountering occasional worker crashes when performing long-running tasks due to SMTLib errors.
OS / Environment
Tested on Ubuntu 20.04 using Python 3.8.2
Behavior
The exceptions seem to fall into three broad categories:
m
here is a regex match on the output of the SMT Solver. In other words, it's returning without finding the expected results. This is presumably due to invalid constraints being passed to it."Unknown Constant" means we asked the solver to use a variable without providing a definition for it. This could mean that some of our SMTLib constraints are not getting sent to the solver. Then again, the unknown constant is sometimes simply named
a_
, so it may be that we're just getting the numbering incorrect here.We're getting the internal string "(BV #x0000555555556020)" as a response from
(check-sat)
, which is not correct. Perhaps some sort of communication issue between the various Manticore threads and the solver process.Any relevant logs
The following exceptions killed all 10 workers when running a sample script under Manticore:
The text was updated successfully, but these errors were encountered: