データフロー解析

データフロー解析は、プログラム上の各地点における事実（例えば、ある代入がどこに到達する可能性があるか、ある値がその後に使用されるかどうか、ある式がすべてのパスで既に計算済みかどうかなど）を構築します。これは実行パスを計算可能な抽象情報に圧縮し、制御フローグラフ（CFG）上で伝播させます。

結果は用途に合わせて保守的である必要があります。コード削除の証明には潜在的な動作を見逃してはいけませんし、潜在的なエラーを報告する分析であれば、ある程度の偽陽許容できます。保守的であることは、適当に推測することではなく、抽象的な結果と実際の実行の間の包含関係を明確にすることです。

分岐の合流から may と must を理解する

x が可能性としてどの定義から来るのかを問う場合は、2つのパスの候補を結合します。式 a+b が必然的に計算済みかどうかを問う場合は、両方のパスでその事実を提供する必要があります。古典的な集合解析では、前者には通常和集合（union）が、後者には通常共通集合（intersection）が使われます。

しかし、may/must は、すべての抽象ドメインが単純な集合同士の和集合・共通集合を使うことを要求しません。格（lattice）の偏序関係、top/bottom、join/meet の命名も規約によって変化するため、意味をまず定義し、その後に数式を書く必要があります。

統一されたフレームワークには5つの定義が必要

Gen/Kill は、多くのビットベクトル解析における便利な形式ですが、すべての伝達関数の唯一の形式ではありません。共通集合による合流を行う must 解析であっても、伝達関数内部の gen ∪ ... を共通集合に変更する必要があるわけではありません。

到達定義：前方の may 解析

定義 d が地点 p に到達するとは、d から p へのパスが存在し、その間に同じ変数の再定義がないことを意味します。変数名だけを記録するのではなく、各代入に独立した番号を振ります。

IN[B] = ∪ OUT[P] （P は B の先行ノードをすべて走査）

OUT[B] = GEN[B] ∪ (IN[B] − KILL[B])

GEN には、ブロックの出口まで生存する定義が含まれます。KILL には、本ブロックの代入によって上書きされる、同じ変数の他の定義が含まれます。ブロック内で d1: x=1; d2: x=2 と順に実行される場合、d1 は出口の GEN には含まれず、d2 が含まれます。

エントリでは通常、パラメータや外部の初期値の定義もモデル化します。教育用のモデルで空集合から開始する場合、これらが解析範囲に含まれていないことを明記すべきです。SSA ではスカラーは一意の静的定義に直接関連付けられますが、メモリ上のエイリアスによる書き込みは別途解析する必要があります。

生存変数：後方の may 解析

地点 p で値が生存しているとは、その値を先に使用し、その後で再定義する後続のパスが存在することを意味します。問題は未来を見るものであるため、後続ノードから前方へ伝播します。

OUT[B] = ∪ IN[S] （S は B の後続ノードをすべて走査）

IN[B] = USE[B] ∪ (OUT[B] − DEF[B])

USE は、ブロック内で最初に定義される前に使用される変数です。DEF はブロック内で定義される変数です。⁠その定義が以前に使用されたことがないことは要求されません。

例えば、ブロック x=x+1; y=x; return y において、USE={x}、DEF={x,y} です。出口の OUT=∅ の場合、入口の IN={x} となります。x が USE と DEF の両方に含まれるのは完全に理にかなっています。ブロックに入る前の古い x が最初の命令で必要であり、ブロック内で新しい x が生成されるためです。

ループにより、生存情報はバックエッジを介して伝播します。ある値の生存範囲は、関連する CFG パス上のプログラム地点の集合であり、ソースコード上の定義行から最終使用行までを単純に直線で結ぶものではありません。

利用可能式：前方の must 解析

地点 p で式 e が利用可能であるとは、p に到達するすべての関連パスで e が計算されており、その後に演算子が変更されていないことを意味します。純粋なスカラーモデルでは：

IN[B] = ∩ OUT[P]

OUT[B] = GEN[B] ∪ (IN[B] − KILL[B])

x=x+y であっても、新しい x による x+y が出口で利用可能になるわけではありません。右辺の計算では古い x が使用され、代入によって x が変更されるためです。GEN を構築する際には、ブロック内の後続の代入およびその文自体の定義を考慮する必要があります。

エントリは通常空で、他の到達可能なブロックは式全体の集合から始めて下方へ収縮していきます。到達不能なブロックや先行ノードのないノードは明確に処理する必要があり、空集合族の共通集合を取って偽の事実を伝播させてはいけません。

Worklist：影響を受けた近傍のみを再計算する

前方解析を例に取ります。境界と各ブロックの状態を初期化し、処理待ちブロックをキューに入れます。B を取り出し、先行ノードの出力を再結合して伝達関数を適用します。OUT が変更された場合、後続ノードをキューに入れます。後方解析では、IN が変更された場合に先行ノードに通知します。

有限高さの格上で、正しい初期値を用いた単調な反復計算は終了します。「最大要素が存在する」だけでは高さが有限であることを意味しません。無限高さの区間ドメインなどでは、widening が必要になる場合があります。反復回数は CFG、ループ、およびドメインに依存し、3〜5回で保証される固定値はありません。Clang データフロー解析入門

ループ内の到達定義：ヘッダを初めて通過した時点では、すべての答えが揃っていない

変数 x の2つの定義のみを分析します。エントリ E で d0: x=0 を実行し、ループ本体 B で d1: x=x+1 を実行します。ループヘッダ H は B に入ることも、出口 X へ進むこともできます。B は再び H へ戻ります。条件や他の変数は、このモデルの定義集合には含まれません。

E から H へ初めて到達した時点では、d0 しか知りません。B をスキャンすると d1 が発見されます。これをバックエッジを介して H に送ると、H は x が前回のループの d1 からも来る可能性があることを知ります。ここで d1 は静的な代入文のアイデンティティであり、動的なループ実行のたびに無限の定義番号を生成するわけではありません。

以下に worklist の実装を示します。状態は定義集合の包含順序を採用し、すべてのブロックは空集合から開始します。エントリには先行ノードがないため、GEN によって d0 が生成されます。すべてのノードが到達可能であるため、ここでは到達不能な入力を別途処理しません。

from collections import deque

succ = {"E": ["H"], "H": ["B", "X"], "B": ["H"], "X": []}
pred = {b: [p for p in succ if b in succ[p]] for b in succ}
gen = {"E": {"d0"}, "H": set(), "B": {"d1"}, "X": set()}
kill = {"E": {"d1"}, "H": set(), "B": {"d0"}, "X": set()}


def solve(order):
    out = {b: set() for b in succ}
    work = deque(order)
    queued = set(order)
    history = []
    while work:
        b = work.popleft()
        queued.remove(b)
        incoming = set().union(*(out[p] for p in pred[b]))
        new = gen[b] | (incoming - kill[b])
        if new != out[b]:
            out[b] = new
            history.append((b, tuple(sorted(new))))
            for nxt in succ[b]:
                if nxt not in queued:
                    work.append(nxt)
                    queued.add(nxt)
    return out, history


expected = {"E": {"d0"}, "H": {"d0", "d1"}, "B": {"d1"}, "X": {"d0", "d1"}}
out, history = solve(["E", "H", "B", "X"])
assert out == expected
assert [v for b, v in history if b == "H"] == [("d0",), ("d0", "d1")]
assert solve(["X", "B", "H", "E"])[0] == expected
# 期待値との比較だけでなく、最終的に各ブロックが元の方程式を満たすか確認する。
for b in succ:
    incoming = set().union(*(out[p] for p in pred[b]))
    assert out[b] == gen[b] | (incoming - kill[b])

ワークキューの順序は中間過程を変えますが、この有限で単調なフレームワークと同一の境界条件下では、最終的な解は同じになります。CFG を1回だけ走査する場合、H はバックエッジを永遠に見ることができないかもしれません。どのノードも変更されていない時点で停止すると、キュー内の他のノードにもたらされる新しい情報を逃す可能性があります。

バックエッジ上の事実は、いつ出口に伝わるのか？

以下のボタンは順序立てた授業の手順を規定するものではなく、処理待ち集合内の実際の解析タスクです。出口を先に処理して、一時的に空集合を得させることもできます。エントリやバックエッジが後で新しい事実を生成した場合、出口は後続ノードを介して再度キューに入ります。1回の不変は、その計算で新しい情報が追加されなかったことを示すだけであり、グローバルな停止条件はキューが空であることです。モデル内の d1 は常に1つの静的代入のアイデンティティです。

$$\mathrm{IN}[B]=\bigcup _{P\in \mathrm{pred}(B)}\mathrm{OUT}[P],\mathrm{OUT}[B]=\mathrm{GEN}[B]\cup (\mathrm{IN}[B]\setminus \mathrm{KILL}[B])$$

不動点とパスごとの求解：どこで精度が失われるか

MOP（Maximum Over Paths）は、各 CFG パスに沿って変換を適用してから合流します。一方、反復方程式では、途中のパスが合流し、その後さらに変換が適用されます。伝達関数が合流に対して分配可能などの条件下では、両者は一致します。そうでない場合、早期の結合は関連情報を失う可能性があります。

例えば、2つのパスがそれぞれ (x=1,y=2) と (x=2,y=1) を得て、その後 z=x+y を計算するとします。パスごとに計算すれば 3 が得られますが、非関係な定数伝播で早期に合流すると、x と y がともに非定数としてマークされ、z=3 を導出できない可能性があります。変数間の関係を保持する抽象ドメインを使用すれば精度を改善できますが、その分コストが高くなります。

MOP も通常、CFG 内の構文パスを走査します。これには、実際には同時に満たすことができない条件を含むパスが含まれる可能性があるため、そのまま「真のプログラム意味論の完璧な解」と呼ぶことはできません。MFP と MOP の大小関係は、採用された格の順序に依存するため、規約を離れて不等号を記録すべきではありません。

相関関係が失われた後、すべての組み合わせを実際のパスとして扱うことはできない

前述の2つのパスを直接集合として書き、正確なパスの状態を {(1,2),(2,1)} とします。x と y の可能な値をそれぞれ個別に保持すると、両方とも {1,2} になります。その後、デカルト積を行うと、(1,1) と (2,2) が追加され、存在しない和 2 と 4 が得られます。

paths = {(1, 2), (2, 1)}
xs, ys = {x for x, y in paths}, {y for x, y in paths}
precise = {x + y for x, y in paths}
nonrelational = {x + y for x in xs for y in ys}
assert precise == {3}
assert nonrelational == {2, 3, 4}
assert precise <= nonrelational

非関係な結果は真の結果を含んでいるため、「z は {2,3,4} に属する可能性がある」と保守的に言うことはできますが、z が常に 3 であることを証明することはできません。この精度の損失は、抽象状態がペアリング関係を保存していないことに起因します。worklist をさらに数回実行しても、すでに捨てられた情報は回復できません。改善するには、抽象ドメインを変更するか、合流を遅らせるか、パス条件を利用する必要があり、同じ方程式を繰り返し実行するだけでは不十分です。

x と y を個別に記憶することで、何が失われるのか？

具体的なパスを2次元座標上の点として描画すると、「相関関係の喪失」を正確に特定できます。x 軸と y 軸にそれぞれ投影してから組み合わせると、真の2点が4点に拡大する可能性があります。追加された点は、新しく発見された実行パスではなく、抽象が許容する追加の状態です。2つ目のパスを変更すると、いつ追加の組み合わせが発生しないかを見ることができます。同じ反復を繰り返しても、失われたペアリング関係を再び見つけることはできません。

$$R\subseteq {\pi }_x(R)\times {\pi }_y(R)$$

SSA と疎な解析

SSA はスカラーの def-use を明示化し、多くの事実を関連する値に沿って伝播させることで、無関係な CFG エッジ上での作業を削減します。しかし、φ 入力と先行エッジは関連しており、ループでは不動点が必要になる場合があり、メモリにはエイリアスと副作用が残ります。SSA は「すべての解析が支配木上の単一パス走査に退化する」ことを保証するものではありません。

速查

関連セクション：古典的最適化、レジスタ割り当て、SSA。

参考

• Clang：Data Flow Analysis。
• LLVM 解析と変換 Pass。

Keywords: dataflow, CFG, may, must, gen, kill, liveness, reaching definitions, available expressions, fixed point, MOP