search

ethereum / hevm

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

Use let expression in copySlice to decrease expression size #489

Closed samalws-tob closed 3 months ago

samalws-tob commented 4 months ago

Description

This PR changes copySlice so that it returns an expression of the form (let ((src [value of src])) (store (store [value of dst] 0 (select src 0)) 1 (select src 1)), rather than (store (store [value of dst] 0 (select [value of src] 0)) 1 (select [value of src] 1)). This reduces the number of times src has to be written out in the SMT expression from size times to only 1 time. This can drastically reduce the size of the resulting SMT expression, especially in the case of nested CopySlices. Fixes #487 .

Checklist

ggrieco-tob commented 3 months ago

I'm wondering what is the status of this PR?

samalws-tob commented 3 months ago

@ggrieco-tob PR is ready but waiting for review from @d-xo or @msooseth

d-xo commented 3 months ago

In general a positive review from @zoep or @arcz is imo enough to merge.

d-xo commented 3 months ago

I am a little confused why the common sub expression elimination pass isn't handling this during smt generation?

zoep commented 3 months ago

I am a little confused why the common sub expression elimination pass isn't handling this during smt generation?

The copySlice expansion happens post-CSE, which happens at the Expr level, so this repeating subterm will not be eliminated.

Regarding SMT encoding, is there any difference between local let and a top-level constant declaration (e.g., in terms of performance)?