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

1. Problem Statement

Dynamic Symbolic Execution (DSE) is a powerful technique for software testing and verification that explores all feasible program paths by treating inputs as symbolic values. However, DSE suffers from the path explosion problem, where the number of execution paths grows exponentially with the number of symbolic conditional branches.

• Current Limitations: The standard approach to mitigate this is dynamic state merging, which combines similar program states at runtime. However, dynamic merging still requires invoking an SMT solver at every symbolic branch to check path feasibility, even when both paths are feasible and will eventually be merged. This creates significant overhead.
• The Gap: While static compiler optimizations (like tail merging) exist, they often fail to handle complex control flow or require semantics-preserving constraints that limit their ability to eliminate branches in real-world code. There is a need for a transformation that aggressively removes expensive symbolic branches to improve DSE scalability, even if it slightly alters program semantics, provided it does not hide existing bugs.

2. Methodology: The cfm-se Transformation

The authors propose cfm-se (Control-Flow Melding for Symbolic Execution), a targeted, non-semantics-preserving but failure-preserving compiler transformation.

Core Concept

The transformation converts control-flow (branches) into data-flow. It identifies conditional branches where the if and else blocks contain similar instruction sequences. Instead of branching, it merges these blocks into a single basic block, executing instructions unconditionally and using select (ternary) instructions to choose operands. This eliminates the symbolic branch, preventing the DSE engine from forking execution.

Key Technical Steps

1. Symbolic Variable Analysis: The system performs an inter-procedural dataflow analysis (based on divergence analysis) to identify symbolic branches—branches where the condition depends on symbolic inputs. It specifically targets "expensive" branches that cause path explosion.
2. Instruction Alignment: For a target branch, the system aligns the instruction sequences of the then and else blocks.
3. Extra Instruction Insertion: If the sequences are not identical, cfm-se inserts extra instructions into the shorter path to make them identical.
   • Constraints: Inserted instructions must be side-effect-free (ALU operations) or safe memory reads/writes.
   • Safety: Original instructions cannot depend on values produced by extra instructions. Extra stores must write back the value they just read (idempotent).
4. Merging: Once aligned, the blocks are merged into a single basic block. The original branch is removed, and select instructions are inserted to handle operand differences.
5. Failure Preservation: The transformation is failure-preserving. While it may introduce new "false positive" bugs (e.g., out-of-bounds memory access due to unconditional execution), it guarantees that any bug present in the original program will still be present in the transformed program. It does not erase existing failures.

False Positive Detection Framework

Since cfm-se is non-semantics-preserving, it can introduce spurious crashes. The authors developed a driver framework to handle this:

1. Run DSE on the transformed program ($P'$).
2. If a crash is detected, re-run the original program ($P$) with the same input.
3. If the original program does not crash, the bug is a false positive.
4. The system records the location of the false positive and adds a constraint to prevent cfm-se from transforming that specific branch in future iterations.

3. Key Contributions

1. cfm-se Transformation: A novel compiler pass that removes expensive symbolic branches by converting control-flow to data-flow, specifically optimized for DSE scalability.
2. Failure-Preserving Guarantee: A theoretical proof and practical framework ensuring that while the transformation may introduce new bugs, it never hides existing bugs in the original code.
3. False Positive Detection System: An automated iterative driver that detects, filters, and avoids locations where the transformation introduces spurious failures.
4. Comprehensive Evaluation: Extensive benchmarks showing significant improvements in DSE performance, code coverage, and bug discovery speed on real-world C programs.

4. Experimental Results

The authors evaluated cfm-se using KLEE (a popular DSE engine) on 11 benchmark algorithms and 9 real-world open-source libraries (e.g., libosip, json.h, protobuf).

• RQ1: DSE Performance (Path Explosion):

  • cfm-se significantly reduced the number of SMT solver calls and explored paths.
  • On 8 out of 11 benchmarks, cfm-se outperformed both vanilla KLEE and KLEE with dynamic state merging.
  • In cases like toupper, it reduced the number of explored paths from $10^7$ to 1, and solver calls from 90 to 11.
  • Combining cfm-se with dynamic state merging (C-SM) yielded the best results for complex loops with dependencies.

• RQ2: Code Coverage:

  • cfm-se achieved maximum line coverage faster than vanilla KLEE in real-world programs.
  • For libosip, cfm-se reached 36% coverage in <500 seconds, whereas vanilla KLEE took nearly an hour.
  • The transformation allowed DSE to bypass deep loops with symbolic branches, reaching deeper code regions sooner.

• RQ3: Bug Discovery:

  • cfm-se found injected bugs faster than the original code.
  • In libosip, cfm-se found a NULL pointer dereference bug in ~18.5 hours, while vanilla KLEE timed out (24 hours) without finding it.
  • The transformation reduced memory pressure (fewer concurrent states), preventing state killing due to memory limits.

• Overhead:

  • Compile-time overhead was negligible (<2ms for most programs).
  • The number of added select instructions was minimal (<2% of total instructions).

5. Significance and Implications

• Scalability: cfm-se addresses the fundamental scalability bottleneck of DSE (path explosion) by performing "compile-time state merging," reducing the runtime burden on the SMT solver.
• Practicality for Real-World Code: Unlike pure semantics-preserving optimizations, cfm-se is willing to alter semantics to gain performance, provided it preserves failure modes. This makes it uniquely suited for testing, where the goal is bug detection rather than strict semantic equivalence.
• Complementarity: The results show that static transformations (cfm-se) and dynamic techniques (state merging) are complementary. Using both yields the best performance.
• Future Direction: The paper highlights the need for better cost models to predict the complexity of constraints generated by such transformations, particularly in the presence of loop-carried dependencies.

In summary, cfm-se offers a pragmatic and highly effective approach to "taming" the path explosion in DSE, enabling deeper and faster analysis of complex real-world software systems.