trailofbits / manticore

Symbolic execution tool
https://blog.trailofbits.com/2017/04/27/manticore-symbolic-execution-for-humans/
GNU Affero General Public License v3.0
3.69k stars 472 forks source link

TooManySolutions: Max number of different solutions hit #520

Open ggrieco-tob opened 7 years ago

ggrieco-tob commented 7 years ago

OS / Environment

Distributor ID: ArchLinux Description: ArchLinux Release: rolling-release

Manticore version

Last revision (e84c0513a2d850e3fe63bd23425d7ba67a88c7dc)

Python version

Python 2.7.13

Summary of the problem

Exception unhandled: TooManySolutions: Max number of different solutions hit

Step to reproduce the behavior

$ ./examples/script/count_instructions.py CROMU_00006

using the pre-compiled CGC binary.

Expected behavior

It shouldn't crash.

Actual behavior

2017-10-11 17:27:35,627: [27189] m.c.executor:ERROR: Exception: Max number of different solutions hit
Traceback (most recent call last):
  File "/home/g/.local/lib/python2.7/site-packages/manticore-0.1.4-py2.7.egg/manticore/core/executor.py", line 457, in run
    if not current_state.execute():
  File "/home/g/.local/lib/python2.7/site-packages/manticore-0.1.4-py2.7.egg/manticore/core/state.py", line 123, in execute
    result = self._platform.execute()
  File "/home/g/.local/lib/python2.7/site-packages/manticore-0.1.4-py2.7.egg/manticore/platforms/decree.py", line 870, in execute
    self.current.execute()
  File "/home/g/.local/lib/python2.7/site-packages/manticore-0.1.4-py2.7.egg/manticore/core/cpu/abstractcpu.py", line 759, in execute
    implementation(*insn.operands)
  File "/home/g/.local/lib/python2.7/site-packages/manticore-0.1.4-py2.7.egg/manticore/core/cpu/abstractcpu.py", line 830, in new_method
    return old_method(cpu, *args, **kw_args)
  File "/home/g/.local/lib/python2.7/site-packages/manticore-0.1.4-py2.7.egg/manticore/core/cpu/x86.py", line 2522, in MOV
    dest.write(src.read())
  File "/home/g/.local/lib/python2.7/site-packages/manticore-0.1.4-py2.7.egg/manticore/core/cpu/x86.py", line 666, in write
    cpu.write_int(self.address(), value, self.size)
  File "/home/g/.local/lib/python2.7/site-packages/manticore-0.1.4-py2.7.egg/manticore/core/cpu/abstractcpu.py", line 506, in write_int
    self.memory[where:where+size/8] = [Operators.CHR(Operators.EXTRACT(expression, offset, 8)) for offset in xrange(0, size, 8)]
  File "/home/g/.local/lib/python2.7/site-packages/manticore-0.1.4-py2.7.egg/manticore/core/memory.py", line 852, in __setitem__
    self.write(index.start, value)
  File "/home/g/.local/lib/python2.7/site-packages/manticore-0.1.4-py2.7.egg/manticore/core/memory.py", line 1013, in write
    solutions = solver.get_all_values(self.constraints, address, maxcnt=0x1000) #if more than 0x3000 exception
  File "/home/g/.local/lib/python2.7/site-packages/manticore-0.1.4-py2.7.egg/manticore/core/smtlib/solver.py", line 374, in get_all_values
    raise TooManySolutions(result)
TooManySolutions: Max number of different solutions hit

Executed  112  instructions.
offlinemark commented 6 years ago

re: #1097

fpse mem can be used here