Microsoftは、Infer#を使用して、Facebook Inferの手続き間の静的分析機能を提供することにより、.NETエコシステム内で利用できる静的アナライザーの選択肢を広げている。
Inferは、2015年にFacebookによってオープンソース化された静的分析ツールである。JavaおよびC/C++/Objective-Cコードをサポートし、AndroidおよびJavaコードでのnullポインター例外、リソースリーク、アノテーションの到達可能性、ロックガードの欠落、同時実行の競合状態などの多くの潜在的な問題を検出できる。そして、Cファミリに属する言語では、nullポインタの逆参照、メモリリーク、コーディング規則、および使用できないAPIを検出できる。
MicrosoftのシニアソフトウェアエンジニアであるXin Shi氏は、.NETで利用できる静的アナライザーはInfer#だけではないと述べている。ただし、Infer#は.NETプラットフォームに独自の機能をもたらす。Infer#を際立たせているのは、他のアナライザーには見られないクロスファンクション分析とインクリメンタル分析に重点を置いていることである。
PreFastは、null逆参照例外とメモリリークのあるインスタンスを検出するが、その分析は純粋に手順内です。一方、JetBrains Resharperは、メモリの安全性の検証に対して開発者のアノテーションに大きく依存しています。
たとえば、Shiは、3つの異なる関数を含む次のコードスニペットで、Infer#がnull逆参照を検出する方法について説明している。
static void Main(string[]) args)
{
var returnNull = ReturnNull();
_ = returnNull.Value;
}
private static NullObj ReturnNull()
{
return null;
}
internal class NullObj
{
internal string Value { get; set; }
}
差分ワークフローとは、Facebookが2つのバージョンのプロジェクトで実行するInferの機能をダビングし、混入した問題、あるいは修正済みの問題に関して比較を提供するものである。これにより、InferをCIワークフローに統合し、PRがメインブランチに受け入れられる前に自動的に処理することができるようになる。
たとえば、Shiは、次のコマンドを実行することで、feature
ブランチとmaster
ブランチの間で変更されたファイルのリストを取得できると説明している。
git diff --name-only origin/feature..origin/master > files-to-analyze.txt
次に、ブランチごとに、それをチェックアウトしてInferを実行する。
git checkout <branch>
infer capture -- make -j 4
infer analyze --changed-files-index files-to-analyze.txt
cp infer-out/report.json <branch>-report.json
最後に、Inferのreportdiff
コマンドを使用して、結果を比較する。
infer reportdiff --report-current feature-report.json --report-previous master-report.json
これにより、feature
ブランチで入り込んだ問題、feature
で修正された問題、そのまま残った問題を含む3つのファイルが出力される。
増分変更を分析する機能により、Inferを大規模なコードベースで効果的に実行できる。この理由から、Microsoftは、Roslyn、.NET SDK、ASP.NET Coreなど、多くの製品でInfer#を使用している。
手続き間分析と差分分析の両方をサポートするために、Inferは分離ロジックを使用する。これにより、コンピューターメモリの操作について推論し、特定のメモリ安全条件を証明できる。この目的のために、Inferは、capture
ステップ中にすべてのコードをSILと呼ばれる中間表現に変換する。SILは、Smallfoot述語フレームワークを活用する。
.NETソースコードを分析するためにInferを使うことの主要な問題は、それをInferが分析する言語であるSILに変換することです。これを行うには、ソース言語の構成要素をOCamlで表す必要があります。
このプロセスを簡素化し、Infer#をC#以外の他の.NET言語に簡単に拡張できるようにするために、MicrosoftはSILの中間言語に依存しないJSONシリアル化を取り入れた。
ソースコードの低レベル表現から作業することの利点は2つあります。1つは、CILがすべての.NET言語(最も一般的なC#に加えてVisual BasicやF#など)の基礎となるため、このようにしてInferSharpはすべての.NET言語をサポートします。次に、CILから糖衣構文が取り除かれます。これにより、翻訳に必要な言語コンテンツが削減され、翻訳が簡素化されます。
Microsoft SILシリアライザーは逆シリアル化パッケージと組み合わされている。逆シリアル化パッケージは、OCamlのSILデータ構造を抽出し、それらをInferのバックエンド分析に使用できるようにするものである。
現在、Infer#はnull逆参照とメモリリークの検出をサポートしている。しかし、Microsoftはすでに、競合状態とスレッドセーフ違反の検出のサポートを追加することで機能を拡張し続けることを発表している。