Concrete replay feature

[offlinemark]

Manticore generates inputs that cause programs to reach a certain state. It's often desirable to be able to reproduce these states concrete -- "Manticore found an input that crashes the program? Let's see it actually crash."

For binaries, reproducing this state under concrete execution is usually pretty easy -- just execute the program with the generated input. For smart contracts, it's not as straightforward to "just execute" a smart contract. For ethereum, It would be nice to just be able to feed an input that was generated, back into Manticore, and have manticore execute concretely to reproduce this state.

Some rough initial work was started in this branch: https://github.com/trailofbits/manticore/tree/dev-concrete-replay

how the feature works in that branch:

• emit a json file for the generated tx data
• cli interface accepts one of these json files
• based on the to/from information in the tx json file, recreate the accounts and contract
• loop through the txs and execute concrete transactions with the data specific in the json file

since that branch, the tx file generation has been merged in master, so that is already done.

the problems with the initial implementation:

• adds a top level ManticoreEVM.txreplay which the cli forwards to. this is in the same vein as ManticoreEVM.multi_tx_analysis, and similarly it doesn't exactly seem like the right place to put this high level code? we need some kind of place in the codebase for this high level logic on top of ManticoreEVM.
• current implementation only supports an owner and attacker account, not arbitrary account setups
• current impl only supports 1 contract account
• the way the cli output is done is a bit hacky, with an inline function definition for a did_close_transaction callback (the whole thing is hacky)

[ehennenfent]

https://github.com/trailofbits/manticore/wiki/Ideas