Facebook 新推出 AL 语言，意在简化程序静态分析

AL 是一种易用的声明式编程语言，适用于抽象语法树（AST）推理，使开发人员可以扩展 Facebook Infer 静态分析器的功能。

Infer 采用 OCaml 编写，可标识 Null 指针访问、资源和内存泄漏，以及其它一些 C、Java 和 Objective-C 代码中的可检测错误。据Facebook 介绍，在他们的iOS 和Android 移动应用中，80% 的软件缺陷是由Infer 正确地检测出的。

AL 易于扩展，这克服了一个局限 Infer 的问题。实现扩展不仅需要具备静态分析的专门技能验，而且需要掌握 Infer 的内部机制。具体而言，AL 意在简化对过程内（Intra-procedural）软件缺陷新类型分析程序（Checker）的定义，即局限于过程代码内的软件缺陷。这类软件缺陷可使用更简单的分析手段检测到，包括借助于程序语法、通用语言习语和自定义约定。举个例子，在 Objective-C 中，为避免存留环路，对象的 delegate通常不应做为 strong引用。针对需求的分析程序可使用 AL 定义为：

 
DEFINE-CHECKER STRONG_DELEGATE_WARNING = {
   LET name_contains_delegate =     
       declaration_has_name(REGEXP("[dD]elegate"));
   SET report_when =
       WHEN
          name_contains_delegate 
          AND is_strong_property()
       HOLDS-IN-NODE ObjCPropertyDecl;
   SET message = "Property or ivar %decl_name% declared strong";
   SET suggestion = "In general delegates should be declared weak or assign";
 };

在上面的 AL 代码中，亮点在report_when语句。该语句在ObjCPropertyDecl对象上定义了一个条件，声明为一个strong引用（is_strong_property）。ObjCPropertyDecl对象就是关联到 Objective-C 属性定义的 AST 节点。

据 Facebook 介绍，通常使用数行 AL 代码就能新定义一个分析程序，并可立即投入使用，无需重新构建 Infer，确保了对新分析程序的快速反馈。AL 还支持定义基于时态逻辑模型的更复杂公式，其中一个AST 节点可关联到时间上某一点，其所有的后代节点均看作是未来可验证的。例如，为保证程序的正确性， HOLDS-EVENTUALLY所关联的表达式可在未来某个时间点上得以验证。

AL 是 Infer 的一个组成部分，已开源于GitHub 上，适用于C、C++ 和Objective-C。

查看英文原文： Facebook’s New AL Language Aims to Simplify Static Program Analysis