Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code

1. Problem Statement

Symbolic execution is a powerful program analysis technique but faces three fundamental limitations that hinder its effectiveness on real-world code:

1. Solver-Hostile Fragments: Complex computations (e.g., non-linear arithmetic, trigonometric functions, floating-point operations) generate constraints that SMT solvers cannot efficiently solve or are undecidable.
2. Global Consistency: Large Language Models (LLMs) used as standalone solvers struggle to maintain long-range, formally checkable dependencies across deep execution paths and multiple functions, often failing to satisfy inter-procedural constraints.
3. Heap Explosion: Programs using dynamic data structures (pointers, linked lists, trees) suffer from path explosion due to the infinite number of possible heap configurations and aliasing relationships.

Existing hybrid approaches that replace SMT solvers entirely with LLMs (e.g., ConcoLLMic) fail to analyze deep, complex codebases because LLMs lack the rigorous global reasoning capabilities of solvers. Conversely, pure symbolic execution gets stuck on "logic bombs"—specific code fragments that block path exploration.

2. Methodology: The Gordian Framework

The authors propose Gordian, a hybrid symbolic execution framework that integrates Large Language Models (LLMs) selectively to assist, rather than replace, SMT solvers. The core innovation is the generation of Ghost Code—auxiliary code added to the program to facilitate reasoning without altering functional behavior.

Gordian operates by identifying difficult code fragments and generating one of three types of LLM-based ghost code:

A. Ghost Code for Fragment Inversion (Bidirectional Constraint Propagation)

• Problem: Fragments like sin(x) or complex arithmetic prevent forward constraint solving.
• Solution: The LLM generates an inverse function (e.g., a golden-section search to invert sin(x)).
• Mechanism:
  1. The difficult fragment is replaced with fresh symbolic variables (havoc).
  2. The SMT solver solves the suffix constraints (post-fragment) to find target output values.
  3. The generated inverse function is executed concretely to propagate these values backward to estimate pre-state inputs.
  4. An optimization solver (OMT) finds the closest valid input that satisfies the prefix constraints (pre-fragment).
  5. This "meet-in-the-middle" approach bridges the gap between complex forward semantics and backward requirements.

B. Ghost Code for Surrogate Modeling

• Problem: Some fragments are non-invertible (many-to-one) or rely on external state, making inversion impossible.
• Solution: The LLM generates a solver-friendly surrogate that approximates the original behavior but translates into theories the SMT solver can handle (e.g., replacing complex crypto or floating-point logic with bit-vector or linear arithmetic approximations).
• Safety: Since the surrogate is an approximation, any inputs generated are validated by re-executing the original program to ensure soundness.

C. Ghost Code for Semantic Heap Partitioning

• Problem: Dynamic data structures cause path explosion due to unbounded heap shapes.
• Solution: The LLM analyzes the domain context and generates code to constrain the heap into a small set of semantic topologies (e.g., a ring, a broken chain, a specific list length).
• Mechanism: A selector variable chooses a topology, and the ghost code enforces specific structural constraints (e.g., n0->next == n1) while leaving data values symbolic. This reduces the search space to meaningful shapes without over-constraining the data.

3. Key Contributions

1. Novel Integration: A framework that uses LLMs to generate lightweight ghost code to aid SMT solvers, preserving global reasoning while bypassing local solver bottlenecks.
2. Three Ghost Code Variants:
   • Inversion for bidirectional constraint propagation.
   • Surrogate modeling for solver-friendly approximation.
   • Semantic heap partitioning for dynamic data structure handling.
3. Comprehensive Evaluation: Implementation on the KLEE engine and evaluation across synthetic benchmarks, a real-world math library, and structured-input parsers.
4. Soundness Guarantee: The system treats LLM outputs as heuristics; all generated inputs are validated against the original program, ensuring that hallucinations do not produce false positives (unsound results).

4. Experimental Results

The framework was evaluated on three benchmarks:

1. LogicBombs (53 synthetic programs): Designed to trigger specific symbolic reasoning challenges.
2. FDLibM (78 entry points): A popular math library with complex floating-point logic.
3. Structured-Input Programs (libexpat, jq, bc): Real-world parsers relying on complex dynamic data structures.

Performance Metrics:

• Coverage Improvement:
  • vs. Traditional Symbolic Execution (KLEE): Improved coverage by 52–84%.
  • vs. LLM-based Techniques (ConcoLLMic, Cottontail): Improved coverage by 86–419%.
  • On LogicBombs, Gordian triggered 94.3% of logic bombs (vs. ~39% for KLEE and ~64% for ConcoLLMic).
  • On FDLibM, Gordian achieved ~91% average line coverage (vs. ~40% for ConcoLLMic and ~63% for KLEE).
• Token Efficiency:
  • Gordian reduced LLM token usage by 90–96% compared to LLM-based baselines.
  • It used roughly 10x to 40x fewer tokens than ConcoLLMic because it only queries the LLM for specific fragments rather than the entire execution path.
• Ablation Study: Confirmed that all three ghost code types contribute uniquely to the performance gains, with their union covering nearly all reachable paths.

5. Significance and Conclusion

Gordian represents a significant shift in how AI is applied to program analysis. Instead of replacing rigorous formal methods (SMT solvers) with probabilistic models (LLMs), it uses LLMs as specialized assistants to generate code that makes difficult problems tractable for solvers.

• Practicality: It successfully scales to real-world libraries and structured-input programs where pure symbolic execution fails and pure LLM approaches lack global consistency.
• Efficiency: By minimizing LLM usage to specific "hot spots," it achieves high coverage at a fraction of the computational cost of fully LLM-driven testing.
• Future Impact: The approach suggests a future where symbolic execution engines dynamically delegate specific reasoning tasks to LLMs, creating a hybrid system that combines the precision of solvers with the domain knowledge and code generation capabilities of LLMs.

The paper concludes that Gordian effectively "defuses" logic bombs in symbolic execution, making it a viable tool for analyzing complex, real-world software systems.