data flow constraints雑記

めも。

range of primitive values

プリミティブの値の範囲は比較的計算しやすい。

void f(int a) {
    if (/* (1) */a < 0) {
        return /* (2) */ - /* (3) */a;
    }
    else {
        return /* (4) */a;
    }
}

これをまじめにやるとSSA変換してマーキングしながら値の範囲を絞らないといけない。結構めんどい。ともあれint型の式は以下のような範囲になる。

(n)	expr	range
1	a	[Integer.MIN_VALUE..Integer.MAX_VALUE]
2	-a	(0..Integer.MAX_VALUE], Integer.MIN_VALUE
3	a	[Integer.MIN_VALUE..0)
4	a	[0..Integer.MAX_VALUE]

「必ず0以上」ってものを探すとしたら、>= 0 を修飾するのが読みやすいか？

/**
 * @when
 *     expr must >= 0
 */
public void found(CtExpression<Integer> expr) {
    // exprは(4)のみ
}

クエリを走らせるたびにSSA変換というのはちょっと無理っぽいぞ。逆SSAが要らないだけまだマシだけど。
まぁ、φ関数は「domainの和集合」って意味にとればいいから、解釈は楽だ。

ちなみに、属性付き型+SSAでかなり見やすくなる。

void f(int a) {
    if (/* (1) */a < 0) {
        int:[< 0] a:0 = a;
        return -a:0;
    }
    else {
        int:[! < 0] a:1 = a;
        return a:1;
    }
}

nullable

Eclipseが比較的頑張ってる。局所的な解析はnullかそうでないかというレベルなら、プリミティブの計算と大差ない。

void f(Object a, Object b) {
    if (/* (1) */a == /* (2) */null) {
        // control flow BREAK
        throw /* (3) */new NullPointerException(/* (4) */"a");
    }
    System.out.println(/* (5) */a.toString());
    System.out.println(/* (6) */b.toString());
    System.out.println(/* (7) */a);
    System.out.println(/* (8) */b);
    System.out.println(/* (9) */this.toString);
}

(n)	expr	null	remarks
1	a	unknonw	初回
2	null	true	trivial
3	new..	false	newなので
4	"a"	false	文字列リテラルなので
5	a	false	(1)以降なので
6	b	unknown	初回
7	a	false	(1)以降なので
8	b	false	(6)以降なので
9	this	false	thisはnullにならない

3値論理の意味は以下。

	意味
true	must null
false	must NOT null
unknown	may null

3値論理を使うとすっきり。「必ず〜である」「必ず〜でない」「不定」のいずれか。nullableに関する三値論理にヒットするクエリの演算子を考えてみると、分類としてはこうなるか？

	true	false	unkwnon
must == null	OK
must != null		OK
may == null	OK		OK
may != null		OK	OK

表記も同様。

/**
 * @when
 *     expr may == null
 */
public void found(CtVariableAccess<?> expr) {
    // 変数参照でmay = nullなのは(1), (6)のみ
}

解析自体は拡張基本ブロックを使ってデータフローを計算すれば自明*1。

こいつも参考程度に。

void f(Object a, Object b) {
    Self:[! null] this:0 = this;
    if (a == null) {
        Object:[null] a:0 = a;
        throw new NullPointerException("a");
    }
    Object:[! null] a:1 = a;
    System.out.println(a:1.toString());
    if (b == null) {
        Object:[null] b:0 = b;
        b:0.toString(); // error: cflow BREAK
    }
    Object:[! null] b:1 = b;
    System.out.println(b:1.toString());
    System.out.println(a:1);
    System.out.println(b:1);
    System.out.println(this:0.toString);
}

まとめ

ある地点でのデータの範囲はmust, may程度で記述できそう。

*1:a.toString()は(function(a) { if (a == null) throw new NullPointerException(); return a; })().toString()のようなものだと考えとく。