制約パーティショニング

Irenka

めも。

クエリでプレースホルダ名をtypoされた時のエラー報告について。

/**
 * @when
 *   ret.result = 0
 */
public void checkReturnZero(CtReturn<?> returnStmt) {
  ...
}

上のクエリは、引数がreturnStmtに対して、クエリ内でretというプレースホルダを用意してそこに制約かけてる。
いくら頑張ってもretに制約かかるだけなので、returnStmtは「CtReturn型」という制約だけで動くのでよろしくない。retの計算は無意味に。

これはおそらく意図しない動作なので、ここでエラーを出す方法についてアイデア。制約関係でざくっとパーティショニングして、明らかに無意味なプレースホルダを探したい。

上のクエリをコンパイルすると、下のようなアセンブリ言語っぽい内部表現を生成。

IrQuery:
  // returnStmtはHack対象集合内のいずれか
  returnStmt in #universe#0
  // returnStmt はCtReturn型
  returnStmt:[RETURN]
  // retはHack対象集合内のいずれか
  ret in #universe#1
  // ret.result を ##2 に束縛
  ##2 = ret.result
  // ##2 は定数 0 に等しい
  ##2 equals 0

あるプレースホルダPが属するパーティションを、partition(P)で表現する。疑似コードとしてはこんな感じ。

partition(placeholder P) returns result:set-of-placeholder
  result := {P}
  for c in constraint(P)
    for r in placeholder(c)
      result := result ∪ r

constraint(set-of-placeholder P) returns result:set-of-constraint
  (プレースホルダPが出現するすべての制約式)

placeholder(set-of-constraint C) returns result:set-of-placeholder
  (制約式Cに出現するすべてのプレースホルダ)

そのうえで、メソッドパラメータと同名のプレースホルダの集合をMSとおいて、次の計算を行う(∪{p in MS} partition(p))。

parameter-relations(set-of-placeholder MS) returns result:set-of-placeholder
  result := {}
  for p in MS
    result := result ∪ partition(p)

最後に、元のクエリで出現した全てのプレースホルダの集合をOPSとおいて、OPSからparameter-relations(MS)の差集合を計算。要素が残っていれば、そのプレースホルダはパラメータに「無関係」であるといえる。はず。

先程の例で探すとこんな感じ。

  • partition(returnStmt) = {returnStmt, #universe#0}
  • partition(ret) = {ret, #universe#1, ##2}
  • parameter-relations(parameters in checkReturnZero) = {returnStmt, #universe#0}
  • {ret, returnStmt} - {returnStmt, #universe#0} = {ret}

この場合、retはreturnStmtに対して何の制約も課さないのでたぶんtypoだよね。という感じで。

ただ、これだけだと少々ぬるい。

ぬるい理由は↓。

/** retはmの中で定義され、返す値は定数1と同値。
 * @when
 *     ret in m.body
 *     ret.result = 1
 */
public void checkReturnZero2(CtMethod<?> m, CtReturn<?> r) {
  ...
}

コンパイルする。

IrQuery:
  m in #universe#0
  m : {@link CtMethod<?>}
  r in #universe#1
  r : {@link CtReturn<?>}
  ##2 = m.body
  ret in ##2
  ##3 = ret.result
  ##3 := 1
  • partition(m) = {m, ret, #universe#0, ##2, ##3}
  • partition(r) = {r, #universe#1}
  • parameter-relations(parameters in checkReturnZero2) = {m, ret, r, ...}
  • {m, r, ret} - {m, ret, r, ...} = {}

これは、「ret in m.body」を経由して ret が partition(m) に入り込んでいるため、最終的には ret が無駄な制約でないと判断されている。確かに、まったくrに影響が出ないわけでもない。

こういうときはちゃんとプレースホルダの宣言をした方がいいのか、悩み中。