Skip to content
Browse files

added klee changes

  • Loading branch information...
1 parent 5c025d2 commit 043166b02119e10eae1e53937e2624cfbb719cf1 @martintrojer committed Nov 10, 2011
View
12 klee/configure
@@ -3068,13 +3068,15 @@ if test "$ac_test_CFLAGS" = set; then
CFLAGS=$ac_save_CFLAGS
elif test $ac_cv_prog_cc_g = yes; then
if test "$GCC" = yes; then
- CFLAGS="-g -O2"
+# CFLAGS="-g -O2"
+ CFLAGS="-g -O0"
else
CFLAGS="-g"
fi
else
if test "$GCC" = yes; then
- CFLAGS="-O2"
+# CFLAGS="-O2"
+ CFLAGS="-O0"
else
CFLAGS=
fi
@@ -4508,13 +4510,15 @@ if test "$ac_test_CXXFLAGS" = set; then
CXXFLAGS=$ac_save_CXXFLAGS
elif test $ac_cv_prog_cxx_g = yes; then
if test "$GXX" = yes; then
- CXXFLAGS="-g -O2"
+# CXXFLAGS="-g -O2"
+ CXXFLAGS="-g -O0"
else
CXXFLAGS="-g"
fi
else
if test "$GXX" = yes; then
- CXXFLAGS="-O2"
+# CXXFLAGS="-O2"
+ CXXFLAGS="-O0"
else
CXXFLAGS=
fi
View
144 klee/lib/Core/.svn/entries
@@ -1,7 +1,7 @@
10
dir
-89647
+89648
http://llvm.org/svn/llvm-project/klee/trunk/lib/Core
http://llvm.org/svn/llvm-project
@@ -32,7 +32,7 @@ file
-2009-11-23T10:48:01.304771Z
+2009-11-19T21:40:51.432050Z
0f47f2647706d70b9923d1287a9f67fc
2009-09-21T00:27:27.787449Z
82421
@@ -66,7 +66,7 @@ file
-2009-11-23T10:48:01.308772Z
+2009-11-19T21:40:51.432050Z
0479fe997c3e087e6d6b67b6438c8c24
2009-05-23T02:42:09.367612Z
72312
@@ -100,7 +100,7 @@ file
-2009-11-23T10:48:01.308772Z
+2009-11-19T21:40:51.432050Z
c8a2d91c3746249bbc9b928666d8394c
2009-05-21T04:36:41.677998Z
72205
@@ -134,7 +134,7 @@ file
-2009-11-23T10:48:01.308772Z
+2009-11-19T21:40:51.432050Z
89169bf18e653d7a52c78f4f7ec2c11f
2009-06-14T06:16:49.603007Z
73327
@@ -168,7 +168,7 @@ file
-2009-11-23T10:48:01.308772Z
+2009-11-19T21:40:51.432050Z
57c6fca60fad2d0b4b3ccfbb694da1f8
2009-05-21T04:36:41.677998Z
72205
@@ -202,7 +202,7 @@ file
-2009-11-23T10:48:01.308772Z
+2009-11-19T21:40:51.432050Z
789b6717b7cd0accd57620ff1b44d365
2009-05-21T04:36:41.677998Z
72205
@@ -236,7 +236,7 @@ file
-2009-11-23T10:48:01.308772Z
+2009-11-19T21:40:51.432050Z
a7cf86d19a898053fdb9fa55d7c33f1a
2009-07-28T07:59:09.938596Z
77306
@@ -270,7 +270,7 @@ file
-2009-11-23T10:48:01.308772Z
+2009-11-19T21:40:51.432050Z
9643ab4eef89b51f40981942f956eaa1
2009-05-21T04:36:41.677998Z
72205
@@ -304,7 +304,7 @@ file
-2009-11-23T10:48:01.308772Z
+2009-11-19T21:40:51.432050Z
560e6ecccf1114728d6ef08cb67a03c9
2009-09-01T06:53:41.550738Z
80665
@@ -338,7 +338,7 @@ file
-2009-11-23T10:48:01.308772Z
+2009-11-19T21:40:51.432050Z
dbba1825a667670b657ad06526eff096
2009-07-25T05:17:51.505453Z
77049
@@ -372,7 +372,7 @@ file
-2009-11-23T10:48:01.312771Z
+2009-11-19T21:40:51.436050Z
445d13bb9d5428c1aa2df58d12a29564
2009-05-21T04:36:41.677998Z
72205
@@ -406,7 +406,7 @@ file
-2009-11-23T10:48:01.312771Z
+2009-11-19T21:40:51.436050Z
96fa12865cc4fe2e8c10b69414001422
2009-06-04T08:59:53.873673Z
72862
@@ -440,7 +440,7 @@ file
-2009-11-23T10:48:01.312771Z
+2009-11-19T21:40:51.436050Z
0925966f0200783513fb21011471bf9f
2009-06-04T08:42:34.267250Z
72860
@@ -474,7 +474,7 @@ file
-2009-11-23T10:48:01.312771Z
+2009-11-19T21:40:51.436050Z
a277286b0b3b9330201c9428e57e905d
2009-07-28T07:59:09.938596Z
77306
@@ -508,7 +508,7 @@ file
-2009-11-23T10:48:01.312771Z
+2009-11-19T21:40:51.436050Z
c48497a6fa43660eea3b5b5a9d0e1b77
2009-06-01T16:34:44.045382Z
72693
@@ -536,16 +536,16 @@ ddunbar
3148
-ExecutorUtil.cpp
+SeedInfo.cpp
file
-2009-11-23T10:48:01.312771Z
-787e0af675fc8d08cc0ec2041cbb946f
-2009-09-01T06:53:41.550738Z
-80665
+2009-11-19T21:40:51.436050Z
+b6dddcbcb61e615ac55ea532055c6659
+2009-06-14T06:52:04.829644Z
+73328
ddunbar
@@ -568,20 +568,19 @@ ddunbar
-5131
+6061
-Makefile
+Searcher.cpp
file
-2009-11-23T10:48:01.312771Z
-689ff889985c03c2d4c621ea95d56a96
-2009-05-21T04:36:41.677998Z
-72205
+2009-11-19T21:40:51.436050Z
+9bf7bdd108bd84b52726fa62f0fe794c
+2009-09-01T06:53:41.550738Z
+80665
ddunbar
-has-props
@@ -602,19 +601,21 @@ has-props
-443
+
+16471
-Searcher.cpp
+Makefile
file
-2009-11-23T10:48:01.312771Z
-9bf7bdd108bd84b52726fa62f0fe794c
-2009-09-01T06:53:41.550738Z
-80665
+2009-11-19T21:40:51.436050Z
+689ff889985c03c2d4c621ea95d56a96
+2009-05-21T04:36:41.677998Z
+72205
ddunbar
+has-props
@@ -635,19 +636,18 @@ ddunbar
-
-16471
+443
-SeedInfo.cpp
+ExecutorUtil.cpp
file
-2009-11-23T10:48:01.312771Z
-b6dddcbcb61e615ac55ea532055c6659
-2009-06-14T06:52:04.829644Z
-73328
+2009-11-19T21:40:51.436050Z
+787e0af675fc8d08cc0ec2041cbb946f
+2009-09-01T06:53:41.550738Z
+80665
ddunbar
@@ -670,15 +670,15 @@ ddunbar
-6061
+5131
Common.h
file
-2009-11-23T10:48:01.316769Z
+2009-11-19T21:40:51.436050Z
d9d708c4e4b92d87baa53323d6fb647d
2009-05-21T04:36:41.677998Z
72205
@@ -712,7 +712,7 @@ file
-2009-11-23T10:48:01.320772Z
+2009-11-19T21:40:51.436050Z
6d88f6346f8181de122d15e281b98704
2009-07-12T20:42:31.043500Z
75427
@@ -746,7 +746,7 @@ file
-2009-11-23T10:48:01.320772Z
+2009-11-19T21:40:51.436050Z
cac7ad413472c37722206b9eae3cfccf
2009-05-21T04:36:41.677998Z
72205
@@ -780,7 +780,7 @@ file
-2009-11-23T10:48:01.320772Z
+2009-11-19T21:40:51.436050Z
f69e4f6bfc84ba80c9a4dbf1d4d018d8
2009-06-14T08:16:07.335356Z
73337
@@ -808,16 +808,16 @@ ddunbar
9928
-Executor.h
+MemoryManager.cpp
file
-2009-11-23T10:48:01.320772Z
-1e0e9c65c1eb4a59465245e644a48ae2
-2009-07-25T05:17:51.505453Z
-77049
+2009-11-19T21:40:51.436050Z
+43e624dd00fd65c6436f42d89de68a01
+2009-06-14T06:16:49.603007Z
+73327
ddunbar
@@ -840,18 +840,18 @@ ddunbar
-16530
+2040
-MemoryManager.cpp
+Executor.h
file
-2009-11-23T10:48:01.320772Z
-43e624dd00fd65c6436f42d89de68a01
-2009-06-14T06:16:49.603007Z
-73327
+2009-11-19T21:40:51.436050Z
+1e0e9c65c1eb4a59465245e644a48ae2
+2009-07-25T05:17:51.505453Z
+77049
ddunbar
@@ -874,15 +874,15 @@ ddunbar
-2040
+16530
ExecutionState.cpp
file
-2009-11-23T10:48:01.320772Z
+2009-11-19T21:40:51.436050Z
fe6bcd72e640db15ff2f35253db8e20c
2009-09-01T06:53:41.550738Z
80665
@@ -916,7 +916,7 @@ file
-2009-11-23T10:48:01.320772Z
+2009-11-19T21:40:51.436050Z
825b9e1e4dd71b0904f0706f24e01f1f
2009-09-01T06:53:41.550738Z
80665
@@ -950,7 +950,7 @@ file
-2009-11-23T10:48:01.320772Z
+2009-11-19T21:40:51.436050Z
5b371064004cbcd028e98e026ca04d86
2009-05-21T04:36:41.677998Z
72205
@@ -984,7 +984,7 @@ file
-2009-11-23T10:48:01.320772Z
+2009-11-19T21:40:51.436050Z
37c5f126fc15f79a564f6dba2e2ca2b1
2009-07-25T05:17:51.505453Z
77049
@@ -1018,7 +1018,7 @@ file
-2009-11-23T10:48:01.324770Z
+2009-11-19T21:40:51.440050Z
5360a784031c9a48901466df9d70d5f9
2009-05-21T04:36:41.677998Z
72205
@@ -1052,7 +1052,7 @@ file
-2009-11-23T10:48:01.324770Z
+2009-11-19T21:40:51.440050Z
7d02ecd50331bd2251f5592ff63e63ca
2009-05-21T04:36:41.677998Z
72205
@@ -1086,7 +1086,7 @@ file
-2009-11-23T10:48:01.324770Z
+2009-11-19T21:40:51.440050Z
10315fd7e3024ae20fc29191504788da
2009-09-01T06:53:41.550738Z
80665
@@ -1120,7 +1120,7 @@ file
-2009-11-23T10:48:01.324770Z
+2009-11-19T21:40:51.440050Z
98a5fc1342097a66b6143b5ce8211b48
2009-07-10T04:15:25.623403Z
75224
@@ -1154,7 +1154,7 @@ file
-2009-11-23T10:48:01.324770Z
+2009-11-19T21:40:51.440050Z
155a2178c8a834a348102c3b5b190817
2009-09-01T06:53:41.550738Z
80665
@@ -1188,7 +1188,7 @@ file
-2009-11-23T10:48:01.324770Z
+2009-11-19T21:40:51.440050Z
cd94d39c80eab163783913741c5c1c5d
2009-07-28T07:59:09.938596Z
77306
@@ -1222,7 +1222,7 @@ file
-2009-11-23T10:48:01.324770Z
+2009-11-19T21:40:51.440050Z
7e5c8f3a62f018cb8e4642d45e6e9c86
2009-05-21T04:36:41.677998Z
72205
@@ -1256,7 +1256,7 @@ file
-2009-11-23T10:48:01.324770Z
+2009-11-19T21:40:51.440050Z
cf722c4bb4076f728b36997c097fb902
2009-07-28T08:58:29.900933Z
77312
@@ -1290,7 +1290,7 @@ file
-2009-11-23T10:48:01.324770Z
+2009-11-19T21:40:51.440050Z
0b242ee8daffac34cfcee4a6019cc29b
2009-09-01T06:53:41.550738Z
80665
@@ -1324,7 +1324,7 @@ file
-2009-11-23T10:48:01.328769Z
+2009-11-19T21:40:51.440050Z
0a2d5879c85d609271dd19f902b9b43a
2009-05-21T04:36:41.677998Z
72205
View
7 klee/lib/Core/AddressSpace.cpp
@@ -118,7 +118,7 @@ bool AddressSpace::resolveOne(ExecutionState &state,
return true;
} else {
bool mustBeTrue;
- if (!solver->mustBeTrue(state,
+ if (!solver->mustBeTrue(state, // Unsigned Greater or Equal
UgeExpr::create(address, mo->getBaseExpr()),
mustBeTrue))
return false;
@@ -132,7 +132,7 @@ bool AddressSpace::resolveOne(ExecutionState &state,
const MemoryObject *mo = oi->first;
bool mustBeTrue;
- if (!solver->mustBeTrue(state,
+ if (!solver->mustBeTrue(state, // Unsigned less than
UltExpr::create(address, mo->getBaseExpr()),
mustBeTrue))
return false;
@@ -141,7 +141,7 @@ bool AddressSpace::resolveOne(ExecutionState &state,
} else {
bool mayBeTrue;
- if (!solver->mayBeTrue(state,
+ if (!solver->mayBeTrue(state, // Maybe in bounds?
mo->getBoundsCheckPointer(address),
mayBeTrue))
return false;
@@ -194,6 +194,7 @@ bool AddressSpace::resolve(ExecutionState &state,
uint64_t example = cex->getZExtValue();
MemoryObject hack(example);
+ // int osize = objects.size();
MemoryMap::iterator oi = objects.upper_bound(&hack);
MemoryMap::iterator begin = objects.begin();
MemoryMap::iterator end = objects.end();
View
4 klee/lib/Core/Executor.cpp
@@ -2338,6 +2338,9 @@ void Executor::run(ExecutionState &initialState) {
while (!states.empty() && !haltExecution) {
ExecutionState &state = searcher->selectState();
KInstruction *ki = state.pc;
+ // Instruction *i = state.pc->inst;
+ // Function *f = i->getParent()->getParent();
+ // std::cerr << "[" << states.size() << "] " << f->getNameStr() << "() " << i->getOpcodeName() << "\n";
stepInstruction(state);
executeInstruction(state, ki);
@@ -2946,6 +2949,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
// XXX there is some query wasteage here. who cares?
ExecutionState *unbound = &state;
+ // int rl_size = rl.size();
for (ResolutionList::iterator i = rl.begin(), ie = rl.end(); i != ie; ++i) {
const MemoryObject *mo = i->first;
const ObjectState *os = i->second;
View
1 klee/lib/Core/Executor.h
@@ -78,6 +78,7 @@ class Executor : public Interpreter {
friend class WeightedRandomSearcher;
friend class SpecialFunctionHandler;
friend class StatsTracker;
+ friend class GuidedSearcher;
public:
class Timer {
View
2 klee/lib/Core/ExternalDispatcher.cpp
@@ -7,6 +7,8 @@
//
//===----------------------------------------------------------------------===//
+#include <stdint.h>
+
#include "ExternalDispatcher.h"
#include "llvm/Module.h"
View
212 klee/lib/Core/Searcher.cpp
@@ -33,6 +33,10 @@
#include "llvm/Support/CFG.h"
#include "llvm/Support/CommandLine.h"
+#include "llvm/PassManager.h"
+#include "llvm/Analysis/CallGraphCFG.h"
+#include "llvm/Analysis/CallPaths.h"
+
#include <cassert>
#include <fstream>
#include <climits>
@@ -52,6 +56,214 @@ namespace klee {
Searcher::~Searcher() {
}
+/// ------------------------------------------------------------------------
+
+#if 0
+namespace boost {
+ void throw_exception( std::exception const & e )
+ {
+ }
+}
+#endif
+
+GuidedSearcher::GuidedSearcher(Executor &_executor, std::string defectFile)
+ : executor(_executor), miss_ctr(0)
+{
+ // Build the path list
+
+ Module *M = executor.kmodule->module;
+ PassManager Passes;
+ // Pass *P = createCallGraphCFGPass(&paths, defectFile);
+ Pass *P = createCallPathsPass(&paths, defectFile);
+ Passes.add(P);
+ Passes.run(*M);
+
+ std::cerr << "GuidededSearcher:: Here's my path(s):\n";
+
+ for(std::vector<pathType>::iterator pit=paths.begin(); pit != paths.end(); ++pit) {
+ pathType path = *pit;
+
+ if (path.empty())
+ continue;
+
+ for (pathType::iterator it=path.begin(); it != path.end(); ++it) {
+ BasicBlock *bb = *it;
+ std::cerr << "[ " << bb->getNameStr() << " {" << bb->getParent()->getNameStr() << "} [" << bb << "] - ";
+ }
+ std::cerr << "\n";
+
+ // Build the instMap
+ // FIX: If many paths shre the leaf BB instMap (which will be very common)
+ // we need to either 1/ Update all paths instMap when a leaf is hit or
+ // 2/ terminate all paths with shared leafs when one paths instMap is completed
+ std::map<llvm::Instruction*, bool> instMap;
+
+ BasicBlock *BB = path.back();
+ for (BasicBlock::iterator bbit = BB->begin(); bbit != BB->end(); ++bbit) {
+ Instruction *I = bbit;
+ if (I->getOpcode() != Instruction::Br)
+ instMap[I] = false;
+ }
+ std::cerr << instMap.size() << " instructions in leaf BB\n";
+ instMaps.push_back(instMap);
+ }
+}
+
+bool GuidedSearcher::done(int index)
+{
+ std::map<llvm::Instruction*, bool> *instMap = &instMaps[index];
+ if (instMap == NULL)
+ return true;
+ if (instMap->empty())
+ return true;
+
+ for(std::map<llvm::Instruction*, bool>::iterator it = instMap->begin(); it != instMap->end(); ++it)
+ if (!it->second)
+ return false;
+ return true;
+}
+
+bool GuidedSearcher::allDone(void)
+{
+ int ctr=0;
+ for(std::vector<pathType>::iterator pit=paths.begin(); pit != paths.end(); ++pit, ctr++) {
+ if (!done(ctr))
+ return false;
+ }
+ return true;
+}
+
+
+int GuidedSearcher::left(int index)
+{
+ std::map<llvm::Instruction*, bool> *instMap = &instMaps[index];
+
+ int ctr = 0;
+ for(std::map<llvm::Instruction*, bool>::iterator it = instMap->begin(); it != instMap->end(); ++it)
+ if (!it->second)
+ ctr++;
+ return ctr;
+}
+
+void GuidedSearcher::killAllStates(void)
+{
+ for (std::vector<ExecutionState*>::iterator it = states.begin(); it != states.end(); ++it) {
+ executor.terminateStateEarly(**it, "GuidedSearcher -- Path reached");
+ }
+ empty();
+}
+
+ExecutionState &GuidedSearcher::selectState()
+{
+ if (paths.size()==0) {
+ std::cerr << "GuidedSearcher: Error, no paths! Terminating all states\n";
+ killAllStates();
+ }
+
+ // std::cerr << "selectState: processing " << states.size() << " state(s)\n";
+
+ for (std::vector<ExecutionState*>::iterator it = states.begin(); it != states.end(); ++it) {
+ ExecutionState *state = *it;
+ Instruction *state_i = state->pc->inst;
+ BasicBlock *state_bb = state_i->getParent();
+
+ // Loop over all paths...
+ // States can go in and out of different paths, we can't really control that,
+ // so we keep picking states in paths that are not done yet.
+ // .. and when a state executes the last instruction in a BB leaf, we terminate that state
+ // (in order to generate the test case)
+ // ... and when all paths are complete, we stop all together.
+
+ int ctr=0; // for index into instMaps
+ for(std::vector<pathType>::iterator pit=paths.begin(); pit != paths.end(); ++pit, ctr++) {
+ pathType path = *pit;
+
+ // Are we done with this path?
+ if (done(ctr))
+ continue;
+
+ // The idea here is to pick a state that has it's PC in a BB that's in the path.
+ // Preferrably as close to the leaf BB as possible, thus
+ // we travese the path in reverse order and return first match.
+
+ for (pathType::reverse_iterator bbit = path.rbegin(); bbit != path.rend(); ++bbit) {
+ BasicBlock *BB = *bbit;
+#if 0
+ std::cerr << " trying s[" << state << "] " << " p[" << ctr << "] " << BB << " "
+ << BB->getParent()->getNameStr() << " >state: "
+ << "{" << state_bb << " " << state_bb->getParent()->getNameStr() << "}\n";
+#endif
+ // is the state_bb in our path?
+ if (state_bb == BB) {
+ instMaps[ctr][state_i] = true;
+ // Are we done? Terminate this state and write out info
+ // FIX: Doesn't this mean that we wont run the last instruction in the BB?
+ if (done(ctr)) {
+ executor.terminateStateOnError(*state, "BB completed", "guidedsearcher");
+ continue;
+ }
+ if (miss_ctr != 0) {
+ std::cerr << miss_ctr << " path misses [" << states.size() << " state(s)]\n";
+ miss_ctr=0;
+ }
+ if (bbit == path.rbegin())
+ std::cerr << "! new hit in leaf [p: " << ctr << " (" << left(ctr) << ")]\n";
+ else
+ std::cerr << "* hit " << state->pc->inst->getParent()->getParent()->getNameStr()
+ << " [p: " << ctr << " (" << left(ctr) << ")]\n";
+ return *state;
+ }
+ }
+ }
+
+ if (allDone()) {
+ std::cerr << "GuidedSearcher done -- terminating remaining states\n";
+ killAllStates();
+ }
+ }
+ // std::cerr << "- found no match\n";
+ miss_ctr++;
+ if ((miss_ctr%1000) == 0)
+ std::cerr << miss_ctr << " path misses [" << states.size() << " state(s)]...\n";
+ return *states[theRNG.getInt32()%states.size()]; // pick a random state (this will help with fork bombing)
+}
+
+void GuidedSearcher::update(ExecutionState *current,
+ const std::set<ExecutionState*> &addedStates,
+ const std::set<ExecutionState*> &removedStates) {
+
+ if (addedStates.size()==0 && removedStates.size()==0)
+ return;
+
+ std::cerr << "Adding " << addedStates.size() << " & removing " << removedStates.size() << " state(s)\n";
+
+ states.insert(states.end(),
+ addedStates.begin(),
+ addedStates.end());
+ for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
+ ie = removedStates.end(); it != ie; ++it) {
+ ExecutionState *es = *it;
+ if (es == states.back()) {
+ states.pop_back();
+ } else {
+ bool ok = false;
+
+ for (std::vector<ExecutionState*>::iterator it = states.begin(),
+ ie = states.end(); it != ie; ++it) {
+ if (es==*it) {
+ states.erase(it);
+ ok = true;
+ break;
+ }
+ }
+
+ assert(ok && "invalid state removed");
+ }
+ }
+}
+
+/// ------------------------------------------------------------------------
+
///
ExecutionState &DFSSearcher::selectState() {
View
36 klee/lib/Core/Searcher.h
@@ -15,6 +15,10 @@
#include <map>
#include <queue>
+#include "llvm/Function.h"
+#include "llvm/BasicBlock.h"
+#include "Executor.h"
+
// FIXME: Move out of header, use llvm streams.
#include <ostream>
@@ -68,6 +72,38 @@ namespace klee {
}
};
+ /// ------------------------------------------------------------------------
+
+ class GuidedSearcher : public Searcher {
+ public:
+ typedef std::vector<llvm::BasicBlock*> pathType;
+
+ private:
+ std::vector<ExecutionState*> states;
+ std::vector<pathType> paths;
+ std::vector<std::map<llvm::Instruction*, bool> > instMaps;
+ Executor &executor;
+ int miss_ctr;
+
+ bool allDone(void);
+ bool done(int index);
+ int left(int index);
+ void killAllStates(void);
+
+ public:
+ GuidedSearcher(Executor &_executor, std::string defectFile);
+ ExecutionState &selectState();
+ void update(ExecutionState *current,
+ const std::set<ExecutionState*> &addedStates,
+ const std::set<ExecutionState*> &removedStates);
+ bool empty() { return states.empty(); }
+ void printName(std::ostream &os) {
+ os << "GuidedSearcher\n";
+ }
+ };
+
+ /// ------------------------------------------------------------------------
+
class DFSSearcher : public Searcher {
std::vector<ExecutionState*> states;
View
5 klee/lib/Core/UserSearcher.cpp
@@ -20,6 +20,9 @@ using namespace llvm;
using namespace klee;
namespace {
+ cl::opt<std::string>
+ UseGuidedSearch("use-guided-search", cl::desc("Specity input XML defect file"));
+
cl::opt<bool>
UseRandomSearch("use-random-search");
@@ -111,6 +114,8 @@ Searcher *klee::constructUserSearcher(Executor &executor) {
searcher = new WeightedRandomSearcher(executor, WeightType);
} else if (UseRandomSearch) {
searcher = new RandomSearcher();
+ } else if (UseGuidedSearch!="") {
+ searcher = new GuidedSearcher(executor, UseGuidedSearch);
} else {
searcher = new DFSSearcher();
}
View
2 klee/stp/AST/AST.cpp
@@ -7,6 +7,8 @@
********************************************************************/
// -*- c++ -*-
+#include <stdint.h>
+
#include "AST.h"
namespace BEEV {
//some global variables that are set through commandline options. it
View
118 klee/stp/AST/ASTKind.cpp
@@ -0,0 +1,118 @@
+// Generated automatically by genkinds.h from ASTKind.kinds Mon Nov 23 16:32:25 2009.
+// Do not edit
+namespace BEEV {
+const char * _kind_names[] = {
+ "UNDEFINED",
+ "SYMBOL",
+ "BVCONST",
+ "BVNEG",
+ "BVCONCAT",
+ "BVOR",
+ "BVAND",
+ "BVXOR",
+ "BVNAND",
+ "BVNOR",
+ "BVXNOR",
+ "BVEXTRACT",
+ "BVLEFTSHIFT",
+ "BVRIGHTSHIFT",
+ "BVSRSHIFT",
+ "BVVARSHIFT",
+ "BVPLUS",
+ "BVSUB",
+ "BVUMINUS",
+ "BVMULTINVERSE",
+ "BVMULT",
+ "BVDIV",
+ "BVMOD",
+ "SBVDIV",
+ "SBVMOD",
+ "BVSX",
+ "BOOLVEC",
+ "ITE",
+ "BVGETBIT",
+ "BVLT",
+ "BVLE",
+ "BVGT",
+ "BVGE",
+ "BVSLT",
+ "BVSLE",
+ "BVSGT",
+ "BVSGE",
+ "EQ",
+ "NEQ",
+ "FALSE",
+ "TRUE",
+ "NOT",
+ "AND",
+ "OR",
+ "NAND",
+ "NOR",
+ "XOR",
+ "IFF",
+ "IMPLIES",
+ "READ",
+ "WRITE",
+ "ARRAY",
+ "BITVECTOR",
+ "BOOLEAN",
+};
+
+unsigned char _kind_categories[] = {
+ 0,
+ 3,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 1,
+ 3,
+ 2,
+ 2,
+ 2,
+ 2,
+ 2,
+ 2,
+ 2,
+ 2,
+ 2,
+ 2,
+ 2,
+ 2,
+ 2,
+ 2,
+ 2,
+ 2,
+ 2,
+ 2,
+ 2,
+ 2,
+ 2,
+ 1,
+ 1,
+ 0,
+ 0,
+ 0,
+};
+
+}; // end namespace
View
79 klee/stp/AST/ASTKind.h
@@ -0,0 +1,79 @@
+// -*- c++ -*-
+#ifndef TESTKINDS_H
+#define TESTKINDS_H
+// Generated automatically by genkinds.pl from ASTKind.kinds Mon Nov 23 16:32:25 2009.
+// Do not edit
+namespace BEEV {
+ typedef enum {
+ UNDEFINED,
+ SYMBOL,
+ BVCONST,
+ BVNEG,
+ BVCONCAT,
+ BVOR,
+ BVAND,
+ BVXOR,
+ BVNAND,
+ BVNOR,
+ BVXNOR,
+ BVEXTRACT,
+ BVLEFTSHIFT,
+ BVRIGHTSHIFT,
+ BVSRSHIFT,
+ BVVARSHIFT,
+ BVPLUS,
+ BVSUB,
+ BVUMINUS,
+ BVMULTINVERSE,
+ BVMULT,
+ BVDIV,
+ BVMOD,
+ SBVDIV,
+ SBVMOD,
+ BVSX,
+ BOOLVEC,
+ ITE,
+ BVGETBIT,
+ BVLT,
+ BVLE,
+ BVGT,
+ BVGE,
+ BVSLT,
+ BVSLE,
+ BVSGT,
+ BVSGE,
+ EQ,
+ NEQ,
+ FALSE,
+ TRUE,
+ NOT,
+ AND,
+ OR,
+ NAND,
+ NOR,
+ XOR,
+ IFF,
+ IMPLIES,
+ READ,
+ WRITE,
+ ARRAY,
+ BITVECTOR,
+ BOOLEAN,
+} Kind;
+
+extern unsigned char _kind_categories[];
+
+inline bool is_Term_kind(Kind k) { return (_kind_categories[k] & 1); }
+
+inline bool is_Form_kind(Kind k) { return (_kind_categories[k] & 2); }
+
+extern const char *_kind_names[];
+
+/** Prints symbolic name of kind */
+inline ostream& operator<<(ostream &os, const Kind &kind) { os << _kind_names[kind]; return os; }
+
+
+}; // end namespace
+
+
+#endif
View
2 klee/tools/klee/Makefile
@@ -18,5 +18,5 @@ ifeq ($(ENABLE_STPLOG), 1)
LIBS += -lstplog
endif
-LIBS += -lstp
+LIBS += -lstp -lxml2
#-ltcmalloc

0 comments on commit 043166b

Please sign in to comment.
Something went wrong with that request. Please try again.