search

ethereum / hevm

symbolic EVM evaluator
https://hevm.dev
GNU Affero General Public License v3.0
223 stars 45 forks source link

Error `TODO: implement copySlice with a symbolically sized region` reached by Echidna #492

Open rappie opened 3 months ago

rappie commented 3 months ago

For more info, see this issue in the Echidna repository: https://github.com/crytic/echidna/issues/1247

d-xo commented 2 months ago

This is a known limitation. The core issue is that smt-lib does not provide primitives for copying slices between arrays. At the moment we unroll concretely sized copySlice's into a sequence of byte read/writes.

In order to handle symbolic slices, we would need to implement one of the strategies from this paper: https://link.springer.com/chapter/10.1007/978-3-642-54108-7_6. This is not a small change, but I think relatively achievable (we should have most of the required machinery to implement their rewriting approach).