trailofbits / deepstate

A unit test-like interface for fuzzing and symbolic execution
Apache License 2.0
815 stars 99 forks source link

manticore failure on testfs example #73

Closed agroce closed 4 years ago

agroce commented 6 years ago

Build https://github.com/agroce/testfs and run

> deepstate-manticore ./Tests 
INFO:deepstate.mcore:Running 1 tests across 1 workers
INFO:deepstate:Running TestFs_FilesDirs from /root/testfs/Tests.cpp(84)
INFO:deepstate:/root/testfs/RamInterface.cpp(149): Making super block
INFO:deepstate:/root/testfs/RamInterface.cpp(152): Making inode free map
INFO:deepstate:/root/testfs/RamInterface.cpp(155): Making block free map
INFO:deepstate:/root/testfs/RamInterface.cpp(158): Making checksum table
INFO:deepstate:/root/testfs/RamInterface.cpp(161): Making inode blocks
INFO:deepstate:/root/testfs/RamInterface.cpp(165): Done creating empty file system.
INFO:deepstate:/root/testfs/RamInterface.cpp(174): Created root directory; File system initialized
INFO:deepstate:nr of allocated inodes = 1

INFO:deepstate:nr of allocated blocks = 1

INFO:deepstate:PATH 0: foo

INFO:deepstate:NAME: foo

INFO:deepstate:nr of allocated inodes = 2

INFO:deepstate:nr of allocated blocks = 2

INFO:deepstate:PATH 0: foo

INFO:deepstate:PATH 1: foo

INFO:deepstate:NAME: foo

INFO:deepstate:nr of allocated inodes = 2

INFO:deepstate:nr of allocated blocks = 2

INFO:deepstate:Input: 00 00 00 06
2018-07-18 04:25:38,593: [18760] m.c.executor:ERROR: Exception: 
Traceback (most recent call last):
  File "/root/.local/lib/python2.7/site-packages/manticore-0.1.10-py2.7.egg/manticore/core/executor.py", line 461, in run
    if not current_state.execute():
  File "/root/.local/lib/python2.7/site-packages/manticore-0.1.10-py2.7.egg/manticore/core/state.py", line 127, in execute
    result = self._platform.execute()
  File "/root/.local/lib/python2.7/site-packages/manticore-0.1.10-py2.7.egg/manticore/platforms/linux.py", line 2216, in execute
    self.current.execute()
  File "/root/.local/lib/python2.7/site-packages/manticore-0.1.10-py2.7.egg/manticore/core/cpu/abstractcpu.py", line 839, in execute
    implementation(*insn.operands)
  File "/root/.local/lib/python2.7/site-packages/manticore-0.1.10-py2.7.egg/manticore/core/cpu/abstractcpu.py", line 937, in new_method
    return old_method(cpu, *args, **kw_args)
  File "/root/.local/lib/python2.7/site-packages/manticore-0.1.10-py2.7.egg/manticore/core/cpu/x86.py", line 5185, in MOVZX
    op0.write(Operators.ZEXTEND(op1.read(), op0.size))
  File "/root/.local/lib/python2.7/site-packages/manticore-0.1.10-py2.7.egg/manticore/core/cpu/x86.py", line 662, in read
    value = cpu.read_int(self.address(), self.size)
  File "/root/.local/lib/python2.7/site-packages/manticore-0.1.10-py2.7.egg/manticore/core/cpu/abstractcpu.py", line 606, in read_int
    data = self._memory.read(where, size / 8, force)
  File "/root/.local/lib/python2.7/site-packages/manticore-0.1.10-py2.7.egg/manticore/core/memory.py", line 931, in read
    assert solver.check(self.constraints)
AssertionError

ERROR:deepstate.mcore:State 6 terminated due to internal error: 
ERROR:deepstate.mcore:Uncaught exception: <class 'manticore.core.smtlib.solver.SolverException'>
Traceback (most recent call last):
  File "build/bdist.linux-x86_64/egg/deepstate/main_manticore.py", line 348, in run_test
    do_run_test(state, apis, test, hook_test)
  File "build/bdist.linux-x86_64/egg/deepstate/main_manticore.py", line 343, in do_run_test
    m.run()
  File "/root/.local/lib/python2.7/site-packages/manticore-0.1.10-py2.7.egg/manticore/manticore.py", line 638, in run
    self._start_workers(procs, profiling=should_profile)
  File "/root/.local/lib/python2.7/site-packages/manticore-0.1.10-py2.7.egg/manticore/manticore.py", line 419, in _start_workers
    target()
  File "/root/.local/lib/python2.7/site-packages/manticore-0.1.10-py2.7.egg/manticore/core/executor.py", line 503, in run
    self._publish('will_terminate_state', current_state, current_state_id, e)
  File "/root/.local/lib/python2.7/site-packages/manticore-0.1.10-py2.7.egg/manticore/utils/event.py", line 118, in _publish
    self._publish_impl(_name, *args, **kwargs)
  File "/root/.local/lib/python2.7/site-packages/manticore-0.1.10-py2.7.egg/manticore/utils/event.py", line 134, in _publish_impl
    sink._publish_impl(_name, *args, **kwargs)
  File "/root/.local/lib/python2.7/site-packages/manticore-0.1.10-py2.7.egg/manticore/utils/event.py", line 126, in _publish_impl
    callback(robj(), *args, **kwargs)
  File "build/bdist.linux-x86_64/egg/deepstate/main_manticore.py", line 291, in done_test
    mc.report()
  File "build/bdist.linux-x86_64/egg/deepstate/common.py", line 370, in report
    b = self.concretize_min(symbols[i], constrain=True)
  File "build/bdist.linux-x86_64/egg/deepstate/main_manticore.py", line 109, in concretize_min
    concrete_val = min(self.state.concretize(val, policy='MINMAX'))
  File "/root/.local/lib/python2.7/site-packages/manticore-0.1.10-py2.7.egg/manticore/core/state.py", line 277, in concretize
    vals = self._solver.minmax(self._constraints, symbolic)
  File "/root/.local/lib/python2.7/site-packages/manticore-0.1.10-py2.7.egg/manticore/core/smtlib/solver.py", line 107, in minmax
    m = self.min(constraints, x, iters)
  File "/root/.local/lib/python2.7/site-packages/manticore-0.1.10-py2.7.egg/manticore/core/smtlib/solver.py", line 102, in min
    return self.optimize(constraints, X, 'minimize')
  File "/root/.local/lib/python2.7/site-packages/manticore-0.1.10-py2.7.egg/manticore/core/smtlib/solver.py", line 444, in optimize
    raise SolverException("Optimizing error, unsat or unknown core")
SolverException: Optimizing error, unsat or unknown core
agroce commented 4 years ago

I think this is no longer relevant