manticore icon indicating copy to clipboard operation
manticore copied to clipboard

Published 20 hours ago • verified publisher icon trailofbits

ERROR: Exception in state 1: ManticoreError('Forking on unfeasible constraint set')

Open mstad opened this issue 4 years ago • 9 comments
trafficstars

Summary of the problem

I try to analyze a simple contract, written in Solidity 0.4.25. During the analysis, an error is shown I launched the manticore command in the virtual environment (python 3.7.11).

Manticore version

Version: 0.3.6

Python version

Python 3.7.11

OS / Environment

No LSB modules are available. Distributor ID: Ubuntu Description: Ubuntu 18.04.4 LTS Release: 18.04 Codename: bionic

Dependencies

capstone==4.0.2 crytic-compile==0.2.0 cytoolz==0.11.0 eth-hash==0.3.1 eth-typing==2.2.2 eth-utils==1.10.0 future==0.18.2 importlib-metadata==4.6.3 intervaltree==3.1.0 -e git+https://github.com/trailofbits/manticore.git@36b3024ff01ffd51c10302d77d8b4690857e0e26#egg=manticore ply==3.11 prettytable==2.1.0 protobuf==3.17.3 pyelftools==0.27 pyevmasm==0.2.3 pysha3==1.0.2 PyYAML==5.4.1 rlp==2.0.1 six==1.16.0 solc-select==0.2.1 sortedcontainers==2.4.0 toolz==0.11.1 typing-extensions==3.10.0.0 unicorn==1.0.2 wasm==1.2 wcwidth==0.2.5 z3-solver==4.8.12.0 zipp==3.5.0

Step to reproduce the behavior

$ git clone https://github.com/trailofbits/manticore.git $ cd manticore

$ virtualenv --python=/usr/bin/python3.7 venv $ source venv/bin/activate

$ pip install solc-select $ solc-select install 0.4.25 ... installed all solc from 0.4.0 to 0.8.4.

$ cd /home/user/.solc-select/arctifacts/ $ cp * /home/user/.local/bin/

Install missing dependencies - for pysha3 $ sudo apt install libpython3.7-dev

Build pysha3 $pip install pysha3

Build manticore from downloaded git $ pip install -e ".[native]" -> 3.6

Install yices2 $ sudo add-apt-repository ppa:sri-csl/formal-methods $ sudo apt-get update $ sudo apt-get install yices2

Following the small smart contract

pragma solidity ^0.4.25;

contract TimedCrowdsale { function isSaleFinished() view public returns (bool) { // TIME_MANIPULATION return block.timestamp >= 1546300800; } }

$ manticore /time_manipulation/timed_crowdsale.sol --core.timeout 1800 --smt.solver yices

Expected behavior

time dependency finding

Actual behavior

Error generation -> no findings in global.findings

Any relevant logs

This are logs shown when the command

manticore /time_manipulation/timed_crowdsale.sol --core.timeout 1800 --smt.solver yices

is performed

2021-08-13 09:40:38,793: [9245] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, <class 'manticore.ethereum.plugins.SkipRevertBasicBlocks'>, <class 'manticore.ethereum.plugins.FilterFunctions'> 2021-08-13 09:40:38,794: [9245] m.main:INFO: Beginning analysis 2021-08-13 09:40:38,796: [9245] m.e.manticore:INFO: Starting symbolic create contract 2021-08-13 09:40:39,154: [9245] m.e.manticore:INFO: Starting symbolic transaction: 0 2021-08-13 09:40:39,531: [9245] m.c.worker:ERROR: Exception in state 1: ManticoreError('Forking on unfeasible constraint set') Traceback (most recent call last): File "/home/mirkostad/Programmi/Tools/manticore/manticore/core/worker.py", line 132, in run current_state.execute() File "/home/mirkostad/Programmi/Tools/manticore/manticore/ethereum/state.py", line 8, in execute return self._platform.execute() File "/home/mirkostad/Programmi/Tools/manticore/manticore/platforms/evm.py", line 3106, in execute self.current_vm.execute() File "/home/mirkostad/Programmi/Tools/manticore/manticore/platforms/evm.py", line 1322, in execute raise Concretize("Symbolic PC", expression=expression, setstate=setstate, policy="ALL") manticore.core.state.Concretize

During handling of the above exception, another exception occurred:

Traceback (most recent call last): File "/home/mirkostad/Programmi/Tools/manticore/manticore/core/worker.py", line 153, in run m._fork(current_state, exc.expression, exc.policy, exc.setstate) File "/home/mirkostad/Programmi/Tools/manticore/manticore/core/manticore.py", line 516, in _fork raise ManticoreError("Forking on unfeasible constraint set") manticore.exceptions.ManticoreError: Forking on unfeasible constraint set

2021-08-13 09:40:39,537: [9245] m.e.manticore:INFO: 0 alive states, 1 terminated states 2021-08-13 09:40:39,662: [9245] m.c.manticore:INFO: Results in /home/mirkostad/Programmi/Tools/manticore/mcore_i_f82fmw 2021-08-13 09:40:39,663: [9245] m.c.manticore:INFO: Total time: 0.5057029724121094

mstad avatar Aug 13 '21 08:08 mstad

I had the same problem, and not just on a few contracts.

step-xiaoyu-ka avatar Aug 23 '21 09:08 step-xiaoyu-ka

@step-xiaoyu-ka @mstad Facing the same issue. The bug exists in the docker image as well.

root@79678e02a3f8:/manticore# manticore examples/evm/umd_example.sol 
2022-01-07 08:52:25,626: [17] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, <class 'manticore.ethereum.plugins.SkipRevertBasicBlocks'>, <class 'manticore.ethereum.plugins.FilterFunctions'>
2022-01-07 08:52:25,626: [17] m.main:INFO: Beginning analysis
2022-01-07 08:52:25,628: [17] m.e.manticore:INFO: Starting symbolic create contract
2022-01-07 08:52:25,994: [17] m.e.manticore:INFO: Starting symbolic transaction: 0
2022-01-07 08:52:26,570: [17] m.c.worker:ERROR: Exception in state 1: ManticoreError('Forking on unfeasible constraint set')
Traceback (most recent call last):
  File "/usr/local/lib/python3.7/dist-packages/manticore/core/worker.py", line 137, in run
    current_state.execute()
  File "/usr/local/lib/python3.7/dist-packages/manticore/ethereum/state.py", line 8, in execute
    return self._platform.execute()
  File "/usr/local/lib/python3.7/dist-packages/manticore/platforms/evm.py", line 3106, in execute
    self.current_vm.execute()
  File "/usr/local/lib/python3.7/dist-packages/manticore/platforms/evm.py", line 1322, in execute
    raise Concretize("Symbolic PC", expression=expression, setstate=setstate, policy="ALL")
manticore.core.state.Concretize

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/usr/local/lib/python3.7/dist-packages/manticore/core/worker.py", line 158, in run
    m._fork(current_state, exc.expression, exc.policy, exc.setstate, exc.values)
  File "/usr/local/lib/python3.7/dist-packages/manticore/core/manticore.py", line 518, in _fork
    raise ManticoreError("Forking on unfeasible constraint set")
manticore.exceptions.ManticoreError: Forking on unfeasible constraint set
 
2022-01-07 08:52:26,576: [17] m.e.manticore:INFO: 0 alive states, 1 terminated states
2022-01-07 08:52:26,675: [17] m.c.manticore:INFO: Results in /manticore/mcore_ijmw898c
2022-01-07 08:52:26,675: [17] m.c.manticore:INFO: Total time: 0.6769917011260986

lahiri-phdworks avatar Jan 07 '22 08:01 lahiri-phdworks

I noticed that the example examples/evm/umd_example.sol runs fine, if the view modifier from function in the smart contract is removed.

lahiri-phdworks avatar Jan 07 '22 09:01 lahiri-phdworks

Same issue for me + unknown solver + 1 hour and a half to get to this point ...

2022-05-13 13:36:57,846: [322] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, <class 'manticore.ethereum.plugins.SkipRevertBasicBlocks'>, <class 'manticore.ethereum.plugins.FilterFunctions'>
2022-05-13 13:36:57,846: [322] m.main:INFO: Beginning analysis
2022-05-13 13:36:57,848: [322] m.e.manticore:INFO: Starting symbolic create contract
2022-05-13 13:37:13,108: [322] m.e.manticore:INFO: Starting symbolic transaction: 0
2022-05-13 15:05:13,136: [322] m.c.worker:ERROR: Exception in state 6: ManticoreError('Forking on unfeasible constraint set')
Traceback (most recent call last):
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/core/worker.py", line 137, in run
    current_state.execute()
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/ethereum/state.py", line 8, in execute
    return self._platform.execute()
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/platforms/evm.py", line 3106, in execute
    self.current_vm.execute()
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/platforms/evm.py", line 1322, in execute
    raise Concretize("Symbolic PC", expression=expression, setstate=setstate, policy="ALL")
manticore.core.state.Concretize

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/core/worker.py", line 158, in run
    m._fork(current_state, exc.expression, exc.policy, exc.setstate, exc.values)
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/core/manticore.py", line 518, in _fork
    raise ManticoreError("Forking on unfeasible constraint set")
manticore.exceptions.ManticoreError: Forking on unfeasible constraint set

2022-05-13 15:08:57,643: [322] m.c.worker:ERROR: Exception in state 0: ManticoreError('Forking on unfeasible constraint set')
Traceback (most recent call last):
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/core/worker.py", line 137, in run
    current_state.execute()
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/ethereum/state.py", line 8, in execute
    return self._platform.execute()
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/platforms/evm.py", line 3106, in execute
    self.current_vm.execute()
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/platforms/evm.py", line 1322, in execute
    raise Concretize("Symbolic PC", expression=expression, setstate=setstate, policy="ALL")
manticore.core.state.Concretize

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/core/worker.py", line 158, in run
    m._fork(current_state, exc.expression, exc.policy, exc.setstate, exc.values)
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/core/manticore.py", line 518, in _fork
    raise ManticoreError("Forking on unfeasible constraint set")
manticore.exceptions.ManticoreError: Forking on unfeasible constraint set

2022-05-13 15:09:03,077: [322] m.c.worker:ERROR: Exception in state 2: SolverUnknown('unsat')
Traceback (most recent call last):
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/core/worker.py", line 137, in run
    current_state.execute()
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/ethereum/state.py", line 8, in execute
    return self._platform.execute()
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/platforms/evm.py", line 3106, in execute
    self.current_vm.execute()
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/platforms/evm.py", line 1322, in execute
    raise Concretize("Symbolic PC", expression=expression, setstate=setstate, policy="ALL")
manticore.core.state.Concretize

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/core/worker.py", line 158, in run
    m._fork(current_state, exc.expression, exc.policy, exc.setstate, exc.values)
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/core/manticore.py", line 515, in _fork
    solutions = state.concretize(expression, policy, explicit_values=values)
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/core/state.py", line 446, in concretize
    vals = self._solver.get_all_values(
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/core/state.py", line 151, in get_all_values
    solved = self._solver.get_all_values(constraints, expression, *args, **kwargs)
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/core/smtlib/solver.py", line 644, in get_all_values
    while self._is_sat():
  File "/home/sandy/.local/lib/python3.8/site-packages/manticore/core/smtlib/solver.py", line 421, in _is_sat
    raise SolverUnknown(status)
manticore.exceptions.SolverUnknown: unsat

sandybradley avatar May 13 '22 13:05 sandybradley

Love how this issue is still open after a year..

htkcodes avatar Jun 30 '22 19:06 htkcodes

still getting the same issue on mac m1.

smuhammathassan avatar Aug 22 '22 13:08 smuhammathassan

Is this actually a bug?

Quiark avatar Aug 27 '22 10:08 Quiark

I wonder if there's anything going on about this issue, has anyone found a fix? It's 2023 and still no workarounds

Akshat-Mishra101 avatar Jan 24 '23 08:01 Akshat-Mishra101

我注意到，如果删除智能合约中函数的修饰符，则该示例examples/evm/umd_example.sol运行良好。view

you're right

sasiyaluba avatar Sep 17 '23 04:09 sasiyaluba