search

runtimeverification / evm-semantics

K Semantics of the Ethereum Virtual Machine (EVM)
BSD 3-Clause "New" or "Revised" License
509 stars 144 forks source link

Constructor calls with symbolic parameters #2219

Closed RaoulSchaffranek closed 5 months ago

RaoulSchaffranek commented 11 months ago

KEVM currently doesn't handle constructor calls with symbolic parameters. The problem is that the parameters are appended to the init code, and #computeValidJumpDests will start branching on them to collect all JUMPDEST locations. The branching leads to a path-explosion problem and eventually produces the following error message: Error internalising cterm: [PredicateExpected ....

Notice that the parameters are just data and not executable bytecode. The init code will utilize a CODECOPY operation to copy the data from the init code to the memory. Hence, looking for JUMPDESTS in this data is not needed.

We solved this issue by replacing the ahead-of-time computation of the valid jump destinations with a just-in-time algorithm. See: https://github.com/runtimeverification/evm-semantics/pull/2112

We also needed the following lemma to lookup opcodes in partially symbolic init code:

    rule [bytes-concat-left-lookup]:
        (A:Bytes +Bytes B:Bytes) [I] => A [I] requires 0 <=Int I andBool I <Int lengthBytes(A) [simplification]
ehildenb commented 11 months ago

The lemma can be added to KEVM as well as a test of it, in its own PR now, so that we can avoid that problem in the future.

palinatolmach commented 5 months ago

Closed as completed by https://github.com/runtimeverification/kontrol/pull/596.