# 预备知识

## 逻辑式语言

Logic programming is a programming paradigm which is largely based on formal logic. Any program written in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic programming language families include Prolog, answer set programming (ASP) and Datalog. In all of these languages, rules are written in the form of _clauses_:

In ASP and Datalog, logic programs have only a declarative reading, and their execution is performed by means of a proof procedure or model generator whose behaviour is not meant to be controlled by the programmer. However, in the Prolog family of languages, logic programs also have a procedural interpretation as goal-reduction procedures:

The declarative reading of logic programs can be used by a programmer to verify their correctness. Moreover, logic-based program transformation techniques can also be used to transform logic programs into logically equivalent programs that are more efficient.

## Datalog

wiki 介绍：

It is often used as a query language for deductive databases. In recent years, Datalog has found new application in data integration, information extraction, networking, program analysis, security, cloud computing and machine learning.[1][2]

1. statements of a Datalog program can be stated in any order.
2. Datalog queries on finite sets are guaranteed to terminate. This makes Datalog a fully declarative language.
3. disallows complex terms as arguments of predicates, e.g., p(1, 2) is admissible but not p(f(1), 2)
4. imposes certain stratification restrictions on the use of negation and recursion. 谓词上的环状依赖不能包含否定规则，简单的说，不管如何推理，不能最终出现 ¬P→P，这样矛盾的形式。
5. requires that every variable that appears in the head of a clause also appear in a nonarithmetic positive (i.e. not negated) literal in the body of the clause。这需要了解逻辑式语言的一般形式，可以见 wiki 最开头的说明。目的就是避免无意义的永真或者永假，或者真值无法通过给出的变量确定的情况。
6. requires that every variable appearing in a negative literal in the body of a clause also appear in some positive literal in the body of the clause[5]（暂时不懂为啥这么定义）
7. Query evaluation with Datalog is based on first-order logic, and is thus sound and complete. 先解释 first-oder logic，中文叫做一阶逻辑或者谓词逻辑。sound 指上近似，程序分析术语，大致意思是按照规则筛选，那么结果一定是复合预期的。complete 指符合规则的一定会被全部筛选出来。
8. Datalog is not Turing complete, and is thus used as a domain-specific language that can take advantage of efficient algorithms developed for query resolution.
9. Solving the boundedness problem on arbitrary Datalog programs is undecidable,[10] but it can be made decidable by restricting to some fragments of Datalog. 不可判定性的处理，这里 fragment of a logical language or theory is a subset of this logical language obtained by imposing syntactical restrictions on the language.

## 逻辑式语言例子

These two lines define two facts, i.e. things that always hold:

This is what they mean: xerces is a parent of brooke and brooke is a parent of damocles. The names are written in lowercase because strings beginning with an uppercase letter stand for variables.

These two lines define rules, which define how new facts can be inferred from known facts.

meaning:

• X is an ancestor of Y if X is a parent of Y.
• X is an ancestor of Y if X is a parent of some Z, and Z is an ancestor of Y.

This line is a query:

It asks the following: Who are all the X that xerces is an ancestor of? It would return brooke and damocles when posed against a Datalog system containing the facts and rules described above.

# souffle

## 介绍

Soufflé is a logic programming language inspired by Datalog. It overcomes some of the limitations in classical Datalog. For example, programmers are not restricted to finite domains, and the usage of functors (intrinsic, user-defined, records/constructors, etc.) is permitted.

One of the major challenges in logic programming is performance and scalability. Soufflé applies advanced compilation techniques for logic programs. We use a range of techniques to achieve high-performance.

declarative rules are efficiently translated to efficient C++ programs on modern computer hardware, including multi-core computers

Soufflé was initially designed for crafting static analysis in logic at Oracle Labs. Since then, there have been many other applications written in the Soufflé language, including applications in reverse engineering, network analysis and data analytics.

Soufflé provides the ability to rapid prototype and make deep design space explorations possible. A wide range of applications have been implemented in the Soufflé language, e.g., static program analysis for Java DOOP, parallelizing compiler framework Insieme, binary disassembler DDISASM, security analysis for cloud computing, and security analysis for smart contracts Gigahorse, Securify, Secuify V2.0, VANDAL. More applications are listed here.

# 基础使用

## 编译

-c 的功能和 -o 类似，差别在于 -c 会在编译之后，立刻执行程序。

# 语法

Facts are just atomic formulas, rules are atomic formulas followed by a condition — one or more atomic formulas conjoined. Explicit disjunctions are not needed. A question consists of one or more atomic formulas conjoined.

Atomic formulas consist of a predicate, optionally followed by a parenthesised list of one or more parameters separated by commas.

Parameters are individual constants — now called names, starting with a lowercase letter, or they are individual variables — or just variables, starting with an uppercase letter. Names have their obvious meaning, whereas variables are either quantified — in facts and rules, or they are to be bound in queries.

There is no unified standard for the specification of Datalog syntax. Thus, each implementation of Datalog may differ. A principle goal of the Soufflé project is speed, tailoring program execution to multi-core servers with large amounts of memory.

## 数据类型

number可以是 10 进制，2 进制，16 进制。

## IO

facts 可以直接写在程序里，也可以通过 .input 从文件读取，默认的间隔用 TAB，输入的文件名字必须和 .decl 名字相同，而且后缀是 .fact

## 一阶逻辑

:- 是逻辑推导的符号，表示 .decl 定义的关系之间的联系，而且定义方式相当自由，允许递归等形式，但是不能是互相矛盾的式子。

## 算术表达式

souffle 做了一定的函子拓展，支持部分内置算术表达式。例如，可以在推导时加上条件

### 算术操作

• Addition: x + y
• Subtraction: x - y
• Division: x / y
• Multiplication: x * y
• Modulo: a % b
• Power: a ^ b
• Counter: autoinc()
• Bit operations: x band y, x bor y, x bxor y, and bnot x
• Logical operations: x land y, x lor y, and lnot x

### 算术比较

The following arithmetic constraints are allowed in Soufflé:

• Less than: a < b
• Less than or equal to: a <= b
• Equal to: a = b
• Not equal to: a != b
• Greater than or equal to: a >= b
• Greater than: a > b

## 内置函子

ord() 会生成此程序中这个 symbol 类型的序号，比如 a 的序号应该小于 b

cout: 统计满足条件的 fact 个数，基本语法是 count:{集合与条件}

max: 很好理解，注意还要制定选择哪一个变量。

min: 和 max 用法完全相同。

sum: 也需要指定变量。

contains(string1, string2) : string2 是否包含 string1

match: 含有通配符的匹配，但是文档里没有说明有哪些通配符，读者暂时只记住下面的例子即可。

# 应用实例

## 数据流分析

data-flow analysis（DFA），数据流分析基于控制流图，是比较典型的用节点和图表示程序运行过程的分析方法。具体可以见博客的软件分析部分。

## 偏序关系

Given a set A(x:symbol), create a successor relation Succ(x:symbol, y:symbol) such that the first argument contains an element x in A, and the second argument contains the successor of x, which is also an element of A. For example, the set A = {"a", "b", "c", "d"} would have successor relation Succ=(("a", "b"), ("b", "c"), ("c", "d")}. Assume that the total order of an element (a symbol in this case) is given by its ordinal number, its internal representation as a number. For example, ord("hello") returns the ordinal number of string "hello" for a given program.

P:x⩽a

，则

## 简单指针分析和别名分析

• 指针分析解答的是一个指针可能指向哪个对象的问题
• 别名分析解答的是两个指针是否能指向同一个对象的问题，如果是就认为二者互为别名。

# 参考

• https://souffle-lang.github.io/docs.html
• http://nickelsworth.github.io/sympas/16-datalog.html
• Datalog and Recursive Query Processing 建议当作工具书去查，除非你要深入研究 datalog

# 附录一数理逻辑定义

1. literal: 原子公式 x 或者是原子公式的否定式 ¬x
2. clause: 有限的 literal 和逻辑连接词构成的命题公式。
3. facts：绝对成立的命题。
4. monotonic：因为蕴含而保持“单调的”
5. sequent calculi ：根据单调关系推导
6. Non-monotonic logic：非单调逻辑，简单地说结论不是蕴含关系。
7. words: 也叫做 string，也就是一系列的字符。
8. letters: 也叫做 symbol，非常基础的东西，可以理解为符号。
9. formal language: 由 words 构成的规则集合，words 由 letters 构成，letters 从给定的字符集中选取。
10. Well-formed formula: 形式语言字符集中的字符以特定规则构成的有限的命题公式。缩写 WFF。
11. sentence: 无自由变量的 WFF。
12. Stratification