💻 computer science

Array-Carrying Symbolic Execution for Function Contract Generation

本文提出了一种在 LLVM 中实现并集成至 Frama-C 平台的新型符号执行框架，通过携带数组连续段的不变式和分配信息，有效解决了含数组操作函数的契约生成难题，其实验结果表明该方法在处理此类函数方面优于现有方案。

原作者： Weijie Lu, Jingyu Ke, Hongfei Fu, Zhouyue Sun, Yi Zhou, Guoqiang Li, Haokun Li

发布于 2026-03-02

📖 1 分钟阅读☕ 轻松阅读

原作者： Weijie Lu, Jingyu Ke, Hongfei Fu, Zhouyue Sun, Yi Zhou, Guoqiang Li, Haokun Li

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这篇论文介绍了一种名为**“数组携带式符号执行”**（Array-Carrying Symbolic Execution）的新技术，旨在自动为计算机程序中的函数生成“使用说明书”（即函数契约）。

为了让你轻松理解，我们可以把编写程序想象成管理一个巨大的图书馆，而这篇论文解决的是如何给图书馆里的特定书架区域（数组）写一份精准的管理日志。

1. 核心问题：为什么需要“使用说明书”？

在软件开发中，一个函数就像一个黑盒子。你给它输入一些数据，它吐出来一些结果。

传统做法：程序员手动写注释，比如“输入必须是正数”、“输出是排序后的列表”。但这很容易出错，或者写得太模糊。
目标：我们希望电脑能自动分析代码，生成一份精准的合同（Contract），告诉别人：
- 输入要求（Precondition）：比如“书架上至少得有一本书”。
- 输出保证（Postcondition）：比如“如果找到了书，就返回它的位置；如果没找到，就返回 0"。
- 修改记录（Assigns）：比如“我只动过第 1 到第 10 页的书，其他书没变”。

难点在哪里？
当程序处理数组（比如一排连续的书架）时，情况变得很复杂。

想象一下，你有一排书架（数组），程序可能会循环检查每一本书。
如果程序在中间某本书找到了目标就停下来（break），或者检查完所有书都没找到才停下来。
现有的工具往往只能看到“我检查了书”，但说不清楚“我具体检查了哪几本”或者“剩下的书有没有被改动”。它们就像是一个近视眼，只能看到大概，看不清细节。

2. 我们的解决方案：带着“记忆”的导游

这篇论文提出了一种新方法，就像给程序执行过程配备了一位带着详细地图和记忆功能的导游。

核心比喻：导游与“连续书架”

想象你正在参观一个巨大的图书馆（程序），导游（我们的新框架）手里拿着一本特殊的日志本。

普通导游（旧方法）：
- 走到书架前，说：“我检查了书。”
- 走到另一排，说：“我改了书。”
- 问题：如果你问“你具体改了哪几本？”，导游可能说“大概吧，反正就是那一堆”。这不够精确，无法生成严谨的合同。
我们的导游（新方法 - 数组携带式符号执行）：
- 携带记忆（Carrying Invariants）：导游不仅记录“我在哪”，还随身携带着关于连续书架的完整记忆。
- 处理“连续段”：当程序检查一排书（数组段）时，导游会标记：“从第 1 本到第 5 本，我确认它们都是红色的；第 6 本我还没看。”
- 处理“分叉路口”（路径合并）：
  - 如果程序遇到一个 if 判断（比如“如果书是红色的就停下”），路会分叉。
  - 旧方法可能会把两条路的信息混在一起，导致信息丢失（“书可能是红的，也可能是蓝的”）。
  - 我们的导游会保留两条路各自的记忆，最后生成一份**“或者...或者..."**的合同：
    - 情况 A：如果在第 3 本停下了，那么前 3 本是红色的，第 3 本是目标。
    - 情况 B：如果走完了所有书，那么所有书都是红色的。
- 合并与拆分（Merge/Split）：
  - 如果程序先处理了前 4 本书，又处理了剩下的书。导游会把这两段无缝拼接起来，告诉你：“整个书架（从第 1 本到第 N 本）都被处理过了”。

3. 具体是怎么工作的？（三步走）

出发（初始化）：
导游拿到程序的“地图”（代码），在起点准备好。如果输入要求是“书架至少有 1 本书”，导游就记下来。
行走与记录（符号执行）：
导游开始模拟程序的每一步。
- 遇到循环（比如“检查每一本书”）：导游不会真的把书一本本翻（那样太慢了），而是调用一个**“预言家插件”**（外部不变式生成器）。
- 预言家告诉导游：“在这个循环里，前 i 本书肯定都是 0 号（没找到目标），或者在第 i 本找到了。”
- 导游把这些**“连续段的规则”（比如 data[0...i] 都是 0）记在日志本上，并带着它们**继续往前走。
生成合同（总结）：
当程序结束时，导游把一路上所有的记忆拼凑起来：
- 输入：必须满足什么条件？
- 输出：最终状态是什么？（比如：如果找到了，返回 1；没找到，返回 0）。
- 修改：哪些书被移动了？（比如：只修改了 rr[0...n] 这部分）。

4. 为什么这很厉害？（实验结果）

作者把这个导游（原型系统）放在了一个真实的图书馆（LLVM 编译器平台）里测试。

对比对象：他们拿它和目前最先进的工具（AutoDeduct）比。
结果：
- 旧工具：面对复杂的“找书”或“批量处理书”的任务，经常晕头转向，要么生成不出说明书，要么说明书太模糊，无法通过验证。
- 新导游：成功为68 个复杂程序生成了精准的说明书，而旧工具只成功了10 个。
- 速度：新导游不仅更准，还快 17 倍！因为它不需要把书一本本翻，而是直接看“连续段”的规律。

5. 总结与局限

一句话总结：
这项技术就像给程序分析员装上了**“透视眼”和“超级记忆力”，让它们能精准地描述程序在处理一排排连续数据**（数组）时到底做了什么，从而自动生成可靠的“使用说明书”。

局限性（导游也会累）：
目前的导游还不太擅长处理极其复杂的迷宫（比如递归的链表、二叉树等指针结构），它主要擅长处理整齐排列的书架（连续数组）。但这已经解决了目前软件验证中最大的痛点之一。

实际意义：
有了这个，未来的软件会更安全、更可靠。就像给每个函数都配了一份自动生成的、经过严格验证的说明书，程序员再也不用担心“这个函数到底改了哪些数据”这种让人头疼的问题了。

这是一篇关于**“面向函数契约生成的数组承载符号执行”（Array-Carrying Symbolic Execution for Function Contract Generation）**的论文技术总结。该研究由上海交通大学和北京大学的团队完成，旨在解决包含数组操作的程序自动化生成函数契约（Function Contracts）的难题。

以下是该论文的详细技术总结：

1. 研究背景与问题 (Problem)

核心问题：函数契约生成是程序分析中的经典问题，旨在自动化地推断函数的输入 - 输出关系。契约通常包括前置条件 (Preconditions)、后置条件 (Postconditions) 和 分配信息 (Assigns)（即函数执行期间修改了哪些内存变量或段）。
具体挑战：在涉及数组操作的程序中，现有的方法在处理**连续数组段（contiguous array segments）**的不变量推断和分配信息生成时面临巨大挑战。
- 现有抽象解释方法难以保留路径敏感的析取循环退出信息并转化为精确的合并数组段分配信息。
- 基于模型检查/SMT 的方法通常针对特定断言进行验证，难以生成通用的、可重用的函数级契约。
- 大语言模型（LLM）容易产生幻觉，且缺乏严格的逻辑保证。
- 现有的符号执行工具（如 KLEE, Clang Static Analyzer）通常缺乏对连续数组区域进行关系推理或归纳不变量推断的能力，往往只能处理单个元素或局部约束。

2. 方法论 (Methodology)

作者提出了一种新颖的符号执行框架，其核心创新在于**“承载”（Carrying）**不变量和连续数组段信息。

2.1 核心架构

混合执行策略：框架结合了外部不变量生成器（Invariant Generators）与符号执行引擎。
- 外部生成器：利用基于 Farkas 引理的仿射/线性不变量生成器（StInGX 风格）以及针对搜索、最大/最小值循环的特定模式生成器，生成循环不变量和摘要。
- 符号执行引擎：在 LLVM 平台上实现，负责沿着程序语句传播这些不变量，并处理数组段的分裂、合并和析取。

2.2 关键技术细节

数组段的表示与处理：
- 定义**连续数组段（Contiguous Array Segments）**为三元组 $\langle \text{起始地址}, \text{长度}, \text{内容摘要} \rangle$ 。
- 内容摘要 (Content Summary)：
  - 直接索引不变量：当数组内容可表示为索引的函数时（如 $arr[i] = i+2$），使用占位符变量表示。
  - 聚合抽象：支持求和、最大值等归约操作，将其作为一等公民的算术表达式处理。
  - 量化约束：对于复杂的循环不变量（如 $\forall k \in [0, i), arr[k] = 0$ ），以逻辑语句形式存储在路径条件中。
数组段的分裂与合并 (Splitting & Merging)：
- 分裂：当写操作发生在数组段内部时，将原段分裂为前缀和后缀段，并传播不变量。
- 合并：在循环分析或写操作后，如果相邻段的内容摘要在语法上等价，则将其合并为一个大段。这对于生成精确的 assigns 子句至关重要（例如将两个循环修改的段合并为一个整体段）。
路径敏感与析取处理：
- 框架能够处理循环的不同退出路径（例如：正常退出 vs. 通过 break 提前退出），保持这些路径的析取不变量，并在后续执行中携带这些信息，从而生成精确的后置条件。
实现细节：
- 基于 LLVM 和 Clang 前端实现（约 19,000 行 C++）。
- 集成 ACSL (ANSI/ISO C Specification Language) 格式。
- 与 Frama-C 验证平台集成，生成的契约可被 Frama-C 的 WP 插件自动验证。

3. 主要贡献 (Key Contributions)

带不变量的符号执行框架：设计了一种能够接收外部生成的数值和数组不变量，并在符号执行过程中沿程序语句传播的框架。这使得框架能够利用循环不变量生成通用属性的函数契约，并为后续循环分析提供紧密的前置条件。
精细化的连续数组段处理：
- 实现了数组段的析取（处理不同执行路径/循环退出模式）。
- 实现了数组段的合并与分裂，从而能够精确追踪数组段上的信息，推导出涉及数组段的整体契约。
原型实现与验证集成：在 LLVM 平台上实现了原型，并集成了 ACSL 和 Frama-C，使得生成的契约不仅能描述程序行为，还能被外部验证器验证其正确性。
实验验证：在广泛的基准测试（包括 SyGuS, OOPSLA-13, SV-Comp 以及真实的 openHiTLS 加密库）上进行了评估。

4. 实验结果 (Results)

评估对象：与最先进的工具链 AutoDeduct 进行对比（未对比 LLM，因方法论不同且存在基准污染风险）。
数据集：282 个 C 程序，涵盖微基准、复杂逻辑模式及真实的加密库函数。
精度 (Precision)：
- 在 281 个测试用例中，作者的工具成功生成了 68 个可被 Frama-C 完全验证的契约。
- 相比之下，AutoDeduct 仅能完全验证 10 个。
- 特别是在处理涉及复杂数组段和指针算术的 openHiTLS 库函数时，作者的工具表现优异，而 AutoDeduct 几乎全部失败（无法生成可验证的循环不变量）。
效率 (Efficiency)：
- 平均运行时间：作者工具为 0.148 秒，AutoDeduct 为 2.703 秒。
- 速度提升约 17.1 倍。这得益于轻量级的符号执行引擎，避免了循环展开和显式枚举所有数组元素。
局限性：
- 目前主要支持简单的指针算术（基址 + 偏移），无法处理递归指针结构（如链表、二叉树）。
- 对某些位运算和嵌套循环的支持有限。

5. 意义与结论 (Significance)

填补空白：该工作解决了现有符号执行和程序分析工具在处理带数组操作的函数契约生成方面的短板，特别是针对连续内存段的推理。
实用价值：生成的契约不仅包含前置/后置条件，还精确描述了内存修改范围（Assigns），这对于模块化验证和大型软件系统的自动化分析至关重要。
验证可靠性：通过集成 Frama-C，证明了生成的契约在逻辑上是sound的，克服了 LLM 生成代码契约时常见的幻觉问题。
未来方向：计划进一步改进数组段分裂合并中的不变量处理，扩展跨过程分析能力，并更深层次地集成现有的不变量生成方法。

总结：这篇论文提出了一种强大的、基于符号执行的自动化方法，通过创新性地“承载”和“操作”连续数组段信息，显著提升了复杂数组操作程序契约生成的精度和效率，为形式化验证领域提供了重要的工具支持。