Robin David, Sébastien Bardin, Laurent Mounier, Marie-Laure Potet, Thanh Dinh Ta, Jean-Yves Marion, and Josselin Feist
Symbolic Execution (SE) is a popular and profitable approach to automatic (code-based) software testing, leading to impressive results in bug finding and security analysis. Concretization and symbolization (C/S) are a crucial part of modern SE tools, together with path predicate computation and path selection, since C/S directly impacts the trade-offs between correctness, completeness and efficiency of the approach. Yet, C/S policies have been barely studied. Especially, design choices behind C/S policy are often hardly explained, and most of SE tools propose only hardcoded C/S policies. We propose a clear separation of concerns between the specification of C/S policies on one side, through a rule-based description language, and the algorithmic core of SE on the other side, revisited to take C/S policies into account. As a first application, we perform an extensive review of C/S policies found in the literature, and we show how to encode them into our language. As a second application, we implement this generic specification mechanism on top of an existing SE tool, demonstrating the applicability of the method. Especially, the overhead induced by the high-level specification mechanism turns out to be very light. As a third application, we propose the first quantitative comparison on C/S policies. This work paves the way for more flexible SE tools with well-documented and reusable C/S policies as well as for a more systematic study of C/S policies.