KLEE命令行参数一览

• 文献标题： Overview of KLEE’s main command-line options
• 文献作者： The KLEE Team.
• 文献来源： http://klee.github.io/docs/options/
• 阅读日期： 2015年12月24日09时许
• 阅读程度： 速读

启发式搜索

• KLEE提供四种启发式搜索模式：

  1. Depth-First Search (DFS): 深度优先.
  2. Random State Search:随机状态选择.
  3. Random Path Selection: 随机路径选择（见KLEE OSDI’08）.
  4. Non Uniform Random Search (NURS):根据所给分发，随机选择状态。分发可基于到未覆盖指令的最小距离（MD2U），查询代价等

• 选择搜索模式的参数是--search,例如
  $ klee --search=dfs demo.o
  $ klee --search=random-path demo.o

• search的参数列表为：

  $ 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
  

• 交错式启发式搜索

  在KLEE中可以循环使用交错的启发式搜索。例如
  $ klee --search=random-state --search=nurs:md2u demo.o

• KLEE中默认的搜索模式

  random-path 和 nurs:covnew.的交错模式。

查询记录

为了记录KLEE进行符号执行的查询过程，可以使用下列参数：

• --use-query-log=TYPE:FORMAT

  TYPE：记录的内容

  • all：记录KLEE在没有优化前的所有查询。

  • solver： 只记录传递给KLEE求解器的查询。注意，一些未优化的查询可能在被KLEE执行前没有执行或修改。

  FORMAT：记录的格式

  • pc，KQuery格式
  • smt2，SMT-LIBv2格式。

• --min-query-time-to-log=TIME (毫秒)

  用于记录超过一定时间限制的查询。

  TIME：毫秒计

  • 等于0时： (默认): 记录所有
  • 小于0时： TIME为负数时，只记录超时的查询，超时值由参数--max-solver-time描述。
  • 大于0时： only queries that took more that TIME milliseconds should be logged.（看不明白 ( ╯□╰ )）

入口点

修改入口点的参数为-entry-point=FUNCTION_NAME， * FUNCTION_NAME*指用作执行入口的函数名。

调用klee-assume

在缺省情况下，当假定的condition不合理时，KLEE会报告一个错误，而使用参数-silent-klee-assume，则可以在此类情况下，悄然结束当前路径的探测。