Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[test] #3

Open
wants to merge 120 commits into
base: main
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
120 commits
Select commit Hold shift + click to select a range
457911c
[fix] Tests for states with mocks
Columpio Oct 2, 2023
743cfec
Memory optimize, remove InstructionInfoTable, add immutable list for …
ladisgin Aug 15, 2023
35aad70
[feat] uint128
Columpio Oct 4, 2023
23039dc
[chore] Optimized KBlock mem
Columpio Oct 5, 2023
3c02329
[fix] Error testcase processing doesn't affect `coveredNew`
misonijnik Oct 5, 2023
a7e217d
[fix] Fix `computeValidity` in partial response case
misonijnik Oct 5, 2023
a967ee0
[chore] Disable test
misonijnik Oct 5, 2023
9502385
[chore] Add a test
misonijnik Oct 5, 2023
10d87a6
[chore] Add an option to disable loop deletion pass
misonijnik Oct 5, 2023
9247847
[fix] Fix stats
misonijnik Oct 5, 2023
6871b04
[feat] Differentiate `isCoveredNew` and `isCoveredNewError`
misonijnik Oct 6, 2023
8bad08f
[chore] Z3 is not required in a lot of tests, so remove the requirements
misonijnik Oct 6, 2023
bef97af
[feat] Improved Iterative Deepening Searcher
Columpio Oct 10, 2023
87ff7c0
[fix] Fixed inner types for unnamed structs.
S1eGa Oct 12, 2023
04fb6b5
[feat] Separate branch and block coverage
misonijnik Sep 22, 2023
e939f09
[chore] Update build.sh
misonijnik Oct 16, 2023
aede6e4
[feat] Prefer a smaller integer vaule in a model
misonijnik Oct 16, 2023
59fdf83
[chore] Optimized IterativeDeepeningSearcher
Columpio Oct 20, 2023
a8d246a
[chore] Optimized getDistance
Columpio Oct 20, 2023
5aa5eb8
[chore] Strip llvm.dbg.declare
Columpio Oct 20, 2023
9e8bf64
[fix] Compare exprs by height in simplifier
ocelaiwo Oct 20, 2023
9706690
[feat] Uninitialized Memory [feat] Sizeless ObjectState
ocelaiwo Oct 17, 2023
f635c8a
[chore] Disable test
misonijnik Oct 21, 2023
8cc4d4b
[fix] Fix performance bugs
misonijnik Oct 22, 2023
95c1595
[fix] Change satisfies function in InvalidReponse
dim8art Oct 21, 2023
05ee674
Change CacheEntry to store constraints_ty
dim8art Oct 21, 2023
4c09778
Create AlphaEquvalenceSolver
dim8art Oct 21, 2023
aa108f2
[fix] Propagation of without filter
Columpio Oct 23, 2023
4882bbf
[fix] Small fixes
Columpio Oct 23, 2023
98df581
[fix] Generate test only for successful solution found
misonijnik Oct 24, 2023
a3a4a05
[chore] Deal with compiler warnings
Columpio Oct 24, 2023
943f003
[feat] Cover on the fly based on time
Columpio Oct 24, 2023
6e92286
[fix] rewriting ordering for terms with equal height
Columpio Oct 24, 2023
7229e16
[fix] Update test
misonijnik Oct 24, 2023
c6b5d1a
[feat] Removed unwanted calls pass
Columpio Oct 25, 2023
7befcf9
[fix] Filter objects and values in `changeVersion`
misonijnik Oct 25, 2023
67480cb
[fix] Clean memory operations
misonijnik Oct 26, 2023
cc224b7
[fix] Fix `AlphaEquivalenceSolver`
misonijnik Oct 27, 2023
d882995
[fix] Halt when LLVM passes already proved unreachability
Columpio Oct 27, 2023
4fd9d16
[chore] Update version and `README.md`
misonijnik Oct 30, 2023
dd6022a
[fix] Improved call remover
Columpio Oct 31, 2023
06cf512
[feat] Add `OptimizeAggressive` option
misonijnik Nov 1, 2023
21c3523
[feat] Getting the performance/memory consumption balance in `Disjoin…
misonijnik Nov 2, 2023
5ab6cd4
[fix] Fix performance for unbalanced expressions
misonijnik Nov 2, 2023
90a9b84
[refactor] Separate `isStuck` and `isCycled`, `isStuck` is smarter now
misonijnik Nov 2, 2023
f315261
[fix] Limit the cexPreferences size
misonijnik Nov 2, 2023
06ca8d2
[fix] Remove unused field
misonijnik Nov 2, 2023
fa4a283
[fix] Fix memory consumption
misonijnik Nov 2, 2023
b06407d
[feat] Enable `coverOnTheFly` after approaching memory cup
misonijnik Nov 2, 2023
44ef6a2
[style]
misonijnik Nov 2, 2023
c7d3c48
[fix] Consider all not empty and not fully covered functions
misonijnik Nov 3, 2023
80f38b5
[fix] Fix perfomance bug
misonijnik Nov 3, 2023
d8f1867
[fix] Fix `isStuck`
misonijnik Nov 3, 2023
5ec276f
[fix] klee-test-comp.c
Columpio Nov 3, 2023
91fe2c3
[feat] Single-file run script
Columpio Nov 3, 2023
69cc99b
[chore] Updated README
Columpio Nov 7, 2023
7f3cff4
[feat] Improve coverage branches tests
misonijnik Nov 5, 2023
7b5f9a6
[fix] `CexCachingSolver`
misonijnik Nov 6, 2023
e485e7f
[fix] Slightly improve performance
misonijnik Nov 5, 2023
1866938
[fix] `AlphaEquivalenceSolver`
misonijnik Nov 7, 2023
435f392
[feat] Add `X86FPAsX87FP80`
misonijnik Nov 7, 2023
be6ef33
[chore] Update `scripts/kleef`
misonijnik Nov 7, 2023
bd7c4b8
[chore] Disable `libc++` tests on msan run because they time out on CI
misonijnik Nov 8, 2023
bca927d
[fix] Must consider the whole concretization
misonijnik Nov 8, 2023
85481ef
[chore] Update `kleef` script
misonijnik Nov 10, 2023
c28e0e2
[chore] Update tests
misonijnik Nov 10, 2023
8d8faad
[fix] `MemoryTriggerCoverOnTheFly`
misonijnik Nov 12, 2023
9ae75c9
[chore] Update `kleef`
misonijnik Nov 12, 2023
45c7b7c
[fix] Optimized free-standing functions are broken
misonijnik Nov 13, 2023
1813fc2
[chore] Update `kleef` script
misonijnik Nov 10, 2023
f585c74
[fix] Address may be symbolic but unique, try resolve firstly
misonijnik Nov 14, 2023
38a378e
[fix] Put in order `fp-runtime` functions
misonijnik Nov 14, 2023
dcdd528
[fix] Bring calls to `SparseStorage` constructor up to date
misonijnik Nov 15, 2023
45c0bb1
[feat] Added Bitwuzla solver in list of available solvers. Added scri…
S1eGa Nov 14, 2023
d9e7223
typo
dim8art Nov 21, 2023
2bcba82
Add lazy calculation of constraint dsu
dim8art Nov 21, 2023
c35bad9
[chore] Update `GuidedSearcher::selectState`
misonijnik Nov 15, 2023
0b27fb6
[fix] Convert all x86FP to x87FP80 in `FPToX87FP80Ext`
misonijnik Nov 17, 2023
9c1caa9
[fix] Restore `newSize` in case `newSize > maxSize`
misonijnik Nov 17, 2023
1df90e8
[chore] `ExprEitherSymcrete` ->`ExprOrSymcrete`
misonijnik Nov 17, 2023
5d91554
[fix] `AlphaBuilder`
misonijnik Nov 20, 2023
c71f2cb
[fix] `CexCachingSolver`
misonijnik Nov 20, 2023
dad6ccd
[fix] SparseStorage::print
ocelaiwo Nov 11, 2023
2cd78c4
[fix] `sizeOfSetRange`
misonijnik Nov 20, 2023
3b48299
[fix] Disable `AlignSymbolicPointers` by default
misonijnik Nov 21, 2023
15b79ad
[chore] Install meson locally
misonijnik Nov 21, 2023
c71b0d3
[fix] Preserve `floatReplacements`
misonijnik Nov 22, 2023
218f70d
[feat] Add new memory usage checks
ocelaiwo Nov 21, 2023
e100a78
[chore] Update options default values
misonijnik Nov 22, 2023
88975c2
[fix] Continue searching for the error if the state is not reproducible
misonijnik Nov 22, 2023
cab6da9
[feat] Added flag to dump all states if function specified in functio…
S1eGa Nov 22, 2023
241358a
[chore] Update tests
misonijnik Nov 21, 2023
592da1c
[chore] Update `build.sh`
misonijnik Nov 23, 2023
20d6e2e
[chore] Update `kleef`
misonijnik Nov 21, 2023
4ab8cfa
[chore] Update `differential-shellcheck.yml`
misonijnik Dec 9, 2023
261d966
[feat] Introduces KValue --- base class for all KLEEs wrappers around…
S1eGa Dec 12, 2023
d9f3156
[refactor] The KValue was stripped of public constructor and made abs…
S1eGa Dec 14, 2023
86e19ba
[refactor] KBlock made abstract, reduntant VALUE constant from KValue…
S1eGa Dec 18, 2023
f0fabeb
[refactor] Added ByteWidth type. Separated symbolicSizeConstantAddres…
S1eGa Dec 21, 2023
5724005
[chore] Remove submodules
misonijnik Dec 18, 2023
d238275
[chore] Add `json` and `optional` into `build.sh`
misonijnik Dec 24, 2023
4169629
[chore] replace nonstd::optional with std::optional
ocelaiwo Dec 28, 2023
fd8a45b
[fix] klee-test-comp.c: remove unused function that fails to compile
ocelaiwo Dec 28, 2023
23192d8
[feat] add entry point multiplex, remove interactive mode
ocelaiwo Dec 28, 2023
36fb45c
[fix] Fix the template argument
misonijnik Dec 30, 2023
219233c
[fix] Add arm float constants
misonijnik Dec 30, 2023
8f9fb7e
[chore] Disable tests with uint128 type on not-x86_64 targets
misonijnik Dec 31, 2023
8451cc5
[fix] Disable test on darwin due to stack overflow
misonijnik Jan 3, 2024
55f7438
[ci] Update `.cirrus.yml`
misonijnik Jan 4, 2024
cf5178a
[fix] Use `find -exec`
misonijnik Jan 17, 2024
c6a4198
[fix] Initialize local variables
misonijnik Jan 19, 2024
8d17abf
[fix] Fix assertion fail
misonijnik Jan 19, 2024
cac9566
Remove unnecessary field from the ImmutableList
ladisgin Jan 23, 2024
4fd12f0
[fix] fix bitwuzla build version fix
ocelaiwo Jan 29, 2024
79aedb6
Add mocks:
Lana243 Jun 16, 2023
f6072e0
Add annotations json parser
mamaria-k Jun 28, 2023
a36439e
Add annotations implementation:
ladisgin Jul 25, 2023
edce929
[chore] clang-format CI check replaced with pre-commit hook using cla…
S1eGa Feb 22, 2024
6b24f90
[chore, git] make entire pipeline dependent on the result of the clan…
S1eGa Feb 27, 2024
f991865
[test]
S1eGa Feb 27, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
[feat] Improved Iterative Deepening Searcher
  • Loading branch information
Columpio authored and S1eGa committed Feb 27, 2024
commit bef97af64c17849641307ec371243bf9140ea4bd
17 changes: 10 additions & 7 deletions lib/Core/ExecutionState.h
Original file line number Diff line number Diff line change
@@ -127,6 +127,7 @@ struct ExecutionStack {
inline value_stack_ty &valueStack() { return valueStack_; }
inline const value_stack_ty &valueStack() const { return valueStack_; }
inline const call_stack_ty &callStack() const { return callStack_; }
inline const info_stack_ty &infoStack() const { return infoStack_; }
inline info_stack_ty &infoStack() { return infoStack_; }
inline const call_stack_ty &uniqueFrames() const { return uniqueFrames_; }

@@ -491,16 +492,18 @@ class ExecutionState {
bool reachedTarget(ref<ReachBlockTarget> target) const;
static std::uint32_t getLastID() { return nextID - 1; };

inline bool isStuck(unsigned long long bound) {
KInstruction *prevKI = prevPC;
if (prevKI->inst->isTerminator() && stack.size() > 0) {
auto level = stack.infoStack().back().multilevel[getPCBlock()].second;
return bound && level > bound;
inline bool isStuck(unsigned long long bound) const {
if (bound == 0)
return false;
if (prevPC->inst->isTerminator() && stack.size() > 0) {
auto &ml = stack.infoStack().back().multilevel;
auto level = ml.find(getPCBlock());
return level != ml.end() && level->second > bound;
}
if (pc == pc->parent->getFirstInstruction() &&
pc->parent == pc->parent->parent->entryKBlock) {
auto level = stack.multilevel[stack.callStack().back().kf].second;
return bound && level > bound;
auto level = stack.multilevel.at(stack.callStack().back().kf);
return level > bound;
}
return false;
}
12 changes: 1 addition & 11 deletions lib/Core/Executor.cpp
Original file line number Diff line number Diff line change
@@ -4295,8 +4295,6 @@ void Executor::run(std::vector<ExecutionState *> initialStates) {
while (!states.empty() && !haltExecution) {
while (!searcher->empty() && !haltExecution) {
ExecutionState &state = searcher->selectState();
KInstruction *prevKI = state.prevPC;
KFunction *kf = prevKI->parent->parent;

executeStep(state);
}
@@ -4375,8 +4373,6 @@ static std::string terminationTypeFileExtension(StateTerminationType type) {
};

void Executor::executeStep(ExecutionState &state) {
KInstruction *prevKI = state.prevPC;

if (CoverOnTheFly && guidanceKind != GuidanceKind::ErrorGuidance &&
stats::instructions > DelayCoverOnTheFly && shouldWriteTest(state)) {
state.clearCoveredNew();
@@ -4389,13 +4385,7 @@ void Executor::executeStep(ExecutionState &state) {
if (targetManager->isTargeted(state) && state.targets().empty()) {
terminateStateEarlyAlgorithm(state, "State missed all it's targets.",
StateTerminationType::MissedAllTargets);
} else if (prevKI->inst->isTerminator() && MaxCycles &&
(state.stack.infoStack()
.back()
.multilevel[state.getPCBlock()]
.second > MaxCycles ||
state.stack.multilevel[state.stack.callStack().back().kf].second >
MaxCycles)) {
} else if (state.isStuck(MaxCycles)) {
terminateStateEarly(state, "max-cycles exceeded.",
StateTerminationType::MaxCycles);
} else {
110 changes: 85 additions & 25 deletions lib/Core/Searcher.cpp
Original file line number Diff line number Diff line change
@@ -640,33 +640,94 @@ void BatchingSearcher::printName(llvm::raw_ostream &os) {

///

IterativeDeepeningTimeSearcher::IterativeDeepeningTimeSearcher(
Searcher *baseSearcher)
: baseSearcher{baseSearcher} {};
class TimeMetric final : public IterativeDeepeningSearcher::Metric {
time::Point startTime;
time::Span time{time::seconds(1)};

ExecutionState &IterativeDeepeningTimeSearcher::selectState() {
public:
void selectState() final { startTime = time::getWallTime(); }
bool exceeds(const ExecutionState &state) const final {
return time::getWallTime() - startTime > time;
}
void increaseLimit() final {
time *= 2U;
klee_message("increased time budget to %f seconds", time.toSeconds());
}
};

class MaxCyclesMetric final : public IterativeDeepeningSearcher::Metric {
public:
using ty = unsigned long long;

private:
ty maxCycles;

public:
explicit MaxCyclesMetric(ty maxCycles) : maxCycles(maxCycles){};
explicit MaxCyclesMetric() : MaxCyclesMetric(1ULL){};

bool exceeds(const ExecutionState &state) const final {
return state.isStuck(maxCycles);
}
void increaseLimit() final {
maxCycles *= 2ULL;
klee_message("increased max-cycles to %llu", maxCycles);
}
};

IterativeDeepeningSearcher::IterativeDeepeningSearcher(
Searcher *baseSearcher, TargetManagerSubscriber *tms,
HaltExecution::Reason m)
: baseSearcher{baseSearcher}, tms{tms} {
switch (m) {
case HaltExecution::Reason::MaxTime:
metric = std::make_unique<TimeMetric>();
return;
case HaltExecution::Reason::MaxCycles:
metric = std::make_unique<MaxCyclesMetric>();
return;
default:
klee_error("Illegal metric for iterative deepening searcher: %d", m);
}
}

ExecutionState &IterativeDeepeningSearcher::selectState() {
ExecutionState &res = baseSearcher->selectState();
startTime = time::getWallTime();
metric->selectState();
return res;
}

void IterativeDeepeningTimeSearcher::update(
ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
const std::vector<ExecutionState *> &removedStates) {
void IterativeDeepeningSearcher::filter(const StatesVector &states,
StatesVector &result) const {
StatesVector states1(states);
std::sort(states1.begin(), states1.end());
std::set_difference(states1.begin(), states1.end(), pausedStates.begin(),
pausedStates.end(), std::back_inserter(result));
}

const auto elapsed = time::getWallTime() - startTime;
void IterativeDeepeningSearcher::update(
const TargetHistoryTargetPairToStatesMap &added,
const TargetHistoryTargetPairToStatesMap &removed) {
if (!tms)
return;
TargetHistoryTargetPairToStatesMap removedRefined(removed.size());
for (const auto &pair : removed) {
StatesVector refined;
IterativeDeepeningSearcher::filter(pair.second, refined);
removedRefined.emplace(pair.first, std::move(refined));
}
tms->update(added, removedRefined);
}

void IterativeDeepeningSearcher::update(ExecutionState *current,
const StatesVector &addedStates,
const StatesVector &removedStates) {

// update underlying searcher (filter paused states unknown to underlying
// searcher)
if (!removedStates.empty()) {
std::vector<ExecutionState *> alt = removedStates;
for (const auto state : removedStates) {
auto it = pausedStates.find(state);
if (it != pausedStates.end()) {
pausedStates.erase(it);
alt.erase(std::remove(alt.begin(), alt.end(), state), alt.end());
}
}
StatesVector alt;
IterativeDeepeningSearcher::filter(removedStates, alt);
baseSearcher->update(current, addedStates, alt);
} else {
baseSearcher->update(current, addedStates, removedStates);
@@ -676,27 +737,26 @@ void IterativeDeepeningTimeSearcher::update(
if (current &&
std::find(removedStates.begin(), removedStates.end(), current) ==
removedStates.end() &&
elapsed > time) {
metric->exceeds(*current)) {
pausedStates.insert(current);
baseSearcher->update(nullptr, {}, {current});
}

// no states left in underlying searcher: fill with paused states
if (baseSearcher->empty()) {
time *= 2U;
klee_message("increased time budget to %f\n", time.toSeconds());
std::vector<ExecutionState *> ps(pausedStates.begin(), pausedStates.end());
baseSearcher->update(nullptr, ps, std::vector<ExecutionState *>());
metric->increaseLimit();
StatesVector ps(pausedStates.begin(), pausedStates.end());
baseSearcher->update(nullptr, ps, {});
pausedStates.clear();
}
}

bool IterativeDeepeningTimeSearcher::empty() {
bool IterativeDeepeningSearcher::empty() {
return baseSearcher->empty() && pausedStates.empty();
}

void IterativeDeepeningTimeSearcher::printName(llvm::raw_ostream &os) {
os << "IterativeDeepeningTimeSearcher\n";
void IterativeDeepeningSearcher::printName(llvm::raw_ostream &os) {
os << "IterativeDeepeningSearcher\n";
}

///
42 changes: 26 additions & 16 deletions lib/Core/Searcher.h
Original file line number Diff line number Diff line change
@@ -160,17 +160,10 @@ class GuidedSearcher final : public Searcher, public TargetManagerSubscriber {
using TargetHistoryTargetPairHashMap =
std::unordered_map<TargetHistoryTargetPair, T, TargetHistoryTargetHash,
TargetHistoryTargetCmp>;

using TargetHistoryTargetPair =
std::pair<ref<const TargetsHistory>, ref<Target>>;
using TargetHistoryTargetPairToSearcherMap =
std::unordered_map<TargetHistoryTargetPair,
std::unique_ptr<TargetedSearcher>,
TargetHistoryTargetHash, TargetHistoryTargetCmp>;
using StatesVector = std::vector<ExecutionState *>;
using TargetHistoryTargetPairToStatesMap =
std::unordered_map<TargetHistoryTargetPair, StatesVector,
TargetHistoryTargetHash, TargetHistoryTargetCmp>;
using TargetForestHisoryTargetVector = std::vector<TargetHistoryTargetPair>;
using TargetForestHistoryTargetSet =
std::unordered_set<TargetHistoryTargetPair, TargetHistoryTargetHash,
@@ -323,26 +316,43 @@ class BatchingSearcher final : public Searcher {
void printName(llvm::raw_ostream &os) override;
};

/// IterativeDeepeningTimeSearcher implements time-based deepening. States
/// are selected from an underlying searcher. When a state reaches its time
/// limit it is paused (removed from underlying searcher). When the underlying
/// searcher runs out of states, the time budget is increased and all paused
/// IterativeDeepeningSearcher implements a metric-based deepening. States
/// are selected from an underlying searcher. When a state exceeds its metric
/// limit, it is paused (removed from underlying searcher). When the underlying
/// searcher runs out of states, the metric limit is increased and all paused
/// states are revived (added to underlying searcher).
class IterativeDeepeningTimeSearcher final : public Searcher {
class IterativeDeepeningSearcher final : public Searcher,
public TargetManagerSubscriber {
public:
struct Metric {
virtual ~Metric() = default;
virtual void selectState(){};
virtual bool exceeds(const ExecutionState &state) const = 0;
virtual void increaseLimit() = 0;
};

private:
std::unique_ptr<Searcher> baseSearcher;
time::Point startTime;
time::Span time{time::seconds(1)};
TargetManagerSubscriber *tms;
std::unique_ptr<Metric> metric;
std::set<ExecutionState *> pausedStates;

void filter(const std::vector<ExecutionState *> &states,
std::vector<ExecutionState *> &result) const;

public:
/// \param baseSearcher The underlying searcher (takes ownership).
explicit IterativeDeepeningTimeSearcher(Searcher *baseSearcher);
~IterativeDeepeningTimeSearcher() override = default;
explicit IterativeDeepeningSearcher(Searcher *baseSearcher,
TargetManagerSubscriber *tms,
HaltExecution::Reason metric);
~IterativeDeepeningSearcher() override = default;

ExecutionState &selectState() override;
void update(ExecutionState *current,
const std::vector<ExecutionState *> &addedStates,
const std::vector<ExecutionState *> &removedStates) override;
void update(const TargetHistoryTargetPairToStatesMap &added,
const TargetHistoryTargetPairToStatesMap &removed) override;
bool empty() override;
void printName(llvm::raw_ostream &os) override;
};
2 changes: 1 addition & 1 deletion lib/Core/StatsTracker.cpp
Original file line number Diff line number Diff line change
@@ -392,7 +392,7 @@ void StatsTracker::stepInstruction(ExecutionState &es) {

Instruction *inst = es.pc->inst;
const KInstruction *ki = es.pc;
InfoStackFrame &sf = es.stack.infoStack().back();
auto &sf = es.stack.infoStack().back();
theStatisticManager->setIndex(ki->getGlobalIndex());
if (UseCallPaths)
theStatisticManager->setContext(&sf.callPathNode->statistics);
20 changes: 7 additions & 13 deletions lib/Core/TargetManager.h
Original file line number Diff line number Diff line change
@@ -25,15 +25,15 @@
namespace klee {
class TargetCalculator;

using TargetHistoryTargetPair =
std::pair<ref<const TargetsHistory>, ref<Target>>;
using StatesVector = std::vector<ExecutionState *>;
using TargetHistoryTargetPairToStatesMap =
std::unordered_map<TargetHistoryTargetPair, StatesVector,
TargetHistoryTargetHash, TargetHistoryTargetCmp>;

class TargetManagerSubscriber {
public:
using TargetHistoryTargetPair =
std::pair<ref<const TargetsHistory>, ref<Target>>;
using StatesVector = std::vector<ExecutionState *>;
using TargetHistoryTargetPairToStatesMap =
std::unordered_map<TargetHistoryTargetPair, StatesVector,
TargetHistoryTargetHash, TargetHistoryTargetCmp>;

virtual ~TargetManagerSubscriber() = default;

/// Selects a state for further exploration.
@@ -47,12 +47,6 @@ class TargetManager {
using StatesSet = std::unordered_set<ExecutionState *>;
using StateToDistanceMap =
std::unordered_map<const ExecutionState *, TargetHashMap<DistanceResult>>;
using TargetHistoryTargetPair =
std::pair<ref<const TargetsHistory>, ref<Target>>;
using StatesVector = std::vector<ExecutionState *>;
using TargetHistoryTargetPairToStatesMap =
std::unordered_map<TargetHistoryTargetPair, StatesVector,
TargetHistoryTargetHash, TargetHistoryTargetCmp>;
using TargetForestHistoryTargetSet =
std::unordered_set<TargetHistoryTargetPair, TargetHistoryTargetHash,
TargetHistoryTargetCmp>;
32 changes: 22 additions & 10 deletions lib/Core/UserSearcher.cpp
Original file line number Diff line number Diff line change
@@ -55,11 +55,17 @@ cl::list<Searcher::CoreSearchType> CoreSearch(
clEnumValN(Searcher::NURS_QC, "nurs:qc", "use NURS with Query-Cost")),
cl::cat(SearchCat));

cl::opt<bool> UseIterativeDeepeningTimeSearch(
"use-iterative-deepening-time-search",
cl::desc(
"Use iterative deepening time search (experimental) (default=false)"),
cl::init(false), cl::cat(SearchCat));
cl::opt<HaltExecution::Reason> UseIterativeDeepeningSearch(
"use-iterative-deepening-search",
cl::desc("Use iterative deepening search based on metric (experimental) "
"(default=unspecified)"),
cl::values(clEnumValN(HaltExecution::Reason::Unspecified, "unspecified",
"Do not use iterative deepening search (default)"),
clEnumValN(HaltExecution::Reason::MaxTime, "max-time",
"metric is maximum time"),
clEnumValN(HaltExecution::Reason::MaxCycles, "max-cycles",
"metric is maximum cycles")),
cl::init(HaltExecution::Reason::Unspecified), cl::cat(SearchCat));

cl::opt<bool> UseBatchingSearch(
"use-batching-search",
@@ -172,16 +178,22 @@ Searcher *klee::constructUserSearcher(Executor &executor,
BatchInstructions);
}

if (UseIterativeDeepeningTimeSearch) {
searcher = new IterativeDeepeningTimeSearcher(searcher);
}

TargetManagerSubscriber *tms = nullptr;
if (executor.guidanceKind != Interpreter::GuidanceKind::NoGuidance) {
searcher = new GuidedSearcher(searcher, *executor.distanceCalculator,
executor.theRNG);
executor.targetManager->subscribe(*static_cast<GuidedSearcher *>(searcher));
tms = static_cast<GuidedSearcher *>(searcher);
}

if (UseIterativeDeepeningSearch != HaltExecution::Reason::Unspecified) {
searcher = new IterativeDeepeningSearcher(searcher, tms,
UseIterativeDeepeningSearch);
tms = static_cast<IterativeDeepeningSearcher *>(searcher);
}

if (tms)
executor.targetManager->subscribe(*tms);

llvm::raw_ostream &os = executor.getHandler().getInfoStream();

os << "BEGIN searcher description\n";
8 changes: 4 additions & 4 deletions test/Feature/Searchers.c
Original file line number Diff line number Diff line change
@@ -18,13 +18,13 @@
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --search=random-path --search=nurs:qc %t2.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-time-search --use-batching-search %t2.bc
// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-search=max-time --use-batching-search %t2.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-time-search --use-batching-search --search=random-state %t2.bc
// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-search=max-time --use-batching-search --search=random-state %t2.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-time-search --use-batching-search --search=nurs:depth %t2.bc
// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-search=max-time --use-batching-search --search=nurs:depth %t2.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-time-search --use-batching-search --search=nurs:qc %t2.bc
// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-search=max-time --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
Loading