Closed zoep closed 6 months ago
I have now fixed this PR I think, but the more general system that I now created needs a review. Furthermore, I am not sure which order should the dop
/take
be, that needs to be checked.
Thanks for the review @arcz ! Let me know if you think it's OK now :)
Description
Changes:
CopySlice
so that the output of hevm is closer to the Expr output of Act. Expressions of the formCopySlice 0 0 size src (ConcreteBuf "")
are rewritten tosrc
whensize
is equal to the size of thesrc
buffer`.CopySlice
simplification necessitated improvement of both decomposition andreadStorage
improvements--nodecompose
decompose
can safely skip writes to anidx
it's not currently reading. This is because indecompose
we have a very good idea of e.g. no mixing of map/array/other and we know exactly what idx is being read. So we have the safeguards necessary to do this.decompose
is now only safe to execute in case everything safely decomposes. This is actually a requirement forAbstractStore k
, as separate queries will deal with the sameAbstractStore k
. Aalthough we could be more lenient and have it decompose for everyAbstractStore k1
and not forAbstractStore k2
and still be OK to decomposeAbstractStore k1
and notAbstractStore k2
. However, the strict one works for now.PEq
of the whole storage -- not with the current setup. We'd need a more sophisticated decompose for that. That kind of check only occurs during equivalence checking. We now check for this and don't perform decomposition on such queries (rare).Checklist