- 文獻(xiàn)標(biāo)題： Overview of KLEE’s main command-line options
- 文獻(xiàn)作者： The KLEE Team.
- 文獻(xiàn)來(lái)源： http://klee.github.io/docs/options/
- 閱讀日期： 2015年12月24日09時(shí)許
- 閱讀程度： 速讀
啟發(fā)式搜索
-
KLEE提供四種啟發(fā)式搜索模式：
- Depth-First Search (DFS): 深度優(yōu)先.
- Random State Search:隨機(jī)狀態(tài)選擇.
- Random Path Selection: 隨機(jī)路徑選擇（見(jiàn)KLEE OSDI’08）.
- Non Uniform Random Search (NURS):根據(jù)所給分發(fā)次舌，隨機(jī)選擇狀態(tài)本刽。分發(fā)可基于到未覆蓋指令的最小距離（MD2U）濒募，查詢代價(jià)等
選擇搜索模式的參數(shù)是--search,例如
$ klee --search=dfs demo.o
$ klee --search=random-path demo.o-
search的參數(shù)列表為：
$ klee --help -search - Specify the search heuristic (default=random-path interleaved with nurs:covnew) =dfs - use Depth First Search (DFS) =random-state - randomly select a state to explore =random-path - use Random Path Selection (see OSDI'08 paper) =nurs:covnew - use Non Uniform Random Search (NURS) with Coverage-New heuristic =nurs:md2u - use NURS with Min-Dist-to-Uncovered heuristic =nurs:depth - use NURS with 2^depth heuristic =nurs:icnt - use NURS with Instr-Count heuristic =nurs:cpicnt - use NURS with CallPath-Instr-Count heuristic =nurs:qc - use NURS with Query-Cost heuristic -
交錯(cuò)式啟發(fā)式搜索
在KLEE中可以循環(huán)使用交錯(cuò)的啟發(fā)式搜索麻顶。例如
$ klee --search=random-state --search=nurs:md2u demo.o -
KLEE中默認(rèn)的搜索模式
random-path 和 nurs:covnew.的交錯(cuò)模式锥忿。
查詢記錄
為了記錄KLEE進(jìn)行符號(hào)執(zhí)行的查詢過(guò)程，可以使用下列參數(shù)：
-
--use-query-log=TYPE:FORMAT
TYPE：記錄的內(nèi)容
all：記錄KLEE在沒(méi)有優(yōu)化前的所有查詢贬芥。
solver： 只記錄傳遞給KLEE求解器的查詢来庭。注意，一些未優(yōu)化的查詢可能在被KLEE執(zhí)行前沒(méi)有執(zhí)行或修改丧肴。
FORMAT：記錄的格式
- pc残揉，KQuery格式
- smt2，SMT-LIBv2格式芋浮。
-
--min-query-time-to-log=TIME (毫秒)
用于記錄超過(guò)一定時(shí)間限制的查詢抱环。
TIME：毫秒計(jì)
- 等于0時(shí)： (默認(rèn)): 記錄所有
- 小于0時(shí)： TIME為負(fù)數(shù)時(shí)，只記錄超時(shí)的查詢纸巷，超時(shí)值由參數(shù)--max-solver-time描述镇草。
- 大于0時(shí)： only queries that took more that TIME milliseconds should be logged.（看不明白 ( ╯□╰ )）
入口點(diǎn)
修改入口點(diǎn)的參數(shù)為-entry-point=FUNCTION_NAME， * FUNCTION_NAME*指用作執(zhí)行入口的函數(shù)名瘤旨。
調(diào)用klee-assume
在缺省情況下梯啤，當(dāng)假定的condition不合理時(shí)，KLEE會(huì)報(bào)告一個(gè)錯(cuò)誤存哲，而使用參數(shù)-silent-klee-assume因宇，則可以在此類(lèi)情況下，悄然結(jié)束當(dāng)前路徑的探測(cè)祟偷。
