Я собираюсь реализовать алгоритм баллов к анализу . Я хотел бы реализовать этот анализ в основном на основе алгоритма Уэйли и Лэма . Уэйли и Лэм используют реализацию Datalog на основе BDD для представления и вычисления отношений анализа точек.
Ниже перечислены некоторые отношения, которые используются в типичном точечном анализе. Обратите внимание, что D(w, z) :− A(w, x),B(x, y), C(y, z) означает, что D(w, z) - это истина, если A(w, x), B(x, y) и C(y, z) - все истина. 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)
Мне нужно понять, является ли Мод хорошей средой для реализации анализа точек. Я заметил, что Мод использует библиотеку BDD с именем BuDDy . Но похоже, что Мод использует BDD для другой цели, то есть унификации . Итак, я подумал, что смогу использовать Мод вместо движка Datalog для вычисления отношений моих точек к анализу. Я предполагаю, что Мод распространяет независимую информацию одновременно. И этот параллелизм потенциально может ускорить мой анализ точек зрения, чем последовательная обработка правил. Но я не знаю, как лучше представлять мои отношения в Моде. Должен ли я сам внедрить BDD в Мод, или внутреннее объединение Мод, основанное на BDD, дает тот же эффект?