Pathing

In order to symbolically execute multiple basic blocks at a time, the decision making process as to which block to execute next requires some sort of pathing strategy. Currently all pathing strategies used by Reilex involve depth first searches, or exhaustive searches of the CFG.
For example, the pathing strategy used by the unused code finder is simply an exhaustive search over the CFG. This is of course massively computationally expensive for any serious software, however for small pieces of software of or small patches, it is acceptable. To reduce some of this computational cost, whenever a pathing decision must be made, both paths are checked for satisfiability with Z3. This is a simple process, since flags are represented as 1 bit bitvectors with some constraint on them, so to check satisfiability of a path, the zero flag constraint is passed to Z3 to solve.

More bathing strategies, like randomized searches and seeded searches are on the way,