Typestate性質(zhì)運(yùn)行時(shí)驗(yàn)證的關(guān)鍵技術(shù)研究.pdf

1、現(xiàn)代大規(guī)模的軟件系統(tǒng)一般都是建立在第三方程序庫之上的，比如大家所熟知的Java類庫。但是，第三方程序庫往往對(duì)其提供的接口規(guī)定了一些調(diào)用規(guī)約，軟件開發(fā)人員必須遵循這些調(diào)用規(guī)約，否則將會(huì)導(dǎo)致軟件系統(tǒng)在運(yùn)行時(shí)出現(xiàn)不可預(yù)知的異常或失效。這些規(guī)約被稱作typestate性質(zhì)，通?？梢允褂脦ё杂勺兞康臅r(shí)序邏輯表示。據(jù)統(tǒng)計(jì)，許多大規(guī)模軟件系統(tǒng)的錯(cuò)誤都是由于違反第三方程序庫的接口調(diào)用規(guī)約而引起的，并且此類錯(cuò)誤不易被軟件開發(fā)和維護(hù)人員發(fā)現(xiàn)和修復(fù)，極大地增

2、加了軟件開發(fā)和維護(hù)成本。靜態(tài)分析程序是否滿足給定的typestate性質(zhì)是一個(gè)不可判斷的問題。通常，大家使用運(yùn)行時(shí)驗(yàn)證這種動(dòng)態(tài)方式測(cè)試程序是否違反typestate性質(zhì)。
　　運(yùn)行時(shí)驗(yàn)證技術(shù)能夠?qū)ypestate性質(zhì)自動(dòng)轉(zhuǎn)換為運(yùn)行時(shí)監(jiān)控器，并對(duì)原程序進(jìn)行插裝處理。但是，插裝過后的程序一般包含了大量的冗余插裝，這會(huì)嚴(yán)重影響程序運(yùn)行時(shí)性能。近年來，大家使用靜態(tài)分析技術(shù)在編譯階段刪除一些不必要的監(jiān)控插裝代碼，以此來降低動(dòng)態(tài)監(jiān)控給程序運(yùn)

3、行時(shí)性能所帶來的不利影響，這就是所謂的混成typestate性質(zhì)分析技術(shù)。Eric Bodden提出的Nop-shadows Analysis(NSA)就是一種典型的混成Typestate性質(zhì)分析技術(shù)。NSA使用部分上下文敏感、過程內(nèi)流敏感的數(shù)據(jù)流分析方法在編譯階段識(shí)別和刪除一些不必要的監(jiān)控插裝代碼。盡管NSA靜態(tài)分析的精度比較高，但是仍然存在一些案例，NSA不能完全刪除其中的監(jiān)控插裝。甚至，對(duì)于某些案例，NSA基本上沒有效果。本課題認(rèn)

4、真地研究分析了失效案例，詳細(xì)地剖析了NSA靜態(tài)分析過程。在此基礎(chǔ)之上，我們提出了三種分別適用于不同情形的優(yōu)化技術(shù)，它們都能針對(duì)某些案例提高NSA靜態(tài)分析精度，在編譯階段識(shí)別和刪除更多的監(jiān)控插裝代碼。具體來說，本文取得了如下貢獻(xiàn)和創(chuàng)新：
　　1.定義了穩(wěn)定configuration的概念，詳細(xì)地分析了它的特性，并提出了基于穩(wěn)定configuration的NSA靜態(tài)分析優(yōu)化技術(shù)。為了識(shí)別后向數(shù)據(jù)流分析結(jié)果中產(chǎn)生的穩(wěn)定configura

5、tion，我們通過增加一個(gè)布爾變量將原來configuration二元組擴(kuò)展為三元組，使configuration能夠記錄狀態(tài)轉(zhuǎn)換信息，并修改了后向數(shù)據(jù)流分析過程中的configuration轉(zhuǎn)換算法。本文提出了消除穩(wěn)定configuration對(duì)識(shí)別冗余監(jiān)控插裝代碼時(shí)的不利影響的規(guī)則，并對(duì)該規(guī)則的正確性進(jìn)行了證明。在程序中存在多個(gè)相同類型的對(duì)象的操作相互交叉的情況下，我們的優(yōu)化技術(shù)能進(jìn)一步提高NSA靜態(tài)分析的精度，識(shí)別和刪除更多的冗余

6、監(jiān)控插裝代碼。
　　2.定義了本地對(duì)象和過程間configuraiton的概念，提出了基于本地對(duì)象的優(yōu)化技術(shù)，它可以進(jìn)一步提高NSA靜態(tài)分析技術(shù)識(shí)別冗余監(jiān)控插裝代碼的能力。本文基于過程內(nèi)流敏感的指針別名信息，設(shè)計(jì)了一個(gè)識(shí)別本地對(duì)象的高效算法。我們通過增加一個(gè)布爾變量將configuration擴(kuò)展為三元組結(jié)構(gòu)，使其能夠記錄數(shù)據(jù)流分析過程中的過程間控制流傳播信息，便于從數(shù)據(jù)流分析結(jié)果中識(shí)別過程間configuration。另外，根據(jù)

7、configuration在控制流圖中的傳播機(jī)理，本文修改了configuration在過程間的傳播轉(zhuǎn)換函數(shù)?；诒镜貙?duì)象和過程間configuration，本文提出了消除過程間configuration對(duì)識(shí)別冗余監(jiān)控插裝代碼時(shí)的不利影響的規(guī)則，并證明了該規(guī)則的正確性。
　　3.提出了基于部分過程間流敏感信息的NSA分析優(yōu)化技術(shù)，其核心思想是利用被調(diào)用方法中所包含的部分流敏感信息，精化過程間方法調(diào)用的數(shù)據(jù)流分析結(jié)果。這樣我們可以不

8、用對(duì)整個(gè)程序的控制流圖進(jìn)行流敏感的數(shù)據(jù)流分析，有效地避免了完全過程間流敏感分析的代價(jià)，還能進(jìn)一步提高NSA靜態(tài)分析的精度。本文定義了兩個(gè)變量綁定和configuration的二元運(yùn)算符，計(jì)算過程間數(shù)據(jù)流分析的結(jié)果。基于過程內(nèi)流敏感的肯定別名分析算法，本文定制了一個(gè)簡(jiǎn)單高效的過程間肯定別名分析算法。在此基礎(chǔ)之上，本文介紹了基于部分過程間流敏感信息的NSA靜態(tài)分析優(yōu)化技術(shù)的工作流程。
　　4.本課題實(shí)現(xiàn)了以上三種優(yōu)化技術(shù)，并將它們集成

9、到Clara框架中，將Clara的靜態(tài)分析階段由3個(gè)擴(kuò)展到6個(gè)。采用學(xué)術(shù)界公認(rèn)的DaCapo基準(zhǔn)程序測(cè)試集，對(duì)比分析和評(píng)估我們所提出的優(yōu)化方法的效果。實(shí)驗(yàn)表明，我們所提出的優(yōu)化方法能夠在超過一半的案例中有明顯的效果，平均每個(gè)案例在原來NSA靜態(tài)分析之后還能進(jìn)一步刪除11個(gè)監(jiān)控插裝代碼。特別是在兩個(gè)案例中，我們得到了非常好的實(shí)驗(yàn)結(jié)果，完全刪除了由原來NSA技術(shù)不能識(shí)別的冗余監(jiān)控插裝代碼，避免了運(yùn)行時(shí)動(dòng)態(tài)監(jiān)控。此外，三種優(yōu)化方法并不會(huì)額外地