在Facebook上，我们的移动代码所做的每一项更改都由我们的静态分析仪Infer进行检查。静态代码分析器是扫描程序的源代码以检测可能的错误的工具。 静态分析器的主要优势在于能够在不运行程序的情况下以及在将软件交付给用户之前检测错误。

      与其他静态分析器相比，Infer的其中一个优点是可以进行大规模的过程间/文件间的复杂分析。也就是说，Infer可以通过跟踪过程间的调用或者跟踪跨越多个文件的程序来检测出细微的bug。

      许多过程调用跟踪值或者过程跨越不同文件来检测细微的错误。值得一提的是，尽管Infer的分析非常复杂且深入，但它能够很好地对大型程序进行分析，这些大型程序可能由由数百万行代码组成。

      尽管Infer有一定的优势，但它也有局限性，其中一个就是它的可扩展性。对于Infer来说，增加一种新的bug检查类型将是一项复杂的任务，因为需要开发人员具有大量的深度静态分析专业知识以及Infer内部的知识。这对于编写那些不需要Infer提供的所有复杂功能的新的bug检查类型来说尤其痛苦。实际上，许多重要的软件错误仅限于单个过程的代码（称为过程内）。为了发现这些缺陷，可以进行简单的分析，而这些分析不需要非常专业的静态分析技术。通常可以通过检查程序的语法来发现这些错误。

      出于这个原因，我们开发了一种名为AL的新语言来轻松地设计出能够检测出这类型缺陷的新检查器。这样，当开发新检查器时，就不需要了解Infer内部的知识，因为AL会帮你解决。AL是一种简单的，能够推理出抽象语法树的声明性语言，它简单、快速并具有较强的互动性。通常用几行AL代码就能够编写一个新的检查器，并且在分析程序时，Infer不必重新编译解释器。你可以立马看到新的检查器的效果，能够有效地帮助我们设计和调整新的检查器。

      AL是开源的，并且包含了Infer。目前，AL适用于C，C ++和Objective-C，我们计划在将来将其扩展到其他语言。

      编写一个新的检查器

      让我们看一个具体的例子，假设我们现在想要编写一个Objective-C的检查器：

            “包含单词'delegate'但不包含单词'queue'的属性不应声明为‘strong’。”

      在没有AL之前，在Infer里添加一个可以检测这种情况的检查器是一项复杂的工作：您需要修改Infer的OCaml源代码来编写AST遍历，并添加新的代码来识别有问题的代码，并在Infer中添加新的错误类型，等等。完成这些任务大多需要深入了解Infer的内部知识。

      AL简化了添加新的检查器的过程。我们只需要编写可以表达上述问题的AL代码并添加一条消息来向用户报告。 然后我们将它打包成一个检查器定义，这样就可以了。AL代码如下：

      检查器的定义以关键字“DEFINE-CHECKER”开始，其后跟着检查器的名字。第一个LET语句定义了变量name_contains_delegate。它使用了AL的断言declaration_has_name，它根据声明名称是否包含正则表达式中指定的单词返回true 或false。 AL的断言是一个在AST节点上进行评估的简单原子公式。AL提供了一个可用于构建检查器的断言库，并且这个库还在不断地增长。变量可用于简化其他定义。

      “SET report_when”定义了一个约束，当其返回true时将会通知Infer报告一个错误，这可以用来定义当检查器发现错误时所给出的出错信息。在我们的例子中，该行代码说明了当我们访问“ObjCPropertyDecl”节点（在Objective-C中声明一个属性的AST节点）时应该报错，此时我们发现了一个包含“delegate” (name_contains_delegate) 并且不包含“queue” (name_does_not_contain_queue)但是却被标记为“strong” (is_strong_property())的属性。

“SET message”语句中定义了发送给用户查阅的错误信息。请注意这些信息中可以包含例如”%decl_name%”的 占位符。这些占位符可以被Infer用他们目前的值进行替换以发送给用户准确的出错信息。在这个例子中，它是检查器的名字。“SET suggestion”语句是可选的，它可以用来提示开发者如何定位和修复Bug。

      一旦完成定义，新的检查器就能够被添加到一个可以被Infer解释的文件中，并且进行代码分析和检查。

        AL表达式

      在AL中，我们可以编写出比示例中更加复杂的表达式。通常，AL基于一个被称为时间序列的数学模型。

      你可以将程序中的AST路径看做时间的离散抽象。更具体地，在AL中，一个AST节点就是一个时间点，并且它的子节点就是未来。

      AL中包含了描述未来如何发展的时间运算符（因此我们可以在节点的后代中找到它）。例如，HOLDS-EVENTUALLY运算说明了表达式在当前节点的某些后代中应该变为真。 例如，以下表达式：

      call_method("removeObserver:") HOLDS-EVENTUALLY   评估了如果在n的后代中的某个点处存在方法“removeObserver：”调用的节点，则n变为真。

      在内部，为了检查表达式的有效性，AL引擎由技术上称为模型检查算法驱动，该算法可以让时态逻辑推理出语法树。

      应用

      在Facebook上，我们已经部署了几个AL检查器。每次代码更改后，它们与其他Infer检查器分析一起运行进行静态代码检查。两个例子是：

      1：直接的原子属性访问：这个检查器会检查是否应该通过其基础字段（称为ivar）直接访问声明为“原子”的ObjC属性，因为这可能会破坏原子性并导致竞争条件。

      2：正在被取消分配注册的观察者状态检查：这个检查器会检查在NSNotificationCenter中注册的观察者对象在取消分配之前是否被取消注册。如果没有，通知中心将继续发送消息给解除分配的对象，导致应用崩溃。

      在Facebook，我们已经证明AL非常有用，可以在Infer中快速添加新的检查器。迄今为止，AL编写的检查器已经报告了数千个错误。在我们继续开发AL的过程中，我们仍然从这个经验中学习。我们计划围绕语言来改进这个工具（特别是调试工具），以便将来能够更容易地编写新的检查器。此外，我们不断扩展AL的断言库和宏库，使其更具表现力。

      对于想要使用新检查器扩展Infer，但对静态分析技术没有深入了解的Objective-C / C / C ++开发人员，AL是一个很好的解决方案。AL由开源Infer解释，并且能够在包含现有linters的linter.al文件中添加新的检查器。

      【英文原文】 https://code.facebook.com/posts/277643589367408

      {测试窝原创译文，译者：初心}

      译者简介：初心，东南大学在读硕士研究生