Concurrency issues when running in multithreaded mode

Open ehennenfent opened this issue 5 years ago • 0 comments

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:

  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.

manticore.exceptions.SolverError: (error "line 7043 column 42: unknown constant a_518854")

"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.

manticore.exceptions.SolverError: ((BV #x0000555555556020))

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'

Oct 06 '20 16:10 ehennenfent