diff options
| author | Cristian Cadar <cristic@cs.stanford.edu> | 2012-09-12 14:37:39 +0000 |
|---|---|---|
| committer | Cristian Cadar <cristic@cs.stanford.edu> | 2012-09-12 14:37:39 +0000 |
| commit | 9b5e99905e6732d64522d0efc212f3f1ce290ccc (patch) | |
| tree | 58739c4be56a01b436fc1fffae5dadc4fe3b8ea3 /www | |
| parent | 1e6f7d11bafab8c8eef907c7bc0a165ce426984b (diff) | |
| download | klee-9b5e99905e6732d64522d0efc212f3f1ce290ccc.tar.gz | |
Restructured the command-line options for setting the search
heuristics in KLEE. The new options are documented at http://klee.llvm.org/klee-options.html. Cleaned a bit the code in UserSearcher.cpp, and fixed some test cases to use the new options. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@163711 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'www')
| -rw-r--r-- | www/Documentation.html | 5 | ||||
| -rw-r--r-- | www/klee-options.html | 73 |
2 files changed, 78 insertions, 0 deletions
diff --git a/www/Documentation.html b/www/Documentation.html index cf20cc5d..b266e439 100644 --- a/www/Documentation.html +++ b/www/Documentation.html @@ -23,6 +23,11 @@ </li> <li> + <a href="klee-options.html">KLEE Options</a>: + Overview of the KLEE's main command-line options. + </li> + + <li> <a href="klee-files.html">KLEE Generated Files</a>: Overview of the main files generated by KLEE. diff --git a/www/klee-options.html b/www/klee-options.html new file mode 100644 index 00000000..22871e0e --- /dev/null +++ b/www/klee-options.html @@ -0,0 +1,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> |