AutoFraming: Synthesizing Dynamic Frames of C Code with LLMs

📄 arXiv: 2610.29046v1 📥 PDF

作者: Han Zhou, Yu Luo, Dianxiang Xu

分类: cs.AI

发布日期: 2026-10-21

备注: 12 pages, 1 figure, 6 tables

💡 一句话要点

提出AutoFraming以解决C代码中帧条件合成不足的问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 C代码合成 帧条件 形式规范 代码属性图 软件验证 程序分析

📋 核心要点

  1. 现有方法主要关注功能合约和循环不变式，忽视了帧条件的合成，导致形式规范不完整。
  2. 本文提出了一种基于LLM的方法，通过分析代码属性图提取帧相关信息，指导LLM生成帧条件。
  3. 在84个ACSL合规函数的基准测试中，成功合成92.9%的无错误帧规范，显著提升了合成性能。

📝 摘要（中文）

大型语言模型（LLMs）在从源代码合成形式规范方面展现出显著潜力。然而，现有方法主要集中于功能合约和循环不变式，忽视了帧条件的合成。帧条件指定了在执行过程中可能或不可能被修改的内存位置，是形式规范的重要组成部分。为了解决这一局限性，本文提出了一种基于LLM的方法，从C代码中合成ACSL帧规范和功能合约。该方法分析代码属性图（CPGs），提取与帧相关的信息，并利用这些信息指导LLM生成准确的帧条件。实验结果表明，该方法在84个来自非平凡真实系统的ACSL合规函数的基准测试中，成功合成了92.9%的无错误帧规范，相较于现有技术提高了179%。

🔬 方法详解

问题定义：本文旨在解决现有方法在合成C代码帧条件方面的不足，现有技术主要集中于功能合约和循环不变式，导致帧条件的缺失，从而影响形式规范的完整性。

核心思路：提出一种基于大型语言模型的合成方法，通过分析代码属性图（CPGs）提取与帧条件相关的信息，利用这些信息指导LLM生成准确的帧条件，从而提升合成的准确性和有效性。

技术框架：整体架构包括三个主要模块：首先，分析输入的C代码生成代码属性图；其次，从图中提取帧相关信息；最后，利用提取的信息指导LLM生成帧条件。

关键创新：最重要的技术创新在于结合代码属性图分析与LLM生成，能够有效提取帧条件所需的信息，显著提高了帧条件合成的准确性，与现有方法相比具有本质的区别。

关键设计：在参数设置上，选择了适合的图分析算法以确保信息提取的准确性，同时设计了损失函数以优化LLM生成的帧条件的质量，确保生成的帧条件符合ACSL规范。

🖼️ 关键图片

fig_0

📊 实验亮点

实验结果显示，在84个ACSL合规函数的基准测试中，成功合成92.9%的无错误帧规范，相较于现有技术提高了179%。在另一个包含51个函数的基准测试中，成功率从80.4%提升至96.1%。此外，作为辅助组件集成到现有LLM基础的ACSL合成框架中，性能提升可达61.9%。

🎯 应用场景

该研究的潜在应用领域包括软件验证、程序分析和自动化测试等。通过提高C代码中帧条件的合成能力，可以增强软件的可靠性和安全性，促进形式化验证技术的广泛应用，具有重要的实际价值和未来影响。

📄 摘要（原文）

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%.