Efficient state merging in symbolic execution

ABSTRACT

Symbolic execution has proven to be a practical technique for building automated test case generation and bug finding tools. Nevertheless, due to state explosion, these tools still struggle to achieve scalability. Given a program, one way to reduce the number of states that the tools need to explore is to merge states obtained on different paths. Alas, doing so increases the size of symbolic path conditions (thereby stressing the underlying constraint solver) and interferes with optimizations of the exploration process (also referred to as search strategies). The net effect is that state merging may actually lower performance rather than increase it.

We present a way to automatically choose when and how to merge states such that the performance of symbolic execution is significantly increased. First, we present query count estimation, a method for statically estimating the impact that each symbolic variable has on solver queries that follow a potential merge point; states are then merged only when doing so promises to be advantageous. Second, we present dynamic state merging, a technique for merging states that interacts favorably with search strategies in automated test case generation and bug finding tools.

Experiments on the 96 GNU Coreutils show that our approach consistently achieves several orders of magnitude speedup over previously published results. Our code and experimental data are publicly available at http://cloud9.epfl.ch.

References

1. S. Anand, P. Godefroid, and N. Tillmann. Demand-driven compositional symbolic execution. In Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008.
2. D. Babic and A. J. Hu. Calysto: scalable and precise extended static checking. In Intl. Conf. on Software Engineering (ICSE), 2008.
3. P. Boonstoppel, C. Cadar, and D. R. Engler. RWset: Attacking path explosion in constraint-based test generation. In Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008.
4. R. S. Boyer, B. Elspas, and K. N. Levitt. SELECT -- a formal system for testing and debugging programs by symbolic execution. In Intl. Conf. on Reliable Software (ICRS), 1975.
5. C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. EXE: Automatically generating inputs of death. In Conf. on Computer and Communications Security (CCS), 2006.
6. C. Cadar, D. Dunbar, and D. R. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Symp. on Operating Systems Design and Implementation (SOSP), 2008.
7. V. Chipounov, V. Kuznetsov, and G. Candea. S2E: A platform for in-vivo multi-path analysis of software systems. In Intl. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2011.
8. E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2004.
9. M. Das, S. Lerner, and M. Seigle. ESP: Path-sensitive program verification in polynomial time. In Intl. Conf. on Programming Language Design and Implem. (PLDI), 2002.
10. L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008.
11. E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM, 18(8):453--457, 1975.
12. N. Eén and N. Sörensson. An extensible SAT-solver. In Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT), 2003.
13. C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In Intl. Conf. on Programming Language Design and Implem. (PLDI), 2002.
14. M. K. Ganai and A. Gupta. Tunneling and slicing: towards scalable BMC. In Design Automation Conf. (DAC), 2008.
15. V. Ganesh and D. L. Dill. A decision procedure for bit-vectors and arrays. In Intl. Conf. on Computer Aided Verification (CAV), 2007.
16. P. Godefroid. Compositional dynamic test generation. In Symp. on Principles of Programming Languages (POPL), 2007.
17. P. Godefroid and D. Luchaup. Automatic partial loop summarization in dynamic test generation. In Intl. Symp. on Software Testing and Analysis (ISSTA), 2011.
18. P. Godefroid, N. Klarlund, and K. Sen. DART: Directed automated random testing. In Intl. Conf. on Programming Language Design and Implem. (PLDI), 2005.
19. P. Godefroid, M. Y. Levin, and D. Molnar. Automated whitebox fuzz testing. In Network and Distributed System Security Symp. (NDSS), 2008.
20. T. Hansen, P. Schachte, and H. Sondergaard. State joining and splitting for the symbolic execution of binaries. In Intl. Conf. on Runtime Verification (RV), 2009.
21. F. Ivancic, Z. Yang, M. K. Ganai, A. Gupta, I. Shlyakhter, and P. Ashar. F-soft: Software verification platform. In Intl. Conf. on Computer Aided Verification (CAV), 2005.
22. F. Ivancic, G. Balakrishnan, A. Gupta, S. Sankaranarayanan, N. Maeda, H. Tokuoka, T. Imoto, and Y. Miyazaki. DC2: A framework for scalable, scope-bounded software verification. In Intl. Conf. on Automated Software Engineering (ASE), 2011.
23. J. C. King. A new approach to program testing. In Intl. Conf. on Reliable Software (ICRS), 1975.
24. S. K. Lahiri and S. Qadeer. Back to the future: revisiting precise program verification using SMT solvers. In Symp. on Principles of Programming Languages (POPL), 2008.
25. C. Lattner and V. Adve. LLVM: A compilation framework for lifelong program analysis and transformation. In Intl. Symp. on Code Generation and Optimization (CGO), 2004.
26. K. R. M. Leino and P. Rümmer. A polymorphic intermediate verification language: Design and logical encoding. In Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2010.
27. L. Mauborgne and X. Rival. Trace partitioning in abstract interpretation based static analyzers. In European Symp. on Programming (ESOP), 2005.
28. K. L. McMillan. Lazy annotation for program testing and verification. In Intl. Conf. on Computer Aided Verification (CAV), 2010.
29. O. Sery, G. Fedyukovich, and N. Sharygina. Interpolation-based function summaries in bounded model checking. In Haifa Verification Conf. (HVC), 2011.
30. D. Wheeler. SLOCCount. http://www.dwheeler.com/sloccount/,2010.
31. Y. Xie and A. Aiken. Scalable error detection using boolean satisfiability. In Symp. on Principles of Programming Languages (POPL), 2005.

Index Terms

• Computing methodologies

  • Symbolic and algebraic manipulation

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

      • Software defect analysis

        • Software testing and debugging

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Logic

  • Models of computation

    • Abstract machines

  • Semantics and reasoning

    • Program reasoning

      • Abstraction

      • Program verification