面向復雜運算程序的符號執(zhí)行搜索策略研究.pdf

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

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