Crash in the symbolic execution of a contract using extcodesize

[ggrieco-tob]

OS / Environment

Distributor ID: ArchLinux
Description: ArchLinux
Release: rolling-release

Manticore version

Last revision (4cb7e3b)

Python version

Python 3.6.6

Summary of the problem

Manticore crashes when with a contract using extcodesize.

Step to reproduce the behavior

This is a solidity contract to reproduce this issue:

contract C {
    function isContract(address x) constant internal returns(bool) {
      uint size;
      if (x == 0) 
        return false;
      assembly {
        size := extcodesize(x)
      }
      return size > 0;
    }

    function C(address x) {
       isContract(x);
    }
}

Expected behavior

It shouldn't fail.

Actual behavior

$ manticore contract_size.sol -v
2018-12-31 10:48:42,999: [24901] m.c.manticore:INFO: Verbosity set to 2.
2018-12-31 10:48:43,175: [24901] m.main:INFO: Beginning analysis
2018-12-31 10:48:43,176: [24901] m.e.manticore:INFO: Starting symbolic create contract
2018-12-31 10:48:43,373: [24901] m.c.executor:INFO: load state 0
2018-12-31 10:48:43,481: [24901] m.c.executor:INFO: Forking. Policy: ALL. Values: 0x76, 0x6f
2018-12-31 10:48:43,488: [24901] m.c.executor:INFO: Forking current state into states [1, 2]
2018-12-31 10:48:43,491: [24901] m.c.executor:INFO: load state 2
2018-12-31 10:48:43,640: [24901] m.c.executor:INFO: load state 1
2018-12-31 10:48:43,723: [24901] m.c.executor:INFO: Forking. Policy: ALL. Values: 0xc6737b8b2a6a7b5fbb5d75b895f628f2922bae14, 0x5da83cffb5bab1cd888417a5ecefe37b9e250d67, 0xafb6d63079413d167770de9c3f50db6477811bdb
2018-12-31 10:48:43,733: [24901] m.c.executor:INFO: Forking current state into states [4, 5, 6]
2018-12-31 10:48:43,737: [24901] m.c.executor:INFO: load state 5
2018-12-31 10:48:43,796: [24901] m.c.executor:INFO: load state 6
2018-12-31 10:48:43,850: [24901] m.c.executor:INFO: load state 4
Traceback (most recent call last):
  File "/home/g/.local/bin/manticore", line 11, in <module>
    sys.exit(main())
  File "/home/g/.local/lib/python3.6/site-packages/manticore/__main__.py", line 38, in main
    ethereum_main(args, logger)
  File "/home/g/.local/lib/python3.6/site-packages/manticore/ethereum/cli.py", line 65, in ethereum_main
    tx_account=args.txaccount, tx_preconstrain=args.txpreconstrain)
  File "/home/g/.local/lib/python3.6/site-packages/manticore/ethereum/manticore.py", line 950, in multi_tx_analysis
    args=args, working_dir=working_dir)
  File "/home/g/.local/lib/python3.6/site-packages/manticore/ethereum/manticore.py", line 613, in solidity_create_contract
    if not self.count_running_states() or len(self.get_code(contract_account)) == 0:
  File "/home/g/.local/lib/python3.6/site-packages/manticore/ethereum/manticore.py", line 520, in get_code
    return self.get_world(state_id).get_code(address)
  File "/home/g/.local/lib/python3.6/site-packages/manticore/ethereum/manticore.py", line 498, in get_world
    state = self.load(state_id)
  File "/home/g/.local/lib/python3.6/site-packages/manticore/ethereum/manticore.py", line 1074, in load
    raise EthereumError("More than one state running; you must specify a state id.")
manticore.exceptions.EthereumError: More than one state running; you must specify a state id.

[disconnect3d]

The problem occurs only if extcodesize is executed in a constructor.

The code to reproduce the issue can be boiled down to:

contract C {
    constructor(address x) public {
        uint size;
        assembly {
            size := extcodesize(x)
        }
    }
}

If we change constructor to function aa manticore runs as expected.

[disconnect3d]

For the example above we end up having 4 states. Each of them executed the same instructions and ended up with RETURN:

The code I used to debug it:

from manticore.ethereum import ManticoreEVM
from manticore.core.plugin import Tracer

m = ManticoreEVM()
m.verbosity(4)
m.register_plugin(Tracer())
m.multi_tx_analysis('issue1315.sol')
m.finalize()

I am not sure what can we do here. It seems to be a great candidate for path merging as there are no branches or side effects here?