Taming the Hydra: Targeted Control-Flow Transformations for Dynamic Symbolic Execution

TL;DR

This paper introduces a compiler transformation that removes costly symbolic branches to enhance the scalability and efficiency of Dynamic Symbolic Execution in analyzing complex programs.

Contribution

It proposes a novel, non-semantics-preserving transformation that reduces symbolic branches, improving DSE performance and bug detection capabilities.

Findings

Significantly improves DSE performance on benchmark programs.

Helps discover more bugs and achieve better coverage in large real-world programs.

Framework for detecting spurious bugs introduced by transformations.

Abstract

Dynamic Symbolic Execution (DSE) suffers from the path explosion problem when the target program has many conditional branches. The classical approach for managing the path explosion problem is dynamic state merging. Dynamic state merging combines similar symbolic program states to avoid the exponential growth in the number of states during DSE. However, state merging still requires solver invocations at each program branch, even when both paths of the branch are feasible. Moreover, the best path search strategy for DSE may not create the best state merging opportunities. Some drawbacks of state merging can be mitigated by compile-time state merging (i.e., branch elimination by converting control-flow into dataflow). In this paper, we propose a non-semantics-preserving but failure-preserving compiler transformation for removing expensive symbolic branches in a program to improve the scalability of DSE. We have developed a framework for detecting spurious bugs that our transformation can insert. Finally, we show that our transformation can significantly improve the performance of DSE on various benchmark programs and help improve the performance of coverage and bug discovery of large real-world programs.