SV-Bechmarks - Githubissues

DonggeLiu / Legion

A coverage-based software testing tool

MIT License

29 stars 4 forks source link

SV-Bechmarks #11

Closed DonggeLiu closed 4 years ago

DonggeLiu commented 5 years ago

Not sure if Legion works on it properly;
Not sure if we can run other baselines (e.g. DFS.py) on it
Any baselines that have been tested in SV-COMP also use ANGR?

gernst commented 4 years ago

TODO:

@Alan32Liu find one benchmark with a timeout and just a few tests, then figure out what happened
@gernst get an account for @Alan32Liu to run sv-benchmarks on the LMU cloud
@Alan32Liu : add option to either discover the first error, or to keep going for maximum coverage

gernst commented 4 years ago

Note: Legion stopping to explore further paths is related to the claripy.errors.BackendError: unexpected type <class 'NotImplementedType'> Furthermore, this issue is not related to instrumentation and also not to the way we use Angr.

gernst commented 4 years ago

Ok it turns out that the code to find states of white nodes by symbolic execution does not match addresses right in all cases, causing it to miss the white node and to symbolically exectute up to the end of the program (which is taking very long for N = 100000 in some sv-benchmarks)

DonggeLiu commented 4 years ago

Pretty sure Legion is compatible with the TestComp framework now:

It did well in the competition
We are able to reproduce similar results on the local server.