1、使用KLEEfe成高代碼覆蓋率的測試用例一、實驗目的本實驗可以幫助學生了解動態符號執行工具KLEE的基本功能一為進一步研究符號執行技術的理論與應用提供基礎。二、實驗內容及環境本實驗展示如何利用klee對一個被測目標函數進行符號執行， 覆蓋全部路徑，并生成測試用例的具體操作流程。實驗虛擬機為Ubuntu 16.04.1 LTS 6g操作系統。三、klee安裝1 .進入安裝主頁klee網站http:/klee.github.io/中有相關的安裝方法，點擊Use KLEE Docke門mage進入。如圖1。usingWhM h Docfcef?Irstailln Docker而白唱肘/Kl FT 口

2、 fx： k*-T jri 后即1FulinE Irom the Etocter Hut>圖1安裝主頁2 .安裝 docker (ubuntu)點擊進入ubuntu版本的docker入口，如圖2.Installing Docker國M通革角一匕米噌：/a口鼠”IWC6wmD&：發7共 日用他-：Jj1 flba- nrtrucScn!i b LbJh.CI . qf Web-，.圖2安裝入口3 .安裝 linux-image-extra-冠更新包管理器sudo apt-get update安裝命令包sudo apt-get install linux-image-extra-$(

3、uname -r) linux-image-extra-virtual4 .更新apt源更新包信息一些準備工作，逐條輸入指令即可，不再展開介紹。sudo apt-get updatesudo apt-get install apt-transport-https ca-certificatessudo apt-key adv -keyserver hkp:ha.pool.sks-:80 -recv-keys 58118E89F3A912897c070ADBF76221572c52609D更新apt源打開 /etc/apt/sources.list.d/docker.list 文件，沒有就創建一

4、個，里面加一句話，如下：gedit/etc/apt/sources.list.d/docker.list輸入 deb /repo ubuntu-xenial main 并各文本保存。更新軟件源sudo apt-get update確定APT連接的是正確的倉庫 apt-cache policy docker-engine5 .安裝最新版本docker安裝dockersudo apt-get install docker-engine啟動docker服務sudo service docker start驗證安裝是否成功，若顯示如圖3所示，則安

5、裝成功sudodocker run hello-worlda -lUjru.vM僮|KM>HUl«i3U»tU>： SUM仙力Siudo) pjssword for xuku :Hello fr« DoclEer!Thti tA9-*thJt mir Ih-lI LihftJExrxthf.To g«riieritr this ness-a9e1. Dicker toc*L 七lie follDMiing steps:1 .» Th#tn|tM 04chlt*依ftok2 . The L-scker daentwi pulled t

6、be "hello-world' Inage frcn the Daciker Hub.I- TM 師c“r的加m</專射7 4 ne*財工加11Tg tMt Vnit? 51通 <修口噂imexentikiblie th«t ipradhiEes tl*e output you arr currmtly refiittfig.TIm toeJtotr dMMMthat autput ，白fcelAr elient.M*ne itt* Er t«r<RtMl ATa try f«ftfnar.事*It，帆,.(事件v商 事育力t

7、C4hE4tiW wlths$ docker run -it ubuntu b4：s-hShare- tFuge-K, autcnate wrlflotn and RDre- trith a free Cockier Hub riccount: httm: /hub. daekjtr. cmFar rwre exarFwles «nd lifceas B visit:圖3 docker安裝成功6 .下載KlE瞄像docker pull klee/klee7 .運行KLEEB像docker run -rm -ti -ulimit='stack=-1:-T klee/klee進入

8、到klee操作界面，如圖4：decker 4曲 aadtnt 匕 1slMm111圖4 klee界面退出命令則是：exit四、實驗步驟1 .選取目標函數函數get_sign如圖5所示：int get_sign(int x if (x = 0) return 0;if (x < 0) return -1;elsereturn 1； 圖5目標函數2 .對目標函數進行插裝對上述目標函數進行插裝，得到源代碼程序get_sign.c打開/Home/klee/examples/get_sign 中的 get_sign.c, 如圖 6所示:int get sign(int x) if x = &quo

9、t;i return H;i£ (k < >-) return "els* return ;I int itainO f int. a ； klee make syrabol ic ( 史上 W 電力:£,三f " a' ) f t色七uz：jft get_sign (a)；)圖6源代碼程序其中，klee_make_symbolic函數將某一個變量符號化。該函數需要三個參數：符號變量地址，符號變量占用內存字節，和它所采用的符號名稱。由于klee相關可執行文件在klee目錄下，所以將get_sign.c放到/Home/klee 目 錄下

10、。3 .編譯成LLVM中間語言KLEE在LLVM中間語言字節碼上進行操作。我們要使用 clang-I ././include -emit-llvm -c -g get_sign.c 將源碼 get_sign.c編譯成 LLVM 中間語言,得到get_sign.bc文件。命令如下：clang -I ././include -emit-llvm -c -g get_sign.c-I是為了讓編譯器可以找到<klee/klee.h>頭文件-g是為了增到調試信息到bitcode文件中。結果如圖7：O kl.w>Upr*4BVe; W，/Idxjrc 用 rwnifri ”必 jMgn4

11、1mMi5，E;二很iH-WHwxaSWGL+M*-T 一，一八就IM總h -c gtt.fi|fi .c k Iweff我詁 1,5W 5 ;-/*kl«_src/ejc amplHps/get.st g咕 Iskl«ff4«c561.5S5,-/kl«=src/tK»nplrs/grt,itQn1 |圖7生成LLVM中間語言4.klee進行符號執行用klee對編譯后得到的中間語言進行符號執行，命令如下:kleeget_sign.bcKLE前號執行后的輸出信息如圖8所示:0設修.的2,1, $一聞./iK/tMfnpy產kUeaf44McMl

12、&e5；*/klH_»rc/exm>lei/geK_si.gifi$ cling - P4/.4/uclude emic-llw r -< / qMjtg.ekl電4f44+3 cS61 sa51-/klee_&rc/«xaiqple5/get_s LgM tsget_i(gn,bc.atl«0f48iac5fil5i9 5/klMTsrc/exMplr5/grt_5iginilS kier grtstflpabc«LE £ ? QUitput dlrct”y Is * hne/ kleek l«_srer

13、ples/gt t_s tgn/k We - unt -1*LMlg STP- S6lFtf b配上mut幸 *1KittsCffnpIviH, 3IC1EE1 d成用。上QHi曲廣辦史2M teStfi 3ilnlf44MC Hl 505； -/kl M_>K/CKM|>l«/WrtLS UinS Ug«t_<tgni.版亡口部.c kl«« -lait kl««-*ut-3km(r44Mc5fiLSfl5：-/klee_sF£ /exaipln/ge t.slgns .圖8 klee符號執行我們選取的g

14、et_sign函數，有三條路徑。程序分別在 a為0, a大于0和a小于0時執行。KLEEQ寸所有三條路徑進行探索，并且為每一條路徑生成一個包含具體值而非符號值的測試用例。5.查看生成的測試用例信息每當命令klee執行一次（注：針對不同或相同的LLVM中間字節碼執行），就會在當前目錄下生成一個klee執行后的信息統計文件。并且有一個快捷方式klee-last,指向最新一次因klee執行而生成的目 錄 klee-out-X。在klee-last指向的目錄中的文件如圖9所示：KIm2修，*48915&|15gMmfid也豈寫£色復含apl生玉，。電l£ listflsse

15、Hbly.ll Hmagr%. tut run. stats. ktrit Narflings. t«tidnforun. tstatstestBflfJeoi .ktest testBe6&B3 .ktestklEUQ F酬15電昌ft*Et 由E 1。力& 圖 9 klee-last 目錄在klee執行信息目錄下的以“ .ktest”為后綴名的文件中，包含有 klee產生的測試用例。在對get_sign函數進行符號執行以后，產 生了三個測試用例，分別位于 test000001.ktest, test000002.ktest, test000003.ktest文件中

16、。在klee-last目錄下用命令行鍵入如下命 令：ktest-tool -write-intsklee-last/test000001.ktest顯示test000001.ktest文件如圖10所示：（該測試用例是執行x>0 時的路徑得來）r44H'£ ' r '1 .】ry,l h -I »! I rr Inh It t電白含電電I, hfm工Cktes.!: ftie : 1 klee- last/ testftfla&&1 Jktest"“條；如iu版.o&jrctbJa'objectfl: i

17、lzc: 4lofijectfl: data: 0kltefFMIBc S41M5 s-/klet&irc/thwpltf/g«t.slgrt5 I圖 10 test000001.ktest 文件內容更新命令，顯示test000002.ktest文件如圖11所示：（該測試用例是執行x=0時的路徑得來）hMf448i«cSA1545i-/klte_>r/eK«HpUi/gvt_jlDnS-NrUe-Uti kl«-lsiktest ftle : 1 klee - last/testwee>82. ktetsB：小口刷.阮】obectb:

18、 ndne bRa'電；$tlf: 4 0;曲M; 1664 女411448：9匚5通1505:匚/七小總打41型£lgn$ 圖 11 test000002.ktest 文件內容更新命令，顯示test000003.ktest文件如圖12所示：（該測試用例 是執行x=0時的路徑得來）He rt f we9c 54 i MI: */it lee_ src /e»«plen/oet_it g s S k test-Coolwr1ite4nts klee-U4kte&t file i' k lee- Last / tes teMfr&3. ktes t«rgi :ftum 6beet£*1object &inwe:b"，。工Um：4object 6t data： -21<74S