Closed anhdungle93 closed 4 years ago
Your example exhibits the above error on OSX using Python3.8, but works just fine with Python3.7. Looking at the traceback, it seems as though Python3.8 uses the fork
syscall for pickling, which doesn't work very well on OSX. Our MacOS branch uses threads in order to avoid this, but that doesn't seem to have carried over to the pickler. I'll need to do some more digging to see whether this is something we can fix or if we need to wait for upstream changes to multiprocessing
.
Edit: Clarified that threads are independent from multiprocessing
@ehennenfent Thanks a lot, I switched to Python 3.7.6, but got a different error
manticore SafeMath.sol
2020-05-27 09:17:31,174: [902] m.c.manticore:WARNING: Manticore is only supported on Linux. Proceed at your own risk!
2020-05-27 09:17:31,832: [902] m.main:INFO: Registered plugins: DetectIntegerOverflow, DetectSuicidal, <class 'manticore.ethereum.plugins.KeepOnlyIfStorageChanges'>, DetectDelegatecall, DetectUninitializedStorage, DetectExternalCallAndLeak, DetectUninitializedMemory, DetectInvalid, DetectEnvInstruction, DetectReentrancySimple, DetectManipulableBalance, DetectReentrancyAdvanced, DetectUnusedRetVal
2020-05-27 09:17:31,832: [902] m.main:INFO: Beginning analysis
2020-05-27 09:17:31,835: [902] m.e.manticore:INFO: Starting symbolic create contract
2020-05-27 09:17:35,065: [902] m.e.manticore:INFO: Starting symbolic transaction: 0
2020-05-27 09:24:12,065: [902] m.e.manticore:INFO: 0 alive states, 15 terminated states
2020-05-27 09:24:12,290: [902] m.e.manticore:INFO: Starting symbolic transaction: 1
2020-05-27 09:24:12,396: [1113] m.c.manticore:INFO: Generated testcase No. 0 - RETURN(1 txs)
2020-05-27 09:24:12,400: [1115] m.c.manticore:INFO: Generated testcase No. 2 - REVERT(2 txs)
2020-05-27 09:24:12,407: [1119] m.c.manticore:INFO: Generated testcase No. 3 - REVERT(2 txs)
2020-05-27 09:24:12,407: [1120] m.c.manticore:INFO: Generated testcase No. 4 - REVERT(2 txs)
2020-05-27 09:24:12,408: [1114] m.c.manticore:INFO: Generated testcase No. 1 - REVERT(2 txs)
2020-05-27 09:24:12,410: [1122] m.c.manticore:INFO: Generated testcase No. 5 - REVERT(2 txs)
2020-05-27 09:24:12,418: [1121] m.c.manticore:INFO: Generated testcase No. 6 - RETURN(2 txs)
2020-05-27 09:24:12,450: [1118] m.c.manticore:INFO: Generated testcase No. 7 - REVERT(2 txs)
2020-05-27 09:24:12,454: [1117] m.c.manticore:INFO: Generated testcase No. 8 - RETURN(2 txs)
2020-05-27 09:24:12,503: [1116] m.c.manticore:INFO: Generated testcase No. 9 - REVERT(2 txs)
2020-05-27 09:24:13,600: [1113] m.c.manticore:INFO: Generated testcase No. 10 - REVERT(2 txs)
2020-05-27 09:24:13,893: [1116] m.c.manticore:INFO: Generated testcase No. 11 - RETURN(2 txs)
2020-05-27 09:24:13,899: [1122] m.c.manticore:INFO: Generated testcase No. 12 - RETURN(2 txs)
2020-05-27 09:24:24,000: [1115] m.c.manticore:INFO: Generated testcase No. 13 - RETURN(2 txs)
2020-05-27 09:24:37,905: [1114] m.c.manticore:INFO: Generated testcase No. 14 - REVERT(2 txs)
Process Process-2:
Traceback (most recent call last):
File "/Users/anhdungle/opt/anaconda3/lib/python3.7/multiprocessing/process.py", line 297, in _bootstrap
self.run()
File "/Users/anhdungle/opt/anaconda3/lib/python3.7/multiprocessing/process.py", line 99, in run
self._target(*self._args, **self._kwargs)
File "/Users/anhdungle/opt/anaconda3/lib/python3.7/site-packages/manticore/ethereum/manticore.py", line 1633, in worker_finalize
finalizer(q.get_nowait())
File "/Users/anhdungle/opt/anaconda3/lib/python3.7/site-packages/manticore/ethereum/manticore.py", line 1628, in finalizer
self.generate_testcase(st, message=message)
File "/Users/anhdungle/opt/anaconda3/lib/python3.7/site-packages/manticore/ethereum/manticore.py", line 1515, in generate_testcase
is_something_symbolic = state.platform.dump(stream, state, self, message)
File "/Users/anhdungle/opt/anaconda3/lib/python3.7/site-packages/manticore/platforms/evm.py", line 3075, in dump
balance = state.solve_one(balance)
File "/Users/anhdungle/opt/anaconda3/lib/python3.7/site-packages/manticore/core/state.py", line 340, in solve_one
return self.solve_one_n(expr, constrain=constrain)[0]
File "/Users/anhdungle/opt/anaconda3/lib/python3.7/site-packages/manticore/core/state.py", line 358, in solve_one_n
value = self._solver.get_value(self._constraints, expr)
File "/Users/anhdungle/opt/anaconda3/lib/python3.7/site-packages/manticore/core/smtlib/solver.py", line 632, in get_value
raise SolverError("Model is not available")
manticore.exceptions.SolverError: Model is not available
2020-05-27 09:31:54,351: [902] m.c.manticore:INFO: Results in /Users/anhdungle/learning/smart_contracts_test/manticore_tests/mcore_bp5jbhp2
I switched to python 3.6 and everything seems fine now.
Sorry, didn't see your last reply come in! For future reference, the "Model not available" error means that Z3 was unable to solve for a value that Manticore asked it for. That could be because some of the constraints placed on it were contradictory, or potentially due to available disk space or memory limitations. If you come across a piece of code you're able to share that works properly on Python 3.6 but fails on later versions, please do share it. Discrepancies between major versions of Python are always something we're concerned about. Thanks for filing!
I was getting this error, switched to python 3.6.1 through a conda environment and now I'm getting AttributeError: 'NoneType' object has no attribute 'result'
. Any ideas how to solve this?
Full error:
Traceback (most recent call last):
File "/Users/cdgmachado/anaconda3/envs/myenv/lib/python3.6/multiprocessing/process.py", line 258, in _bootstrap
self.run()
File "/Users/cdgmachado/anaconda3/envs/myenv/lib/python3.6/multiprocessing/process.py", line 93, in run
self._target(*self._args, **self._kwargs)
File "/Users/cdgmachado/anaconda3/envs/myenv/lib/python3.6/site-packages/manticore/ethereum/manticore.py", line 1756, in worker_finalize
finalizer(q.get_nowait())
File "/Users/cdgmachado/anaconda3/envs/myenv/lib/python3.6/site-packages/manticore/ethereum/manticore.py", line 1747, in finalizer
if only_alive_states and last_tx.result in {"REVERT", "THROW", "TXERROR"}:
AttributeError: 'NoneType' object has no attribute 'result'
This is how I'm calling manticore, with remaps included:
manticore contracts/ethereum/ProxyFactory.sol --solc-remaps "@openzeppelin=node_modules/@openzeppelin @uniswap=node_modules/@uniswap @chainlink=node_modules/@chainlink @rari-capital=node_modules/@rari-capital hardhat=node_modules/hardhat" --contract ProxyFactory.sol
Summary of the problem
I tried to use manticore (installed in a conda environment) on the following contract
with two manticore versions, one directly from pip and one from git master branch. The one from pip has the error:
and the one from git master
Manticore version
both are of version 0.3.3
Python version
the python version of the environment for the version from pip: 3.8.2 the python version of the environment for the version from git master: 3.8.3
OS / Environment
MacOS Catalina