Error TODO: implement copySlice with a symbolically sized region reached by Echidna

[rappie]

For more info, see this issue in the Echidna repository: crytic/echidna#1247

[d-xo]

This is a known limitation. The core issue is that smt-lib does not provide primitives for copying slices between arrays. At the moment we unroll concretely sized copySlice's into a sequence of byte read/writes.

In order to handle symbolic slices, we would need to implement one of the strategies from this paper: https://link.springer.com/chapter/10.1007/978-3-642-54108-7_6. This is not a small change, but I think relatively achievable (we should have most of the required machinery to implement their rewriting approach).

[msooseth]

This is being worked on by the developers of Bitwuzla, so currently, I'd like to not work on this on our end, to reduce duplication of work. Hopefully, in a few months this will be fixed :) Yay!

[ggrieco-tob]

Is #591 related to this issue?

[msooseth]

#591 is related indeed, thanks! But it doesn't actually solve it :( Instead, it makes sure that when an error is encountered, we don't abandon the whole operation, only the ones we cannot deal with :)

[ggrieco-tob]

Great, this is good step forward, since currently the symbolic worker will crash and that's not good 😄

[msooseth]

@ggrieco-tob Exactly! It actually should work now. Let me know what your experience is with it. If you wanna review, that'd also be nice :)