ポイントツー分析アルゴリズムを実装します。主にWhaley と Lam によるアルゴリズムに基づいて、この分析を実装したいと思います。Whaley と Lam は、DatalogのBDDベースの実装を使用して、ポイントと分析の関係を表現および計算します。
以下に、典型的なポイントツー分析で使用されるリレーションの一部を示します。、 、およびがすべて真である場合、D(w, z) :− A(w, x),B(x, y), C(y, z)意味D(w, z)は真であることに注意してください。BDD は、これらの関係を表すために使用されるデータ構造です。A(w, x)B(x, y)C(y, z)
関係
input vP0 (variable : V, heap : H)
input store (base : V, field : F, source : V)
input load (base : V, field : F, dest : V)
input assign (dest : V, source : V)
output vP (variable : V, heap : H)
output hP (base : H, field : F, target : H)
ルール
vP(v, h) :− vP0(v, h)
vP(v1, h) :− assign(v1, v2), vP(v2, h)
hP(h1, f,h2) :− store(v1, f, v2), vP(v1, h1), vP(v2, h2)
vP(v2, h2) :− load(v1, f, v2), vP(v1, h1), hP(h1, f, h2)
Maudeがポイントツー分析を実装するのに適した環境であるかどうかを理解する必要があります。Maude がBuDDyという BDD ライブラリを使用していることに気付きました。しかし、Maude は BDD を別の目的、つまり統合のために使用しているようです。そのため、Datalog エンジンの代わりに Maude を使用して、ポイントと分析の関係を計算できるのではないかと考えました。モードは独立した情報を同時に伝播すると思います。そして、この並行性により、ポイントツー分析がルールの順次処理よりも速くなる可能性があります。しかし、モードで私の関係を表現する最良の方法がわかりません. Maude に自分で BDD を実装する必要がありますか、それとも BDD に基づく Maude の内部統合は同じ効果がありますか?