Resolving loop based path explosion during Symbolic Execution

Symbolic execution is a widely used method for testing device drivers and achieving high code coverage. One problem in exploring code using symbolic execution is loop based path explosion. First, trying all paths using dynamic techniques does not guarantee additional code coverage. Second, large formulas to reach new branch using static analysis do not scale well due to constraint solver limitations.This paper describes challenger deep, a static analysis tool that precomputes a sequence of sub-paths within the loop body so that a specified branch of code can be reached. We use Z3 constraint solver for small queries. For larger queries where Z3 takes exceedingly large time, we switch to a genetic algorithm. Our tool is generic and can be used in both functional testing or whole program testing when a loop construct is encountered.