Facebookの新言語ALは静的プログラム解析を簡単化する

ALは抽象構文木に関する推論を行うためのシンプルな宣言型言語だ。これを使うことで、Facebook Inferの静的解析を拡張することができる。

InferはOCamlで書かれたツールで、C、Java、Objective-Cのコードに対して、Nullポインターアクセス、リソースおよびメモリリーク、その他検出可能なエラーを通知することができる。Facebookによると、自社のiOSおよびAndroid用のモバイルアプリにおいて、Inferは80%のバグを正しく識別できるという。

Inferを拡張するには、静的解析の専門知識とInfer内部の知識の両方が必要になる。ALはそのInferの制限を克服して、簡単にしようとするものだ。特にALは、新しいタイプのプロシージャ内バグ、すなわち単一プロシージャのコードに限定したバグのチェッカー定義の簡単化を狙っている。こうしたバグは、プログラムの構文、よくある言語イディオム、カスタム規約を活用したシンプルな解析により検出できる。たとえば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の部分だ。strong参照として宣言されたObjCPropertyDeclオブジェクト – Objective-Cのプロパティ宣言に関連づけられたASTノード – （is_strong_property）という条件を定義している。

Facebookによると、新しいチェッカーは通常、ALで数行書くことで定義でき、Inferを再ビルドする必要なく、すぐに新しいチェッカーの反応を確認できるという。さらにALは、時相論理（temporal logic）モデルに基づいた複雑な式の定義をサポートしている。そこでは、ASTノードを特定の時点に関連づけ、すべての子孫を将来起こり得ることとみなす。ALは将来のノードのプロパティを定義するオペレータを提供している。HOLDS-EVENTUALLYオペレータは、プログラムが将来のある時点で正しいことを検証する式に関連づけることができる。

ALはInfer（GitHubから入手可能）の一部であり、C、C++、Objective-Cのコードに使うことができる。