Make use of S2E parallel execution mode
Old issue, but is important to tackle soon. Now that we have a foothold on the new version of s2e working with single concrete inputs at a time, the next step is to implement an interface to the parallel execution mode to speed things up.
This appears to be somewhat straightforward based on the docs link above. It looks like it involves editing the launch s2e script before invoking the s2e run command. I'm not sure how you specify multiple concrete inputs, the docs refer to symbolic exploration.
High level tasks for this issue:
- Add support to BinRec's justfile and python API as needed to support running a project with multiple concrete inputs
- Create a copy of the walkthrough in the README that uses parallel execution. We will add this to the docs eventually once we start assembling them.
- Create unit tests as necessary for components built
- Add new integration tests that use the parallel execution mode (a subset of the benchmarks we already have is fine)
I believe that the docs about parallel execution is only for symbolic execution/analysis, which our S2E integration does not support currently, trailofbits/binrec-prerelease#82, which is why the docs don't mention specifying multiple concrete inputs.
So, I think this is blocked until we have symbolic execution/analysis working.
This issue is no longer blocked as symbolic tracing is now supported.
Marking low-priority - we only need to do this if/when performance fails to scale with binary size.