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

11 files changed, 181 insertions, 125 deletions

diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index 9703e973..58772bbb 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -66,6 +66,18 @@ namespace klee {
       tmp.insert(es);
       update(current, std::set<ExecutionState*>(), tmp);
     }
+
+    enum CoreSearchType {
+      DFS,                
+      RandomState,
+      RandomPath,
+      NURS_CovNew,
+      NURS_MD2U,
+      NURS_Depth,
+      NURS_ICnt,
+      NURS_CPICnt,
+      NURS_QC
+    };
   };
 
   class DFSSearcher : public Searcher {
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index 1aff9e5e..361092d2 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -20,61 +20,27 @@ using namespace llvm;
 using namespace klee;
 
 namespace {
-  cl::opt<bool>
-  UseRandomSearch("use-random-search");
-
-  cl::opt<bool>
-  UseInterleavedRS("use-interleaved-RS");
-
-  cl::opt<bool>
-  UseInterleavedNURS("use-interleaved-NURS");
-
-  cl::opt<bool>
-  UseInterleavedMD2UNURS("use-interleaved-MD2U-NURS");
-
-  cl::opt<bool>
-  UseInterleavedInstCountNURS("use-interleaved-icnt-NURS");
-
-  cl::opt<bool>
-  UseInterleavedCPInstCountNURS("use-interleaved-cpicnt-NURS");
-
-  cl::opt<bool>
-  UseInterleavedQueryCostNURS("use-interleaved-query-cost-NURS");
+  cl::list<Searcher::CoreSearchType>
+  CoreSearch("search", cl::desc("Specify the search heuristic (default=random-path interleaved with nurs:covnew)"),
+	     cl::values(clEnumValN(Searcher::DFS, "dfs", "use Depth First Search (DFS)"),
+			clEnumValN(Searcher::RandomState, "random-state", "randomly select a state to explore"),
+			clEnumValN(Searcher::RandomPath, "random-path", "use Random Path Selection (see OSDI'08 paper)"),
+			clEnumValN(Searcher::NURS_CovNew, "nurs:covnew", "use Non Uniform Random Search (NURS) with Coverage-New"),
+			clEnumValN(Searcher::NURS_MD2U, "nurs:md2u", "use NURS with Min-Dist-to-Uncovered"),
+			clEnumValN(Searcher::NURS_Depth, "nurs:depth", "use NURS with 2^depth"),
+			clEnumValN(Searcher::NURS_ICnt, "nurs:icnt", "use NURS with Instr-Count"),
+			clEnumValN(Searcher::NURS_CPICnt, "nurs:cpicnt", "use NURS with CallPath-Instr-Count"),
+			clEnumValN(Searcher::NURS_QC, "nurs:qc", "use NURS with Query-Cost"),
+			clEnumValEnd));
 
   cl::opt<bool>
-  UseInterleavedCovNewNURS("use-interleaved-covnew-NURS");
-
-  cl::opt<bool>
-  UseNonUniformRandomSearch("use-non-uniform-random-search");
-
-  cl::opt<bool>
-  UseRandomPathSearch("use-random-path");
-
-  cl::opt<WeightedRandomSearcher::WeightType>
-  WeightType("weight-type", cl::desc("Set the weight type for --use-non-uniform-random-search"),
-             cl::values(clEnumValN(WeightedRandomSearcher::Depth, "none", "use (2^depth)"),
-                        clEnumValN(WeightedRandomSearcher::InstCount, "icnt", "use current pc exec count"),
-                        clEnumValN(WeightedRandomSearcher::CPInstCount, "cpicnt", "use current pc exec count"),
-                        clEnumValN(WeightedRandomSearcher::QueryCost, "query-cost", "use query cost"),
-                        clEnumValN(WeightedRandomSearcher::MinDistToUncovered, "md2u", "use min dist to uncovered"),
-                        clEnumValN(WeightedRandomSearcher::CoveringNew, "covnew", "use min dist to uncovered + coveringNew flag"),
-                        clEnumValEnd));
-  
-  cl::opt<bool>
-  UseMerge("use-merge", 
-           cl::desc("Enable support for klee_merge() (experimental)"));
- 
-  cl::opt<bool>
-  UseBumpMerge("use-bump-merge", 
-           cl::desc("Enable support for klee_merge() (extra experimental)"));
- 
-  cl::opt<bool>
   UseIterativeDeepeningTimeSearch("use-iterative-deepening-time-search", 
                                     cl::desc("(experimental)"));
 
   cl::opt<bool>
   UseBatchingSearch("use-batching-search", 
-           cl::desc("Use batching searcher (keep running selected state for N instructions/time, see --batch-instructions and --batch-time"));
+		    cl::desc("Use batching searcher (keep running selected state for N instructions/time, see --batch-instructions and --batch-time)"),
+		    cl::init(false));
 
   cl::opt<unsigned>
   BatchInstructions("batch-instructions",
@@ -85,68 +51,62 @@ namespace {
   BatchTime("batch-time",
             cl::desc("Amount of time to batch when using --use-batching-search"),
             cl::init(5.0));
+
+
+  cl::opt<bool>
+  UseMerge("use-merge", 
+           cl::desc("Enable support for klee_merge() (experimental)"));
+ 
+  cl::opt<bool>
+  UseBumpMerge("use-bump-merge", 
+           cl::desc("Enable support for klee_merge() (extra experimental)"));
+
 }
 
+
 bool klee::userSearcherRequiresMD2U() {
-  return (WeightType==WeightedRandomSearcher::MinDistToUncovered ||
-          WeightType==WeightedRandomSearcher::CoveringNew ||
-          UseInterleavedMD2UNURS ||
-          UseInterleavedCovNewNURS || 
-          UseInterleavedInstCountNURS || 
-          UseInterleavedCPInstCountNURS || 
-          UseInterleavedQueryCostNURS);
+  return (std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_MD2U) != CoreSearch.end() ||
+	  std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_CovNew) != CoreSearch.end() ||
+	  std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_ICnt) != CoreSearch.end() ||
+	  std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_CPICnt) != CoreSearch.end() ||
+	  std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_QC) != CoreSearch.end());
 }
 
-// FIXME: Remove.
-bool klee::userSearcherRequiresBranchSequences() {
-  return false;
+
+Searcher *getNewSearcher(Searcher::CoreSearchType type, Executor &executor) {
+  Searcher *searcher = NULL;
+  switch (type) {
+  case Searcher::DFS: searcher = new DFSSearcher(); break;
+  case Searcher::RandomState: searcher = new RandomSearcher(); break;
+  case Searcher::RandomPath: searcher = new RandomPathSearcher(executor); break;
+  case Searcher::NURS_CovNew: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::CoveringNew); break;
+  case Searcher::NURS_MD2U: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::MinDistToUncovered); break;
+  case Searcher::NURS_Depth: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::Depth); break;
+  case Searcher::NURS_ICnt: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::InstCount); break;
+  case Searcher::NURS_CPICnt: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::CPInstCount); break;
+  case Searcher::NURS_QC: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::QueryCost); break;
+  }
+
+  return searcher;
 }
 
 Searcher *klee::constructUserSearcher(Executor &executor) {
-  Searcher *searcher = 0;
-
-  if (UseRandomPathSearch) {
-    searcher = new RandomPathSearcher(executor);
-  } else if (UseNonUniformRandomSearch) {
-    searcher = new WeightedRandomSearcher(executor, WeightType);
-  } else if (UseRandomSearch) {
-    searcher = new RandomSearcher();
-  } else {
-    searcher = new DFSSearcher();
+
+  // default values
+  if (CoreSearch.size() == 0) {
+    CoreSearch.push_back(Searcher::RandomPath);
+    CoreSearch.push_back(Searcher::NURS_CovNew);
   }
 
-  if (UseInterleavedNURS || UseInterleavedMD2UNURS || UseInterleavedRS ||
-      UseInterleavedCovNewNURS || UseInterleavedInstCountNURS ||
-      UseInterleavedCPInstCountNURS || UseInterleavedQueryCostNURS) {
+  Searcher *searcher = getNewSearcher(CoreSearch[0], executor);
+  
+  if (CoreSearch.size() > 1) {
     std::vector<Searcher *> s;
     s.push_back(searcher);
-    
-    if (UseInterleavedNURS)
-      s.push_back(new WeightedRandomSearcher(executor, 
-                                             WeightedRandomSearcher::Depth));
-    if (UseInterleavedMD2UNURS)
-      s.push_back(new WeightedRandomSearcher(executor, 
-                                             WeightedRandomSearcher::MinDistToUncovered));
-
-    if (UseInterleavedCovNewNURS)
-      s.push_back(new WeightedRandomSearcher(executor, 
-                                             WeightedRandomSearcher::CoveringNew));
-   
-    if (UseInterleavedInstCountNURS)
-      s.push_back(new WeightedRandomSearcher(executor, 
-                                             WeightedRandomSearcher::InstCount));
-    
-    if (UseInterleavedCPInstCountNURS)
-      s.push_back(new WeightedRandomSearcher(executor, 
-                                             WeightedRandomSearcher::CPInstCount));
-    
-    if (UseInterleavedQueryCostNURS)
-      s.push_back(new WeightedRandomSearcher(executor, 
-                                             WeightedRandomSearcher::QueryCost));
-
-    if (UseInterleavedRS) 
-      s.push_back(new RandomSearcher());
 
+    for (unsigned i=1; i<CoreSearch.size(); i++)
+      s.push_back(getNewSearcher(CoreSearch[i], executor));
+    
     searcher = new InterleavedSearcher(s);
   }
 
@@ -154,10 +114,12 @@ Searcher *klee::constructUserSearcher(Executor &executor) {
     searcher = new BatchingSearcher(searcher, BatchTime, BatchInstructions);
   }
 
+  // merge support is experimental
   if (UseMerge) {
     assert(!UseBumpMerge);
+    assert(std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::RandomPath) == CoreSearch.end()); // XXX: needs further debugging: test/Features/Searchers.c fails with this searcher
     searcher = new MergingSearcher(executor, searcher);
-  } else if (UseBumpMerge) {    
+  } else if (UseBumpMerge) {
     searcher = new BumpMergingSearcher(executor, searcher);
   }
   
diff --git a/lib/Core/UserSearcher.h b/lib/Core/UserSearcher.h
index 9571bf5b..d01a017f 100644
--- a/lib/Core/UserSearcher.h
+++ b/lib/Core/UserSearcher.h
@@ -17,8 +17,6 @@ namespace klee {
   // XXX gross, should be on demand?
   bool userSearcherRequiresMD2U();
 
-  bool userSearcherRequiresBranchSequences();
-
   Searcher *constructUserSearcher(Executor &executor);
 }
 
diff --git a/test/Dogfood/ImmutableSet.cpp b/test/Dogfood/ImmutableSet.cpp
index bdb9f431..95320a82 100644
--- a/test/Dogfood/ImmutableSet.cpp
+++ b/test/Dogfood/ImmutableSet.cpp
@@ -1,5 +1,5 @@
 // RUN: %llvmgxx -I../../../include -g -DMAX_ELEMENTS=4 -fno-exceptions -emit-llvm -c -o %t1.bc %s
-// RUN: %klee --libc=klee --max-forks=200 --no-output --exit-on-error --optimize --disable-inlining --use-non-uniform-random-search --use-cex-cache %t1.bc
+// RUN: %klee --libc=klee --max-forks=200 --no-output --exit-on-error --optimize --disable-inlining --search=nurs:depth --use-cex-cache %t1.bc
 
 #include "klee/klee.h"
 #include "klee/Internal/ADT/ImmutableSet.h"
diff --git a/test/Feature/CopyOnWrite.c b/test/Feature/CopyOnWrite.c
index ee3ea15e..ce77c802 100644
--- a/test/Feature/CopyOnWrite.c
+++ b/test/Feature/CopyOnWrite.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
-// RUN: %klee --use-random-search --exit-on-error %t1.bc
+// RUN: %klee --search=random-state --exit-on-error %t1.bc
 
 #include <assert.h>
 
diff --git a/test/Feature/MakeSymbolicName.c b/test/Feature/MakeSymbolicName.c
index a4d4e2a6..a31b4a9b 100644
--- a/test/Feature/MakeSymbolicName.c
+++ b/test/Feature/MakeSymbolicName.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
-// RUN: %klee --use-random-search --exit-on-error %t1.bc
+// RUN: %klee --search=random-state --exit-on-error %t1.bc
 
 #include <assert.h>
 
diff --git a/test/Feature/Searchers.c b/test/Feature/Searchers.c
index d61037b9..b120d354 100644
--- a/test/Feature/Searchers.c
+++ b/test/Feature/Searchers.c
@@ -1,27 +1,30 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
 // RUN: %klee %t2.bc
-// RUN: %klee --use-random-search %t2.bc
-// RUN: %klee --use-non-uniform-random-search %t2.bc
-// RUN: %klee --use-non-uniform-random-search --weight-type=query-cost %t2.bc
+// RUN: %klee --search=random-state %t2.bc
+// RUN: %klee --search=nurs:depth %t2.bc
+// RUN: %klee --search=nurs:qc %t2.bc
 // RUN: %klee --use-batching-search %t2.bc
-// RUN: %klee --use-batching-search --use-random-search %t2.bc
-// RUN: %klee --use-batching-search --use-non-uniform-random-search %t2.bc
-// RUN: %klee --use-batching-search --use-non-uniform-random-search --weight-type=query-cost %t2.bc
-// RUN: %klee --use-merge --debug-log-merge --debug-log-state-merge %t2.bc
-// RUN: %klee --use-merge --use-batching-search %t2.bc
-// RUN: %klee --use-merge --use-batching-search --use-random-search %t2.bc
-// RUN: %klee --use-merge --use-batching-search --use-non-uniform-random-search %t2.bc
-// RUN: %klee --use-merge --use-batching-search --use-non-uniform-random-search --weight-type=query-cost %t2.bc
+// RUN: %klee --use-batching-search --search=random-state %t2.bc
+// RUN: %klee --use-batching-search --search=nurs:depth %t2.bc
+// RUN: %klee --use-batching-search --search=nurs:qc %t2.bc
+// RUN: %klee --search=random-path --search=nurs:qc %t2.bc
+// RUN: %klee --use-merge --search=dfs --debug-log-merge --debug-log-state-merge %t2.bc
+// RUN: %klee --use-merge --use-batching-search --search=dfs %t2.bc
+// RUN: %klee --use-merge --use-batching-search --search=random-state %t2.bc
+// RUN: %klee --use-merge --use-batching-search --search=nurs:depth %t2.bc
+// RUN: %klee --use-merge --use-batching-search --search=nurs:qc %t2.bc
 // RUN: %klee --use-iterative-deepening-time-search --use-batching-search %t2.bc
-// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --use-random-search %t2.bc
-// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --use-non-uniform-random-search %t2.bc
-// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --use-non-uniform-random-search --weight-type=query-cost %t2.bc
+// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --search=random-state %t2.bc
+// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --search=nurs:depth %t2.bc
+// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --search=nurs:qc %t2.bc
 
 
 /* this test is basically just for coverage and doesn't really do any
    correctness check (aside from testing that the various combinations
    don't crash) */
 
+#include <stdlib.h>
+
 int validate(char *buf, int N) {
 
   int i;
diff --git a/test/Runtime/POSIX/DirConsistency.c b/test/Runtime/POSIX/DirConsistency.c
index 30696650..24bb8a6e 100644
--- a/test/Runtime/POSIX/DirConsistency.c
+++ b/test/Runtime/POSIX/DirConsistency.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
-// RUN: %klee --run-in=/tmp --use-random-search --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t1.log
+// RUN: %klee --run-in=/tmp --search=random-state --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t1.log
 // RUN: %llvmgcc -D_FILE_OFFSET_BITS=64 %s -emit-llvm -O0 -c -o %t.bc
-// RUN: %klee --run-in=/tmp --use-random-search --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t2.log
+// RUN: %klee --run-in=/tmp --search=random-state --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t2.log
 // RUN: sort %t1.log %t2.log | uniq -c > %t3.log
 // RUN: grep -q "4 COUNT" %t3.log
 
diff --git a/test/Runtime/POSIX/FD_Fail2.c b/test/Runtime/POSIX/FD_Fail2.c
index 062f7027..b42e03bf 100644
--- a/test/Runtime/POSIX/FD_Fail2.c
+++ b/test/Runtime/POSIX/FD_Fail2.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee --libc=uclibc --posix-runtime %t1.bc --sym-files 0 0 --max-fail 1
+// RUN: %klee --libc=uclibc --posix-runtime --search=dfs %t1.bc --sym-files 1 10 --max-fail 1
 // RUN: test -f klee-last/test000001.ktest
 // RUN: test -f klee-last/test000002.ktest
 // RUN: test -f klee-last/test000003.ktest
@@ -14,21 +14,24 @@
 #include <sys/types.h>
 #include <sys/stat.h>
 #include <fcntl.h>
+#include <stdio.h>
 
 int main(int argc, char** argv) {
   char buf[1024];  
-  int fd = open("/etc/fstab", O_RDONLY);
+  int fd = open("A", O_RDONLY);
   assert(fd != -1);
-    
-  int r = read(fd, buf, 1, 100);
+
+  int r;
+
+  r = read(fd, buf, 1, 5);
   if (r != -1)
     printf("read() succeeded\n");
-  else printf("read() failed with errno %s\n", strerror(errno));
+  else printf("read() failed with error '%s'\n", strerror(errno));
 
   r = close(fd);
   if (r != -1)
     printf("close() succeeded\n");
-  else printf("close() failed with errno %s\n", strerror(errno));
+  else printf("close() failed with error '%s'\n", strerror(errno));
 
   return 0;
 }
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>