copySlice can return giant SMT queries from reasonable-sided expressions

[samalws-tob]

copySlice, defined here, copies its src argument size times into the resulting SMT string. It can get even worse with nested CopySlices, where we end up getting exponential size. In particular, when exprToSMT is called on this expression...

(CopySlice (Lit 0x0) (Lit 0x0) (Lit 0x40) (WriteWord (Lit 0x0) (SLoad (Keccak (CopySlice (Lit 0x0) (Lit 0x0) (Lit 0x40) (WriteWord (Lit 0x0) (SLoad (Keccak (CopySlice (Lit 0x0) (Lit 0x0) (Lit 0x40) (WriteWord (Lit 0x0) (Var "arg1") (ConcreteBuf "\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\SOH")) (ConcreteBuf ""))) (ConcreteStore (fromList []))) (ConcreteBuf "\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\SOH")) (ConcreteBuf ""))) (ConcreteStore (fromList []))) (ConcreteBuf "\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL")) (ConcreteBuf ""))

...exprToSMT returns a 35-million-character-long value.

Ideally the prelude passed to the SMT solver would include a recursive copySlice 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 because src 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:

pragma solidity 0.8.13;
contract Challenge {
    mapping(uint256 => uint256[]) private _mapA;
    mapping(uint256 => uint256) private _mapB;
    function challenge(uint256 a) external {
        uint256 val;
        unchecked {
            val = _mapA[_mapB[_mapB[a]]][0];
        }   
        require(val == 0); 
    }   
}

[samalws-tob]

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]