datalog

Posted on

DataLog学习

一直听说用datalog来做程序分析很NB，所以一直想学习他的使用方式。

参考: https://souffle-lang.github.io/tutorial

有向图可达性分析

1
2
3
4
5
6
7
8
9
.decl edge(n: symbol, m: symbol)
edge("a", "b"). /* facts of edge */
edge("b", "c").
edge("c", "b").
edge("c", "d").
.decl reachable (n: symbol, m: symbol)
.output reachable // output relation reachable
reachable(x, y):- edge(x, y). // base rule
reachable(x, z):- edge(x, y), reachable(y, z). // inductive rule
image-20211230141036143

对于这样一个有向图，做可达性分析， 只要做好了顶点之间的边的关系，您不需要dfs, bfs,几行代码就可以搞定：

image-20211230141323656

这全靠着datalog支持递归。

比如第二条规则

1
reacheable(x, z) :- reachable(x, y),reachable(y, z).

其中你告诉引擎, 如果一个符号x连接y, y连接z，那么x, z相连。 比如a到d, 引擎先根据第一条推导出a->b，b->c, c->d,然后开始递归，即然a->b, b->c那么a->c,即然a->c, c->d那么a->d。

二叉树同级节点

Example graph

给定一颗二叉树，找出同级节点： 如b, c同级; d, f同级。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
.decl Parent(n: symbol, m: symbol)
Parent("d", "b").
Parent("e", "b").
Parent("f", "c").
Parent("g", "c").
Parent("b", "a").
Parent("c", "a").

.decl Person(n: symbol)
Person(x) :- Parent(x, _).   // 从子中提取person
Person(x) :- Parent(_, x).   // 从父母中提取person

.decl SameGeneration(n: symbol, m:symbol)
SameGeneration(x, x) :- Person(x). // 做一个自身到自身的关系映射, 做为初始化
SameGeneration(x, y) := Parent(x, p), SameGeneration(p, q), Parent(y, q). // 逻辑： 如果p是x的父母，p和q同级，那么q的孩子y和x也同级(父父同级->子子同级)

.output SameGeneration

image-20211230143847717

注：自己和自己一定同级。

0x03 Data-flow analysis

Reaching definition example

这里有一个程序流图，做一个数据流分析。

Data-flow analysis(DFA) aims to determine static properties of programs.

正向来分析变量v的reaching definition:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
// define control flow graph
// via the Edge relation
.decl Edge(n: symbol, m: symbol)
Edge("start", "b1").
Edge("b1", "b2").
Edge("b1", "b3").
Edge("b2", "b4").
Edge("b3", "b4").
Edge("b4", "b1").
Edge("b4", "end").

// 两个define点互为gen,kill
// Generating Definitions 
.decl GenDef(n: symbol, d:symbol)   
GenDef("b2", "d1").
GenDef("b4", "d2").

// Killing Definitions
.decl KillDef(n: symbol, d:symbol)
KillDef("b4", "d1").
KillDef("b2", "d2").

// Reachable
.decl Reachable(n: symbol, d:symbol)  
Reachable(u,d) :- GenDef(u,d).    
Reachable(v,d) :- Edge(u,v), Reachable(u,d), !KillDef(u,d).

.output Reachable

推导式:

1
2
Reachable(u,d) :- GenDef(u,d).    // 初始化define点, 相当于Gen_B
Reachable(v, d) :- Edge(u, v), Reachable(u, d), !KillDef(u, d). //相当于(IN[B]-killB)

递归地实现了reaching definition 的迭代数据流算法:

截屏2020-05-09 下午9.11.28

参考南大程序分析第三节