Can Large Language Models Simulate Symbolic Execution Output Like KLEE?

TL;DR

This paper investigates whether GPT-4o can simulate KLEE's symbolic execution outputs, focusing on identifying the most constrained execution path in C programs, aiming to reduce computational costs.

Contribution

It demonstrates the potential and limitations of large language models in approximating symbolic execution tasks, a novel exploration in program analysis.

Findings

GPT-4o achieved about 20% accuracy in output prediction.

The model could partially identify the most constrained path.

Results highlight current LLM capabilities and challenges in symbolic execution simulation.

Abstract

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 was to explore whether LLMs could one day replace parts of symbolic execution to save time and resources. One specific goal was to have GPT-4o identify the most constrained path in a program, this is the execution path with the most symbolic conditions. These paths are especially important because they often represent edge cases that are harder to test and more likely to contain deep bugs. However, figuring this out usually requires fully running KLEE, which can be expensive. So, we tested whether GPT-4o could predict the KLEE outputs and the most complex path using a dataset of 100 C programs. Our results showed about 20% accuracy in generating KLEE-like outputs and identifying the most constrained path. While not highly accurate, this early work helps show what current LLMs can and can't do when it comes to simulating symbolic execution.