前言

前段时间看 Doop 顺手整理了篇 LogiQL 入门,现在整理一下 Soufflé 的使用记录。Soufflé 是一款开源的 Datalog 引擎,相对 LogixBlox 更新更快(至少有论文这么总结),而 Doop 默认使用和维护了一整套 Soufflé 的规则。因为是开源引擎,所以有相关工作直接对 Doop 和 Soufflé 进行修改,用于实现一些分析,然后发了顶会😇😇😇

相关资料真的是少,不然就是难读,反正花时间看呗(摊手),最终目的是看懂 Doop 中的规则。

安装 Soufflé

实验使用 Ubuntu 20.04 进行,souffle、doop(java8)都可以成功安装和使用。

Soufflé 有一个解释器和一个编译器来执行 Datalog 程序,通过脚本安装。PS:万一无法下载,可能是服务器问题(之前也宕机过)

1
2
3
4
5
# 下载
curl -s https://packagecloud.io/install/repositories/souffle-lang/souffle/script.deb.sh | sudo bash

# 安装
sudo apt install souffle -y

使用 Soufflé

一个简单的例子

example.dl 定义“边”和“路径”

  • edge 是一个 .input 关系,将从磁盘读取
  • path 是一个 .output 关系,将被写入磁盘
  • 如果有一条从 x 到 y 的边,那么就有一条从 x 到 y 的路径
  • 如果有一条从 x 到 z 的路径,并且从 z 到 y 有一条边,那么就有一条从 x 到 y 的路径
1
2
3
4
5
6
7
8
9
.decl edge(x:number, y:number)  // 声明
.input edge // 没有指定文件,默认从 edge.facts 中读取

.decl path(x:number, y:number) // 声明
.output path // 输出为 path.csv

// 定义,注意末尾的 . 符号
path(x, y) :- edge(x, y).
path(x, y) :- path(x, z), edge(z, y).

如果输入的 edge 关系是图中的顶点对,根据上面的两个规则,输出的路径关系将提供所有顶点对 x 和 y,即图中存在 x 到 y 的路径。

输入文件 edge.facts,使用制表符分隔:

1
2
1 2
2 3

执行分析,-F 表示输入文件路径,-D 表示输出文件路径:

1
2
souffle -F. -D. example.dl
# souffle -F./input -D./output example.dl

查看输出文件 path.csv,包含所有存在路径的顶点对:

1
2
3
1	2
2 3
1 3

上面运行的是 解释器模式,Soufflé 还支持 编译器模式,将 Datalog 程序转换为 C++ 程序,然后编译生成可执行文件,使用 -o 参数:

1
2
3
4
5
# 生成可执行文件
souffle -F. -D. -oexample example.dl

# 执行分析
./example -F. -D. example.dl

-r 参数用于调试,生成 HTML 格式的调试报告 example.html

1
souffle -F. -D. -rexample.html example.dl

-p 参数用于分析,以下命令将创建一个包含分析信息的日志文件 example.log

1
souffle -F. -D. -pexample.log example.dl

souffle 还提供了一个命令行工具 souffleprof,可用于分析 example.log:

1
souffleprof example.log

例1

Datalog 是一种(声明式)基于逻辑的查询语言,允许用户执行递归查询。Datalog 语法的规范没有统一的标准,通常采用 Prolog 风格的语法。Soufflé 的语法受到 Datalog 实现的启发,即 Z3 中的 bddbddb(BDD-Based Deductive DataBase) 和 muZ。

Soufflé 为大规模面向逻辑的编程提供了软件工程功能(例如组件),对于实际使用,Soufflé 通过算术函子(arithmetic functors)扩展了 Datalog 使其图灵等价,让程序员能够编写非终止的程序。

  • 非终止的一个例子是事实 A(0) 和规则 A(i + 1) :- A(i),没有额外的约束
  • 这导致 Soufflé 尝试输出无限数量的关系 A(n),其中 n >= 0
  • 这在某种程度上类似于 C 等命令式编程语言中的无限 while 循环。但是,算术函子提供的表达能力增强非常方便编程。

传递闭包

集合 X 上的关系 R 是可传递的,如果对于 X 中的所有 x、y、z,当 x R yy R zx R z。下面的示例表示有向图,其中边定义关系,如果元组满足以下两个规则中的任何一个,则元组处于传递闭包(可达关系)中。

  • 实际上,edge 中的所有元素都是可达的(根据基本规则),归纳规则捕获了传递属性,包括像 reachable("a", "d") 这样的元组。
1
2
3
4
5
6
7
8
9
10
11
12
.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

同代

给定一棵树(具有特定根节点的有向无环图),目标是找到哪些节点处于同一级别。

  • 下图中节点 b 和 c 处于同一级别,节点 e 和 g 也处于同一级别。

定义 Parent 关系,然后描述这棵树;定义 Person 关系和 SameGeneration 关系

1
2
3
4
5
6
7
8
9
10
11
12
13
.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(x) :- Parent(_, x). // 父代

.decl SameGeneration (n: symbol, m: symbol)
SameGeneration(x, x):- Person(x). // 自己和自己是同代
SameGeneration(x, y):- Parent(x,p), SameGeneration(p,q), Parent(y,q). // 父代相等时,子代是同代

.output SameGeneration

数据流分析

数据流分析(Data-flow analysis, DFA)旨在确定程序的静态属性,基于控制流图(Call Flow Graphs, CFG),根据节点和图的属性进行程序分析。

一个例子是可达性定义(reaching definition):变量的定义是否到达程序中特定的点。因为变量的赋值可以直接影响程序中另一点的值,这里考虑变量 v 的明确定义 d:

1
d: v = <expression>;

如果从 d 到 u 的所有路径都不包含 v 的任何明确定义,则变量 v 的定义 d 被认为可到达语句 u。注意即使没有明确的定义,函数也可能对变量产生副作用。

考虑以下控制流图,包含变量 v 的明确定义 d1 和 d2,只有 d2 定义的 v 能达到 B3。

以下代码输出 CFG 的所有阶段,其中 v 可能被这些定义之一捕获。

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
// define control flow graph
// via the Edge relation
.decl Edge(n: symbol, m: symbol) // 边 n -> m
Edge("start", "b1").
Edge("b1", "b2").
Edge("b1", "b3").
Edge("b2", "b4").
Edge("b3", "b4").
Edge("b4", "b1").
Edge("b4", "end").

// Generating Definitions
.decl GenDef(n: symbol, d:symbol) // 生成定义 n -> d
GenDef("b2", "d1").
GenDef("b4", "d2").

// Killing Definitions
.decl KillDef(n: symbol, d:symbol) // 销毁定义 n -> d
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). // 边uv,u 点可达且没有销毁定义 d,则 d 可达 v

.output Reachable

关于输入和 C 预处理器的备注

与 C++ 一样,Soufflé 使用两种类型的注释:

  • 类型 1:// 这是备注
  • 类型 2:/* 这也是备注 */

C 预处理器处理来自 Soufflé 的输入(即可以使用宏),例如:

1
2
#include "myprog.dl"
#define MYPLUS(a,b) (a+b)

例2:关系

关系定义

关系必须声明后才能使用,在 Soufflé 代码中编写代码行的顺序不会影响程序的正确性。使用两个字段 a 和 b 声明关系 edge,每个字段都是符号(字符串)。

1
.decl edge(a:symbol, b:symbol)

I/O 指令

用户可以指定用于加载输入和将输出写入文件的指令:

  • 输入指令 .input <relation-name><relation-name>.facts 读取,默认情况下由制表符分隔
  • 输出指令 .output <relation-name> 写入文件,通常是 <relation-name>.csv(默认)或 stdout(取决于选项)
  • 打印关系大小指令 .printsize <relation-name> 将给定关系的基数(cardinality)打印到标准输出。
1
2
3
4
5
6
7
8
9
10
11
12
13
.decl A(n: symbol)
.input A // facts are read from file A.facts

.decl B(n: symbol)
B(n) :- A(n).

.decl C(n: symbol)
.output C // output appears in C.csv
C(n) :- B(n).

.decl D(n: symbol)
.printsize D // the number of facts in D is printed
D(n) :- C(n).

关系可以从以下文件加载或写入以下文件:

  • 任意 CSV 文件
  • 压缩的文本文件
  • SQLite3 数据库

例如,要将评估后的关系存储到 SQLite3 数据库中,用户可以指定如下内容:

1
2
.decl A(a:number, b:number)
.output A(IO=sqlite, dbname="path/to/sqlite3db")

目标

Datalog 中的目标是形式为 false <= p 的逻辑关系,其中 p 是逻辑关系。在 Soufflé 中目标是由输出指令模拟的,优点是可以在一次 Soufflé 程序的执行中评估多个独立的目标。

语法便利

可以编写具有多个头的规则,这是一种语法糖,可以最大限度地减少编码工作。下面是一个利用此功能的代码片段以及未应用转换的等效代码:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
// Multiple heads
.decl A(x:number)
A(1). A(2). A(3).
.decl B(x:number)
.decl C(x:number)
B(x), C(x) :- A(x). // 同时定义
.output B,C

// Single head
.decl A(x:number)
A(1). A(2). A(3).
.decl B(x:number)
B(x) :- A(x).
.decl C(x:number)
C(x) :- A(x).
.output B,C

类似地,规则体中的析取(disjunctions)也可以作为语法糖,例如:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
// Disjunction in rule bodies
.decl edge(x:number, y:number)
edge(1,2). edge(2,3).
.decl path(x:number, y:number)
path(x,y) :-
edge(x,y); // 或
edge(x,q), path(q,y).
.output path

// No disjunction in rule bodies
.decl edge(x:number, y:number)
edge(1,2). edge(2,3).
.decl path(x:number, y:number)
path(x,y) :- edge(x,y).
path(x,y) :- edge(x,q), path(q,y).

例3:属性的类型系统

Soufflé 的类型系统是静态的,就像 C 之类的语言一样,而与 Python 之类的语言不同。必须在编译(或解释)之前定义关系的属性,并在编译时检查类型。让程序员清楚地了解关系的定义及其用法,在运行时不进行动态检查能够最大限度地减少评估时间。

原子类型

Soufflé 有两种基本类型,符号类型 symbol 和数字类型 number。符号类型包含所有字符串,在内部由一个序数(ordinal number)表示。值 ord("hello") 对应于给定程序的这个序数,在这种情况下是字符串 “hello”。数字类型包括所有数字的全域。

例4:算术表达式

Soufflé 允许算术函子,扩展了传统的 Datalog 语义,函子中的变量可能不包含任何自由变量。一个简单的例子,最后一行连接中的第二个条件调用了算术运算符 <

1
2
3
4
.decl A(n: number)
.output A
A(1).
A(x+1) :- A(x), x < 9. // 当 x 小于 9

打印斐波那契数列:

1
2
3
4
5
.decl Fib(i:number, a:number)
.output Fib
Fib(1, 1).
Fib(2, 1).
Fib(i + 1, a + b) :- Fib(i, a), Fib(i-1, b), i < 10.

Soufflé 中允许使用以下算术函子:

  • 加法:x + y
  • 减法:x - y
  • 除法:x / y
  • 乘法:x * y
  • 模数:a % b
  • 幂:a ^ b
  • 计数器:autoinc()
  • 位操作:x band yx bor yx bxor ybnot x
  • 逻辑运算:x land yx lor ylnot x

Soufflé 中允许以下算术约束:

  • 小于:a < b
  • 小于或等于:a <= b
  • 等于:a = b
  • 不等于:a != b
  • 大于或等于:a >= b
  • 大于:a > b

在源码中,数字可以写成十进制、二进制和十六进制:

1
2
3
4
.decl A(x:number)
A(4711).
A(0b101).
A(0xaffe).

数字编码

数字可以用作逻辑值,如在 C 中:

  • 0 代表假
  • != 0 代表真

因此,它们可用于逻辑运算 xland yx lor ylnot x

1
2
3
.decl A(x:number)
.output A
A(0 lor 1).

函子 autoinc()

函子 autoinc() 在每次求值时都会产生一个新数字,但是不允许在递归关系中使用。可用于为符号创建唯一编号(充当标识符),例如:

1
2
3
4
5
6
.decl A(x: symbol)
A(“a”). A(“b”). A(“c”). A(“d”).

.decl B(x: symbol, y: number)
.output B
B(x, autoinc()) :- A(x). // 为 a、b、c、d 各生成一个标识符

给定一个集合 A(x:symbol),创建一个后继关系 Succ(x:symbol, y:symbol) 使得第一个参数包含 A 中的元素 x,第二个参数包含 x 的后继,这也是一个 A 的元素。
例如,集合 A = {"a", "b", "c", "d"} 具有后继关系 Succ=(("a", "b"), ("b", "c"), ("c", "d")}。假设一个元素(在这种情况下是一个符号)的总顺序根据它的序数计算,内部表示为一个数字。

1
2
3
4
5
6
7
8
9
10
11
.decl A(x:symbol) input         // 集合
.decl Less(x:symbol, y:symbol)
Less(x,y) :- A(x), A(y), ord(x) < ord(y). // 排序关系:x < y

.decl Transitive(x:symbol, y:symbol)
Transitive(x,z) :- Less(x,y), Less(y,z). // 传递关系:x < y && y < z => (x, z)

.decl Succ(x:symbol, y:symbol)
Succ(x,y) :- Less(x,y), !Transitive(x,y). // 后继关系:x < y && 不存在传递关系

.output Less, Transitive, Succ

计算后继关系的第一个和最后一个元素。

1
2
3
4
5
.decl First(x: symbol) output
First(x) :- A(x), !Succ(_, x). // 没有前驱

.decl Last(x: symbol) output
Last(x) :- A(x), !Succ(x, _). // 没有后继

例5:聚合

Soufflé 中的聚合是指使用特定的函子来汇总有关查询的信息,聚合类型包括计数、求最小值/最大值、求和。在 Soufflé 中,信息通常不能从子目标(聚合函子的参数)流到外部作用域。例如,如果希望找到关系 Cost(x) 的最小值,无法找到使成本最小化的特定 x 值,因为这样的 x 值可能不是唯一的。

计数

计数函子用于计算子目标的集合大小,语法为 count:{<sub-goal>}

以下示例输出“蓝色”汽车的数量,即 Car 中第二个参数为“蓝色”的元素数量:

1
2
3
4
5
6
7
8
9
.decl Car(name: symbol, colour:symbol)
Car("Audi", "blue").
Car("VW", "red").
Car("BMW", "blue").

.decl BlueCarCount(x: number)
BlueCarCount(c) :- c = count:{Car(_, "blue")}.

.output BlueCarCount

最大值/最小值/求和

max 函子输出集合的最大值,语法为 max <var>:{<sub-goal(<var>)>}

1
2
3
4
5
6
7
.decl A(n:number)
A(1). A(10). A(100).

.decl MaxA(x: number)
MaxA(y) :- y = max x:{A(x)}.

.output MaxA

最小值语法为 min <var>:{<sub-goal>(<var>)>};求和语法为 sum <var>:{<sub-goal>(<var>)>}

Soufflé 程序

主要整理 Doop 中用到的一些内容,包括基本的关系、类型、规则,以及进阶的自定义函子、组件、编译指令。(这不是全包含了吗😅)

  • 语言(Language)
  • 关系(Relations)
  • 类型(Types)
  • 规则(Rules)
  • 组件(Components)
  • 用户定义函子(User-Defined Functors)
  • 编译指令(Pragma)

组成

语言

Soufflé 中的主要语言元素是关系声明(relation declarations)、事实(facts)、规则(rules)和指令(directives)。

例如,以下程序中包含两个关系 A 和 B,关系必须声明(以便编译时检查属性的使用);关系 A 有两个事实:A(1,2).A(2,3).,事实是无条件成立的规则,即事实是 Horn Clause A(1,2) ⇐ true;关系 B 有两个规则:B(x,y) :- A(x,y).B(x,z) :- A(x,y), B(y,z).,表示 Horn Clause B(x,y) ⇐ A(x,y)B(x,y) ⇐ A(x,y), B(y,z)

最后的指令 .output B 表示在执行结束时查询关系 B,并将其写入文件或打印到屏幕中。关系声明、事实、规则和指令的顺序可以是任意的,并不影响最终的执行。

1
2
3
4
5
6
7
8
9
.decl A(x:number, y:number)  // declaration of relation A
A(1,2). // facts of relation A
A(2,3).

.decl B(x:number, y:number) // declaration of relation B
B(x,y) :- A(x,y). // rules of relation B
B(x,z) :- A(x,y), B(y,z).

.output B // Output relation B

关系

Soufflé 要求声明关系,关系是一组有有序元组 (x1, ..., xk),其中每个元素 xi 都是由类型定义的数据域的成员。以下声明定义了仅包含数字对的关系 A,第一个属性被命名为 x,第二个属性被命名为 y,两个属性的类型都是数字。

1
.decl A(x:number, y:number).

Soufflé 的类型检查器将推断规则中的变量类型,并检查它们是否正确使用。

类型

Soufflé 利用类型化的 Datalog 方言进行静态检查,从而能够提早发现查询规范中的错误。必须为关系的任何属性指定类型,Soufflé 中有四种原始类型:符号(symbol)、数字(number)、无符号数字(unsigned)、浮点数(float)。

规则

规则是条件逻辑语句,以头部开始,然后是身体。例如,如果一对 (x, y) 在 B 中则 A 成立:

1
A(x,y) :- B(x,y).

组件

Soufflé 有组件这个概念,可用于模块化大型逻辑程序。一个组件可能包含其他组件、关系、类型声明、事实、规则和指令;组件必须声明和实例化后才可以使用,每个组件都有自己的命名空间;组件可以继承一个或多个超级组件。

用户定义函子

可以使用用户定义函子扩展 Soufflé,用户定义函子用 C/C++ 实现。用户定义函子有两种风格:朴素函子和有状态的函子,有状态的函子公开记录和符号表。

编译指令

用编译指令配置 Soufflé,例如,可以在源码中设置命令行选项。

组件 Components

组件是程序的模块化部分,可以封装元素,包括关系声明、类型声明、规则、事实、指令和其他组件。组件包含声明和实例化两个操作。

使用 .comp 关键字声明组件,组件包含的元素定义在 {...} 内:

1
2
3
4
5
.comp MyComponent {
.type myType = number // type
.decl TheAnswer(x:myType) // component relation
TheAnswer(42). // component fact
}

使用 .init 关键字初始化组件,在内部,Soufflé 将组件实例扁平化(flatten),并为每个组件实例创建命名空间,因此要用限定名称调用其中的元素。

1
2
3
4
5
.init myInstance1 = MyComponent         // 实例化

.decl Test(x:number)
Test(x) :- myInstance1.TheAnswer(x). // . 限定
.output Test

对于上面的例子,Soufflé 在内部对组件实例进行了如下扩展:

1
2
3
4
5
6
7
.type myInstance1.myType = number
.decl myInstance1.TheAnswer(x:myType) // relation of myInstance1
myInstance1.TheAnswer(42). // fact of myInstance1

.decl Test(x:number)
Test(x) :- myInstance1.TheAnswer(x).
.output Test

可以使用 souffle --show=transformed-datalog xxx.dl > expansion.dl 生成扩展后的 datalog 文件。

下面定义了两个 MyComponent 实例:

1
2
3
4
5
6
7
8
.init myInstance1 = MyComponent
.init myInstance2 = MyComponent
myInstance2.TheAnswer(33).

.decl Test(x:number)
Test(x) :- myInstance1.TheAnswer(x).
Test(x) :- myInstance2.TheAnswer(x).
.output Test

Soufflé 在内部生成以下逻辑程序,通过前缀避免名称冲突:

1
2
3
4
5
6
7
8
9
10
11
12
.type myInstance1.myType = number
.decl myInstance1.TheAnswer(x:myType) // relation of myInstance1
myInstance1.TheAnswer(42). // fact of myInstance1
.type myInstance2.myType = number
.decl myInstance2.TheAnswer(x:myType) // relation of myInstance1
myInstance2.TheAnswer(42). // fact of myInstance1
myInstance2.TheAnswer(33).

.decl Test(x:number)
Test(x) :- myInstance1.TheAnswer(x).
Test(x) :- myInstance2.TheAnswer(x).
.output Test

如果规则/事实在没有关系声明的组件中定义,Soufflé 不会预先添加前缀,而是会将解析推迟到实际的组件实例化。

1
2
3
4
5
6
7
8
9
10
11
12
.decl Out(x:number) 
.comp A {
.decl R(x:number)
.comp Count { // 在组件内部定义组件
R(1). // fact accessing R outside of Count
R(x+1):- R(x), x<10. // rule accessing R outside of Count
}
.init myCount = Count // instantiate Count
Out(x) :- R(x). // rule accessing Out outside of A
}
.init myA = A
.output Out

Soufflé 会将代码扩展,实际会是这样:

1
2
3
4
5
6
7
.decl Out(x:number) 
.decl myA.R(x:number)
myA.R(1).
myA.R((x+1)) :- myA.R(x), x < 10.
Out(x) :-
myA.R(x).
.output Out

如果规则和事实在本地作用域中被实例化,那么前缀将被预先添加到前面。

类型参数化

组件可以通过未限定的类型名称进行参数化,下面的例子实例化了两个不同的类型的组件:

1
2
3
4
5
6
7
.comp ParamComponent<myType> {
.decl TheAnswer(x:myType) // component relation
TheAnswer(42). // component fact
.output TheAnswer // component output directive
}
.init numberInstance = ParamComponent<number>
.init floatInstance = ParamComponent<float>

在内部,Soufflé 将显式实例化不同属性的组件:

1
2
3
4
5
6
7
.decl numberInstance.TheAnswer(x:number)     // relation of numberInstance
numberInstance.TheAnswer(42). // fact of numberInstance
.output numberInstance.TheAnswer // output directive of numberInstance

.decl floatInstance.TheAnswer(x:float) // relation of floatInstance
floatInstance.TheAnswer(42). // fact of floatInstance
.output floatInstance.TheAnswer // output directive of floatInstance

组件名称也可以用参数传递,例如,实例化时指定生成组件 One:

1
2
3
4
5
6
7
8
9
10
11
12
.decl R(x:number)
.comp Case<Selector> {
.comp One {
R(1).
}
.comp Two {
R(2).
}
.init selection = Selector // instantiation depending on type parameter "Selector"
}
.init myCase = Case<One>
.output R

在内部将生成以下程序:

1
2
3
.decl R(x:number) 
R(1).
.output R

继承

一个组件可以继承多个超级组件,超级组件的元素将被传递给子组件。使用 : 继承超级组件,用 , 分隔:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
.comp Base1 {
.type myNumber = number
.decl TheAnswer(x:myNumber)
TheAnswer(42).
}
.comp Base2 {
TheAnswer(41).
}
.comp Sub : Base1, Base2 { // inherit from Base1 and Base2
.decl WhatIsTheAnswer(n:myNumber)
WhatIsTheAnswer(n) :- TheAnswer(n).
.output WhatIsTheAnswer
}
.init mySub = Sub

组件 Base1 和 Base2 将所有组件元素传递给子组件 Sub,在内部实例化 mySub 时生成以下代码:

1
2
3
4
5
6
7
.type mySub.myNumber = number
.decl mySub.TheAnswer(x:mySub.myNumber)
.decl mySub.WhatIsTheAnswer(n:mySub.myNumber)
mySub.TheAnswer(42).
mySub.TheAnswer(41).
mySub.WhatIsTheAnswer(n) :- mySub.TheAnswer(n).
.output mySub.WhatIsTheAnswer

可重写的关系

如果在超级组件中将关系声明为可覆盖(overridable),则子组件可以重写关联的规则和事实。例如

1
2
3
4
5
6
7
8
9
10
11
12
.comp Base {
.decl R(x:number) overridable
R(1).
R(x+1) :- R(x), x < 5.
.output R
}
.comp Sub : Base {
.override R
R(2).
R(x+1) :- R(x), x < 4.
}
.init mySub = Sub

子组件丢弃事实 R(1). 和规则 R(x+1) :- R(x), x < 5.,然后进行重写,在内部实例化 mySub 时生成以下代码:

1
2
3
4
5
6
.decl mySub.R(x:number)overridable 
mySub.R(2).
mySub.R((x+1)) :-
mySub.R(x),
x < 4.
.output mySub.R

例如,可以用 PrecisePointsto 继承和覆盖 AbstractPointsto 的 HeapAllocationMerge 关系,实现更精确的分析:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
.comp AbstractPointsto{
.decl HeapAllocationMerge(heap,mergeHeap) overridable
HeapAllocationMerge(heap,"<<string-constant>>") :-
StringConstant(heap).
// ...
}

.comp PrecisePointsto : AbstractPointsto{ // 继承
.override HeapAllocationMerge // 覆盖
HeapAllocationMerge(heap,"<<string-constant>>") :-
StringConstant(heap),
!ClassNameStringConstant(heap),
!SimpleNameStringConstant(heap).
}

.init precise_pointsto = PrecisePointsto

类型参数化和继承

超级组件的类型参数可以在子组件声明中明确指定,下面定义了一个带参数 K 的子组件 B,用于实例化带参数 K 的超组件 A:

1
2
.comp A<T> { .... }
.comp B<K> : A<K> { ... }

类型参数也可以用作基类,基于类型参数 T 选择性继承,A<T> 的实例定义继承的超级组件:

1
.comp A<T> : T { ... }

通过继承,可以实现复杂的组件实例化,注意这里要引入一个新的组件,因为参数 Graph<number> 不是简单的标识符:

1
2
3
4
5
6
// 错误
.init reach = Reachability<Graph<number>> // syntax error

// 正确
.comp NumberGraph : Graph<number> { } // NumberGraph inherits
.init reach = Reachability<NumberGraph>

编译指令 Pragma

允许直接在源码中设置命令行标志和配置,例如下面的代码将在调用 souffle 时指定 --legacy 标志:

1
2
3
.pragma "legacy" 
.decl A(x:number) output
A(1).

有一些配置不能用命令行标志设置,因此也就不能用这种方法设置。

结语

想更深入地了解 Datalog 可以看看 Datalog and Recursive Query Processing,还有学长推荐的 Dimension Shift! 一起来学Datalog吧!,这方面我倒是没有扩展地去看;Doop 框架的提出可以看 Strictly Declarative Specification of Sophisticated Points-to Analyses,具体的指针分析实现可以参考 Pointer Analysis

Doop 虽然很强大,但是学起来比较困难,而且我还没什么 Java 基础… 费劲。

参阅