ethereum / hevm

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

Fuzzer bug in `readWord-equivalence` #502

Closed d-xo closed 1 month ago

d-xo commented 1 month ago

Found this in a ci run:

2024-07-12T15:31:51.7398020Z hevm> Sat (SMTCex {vars = fromList [(TxValue,0x0)], addrs = fromList [], buffers = fromList [], store = fromList [], blockContext = fromList [], txContext = fromList []})
2024-07-12T15:31:51.7408340Z hevm> FAIL (0.21s)
2024-07-12T15:31:51.7408670Z hevm>       *** Failed! Falsified (after 17 tests):
2024-07-12T15:31:51.7410170Z hevm>       (CopySlice (Lit 0x21) (Lit 0x5d) (Lit 0x3f) (CopySlice (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) (Lit 0x36) (Lit 0x35) (ConcreteBuf "t\200&") (ConcreteBuf "\232\f\RS\149=;")) (CopySlice BlockNumber (Lit 0x1d) (Lit 0x1) (ConcreteBuf "\154\251\223\213\255\199\194j\253\160\176\&6\221\227\&9:\200\143\138\129\224:\221") (ConcreteBuf "")),Lit 0x5e)
2024-07-12T15:31:51.7411810Z hevm>       Use --quickcheck-replay=371577 to reproduce.
2024-07-12T15:31:51.7412270Z hevm>       Use -p '/readWord-equivalance/' to rerun this test only.
msooseth commented 1 month ago

This is not really a bug... it's again the (CopySlice (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) which is already tracked here: https://github.com/ethereum/hevm/issues/401

I am closing this, and because of the link above, this issue will show up in https://github.com/ethereum/hevm/issues/401 so we can always come back here for info once we decide a way to fix that.