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.67k stars 471 forks source link

m.c.worker:ERROR: Exception object cannot be interpreted as an integer #1575

Open z3roTo0ne opened 4 years ago

z3roTo0ne commented 4 years ago

OS / Environment

I am using docker pull trailofbits/manticore

Manticore version

root@e7ced4975af0:/manticore/hacking_time# manticore --version
Manticore 0.3.2.1

Python version

root@e7ced4975af0:/manticore/hacking_time# python3 --version
Python 3.6.9

Dependencies


root@e7ced4975af0:/manticore/hacking_time# pip freeze
asn1crypto==0.24.0
capstone==4.0.1
cryptography==2.1.4
crytic-compile==0.1.5
cytoolz==0.10.1
dataclasses==0.7
eth-hash==0.2.0
eth-typing==2.2.1
eth-utils==1.8.4
future==0.18.2
idna==2.6
keyring==10.6.0
keyrings.alt==3.0
manticore==0.3.2.1
ply==3.11
prettytable==0.7.2
pycrypto==2.6.1
pyelftools==0.26
pyevmasm==0.2.0
pygobject==3.26.1
pysha3==1.0.2
pyxdg==0.25
PyYAML==5.2
rlp==1.2.0
SecretStorage==2.3.1
six==1.11.0
toolz==0.10.0
unicorn==1.0.2rc1
wasm==1.2
wrapt==1.11.2
z3-solver==4.8.7.0

Summary of the problem

2019-12-16 03:03:41,733: [1188] m.c.worker:ERROR: Exception in state 1: TypeError("'BitVecConstant' object cannot be interpreted as an integer",)

Step to reproduce the behavior

just run manticore test.sol --contract abc

Any relevant logs

image

feliam commented 4 years ago

Hey! @z3roTo0ne hank you for this. we are looking into it. Could you provide the test.sol?

z3roTo0ne commented 4 years ago

Hi, Here is the test.sol: https://gist.github.com/z3roTo0ne/7609d8af0133878f7219471d6f711cf

z3roTo0ne commented 4 years ago

sorry ,here is the test.sol, the previous one has been deleted: https://gist.github.com/z3roTo0ne/a62a9501823ed77ab173e6efc6df07b3

feliam commented 4 years ago

Thanks. I'm failing to reproduce it so far. You can try this if you like..

diff --git a/manticore/ethereum/detectors.py b/manticore/ethereum/detectors.py
index 521525e..05aab42 100644
--- a/manticore/ethereum/detectors.py
+++ b/manticore/ethereum/detectors.py
@@ -678,7 +678,8 @@ class DetectUninitializedMemory(Detector):

     def did_evm_write_memory_callback(self, state, offset, value, size):
         current_contract = state.platform.current_vm.address
-
+        if isinstance(offset, Constant):
+            offset = offset.value
         # concrete or symbolic write
         for offset_i in range(offset, offset + size):
             state.context.setdefault("{:s}.initialized_memory".format(self.name), set()).add(
AsemGhaleb commented 4 years ago

I am facing the same issue. Following is the command I am using and attached is the contract source to reproduce the issue.

manticore --contract HotDollarsToken 1.sol

1.sol.zip