STATICCALLS with symbolic arguments mess up the stack

[ToonVanHove]

Description

A STATICCALL with symbolic arguments is not supported, however it also doesn't place an item on the stack to describe the result of the call. This means that there is 1 less item on the stack compared to what the EVM program expects, this leads to stack management issues and stack underflows.

The code responsible is at mythril/laser/ethereum/call.py:222

    except TypeError:
        log.debug("CALL with symbolic start or offset not supported")
        return [global_state]

How to Reproduce

Running this bytecode in Mythril leads to a STATICCALL with symbolic arguments and eventually a stack underflow.

0x600436101561000d576100ff565b60046000601c37600051346101055763029b2f348118610030573360e05261004a565b63cb49506481186100fd5760a4358060a01c6101055760e0525b60006101405261012060006001818352015b6020610120510261014001516101005260046101a0527fc2985578000000000000000000000000000000000000000000000000000000006101c0526101a05060206102006101a0516101c0600060e0515af16100bd573d600060003e3d6000fd5b6101e060203d8082116100d057816100d2565b805b905090508152602081510180610160828460045afa905050508151600101808352811861005c575050005b505b60006000fd5b600080fd

Possible solutions

• Produce a new symbol and put it on the stack as a result value.

    except TypeError:
        log.debug("CALL with symbolic start or offset not supported")
        insert_ret_val(global_state)
        return [global_state]

• Or, stop symbolic execution after encountering an unsupported symbolic call.