binrec-tob icon indicating copy to clipboard operation
binrec-tob copied to clipboard

Make use of S2E parallel execution mode

Open hbrodin opened this issue 4 years ago • 4 comments

Instead of running the cmd-debian-mt.sh script, can we use S2E parallel execution mode directly?

hbrodin avatar Oct 12 '21 08:10 hbrodin

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:

  1. Add support to BinRec's justfile and python API as needed to support running a project with multiple concrete inputs
  2. 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.
  3. Create unit tests as necessary for components built
  4. Add new integration tests that use the parallel execution mode (a subset of the benchmarks we already have is fine)

michaelbrownuc avatar Jan 27 '22 14:01 michaelbrownuc

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.

ameily avatar Feb 02 '22 16:02 ameily

This issue is no longer blocked as symbolic tracing is now supported.

michaelbrownuc avatar Apr 06 '22 20:04 michaelbrownuc

Marking low-priority - we only need to do this if/when performance fails to scale with binary size.

michaelbrownuc avatar Apr 06 '22 20:04 michaelbrownuc