Pre

相信很多閱讀龍書/PPA朋友在使用C++之類的語言實(shí)現(xiàn)書上的程序分析算法的時候會感覺到無比頭疼颜阐，甚至是在實(shí)現(xiàn)完成之后還是對算法稀里糊涂的。因?yàn)檫@些書在描述算法的時候往往是基于函數(shù)式語言來實(shí)現(xiàn)的吓肋！在我之前對幾種常用數(shù)據(jù)流分析的實(shí)現(xiàn)中我也選擇了Racket, 實(shí)踐證明Racket在描述這些算法的過程中非常的絲滑凳怨。
不過，在工業(yè)界的實(shí)踐過程中，大多數(shù)算法的實(shí)現(xiàn)最終都是使用C++的肤舞，因?yàn)樵诋a(chǎn)品級別的代碼中性能是非常重要的紫新，特別是隨著算法本身的復(fù)雜度提升，比如說過程間分析李剖，如果使用racket去做弊琴，就顯得非常的捉襟見肘了。C++的性能和程序員的技巧的關(guān)系固然是正相關(guān)但是卻是不成正比的杖爽，相信只要稍微寫過一點(diǎn)C++的人都會明白我在說什么敲董。

那么有沒有一種語言比Racket描述算法更簡單，比C++(至少是90%+的程序員寫的C++)更加快慰安？
試試Datalog吧腋寨！

接下來的文章中我首先會給出Datalog的詳細(xì)介紹，然后介紹如何用Datalog語言來描述PPA中定義的While Language, 并使用Datalog來實(shí)現(xiàn)Live Variable Analysis.

什么是Datalog

Datalog $^1$ 最早是一種在被使用在關(guān)系型數(shù)據(jù)庫中的語言化焕，他的語法非常的簡單直接萄窜，只有如何描述“關(guān)系”。準(zhǔn)確的說Datalog算不得一門真正的語言撒桨，你是沒有辦法找到一門語言就叫Datalog的(就像LISP)查刻，但是有很多實(shí)現(xiàn), 目前最常見，也是最快的實(shí)現(xiàn)是logicblox(商業(yè))和soufflé (開源)凤类。從我個人已知的情況來說穗泵，目前soufflé $^2$ 是logicblox的上位替換。所以在接下來的所有介紹中我會主要使用soufflé谜疤〉柩樱總得來說soufflé這門語言是原本Datalog的擴(kuò)展版。但是里面不是所有東西我都喜歡用夷磕，我會略去那些部分履肃。

語法

定義關(guān)系謂詞

.decl NextNumber(a: number, b: number)

Datalog是一種用來描述關(guān)系的語言，在這里面所有東西都是關(guān)系(Relation). 從常規(guī)編程語言的角度坐桩，這就比較像一個函數(shù)尺棋，這個函數(shù)有兩個參數(shù)a, b，返回是Bool類型绵跷。也就是說在datalog中我們只能定義返回真假的函數(shù)膘螟。

如果relation是一種函數(shù)，那當(dāng)參數(shù)取不同值的時候抖坪，我們返回到底是真還是假呢萍鲸？
在datalog的語義模型中，這取決于我們的Rule和Fact.

Fact

NextNumber(1,2).
NextNumber(2,3).

這行代碼就是說我們告訴Datalog求解器“1的下一個數(shù)是2”擦俐。這是一個Fact, NextNumber(1,2) = True。需要注意的是我們并不能告訴Datalog什么是False,但是可以定義Fact

NotNextNumber(2,1).

soufflé支持直接從文件中讀取Fact

.input NextNumber(IO=file, delimiter=",")

Consequence Rule

Flow(a, b) :- Edge(a, b).
Flow(a, c) :- Flow(a, b), Flow(b, c). 
// if we have facts Edge(1,2) Edge(2,3), we can also infer fact Flow(1,3)

rule是邏輯規(guī)則握侧，等價與

u ? p ∧ q ∧ … ∧ t

這種邏輯表達(dá)式被稱為Horn Clause.
rule可以遞歸定義蚯瞧。

輸出

.output Flow

輸出所有可能的Flow關(guān)系嘿期，用之前的例子就 Flow(1,2),Flow(2,3),Flow(1,3). soufflé如果這么寫會直接輸出結(jié)果到對應(yīng)的文件。

這就是所有的datalog syntax啦埋合！
但是要注意Datalog程序還需要滿足下面的條件

所有的fact必須接地(ground),也就是說在Fact中只能出現(xiàn)值而不能出現(xiàn)變量备徐，Edge(1,a)就是不合法的
所有在rule頭部(:-之前)出現(xiàn)的變量必須在rule體中出現(xiàn)。

這兩條規(guī)則直接保證了Datalog程序是有限的甚颂，一定會停機(jī)蜜猾。換句話說，datalog并不是圖靈完備的振诬。

~~如果你對理論沒啥興趣下面小節(jié)請?zhí)^~~

語義

介紹datalog的語義之前蹭睡，先提一下兩個概念，

外部數(shù)據(jù)庫(EDB)：程序運(yùn)行之前由用戶提供的Facts赶么。
內(nèi)部數(shù)據(jù)庫(IDB)：所有在rule在進(jìn)行邏輯推理運(yùn)算過程中推論出的間接產(chǎn)生的Facts肩豁。

邏輯語義(logic semantic)

我們可以使用經(jīng)典的一階邏輯來描述Datalog的語義。

先介紹背景知識辫呻。

Datalog rule

L0 :- L1, L2, ...., Lm

等價與一個描述為一個滿足斯科倫范式(Skolem Normal Form)的一階邏輯表達(dá)式
$\forall X_1.....\forall X_m(L_1\land .... \land L_m \implies L_0)$

Herbrand Universe(埃爾布朗空間)
對與一個斯科倫化的一階邏輯表達(dá)式S, 他的埃爾布朗空間H可以由如下規(guī)則定義：

S中的所有常量屬于H, 如果S中沒有常量清钥， H包含任意常量c
如果 $t_1\in H, ... t_n \in H$ , 那么 $f(t1, ... ,tn) \in H$

不難看出埃爾布朗空間定義了一階邏輯中的常量和可以推出的常量。而這和Datalog的Facts直接相信大家都已經(jīng)可以感覺出聯(lián)系了放闺。

可以進(jìn)一步定義Herbrand Base(埃爾布朗基礎(chǔ))：
變量全接地的思科倫范式和他的埃爾布朗空間中的表達(dá)式祟昭。
也就是說在一個Datalog程序中，埃爾布朗基礎(chǔ)表示了這個程序的所有Facts.定義的前半部分也叫外埃爾布朗基礎(chǔ)(EHB), 而后半部分則叫內(nèi)埃爾布朗基礎(chǔ)(IHB).

如果S是一個Datalog程序的子句集合怖侦，cons(S) 代表所有S的邏輯推論得出的Facts.

現(xiàn)在我們可以來定義語義了从橘。
Datalog程序P, 可以被描述為一個從EHB到IHB的映射關(guān)系 $M_p$ , 而所有在EHB中的外部數(shù)據(jù)庫E，總有一個映射 $M_P(E) = cons(P \cup E) \cap IHB$
K和L是兩個字面量(不一定接地)础钠，如 $\theta$ 是一個變量替換恰力， $k \theta = L$ , 我們可以說K包攝L,記做 $K ~ \triangleright ~ L$ ,也可以說L是K的一個實(shí)例(instance).
而一個Datalog查詢G(查詢就是比如輸出所有關(guān)系Edge)可以描述為,（順序根據(jù)包攝關(guān)系來）

$\forall E \subseteq EHB, M_{P,G}=\{H | H \in M_p(E) > H \}$

模型論語義(model theory semantic)

我們也可以從模型論的角度來描述Datalog的語義。
模型論是洛文海姆旗吁，斯科倫踩萎，歌德爾等人發(fā)展起來的一門學(xué)科, 感謝我的老師Shukai Chin在我初學(xué)的時候教了我很多這些知識。它主要是使用Interpretation來描述形式化語義很钓。~~我真的不知道怎么翻譯Interpretation香府，我在國內(nèi)的時候理論課就沒上心過。~~
Datalog的interpretation就是如何給表達(dá)式中的變量賦值码倦，每個謂詞到底表達(dá)了什么樣的含義企孩。如果一個子句C在某種interpretation中為真，那么我們稱這個interpretation滿足(satisfy) C袁稽。
對于一條datalog的Consequence Rule, 我們可以有如下的定義勿璃。一個Fact F,和一組子句S, 不論在什么樣的interpretation下都滿足S,那么可以說F follow from S，記做 $S \vDash F$ .
Datalog 這個形式系統(tǒng)滿足一種特殊的interpretation,叫Herbrand Interpretation.這種對一階邏輯的interpretation非常的簡單，對于每一個字面常量补疑，我們可以interpret到他本身歧沪，對于每一個謂詞，我們只能賦已知的常量給其中的變量莲组。

任意一個埃爾布朗解釋都對應(yīng)埃爾布朗基礎(chǔ)中的子集t上诊胞。在這種解釋中所有接地的fact都為true。用數(shù)學(xué)表達(dá)式來寫就是
$t \iff p(c_1, ....,c_n)$

一條datalog rule $L0 :- L1, ..., Ln$ 為真對應(yīng)的就是存在一中變量替換 $\theta$ 能把所有rule中的變量全部替換為常量锹杈。用符號表示就是 $L_1\theta \in t ~ \land ... \land L_n\theta \in t \Rightarrow L_0\theta$ .
進(jìn)一步撵孤，如果一個埃爾布朗解釋 I滿足一組datalog語句S，那我們可以說I是S的一個埃爾布朗模型(Herbrand Model).

而cons(S)可以表達(dá)為

從定義中我們不難看出任意兩個埃爾布朗模型t1,t2, $t_1 \cap t_2$ 依然是一個埃爾布朗模型，這種性質(zhì)被稱作model intersection property。所有基于Horn Clause的形式系統(tǒng)都具有這個性質(zhì)文狱。而其中cons 模型是其他所有模型的子集牡肉，所以也被稱為最小埃爾布朗模型。

證明論語義Proof Theory Semantic

u1s1這部分應(yīng)該是最重要的語義部分因?yàn)樯婕昂芏嗲笾抵惖淖C明，但是我學(xué)得不是很好，暫時跳過。喻圃。。

Datalog 推論的不動點(diǎn)性質(zhì)

直接放結(jié)論吧：
S 是fact和相關(guān)rule的集合粪滤， fact1是從現(xiàn)有fact的1步推斷斧拍，則 Cons(s) 可以表示為：

這里可以看出如果我們的解釋滿足埃爾布朗模型，那么這個解釋就是Ts的不動點(diǎn)杖小，如果是Cons(s)肆汹，他是最小埃爾布朗模型，也意味著他是最小不動點(diǎn)予权。

為什么使用Datalog

其一
從上面的語義中不難看出昂勉，datalog雖然說是Prolog的一個子集，但是他們的語義卻相差非常的多扫腺。Datalog必須是滿足Herband Model的岗照，這樣他的表達(dá)能力其實(shí)受到了非常大的限制，但是如果我們把它用在powerset處理笆环，不動點(diǎn)計算上攒至，這個語義模型卻是非常合適的。目前非常多的程序分析算法都屬于這種情況躁劣，所以使用Datalog來做程序分析從語義上來說是非常非常合適的.
第二
正是因?yàn)閐atalog有大量的限制迫吐，所以他的求值也和prolog之類的邏輯式編程語言區(qū)別非常的大。目前從Bench mark 來看至少soufflé的速度相比其他的約束求解器是非常非痴送快的志膀。 Soufflé的主要工作方式是熙宇，同過templete技巧配合非常高效的數(shù)據(jù)結(jié)構(gòu)(一個trie)實(shí)現(xiàn)從datalog代碼最終生成高效C++代碼的過程。總得來說梧却，肯定是比你自己手寫worklist之類的算法的效率高很多的奇颠。

Comparison of Datalog evaluation tools for random-graphconnectivity problem.

Comparison of Datalog evaluation tools for a context-insensitive points-to analysis on the OpenJDK7 library.

我沒有soufflé和logicblox的對比benchmark败去，但是據(jù)說logicblox的效率至少并沒有比soufflé高放航。

Case Study: 使用fact來表示PPA中的While language

之前的介紹中應(yīng)該不難發(fā)現(xiàn)datalog是基于一階邏輯的一種特殊形式，既然是一階圆裕，自然也就不能實(shí)現(xiàn)rule或者fact的嵌套广鳍。

while language

觀察上面的程序我們不難發(fā)現(xiàn)，編程語言一般都是有互相嵌套與遞歸的結(jié)構(gòu)的吓妆，這一點(diǎn)如果我們使用c++之類的語言可以用對象直接的組合來實(shí)現(xiàn),如果是使用racket之類的函數(shù)式編程赊时。那么利用S表達(dá)式，我們對于AST的表示是非常簡單的行拢，簡直是可以直接輸入代碼啦23333

(define example2-11
  '((1 = x 2)
    (2 = y 4)
    (3 = x 1)
    (if (4 (> y x))
        (5 = z y)
        (6 = z (* y y)))
    (7 = x z)))

但是datalog的情況其實(shí)和c++有點(diǎn)像祖秒，我們沒有高階的數(shù)據(jù)類型，我們只能用類似鏈表的方式舟奠，每一層存放下一級的指針竭缝。datalog甚至更慘，它連指針都沒有沼瘫，我們只能人為的用index去代替指針(想象一下你怎么把一個c++對象放到數(shù)據(jù)庫中)

// in datalog in order to discriminate different facts in relational, we need a id for expression
.decl Var(id: number, name: symbol)
.input Var(IO=file, delimiter=",")
.decl Num(id: number, val: symbol)
.input Num(IO=file, delimiter=",")
.decl Bool(id: number, val: symbol)
.input Bool(IO=file, delimiter=",")
// aexpr struture(aexpr which is only aexpr), all op-a here is just binary
// assume facts are always well-formed (`op` is op-a, left/right are aexpr)
.decl AExprStruct(id: number, op: symbol, leftId: number, rightId: number)
.input AExprStruct(IO=file, delimiter=",")
// similar to AExprStruct
.decl BExprStruct(id: number, op: symbol, leftId: number, rightId: number)
.input BExprStruct(IO=file, delimiter=",")
// relation
.decl RExprStruct(id: number, op: symbol, leftId: number, rightId: number)
.input RExprStruct(IO=file, delimiter=",")
.decl Assign(label: number, var: number, aexprId: number)
.input Assign(IO=file, delimiter=",")
.decl Skip(label: number)
.input Skip(IO=file, delimiter=",")
// if next is -1 means end
.decl Seq(id: number, prev: number, next: number)
.input Seq(IO=file, delimiter=",")
.decl If(id: number, eguardId: number, etrueId: number, efalseId: number)
.input If(IO=file, delimiter=",")
.decl While(id: number, eguardId: number, ebodyId: number)
.input While(IO=file, delimiter=",")

然后再寫一堆的.facts 文件抬纸，當(dāng)然實(shí)踐中fact必須使用別的語言去做parse生成處理。
這也是我覺得目前datalog的弱點(diǎn)之一耿戚，沒有結(jié)構(gòu)化的fact湿故，導(dǎo)致fact rule很不容易閱讀。這種fact被稱為"flatten facts"膜蛔，大量的id讓人難以搞清楚實(shí)際的類型坛猪。soufflé是有類型系統(tǒng)的，但是你們可以看到我只用了symbol和number因?yàn)樗袆e的都只是這兩個alias而已.....我其實(shí)很不喜歡在datalog上用這樣的類型系統(tǒng)皂股，我甚至覺得不如沒有類型來的清爽墅茉。因?yàn)榉凑齠latten以后所有東西都是指針(number)類型。從數(shù)據(jù)庫的角度上來說屑墨，這些只是數(shù)據(jù)庫的外鍵之間互相連接而已躁锁。

Case Study: Live Variable Analysis in Datalog

Live variable 相信大部分看過龍書，PPA的同學(xué)都不會太陌生卵史，是做dead code elimination中的一個步驟战转。主要是判斷在一個給定的程序位置，某一個變量是否“存活”以躯，即有沒有重新定義槐秧。

先看PPA上使用類似一階邏輯的集合語言的描述吧

接下來使用rakcet + chaotic interation算法可以有如下的實(shí)現(xiàn)

;; live variable analysis

;; For each program point, which variable may be live at the exit from the point
;; apparently, this can be used in dead code elimination

;; Yihao Sun
;; 2020 Syracuse

#lang racket

(require "tiny-lang.rkt"
         "flow.rkt")

(provide (all-defined-out))

;; left hand var will will kill a var
;; kill-LV : Blocks* → P(Var*)
(define (kill-LV b)
  (match b
    [`(,label = ,(? variable? x) ,(? aexpr? a)) (set x)]
    [`(,label ,(? bexpr? b)) (set)]
    [`(,label SKIP) (set)]))

;; gen all varible in right
;; gen-LV : Blocks* → P(Var*)
(define (gen-LV b)
  (match b
    [`(,label = ,(? variable? x) ,(? aexpr? a)) (list->set (free-vars a))]
    [`(,label ,(? bexpr? b)) (list->set (free-vars b))]
    [`(,label SKIP) (set)]))

;; entry and exit
(define (LV-chaos s*)
  (define lab* (labels s*))
  (define flow-set? (flow? s*))
  (define init-map
    (for/fold ([res (hash)])
              ([l (in-list lab*)])
      (hash-set res l (set))))
  (define (lv-exit entrym exitm l)
    (define ls-prime
      (for/fold ([res '()])
                ([edge flow-set?])
        (match edge
          [`(,from ,to)
           (if (equal? to l)
               (cons from res)
               res)])))
    (if (empty? ls-prime)
        (hash-set exitm l (set))
        (hash-set exitm l
                  (apply set-union
                         (map (λ (l-prime) (hash-ref entrym l-prime))
                              ls-prime)))))
  (define (lv-entry entrym exitm l)
    (define bl (find-block-by-label s* l))
    (hash-set entrym l
              (set-union (set-subtract (hash-ref exitm l)
                                       (kill-LV bl))
                         (gen-LV bl))))
  (define (iter1 entrym exitm)
    (for/fold ([res-entry entrym]
               [res-exit exitm])
              ([l (in-list lab*)])
      (values (lv-entry res-entry res-exit l)
              (lv-exit res-entry res-exit l))))
  (define (iter-to-fix entrym exitm)
    (let-values ([(next-entrym next-exitm) (iter1 entrym exitm)])
      (begin
        (cond
          [(and (equal? next-entrym entrym)
                (equal? next-exitm exitm))
           (values next-entrym next-exitm)]
          [else
           (iter-to-fix next-entrym next-exitm)]))))
  (iter-to-fix init-map init-map))

總得來說啄踊，其實(shí)kill/gen函數(shù)的部分還算是簡潔直接，基本上可以直接對PPA上的描述進(jìn)行直接翻譯刁标，但是后面的計算不動點(diǎn)的部分著實(shí)是長颠通，而且不容易閱讀，第一次做可能也不知道怎么吧Entry/Exit函數(shù)和原本的算法結(jié)合起來膀懈，不夠直觀顿锰。

下面是datalog的

// live variable analysis

// Yihao Sun
// 2020 Syracuse

#include "flow.dl"

// variable "x" is killed at block "l"
.decl KillLV(x: symbol, l: number)
KillLV(x, l) :- Assign(l, vid, _), Var(vid, x).

// varibale "x" is become alive at block "l"
.decl GenLV(x: symbol, l: number)
GenLV(x, l) :- Assign(l, _, a), FreeIn(x, a).
GenLV(x, l) :- BExprStruct(l, _, _, _), FreeIn(x, l).
GenLV(x, l) :- RExprStruct(l, _, _, _), FreeIn(x, l).

// variable "x" is alive when entry/exit block "l"
.decl EntryLV(x: symbol, l: number)
.output EntryLV
.decl ExitLV(x: symbol, l: number)
.output ExitLV

ExitLV(x, l) :-
   LastStmt(fl), l!=fl,
   FlowReverse(lp, l),
   EntryLV(x, lp).

EntryLV(x, l) :- GenLV(x, l).
EntryLV(x, l) :-
   ExitLV(x, l),
   !KillLV(x, l).

不得不說，確實(shí)是短

那些為空的情況都不再需要去聲明了我們只需要專注于程序pattern match中的interesting case
我們不再需要去手動的計算不動點(diǎn)了启搂，因?yàn)閐atalog的語義保證了我們的計算結(jié)果就是不動點(diǎn)硼控，這一點(diǎn)大大簡化了代碼
對于很多冪集操作我們不再需要輔助函數(shù)去獲取某種特定類型的信息，可以直接用relation胳赌。

總結(jié)

Datalog在寫數(shù)據(jù)流分析上來說是幾乎完美的牢撼，它的語義模型簡直就是為了這個應(yīng)用場景而生的。你需要的不動點(diǎn)計算和冪集操作疑苫，都已經(jīng)在語義當(dāng)中了熏版。而且Soufflé的生成的C++ code, 也是足夠高效，總之捍掺，真香撼短。

完整的代碼還是在我的ppa-in-code 倉庫里

Ref

[1] Ceri, S., Gottlob, G., & Tanca, L. (1989). What you always wanted to know about Datalog(and never dared to ask). IEEE transactions on knowledge and data engineering, 1(1), 146-166.
[2] Jordan, H., Scholz, B., & Suboti?, P. (2016, July). Soufflé: On synthesis of program analyzers. In International Conference on Computer Aided Verification (pp. 422-430). Springer, Cham.
[3] Serge Abiteboul, Richard Hull, and Victor Vianu. 1995. Foundations of Databases: The Logical Level (1st. ed.). Addison-Wesley Longman Publishing Co., Inc., USA.

Dimension Shift! 一起來學(xué)Datalog吧！