Checker FrameworkによるJavaのNullnessの静的解析

[Checker Framework](http://types.cs.washington.edu/checker-framework/) を使うとJavaのソースコードに対してNullnessやコンストラクトされていないオブジェクトの逸出などを静的解析によって検出することができます。これまでもEclipseやIntelliJなどのIDEにもそのような機能はありましたが、Checker Frameworkの場合はIDEから独立したツールなので、CIなどで走らせることもできて使いやすいです。このChecker FrameworkはOracleの[ドキュメント](https://docs.oracle.com/javase/tutorial/java/annotations/type_annotations.html)や[ブログ](https://blogs.oracle.com/java-platform-group/entry/java_8_s_new_type)などでも登場しています。ここでは導入などは省き、Nullnessに対してどのような検出が可能で、どのような対処ができるのかを説明します。

# 基本的なNullness Check

次のようなメソッドを考えます。

```java
String toString(Message obj) {
  return obj.toString();
}
```

Checker Frameworkはすべての型を基本的に`@NonNull`とみなすため、このコードは検査に通ります。次のようなコードは通りません。

```java
String toString(@Nullable Message obj) {
  // error: [dereference.of.nullable] dereference of possibly-null reference obj
  return obj.toString();
}
```

次のようにしても通りません。

```java
String toString(@Nullable Message msg) {
  if (msg == null) {
    // error: [return.type.incompatible] incompatible types in return.
    return null;
    // found   : null
    // required: @Initialized @NonNull String
  }
  return msg.toString();
}
```

これだと通ります。[^nullreturn]

```java
@Nullable
String toString(@Nullable Message msg) {
  if (msg == null) {
    return null;
  }
  return msg.toString();
}
```

[^nullreturn]: 普通はこういう状況では空文字列や`"(null)"`を返すようにする気がしますが、ここではサンプルなので無視します。

`msg`が`null`のときだけ返り値も`null`になる可能性があることを示したいときは`@PolyNull`を使います。

```java
@PolyNull
String toString(@PolyNull Message msg) {
  if (msg == null) {
    return null;
  }
  return msg.toString();
}
```

`@PolyNull`は同一シグネチャにある他の`@PolyNull`と連動して、全部が`@Nullable`になった場合と全部が`@NonNull`になった場合の２つのシグネチャがあるように振る舞います。上の例の場合は、`msg`が`@Nullable`だった場合は`null`を返す可能性があるので返り値も`@Nullable`に、逆に`msg`が`＠NonNull`だった場合は必ず戻り値も`@NonNull`になります。`@PolyNull`が提供する機能はあまり直感的ではないですし、限定的です。

次のようなコードはチェックすることができません。

```java
String firstNonNull(Message a, Message b) {
  if (a != null) {
    return a.toString();
  }
  if (b != null) {
    return b.toString();
  }
  return null;
}
```

この例では`a`または`b`が`@NonNull`であったときだけ返り値も`@NonNull`であってほしいのですが、そのような表現をすることは、現在のChecker Frameworkではできません。

# Genericsに対するNullness Check

Checker Frameworkは型変数に対してもNullnessを調べることができます。しかし、型変数は通常の型と違い、デフォルトで`@Nullable`のような動きになります。

```java
<T> String toString(T obj) {
  // error: [dereference.of.nullable] dereference of possibly-null reference obj
  return obj.toString();
}
```

これを回避するために、次の２つの方法が考えられます。

* `<T>`が`@Nullable`でも動くように`if (obj == null)`のようなチェックを入れる。
* `<T>`が`@NonNull`しか取れないように制限する。

前者は基本的なNullness checkと同じなので、後者について見ていきましょう。

```java
<T extends @NonNull Object> String toString(T obj) {
  return obj.toString();
}
```

Java8よりアノテーションは型に対してもつけることができるようになりました。ここでは型変数`<T>`に対する制約条件として`@NonNull Object`を指定しています。先に述べたように、通常の型については`@NonNull`がデフォルトになっているので、実際には`<T extends Object>`でも同様の効果が得られます。

## Nullnessと型階層

ここで一旦Javaの型階層とGenericsについておさらいしておきましょう。

Javaのすべての型は`Object`を継承しています。なので、次のような２つのクラス定義は、実質的に同じです。

```java
class Message {
}

class Message extends Object {
}
```

Genericsの型変数に対しては、どのような型を継承している必要があるかを指定することができます。例えば次のようなメソッドの場合、`Message`または`Message`を継承したオブジェクトしか引数として渡すことができません。

```java
<T extends Message> void method(T obj) {}
```

このような継承を続けていくと、例えば次のような構造になります。

![Types](https://qiita-image-store.s3.amazonaws.com/0/18199/65a11360-bc2a-9fc1-bb1b-9982bb92c43e.png)

これをNullableが入った型の世界に拡張すると次のようになります。

![Nullable Types](https://qiita-image-store.s3.amazonaws.com/0/18199/e58c3391-d462-422e-a9e4-cd30b45f46c2.png)

ちょっと複雑になりましたが、詳しく見るとそこまでではありません。例えば`@NonNull RequestMessage`は`@NonNull Message`にも`@Nullable RequestMessage`にもなれます。

```java
void nullness(@NonNull RequestMessage msg) {
  @NonNull Message nonNullMessage = msg;
  @Nullable RequestMessage nullableRequestMessage = msg;
}
```

`@NonNull RequestMessage`から`@NonNull Message`へのキャストは、通常の`RequestMessage`から`Message`へのキャストと変わりません。新しいのは`@NonNull`から`@Nullable`へのキャストです。これも確かに`null`じゃない値を`null`かもしれない変数に代入すると考えれば、特に大したことではありません。逆に`null`かも知れない値を`null`ではないとされている変数に代入しようとすると、それはダメだということになります。

```java
void nullness(@Nullable Message msg) {
  // error: [assignment.type.incompatible] incompatible types in assignment.
  @NonNull Message nonNullMessage = msg;
  // found   : @Initialized @Nullable Message
  // required: @UnknownInitialization @NonNull Message
}
```

---

もう一度先ほどのGenericsに対するNullness checkを見てみましょう。

```java
<T extends @NonNull Object> String toString(T obj) {
  return obj.toString();
}
```

ここで`@NonNull Object`を継承しているのは、先の図の中では`@NonNull Object`と`@NonNull Message`、`@NonNull RequestMessage`しかありません。型変数`<T>`として使えるのは`@NonNull`のオブジェクトしか無いことになります。

最初に型変数はデフォルトで`@Nullable`のような動きになると述べました。これは制約がない型変数`<T>`は、基本的にすべての型が取れるということになるはずなので、型階層の一番上、つまり`@Nullable Object`が暗黙の制約条件として選ばれるからです。

# Polymorphic Nullness

GenericsはNullnessに対してもPolymorphicな動きをするため、`@PolyNull`と同じようなことを簡潔に表現できます。

```java
void modify(Message msg) {
}

<T extends @Nullable Message> T modifyIfNonNull(T msg) {
  if (msg != null) {
    modify(msg);
  }
  return msg;
}

@Nullable
Message nullableMessage(@Nullable Message msg) {
  return modifyIfNonNull(msg);
}

Message nonNullMessage(Message msg) {
  return modifyIfNonNull(msg);
}
```

`modifyIfNonNull`は`@Nullable`な引数をとったときは`@Nullable`な値を返す一方で、`@NonNull`な引数ととったときは`@NonNull`な値を返しています。これは`nullableMessage`が`modifyIfNonNull`を呼んだときは`<T>`は`@Nullable Message`になっていて、`nonNullMessage`が`modifyIfNonNull`を呼んだときは`@NonNull Message`になっているからです。

# JavaのNullnessに対する基本戦略

基本的にJavaのすべての変数は`@NonNullByDefault`であるべきです。特別な理由がない限り、`@NonNull`は単に冗長なだけなので、つけることはしません。これはChecker Frameworkにおけるデフォルト動作にもなっていますし、ドキュメントでも`@NonNull`を書くのは極稀であると書かれています。必要な部分だけ`@Nullable`をつけるようにしましょう。また、`Preconditions#checkNotNull`のようなNullnessに対する防御的プログラミングも推奨しません。静的解析によってこういった性質はコンパイル時に保証されるので、単に冗長なだけになってしまいます。

Java8より`Optional`が導入されましたが、`Optional`の仕様策定側からも[コメント](http://stackoverflow.com/questions/26327957/should-java-8-getters-return-optional-type/26328555#26328555)があるように、`Optional`はLambdaをベースにしたコーディングスタイルと適合するようにデザインされたクラスです。`Optional`によってJavaの言語レベルでNullnessを明示できるのは結構なことですが、これを`null`の代用として使い、`if (obj != null)`の代わりに`if (obj.isPresent())`を使うのは、あまり効果的ではありません。[^nullcomplaints]Lambdaを使ったコードベースであっても、Checker Frameworkが提供するNullnessの解析は依然として有効ですし、Genericsを使ったPolymorphicなNullnessの保証は、限定的ではあるにせよ、`Optional`より綺麗に表現することができます。


[^nullcomplaints]: Javaにおいて`null`が非常によく嫌われる傾向がありますが、よく設計されたシステムでは`null`がいたるところで散見されることはありません。`null`や検査例外は局所的なエラー状態を表しており、回復可能性がないと判断した時点で非検査例外によって即座にトップレベルまでエスカレーションされるからです。また、`null`が現れることが普通である部分では、Null Objectのようなパターンを用いることで`null`チェックを回避します。あまりよく設計されていないシステムでは、ある部分で`null`が出てくると、とりあえず`null`を返しておくというコードが多発します。`null`が出てくるということが例外的であるような状況では、回復可能性が低いことが多いため、非検査例外を投げる設計のほうが適切です。しかし例外に対する理解が低い場合、例外はなんとなく難しそうだからという理由で、とりあえず`null`を返してしまうようです。この「とりあえずわからないから`null`を返す」が積み重なると、いたるところで`null`チェックをしなければいけなくなり、結果として「Javaはどこでも必ず`null`チェックが必要で面倒くさい」という意見を持つようになります。「とりあえず`null`を返す」という習慣を直さないかぎり、`Optional`もChecker Frameworkもコード品質を改善することができません。