28#include "llvm/IR/Constants.h"
29#include "llvm/IR/Instructions.h"
30#include "llvm/IR/Module.h"
31#include "llvm/Support/CommandLine.h"
47 const std::vector<ExecutionState *> &addedStates,
48 const std::vector<ExecutionState *> &removedStates) {
50 states.insert(
states.end(), addedStates.begin(), addedStates.end());
53 for (
const auto state : removedStates) {
54 if (state ==
states.back()) {
57 auto it = std::find(
states.begin(),
states.end(), state);
58 assert(it !=
states.end() &&
"invalid state removed");
69 os <<
"DFSSearcher\n";
80 const std::vector<ExecutionState *> &addedStates,
81 const std::vector<ExecutionState *> &removedStates) {
85 if (!addedStates.empty() && current &&
86 std::find(removedStates.begin(), removedStates.end(), current) == removedStates.end()) {
87 auto pos = std::find(
states.begin(),
states.end(), current);
88 assert(pos !=
states.end());
94 states.insert(
states.end(), addedStates.begin(), addedStates.end());
97 for (
const auto state : removedStates) {
98 if (state ==
states.front()) {
101 auto it = std::find(
states.begin(),
states.end(), state);
102 assert(it !=
states.end() &&
"invalid state removed");
113 os <<
"BFSSearcher\n";
126 const std::vector<ExecutionState *> &addedStates,
127 const std::vector<ExecutionState *> &removedStates) {
129 states.insert(
states.end(), addedStates.begin(), addedStates.end());
132 for (
const auto state : removedStates) {
133 auto it = std::find(
states.begin(),
states.end(), state);
134 assert(it !=
states.end() &&
"invalid state removed");
144 os <<
"RandomSearcher\n";
168 assert(0 &&
"invalid weight type");
182 return std::pow(0.5, es->
depth);
186 double inv = 1. / std::max((uint64_t) 1, count);
192 double inv = 1. / std::max((uint64_t) 1, count);
202 es->
stack.back().minDistToUncoveredOnReturn);
204 double invMD2U = 1. / (md2u ? md2u : 10000);
206 double invCovNew = 0.;
209 return (invCovNew * invCovNew + invMD2U * invMD2U);
211 return invMD2U * invMD2U;
218 const std::vector<ExecutionState *> &addedStates,
219 const std::vector<ExecutionState *> &removedStates) {
223 std::find(removedStates.begin(), removedStates.end(), current) == removedStates.end())
227 for (
const auto state : addedStates)
231 for (
const auto state : removedStates)
240 os <<
"WeightedRandomSearcher::";
242 case Depth : os <<
"Depth\n";
return;
243 case RP : os <<
"RandomPath\n";
return;
244 case QueryCost : os <<
"QueryCost\n";
return;
245 case InstCount : os <<
"InstCount\n";
return;
249 default : os <<
"<unknown type>\n";
return;
257#define IS_OUR_NODE_VALID(n) \
258 (((n).getPointer() != nullptr) && (((n).getInt() & idBitMask) != 0))
261 : processTree{processTree},
263 idBitMask{processTree.getNextId()} {};
266 unsigned flips=0, bits=0;
272 assert(n != n->
right.getPointer());
273 n = n->
right.getPointer();
276 assert(n != n->
left.getPointer());
277 n = n->
left.getPointer();
284 n = ((flips & (1U << bits)) ? n->
left : n->
right).getPointer();
292 const std::vector<ExecutionState *> &addedStates,
293 const std::vector<ExecutionState *> &removedStates) {
295 for (
auto es : addedStates) {
299 childPtr = parent ? ((parent->left.getPointer() == pnode) ? &parent->left
303 childPtr->setInt(childPtr->getInt() |
idBitMask);
309 ? ((parent->left.getPointer() == pnode) ? &parent->left
316 for (
auto es : removedStates) {
322 parent ? ((parent->left.getPointer() == pnode) ? &parent->left
326 childPtr->setInt(childPtr->getInt() & ~
idBitMask);
339 os <<
"RandomPathSearcher\n";
346 : baseSearcher{baseSearcher} {};
362 assert(!
baseSearcher->empty() &&
"base searcher is empty");
370 if (!cur_mergehandler->hasMergedStates()) {
379 llvm::errs() <<
"Preemptively releasing states\n";
383 cur_mergehandler->releaseStates();
391 const std::vector<ExecutionState *> &addedStates,
392 const std::vector<ExecutionState *> &removedStates) {
396 baseSearcher->update(current, addedStates, removedStates);
405 os <<
"MergingSearcher\n";
412 : baseSearcher{baseSearcher},
413 timeBudget{timeBudget},
414 instructionBudget{instructionBudget} {};
441 const std::vector<ExecutionState *> &addedStates,
442 const std::vector<ExecutionState *> &removedStates) {
444 if (std::find(removedStates.begin(), removedStates.end(),
lastState) != removedStates.end())
447 baseSearcher->update(current, addedStates, removedStates);
455 os <<
"<BatchingSearcher> timeBudget: " <<
timeBudget
457 <<
", baseSearcher:\n";
459 os <<
"</BatchingSearcher>\n";
466 : baseSearcher{baseSearcher} {};
475 const std::vector<ExecutionState *> &addedStates,
476 const std::vector<ExecutionState *> &removedStates) {
481 if (!removedStates.empty()) {
482 std::vector<ExecutionState *> alt = removedStates;
483 for (
const auto state : removedStates) {
487 alt.erase(std::remove(alt.begin(), alt.end(), state), alt.end());
492 baseSearcher->update(current, addedStates, removedStates);
497 std::find(removedStates.begin(), removedStates.end(), current) == removedStates.end() &&
508 baseSearcher->update(
nullptr, ps, std::vector<ExecutionState *>());
518 os <<
"IterativeDeepeningTimeSearcher\n";
526 for (
auto searcher : _searchers)
537 const std::vector<ExecutionState *> &addedStates,
538 const std::vector<ExecutionState *> &removedStates) {
542 searcher->update(current, addedStates, removedStates);
550 os <<
"<InterleavedSearcher> containing " <<
searchers.size() <<
" searchers:\n";
552 searcher->printName(os);
553 os <<
"</InterleavedSearcher>\n";
Implementation of the region based merging.
#define IS_OUR_NODE_VALID(n)
std::deque< ExecutionState * > states
void printName(llvm::raw_ostream &os) override
Prints name of searcher as a klee_message().
ExecutionState & selectState() override
void update(ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override
ExecutionState & selectState() override
std::unique_ptr< Searcher > baseSearcher
unsigned lastStartInstructions
BatchingSearcher(Searcher *baseSearcher, time::Span timeBudget, unsigned instructionBudget)
ExecutionState * lastState
void update(ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override
unsigned instructionBudget
void printName(llvm::raw_ostream &os) override
Prints name of searcher as a klee_message().
time::Point lastStartTime
StatisticRecord statistics
std::vector< ExecutionState * > states
void printName(llvm::raw_ostream &os) override
Prints name of searcher as a klee_message().
void update(ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override
ExecutionState representing a path under exploration.
stack_ty stack
Stack representing the current instruction stream.
SolverQueryMetaData queryMetaData
Statistics and information.
std::uint32_t depth
Exploration depth, i.e., number of times KLEE branched for this state.
std::uint32_t instsSinceCovNew
Counts how many instructions were executed since the last new instruction was covered.
KInstIterator pc
Pointer to instruction to be executed after the current instruction.
ExecutionState & selectState() override
std::vector< std::unique_ptr< Searcher > > searchers
void printName(llvm::raw_ostream &os) override
Prints name of searcher as a klee_message().
InterleavedSearcher(const std::vector< Searcher * > &searchers)
void update(ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override
std::unique_ptr< Searcher > baseSearcher
void printName(llvm::raw_ostream &os) override
Prints name of searcher as a klee_message().
std::set< ExecutionState * > pausedStates
ExecutionState & selectState() override
IterativeDeepeningTimeSearcher(Searcher *baseSearcher)
void update(ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override
void update(ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override
std::unique_ptr< Searcher > baseSearcher
ExecutionState & selectState() override
void printName(llvm::raw_ostream &os) override
Prints name of searcher as a klee_message().
MergingSearcher(Searcher *baseSearcher)
std::vector< MergeHandler * > mergeGroups
void continueState(ExecutionState &state)
Continue a paused state.
std::vector< ExecutionState * > pausedStates
States that have been paused by the 'pauseState' function.
void pauseState(ExecutionState &state)
ExecutionState & selectState() override
RandomPathSearcher(PTree &processTree, RNG &rng)
void printName(llvm::raw_ostream &os) override
Prints name of searcher as a klee_message().
void update(ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override
void update(ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override
void printName(llvm::raw_ostream &os) override
Prints name of searcher as a klee_message().
std::vector< ExecutionState * > states
ExecutionState & selectState() override
virtual ExecutionState & selectState()=0
uint64_t getIndexedValue(const Statistic &s, unsigned index) const
uint64_t getValue(const Statistic &s) const
void update(ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override
ExecutionState & selectState() override
WeightedRandomSearcher(WeightType type, RNG &rng)
void printName(llvm::raw_ostream &os) override
Prints name of searcher as a klee_message().
std::unique_ptr< DiscretePDF< ExecutionState *, ExecutionStateIDCompare > > states
double getWeight(ExecutionState *)
Point getWallTime()
Returns point in time using a monotonic steady clock.
uint64_t computeMinDistToUncovered(const KInstruction *ki, uint64_t minDistAtRA)
llvm::PointerIntPair< PTreeNode *, PtrBitCount, uint8_t > PTreeNodePtr
llvm::cl::opt< bool > DebugLogIncompleteMerge
void klee_message(const char *msg,...) __attribute__((format(printf
llvm::cl::opt< bool > UseIncompleteMerge
StatisticManager * theStatisticManager
unsigned id
The instruction id.
const InstructionInfo * info
CallPathNode * callPathNode