Optimize memory representation and operations #707
Conversation
| buf <- freezeMemory mem | ||
| copyBytesToMemory buf sz srcOff dstOff | ||
| SymbolicMemory mem -> do | ||
| assign (#state % #memory) (SymbolicMemory $ copySlice srcOff dstOff sz mem mem) |
There was a problem hiding this comment.
I think this previous code results in a bit simpler representation for the symbolic case, so we might want to keep it and only modify the concrete case
|
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. |
|
OK, I had a look. Either way Will get executed. But with your system, we first execute which is basically another copyslice. So I'd rather keep the concrete and the symbolic separate. Otherwise, it looks cool! |
This might be desirable to keep Concrete turned Symbolic memories small
elopez
changed the title
| -- We want to always grow at least a chunk, to avoid the performance impact | ||
| -- that would happen with repeated small expansion operations, as grow does | ||
| -- a larger *copy* of the vector on a new place | ||
| memory' <- VUnboxed.Mutable.grow memory $ max toAlloc vm.config.minMemoryChunk |
There was a problem hiding this comment.
maybe this should be a growth factor rather than a fixed min amount
There was a problem hiding this comment.
Nice find! So I had lots of issues in C++ where I was growing by a fixed chunk... (side-note: never use resize, use insert if it will grow later) not sure how relevant that is here, but it was a painful experience :D My suggestion would be to grow some factor, usually 2x is a good rule of thumb, but 1.5x can also work. But perhaps also make sure we grow at least some value (so we don't allocate by small chunks at the beginning). I'd rather avoid repeated allocations. What do you think?
| @@ -44,6 +44,7 @@ vmForEthrunCreation creationCode = | |||
| , allowFFI = False | |||
| , freshAddresses = 0 | |||
| , beaconRoot = 0 | |||
| , minMemoryChunk = 1 | |||
There was a problem hiding this comment.
Do we need this controllable? We can just set it to a sane default instead? I'd rather not have config options for stuff that a good default works for. It's useful to have this during figuring out what a good default is, but later, it may become a distraction perhaps? What do you think?
There was a problem hiding this comment.
My concern that led me to make this a tunable was symbolic execution. I'm not particularly familiar with how it is represented though so take this with a grain of salt, but what would happen if you end up having a large concrete memory due to the "optimistic growth", which then turns symbolic due to some other reason? How would that get encoded into Z3 et al? Would it hurt performance?
If my concern is unfounded I'm all for picking a good default and not having to have this option 😄
Description
An Echidna user reported continuously increasing memory while running mstore/mcopy operations. This PR attempts to resolve that by
Checklist