选自TowardsDataScience，作者：Jesus Rodriguez

机器之心编译，参与：Geek AI、路

  • Infer 官网地址：https://fbinfer.com/

  • GitHub 地址：https://github.com/facebook/infer

不久前，一支来自 Facebook 的工程团队斩获了 ACM SIGPLAN POPL 最具影响力论文奖，这是机器学习研究社区最受关注的奖项之一。该团队获奖论文为「Compositional Shape Analysis by Means of Bi-abduction」，介绍了近年来我最喜欢的机器学习应用之一「Project Infer」背后的科学原理。Project Infer 的目标是：在移动应用程序发布之前检测其代码中的 bug，这样的技术似乎是科幻电影中的桥段。

移动应用程序中出现 bug 的代价往往很大。在移动应用程序被分发到数千台移动设备后再发现错误，对于任何开发者来说都是一场噩梦。传统的移动应用程序测试重点关注重建已知的场景，但是实际上还存在许多可能触发错误条件的代码组合，而它们是传统的测试方法无法检测到的。Project Infer 则会扫描移动应用程序的代码，并检测出可能的错误条件，最后由开发者复核。自从三年前该软件开源以来，Project Infer 就已经被 AWS、Spotify 及 Uber 等世界顶级公司所采用。

Project Infer 是如何工作的？

Project Infer 使用逻辑推理对软件程序可能出现的执行结果进行推理。任何大型的移动应用程序都可能包含数亿个可能触发错误条件的代码组合，这使得传统的代码分析例程无法扩展到所有可能的情况。Facebook 的 Infer 构建了关于应用程序的增量式知识，提高应用程序整个开发生命周期中的开发效率。

从顶层看，Facebook Infer 的工作流可以分成两个主要阶段：捕获和分析。而其生命周期也可被分成两个主要的部分：全局部分和差分部分。

在「捕获」阶段，Infer 使用编译命令将待分析的文件转换成其内部的中间语言。而「分析」阶段则会探索每个函数可能会触发哪些错误条件。如果 Infer 在分析某个方法或函数时遇到了某些错误，它将停止运行有错误的方法或函数，但将继续分析其它方法和函数。下面的动画演示了 Facebook Infer 在捕获和分析阶段的运行情况。

从程序执行的角度来看，Facebook 的 Infer 可以在两种模式下使用：全局模式和差分模式。当 Infer 分析给定项目中的所有文件时，Infer 将在全局工作流下运行。对于使用 Gradle 编译的项目，可使用下面的语法运行 Infer 的全局工作流：

infer run -- gradle build

在增量式构建的系统（在移动应用程序中很常见）中应用 Infer 时往往会使用差分工作流。在该场景下，我们首先需要运行 Infer 的「捕获」阶段，获得所有的编译命令，然后使用 –-reactive 参数来分析代码的变化。

gradle cleaninfer capture -- gradle buildedit some/File.java# make some changes to some/File.javainfer run --reactive -- gradle build

可以使用 InferTraceBugs 命令来研究 Infer 生成的报告。

infer run -- gradle buildinferTraceBugs

Project Infer 背后的科学原理

Facebook Infer 基于两种新颖的数学技术：分离逻辑（separation logic）和双向假说推理（bi-abduction）。

分离逻辑使 Infer 能够对应用程序存储小的、独立部分的推理进行分析，而不必在每一步都考虑整个内存。从数学上讲，分离逻辑对计算机内存的突变进行推理。分离逻辑的核心元素就是 * 操作，我们称其为分离合取（separating conjunction），读作「... 与... 分别成立」。例如，公式「x↦y∗y↦x」可以读作「x 指向 y 与 y 指向 x 分别成立」（「如果 x，那么 y」与「如果 y，那么 x」分别成立），这类似于内存指针的工作原理。大多数对于计算机函数的逻辑推理往往是通过适当地更新「* 合取」，从而模仿 RAM 中的就地操作更新来运行的，而分离逻辑为对计算机程序的推理提供了基础。

双向假说推理是分离逻辑的一种逻辑推理形式，它将局部推理的关键思想自动化。对于 Infer 来说，双向假说推理可以被视为一种逻辑推理技术，它使该框架能够发现应用程序代码中独立部分的行为特性。双向假说推理将假说推理作为「frame 问题」的一种反演：它同时对 anti-frame（缺失部分状态）和 frame（没有被某个操作触及的部分状态）进行推断，它是一种新的过程间分析算法的基础。

从数学上来说，双向假说推理问题是用下面的语法表述的：A∗?antiframe⊢B∗?frame。其目的是找到一对使得蕴含语句成立的 frame 和 anti-frame。在 Facebook Infer 环境下，双向假说推理为从原始代码中推断出「前缀/后缀」规范提供了一种方法（只要我们知道底层代码的原语规范）。

Facebook Infer 是不同机器学习领域多年研究成果的集大成者。这些工作产出了一系列重要的研究论文，它们为推理逻辑和机器学习的其它领域做出了突破性贡献。下面，本文将回顾其中的一些重要论文：

  • Compositional Shape Analysis by means of Bi-Abduction：这篇论文获得了著名的 ACM SIGPLAN POPL 最具影响力论文奖，介绍了组合形态分析的原则。基于双向假说推理的组合形态分析是一种独立于程序调用者进行过程分析的分析方式。组合形态分析将传统的形态分析扩展到了计算机程序分析任务中。其思路是通过有效地分析各个独立的部分并对缺失部分进行推断来分析程序。

  • A Local Shape Analysis Based on Separation Logic：该论文介绍了分离逻辑这一描述程序分析的机制。该论文阐述的主要观点是，我们能够在并不理解整个内存堆（heap）、只掌握其中一些独立单元的情况下，对内存堆中的数据结构进行分析。例如，我们在不分析整个堆的情况下推断出某些特定的单元生成了一个链表。

  • Smallfoot: Modular Automatic Assertion Checking with Separation Logic：该论文提出了 Smallfoot 技术，它是 Facebook Infer 的前身，将分离逻辑用于对软件程序中轻量级数据结构进行推断。

  • AL: A new declarative language for detecting bugs with Infer：AL 为 Facebook Infer 提供了重要的可扩展性模型。从概念上讲，AL 使任何工程师可在不了解 Infer 内部工作原理的情况下设计出新的检查程序。AL 是一种声明式语言，它支持以简单的交互方式对语法树进行推理。

  • Moving Fast with Software Verification：最后这篇论文介绍了 Facebook 如何在内部使用 Project Infer。该论文介绍了 Facebook 工程师如何将 Infer 集成到他们的开发流程中，从而为 Instagram、Facebook Messenger 以及 Facebook 在 Android 和 iOS 平台上的移动应用程序提供静态分析支持。

Facebook Infer 是最早发布、最实用的将机器学习用于软件编程的应用之一。尽管到目前为止，Infer 的使用对象还局限于移动应用程序，但是它的许多设计原则适用于通用应用程序。说不定，未来会出现一版用于机器学习程序的 Infer 呢！

原文链接：https://towardsdatascience.com/machine-learning-for-detecting-code-bugs-a79f37f144b7

声明：本文来自机器之心，版权归作者所有。文章内容仅代表作者独立观点，不代表安全内参立场，转载目的在于传递更多信息。如有侵权，请联系 anquanneican@163.com。