面向復(fù)雜運(yùn)算程序的符號(hào)執(zhí)行搜索策略研究.pdf

1、隨著軟件在信息社會(huì)發(fā)揮著越來越重要的作用，人們對(duì)軟件可信性質(zhì)的要求也越來越高。作為一種精確的程序分析技術(shù)，符號(hào)執(zhí)行能夠有效地提高軟件的可信性質(zhì)，因此被廣泛地應(yīng)用于學(xué)術(shù)界和工業(yè)界。但是，符號(hào)執(zhí)行中約束求解所占的時(shí)間比例非常高。同時(shí)，不同復(fù)雜度的約束的求解時(shí)間開銷差距懸殊，很小一部分復(fù)雜約束的求解占用了大部分的求解時(shí)間。這一現(xiàn)象在對(duì)包含復(fù)雜數(shù)值計(jì)算的程序進(jìn)行符號(hào)執(zhí)行時(shí)尤為明顯。該現(xiàn)象限制了求解器在指定時(shí)間內(nèi)的約束求解數(shù)，從而降低了符號(hào)執(zhí)行的

2、語(yǔ)句覆蓋率和路徑覆蓋率。
　　針對(duì)以上特征，本文提出了基于求解開銷預(yù)測(cè)的符號(hào)執(zhí)行搜索策略。約束的復(fù)雜度和它的邏輯表達(dá)式長(zhǎng)度、包含的運(yùn)算和操作類型，以及涉及的變量和常量的類型及大小等因素有關(guān)?；趯?shí)驗(yàn)總結(jié)出了度量約束復(fù)雜度的經(jīng)驗(yàn)公式，并結(jié)合約束的歷史求解開銷來預(yù)測(cè)當(dāng)前的求解開銷，通過對(duì)求解開銷預(yù)測(cè)值進(jìn)行加權(quán)實(shí)現(xiàn)了加權(quán)隨機(jī)的搜索策略，從而在符號(hào)執(zhí)行過程中優(yōu)先探索求解開銷較小的路徑。本文在KLEE中實(shí)現(xiàn)了上述搜索策略，并對(duì)GNU科學(xué)計(jì)算