之前我簡單的介紹過幾種常見的過程內(nèi)分析算法邻耕。 可以看到這些算法有非常大的相似性冲呢，本質(zhì)都是使用一個(gè)worklist里面存放需要分析的語句舍败，再使用Kill/Gen 函數(shù)（或者說方程）對(duì)系統(tǒng)的約束條件進(jìn)行求解，最終得到想要的結(jié)果敬拓。 很自然的就可以想到有沒有一種理論可以把之前提到這幾種過程內(nèi)分析算法給統(tǒng)一起來邻薯，變成一種框架式的代碼，這樣比較方便我們使用和reason乘凸。

使用代數(shù)結(jié)構(gòu)來抽象問題厕诡， 以得到框架化的結(jié)構(gòu)，是程序分析中的常用思路营勤，并且使用抽象代數(shù)結(jié)構(gòu)灵嫌，在證明的時(shí)候也會(huì)比較容易一點(diǎn)。格(lattice)就是被廣泛使用的一種代數(shù)結(jié)構(gòu)葛作。

偏序集(Partial Order Set) 與格(Lattice)

在介紹格之前先簡單介紹一下偏序集(partial order set)寿羞。 因?yàn)楦袷嵌x在他上面的。
偏序關(guān)系沒啥好多說的赂蠢，如果你沒有學(xué)習(xí)過代數(shù)知識(shí)其實(shí)也很好理解绪穆，通俗的說就是元素之間有大小關(guān)系，但是不是每一個(gè)元素互相都有大小關(guān)系虱岂，有些沒法比較玖院，經(jīng)典例子就是拓?fù)漤樞颉?br> 偏序集是一個(gè)二元組 其中

• 是一個(gè)P上的二元關(guān)系，
• 滿足自反性第岖，反對(duì)稱性难菌， 傳遞性

如果在一個(gè)偏序集中， 存在一個(gè)任意兩個(gè)元素都有唯一的上界和下界那么這個(gè)偏序集合構(gòu)成一個(gè)格(lattice)蔑滓。
根據(jù)定義不難發(fā)現(xiàn)郊酒，兩元素之間一定存在取上界和取下界的函數(shù)遇绞，可定義如下：
是meet操作符， 可以求出x 猎塞，y的上界

• ,
• 若 , 并且,那么有

是join操作符试读， 可以求出x 杠纵，y的下界

• ,
• 若 , 并且,那么有

如果上述的join和meet操作只有一個(gè)被定義了荠耽，這種代數(shù)結(jié)構(gòu)被稱作半格(semi-lattice)

如果我們繼續(xù)增加限制，meet和join操作必須對(duì)所有P的子集都有定義比藻，那么這種格也被稱作完全格(complete lattice).
性質(zhì)：
一個(gè)完全格必有一個(gè)全局的最大值(top)和一個(gè)最小值(bottom), 記做,
所以可以完全格也可以用以下的六元組來表示

回到程序分析上來說铝量，因?yàn)槲覀冃枰蠼獾膯栴}的最終都是要通過迭代求得一個(gè)不動(dòng)點(diǎn)，在計(jì)算的過程中银亲，中間的結(jié)果就一定是有某種順序的慢叨，但是大多數(shù)情況下這種順序又是偏序的，而且因?yàn)槲覀兊牡瘮?shù)每一步都必然有結(jié)果务蝠， 所以使用格這一代數(shù)結(jié)構(gòu)是比較完美符和要求的拍谐。
比如求解available expression的過程就可以用下面的格來表述：

available expression

常數(shù)傳播(constant propagation)就可以用如下格：

constant propgation

Worklist 算法

之前的文章我已經(jīng)實(shí)現(xiàn)過混沌迭代(chaotic iteration)求解數(shù)據(jù)流分析的問題。在那個(gè)算法中馏段，我們判斷不動(dòng)點(diǎn)的時(shí)候每次都要把整個(gè)step函數(shù)的結(jié)果和之前一次的執(zhí)行結(jié)果去比較轩拨。這個(gè)思路非常的直接，其實(shí)對(duì)于數(shù)據(jù)流分析院喜，我們有更加簡單的判斷方法亡蓉。
我們可以在這個(gè)算法的基礎(chǔ)上添加一個(gè)worklist來統(tǒng)合我們的算法，比如一個(gè)Forward Must Analysis就可以用如下算法實(shí)現(xiàn)

Out(s) = ? for all statements s
W := { all statements }                    (worklist) 
repeat {
    Take s from W
    In(s) := ∩s′? pred(s) Out(s′)
    temp := Gen(s) ∪ (In(s) - Kill(s))
    if (temp != Out(s)) { 
        Out(s) := temp 
        W := W ∪ succ(s)
    }
} until W = ?

單調(diào)性(monotonicity)與算法終止的證明

根據(jù)偏序集的性質(zhì)我們不難在偏序集（為定義域）上定義單調(diào)函數(shù)
f是單調(diào)的(monotonic)：假如 那么
在上面的worklist算法中喷舀，觀察

In(s) := ∩s′? pred(s) Out(s′)
temp := Gen(s) ∪ (In(s) - Kill(s))
也可以內(nèi)連一下---> 
temp := fs(∩s′? pred(s) Out(s′))

其中也叫傳遞函數(shù)(transfer function)
可以發(fā)現(xiàn)這一迭代的核心計(jì)算部分（計(jì)算temp）的過程就是一個(gè)單調(diào)的函數(shù)(Forward Must請(qǐng)自動(dòng)帶入available express和上面有過的lattice圖)

從前面的格圖上我們可以看出來砍濒，格是有類似高度的屬性的。
首先定義下鏈(chain):
Y是偏序集P的一個(gè)子集硫麻，并有.
通俗的說就是格這個(gè)圖里的一條路徑爸邢。因?yàn)槎际怯眯∮阪溄拥乃赃@是一條下降的路徑被稱為降鏈(Descending Chain)
接下來可以定義格的高度(height)了：
格中最長的降鏈被稱為格的高度。

在定義了單調(diào)函數(shù)和格的高度之后之后我們可以這樣來證明算法可終止拿愧。
因?yàn)樯鲜稣麄€(gè)迭代函數(shù)中甲棍， 要么是W在減小，要不是Out(s)在減小赶掖，所以感猛，整個(gè)迭代函數(shù)必然是單調(diào)遞減的。從格的角度來說奢赂，因?yàn)楦袷怯邢薷叩呐惆祝詫?duì)于任意給定的程序語句集合s, (AExp,具體的可以翻之前PPA的小節(jié)), Out(s)只能遞減有限次。故算法可終止膳灶。并且算法的時(shí)間復(fù)雜度為 ,

• n是語句集合s的大小
• k是格的高度
• 假設(shè)meet的時(shí)間復(fù)雜度是1

進(jìn)一步抽象前向分析算法

我們可以把之前Forward Must算法中傳遞函數(shù)稍微做一下修改咱士，把原本的集合操作替換成meet操作符立由，就得到了一個(gè)更加泛化的算法。 Must和May不過是算法先從開始然后選取合適的meet函數(shù),給出符合要求的格P序厉。

temp := fs(?s′? pred(s) Out(s′))

總結(jié)如下：
Available Expression

• P = 所有語句
• =
• = 所有語句

reach definition

• P = 賦值語句
• =
• =

分配率(distributive)

如果一個(gè)偏序集上的函數(shù)滿足分配率锐膜，那么
如果有
則
定義其實(shí)和一般的函數(shù)分配率沒有什么區(qū)別
不難發(fā)現(xiàn)我們之前說過的所有kill/gen style的分析算法都符合這一點(diǎn)， 我們?cè)贛eet函數(shù)操作的過程中并沒有發(fā)生信息的丟失弛房。

滿足交換率的問題我們可以統(tǒng)一抽象為meet over all path(MOP) solution.
(其實(shí)我應(yīng)該先定義路徑(Path)是算法從程序起點(diǎn)到運(yùn)行到哪個(gè)block入口的遍歷過程)
定義如下：

• 是傳遞函數(shù)
• 如果p是路徑, 有代入f后
• paths(s) 是從entry到sd的路徑
• 

那么有沒有不符合分配率的算法呢道盏？當(dāng)然是有的，最經(jīng)典的例子是常量傳播(constant propgation)算法文捶。
具體的等下一次我寫Constant Prop的時(shí)候再證明好啦荷逞。

這一次的文章基本完全翻譯自Kris導(dǎo)師的slides
因?yàn)檎娴姆浅：茫郧暗谝淮巫xPPA這個(gè)章節(jié)的時(shí)候真的云里霧里的粹排。

btw, proud of my code here!
我的實(shí)現(xiàn)