Python Symbolic Execution with LLM-powered Code Generation

符号执行是软件测试中的关键技术，它通过收集符号路径约束并使用SMT求解器解决约束来生成测试用例。符号执行已被证明有助于生成高覆盖率的测试用例，但它的局限性，例如解决路径约束的困难，阻止了它在软件测试中的广泛使用。此外，符号执行在应用于像Python这样的动态类型语言时遇到了许多困难，因为将灵活的Python语法转换为严格的求解器非常具有挑战性。 为了克服在Python中应用符号执行的主要挑战，我们提出了一个LLM增强的代理，LLM-Sym，它自动调用SMT求解器Z3来解决执行路径约束。基于一个入门级符号执行引擎，我们的LLM代理可以扩展支持具有复杂数据类型“列表”的程序。LLM-Sym的核心贡献是将复杂的Python路径约束转换为Z3代码。为了实现准确的路径到Z3的转换，我们设计了一个多步代码生成流水线，包括类型推断、检索和自我精化。我们的实验表明，LLM-Sym能够解决具有复杂控制流和列表数据结构的Leetcode问题的路径约束，这对于骨干符号执行引擎来说是不可能的。我们的方法为LLM的生成能力与符号求解器的推理能力的结合铺平了道路，并在LLM增强的测试用例生成方面开辟了新的机遇。

解决在Python中应用符号执行的困难，特别是对于复杂数据类型的支持，如列表（list）。

提出了一种基于LLM的代理工具LLM-Sym，将Python中的复杂路径约束转换为Z3代码，并使用Z3求解器解决约束。通过多步代码生成流水线实现了准确的路径到Z3代码的转换。

LLM-Sym能够解决具有复杂控制流和列表数据结构的Leetcode问题的路径约束，这是基础符号执行引擎无法实现的。该方法为LLM增强测试用例生成的可能性打开了新的机会。

最近的相关研究包括：1. "Exploring the Limits of Language Modeling for Code Generation" 2. "Neural Program Synthesis with Priority Queue Training"