数据流
數據流
引子
編譯器后端會對前端生成的中間代碼做很多優化,也就是在保證程序語義不變的前提下,提高程序執行的效率或減少代碼size等優化目目標。優化需要依靠代碼分析給出的"指導信息"來相應地改進代碼,而代碼分析中最重要的就是數據流分析。另外數據流分析是程序靜態分析的基礎。所以掌握數據流分析對編譯后端極為重要。
何為數據流分析
數據流分析指的是一組用來獲取有關數據如何沿著程序執行路徑流動的相關信息的技術
數據分析的目的是提供一個過程(或一大段程序)如何操作其數據的全局信息。
從上面的表述中,我們可以看到數據流分析通過靜態代碼來"推斷"程序執行的相關信息,數據流分析并不真正執行程序。雖然數據流分析和符號執行在某些方面比較相似,但還是兩種不同的概念,更確切的說數據流分析是符號執行的基礎。
數據流分析和符號執行從某些方面都很相似,例如符號執行有程序點(ProgramPoint)的概念,并且在當前程序存儲著程序運行到此刻的所有狀態和值信息(一般情況下不會維護歷史程序點的信息,開銷太大)。數據流分析中也有程序點的概念,程序點存儲著數據流信息。兩者都是在CFG(Control Flow Graph)圖的基礎上,進行的分析。Clang的靜態分析示意圖如下所示,Clang會時刻維護符號執行當前的狀態和內存信息。從這一點上看,符號執行和虛擬機更為相似。
但數據流分析和符號執行還是不同的,雖然都有程序點,但程序點存儲的信息卻是兩個不同的概念。數據流分析中程序點存儲的是數據流值,這些數據流值是和具體的數據流問題相關的,有可能是當前程序點的定值信息,也可能是可用表達式信息,這些信息標識這該程序內含的一些屬性。符號執行中程序點存儲的是程序符號執行到此處的所有狀態和值信息,這些信息和程序運行更為相關。
而且兩者的分析方法也不同,符號執行是單次執行,而數據流分析大多采用迭代分析的框架,然后在迭代分析的過程中不斷更新程序點的數據流信息,最終得到比精確解更?。ǜJ兀┑慕?。但為了進行更為激進的優化,要求數據流分析在保證保守的同時又盡可能是激進的。
數據流抽象
在前面的文章中我們也提到過,程序的執行可以看作是程序狀態的一系列轉換。程序狀態是由程序中所有的變量的值以及運行時棧幀上的相關值組成。程序語句對應著轉換函數,將前一個程序點的輸入程序轉換到下一個程序點的新的輸出狀態。
上圖所示中的紅點表示的就是程序點,數據流轉換函數就是作用在程序點上的狀態,并沿著程序路勁一步步進行的。其實這個過程就是一個自動機,抽象出的自動機如下所示。程序點代表自動機中的一個節點,程序語句或者說是轉換函數代表自動機中的一條邊。一般來說,一個程序有無窮多條可能的執行路徑,執行路徑的長度并沒有上屆(例如死循環)。程序分析可以推斷出各個程序點的程序狀態(有窮的特性集合),當然很少有哪種數據流分析會用到所有的數據流信息,一般只是提取出感興趣的特性集合進行分析。
我們考慮的多數數據流分析問題關注的是各種程序對象(常數,變量,定值,表達式等)的集合,以及在過程內任意一點這些對對象的什么集合是合法的有關判斷。另外在數據流分析中,一般是會忽略掉路徑條件判斷的,也就是說默認所有路徑都是可達(這種近似是正確且有效,現在我還沒有找到忽略條件也能保證數據流分析正確性的證明?。?/strong>,在程序分析中忽略掉程序控制條件,所以核心部分就是狀態數據如何變化了,也就是數據流分析。
我們雖然可以對過程的控制流圖進行數據流分析,但通常更為有效的做法是將它分解為局部數據流分析和全局數據流分析,局部數據流分析針對每一個基本塊進行,全局數據流分析針對控制流圖進行分析,其實就是一個粒度問題。我們可以將同一個基本塊內的各個語句的作用綜合起來和合成整一個基本快的作用。例如我們可以將上面的自動機改造為基于基本塊的形式,如下圖所示:
數據流分析模式
在數據流分析中,程序點一般和數據流值(data-flow value)關聯起來,注意這個數據流值不是程序中變量的值。"這個值是在該點可能觀察到的所有程序狀態的集合的抽象表示",這句話說起來有點繞口,每個數據流分析問題都有其對應的值域,每個程點的數據流值都是該值域的子集。比如,到達定值的數據流值的域是程序的定值集合的所有子集的集合。某個數據流值是一個定值的集合,數據流分析的目的就是推導出所有程序點與其對應的到達定值的集合。
一個定值是對某個變量的復制??赡苎刂硹l路徑到達某個程序點的定值稱為到達定值(reaching definition)
我們把每個語句s之前和之后的數據流值分別記為IN[s]和OUT[s]。數據流問題就是對一組約束求解,得到所有IN[s]和OUT[s]的結果。
每個語句都約束了該語句之前程序狀態和之后程序狀態的關系,也就是說語句s限定了IN[s]和OUT[s]之間的關系。整個程序就是由無窮個這樣的約束構成的。數據流問題(data-flow problem)就是對這一組約束求解,另外約束不僅有語義(傳遞函數)上的約束,更有基于控制流的約束。
傳遞函數
在一個語句之前和之后的數據流值受該語句語義道德約束,也就是程序語句前后程序點的數據流值受該語句語義的約束,這種約束關系稱為傳遞函數(transfer function)。
傳遞函數有兩種風格:數據流信息可能沿著執行路徑前向傳播,或者沿著程序路徑逆向流動,相應就有前向(forward)數據流問題和后項(backward)數據流問題。
大部分人剛接觸到后向數據流問題時會比較困惑,數據流值怎么會依賴于后面的數據流值信息呢。其實這是由于有些人還是對于數據流值的概念不是很理解去,將數據流值簡單的歸結于變量的值,如果這么對比的話,就會出現矛盾。
對于前向數據流問題,一個程序語句S的傳遞函數以語句前程序點的數據流值作為輸入,并產生出語句之后程序點對應的新數據流值。例如到達定值就是前向數據流問題。
對于后向數據流問題,一個程序語句s的傳遞函數以及語句后的程序點的數據流值作為輸入,變換為成語句之前程序點的新數據流值。例如活變量分析就是后向數據流問題。
控制流約束
第二組關于數據流值的約束是從控制流中得到的,基本塊內都是順序執行,沒有控制流的約束。但是基本塊之間有相應的控制流約束,例如一個基本塊的最后一個語句和后繼基本塊的第一個語句之間地約束,這些約束比較復雜。
基本塊上的數據流模式
前面我們已經提到過程序語句的約束分為兩種,基于程序語句語義的約束和基于控制流的約束?;緣K之間的約束都是基于控制流的約束,由于基本塊內沒有分支,所以我們可以基于整個基本塊來描述基于塊對于數據流值的約束,而不是基于程序語句(前面也提到過,我們可以使用局部數據流和全局數據流分析結合更加高效)。我們以基本塊為最小單位來研究基本塊上的數據流模式。
基本塊的傳遞函數和基本塊內程序語句所表示的傳遞函數之間的關系如上圖所示。那么基本塊之間的約束是如何的呢?如下圖所示。
圖中展示出來的是基本塊之間的前向數據流問題的約束方程。后向束流問題的方程如下圖所示。
數據流分析就是根據這一組約束,得到一個滿足這些約束的解。和線性算法方程不同,數據流方程通常沒有唯一解。數據流分析的目標是尋找一個最"精確的"滿足這兩組約束(即控制流和傳遞函數)的解,當然這個解必須是保守的,能夠保證我們根據這個解進行代碼優化不會導致不安全的轉換。
當然數據流分析,不是直接聯立方程求解,一般是通過一種迭代分析的方法求解的。
到達定值
什么是到達值
"到達值"是最常見的和有用的數據流模式之一。編譯器能夠根據到達定值信息知道x在點p上的值是否為常量,而如果x在點p上被使用,則調試器可以指出x是否未經定值就被使用。
如果存在一條從緊隨在定值d后面的程序點到達某一個程序點p的路徑,并且在這條路徑行d沒有被"殺死",我們就說定值d到達程序點p。如果在這條路徑上有對變量x的其他定值,我們就說變量x的這個定值(定值d)被"殺死"了。
到達值的示意圖如下所示。
注:上面這個圖不嚴謹,p是程序點,應該緊挨著下面的矩形而不是表示矩形。圖中的矩形表示的是一條語句。
到達值有以下用法:
創建use/def鏈
常量傳播
循環不變量外提
變量x的一個定值是(可能)將一個賦值給x的語句。過程參數,數組訪問和間接引用都可以有別名,因此指出一個語句是否向特定程序變量x賦值并不是件很容易地事情。
存在別名的情況下需要作別名分析,如果為了提高分析效率而不介意損失一些分析精度的話,可以做保守估計,例如我們不知道當前語句對哪個變量賦值,我們就在此處針對每個變量產生一個定值。這是一種無奈的折中。此處我們不考慮別名情況。
到達定值的傳遞函數
首先我們做一些假設:
一個語句節點至多能夠對一個變量定值
我們可以通過節點編號索引到該賦值語句
當然,在實際情況中一個語句節點可能會對不止一個變量定值。下面我們定義一下gen[n]函數和kill[n]函數。
gen[n]:節點n產生的定值(假設一個語句節點至多一個定值)
kill[n]:節點n"殺死"的定值
|
程序語句 |
gen[s] |
kill[s] |
|
s: t = b op c |
{s} |
def[t] - {s} |
|
s: t = M[b] |
{s} |
def[t] - {s} |
|
s: M[a] = b |
{s} |
{*} - {s} |
|
s: if a op b goto L |
{} |
{} |
|
s:goto L |
{} |
{} |
|
s: L: |
{} |
{} |
|
s: f(a, …) |
{} |
{} |
|
s: t = f(a, …) |
{s} |
def[t] - {s} |
上面的表格列舉了一些程序語句的gen和kill傳遞函數形式。第一行的列舉的"s:t=b op c",產生了定值s并"殺死"了除定值s以外所有對變量t的定值。
注意:定值是一個程序,對同一個變量可以存在多個不同的定值
我們也可以先計算出各個程序語句的gen和kill結果,然后綜合基本塊中的各個語句生成整個基本塊的gen和kill集合。如下圖所示,其中我們先默認各個基本塊的起始和結束處所有定值都可以到達,下圖程序中總共有7個定值,分別為d1,d2,d3,d4,d5,d6,d7.
經過第一次的傳遞函數作用,各個基本塊到達定值集合的變化情況如圖左所示。
到達值的保守性
在前面介紹數據流分析時,曾經提到過數據流分析允許一定的不精確性。但是它們都是在"安全"或者說"保守"的方向上不精確。如下圖所示:
只要我們得到的解偏于保守的一方即可,然后再盡力的向精確的方向靠近,不同的應用"保守"的定義也不同。在大部分到達定值的應用中,在一個定值不可能到達某點的情況下假設其能夠到達是保守的。如下圖所示:
因此在設計一個數據流模型的時候,我們必須知道這些信息將如何被使用,并保證我們做出的任何估算都是在"保守"或者說"安全"的方向上。每個模式合區應用都要單獨考慮。
也就是說,不能套用同一個模式來判斷"保守"或者"安全"的方向,在可用表達式中,"安全"的定義就和到達定值不同。如果可用表達式沒有到達某個程序點,而得出的解表明到達了,則這是不安全的。
到達定值的傳遞方程以及控制流方程
到達定值對于單個語句的傳遞方程如下圖所示,一個基本塊內的依據就是按照這組方程建立起聯系的。和單個語句一樣,一個基本塊也會生成一個定值集合,并殺死一個定值集合。
根據基本塊之間的控制流得到的約束集合,我們可以生成一個控制流方程。其實控制流方程的含義就是在路勁交叉點進行數據流值的交匯,在到達定值中,交匯運算就是并集運算()。
對于到達定值來說,只要一個定值能夠沿著至少一個路徑到達某個程序點,就說這個定值到達該程序點。所以控制流方程的交匯運算時并集,但是對于其他一些數據流問題交匯運算時交集,例如可用表達式。
到達定值的迭代分析算法
假設每個控制流圖都有兩個空的基本塊,代表了控制流圖的ENTRY節點和EXIT節點。由于沒有定值到達這個圖的開始,所以基本塊ENTRY的傳遞函數是一個簡單的返回空集的常函數,即OUT[ENTRY]=空集。
到達定值問題使用下面方程的定義:
OUT[ENTRY]=空集
且對于所有的不等于ENTRY的基本塊B,有
OUT[B]=gen(B)(IN[B]-kill(B))
IN[B]= OUT[P],其中P是B的一個前驅基本塊
我們可以使用下面的算法來求這個方程組的解。
到達定值算法:
輸入:一個流圖,其中每個基本塊B的kill(B)集合gen(B)集都已經計算出來了。
輸出:到達流圖中各個基本塊B的入口點和出口點的定值的集合,即IN[B]和OUT[B]。
方法:我們使用迭代的方法來求解。一開始,我們"估計"對于所有基本塊B都有OUT[B]=空集,并逐步逼近想要的IN和OUT值。因為我們必須不停地迭代直到各個IN值(因此各個OUT值也)收斂,所以我們使用一個bool變量change來記錄每次掃描各基本塊時是否有OUT值發生變化。
從算法中我們可以明確看到,數據流值是從前驅P到IN[B]然后在流向OUT[B]這樣一個從前向后不斷傳播的。然后從空集不斷擴大直到越過精確解到達"保守解"。
迭代算法不斷從空向到達定值結果越來越多的方向靠近,最終會跨越精確解到達保守解的部分,主要因為兩個原因導致一定會越過精確解:
不考慮路徑條件,假設所有路徑都可達;這樣某些定值最終會到達他們本來到達不了的地方
存在別名時,給無法確認的"別名"賦值時,給所有變量添加一個定值(注意此處并沒有kill掉所有的定值,因為添加所有可能的定值,刪除肯定被kill掉定值,這樣才能保證"保守")
這個算法還有可以改進的地方,其中一個就是精心安排迭代分析時基本塊的順序,基本按照CFG從入口ENTRY到EXIT順序。如果當前基本塊的到達定值結果發生了改變,那么就把其所有后繼基本塊加入待迭代的工作列表workList。
另外到達定值使用了一種位向量的結構,來表示到達定值集合。即每個程序點的到達定值使用一個為向量表示,例如該程序有7個定值,那么位向量為7,初始向量"0000000"表示此時定值為空,如果第3號定值到達了當前程序點,那么位向量為"0010000"
活躍變量的數據流方程
我們給出兩個定義:
def(or definition)
use
def[v] = 定義變量v的所有CFG節點集合
def[n] = 節點n定義的變量集合
use[v] = 使用變量v的CFG節點集合
use[n] = 在節點n使用的變量集合
計算活躍性的規則:
(1)產生活躍性
(2)活躍性如何越過程序語句節點之間的邊
(3)活躍性如何越過程序語句節點
我們列出活躍變量的數據流方程如下所示,注意此處我們將語義約束和控制約束同時寫出來了(因為我們現在是以單個程序語句為圖節點,而不是單個基本塊)
in [n] = use [n] U ( out [n] - def [n] )
out [n] = U
in [s] , 其中s是節點n的后繼節點
從這兩個方程我們可以看出,對于活躍變量分析來說數據流是從后向前傳播的。我們這里解釋一下為什么要從out[n]中刪除def[n],
下面給出活躍變量分析的算法:
注:此處CFG是以程序語句為單個節點構建的
當然這個算法沒有考慮到CFG圖中節點的順序,效率比較低,我們將CFG圖中的節點反序,用來求解。改進算法如下:
我們也可以基本塊為單位來就行活躍變量的分析,但是我們得首先根據基本塊中程序語句的傳遞函數合并成為基本塊的傳遞函數。定義如下:
def [B] 是指如下變量的集合,這個變量在B中的定值(即被明確地)先于任何對它們的使用
use [B]是指如下變量的集合,它們的值可能在B中先于任何對它們的定值被使用
注意:上述我們標注的黑色部分,在def[B]中需要被明確定值,而在use中條件弱化,只需要可能就行了。類似于到達定值,這樣做是為了保守性。在活躍變量中,假設變量活躍到程序結束是沒有問題的,只是會損失些可以優化的點(例如寄存器分配時兩個變量的活躍區間相互重疊的概率就會變得很大),但是如果將變量的活躍期縮短的話,有可能就將該寄存器挪做他用,這樣就會導致程序錯誤。所以在活躍變量分析中,將活躍變量盡可能的向前傳播是有利于偏向保守的。但是不能一味的偏于保守,否則得到的信息就沒有任何價值,在保證保守的同時,盡可能的向精確解靠攏(所以殺死被明確賦值的變量)
所以我們在殺死變量時(即在基本塊內明確定義,在 def[B] 中)必須明確規定,但是盡可能地向前傳播(也就是如果可能在use[B] 中,直接加入就好)。如下圖所示,我們所求得的結果必須能夠保證在保守解部分,并盡力向精確解靠近。為了保證保守性,需要做到如下兩點:
忽略路徑分支條件,保證所有路徑都可達
只要有可能是活的,就向其中加入該變量。只有在該活躍變量被明確殺死時(例如被明確賦值),才刪除
如果以基本塊為單位,那么得到的數據流方程如下圖所示:
第一個方程描述了邊界條件,即在程序出口處沒有變量是活躍的。
第二個方程說明一個變量要在進入一個基本塊時活躍,必須滿足兩個條件中的一個:要么它在基本塊內被重新定值之前就被使用;要么它在基本塊的出口處活躍且在基本塊內沒有對它進行重新定值。
第三個方程說明一個變量在一個基本塊的出口處活躍當前僅當它在該基本塊的某個后繼入口處活躍。
和到達定值相同,活躍變量不需要在后繼基本塊入口都活躍,只要在其中一個基本塊入口活躍即可。但是活躍變量是后向數據流模式。在各個數據流模式中,我們都沿著路徑傳播信息,有的數據流問題,要求對應性質需要在所有路徑上都成立,而有的數據流只需要存在一個滿足該性質的路徑即可。
基于基本塊的活躍變量分析算法:
輸入:一個流圖,其中每個基本塊的use和def已經計算出來了。
輸出:該流圖中的各個基本塊B的入口和出口處的活躍變量集合,即 IN[ B ] 和 OUT[ B ]。
該算法得到的具有最小活躍變量(亦即盡量向精確解靠近)的集合。
可用表達式
如果從流圖入口結點到達程序點 p 的每條路徑都對表達式 x + y 求值,且從最后一個這樣的求值之后到p點的路徑上沒有再次對x或y賦值,那么 x + y 在 p 點上可用(available)。
注意在可用表達式的定義中,我特意加黑了每條路徑,這是和到達定值不同的,對于到達定值來說至少存在一條這樣的路徑即可。
對于可用表達式數據流模式而言,如果一個基本塊對 x 或 y 賦值(或可能對它們賦值),并且之后沒有再重新計算 x + y,我們就說該基本塊"殺死"了表達式 x + y。
如果一個基本塊一定對 x + y 求值,并且之后沒有再對 x 或 y 定值,那么這個基本塊生成表達式 x + y 。
可用表達式信息的主要用途就是尋找全局公共子表達式。每個程序都有有限個表達式,這有限個表達式就是可用表達式數據流分析的值域,也就是每個程序點的可用表達式就是這個值域的子集。
int z = x * y;
print s + t;
int w = u / v;
// ...
// program contains expressions { x * y, s + t, u / v, ...}
1
2
3
4
5
可用性是表達式在數據流中的一個屬性,"這個表達式是否計算過?"。在一條指令之前,每個表達式只能是可用或者不可用,所以通常都是從指令的角度來考慮表達式的可用性,每條指令(或者流圖中的一個結點)都關聯著一組可用表達式。
int z = x * y;
print s + t;
int w = u / v; // 3: avail(3) = { x * y, s + t}
1
2
3
例如在結點3處,有兩條可用表達式"x * y" 和 "s + t"。從很多方面來看,可用表達式和活變量都有相似之處,都是數據流的一種屬性,并且在每個程序點都關聯著一組值的集合。在活躍變量分析中,數據流從后向前傳播,一個對 x 的賦值語句,會"殺死"變量x的活躍性,在可用表達式的分析中,數據流從前向后傳播,一個對 x 的賦值語句會"殺死"所有包含 x 運算子的表達式。
除了數據流方向這一個區別之外,還有一個很重要的區別,就是在可用表達式分析中,我們必須能夠保證該表達式在當前程序點絕對可用,也就是說我們必須保證該表達式被計算過(即使有丟失可用表達式的可能),而不是該表達式在此處可能可用。也就是說可用表達式分析是一種must分析,而活躍變量分析是一種may分析。
如果一個表達式被認為是可用的,我們有可能會做一些比較危險的事情(例如刪除重復計算該表達式的指令)。在活變量分析中,更多的活變量就更能夠保證安全性,但是在可用表達式中,越少的可用表達式才更能保證安全性。
當程序運行時可用表達式和不可用表達式如下圖所示,這個圖表示的動態執行時的精確解(也就是如果某個基本塊不可能執行到,那么這個基本塊對可用表達式分析的影響為0)。
假設有以下代碼,在數據流分析中不可能真正確切的知道哪些路徑可達,所以假設所有路徑可達是安全的,雖然會損失些可以優化的機會。
在安全的前提下,數據流分析還是會盡量向精確靠近,這樣才能把優化發揮的更徹底。上述代碼對應的可用表達式的圖示如下。其中 x + y 是我們在數據流分析的過程中將其殺死的,其實在真正代碼的執行過程中,B3塊可能不會被真正執行,也就是說 x + y 可能是可用的。但是數據流分析的第一準則是安全性,然后才會在安全的前提下做更為激進的分析。和活變量分析類似,我們盡量會在安全的前提下,向精確解靠近。
我們可以用類似于計算到達定值的方式計算可用表達式。假設 U 是所有出現在程序中一個或多個語句的右部的表達式的全集。對于每個基本塊B,令IN[ B ]表示在B的開始處可用的的U中的表達式的集合。令OUT[ B ]表示在B的結尾處可用的表達式集合。定義e_gen[B]為B生成的表達式的集合,而e_kill[B]為被B殺死的U中的表達式的集合。所以我們可以相關的數據流方程和控制流方程。
上面的方程和到達定值的方程組看起來幾乎一樣,但是一點很重要的區別是這個方程組的交匯運算是交集運算,而不是并集運算。因為只有當一個表達式在一個基本塊的多有前驅的結尾處都可用,它才會在該基本塊的開頭可用。
在到達定值方程的過程中,我們首先假設任何地方都沒有定值到達,然后逐漸增大到到達定值的集合,最終構建得到該解。我們最終會求解到達定值方程組,得到符號"到達"定義的最小集合。
而在求解可用表達式的過程中,我們首先假設除了入口塊之外的所有基本塊的出口處,所有可用表達式都是可用的,然后不斷的將這個解縮小,直到得到一個最大的可用表達式集合的解。
例如我們開始假設所有表達式可用,然后不斷的縮減得到的解,直到越過了精確解范疇。
由于數據流分析會忽略所有的路徑條件,假設所有的路徑可達,所以數據流解的集合會不斷的縮小直到一個最大的精確的安全解。
這里我們證明一下為什么考慮全路徑的情況下,一定會越過精確解??紤]下面的代碼:
(1)多考慮一個路徑,肯定會殺死一個原有的可用的表達式
(2)即使多考慮的路徑中會生成新的可用表達式,但是由于數據流方程是交集運算,所以單單多考慮的路徑的生成還不行,還需要其他的路徑都生成該表達式,該表達式才會生成出來。也就是說,多考慮的路徑中生成的表達式其實沒有任何意義。
例如上圖中的代碼,假設 B1 -> B3 -> B4 這條路徑不可達,B3塊會殺死表達式x + y,雖然會生成表達式 d + c 但是由于可用表達式的交匯運算時交集,所以必須B2塊生成表達式 d + c 才算真正生成表達式 d + c ,也就是無效路徑生成的表達式其實沒有意思的。也就是多考慮一條路徑只會殺死更多的表達式。
不知道一個表達式是可用的只會使我們失去改進代碼的機會,而把一個不可用的表達式則會使我們改變程序的計算結果??捎帽磉_式的迭代算法如下所示:
下面我們總結一下前面所提到過的MUST和MAY分析。
|
特點 |
May |
Must |
|
safe |
更大的集合 |
更小的集合 |
|
desired information |
small set |
large set |
|
Gen |
添加可能為真的值 |
只添加保證為真的值 |
|
Kill |
只刪除保證為假的值 |
刪除所有可能為假的值 |
|
merge |
union |
intersection |
通過上面的表格,我們可以看出May分析是盡可能向集合增大的方向前進,而Must分析是盡可能的向集合減小的方向前進。那么有沒有一個統一的數據流分析框架來表示呢,不用去關注最終得到的解釋最大不動點還是最小不動點,是用交集還是用并集等等。答案是有,后面我們介紹數據流分析中格的概念,格這種數據結構是一個非常直觀的表示數據流分析的框架。
Sound And Complete
前面我通過可用表達式的例子說明精確解與保守解的概念,其實這種提法并不標準。下面我摘抄《A Brief Introduction to Static Analysis - Sam Blackshear》講義中的內容。
當我們編寫一個程序的時候,我們希望知道程序是否滿足某個屬性,例如程序P是否沒有空指針解引用(NPD),或者程序中的所有的類型轉換是否是安全的。如果對程序P進行手工驗證,在程序P比較復雜的時候,過程會很繁瑣。所以可以通過一個程序(或者靜態分析工具)去驗證程序P的某些屬性是否滿足。
但是驗證某個程序的屬性是不可判定的,見如何理解萊斯定理對程序靜態分析的限制。
雖然我們無法得到程序的精確解,但是我們可以使用overapproximation或者underapproximation來嘗試得到一個較為精確的解。
A sound static analysis overapproximates the behaviors of the program. A sound static analyzer is guaranteed to identify all violations of our property φ, but may also report some "false alarms", or violations of φ that cannot actully occur.
A complete static analysis underapproximates the behaviors of the program. Any violation of our property φ reported by a complete static analyzer corresponds to an actual violation of φ, but there is no guarantee that all actual violations of φ will be reported.
上面的的sound static analysis其實就對應我們上面說的保守解,是一種overapproximation,就是考慮程序中實際并不可行的路徑,所以能夠覆蓋完所有的違反屬性φ的場景,但是有誤報。
而上面的complete static analysis是一種就對應上面我們所描述的超過精確解的值,這些值保證都違反了φ,但是并不能覆蓋完所有的值,有漏報。
Note that when a sound static analyzer reports no errors, our program is guaranteed not to violate φ! This is a powerful guarantee. As a result, most static analysis tools choose to be sound rather than complete.
但是在某些靜態分析工具中在某些場景中是不可能做到sound的,例如clang static analyzer,在指針場景中,指針ptr有可能指向任意的變量,如果要對指針ptr指向的內存區域進行賦值,"sound static analysis"會將程序中所有變量進行賦值,那么繼續向下就會變得非常不精確,這是不可能接受的,整個分析過程會得不到任何有價值的信息。
總結
- 上一篇: [javascript] Date 时间
- 下一篇: 两个不同的路由器怎么桥接两个不同牌子的无