我应该如何在 Maude 中实施点分析？

Question

我将实现一个指向分析算法。我想主要基于Whaley和Lam的算法来实现这个分析。 Whaley 和 Lam 使用基于 BDD 的 Datalog 来表示和计算点分析关系。

下面列出了典型的点分析中使用的一些关系。请注意，D(w, z) :− A(w, x),B(x, y), C(y, z) 表示 D(w, z)A(w, x)、B(x, y) 和 C(y, z) 均为 true，则 > 为 true。 BDD就是用来表示这些关系的数据结构。

关系

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统一也有同样的效果？