徐　超,陳　勇,葛紅美,何炎祥

(1.南京審計(jì)大學(xué),江蘇南京210029;2.中國電子科技集團(tuán)第十四研究所，江蘇南京 210013；3.武漢大學(xué)計(jì)算機(jī)學(xué)院,湖北武漢 430072)

?

基于符號執(zhí)行的能耗錯(cuò)誤檢測方法

徐超1,陳勇2,葛紅美1,何炎祥3

(1.南京審計(jì)大學(xué),江蘇南京210029;2.中國電子科技集團(tuán)第十四研究所，江蘇南京 210013；3.武漢大學(xué)計(jì)算機(jī)學(xué)院,湖北武漢 430072)

能耗是制約便攜式智能設(shè)備發(fā)展的重要瓶頸.隨著嵌入式操作系統(tǒng)的廣泛應(yīng)用,因不能合理使用操作系統(tǒng)的API而導(dǎo)致的能耗錯(cuò)誤已經(jīng)成為各種嵌入式應(yīng)用開發(fā)過程中不容忽視的因素.為減少應(yīng)用中的能耗錯(cuò)誤,以符號執(zhí)行技術(shù)為基礎(chǔ),根據(jù)禁止休眠類能耗錯(cuò)誤的特點(diǎn),設(shè)計(jì)了對應(yīng)的能耗錯(cuò)誤檢測方法.該方法首先利用過程內(nèi)分析,獲得單個(gè)函數(shù)的符號執(zhí)行信息.然后借助過程間分析對單個(gè)函數(shù)的符號執(zhí)行信息進(jìn)行全局綜合,得到更為精確的執(zhí)行開銷、鎖變量匹配等相關(guān)信息,以更好的檢測能耗錯(cuò)誤.同時(shí),符號執(zhí)行記錄了對應(yīng)的分支路徑信息,利用該信息能夠結(jié)合約束求解器較為方便的生成出錯(cuò)的測試用例,進(jìn)而定位錯(cuò)誤位置.通過示例和實(shí)驗(yàn),驗(yàn)證了該方法在能耗錯(cuò)誤檢測方面的可行性和有效性.

能耗錯(cuò)誤;符號執(zhí)行;錯(cuò)誤檢測;過程內(nèi)分析;過程間分析

1　引言

隨著手持智能化設(shè)備的廣泛普及,以iOS和Android等手機(jī)操作系統(tǒng)為基礎(chǔ)平臺(tái)的應(yīng)用得到了迅猛發(fā)展.但與此同時(shí),由于手機(jī)、平板電腦等手持設(shè)備電池容量的限制,很多應(yīng)用因其使用時(shí)的高能耗而使得其難以得到用戶的支持.如何降低這些手機(jī)應(yīng)用運(yùn)行時(shí)的能耗已經(jīng)引起了不少專家學(xué)者的關(guān)注.其中,Abhinav Pathak等人指出,除了應(yīng)用本身功能需要的能耗開銷外,軟件中存在的能耗錯(cuò)誤是能源消耗的一個(gè)重要因素.2011年,Abhinav Pathak等人[1]以智能手機(jī)為基礎(chǔ),從軟硬件的角度現(xiàn)有的移動(dòng)設(shè)備中的能耗問題進(jìn)行了分析,首次提出了能耗錯(cuò)誤(ebug)的概念,并提出了一種基于eprof[2]等能耗分析工具的能耗錯(cuò)誤檢測和調(diào)試框架.隨后,Abhinav Pathak等人[3]以及Panagiotis Vekris等人[4]針對No-Sleep的能耗錯(cuò)誤,分別利用到達(dá)-定義鏈和過程間數(shù)據(jù)流分析的方法對該類能耗錯(cuò)誤進(jìn)行檢測.Adam J.Oliner等人[5]基于統(tǒng)計(jì)的思想,利用其開發(fā)的Carat搜集智能設(shè)備中各個(gè)應(yīng)用在各種環(huán)境下消耗的電量,并將其傳遞給云服務(wù)器.然后通過云服務(wù)器對數(shù)據(jù)的統(tǒng)計(jì)分析,給出各個(gè)應(yīng)用中可能的能耗錯(cuò)誤以及較好的使用方法,傳遞給用戶以指導(dǎo)其較好的配置其智能設(shè)備,獲得能耗的節(jié)約,提高設(shè)備的持續(xù)使用時(shí)間.最近,Abhilash Jindal[6]等人從智能設(shè)備的更底層應(yīng)用出發(fā),分析了軟件驅(qū)動(dòng)程序中存在的休眠沖突問題而導(dǎo)致的能耗錯(cuò)誤,并設(shè)計(jì)了一種避免該類錯(cuò)誤的系統(tǒng)以提高設(shè)備的能效.

能耗錯(cuò)誤主要是指某些設(shè)備長期處于無效工作狀態(tài)而導(dǎo)致的能源消耗.其錯(cuò)誤的主要包括禁止休眠(No Sleep)錯(cuò)誤,循環(huán)詢問錯(cuò)誤等.禁止休眠錯(cuò)誤是由于使用了不對稱的API使得設(shè)備無法進(jìn)入休眠狀態(tài)而導(dǎo)致的無效能源消耗,如Android系統(tǒng)中使用了PARTIAL-WAKE-LOCK,但當(dāng)該部件工作結(jié)束后未使用對應(yīng)的UNLOCK操作,使得該部件一直處于激活狀態(tài)消耗大量能耗.循環(huán)詢問錯(cuò)誤是指某些應(yīng)用一直訪問無法應(yīng)答的部件而導(dǎo)致的無效能源消耗.如訪問遠(yuǎn)程服務(wù)器的程序,為保證連接的穩(wěn)定性,程序員有可能采用無限循環(huán)頻繁嘗試連接服務(wù)器,直至連接到服務(wù)器.但如果遠(yuǎn)程服務(wù)器已經(jīng)崩潰,該程序?qū)⒁蝾l繁的連接操作而導(dǎo)致大量無效能源消耗.根據(jù)文獻(xiàn)[3]的研究結(jié)果,70%的能耗錯(cuò)誤屬于禁止休眠類能耗錯(cuò)誤,檢測和糾正禁止休眠類能耗錯(cuò)誤是能耗錯(cuò)誤檢測工作的重點(diǎn).

但這些能耗錯(cuò)誤并不會(huì)影響程序的正確運(yùn)行,以保障程序正確轉(zhuǎn)換為基本目標(biāo)的傳統(tǒng)編譯器對該類錯(cuò)誤的檢測幾乎無能為力,軟件開發(fā)者很難在軟件開發(fā)過程中有效發(fā)現(xiàn)該類錯(cuò)誤.且鑒于禁止休眠類能耗錯(cuò)誤的重大比例,本文將主要針對禁止休眠類能耗錯(cuò)誤進(jìn)行分析檢測.

符號執(zhí)行技術(shù)是上個(gè)世紀(jì)70年代提出的一種路徑敏感靜態(tài)分析方法[7,8].其基本思想是以符號的形式替換輸入,根據(jù)程序中每條語句的具體語義,模擬程序的執(zhí)行.當(dāng)遇到分支條件時(shí),則將該條件增加到對應(yīng)的后續(xù)語句的執(zhí)行約束中.其分析的最終結(jié)果將獲得程序中每條執(zhí)行路徑及其需要滿足的約束條件映射表,我們可以利用約束求解器從該結(jié)果中獲得執(zhí)行某條程序路徑的一組輸入數(shù)據(jù)組合,進(jìn)而獲得對應(yīng)路徑的分析結(jié)果及其測試用例.

由于符號執(zhí)行技術(shù)能夠?qū)Τ绦蜻M(jìn)行路徑敏感分析,模擬程序各執(zhí)行路徑的狀態(tài)信息,不但能夠較好的檢測加解鎖匹配、加解鎖操作時(shí)間間隔等與禁止休眠類能耗錯(cuò)誤主要特征相關(guān)的問題,而且其記錄的路徑約束映射表也可以幫助生成對應(yīng)的測試用例,幫助定位錯(cuò)誤的位置.因此,本文將結(jié)合符號執(zhí)行技術(shù),設(shè)計(jì)一種對禁止休眠類能耗錯(cuò)誤的檢測方法.

2　禁止休眠類能耗錯(cuò)誤簡介

禁止休眠錯(cuò)誤是由于使用了不對稱的API使得設(shè)備無法進(jìn)入休眠狀態(tài)而導(dǎo)致的無效能源消耗.Abhinav Pathak等人通過進(jìn)一步的研究[3],將禁止休眠類能耗錯(cuò)誤進(jìn)一步劃分為3個(gè)類別:路徑型禁止休眠(No-Sleep Code Paths)、競爭型禁止休眠(No-Sleep Race Condition)和擴(kuò)張型禁止休眠(No-Sleep Dilation).路徑型禁止休眠能耗錯(cuò)誤主要是指單線程的應(yīng)用中的某條路徑存在未釋放的能耗相關(guān)鎖.其錯(cuò)誤模式主要有三種:(1)當(dāng)鎖釋放操作在條件分支中時(shí),該操作只在部分分支中進(jìn)行了釋放操作,而不是所有分支都進(jìn)行了釋放操作;(2)當(dāng)鎖的釋放操作在有可能出現(xiàn)異常的塊中,由于沒有在異常捕獲塊(即catch塊)中添加對應(yīng)的鎖釋放操作,而有可能在程序執(zhí)行異常時(shí)出現(xiàn)鎖未釋放的情況;(3)雖然程序中存在對應(yīng)的釋放鎖操作,但由于上層應(yīng)用存在其他資源的死鎖(如應(yīng)用級的死鎖),使得程序無法進(jìn)入所釋放的程序點(diǎn)而使得能源的大量消耗.

競爭型禁止休眠能耗錯(cuò)誤主要針對鎖操作在多線程中調(diào)用的情況:一個(gè)線程進(jìn)行加鎖操作,另一個(gè)線程進(jìn)行釋放鎖操作.由于線程執(zhí)行順序的問題,程序有可能出現(xiàn)釋放操作的線程先于加鎖操作的線程而無法完成鎖的最終釋放操作.

擴(kuò)張型禁止休眠能耗錯(cuò)誤是指加解鎖鎖操作雖然匹配,但在加解鎖操作之間花費(fèi)了比期望更多的時(shí)間進(jìn)行相應(yīng)的操作.產(chǎn)生這類鎖的原因主要有兩種:(1)由于延遲,在獲得了鎖以后并非直接進(jìn)行鎖相關(guān)操作,而是等待其他信號到來再進(jìn)行相應(yīng)操作,但該操作所需時(shí)間可能無法估計(jì)(如人工交互);(2)在加解鎖操作之間增加了大量與該鎖操作無關(guān)的處理.

由以上三類禁止休眠類錯(cuò)誤可以看出,其出錯(cuò)的因素主要同鎖變量的加載與釋放操作以及路徑的執(zhí)行情況相關(guān).因此如果能對鎖變量進(jìn)行跟蹤,找到其最壞執(zhí)行路徑進(jìn)行分析,則可以較為容易的獲得對應(yīng)的錯(cuò)誤,而這正是符號執(zhí)行技術(shù)主要的特點(diǎn),因此本文將主要以該技術(shù)為基礎(chǔ)進(jìn)行分析.

3　符號執(zhí)行技術(shù)

符號執(zhí)行經(jīng)歷了近40年的研究,針對不同環(huán)境形成了一系列分析方法[9～14],出現(xiàn)了許多分析工具,如JPF-SE[15],Klee[16],EXE[17],CUTE[18]等,但其分析過程也難以避免的存在一定的缺陷[19～21]:

(1)它難以處理復(fù)雜的數(shù)據(jù)結(jié)構(gòu).如當(dāng)賦值給數(shù)組下標(biāo)為變量的數(shù)組元素時(shí),則難以進(jìn)行精確的確定符號.

(2)由于它需要記錄所有路徑的約束條件,因此當(dāng)程序較大時(shí),一方面將會(huì)遇到路徑爆炸問題,嚴(yán)重影響符號執(zhí)行的效率.另一方面也將導(dǎo)致大量約束條件的產(chǎn)生,影響約束求解器的效率.

(3)當(dāng)遇到循環(huán)時(shí),其模擬符號執(zhí)行將可能進(jìn)入死循環(huán).

(4)當(dāng)程序較大時(shí),如果其對函數(shù)調(diào)用進(jìn)行遞歸分析,將會(huì)由于調(diào)用函數(shù)過多或者是遞歸函數(shù)而使得分析開銷十分巨大.

因此,為使得本文的分析技術(shù)能夠有效的進(jìn)行,本文根據(jù)鎖變量在程序中出現(xiàn)的特點(diǎn),對符號執(zhí)行的分析過程進(jìn)行一定的簡化.

(1)由于本文主要針對鎖變量的加載與釋放進(jìn)行分析,而鎖變量通常不是數(shù)組元素等復(fù)雜數(shù)據(jù)結(jié)構(gòu),因此對于下標(biāo)為變量的數(shù)組元素賦值,本文將采用懶賦值的方式將其賦值為“不確定”.

(2)由于本文是盡最大可能查找出程序中所有可能存在的能耗錯(cuò)誤,因此將只需找出每個(gè)鎖變量在最壞情況下的路徑,因此記錄的路徑約束只限于鎖變量最壞情況下的那天分支,以避免路徑爆炸和約束求解器過大的求解復(fù)雜度.

(3)由于鎖變量一般較少出現(xiàn)在循環(huán)體中,而且一旦其出現(xiàn)在其中,且是計(jì)數(shù)型的加鎖操作,則將很有可能導(dǎo)致鎖釋放的不匹配,因此對于循環(huán)體,本文將不對其進(jìn)行迭代分析,只是根據(jù)迭代次數(shù)將其定義的變量的符號值設(shè)定為“不確定”,以避免無限迭代.

(4)由于本文只關(guān)心最壞情況下鎖變量的情況,因此對于函數(shù)調(diào)用,本文只根據(jù)該函數(shù)中的鎖變量最壞情況下狀態(tài)值進(jìn)行迭代分析,而不重新將調(diào)用參數(shù)作為輸入值對其進(jìn)行遞歸分析,以避免函數(shù)遞歸分析過大的分析開銷.

4　基于符號執(zhí)行技術(shù)的能耗錯(cuò)誤分析方法

由于能耗錯(cuò)誤產(chǎn)生的主要原因是程序員在申請系統(tǒng)資源的過程中沒有正確使用鎖操作,使得其長期處于無效工作狀態(tài)而造成的大量能源消耗.能耗錯(cuò)誤同加解鎖操作的程序點(diǎn)和種類有著十分密切的關(guān)系.為檢測程序中可能存在的能耗錯(cuò)誤,我們不但需要檢測在最壞情況下是否存在鎖操作不匹配的情況,以發(fā)現(xiàn)路徑型禁止休眠類錯(cuò)誤,而且還需要獲得盡可能精確的加解鎖操作之間的時(shí)間間隔,以提醒程序員核查那些出現(xiàn)在加解鎖操作之間而等待時(shí)間長的代碼段是否與其加解鎖的資源相關(guān),從而最大程度避免擴(kuò)張型禁止休眠類錯(cuò)誤的產(chǎn)生.同時(shí),為能夠較為精確的定位能耗錯(cuò)誤,還需要獲得最壞情況下程序執(zhí)行的路徑信息,以便于反向跟蹤對應(yīng)的錯(cuò)誤位置.本節(jié)將主要結(jié)合符號執(zhí)行技術(shù)的思想,對程序的語義進(jìn)行擴(kuò)充,以檢測和定位程序中禁止休眠類能耗錯(cuò)誤,進(jìn)一步提高程序的能效.由于競爭型禁止休眠類錯(cuò)誤主要同線程的調(diào)度相關(guān),而一旦明確了線程調(diào)度的序列,則可以將其歸約為面向路徑型和擴(kuò)張型禁止休眠類能耗錯(cuò)誤的檢測問題,因此本節(jié)將主要討論路徑型和擴(kuò)張型禁止休眠類能耗錯(cuò)誤的檢測.

4.1能耗錯(cuò)誤過程內(nèi)分析

在進(jìn)行能耗錯(cuò)誤過程內(nèi)分析時(shí),本文首先對源文件進(jìn)行預(yù)處理,將鎖操作相關(guān)函數(shù)調(diào)用轉(zhuǎn)換為對變量的整數(shù)運(yùn)算,并將對應(yīng)的轉(zhuǎn)換后的變量保存在鎖符號集合“S”中,以便于能耗錯(cuò)誤分析時(shí)對該變量進(jìn)行識別.與文獻(xiàn)[3]不同,本文將該文獻(xiàn)中的兩種鎖操作類型擴(kuò)展為四種類型的鎖操作,即在原始賦值類型的鎖操作基礎(chǔ)上增加了自增和自減兩種鎖操作,使得該能耗檢測程序既能夠處理信號量型資源鎖,也能夠處理變量型資源鎖.其預(yù)處理的示例結(jié)果如下所示.在該程序示例中,我們將鎖操作變量wm和wl轉(zhuǎn)為對應(yīng)的整型變量.并根據(jù)其不同的鎖操作類型(wm為計(jì)數(shù)鎖,wl為信號鎖),分別在鎖加載(acquire)以及鎖釋放操作(release)時(shí)采用賦值操作(轉(zhuǎn)換后程序(b)中行7和10)以及自增操作(轉(zhuǎn)換后程序(b)中行8、14、16和22).同時(shí),為處理源程序 (a)中24行針對鎖變量為空的判斷而增加的鎖釋放操作,本文按文獻(xiàn)[3]中所示方法增加對應(yīng)的“else”操作(轉(zhuǎn)換后程序(b)中行23和24所示).能耗分析預(yù)處理示例如下:

1. publicclassTest{2. PowerManagerpm=(Pow-erManager)getSystemService();3. PowerManager.WakeLockwm=pm.newWakeLock();4. Stringdatas;5. intk;6. voidOnCreate(){7. PowerManager.Wake-Lockwl=pm.newWakeLock();8. wl.setReferenceCounted(false);9. wl.acquire();10. wm.acquire();11. net-sync();12. wl.release();13. }14. net-sync(){15. if(k<3){16. wm.acquire();17. net-working();18. wm.release();19. }20. }21. net-working(){//C(getServerData)=MaxCost1. publicclassTest{2. intwm=0;3. Stringdatas;4. intk;5. voidOnCreate(){6. intwl=0;7. wl=1;8. wm=wm+1;9. net-sync();10. wl=0;11. }12. net-sync(){13. if(k<3){14. wm=wm+1;15. net-working();16. wm=wm-1;17. }18. }19. net-working(){20. //C(getServerData)=MaxCost21. datas=getServerData();22. if(wm!=null)23. wm=wm-1;24. else22. datas=getServerData();23. if(wm!=null)24. wm.release();25. }26. }25. wm=wm-1;26. }27. }S={wl,wm}(a)源程序(b)轉(zhuǎn)換后程序

由于文獻(xiàn)[22]中所針對的語言非常簡單,而且又很強(qiáng)的表達(dá)能力,既能表達(dá)像匯編語言這種較低層次的語言,又能表達(dá)像Java這樣的高級語言,同時(shí)它也是許多編程語言在編譯器分析時(shí)實(shí)際使用的中間表達(dá)形式的語言,具有較好的通用性.而且Java語言正是本文檢測所針對的Android系統(tǒng)所使用的語言.因此,在經(jīng)過對源程序的預(yù)處理,將鎖變量操作轉(zhuǎn)為整型變量的操作后,本文主要以該語言為基礎(chǔ),在增加了函數(shù)調(diào)用以及塊成分后對其進(jìn)行分析處理,轉(zhuǎn)換后的語法如下所示.

為使得符號執(zhí)行能夠獲得能耗錯(cuò)誤檢測過程所需信息,本文對傳統(tǒng)的符號執(zhí)行進(jìn)行了修改:(1)在符號執(zhí)行過程中加入執(zhí)行時(shí)間的估計(jì)信息,以便于提取No-SleepDilation類錯(cuò)誤;(2)本文的符號執(zhí)行將主要針對鎖變量相關(guān)路徑進(jìn)行懶符號執(zhí)行分析,以避免符號執(zhí)行過程中謂詞約束條件過長和路徑爆炸等問題.轉(zhuǎn)換后的語法成分的符號執(zhí)行過程如表1所示.

表1　各語法成分符號執(zhí)行擴(kuò)展語義

續(xù)表

續(xù)表

在修改后的符號執(zhí)行過程中,本文采用八元組(e,σ,P,C,S,Σ,ι,?)記錄符號執(zhí)行的狀態(tài)信息.其中e記錄當(dāng)前表達(dá)式的值,σ、P和C分別表示符號表、約束條件以及執(zhí)行開銷值的映射表.這三個(gè)符號以符號名為索引值,構(gòu)建對應(yīng)符號的相關(guān)信息.S為當(dāng)前程序中使用的鎖變量對應(yīng)的符號名,Σ為程序地址到對應(yīng)語句的映射,ι為下一條分析的程序地址.?記錄已經(jīng)分析過的語句地址集合.此外,為解決多分支合并問題,本文在符號執(zhí)行過程中增加了兩個(gè)狀態(tài)保存鏈表I和R,分別用于保存當(dāng)前分支塊結(jié)構(gòu)所有可能的運(yùn)行結(jié)果信息和當(dāng)前函數(shù)返回狀態(tài)信息.當(dāng)遇到塊結(jié)束標(biāo)記(或函數(shù)返回標(biāo)記)時(shí),依次遍歷每個(gè)鎖變量x,通過對比對應(yīng)鏈表中σx值的大小,以獲取最壞情況下的分支狀態(tài)信息(即通過Maxσ函數(shù)選擇σx值最大的分支作為最壞分支).同時(shí)為記錄No-SleepDilation類錯(cuò)誤和循環(huán)內(nèi)錯(cuò)誤,使用鎖變量位置信息映射表l跟蹤鎖操作,使用兩個(gè)全局映射表CE和FE記錄對應(yīng)鎖變量的相應(yīng)錯(cuò)誤.其具體對應(yīng)關(guān)系如表2所示.

表2　符號執(zhí)行狀態(tài)信息

由于鎖變量通常不作為函數(shù)參數(shù)傳遞,因此為減少分析開銷以及路徑爆炸等問題,本文對函數(shù)的輸入?yún)?shù)采用懶賦值方法進(jìn)行賦值(即賦值為不確定“⊥”).同時(shí),為便于分析,本文將所有的返回語言均使用goto語句跳轉(zhuǎn)到唯一的函數(shù)出口returnExit.每當(dāng)遇到函數(shù)f,則采用規(guī)則1,首先對其內(nèi)所屬塊依次調(diào)用符號執(zhí)行(即(e,σ,P,C,S,Σ,ι,?)←SymExec(block*)),將可能包含最壞執(zhí)行情況的符號執(zhí)行結(jié)果的狀態(tài)信息保存到R列表中,然后依次分析S集合中的每個(gè)鎖變量x,由于根據(jù)鎖變量的整形轉(zhuǎn)換方法,當(dāng)鎖變量的值越高時(shí),說明在該函數(shù)中其加鎖操作也越多,這就越可能使得鎖釋放操作的不足,所以該分支也將是針對于鎖變量的最壞分支.因此我們將σx值最大的分支狀態(tài)信息作為該函數(shù)對該所變量x的符號執(zhí)行結(jié)果返回(即?x,(σx,Px,Cx)←Maxσ(R)).最后返回該最壞情況下與鎖變量相關(guān)的符號表信息、約束條件信息以及執(zhí)行開銷信息,以便于在過程間分析時(shí)計(jì)算其鎖匹配、錯(cuò)誤定位以及執(zhí)行開銷等信息.

對于塊操作,其執(zhí)行過程類似于函數(shù)(如規(guī)則2),也是按照語句次序依次執(zhí)行塊內(nèi)每條語句,保存該塊中可能包含最壞執(zhí)行情況的符號執(zhí)行結(jié)果狀態(tài)信息到I列表中.然后更新該語句為已分析(?←?∪{ι}),將每個(gè)鎖變量的最壞執(zhí)行結(jié)果作為該塊的最終執(zhí)行結(jié)果,傳遞給后續(xù)語句繼續(xù)分析.由于可能存在循環(huán),一個(gè)塊可能執(zhí)行多次,因此塊的執(zhí)行開銷還需要增加對應(yīng)塊的執(zhí)行次數(shù).同時(shí),當(dāng)塊的執(zhí)行次數(shù)不為1時(shí),由于其處于循環(huán)內(nèi),符號執(zhí)行可能使得其塊內(nèi)定義過的符合出現(xiàn)任意值,因此我們設(shè)定該塊內(nèi)定義過的符號值為不可知狀態(tài).最后,我們設(shè)定其后續(xù)執(zhí)行序列為塊出口語句(ι←Σ[blockExitb]).

在對一般語句分析時(shí),其基本操作時(shí)修改當(dāng)前已分析語句(即?值)、更新當(dāng)前執(zhí)行開銷值(即C值)和設(shè)定下一條執(zhí)行語句(即ι值)(如規(guī)則3、4等).對于賦值語句,由于其將修改對應(yīng)符號的當(dāng)前值,因此需進(jìn)一步更新對應(yīng)符號的符號表(σx←σx[val(exp)/var]).同時(shí)對于鎖變量,如果當(dāng)前的值不為0(即為加鎖狀態(tài)),且當(dāng)前的執(zhí)行開銷(Cx)超過執(zhí)行開銷閾值τ,則說明該鎖將可能長期處于加鎖狀態(tài),因而將其加入對應(yīng)的CE列表中.而如果此時(shí)鎖變量的值為0,則說明此時(shí)鎖在該操作前處于關(guān)閉狀態(tài),因而重置執(zhí)行開銷值Cx=0.對于goto語句,則需根據(jù)跳轉(zhuǎn)的位置添加對應(yīng)的狀態(tài)信息到塊狀態(tài)列表I和函數(shù)狀態(tài)列表R中.

對于if條件語句,由于可能存在循環(huán),因此先判斷該語句是否已經(jīng)被分析,如果已經(jīng)被分析,則說明是循環(huán)的節(jié)點(diǎn),不作處理,直接執(zhí)行后續(xù)指令.當(dāng)是第一次分析該語句時(shí),則分別對if分支和else分支進(jìn)行符號執(zhí)行.如果其中某條分支跳轉(zhuǎn)到已分析指令(即ι∈?),則說明該塊是循環(huán)中塊.由于循環(huán)執(zhí)行次數(shù)通常難以計(jì)算,因此在循環(huán)的一次迭代內(nèi)出現(xiàn)鎖變量的局部增益大于0,則該循環(huán)體很大情況下會(huì)出現(xiàn)鎖的不匹配情況,因而此時(shí)給出對應(yīng)的鎖不匹配的提示信息,將其加入對應(yīng)的FE列表中.否則對每個(gè)鎖相關(guān)變量x,分別比較if兩個(gè)分支中該變量的符號執(zhí)行值,選擇其最壞執(zhí)行塊(即σx值最大的塊)作為該塊的執(zhí)行結(jié)果,當(dāng)兩個(gè)塊結(jié)果一樣時(shí),則隨機(jī)選擇一條分支(本文選擇分支1)加入該鎖變量的執(zhí)行結(jié)果中.同時(shí)按其選擇的結(jié)果分支將對應(yīng)的if條件表達(dá)式加入到符號執(zhí)行的約束變量中.其具體描述如表1規(guī)則14所示.

對于表達(dá)式,則主要根據(jù)其操作類型,完成對表示式e的符號計(jì)算以及執(zhí)行開銷的計(jì)算,為賦值等一般語句準(zhǔn)備對應(yīng)的數(shù)據(jù).

在構(gòu)建了符號執(zhí)行策略后,過程內(nèi)分析如算法1所示.對于程序中的每個(gè)函數(shù),自頂向下依次對程序進(jìn)行分析,根據(jù)其匹配的符號執(zhí)行規(guī)則進(jìn)行相應(yīng)的操作,獲得對應(yīng)的符號執(zhí)行的狀態(tài)信息.

4.2能耗錯(cuò)誤過程間分析

在過程間分析時(shí),為避免路徑爆炸和約束求解過于復(fù)雜,本文只對能耗錯(cuò)誤相關(guān)變量進(jìn)行過程間分析,對符號執(zhí)行采用懶賦值方式(即函數(shù)調(diào)用結(jié)果賦值為⊥).其過程間分析如算法2所示.

4.3基于懶替換的符號執(zhí)行策略

基于懶替換的符號執(zhí)行是文獻(xiàn)[23]中提出的緩解傳統(tǒng)符號執(zhí)行符號計(jì)算過于復(fù)雜,時(shí)間和空間開銷過大而引人的有效方法.其基本想法是在符號執(zhí)行過程中,放寬必須進(jìn)行符號替換的要求,減少不必要的符號替換和符號計(jì)算.

如對于for循環(huán)語句,如下所示:

當(dāng)high為函數(shù)參數(shù)時(shí),若使用傳統(tǒng)的符號執(zhí)行跟蹤c值,則要么通過限定high值進(jìn)行有限長度的展開,其不但需要多次計(jì)算,而且每次計(jì)算結(jié)果均要保存.即當(dāng)設(shè)high值限定為K值時(shí),對于c變量,通過該步驟,需要計(jì)算K次,為c保存K個(gè)空間.當(dāng)c繼續(xù)進(jìn)行后續(xù)操作時(shí),將需要對每個(gè)c值進(jìn)行計(jì)算,從而導(dǎo)致其計(jì)算次數(shù)和保存空間成指數(shù)增長.

但對于懶替換策略,則直接將c認(rèn)為是不確定值,從而將原來的指數(shù)增長變?yōu)榱顺?shù)空間.由于本文分析的主要是鎖變量,其要求前后必須完全匹配,因此當(dāng)出現(xiàn)不確定值時(shí),則可說明其存在風(fēng)險(xiǎn)的可能性極大.當(dāng)然也存在不準(zhǔn)確的情況,如下所示:

for(i=0;i

但根據(jù)后續(xù)實(shí)驗(yàn)的檢測結(jié)果可以看出,所有測試用例的檢測結(jié)果均為出現(xiàn)誤檢測率,說明該情況出現(xiàn)的概率極低,本文的檢測方法具有較強(qiáng)的適應(yīng)性.

5　應(yīng)用舉例

為更好的說明以上能耗錯(cuò)誤分析方法,本文以能耗分析預(yù)處理源程序?yàn)槔?對OnCreate函數(shù)進(jìn)行分析,其第一次迭代過程分析過程中各狀態(tài)及使用的規(guī)則如表4所示,其中初始輸入數(shù)據(jù)如表3所示.假設(shè)函數(shù)getServerData主要完成從服務(wù)器端獲得數(shù)據(jù),因而該函數(shù)有可能因網(wǎng)絡(luò)問題而處于長時(shí)間等待狀態(tài),因此初始化該函數(shù)的執(zhí)行開銷為最大值τ.

表3　初始輸入數(shù)據(jù)

表4　OnCreate函數(shù)第一次迭代分析過程

續(xù)表

表5　各函數(shù)多次迭代結(jié)果分析

續(xù)表

表5給出各迭代遍中各函數(shù)的返回結(jié)果及變化標(biāo)記信息.有該表可以看出,經(jīng)過4次迭代后,3個(gè)函數(shù)的結(jié)果集均達(dá)到不動(dòng)點(diǎn),即變化標(biāo)記值均為“false”.此時(shí)從入口函數(shù)OnCreate的返回結(jié)果可以看出,其CE集合中有兩個(gè)元素,即“[6,10,k<3]”和“[14,16,k<3]”,從而表明在程序的行6到行10以及行14到行16之間,一旦滿足k<3的條件時(shí),可能存在的No-SleepDilation類錯(cuò)誤(主要由于getServerData長時(shí)間等待操作).從最終鎖變量映射表σ={,}可知,由于wm鎖變量的值不為0,存在鎖的添加與釋放不匹配的情況.根據(jù)對應(yīng)的鎖約束條件P可知,其鎖不匹配現(xiàn)象將在k≥3的情況下出現(xiàn).

6　實(shí)驗(yàn)結(jié)果與分析

6.1實(shí)驗(yàn)構(gòu)建

為評估該方法的有效性,本文以Java為目標(biāo)語言,先對Android源碼社區(qū)的10個(gè)開源App隨機(jī)插入能耗錯(cuò)誤,并對18個(gè)惡意App進(jìn)行反編譯獲得對應(yīng)的源程序,然后利用eclipse中的ASTParser作為Java源代碼的前端解析器,生成對應(yīng)的AST分析樹.接著以該分析樹為基礎(chǔ),構(gòu)建上節(jié)提出的錯(cuò)誤檢測方案.最后將分析結(jié)果同文獻(xiàn)[3]中提出的基于數(shù)據(jù)流分析的方法進(jìn)行對比,以獲得該方法的最終評估效果.具體實(shí)驗(yàn)框架如圖1所示.

6.2實(shí)驗(yàn)結(jié)果與分析

在具體實(shí)驗(yàn)過程中,本文采用開源社區(qū)AppCodes的9個(gè)Android源程序?yàn)榛A(chǔ),通過在其中隨機(jī)插入能耗錯(cuò)誤構(gòu)建本文實(shí)驗(yàn)的測試用例.通過與文獻(xiàn)[3]中基于數(shù)據(jù)流錯(cuò)誤檢測技術(shù)的對比,獲得如表 6所示實(shí)驗(yàn)結(jié)果.根據(jù)前面所述的能耗模型,編譯器在能耗錯(cuò)誤檢測過程的綠色指標(biāo)主要與錯(cuò)誤檢測的精度(包括檢測的總錯(cuò)誤數(shù)和誤檢測的錯(cuò)誤數(shù))以及給出的錯(cuò)誤路徑的精度(包括給出出錯(cuò)時(shí)對應(yīng)的正確執(zhí)行路徑數(shù)以及錯(cuò)誤的執(zhí)行路徑數(shù))兩大部分組成,因此在該中主要給出了4個(gè)指標(biāo):其中PE和DE分別表示路徑型禁止休眠能耗錯(cuò)誤和擴(kuò)展型禁止休眠能耗錯(cuò)誤,MD和MP分別表示誤報(bào)的錯(cuò)誤數(shù)和誤報(bào)的路徑數(shù).由于競爭型能耗錯(cuò)誤通常通過人為指定事件觸發(fā)順序,然后進(jìn)行檢測.而在知曉了事件觸發(fā)順序后,則可以通過該觸發(fā)順序很直接的按照前兩類能耗錯(cuò)誤檢測方法進(jìn)行檢測,因而本文未對其進(jìn)行分析驗(yàn)證.

表6　能耗錯(cuò)誤檢測實(shí)驗(yàn)結(jié)果

接著,本文對現(xiàn)有的18個(gè)惡意App進(jìn)行反編譯,獲得其對應(yīng)的源程序,然后通過與文獻(xiàn)[3]中基于數(shù)據(jù)流錯(cuò)誤檢測技術(shù)的對比,獲得如表 7所示實(shí)驗(yàn)結(jié)果.

表7　能耗錯(cuò)誤檢測試驗(yàn)結(jié)果2

由以上實(shí)驗(yàn)結(jié)果可以看出,基于數(shù)據(jù)流分析的能耗錯(cuò)誤檢測方法與符號執(zhí)行技術(shù)能耗錯(cuò)誤檢測方法均有較高的檢測準(zhǔn)確度,對于植入的能耗錯(cuò)誤,其誤報(bào)率均為0.但基于數(shù)據(jù)分析的能耗錯(cuò)誤主要針對于不計(jì)數(shù)性的鎖變量進(jìn)行檢測,且未考慮檢測擴(kuò)展型禁止休眠能耗錯(cuò)誤,因此對于該類錯(cuò)誤無能為力,因而其總體錯(cuò)誤檢測率明顯低于本文方法.

通過對表7中18個(gè)測試用例檢測的能耗錯(cuò)誤進(jìn)行修正,然后采用紅米note手機(jī)實(shí)測半小時(shí),獲得的能耗對比結(jié)果如表8所示.

表8　能耗對比結(jié)果

由以上能耗結(jié)果可以看出,修正能耗錯(cuò)誤后,采用數(shù)據(jù)流分析的方法平均能夠節(jié)約29%的能耗,而本文的分析方法能夠進(jìn)一步提升能耗的效率,平均能夠節(jié)約62.6%的能耗,這對于依靠容量有限的電池作為電源的智能移動(dòng)終端設(shè)備將是十分重要的.

7　總結(jié)

能耗是綠色需求中一個(gè)重要指標(biāo),能耗錯(cuò)誤檢測對提高系統(tǒng)的綠色程度具有不容忽視的作用.本文首先對能耗錯(cuò)誤的分類以及符號執(zhí)行技術(shù)進(jìn)行簡要分析,然后針對禁止休眠類能耗錯(cuò)誤,以符號執(zhí)行技術(shù)為基礎(chǔ),設(shè)計(jì)了能耗錯(cuò)誤檢測和定位方法.該方法首先利用過程內(nèi)分析,獲得單個(gè)函數(shù)的符號執(zhí)行信息,然后利用過程間分析對單個(gè)函數(shù)的符號執(zhí)行信息進(jìn)行全局分析,以獲得較為準(zhǔn)確的執(zhí)行開銷、鎖變量匹配等相關(guān)信息,檢測出對應(yīng)的能耗相關(guān)錯(cuò)誤.同時(shí),符號執(zhí)行記錄了對應(yīng)的分支路徑信息,利用該信息不但較好的生成對應(yīng)的測試用例,而且可以結(jié)合約束求解器快速定位錯(cuò)誤位置,為開發(fā)出高綠色指標(biāo)的軟件提供保障.

[1]Pathak A,Hu Y C,Zhang M.Bootstrapping energy debugging on smartphones:a first look at energy bugs in mobile devices[A].Proceedings of the 10th ACM Workshop on Hot Topics in Networks[C].Cambridge,USA:ACM;2011.5-10.

[2]Pathak A,Hu Y C,Zhang M.Where is the energy spent inside my app?:fine grained energy accounting on smartphones with eprof[A].Proceedings of the 7th ACM european conference on Computer Systems[C].Bern,Switzerland:ACM;2012.29-42.

[3]Pathak A,Jindal A,Hu Y C,et al.What is keeping my phone awake:characterizing and detecting no-sleep energy bugs in smartphone apps[A].Proceedings of the 10th international conference on Mobile systems,applications,and services[C].Ambleside,United Kingdom:ACM;2012.267-280.

[4]Vekris P,Jhala R,Lerner S,et al.Towards verifying android apps for the absence of no-sleep energy bugs[A].Proceedings of the 2012 USENIX conference on Power-Aware Computing and Systems[C].New York,USA:USENIX Association;2012.3-13.

[5]Oliner A J,Iyer A,Lagerspetz E,et al.Collaborative energy debugging for mobile devices[A].Proceedings of the Eighth USENIX conference on Hot Topics in System Dependability[C].Berkeley,CA,USA:USENIX Association;2012.6-6.

[6]Jindal A,Pathak A,Hu Y C,et al.Hypnos:understanding and treating sleep conflicts in smartphones[A].Proceedings of the 8th ACM European Conference on Computer Systems[C].Prague,Czech Republic:ACM;2013.253-266.

[7]King J C.Symbolic execution and program testing[J].Communications of the ACM,1976,19(7):385-394.

[8]Boyer R S,Elspas B,Levitt K N.SELECT-a formal system for testing and debugging programs by symbolic execution[J].Acm Sigplan Notices,1975,10(6):234-245.

[9]Khurshid S,P?s?reanu C S,Visser W.Generalized Symbolic Execution for Model Checking and Testing[M].Tools and Algorithms for the Construction and Analysis of Systems.Springer Berlin Heidelberg,2003.553-568.

[10]P Godefroid,N Klarlund,K Sen.DART:Directed Automated Random Testing[A].Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation[C].Chicago,USA;2005.213-223.

[11]Majumdar R,Sen K.Hybrid concolic testing[A].29th International Conference on Software Engineering[C].Minneapolis,USA:IEEE;2007.416-426.

[12]Burnim J,Sen K.Heuristics for Scalable Dynamic Test Generation[J].IEEE Computer Society,2008(8):443-446.

[13]Anand S,Godefroid P,Tillmann N.Demand-Driven Compositional Symbolic Execution[M].Tools and Algorithms for the Construction and Analysis of Systems.Springer Berlin Heidelberg,2008.367-381.

[14]Staats M,Pǎsǎreanu C.Parallel symbolic execution for structural test generation[A].Proceedings of the 19th international symposium on Software testing and analysis[C].Trento,Italy:ACM;2010.183-194.

[15]Anand S,P?s?reanu C S,Visser W.JPF-SE:A Symbolic Execution Extension to Java Pathfinder[M].Springer Berlin Heidelberg,Tools and Algorithms for the Construction and Analysis of Systems,2007:134-138.

[16]Cadar C,Dunbar D,Engler D R.KLEE:Unassisted and automatic generation of high-coverage tests for complex systems programs[A].OSDI[C].Berkeley,USA;2008.209-224.

[17]Cadar C,Ganesh V,Pawlowski P M,et al.EXE:automatically generating inputs of death[J].ACM Transactions on Information and System Security (TISSEC),2008,12(2):10-20.

[18]Sen K,Marinov D,Agha G.CUTE:A Concolic Unit Testing Engine for C[M].ACM,2005.50-60.

[19]梅宏,王千祥,張路,等.軟件分析技術(shù)進(jìn)展[J].計(jì)算機(jī)學(xué)報(bào),2009,32(9):1697-1710.

MEI Hong,WANG Qian-Xiang,ZHANG Lu,et al.Software Analysis:A road map[J].Chinese Journal of Computers,2009,32(9):1697-1710.(in Chinese)

[20]范文慶.分段符號執(zhí)行模型及其環(huán)境交互問題研究[D].北京:北京郵電大學(xué),2010.40-50.

Fan Wenqing.Research on the implementation model of the sub symbolic execution model and its environment interaction[D].Beijing:Beijing University of Posts and Telecommunications,2010.40-50.(in Chinese)

[21]Boonstoppel P,Cadar C,Engler D.RWset:Attacking Path Explosion in Constraint-Based Test Generation[M].Springer Berlin Heidelberg,Tools and Algorithms for the Construction and Analysis of Systems，2008.351-366.

[22]Schwartz E J,Avgerinos T,Brumley D.All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask)[A].2010 IEEE Symposium on Security and Privacy[C].Oakland,California;2010.317-331.

[23]林夢香,陳胤立,陳睿,等.基于懶替換的C符號執(zhí)行[J].北京航空航天大學(xué)學(xué)報(bào),2009,06(6):687-691.

Lin Mengxiang,Chen Yinli,Chen Rui,et al.Execution of C symbols based on lazy replacement[J].Journal of BeiJing University of Aeronautics and Astronautics,2009,06(6):687-691.(in Chinese)

徐超男,1980年出生,湖北紅安人,博士,副教授,研究方向?yàn)榭尚跑浖?、嵌入式系統(tǒng)和計(jì)算機(jī)審計(jì).

E-mail:xuchao@nau.edu.cn

陳勇(通信作者)男,1986年出生,湖南婁底人,博士,工程師,研究方向?yàn)橹饕芯款I(lǐng)域?yàn)榫幾g優(yōu)化,可信軟件,嵌入式系統(tǒng)優(yōu)化.

E-mail:cyong1000@163.com

Symbolic Execution Based Energy Bug Detecting Method

XU Chao1,CHEN Yong2,GE Hong-mei1,HE Yan-xiang3

(1.NanjingAuditUniversity,Nanjing,Jiangsu210029,China;2.The14thResearchInstituteofCETC,Nanjing,Jiangsu210013,China; 3.ComputerSchoolofWuhanUniversity,Wuhan,Hubei430072,China)

Energy is one important bottleneck to the development of intelligent portable device.With the wide use of embedded operation system,the energy bug caused by unsuitablely using the API of the operation system has become the important factor in the designment of the embedded application.According to the characteristics of the No-Sleeping energy bug,a symbolic execution based energy bug detecting method is proposed to reduce the energy bug.It first uses intraprocedural analysis technology to analyze one function independently to get the energy information of the function.Then,the interprocedural analysis technology is applied to get the globe analysis of the program by the information of intraprocedural analysis which can get more accuate information for energy bug detection.Meanwhile,constraint solver can be combined to obtain the counter-example for locating the position of the error.Example and experiment results verify that the method is feasible and effective in energy bug detection.

energy bug;symbolic execution;bug detection;intraprocedural analysis;interprocedural analysis

2015-09-27;

2016-01-04;責(zé)任編輯:馬蘭英

國家自然科學(xué)基金(No.61170022);江蘇省高校自然科學(xué)研究面上項(xiàng)目(No.15KJB520019);江蘇省“六大人才”高峰項(xiàng)目資助;江蘇省高?！扒嗨{(lán)工程”優(yōu)秀青年骨干教師培養(yǎng)對象資助;江蘇高校優(yōu)勢學(xué)科建設(shè)工程資助項(xiàng)目

TP311

A

0372-2112 (2016)05-1040-11

電子學(xué)報(bào)URL:http://www.ejournal.org.cn10.3969/j.issn.0372-2112.2016.05.005