大學(xué)數(shù)據(jù)流分析課件

第2章數(shù)據(jù)流分析數(shù)據(jù)流分析的用途編譯優(yōu)化、程序維護(hù)程序安全性的檢查和編譯原理課程的區(qū)別基于源代碼的結(jié)構(gòu)化分析方法，而不是基于基本塊和程序流圖的分析從過程內(nèi)討論到過程間強(qiáng)調(diào)理論基礎(chǔ)/sundae_meng第2章數(shù)據(jù)流分析數(shù)據(jù)流分析的用途http://www.d1第2章數(shù)據(jù)流分析數(shù)據(jù)流分析的正確性數(shù)據(jù)流分析所得結(jié)論同程序運(yùn)行時(shí)的情況一致需要定義機(jī)器模型和操作語(yǔ)義，證明所得結(jié)論對(duì)操作語(yǔ)義可靠由于數(shù)據(jù)流分析收集的信息同基本塊和控制流有關(guān)，通常和變量值無(wú)關(guān)，因此不同于一般的可靠性證明，例如Hoare邏輯的賦值公理是可靠的

{x=1}x:=x+1{x=2}/sundae_meng第2章數(shù)據(jù)流分析數(shù)據(jù)流分析的正確性http://www.2活躍變量分析活躍變量分析的正確性需要將該正確性概念形式地表達(dá)出來(lái)在活躍變量的初值相同的不同格局下S,1和S,2執(zhí)行程序S的結(jié)果應(yīng)該是一樣的再細(xì)化一下，程序每執(zhí)行一步，得到的不同格局S,1

和S,2

中，活躍變量的值都相同/sundae_meng活躍變量分析活躍變量分析的正確性http://www.doc3第2章數(shù)據(jù)流分析數(shù)據(jù)流分析的基礎(chǔ)把各種數(shù)據(jù)流模式作為一個(gè)整體來(lái)抽象地研究，然后可以形式地回答數(shù)據(jù)流算法的下列幾個(gè)基本問題：在什么情況下數(shù)據(jù)流分析中使用的迭代算法是正確的？該迭代算法所得解的精度如何？該迭代算法是否收斂？數(shù)據(jù)流方程的解的含義是什么？/sundae_meng第2章數(shù)據(jù)流分析數(shù)據(jù)流分析的基礎(chǔ)http://www.d4第2章數(shù)據(jù)流分析為一類數(shù)據(jù)流模式建一個(gè)共同理論框架總結(jié)已討論過的四種數(shù)據(jù)流分析模式整理出該框架的一些基本特征或原則規(guī)范框架中的性質(zhì)空間要滿足的特征規(guī)范框架中遷移函數(shù)要滿足的性質(zhì)給出框架的定義區(qū)分單調(diào)框架和分配框架的區(qū)別常量傳播數(shù)據(jù)流模式不是分配的/sundae_meng第2章數(shù)據(jù)流分析為一類數(shù)據(jù)流模式建一個(gè)共同理論框架htt5第2章數(shù)據(jù)流分析位向量框架（Bitvectorframework）Single-bitrepresentationofeachdataflowpropertySeparabilityofsolution

Dataflowpropertiescanbeevaluated independently

MergeoperationisabitwiseANDorOR operationMonotonicbitfunction

Abitfunctioncannotnegateanybit/sundae_meng第2章數(shù)據(jù)流分析位向量框架（Bitvectorfra6第2章數(shù)據(jù)流分析分配性蘊(yùn)涵單調(diào)性的證明l1

l2

并且f(l1

l2)=f(l1)

f(l2)蘊(yùn)涵f(l1)

f(l2)證明

因?yàn)?f(l2)=f(l1

l2)=f(l1)

f(l2)所以 f(l1)

f(l2)/sundae_meng第2章數(shù)據(jù)流分析分配性蘊(yùn)涵單調(diào)性的證明http://ww7第2章數(shù)據(jù)流分析常量傳播框架的非分配性 說(shuō)明常量傳播框架沒有分配性的例子B1EXITz=x+yx=2y=3B3B2x=3y=2/sundae_meng第2章數(shù)據(jù)流分析常量傳播框架的非分配性 說(shuō)明常量傳播框架8第2章數(shù)據(jù)流分析整數(shù)格表示沒有任何信息可用表示可能不是常量…3210123…/sundae_meng第2章數(shù)據(jù)流分析整數(shù)格…329第2章數(shù)據(jù)流分析用集合之間的包含關(guān)系來(lái)定義部分函數(shù)之間的偏序{0,1,1,1,2,1}常函數(shù)1階乘函數(shù){0,1,1,1,2,2}{0,1,1,1}{0,1}{0,5}......................../sundae_meng第2章數(shù)據(jù)流分析用集合之間的包含關(guān)系來(lái)定義部分函數(shù)之間的10第2章數(shù)據(jù)流分析數(shù)據(jù)流方程的求解IDEAL，基于程序所有可能執(zhí)行路徑的解，它少于或等于流圖上的執(zhí)行路徑MeetOverallPaths(MOP)，不僅匯集了所有可能路徑的數(shù)據(jù)流值，而且還包括了那些不可能被執(zhí)行路徑的數(shù)據(jù)流值MaximumFixedPoint(MFP)，由迭代算法得到的解迭代算法得到的MFP解總是安全的

MFPMOPIDEAL/sundae_meng第2章數(shù)據(jù)流分析數(shù)據(jù)流方程的求解http://www.d11第2章數(shù)據(jù)流分析MOP和MFP的比較由MOP的定義，有

MOPo[B4]=((fB3?fB1)(fB3?fB2))(vENTRY)在迭代算法(MFP)中，如果按B1，B2，B3和B4的次序訪問結(jié)點(diǎn)，那么

MFPo[B4]=

fB3(fB1(vENTRY)

fB2(vENTRY))說(shuō)明路徑上較早匯合之影響的流圖B1ENTRYB4B3B2/sundae_meng第2章數(shù)據(jù)流分析MOP和MFP的比較說(shuō)明12第2章數(shù)據(jù)流分析敏感性分析路徑敏感分析 根據(jù)條件分支語(yǔ)句中的謂詞來(lái)計(jì)算不同路徑上的信息，它能夠區(qū)分控制流圖上不同路徑的信息路徑不敏感分析 先前討論的都是路徑不敏感分析流不敏感分析 語(yǔ)句的執(zhí)行次序?qū)Ψ治鰜?lái)說(shuō)無(wú)關(guān)緊要，S1;S2和S2;S1的分析結(jié)果肯定一樣流敏感分析

先前討論的都是流敏感分析/sundae_meng第2章數(shù)據(jù)流分析敏感性分析http://www.doci13第2章數(shù)據(jù)流分析敏感性分析上下文不敏感分析 組合所有調(diào)用點(diǎn)的狀態(tài)信息，對(duì)過程體僅分析一次，返回狀態(tài)集合的信息用于所有的返回點(diǎn)上下文敏感分析 區(qū)分帶不同上下文信息的不同調(diào)用/sundae_meng第2章數(shù)據(jù)流分析敏感性分析http://www.doci14第2章數(shù)據(jù)流分析過程間分析的關(guān)注點(diǎn)上下文敏感分析 要注意調(diào)用和返回的匹配，注意上下文信息的傳遞參數(shù)傳遞的方式 僅考慮傳值和傳結(jié)果方式 其他如傳引用，會(huì)引起別名過程作為參數(shù)

在此不考慮/sundae_meng第2章數(shù)據(jù)流分析過程間分析的關(guān)注點(diǎn)http://www.15第2章數(shù)據(jù)流分析數(shù)據(jù)流分析的用途編譯優(yōu)化、程序維護(hù)程序安全性的檢查和編譯原理課程的區(qū)別基于源代碼的結(jié)構(gòu)化分析方法，而不是基于基本塊和程序流圖的分析從過程內(nèi)討論到過程間強(qiáng)調(diào)理論基礎(chǔ)/sundae_meng第2章數(shù)據(jù)流分析數(shù)據(jù)流分析的用途http://www.d16第2章數(shù)據(jù)流分析數(shù)據(jù)流分析的正確性數(shù)據(jù)流分析所得結(jié)論同程序運(yùn)行時(shí)的情況一致需要定義機(jī)器模型和操作語(yǔ)義，證明所得結(jié)論對(duì)操作語(yǔ)義可靠由于數(shù)據(jù)流分析收集的信息同基本塊和控制流有關(guān)，通常和變量值無(wú)關(guān)，因此不同于一般的可靠性證明，例如Hoare邏輯的賦值公理是可靠的

{x=1}x:=x+1{x=2}/sundae_meng第2章數(shù)據(jù)流分析數(shù)據(jù)流分析的正確性http://www.17活躍變量分析活躍變量分析的正確性需要將該正確性概念形式地表達(dá)出來(lái)在活躍變量的初值相同的不同格局下S,1和S,2執(zhí)行程序S的結(jié)果應(yīng)該是一樣的再細(xì)化一下，程序每執(zhí)行一步，得到的不同格局S,1

和S,2

中，活躍變量的值都相同/sundae_meng活躍變量分析活躍變量分析的正確性http://www.doc18第2章數(shù)據(jù)流分析數(shù)據(jù)流分析的基礎(chǔ)把各種數(shù)據(jù)流模式作為一個(gè)整體來(lái)抽象地研究，然后可以形式地回答數(shù)據(jù)流算法的下列幾個(gè)基本問題：在什么情況下數(shù)據(jù)流分析中使用的迭代算法是正確的？該迭代算法所得解的精度如何？該迭代算法是否收斂？數(shù)據(jù)流方程的解的含義是什么？/sundae_meng第2章數(shù)據(jù)流分析數(shù)據(jù)流分析的基礎(chǔ)http://www.d19第2章數(shù)據(jù)流分析為一類數(shù)據(jù)流模式建一個(gè)共同理論框架總結(jié)已討論過的四種數(shù)據(jù)流分析模式整理出該框架的一些基本特征或原則規(guī)范框架中的性質(zhì)空間要滿足的特征規(guī)范框架中遷移函數(shù)要滿足的性質(zhì)給出框架的定義區(qū)分單調(diào)框架和分配框架的區(qū)別常量傳播數(shù)據(jù)流模式不是分配的/sundae_meng第2章數(shù)據(jù)流分析為一類數(shù)據(jù)流模式建一個(gè)共同理論框架htt20第2章數(shù)據(jù)流分析位向量框架（Bitvectorframework）Single-bitrepresentationofeachdataflowpropertySeparabilityofsolution

Dataflowpropertiescanbeevaluated independently

MergeoperationisabitwiseANDorOR operationMonotonicbitfunction

Abitfunctioncannotnegateanybit/sundae_meng第2章數(shù)據(jù)流分析位向量框架（Bitvectorfra21第2章數(shù)據(jù)流分析分配性蘊(yùn)涵單調(diào)性的證明l1

l2

并且f(l1

l2)=f(l1)

f(l2)蘊(yùn)涵f(l1)

f(l2)證明

因?yàn)?f(l2)=f(l1

l2)=f(l1)

f(l2)所以 f(l1)

f(l2)/sundae_meng第2章數(shù)據(jù)流分析分配性蘊(yùn)涵單調(diào)性的證明http://ww22第2章數(shù)據(jù)流分析常量傳播框架的非分配性 說(shuō)明常量傳播框架沒有分配性的例子B1EXITz=x+yx=2y=3B3B2x=3y=2/sundae_meng第2章數(shù)據(jù)流分析常量傳播框架的非分配性 說(shuō)明常量傳播框架23第2章數(shù)據(jù)流分析整數(shù)格表示沒有任何信息可用表示可能不是常量…3210123…/sundae_meng第2章數(shù)據(jù)流分析整數(shù)格…3224第2章數(shù)據(jù)流分析用集合之間的包含關(guān)系來(lái)定義部分函數(shù)之間的偏序{0,1,1,1,2,1}常函數(shù)1階乘函數(shù){0,1,1,1,2,2}{0,1,1,1}{0,1}{0,5}......................../sundae_meng第2章數(shù)據(jù)流分析用集合之間的包含關(guān)系來(lái)定義部分函數(shù)之間的25第2章數(shù)據(jù)流分析數(shù)據(jù)流方程的求解IDEAL，基于程序所有可能執(zhí)行路徑的解，它少于或等于流圖上的執(zhí)行路徑MeetOverallPaths(MOP)，不僅匯集了所有可能路徑的數(shù)據(jù)流值，而且還包括了那些不可能被執(zhí)行路徑的數(shù)據(jù)流值MaximumFixedPoint(MFP)，由迭代算法得到的解迭代算法得到的MFP解總是安全的

MFPMOPIDEAL/sundae_meng第2章數(shù)據(jù)流分析數(shù)據(jù)流方程的求解http://www.d26第2章數(shù)據(jù)流分析MOP和MFP的比較由MOP的定義，有

MOPo[B4]=((fB3?fB1)(fB3?fB2))(vENTRY)在迭代算法(MFP)中，如果按B1，B2，B3和B4的次序訪問結(jié)點(diǎn)，那么

MFPo[B4]=

fB3(fB