Facebook 代码分析工具 infer 静态代码检查工具

Question

今天，我们开源了一个名叫 Facebook Infer 的静态程序分析库，该库用于在程序分发之前定位代码 bug。静态分析器是一个不需要运行代码就可以准确地找出代码 bug 的自动化工具。它是传统的动态测试的补充，传统的动态测试允许每次只运行一个独立的代码单元来检测程序的正确性，静态分析则允许一次性检测多个、甚至所有代码。

Facebook Infer 使用数学逻辑来推理程序的运行，当在查找程序时来推测程序员在代码中所要做的操作。我们内部使用 Facebook Infer 来分析 facebook 的 Android 和 iOS 应用，例如 facebook messagers, Instagram 等等。现在，这个分析器能够发现空指针、内存泄漏等能够使应用奔溃的大量代码 bug.

每个月我们都会修复使用 Facebook Infer 发现的数百个潜在的 bug，从而避免这些 bug 提交到我们的代码仓库。这些成果大大减少了我们研发人员查找 bug 的时间，也使得我们的用户能够使用更高质量的应用。

动机

facebook 喜欢在产品完成之后尽可能快的分发出去，而不是在一连串冗长的手动测试之后。这种方式在移动应用端的风险比 web 端更大。当一个 web 的 bug 被发现时，我们可以马上修复并且提交到服务器上。

但是为了修复移动应用的 bug,我们需要像应用市场更新应用安装文件。因此，这也使得在将应用分发给用户之前发现 bug 变得更有价值。结合静态分析和自动测试能够帮助 Facebook 在将产品分发出去之前找到 crashed 和内存泄漏，这使得我们的应用端应用的研发更为有效、迅速。

为了符合开发者的工作流程，当开发者提交了代码后 Facebook Infer 增量地执行以分析代码的修改。当发现潜在 bug 时分析器会自动地在代码中添加评论。这些 bug 报告都是高质量的，因此我们可以帮助开发者快速的找到问题所在。在最近的几个月中，bug 的修复率已经高达 80%,对于一个自动化工具来说那是相当高了。

在现在的开发模式中，我们运行分析器来分析我们的 Android 和 iOS 代码，但是我们还可以做更多的事。Facebook Infer 还可以分析 c 语言项目和 java 代码，我们计划在未来扩展它的兼容性。有你的帮助，我们希望 Facebook Infer 能够有更广阔的用途。

核心技术 : 逻辑分离和 bi-abduction

facebook infer 使用逻辑来推理程序的执行,但是通过这种方式来推理上百万行代码量的应用时会变得非常困难。从理论上讲，需要检查的代码数量会多过预计的数量。此外，在 Facebook 我们的代码并不是手工修复代码，而是一个不断进化的系统，这个系统被很多开发者频繁的更新。一天之内大量代码的修改在我们的移动开发中并不常见。因此这个代码分析器的需求变得更有挑战，因为我们期望一个能够快速检查代码修改的工具，这个时间应该在 10 分钟之内。这样的规模和速度需要更高级的数学模型，Facebook Infer 使用了两种技术: 逻辑分离和 bi-abduction。

逻辑分离是使 Facebook Infer 分析能够推断出应用存储的独立小部分的一种理论，从而不用考虑每一步存储的完整性。因为考虑每一步的存储完整性对当今的大型可寻址虚拟内存处理器来说是一个很蛋疼的事。

Bi-abduction 是一种逻辑推理技巧，可以使 Facebook Infer 挖掘到应用代码独立部分的行为特性。在其运行时把这些特性存储下来之后，Facebook 只需要分析软件中发生改变的部分，其他的部分可以直接套用先前的分析结果。

结合这几种方法，我们的分析器能够在数分钟之内在上百万行代码中找到被修改的代码中存在的复杂问题。

历史 : 从代码检查理论到为十多亿人服务的蜕变

软件的自动检查在计算机科学社区是一个长期依赖的目标。Facebook Infer 在这个领域构建了一个基本实现， 包含霍尔逻辑和抽象解释。在加入 facebook 之前，我们参与到了其他基础设施的开发工作，“逻辑分离”作为能够实现软件自动检查的结果出现在人们的视野中。

逻辑分离是在计算机科学领域的一个重大突破-一种新的数学逻辑被用于描述计算机内存的变化（类似于布尔逻辑用来描述电路）。我们专注于将这个理论运用和自动化,创建一系列原型工具（例如 Smallfoot, Space Invader, Abductor) 来支撑这些推理逻辑，最终发现了 bi-abduction 是模块化分析程序的一种有效形式。

基于上述研究成果,我们 2009 年创建了一个名为 Monoidics 的公司。Monoidics 在 2013 年加入 Facebook，从那以后我们采用持续开发和部署的风格来开发我们的产品，在我们的分析器团队和 facebook 移动软件开发工程师的不断努力的迭代开发下我们的分析器得到了很大的提升。我们也展示了当运用到 facebook 代码库时代码检查技术能够得到快速的发展。

展望未来

程序检查是一个有着活跃研究社区和前景光明的领域。在 facebook,我们说过这趟旅行我们只完成了 1%。在程序检查领域还有很多的工作需要我们去完成。但是，随着我们的不断努力，我们相信这个领域的成果会让软件工程师解放出更多的价值。我们可以展望未来，有你的帮助，程序检查技术能够提供更多、更有用的技术来使得我们的代码更可靠、更高效。

你可以下载和试用 Facebook Infer 或者移步到 fbinfer.com 以了解更多的详细情况。