Tight field bounds have been successfully used in the context of bounded-exhaustive bug finding. They allow one to check the correctness of, or find bugs in, code manipulating data structures whose size made this kind of analyses previously infeasible. In this article we address the question of whether tight field bounds can also contribute to a significant speed-up for symbolic execution when using a system such as Symbolic Pathfinder. Specifically, we propose to change Symbolic Pathfinder's lazy initialization mechanism to take advantage of tight field bounds. While a straightforward approach that takes into account tight field bounds works well for small scopes, the lack of symmetry-breaking significantly affects its performance. We then introduce a new technique that generates only non-isomorphic structures and consequently is able to consider fewer structures and to execute faster than lazy initialization.
展开▼
