MkdirRmdir example fails with Manticore

[agroce]

This is for the https://github.com/agroce/testfs example.

clang -c *.c
clang++ -o mkdirrmdir MkdirRmdir.cpp *.o -static -Wl,--allow-multiple-definition,--no-export-dynamic -ldeepstate
~/testfs# deepstate-manticore ./mkdirrmdir
INFO:deepstate.mcore:Running 1 tests across 1 workers
2018-12-21 19:49:36,262: [63621] 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 5201, in MOVSX
    op0.write(Operators.SEXTEND(op1.read(), op1.size, 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 1 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 372, in run_test
    do_run_test(state, apis, test, hook_test)
  File "build/bdist.linux-x86_64/egg/deepstate/main_manticore.py", line 367, 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 311, in done_test
    mc.report()
  File "build/bdist.linux-x86_64/egg/deepstate/common.py", line 374, in report
    b = self.concretize_min(symbols[i], constrain=True)
  File "build/bdist.linux-x86_64/egg/deepstate/main_manticore.py", line 113, 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

[ggrieco-tob]

Can you re-test with the latest release? (it will use manticore from master, instead of the the old version)

[agroce]

I get about 8 billion 2019-04-22 20:48:03,461: [42608] m.n.c.abstractcpu:WARNING: Unimplemented instruction: 0x00007fffffdbf650: 0f 16 04 24 movhps xmm0, qword ptr [rsp]

[agroce]

but it hasn't crashed, at least

[agroce]

some compile option that would help here