Proj THUDBFuzz Paper Reading: 南京大学软件分析课程2020, 14 Datalog-Based Program Analysis

Motivation

目的：套用数理逻辑思路
Datalog：声明式语言（这里需要和c++这种命令式语言做出区别），简洁，可读性，易于实现。

Intro-Datalog

Datalog是Prolog的子集，在1980年代作为database language出现。
Datalog program = Facts + Rules

特点：

无副作用
无控制流（？）
无函数
图灵不完备

Predicate/Relation：相当于一张数据表
Fact：特定元组必然存在于特定Predicate里的担保。一
Relational atom，当Relational atom P(x1, x2, .., xn)（形如Predicate_Name(Arg_1_Name, Arg_2_Name, ..., Arg_N_Name)）为true时fact P(x1, x2, ..., xn)成立。
Arithmetic Atoms: 例如age >= 18
Datalog Rules: 基本形式 H <- B1, B2, ..,Bn 常用来声明fact如何推导。Datalog支持递归规则。比如Reach(from, to) <-Reach(from, node), Edge(node, to).

例如:
Adult(person) <-Age(person,age), age >= 18.
如果存在age>=18且(person, age)属于Predicate Age，那么Adule(person)为真

Predicates可分为两种

Extensional Database(EDB)：先验知识，不可改变，相当于inputs
Intensional Database(IDB):推测得到的predicates

逻辑或的方式

多条规则的head相同，这多条规则构成或关系。比如SportFan(person) <-Hobby(person,“jogging”). SportFan(person) <-Hobby(person,“swimming”).
用分号 SportFan(person) <-Hobby(person,“jogging”); Hobby(person,“swimming”).
- 分号(or)的运算优先级小于逗号(and)

逻辑取反的方式

叹号 !B(...)

Rule Safety

是否存在会使得Datalog陷入死循环的规则？
A(x) <- B(y), x > y. 能够满足x>y的值是无穷的。
为此，Datalog定义safe rule为：所有变量都至少出现在非负relational atom里过（所有变量都可以检索）。
unsafe rule不允许。因此，A(x) <- B(y), !C(x,y). 也是不允许的。

此外A(x) <- B(x), !A(x) 会导出矛盾，使得推出的head不正确，因此递归和取反被要求不能同时出现。
因此Reach(from, to) <-!Reach(from, node), Edge(node, to). 不能出现。

Modern Datalog Engines

Datalog engine deduces facts by given rules and EDB predicates until no new facts can be deduced.
LogicBlox, Soufflé, XSB, Datomic, Flora-2, ...

因为facts只会增加，不会减少，所以Datalog程序是单调的。
又因为IDB predicates的潜在值是有限的（safe)，所以Datalog Program一定能够终止。