Can Large Language Models Solve Path Constraints in Symbolic Execution?

TL;DR

This paper explores using large language models to solve path constraints in symbolic execution, demonstrating their potential to generate test cases and classify paths, thereby overcoming limitations of traditional SMT-based methods.

Contribution

It introduces an empirical evaluation of LLMs for path constraint solving in symbolic execution, including new benchmarks and pipelines for test case generation and path classification.

Findings

LLMs can solve path constraints with 60% accuracy in test case generation.

LLMs improve coverage in real-world software where traditional tools struggle.

State-of-the-art LLMs show promise for extending symbolic execution capabilities.

Abstract

Symbolic execution is an important software analysis technique which benefits downstream tasks such as software testing and debugging. However, several limitations hinder symbolic execution from application on real-world software. One of the limitations is the inability to solve diverse execution path constraints: traditional symbolic execution based on SMT solvers is difficult to handle execution paths with complex data structures or external API calls. In this paper, we focus on investigating the possibility of adopting large language models (LLM) for path constraint solving instead of traditional solver-based techniques in symbolic execution. We conduct an empirical study to evaluate the ability of LLMs in two types of path constraint solving: generating test inputs to facilitate an execution path, and determining whether a given execution path can be satisfied without triggering any bugs. We build new evaluation pipelines and benchmarks for two tasks: test case generation and path classification, which include data sources from both competition-level programs and real-world repositories. Our experiment results show that state-of-the-art LLMs are able to solve path constraints in both generation and classification tasks, with 60% of generated test cases that accurately cover the given execution path. Moreover, LLMs are capable of improving test coverage by covering execution paths in real-world repositories where traditional symbolic execution tools cannot be applied. These findings highlight the possibility of extending symbolic execution techniques with LLMs in the future to improve the ability and generalizability of symbolic execution.