Can Large Language Models Simulate Symbolic Execution Output Like KLEE?
Rong Feng, Vanisha Gupta, Vivek Patel, Viroopaksh Reddy Ernampati, Suman Saha
符号执行有助于检查程序,探索基于符号输入的不同路径。 像KLEE这样的工具是常用的,因为它们可以自动检测bug并创建测试用例。 但是,KLEE最大的问题之一是,当程序有很多分支路径时,它的速度会有多慢 - 它通常变得过于资源繁重,无法运行在大型或复杂的代码上。 在这个项目中,我们想看看像GPT-4o这样的大型语言模型是否可以模拟KLEE生成的输出类型。 这个想法是探索LLM是否可以有一天取代符号执行的部分,以节省时间和资源。 一个具体目标是让GPT-4o识别程序中受约束的路径,这是具有最大象征意义条件的执行路径。 这些路径尤其重要,因为它们通常代表难以测试的边缘案例,并且更有可能包含深度错误。 然而,弄清楚这一点通常需要完全运行的KLEE,这可能是昂贵的。 因此,我们测试了GPT-4o是否可以使用100 C程序的数据集预测KLEE输出和最复杂的路径。 我们的结果显示,在生成类似KLEE的输出和识别最受限的路径方面,准确率约为20%。 虽然不是高度准确,但这项早期工作有助于显示当前LLM在模拟符号执行时可以做什么和不能做什么。
Symbolic execution helps check programs by exploring different paths based on symbolic inputs. Tools like KLEE are commonly used because they can automatically detect bugs and create test cases. But one of KLEE's biggest issues is how slow it can get when programs have lots of branching paths-it often becomes too resource-heavy to run on large or complex code. In this project, we wanted to see if a large language model like GPT-4o could simulate the kinds of outputs that KLEE generates. The idea...