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

Abstract

Symbolic execution is a powerful program analysis technique, but its effectiveness is fundamentally limited by solver-hostile program fragments, complex numerical reasoning, and unbounded heap structures. Recent work proposed replacing constraint solvers with large language models (LLMs) to bypass these limitations, but such approaches struggle to analyze real-world codebases, where deep execution paths require globally consistent reasoning across many interacting constraints. We present Gordian, a hybrid symbolic execution framework that uses LLMs selectively to generate lightweight ghost code that aids an SMT solver in handling solver-hostile code fragments, while preserving its precise, global reasoning capability. In particular, we propose three types of ghost code: (1) inversion of difficult code fragments with iterative bidirectional constraint propagation, (2) modeling via solver-friendly surrogates while preserving relevant behavior, and (3) semantic partitioning of unbounded heap spaces. We implemented Gordian on top of the KLEE symbolic execution engine and evaluated it on synthetic "logic bombs" capturing distinct symbolic reasoning challenges, a popular mathematical library FDLibM, and three structured-input programs (libexpat, jq, and bc). Across all benchmarks, Gordian improves coverage on average by 52-84% over traditional symbolic execution baselines, and by 86-419% over LLM-based techniques, while reducing LLM token usage by an average of 90-96%. This highlights the practicality and effectiveness of this approach in real-world settings.

Figures (8)

• Figure 1: Gordian propagates constraints through a difficult code fragment that involves trigonometric operations using a concrete execution of an LLM-generated ghost function that inverts the fragment.
• Figure 2: Gordian tackles heap-configuration explosion by using LLM-generated ghost code to constrain the heap to semantically meaningful data-structure shapes while preserving symbolic contents.
• Figure 3: A simplified fragment of Gordian's prompt template for generating ghost code that inverts a difficult fragment, where SIGN is the signature of the desired function, VARS are the variables, whose values the inversion needs to compute, and CODE is the code fragment.
• Figure 4: Running example to illustrate ghost inversion and bidirectional constraint propagation.
• Figure 5: Bidirectional constraint propagation.