Llms synthesize accurate memory frame specifications for c code
AutoFraming: Synthesizing Dynamic Frames of C Code with LLMs
Artificial Intelligence
Summary
Programs often change certain pieces of memory while running, and it is important to know exactly which parts are affected. The authors found that prior tools focused on the program's function but ignored these memory changes. They developed a way to use large language models (LLMs) combined with code analysis to describe precisely what parts of memory a C program can modify. Their method works much better than previous ones, producing accurate memory change descriptions for many real-world code examples.
What this means in practice
- •For software verification engineers: Generate precise memory modification specifications for C functions to improve program correctness checks and automated verification.
- •For embedded systems developers: Obtain detailed frame conditions for safety-critical C code to support certification and reduce bugs related to unintended memory changes.
Authors
Han Zhou, Yu Luo, Dianxiang Xu
Abstract
Large language models (LLMs) have shown considerable promise in synthesizing formal specifications from source code. However, existing approaches primarily focus on functional contracts and loop invariants, while largely neglecting frame conditions, which specify the memory locations that may or may not be modified during execution and constitute an essential part of formal specifications. To address this limitation, we propose an LLM-based approach for synthesizing ACSL frame specifications alongside functional contracts from C code. Our approach analyzes code property graphs (CPGs) to extract frame-relevant information from the input code and leverages this information to guide the LLM in generating accurate frame conditions. The resulting specifications capture both region-separation constraints and data dependencies that govern variable modifications. Experimental results demonstrate the effectiveness of our approach. On a benchmark of 84 ACSL-compliant functions from non-trivial real-world systems, our method successfully synthesizes error-free frame specifications for 92.9% of the functions, representing a 179% relative improvement over state-of-the-art techniques. On a second benchmark consisting of 51 functions, the success rate increases from 80.4% to 96.1%. Furthermore, when integrated as an auxiliary component into existing LLM-based ACSL-synthesis frameworks, our approach improves frame-specification generation performance by up to 61.9%.