blob: 22871e0e76aa847d72dc286c5b33e5b1b84b6366 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN"
"http://www.w3.org/TR/html4/strict.dtd">
<!-- Material used from: HTML 4.01 specs: http://www.w3.org/TR/html401/ -->
<html>
<head>
<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
<title>The KLEE Symbolic Virtual Machine</title>
<link type="text/css" rel="stylesheet" href="menu.css">
<link type="text/css" rel="stylesheet" href="content.css">
</head>
<body>
<!--#include virtual="menu.html.incl"-->
<div id="content">
<!--*********************************************************************-->
<h1>KLEE Options</h1>
<!--*********************************************************************-->
<h2>Search Heuristics</h2>
<h3>Main search heuristics</h3>
<p>
KLEE provides four main search heuristics:
<ol>
<li><b>Depth-First Search (DFS):</b> Traverses states in depth-first order.</li>
<li><b>Random State Search:</b>Randomly selects a state to explore.</li>
<li><b>Random Path Selection:</b> Described in our <a href="http://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf">KLEE OSDI'08</a> paper.</li>
<li><b>Non Uniform Random Search (NURS):</b> Selects a state randomly according to a given distribution. The distribution can be based on the minimum distance to an uncovered instruction (MD2U), the query cost, etc.
</ol>
To select a search heuristic, use the <b>--search</b> option provided by KLEE. For example:
<pre class="output">
$ klee --search=dfs demo.o</pre>
runs <i>demo.o</i> using DFS, while
<pre class="output">
$ klee --search=random-path demo.o </pre>
runs it using the random path selection strategy.
The full list of options is shown in KLEE's help message:
<pre class="output">
$ 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 </pre>
<h3>Interleaving search heuristics</h3>
<p>
Search heuristics in KLEE can be interleaved in a round-robin
fashion. To interleave several search heuristics to be interleaved, use the <b>--search</b> multiple times. For example:
<pre class="output">
$ klee --search=random-state --search=nurs:md2u demo.o </pre>
interleaves the Random State and the NURS:MD2U heuristics in a round robin fashion.
<br/>
</p>
<h3>Default search heuristics</h3>
<p>
The default heuristics used by KLEE are <i>random-path</i> interleaved with <i>nurs:covnew</i>.
</p>
</div>
</body>
</html>
|
