Optimize memory representation and operations

[elopez]

Description

An Echidna user reported continuously increasing memory while running mstore/mcopy operations. This PR attempts to resolve that by

• avoiding freezing the full memory on mcopy
• avoiding multiple, repeated small memory expansions, as each expansion has to copy the whole memory contents
  • this is disabled by default, to maintain the concrete memory small (as it might be symbolized at some later point), but a config value on the VM is available by anyone doing pure concrete execution (e.g. Echidna). Limited empirical testing showed 64k is a good value to use.

Checklist

• tested locally
• added automated tests
• updated the docs
• updated the changelog

[msooseth]

Thanks! I am looking at it. Only changing the concrete one is definitely OK. I'm trying to see what's the deal with the Symbolic. Feels like it'd be nice to unify the two, like you did.

[msooseth]

OK, I had a look. Either way

assign (#state % #memory) (SymbolicMemory $ copySlice srcOff dstOff sz mem mem)

Will get executed. But with your system, we first execute buf <- readMemory srcOff sz, which means:

copySlice offset' (Lit 0) size' mem mempty

which is basically another copyslice. So I'd rather keep the concrete and the symbolic separate.

Otherwise, it looks cool!

[msooseth]

Hey! If you could remove that tunable then I think we could just merge :) Would be nice!

[msooseth]

Thanks, this is great! Can you please add a CHANGELOG element? Then I think we can merge :)

[msooseth]

Thanks! I squash-merged, so it's a single commit. I hope that's OK!