nilaway
どんなもの?
- nil パニックによるランタイムエラーになる箇所を指摘してくれる静的解析ツール
- スタンドアロンで動く。golangci-lintで使用するにはカスタマイズが必要。
先行技術やツールと比べてどこがすごい?
- 標準パッケージに同梱されているnilness1ではチェックできないnil パニックとなりうる箇所を指摘する
- 関数やパッケージの境界を跨いでnilフローを追跡
- nil インターフェース値を報告
例えば以下のコードでは、nilnessはエラーを報告してくれないが、nilawayはnilパニックを報告してくれる。
技術のキモはどこ?
Our main idea is that nilability flows in code can be modeled as a system of global typing constraints, which can then be solved using a 2-SAT algorithm to determine potential contradictions Core Idea of nilaway2
コード内のnil可能性フローを型付け制約のシステムとしてモデル化し、2-SATアルゴリズムでnilable constraint
からnonnil constaint
にnil 値が流れている箇所を割り出しているところ。
どういうこと?
2-SATアルゴリズム3
- いくつかの変数とそれらの変数に対する「AならばB」といった制約条件が与えられたときに、全ての制約条件を満たすような変数の値の組み合わせ(真偽)を見つけられるかどうかを判定する。
- 例:「雨が降ったら傘をさす」という制約条件は、変数「雨」と「傘」が、「雨が真ならば傘も真」という関係になっていると考えることができる。2-SAT問題では、このような制約条件がたくさん与えられ、それらをすべて満たせるかを判定する。
- nilawayでは、プログラム中のnil値のフロー(nil値がどこから来てどこへ行くのか)を、この2-SAT問題としてモデル化し、
nilable constraint
からnonnil constaint
にnil値が流れている箇所(矛盾)を見つけている。
nilable constraint(以降、nilable 制約)
- 変数や値がnilになる可能性があるということを表す制約
- 以下コードでは、関数fooはstring型のポインタを返しているが、変数xは初期化されていない。そのため、xはnilである可能性があり、
return x
はnilable 制約となる。
nonnil constraint(以降、non nil制約)
- 変数や値がnilではないということを表す制約
このコードでは、関数barはstring型のポインタを引数として受け取り、そのポインタが指す値を表示している。ここで、ポインタxがnilの場合、*x
による参照はnil パニックを引き起こすため、*x
はnon nil制約となる。
具体例
以下のコードを実行するとnil パニックになる。obj
はnilになるにも関わらず、メソッドを呼び出そうとしているため。
ざっくり、筆者が理解した範囲で処理の流れを追ってみる。
-
nilable constraint
とnonnil constraint
の収集- MyFunc() 関数の戻り値が MyInterface 型の nilインターフェース値を返しているため、nilable 制約としてマーク。
- main() 関数内の obj.Method() の呼び出しは、obj がnon nil制約であることをマーク。インターフェースのメソッドを呼び出すには、インターフェースが具体的な型の実装へのポインタを保持している必要があるため。
-
含意グラフの構築
- 収集した制約に基づいて、次のような含意グラフ4を構築する。
- ノード: MyFunc() の戻り値, obj
- エッジ: MyFunc() の戻り値 -> obj
- 収集した制約に基づいて、次のような含意グラフ4を構築する。
-
含意グラフの走査:
- nilaway は、MyFunc() の戻り値が nil であるという情報から始め、含意グラフのエッジを介して obj に伝播する。その結果、obj も nil であると推論される。
-
矛盾の検出
- nilaway は、obj に対して nil 可能とnon nil の両方の制約があることを検出する。obj が nil の場合に obj.Method() を呼び出すと nil パニックが発生することを意味し、エラーとして報告する。
:::message 筆者は残念ながら当該分野の専門ではないため、2-SATアルゴリズムの理解及びこのツールでの実装について正確とはいえません。もし誤りがあれば、ご指摘いただけると幸いです。 :::
次に読むべき情報は?
Uber Blog -engineering
nilawayのアーキテクチャ
おわりに
注意点ですが、公式リポジトリで言及されている通り、nilaway は現在開発中というステータスです。ドキュメントが充実していない・一部欠けているなど注意が必要です。
とはいえ、気づきにくいnilパニックを報告してくれる実用的ツールです。皆さんもプロジェクトに組み込んで試してみてはいかがでしょうか。
Footnotes
-
https://pkg.go.dev/golang.org/x/tools/go/analysis/passes/nilness ↩
-
https://www.uber.com/en-JP/blog/nilaway-practical-nil-panic-detection-for-go/#:~:text=Our%20main%20idea%20is%20that%20nilability%20flows%20in%20code%20can%20be%20modeled%20as%20a%20system%20of%20global%20typing%20constraints%2C%20which%20can%20then%20be%20solved%20using%20a%202-SAT%20algorithm%20to%20determine%20potential%20contradictions ↩
-
https://en.wikipedia.org/wiki/2-satisfiability?uclick_id=3a0e8c6c-f4fe-4f94-9448-eb11df90bde1 ↩