Closed samalws-tob closed 3 months ago
This also might be doable using let expressions. Example:
copySliceNew :: Expr EWord -> Expr EWord -> Expr EWord -> Builder -> Builder -> Builder
copySliceNew srcOffset dstOffset size src dst = "(let ((src " <> src <> ")) " <> copySliceOld srcOffset dstOffset size "src" dst <> ")"
copySliceOld :: Expr EWord -> Expr EWord -> Expr EWord -> Builder -> Builder -> Builder
copySliceOld = [current implementation]
copySlice
, defined here, copies itssrc
argumentsize
times into the resulting SMT string. It can get even worse with nestedCopySlice
s, where we end up getting exponential size. In particular, whenexprToSMT
is called on this expression......
exprToSMT
returns a 35-million-character-long value.Ideally the
prelude
passed to the SMT solver would include a recursivecopySlice
function which handles the functionality that's now done in haskell, but I'm not sure how this would affect SMT performance. This would be ideal becausesrc
would only need to be typed out once in the SMT expression.I can go into more detail, if needed, on how this expression came up in practice. Long story short, this expression was involved while testing a symbolic execution PR for echidna on the following contract: