Performance on DeepState Lists example much worse than angr

[agroce]

OS / Environment

Ubuntu trusty (in Travis)

Manticore version

0.1.10

Python version

2.7

Summary of the problem

In DeepState CI tests, Lists example runs in ~100 seconds using angr backend, but manticore times out at 50 minutes, with multiple solver timeouts.

Step to reproduce the behavior

See https://travis-ci.org/trailofbits/deepstate/jobs/403967802

1. Install DeepState
2. deepstate-manticore build/examples/Lists

[offlinemark]

thanks for letting us know!

[offlinemark]

here's the deepstate Lists example

  ForAll<std::vector<int>>([] (const std::vector<int> &vec1) {
    std::vector<int> vec2 = vec1;
    std::reverse(vec2.begin(), vec2.end());
    std::reverse(vec2.begin(), vec2.end());
    ASSERT_EQ(vec1, vec2)
        << "Double reverse of vectors must be equal.";
  });
}

it seems this test is doing a ForAll<std::vector<int>>, which I believe means to create a symbolic std::vector<int>. i'm not entirely sure what this means in terms of what bytes DeepState makes symbolic at the memory level (would love some details on this!), but my hypothesis is that Manticore struggles with the dynamic allocations involves with std::vectors. i believe angr uses SimProcedures to model malloc family functions, we don't have models for those at the moment.

@ggrieco-tob noticed that angr reports some warnings related to symbolic brk: https://travis-ci.org/trailofbits/deepstate/jobs/403901656