软件分析08 Datalog

\newcommand\norm[1]{\left\lVert#1\right\rVert} \newcommand\abs[1]{\left\lvert#1\right\rvert}

Datalog最早作为数据库的查询语言出现，是非图灵完备的编程语言

语法

和数理逻辑的命题逻辑、谓词逻辑基本是一致的，如果看的教材和我一样是Mathematical Logic in Computer Science的话甚至会发现很多描述的语句都是一样的

,表示and

;表示or

!表示not，这些运算可以用括号改变优先级

每条语句的最后要加.表示结束，这个老是忘….

Predicate

即谓词。谓词可以看成是一个函数，n元谓词就是一个$D^n\mapsto \left{\;0,1\;\right}$的函数，其中$D$是命题变元(变量)与命题常元(常量)构成的集合

在Datalog中，我们讨论的都是有限论域，因此使谓词P为真的命题有限。记$F(P)$为所有在谓词P下为真的n元组，则我们称这些元素为Facts。这样就把一个函数变成判断元素是否属于某集合的问题了。

谓词分为两类，算术谓词x >= y和关系谓词Friends(x, y)，算术谓词是Unbounded的

Inference Rules

即推理规则。用PPT的例子就是Datalog的推理规则形如

Adult(x) <- Person(x, age), age >= 18.

<-可以看成是向左的箭头(好形象！)，箭头左侧的称为Head，右侧是Body。语句的意思是”若Body为真，则Head为真”

这句话的意思是”若x是age岁的人 且 age>=18 那么x是成年人”

考虑形式化命题会怎么说

$((\forall x)(Person(x)\wedge Age(x)>=18))\vdash Adult(x) $

观察区别即可发现，如果不使用函数的概念(形式化命题里的$Age()$)，我们就需要维护某个元素所有相关的信息，即用元组

求解

Safe Rules

既然涉及到枚举，就要看看是不是可穷尽的

考虑如下两组Rules

A(x) <- B(y), x >= y.

A(x) <- B(y), !C(x, y).

对于1. 如果我们讨论的是正整数域，且$F(B)$非空，则必然存在无穷多的x满足要求…

对于2. 由于$F(C)$有限，因此$F(!C)$有无穷多元素，因此也存在无穷多的x满足要求…

基于上述情况，Datalog对Rules作出了规定：

Head中的变元必须在Body中的某个非否定谓词中出现过(即必须是Bounded Variable)

同样，再考虑如下Rule

A(x) <- !A(x).

很显然就不是合理的Rule，毕竟都不是重言式…因此设定Rules的时候也要考虑是否永真的问题(不能有矛盾)

IDB & EDB

IDB = Intensional DataBase 内涵谓词

EDB = Extensional DataBase 外延谓词

大概理解就是在初始阶段会规定一些谓词，这些就是EDB

而在推理过程中出现的谓词则是IDB。Head一定是IDB，而Body可以IDB、EDB

通常EDB是不可变的(常元)，而IDB可以随着程序的进行而修改，例如如果我想表示”喜欢猫 或 喜欢狗 的人是好人”，那么我可以写

Good(x) <- Likes(x, "Dog").

Good(x) <- Likes(x, "Cat").

当然也可以写

Good(x) <- Likes(x, "Dog"); Likes(x, "Cat").

递归

Datalog的强大之处就在于递归

考虑给定等价关系集合的传递闭包，就可以这么写

Eq(x, y) <- Rel(x, y)


Eq(x, y) <- Eq(x, z), Rel(z, y)

其中Rel(x, y)是EDB中提前定义好的常元

在指针分析中的应用

应用Datalog就能很容易翻译和实现前面讲到的Flow Insensitive & Context Insensitive分析

首先规定下面几个谓词

New(x, o)

Assign(x, y)

Store(x, f, y)

Load(x, y, f)


VCall(l, x, k) #l: x.k(a1,a2...an)

Dispatch(o, k, m)

ThisVar(m, this)

Argument(l, i, ai) #ith argument at l: is ai

Parameter(m, i, pi) #ith parameter at method m is pi

MethodReturn(m, ret) #return var at method m is ret

CallReturn(l, r) #r receives return value at l:

推导规则就是翻译PPT

VarPointsTo(x, o) <- New(x, o).

VarPointsTo(x, o) <- VarPointsTo(y, o), Assign(x, y).

FieldPointsTo(o1, f, o2) <- VarPointsTo(x, o1), VarPointsTo(y, o2), Store(x,
f, y).

VarPointsTo(x, o2) <- VarPointsTo(y, o1), FieldPointsTo(o1, f, o2), Load(x, y,
f).


CallGraph(l, m), Reachable(m), VarPointsTo(this, o) <- VCall(l, x, k),
VarPointsTo(x, o), Dispatch(o, k, m), ThisVar(m, this).

VarPointsTo(pi, o) <- CallGraph(l, m), Argument(l, i, ai), Parameter(m, i,
pi), VarPointsTo(ai, o).

VarPointsTo(r, o) <- MethodReturn(m, ret), CallGraph(l, m), CallReturn(l, r),
VarPointsTo(ret, o).

全程序分析还要加上一个默认的入口方法，没了