利用 LLM 驱动代码生成的 Python 符号执行
Python Symbolic Execution with LLM-powered Code Generation
AI总结：
本文提出 LLM-Sym 智能体，通过类型推断、检索与自我精化流水线将 Python 复杂路径约束转换为 Z3 代码，使入门级符号执行引擎可处理含 list 和复杂控制流的程序。
摘要：
符号执行是软件测试中的一项关键技术，它通过收集符号路径约束，随后使用 SMT 求解器求解约束来生成测试用例。符号执行已被证明有助于生成高覆盖率测试用例，但其局限性（例如求解路径约束的困难）阻碍了它在软件测试中的更广泛应用。此外，符号执行在应用于 Python 等动态类型语言时遇到了许多困难，因为将灵活的 Python 语法转换为严格的求解器极具挑战性。为了克服在 Python 中应用符号执行的主要挑战，我们提出了一个由 LLM 赋能的智能体 LLM-Sym，它会自动调用 SMT 求解器 Z3 来求解执行路径约束。基于一个入门级符号执行引擎，我们的 LLM 智能体能够将其扩展为支持包含复杂数据类型 `list' 的程序。LLM-Sym 的核心贡献是将复杂的 Python 路径约束转换为 Z3 代码。为实现准确的路径到 Z3 转换，我们设计了一个包含类型推断、检索和自我精化的多步骤代码生成流水线。实验表明，LLM-Sym 能够在具有复杂控制流和列表数据结构的 Leetcode 问题上求解路径约束，而这对于作为骨干的符号执行引擎是不可能的。我们的方法为结合 LLM 的生成能力与符号求解器的推理能力铺平了道路，并为 LLM 增强的测试用例生成开辟了新机遇。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
