静态分析代码质量开发工具【免费下载链接】inferA static analyzer for Java, C, C, and Objective-C项目地址https://gitcode.com/gh_mirrors/infer/infer点击查看免费下载分离逻辑Separation Logic与双溯因Bi-abduction是 Facebook Infer 静态分析器实现规模化推理的理论基石前者用一条框架规则把对程序行为的推理切分成可以独立组合的内存局部小块后者则让分析器在不要求程序员手写全部前置/后置条件的前提下自动推断出每个过程procedure的前置与后置规格。本文以 Infer 1.3.0 版本文档为骨架结合本仓库中的源码实现如 PulseAbductiveDomain.mli 等系统讲解分离合取、Hoare 三元组、框架规则、antiframe/frame 的推导过程以及它们如何支撑 Infer 的规模化分析与增量分析能力。读完本文你将理解 Infer为什么能对大型代码库做自动化验证的根本机理并能看懂其分析结果与后续技术论文。分离逻辑面向内存变更的推理框架分离逻辑是一种特殊的数理逻辑其设计目标就是便于对**计算机内存的变更mutation进行推理。它的核心思想是把对整段内存的推理切分成一个个对应局部内存操作的小块推理完成后再把这些小块组合compose**起来。正是这种先局部、后组合的机制使分析具备了可扩展性——这也是它被选作 Infer 理论内核的原因。分离合取*把堆切成不相交的 heaplet分离逻辑建立在一种称为**分离合取separating conjunction**的逻辑连接词之上记作*读作and separately并且分开地。分离逻辑公式的解释对象是程序分配的堆heap。公式A * B对某一块程序堆称为一个 heaplet成立当且仅当这块堆可以被划分成两个子 heaplet分别由A和B描述。例如公式x ↦ y * y ↦ x可读作x 指向 y并且分开地y 指向 x。该公式精确地描述了恰好两个已分配的内存单元第一个单元分配在指针x所表示的地址上其内容是y的值第二个单元分配在指针y所表示的地址上其内容是x的值。关键之处在于因为*强制要求两个部分分离所以这两个单元必然位于内存中两个不同的区域。换句话说*断言了x与y不持有相同的值——即这两个指针不互为别名not aliased。上面公式所定义的 heaplet 划分可以直观地看作左侧x与y互相指向的环形结构等价于右侧两个独立单向指向x ↦ y与y ↦ x的分离合取。分离合取最重要的一点是它与内存变更的配合方式对程序命令的推理往往就是就地更新某个*-合取项这恰好模拟了 RAM 上就地更新的操作语义。Hoare 三元组与小规格分离逻辑使用形如下式的Hoare 三元组Hoare triple作为程序行为的抽象规格{ pre } prog { post }其中pre是前置条件preconditionprog是程序片段post是后置条件postcondition。例如我们可以为关闭作为参数传入的资源的方法写下如下规格{ r ↦ open } closeResource(r) { r ↦ closed } (spec)这份规格只提及一块状态r ↦ open与r ↦ closed这正是一种小规格small specification它描述closeResource()的工作方式时只说自己直接碰触的那部分状态完全不涉及其他内存。现在假设我们有两个资源r₁和r₂当前状态由r₁ ↦ open * r₂ ↦ open描述然后我们关闭第一个。按操作语义我们应当就地更新内存把r₂ ↦ open原样留下{ r₁ ↦ open * r₂ ↦ open } closeResource(r₁) { r₁ ↦ closed * r₂ ↦ open } (use)这里发生的事正是小规格(spec)描述了closeResource()的行为而(use)用这份规格就地更新了一个更大的前置条件。框架规则局部推理的钥匙上述从小到大的规格推导是一个一般模式的特例。分离逻辑中有这样一条规则允许从较小规格推出较大规格{ pre } prog { post } ───────────────────────────── { pre * frame } prog { post * frame }从(spec)到(use)的推导只需取pre为r₁ ↦ openpost为r₁ ↦ closedframe为r₂ ↦ open这条规则被称为分离逻辑的框架规则frame rule。它的名字来自人工智能领域的经典难题框架问题frame problem一般而言frame描述的是保持不变的那部分状态。这个术语借用了动画的类比——背景场景frame始终不变而场景中的对象与角色在变化。框架规则是分离逻辑中**局部推理local reasoning**原则的关键推理与规格应当只聚焦于程序真正访问的资源称为 footprint足迹而不必提及那些不变的部分。双溯因Bi-abduction自动化局部推理双溯因是分离逻辑上的一种逻辑推理形式它把局部推理的上述关键思想自动化。从蕴含到 bi-abduction 问题通常逻辑处理的是有效性或蕴含entailment语句例如A ⊢ B它表示A蕴含B。Infer 在其内部定理证明器逐语句运行程序时使用的正是这一推理问题的推广形式A * ?antiframe ⊢ B * ?frame这个形式被称为bi-abduction双溯因。这里的问题是让定理证明器自行发现一对 frame框架与 antiframe反框架公式使得上述蕴含成立。为什么能规模化把整体分析拆成独立小分析对大型程序的全局分析在计算上通常不可行。而 bi-abduction 把一个大型程序的整体分析分解为对其各个过程的相互独立的小分析。这给 Infer 带来了两个直接能力可扩展性分析成本独立于被分析代码的总体规模增量分析incremental analysis由于分析被拆成相互独立的小块当代码发生变更后再次分析整个程序时未变更部分的既有分析结果可以直接复用只需重新分析变更部分。这对于把静态分析工具如 Infer集成进日常开发流程极具价值。函数调用处的 bi-abduction为了把全局分析分解为相互独立的小分析先看分离逻辑中如何分析一次函数调用。假设我们已有函数f()的规格{ pre_f } f() { post_f }并且通过分析调用者我们算出了在调用f之前公式CallingState成立。那么要使用f的规格下面的蕴含必须成立CallingState ⊢ pre_f (Function Call)正是基于这一点bi-abduction 在过程调用点被用于两个目的发现缺失的状态即让上述蕴含成立、使分析得以继续所需的 antiframe以及发现过程保持不变的状态即 frame。一个完整的推导示例从裸代码到整体规格假设有如下没有任何整体规格的裸代码closeResource(r1); closeResource(r2)我们要演示如何为它发现一份 pre/post 规格。第一步第一个语句。结合上面的(spec)分析第一个语句时人可能会想如果前置条件里有r1 ↦ open就好了。技术上我们提出一个 bi-abduction 问题emp * ?antiframe ⊢ r1 ↦ open * ?frame其中emp表示空状态empty state它记录着一开始我们什么都不假定。这个问题很容易填满取antiframe r1 ↦ open、frame emp得到平凡成立的蕴含emp * r1 ↦ open ⊢ r1 ↦ open * emp应用逻辑规则可等价改写为r1 ↦ open ⊢ r1 ↦ open注意这恰好满足(Function Call)对正确发起调用的要求。于是我们把该信息加入pre同时把(spec)中第一个语句的post信息也记录下来{ r1 ↦ open } closeResource(r1) { r1 ↦ closed } closeResource(r2)第二步第二个语句。现在处理第二个语句。上面部分符号执行轨迹中的前置条件r1 ↦ closed并不包含closeResource(r2)所需的信息因此我们补上r2 ↦ open放入pre并把这个断言一路回传thread back到开头{ r1 ↦ open * r2 ↦ open } closeResource(r1) { r1 ↦ closed * r2 ↦ open } closeResource(r2)需要回传的这部分信息正是第二个 bi-abduction 问题中的 antiframe 部分r1 ↦ closed * ?antiframe ⊢ r2 ↦ open * ?frame其解取antiframe r2 ↦ open、frame r1 ↦ closed。注意antiframe 恰恰是前置条件中缺失的那部分信息有了它closeResource(r2)才能继续而另一方面framer1 ↦ closed是closeResource(r2)不会改变的那部分状态按框架规则可以把它一路贯穿到整体后置条件{ r1 ↦ open * r2 ↦ open } closeResource(r1) { r1 ↦ closed * r2 ↦ open } closeResource(r2) { r1 ↦ closed * r2 ↦ closed }于是我们通过对代码做符号执行沿途用 bi-abduction 发现前置条件对 antiframe 的溯因以及未被触碰的内存部分frame就为这段代码得到了完整的 pre 与 post 规格。自动化程度与意义一般而言只要知道了代码底层原语primitive的规格bi-abduction 就能从裸代码推断出 pre/post 规格——人类无需为所有过程手写前置条件和后置条件这正是 Infer 高度自动化的关键也是 Infer 的工作原理、可扩展性以及增量分析能力的共同基础。背景溯因与框架问题这里用到的逻辑术语来自人工智能与科学哲学哲学家查尔斯·皮尔士Charles Peirce提出了溯因推理abductive inference将其描述为支撑假设形成即猜测关于世界的什么东西可能是真的的机制是科学过程中最具创造性的部分。溯因与框架问题在 AI 中都备受关注。Infer 使用自动化形式的溯因来生成描述程序所触碰内存的前置条件即上面的 antiframe 部分使用框架推理来发现什么没被触碰随后用演绎推理从前置条件出发计算出描述程序效果的公式。某种意义上Infer 模拟了人类理解程序时的做法它溯因出程序需要什么再演绎出由此产生的结论。当推理出问题时Infer 就会报告一个潜在 bug。仓库中的实现佐证bi-abduction 如何落地上述描述相对于 Infer 的真实实现必然是简化的但仓库源码中处处可见这套理论的直接落地可以作为进一步研读的入口。Pulse 分析当代的 abductive 域当前 Infer 的主力分析器 Pulse 在 PulseAbductiveDomain.mli 中明确声明其域遵循 bi-abduction 的原则并引用论文Compositional Shape Analysis by Means of Bi-AbductionJACM, 2011作为依据该模块在 PulseBaseDomain 之上构建了abductive溯因式、值规范化的一层。其注释给出了非常直观的说明当从前置条件可达的内存位置发生第一次读操作时这意味着该内存位置最好在函数一开始就已分配操作才安全因此分析器溯因abduce出这一事实并把它加入前置条件除非已知该地址无效。模块中区分了PostDomain当前程序点之后的状态与PreDomain按 bi-abduction 风格推断出的程序点前置条件PreDomain的注释还指出理论上PreDomain应是Domain的倒格inverted lattice但由于实际从不 join 状态或检查蕴含两者合并为一。状态类型t同时携带post、pre与path_condition路径上对 pre 和 post 都成立的算术事实正是每个程序点同时维护前置与后置抽象状态这一 bi-abduction 工作方式的直接体现。其中的dealias_post函数注释以x |- z * y |- z应变为x |- z * y |- zz为新的抽象值为例说明替换别名位置字里行间仍是分离合取*的表述习惯。中间表示与旧分析中的分离逻辑痕迹在中间表示层Sil.mli 中某个抽象位置abstraction point的注释明确写道一个好地方应用抽象主要用于 biabduction 分析说明 bi-abduction 分析对 IR 上的抽象点设置有着特定需求。后端模块 Devirtualizer.ml 的resolve_method函数注释注明其灵感来自biabduction/Symexec.ml即早期 bi-abduction 符号执行器的方法解析逻辑。缓冲区越界分析 bufferoverrun/BiabductionProp.ml及对应 .mli继承了这个命名与思路在 Checker.ml 中BufferOverrunCheckerInferBO已被标记为UserFacingDeprecated弃用消息为Use Pulse instead这也印证了分离逻辑风格的检查器正在向 Pulse 这一新的 bi-abduction 风格分析迁移。在实验性教学材料 labs/README.md 中运行infer -- javac Leaks.java后报告的资源泄漏也明确注明这些报告来自基于分离逻辑的 biabduction 分析可作为理解该分析的入门演练。延伸阅读技术论文以下论文提供了 Infer 的部分技术背景以及在 Facebook 内部使用 Infer 的方式。其中关于推理的表述是精确但仍经过简化的论文之外还有大量未记录的工程决策再进一步你可以直接阅读 Infer 的源码Local Reasoning about Programs that Alter Data Structures—— 较早的分离逻辑论文推进了关于局部推理与框架规则的思想。Smallfoot: Modular Automatic Assertion Checking with Separation Logic—— 第一个分离逻辑验证工具引入了框架推理frame inference。A Local Shape Analysis Based on Separation Logic—— 分离逻辑与抽象解释的结合通过不动点计算推导循环不变式。Compositional Shape Analysis by Means of Bi-Abduction—— bi-abduction 的原始论文也是 PulseAbductiveDomain.mli 明确引用的理论依据。Moving Fast with Software Verification—— 关于 Facebook 内部使用 Infer 的方式。小结分离逻辑用分离合取*与框架规则把程序只影响一小块内存这一事实形式化使规格可以是局部的、可组合的bi-abduction 则以A * ?antiframe ⊢ B * ?frame的形式把发现缺失前提、发现不变框架自动化从而让 Infer 能自动从裸代码推断过程规格、按过程分解全局分析并支撑复用未变更部分分析结果的增量分析。这一整套机理正是理解 Infer 为什么能规模化地应用于大型真实代码库的钥匙——如果你想进一步验证可以打开 PulseAbductiveDomain.mli 看它在源码里如何把第一次读到前置条件可达的内存翻译成把该位置已分配这一事实溯因进前置条件。赞分享静态分析代码质量开发工具【免费下载链接】inferA static analyzer for Java, C, C, and Objective-C项目地址https://gitcode.com/gh_mirrors/infer/infer点击查看免费下载相关推荐Infer 静态分析器的理论基石分离逻辑与 Bi-abduction 推理Infer 静态分析器的理论基石分离逻辑与 Bi abduction 推理 导读 本文围绕 Facebook 开源静态分析器 Infer当前仓库 gh_mi静态分析代码质量开发工具分离逻辑与双消解Bi-abductionInfer 可扩展静态分析的理论基石分离逻辑与双消解Bi abductionInfer 可扩展静态分析的理论基石 output静态分析代码质量开发工具Infer 静态分析器深度解析Infer.SL、Infer.AI 与分离逻辑分析架构Infer 静态分析器深度解析Infer.SL、Infer.AI 与分离逻辑分析架构 本文以 Infer 官方文档 website/versioned_doc静态分析代码质量开发工具上一篇DiceBear HTTP API完全指南无需代码通过URL生成动态头像下一篇96种相机位如何实现精准视角控制Qwen-Image-Edit-2511多视角LoRA机制完整解析创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考