Infeasible path generalization in dynamic symbolic execution
Résumé
Context:
Automatic code-based test input generation aims at generating a test suite ensuring good code coverage. Dynamic Symbolic Execution (DSE) recently emerged as a strong code-based testing technique to increase coverage by solving path conditions with a combination of symbolic constraint solving and concrete executions.
Objective:
When selecting paths in DSE for generating test inputs, some paths are actually detected as being infeasible, meaning that no input can be found to exercize them. But, showing path infeasibility instead of generating test inputs is costly and most effort could be saved in DSE by reusing path infeasibility information.
Method:
In this paper, we propose a method that takes opportunity of the detection of a single infeasible path to generalize to a possibly infinite family of infeasible paths. The method first extracts an explanation of path condition, that is, the reason of the path infeasibility. Then, it determines conditions, using data dependency information, that paths must respect to exhibit the same infeasibility. Finally, it constructs an automaton matching the generalized infeasible paths.
Results:
We implemented our method in a prototype tool called IPEG (Infeasible Path Explanation and Generalization), for DSE of C programs. First experimental results obtained with IPEG show that our approach can save considerable effort in DSE, when generating test inputs for increasing code coverage.
Conclusion:
Infeasible path generalization allows test generation to know of numerous infeasible paths ahead of time, and consequently to save the time needed to show their infeasibility.