我将实现一个指向分析算法。我想主要基于Whaley 和 Lam 的算法来实现这个分析。Whaley 和 Lam 使用基于BDD的Datalog实现来表示和计算点到分析关系。
下面列出了在典型的指向分析中使用的一些关系。请注意，如果、和都为真，则D(w, z) :− A(w, x),B(x, y), C(y, z)表示为真。BDD 是用来表示这些关系的数据结构。D(w, z)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 用于不同的目的，即统一。所以，我想我也许可以使用 Maude 而不是 Datalog 引擎来计算我的点到分析的关系。我假设莫德同时传播独立信息。这种并发性可能会使我的指向分析比顺序处理规则更快。但是，我不知道代表我在莫德的关系的最佳方式。是我自己在 Maude 中实现 BDD，还是 Maude 基于 BDD 的内部统一也有同样的效果？