Closed mrx23dot closed 2 years ago
Oyente was designed before the fork Byzantium
(block 7,280,000 on the main chain, 28 Feb 2019) that introduced the instruction SHL
, and apparently has never been upgraded by the semantics of newer instructions. Oyente does not handle the operations SHR
, SAR
, EXTCODEHASH
, CHAINID
, SELFBALANCE
, BASEFEE
and CREATE2
(same or later fork). Oyente even uses the opcode for CREATE2
internally for a different purpose.
Not being able to handle SHL
is particularly painful, as this instruction appears, since quite some time, near the beginning of every bytecode generated by the Solidity compiler, to dissect the call data to obtain the four byte signature of the called method.
Thanks for the detailed answer!
Running latest Oyente on contract: https://etherscan.io/address/0xe681f80966a8b1ffadecf8068bd6f99034791c95#code extracted binary via etherscan API: 0xe681f80966a8b1ffadecf8068bd6f99034791c95.txt
Many other contracts pass this way.
cmd
docker start oyente_cont && docker exec -i oyente_cont python /oyente/oyente/oyente.py --compilation-error --depthlimit 4 --looplimit 100 -s 0xe681f80966a8b1ffadecf8068bd6f99034791c95.txt -b
fails with
Was compiled with v0.7.6+commit.7338295f according to etherscan