软件分析笔记8 Datalog

Datalog = Data + Logic，是声明式编程语言(Declarative Programming Language) Prolog的一个子集

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

语法

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

,表示and
;表示or
!表示not，这些运算可以用括号改变优先级
每条语句的最后要加.表示结束，这个老是忘....

Predicate

即谓词。谓词可以看成是一个函数，n元谓词就是一个(D^nmapsto left{;0,1; ight})的函数，其中(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()))，我们就需要维护某个元素所有相关的信息，即用元组

求解

就是列真值表，(prodlimits_{Bin Body} |B|)枚举所有可能的值求解(F(P))

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).

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