PaperlayerView exact revision on arXiv

Source-linked AI summary

Python Symbolic Execution with LLM-powered Code Generation

Wenhan Wang, Kaibo Liu, An Ran Chen, Ge Li, Zhi Jin, Gang Huang, Lei Ma

arXiv:2409.09271v1cs.SEcs.PL

TL;DR

Symbolic execution for Python is difficult because dynamic typing and flexible data structures complicate translation of path constraints into SMT constraints. LLM-Sym uses an LLM to generate Z3 code through a multi-step pipeline, extending a basic engine to Python lists. In LeetCode trace experiments, it solves around 60% of traces, outperforms pure LLM-based approaches, and costs less than one-third of GPT-4o while achieving similar results.

  • Problem

    Dynamic typing and flexible Python data structures make it difficult to translate execution paths into SMT constraints, while path-constraint solving also limits symbolic execution’s broader use.

    Source: §1 · p. 2

  • Method

    LLM-Sym extends an introductory symbolic execution engine with an LLM agent that generates Z3 code using type inference, retrieved templates, and self-refinement.

    Source: §1 · p. 2

  • Results

    LLM-Sym correctly solves around 60% of execution traces, outperforms pure LLM-based approaches, and costs less than one-third of GPT-4o while achieving similar results.

    Source: §1 · p. 3

  • Takeaways & Limitations

    The authors report that LLM-Sym can generate correct Z3 code and test cases for long LeetCode paths, including constraints on Python lists.

    Source: §1 · p. 3, §7 · p. 18

    LLM-Sym does not address the path-explosion weakness of its execution-path extractor.

    Source: §3.1 · p. 6

Abstract

from arXiv · show

Symbolic execution is a key technology in software testing, which generates test cases by collecting symbolic path constraints and then solving constraints with SMT solvers. Symbolic execution has been proven helpful in generating high-coverage test cases, but its limitations, e.g., the difficulties in solving path constraints, prevent it from broader usage in software testing. Moreover, symbolic execution has encountered many difficulties when applied to dynamically typed languages like Python, because it is extremely challenging to translate the flexible Python grammar into rigid solvers. To overcome the main challenges of applying symbolic execution in Python, we proposed an LLM-empowered agent, LLM-Sym, that automatically calls an SMT solver, Z3, to solve execution path constraints. Based on an introductory-level symbolic execution engine, our LLM agent can extend it to supporting programs with complex data type `list'. The core contribution of LLM-Sym is translating complex Python path constraints into Z3 code. To enable accurate path-to-Z3 translation, we design a multiple-step code generation pipeline including type inference, retrieval and self-refine. Our experiments demonstrate that LLM-Sym is capable of solving path constraints on Leetcode problems with complicated control flows and list data structures, which is impossible for the backbone symbolic execution engine. Our approach paves the way for the combination of the generation ability of LLMs with the reasoning ability of symbolic solvers, and opens up new opportunities in LLM-augmented test case generation.

1 Introduction

Python’s dynamic typing and flexible data structures make path-to-SMT translation difficult, limiting symbolic execution. LLM-Sym uses an LLM to generate Z3 code, and its LeetCode evaluation reports that it solves around 60% of execution traces and outperforms pure LLM-based approaches.

1 Introduction

  • Python’s dynamic typing and flexible data structures, including variable-length lists, make it difficult to translate execution paths into SMT constraints.Without explicit type annotations, solver variables’ types are difficult to define; list-length conditions may require additional constraints.Source: §1 · p. 2
  • LLM-Sym uses an LLM agent to generate code that calls Z3, extending an introductory symbolic execution engine rather than writing fixed translation rules.The underlying engine’s path extractor is retained, while its rule-based path-to-Z3 translator is replaced.Source: §1 · p. 2
  • Its pipeline infers variable types, generates Z3 code for path chunks with retrieved templates, self-refines buggy code, and then asks Z3 to solve the constraints.If code fixes fail, the system directly uses an LLM solver; test cases are generated from the solving results.Source: §1 · pp. 2–3
  • LLM-Sym correctly solves around 60% of the execution traces, outperforms pure LLM-based approaches, and costs less than one-third of GPT-4o while achieving similar results.The evaluation uses 111 traces from 50 LeetCode programs.Source: §1 · p. 3
  • The paper presents LLM-Sym as supporting Python lists and dynamic data types without concolic execution, and reports correct code and test cases for long LeetCode paths.The authors also introduce a dataset of LeetCode execution paths for evaluation.Source: §1 · p. 3

2 Motivating Example

The motivating example contrasts straightforward rule-based translation of simple, explicitly typed paths with paths involving complex data structures or non-trivial list reasoning. LLM-Sym targets the latter by generating Z3 code for constraints that are solver-solvable but difficult to encode by hand.

2 Motivating Example

  • For a simple path with explicit integer types and basic operators, variables can be converted to SSA and statements added to the solver using straightforward translation rules.The Fuzzing Book implementation used 76 lines of code to translate one line of execution path into Z3 code.Source: §2 · pp. 3–4
  • User-defined types and external function calls can make rule-based translation unable to describe a path’s constraints accurately; concolic execution instead relies on concrete inputs.The paper notes that concrete inputs may make certain paths difficult to reach and that executing unverified inputs may introduce security risks.Source: §2 · p. 4
  • For constraints solvable by Z3 but requiring non-trivial reasoning, LLM-Sym generates Z3 code for operations such as list indexing, list assignments, and abs().The motivating figure describes LLMs as capable of generating complex code with non-trivial patterns.Source: §2 · p. 4, Figure 1 · p. 4

3 Approach

LLM-Sym extracts Python execution paths, then uses an LLM agent to translate path constraints into Z3 code and generate test cases. Its pipeline combines type prediction, retrieved code templates, and self-refinement, with direct LLM solving as a fallback.

3 Approach

  • LLM-Sym turns extracted Python paths into Z3 constraints using retrieved templates and self-refinement, then generates test cases from solver results.If Z3 code generation fails, it asks an LLM to solve the path directly.Source: §3 · p. 5, §3.2.2 · p. 8, §3.2.3 · p. 9

3.1 Execution path extractor

  • The extractor builds a CFG from the program’s AST and uses breadth-first search to extract paths; long paths are split into chunks because they can increase generation errors.The default chunks contain one statement; an alternative splits at condition statements.Source: §3.1 · pp. 5–6
  • Path extraction retains an intrinsic path-explosion weakness, which the authors do not target with their improvements.The extractor also adds support for class definitions and marks loop iterations in path nodes.Source: §3.1 · pp. 5–6

3.2.1 Type predictor.

  • Before generating Z3 code, an LLM predicts variable types from the program, assuming each variable’s type stays unchanged during execution.For sequence and mapping variables, the predictor is prompted to specify element, key, and value types.Source: §3.2.1 · p. 6

3.2.2 Z3 code generator.

  • The Z3 code generator processes path chunks using predicted types and prior code, while tracking SSA indices in a variable environment.A manually built retrieval base provides 14 Python-to-Z3 templates, including four list operations modeled with Z3.Array values and symbolic lengths.Source: §3.2.2 · p. 7, Table 1 · p. 8
  • Generated code is executed after each chunk; when it fails, an LLM attempts repairs up to three times before generation stops and direct LLM solving takes over.The repair prompt includes the buggy code and its error message.Source: §3.2.2 · pp. 7–8, §3.2.4 · p. 9

3.2.3 Test case generator.

  • After solving, the test-case generator identifies input-related SSA values and reconstructs Python inputs, including lists from Z3 arrays and their lengths.GPT-4o is used for this module because it interprets Z3 arrays better than GPT-4o-mini.Source: §3.2.3 · p. 9

3.2.4 LLM solver.

  • When Z3 code generation cannot solve a path, a simple-prompt LLM solver predicts satisfiability and generates possible input values and a test case.Improving this solver is left to future work.Source: §3.2.4 · p. 9

4 Experiments

On the LeetCode dataset, LLM-Sym generated test cases reproducing over 63% of input execution traces. Experiments also examined its retrieval, self-refine, and Z3-code-generation components, their comparison with direct LLM solving, and efficiency.

4.1 Experiment settings

  • LLM-Sym used GPT-4o-mini for modules other than test-case generation, which used GPT-4o; the agent was implemented with AutoGen.The paper identifies the AutoGen library as the implementation framework.Source: §4.1 · p. 10

4.2 Dataset

  • The dataset comprised 111 execution traces from 50 LeetCode programs, truncated to a maximum length of 20 statements and averaging 12.3 statements.The backbone engine could solve none of these traces, given absent explicit type annotations and Python list structures.Source: §4.2 · p. 10

4.3 RQ1: Capability of LLM-Sym

  • Over 63% of 111 generated results reproduced the exact execution trace of the input example.The evaluation counted results that solved path constraints, produced runnable tests, and correctly fulfilled the trace.Source: §4.3 · p. 10
  • For list assignment, retrieval supplied a relevant template, and the generator composed array assignments to implement swapping list elements.The example also reports that the generator correctly handled this operation despite similar patterns being absent from the template knowledge base.Source: §4.3 · pp. 11–12
  • An incorrect SSA-variable reference changed the generated constraints and made a satisfiable path unsolvable in the illustrated failure case.The generator used _num_0 where the path required _num_1.Source: §4.3 · pp. 12–13

4.4 RQ2: Submodule analysis

  • Two retrieved templates yielded the highest path pass rate; line-based chunks outperformed condition-based chunks, and even five-template retrieval missed relevant templates for 19% of statements.Self-refine fixed a Z3 type error by replacing Python // with Z3Py / for integer division, but the authors say it is unlikely to fix code beyond the generator's ability.Source: §4.4 · pp. 13–15

4.5 RQ3: comparison between Z3 code generator and LLM solver

  • With two retrieved templates, the Z3 code generator produced 74 solutions at a 73% pass rate, exceeding the LLM solver's solution count and pass rate.The table excludes UNSAT generation results.Source: §4.5 · p. 15, Table 6 · p. 15

4.6 RQ4: Time and cost efficiency

  • LLM-Sym averaged 20.2 seconds and $0.005 per path; its cost was one-third of GPT-4o's, with time overhead under twice as high.The authors report similar results to GPT-4o and attribute LLM-Sym's lower cost to its GPT-4o-mini backbone.Source: §4.6 · pp. 16–17, Table 8 · p. 16

5 Threats to Validity

The authors bound validity claims by the models and Python operations evaluated, and by the benchmark data used.

5.1 Model validity

  • The evaluation uses GPT-4o and GPT-4o-mini, without testing other models.The authors describe these models as widely used state-of-the-art LLMs and consider the results representative.Source: §5.1 · p. 17
  • LLM-Sym supports only part of Python list operations and does not explicitly support other data structures.The authors say support for additional operations can be added through knowledge-base examples; the Z3 code generator is also limited by Z3, with stronger LLM-solver reasoning left for future work.Source: §5.1 · p. 17

5.2 Data validity

  • The evaluation covers only a subset of LeetCode solutions, chosen as an initial step before evaluating more complicated real-world data.The authors say they first aim to understand LLM-Sym on simple, restricted programs.Source: §5.2 · p. 17

6 Related Work

Related work covers symbolic execution and Python support, then LLM-based test generation and approaches combining LLMs with testing or analysis tools.

6.1 Symbolic execution

  • Symbolic execution uses symbolic values and SMT solving to explore paths, but can face path explosion and difficulty solving nonlinear constraints or external API calls.Concolic execution combines concrete execution with collected path constraints; KLEE, SPF, and Triton are cited as engines based on it.Source: §6.1 · p. 17
  • Few symbolic execution engines support Python; PyExZ3 lacks list support and is deprecated, while CrossHair is concolic and requires explicit input type annotations.The paper does not compare CrossHair because it does not support pure-symbolic constraint solving.Source: §6.1 · pp. 17–18

6.2 LLM for test case generation

  • LLM-based test-generation work includes unit tests and benchmark datasets, while Symprompt gives execution paths to an LLM in one prompt without improving constraint solving.The authors note that this single-prompt approach may hinder complex constraint reasoning.Source: §6.2 · p. 18
  • Other approaches combine LLMs with testing or analysis tools: CodaMosa supplies seeds to Pynguin, TELPA [34] guides method sequences, and HITS [32] uses program slices.Source: §6.2 · p. 18

7 Conclusion

LLM-Sym uses an LLM agent to generate Z3 code for Python path constraints, focusing its knowledge base on lists. Experiments report correct code generation for long LeetCode paths and an advantage for LLM-plus-Z3 over a state-of-the-art LLM.

7 Conclusion

  • LLM-Sym combines a retrieval knowledge base and self-refinement to generate Z3 code for complex Python statements.The knowledge base focuses on Python lists, and LLMs solve constraints that Z3 cannot solve.Source: §7 · p. 18
  • LLM-Sym generates correct Z3 code for long path constraints in LeetCode programs.Source: §7 · p. 18
  • Integrating a cost-efficient LLM with Z3 beats the most state-of-the-art LLM in constraint solving for Python symbolic execution.Source: §7 · p. 18
Loading 2409.09271v1…