A Symbolic Ethereum Virtual Machine (EVM) bytecode interpreter, parser and decompiler, along with several other utils for programmatically extracting information from EVM bytecode.
Instead of always follow jump destinations (and loop unrolling) determine when to stop symbolic execution. The main issue is when jump destinations are in different basic blocks. That is, when a jump destination is pushed in one basic block, but it's jumped to in a different one.
The main problem that arises when deduplicating basic blocks is the introduction of phi-nodes or equivalent. The introduction of Local expressions represent SSA nodes. For a quick intro to SSA see https://www.cs.cornell.edu/courses/cs6120/2022sp/lesson/6/. When introducing phi-nodes it might require to re-execute already executed states.
Instead of always follow jump destinations (and loop unrolling) determine when to stop symbolic execution. The main issue is when
jumpdestinations are in different basic blocks. That is, when ajumpdestination ispushed in one basic block, but it'sjumped to in a different one.Some papers that might solve this issue
The main problem that arises when deduplicating basic blocks is the introduction of
phi-nodes or equivalent. The introduction ofLocalexpressions represent SSA nodes. For a quick intro to SSA see https://www.cs.cornell.edu/courses/cs6120/2022sp/lesson/6/. When introducingphi-nodes it might require to re-execute already executed states.As an alternative one can use Basic Block Arguments https://2pi.dk/2022/05/bb-arguments, but I'm not sure how to convert from a stack based execution to BB arguments. Discussion about
phi-nodes vs BB arguments might be helpful https://news.ycombinator.com/item?id=22432344 and https://mlir.llvm.org/docs/Rationale/Rationale/#block-arguments-vs-phi-nodes.For reference, how a similar library handles
jumpiandjumpinstructionsjumpihttps://github.com/a16z/halmos/blob/main/src/halmos/sevm.py#L1878jumphttps://github.com/a16z/halmos/blob/main/src/halmos/sevm.py#L1949