Skip to content

Commit 0ed3a65

Browse files
dim8artdim8art
committed
[fix} Fixed ran out of inputs problem
1 parent 341ca93 commit 0ed3a65

File tree

7 files changed

+93
-92
lines changed

7 files changed

+93
-92
lines changed

‎lib/Core/Executor.cpp‎

Lines changed: 55 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -234,7 +234,14 @@ cl::opt<bool> RunForever("run-forever",
234234
cl::desc("Store states when out of memory and explore "
235235
"them later (default=false)"),
236236
cl::init(false), cl::cat(SeedingCat));
237-
237+
cl::list<std::string>
238+
SeedOutDir("seed-dir",
239+
cl::desc("Directory with .ktest files to be used as seeds"),
240+
cl::cat(SeedingCat));
241+
242+
cl::list<std::string> SeedOutFile("seed-file",
243+
cl::desc(".ktest file to be used as seed"),
244+
cl::cat(SeedingCat));
238245
} // namespace klee
239246

240247
namespace {
@@ -1222,18 +1229,16 @@ void Executor::branch(ExecutionState &state,
12221229
}
12231230

12241231
if (state.isSeeded) {
1225-
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
1226-
seedMap->find(&state);
1232+
std::map<ExecutionState *, seeds_ty>::iterator it = seedMap->find(&state);
12271233
assert(it != seedMap->end());
12281234
assert(!it->second.empty());
1229-
std::vector<ExecutingSeed> seeds = it->second;
1235+
seeds_ty seeds = it->second;
12301236
seedMap->erase(it);
12311237
objectManager->unseed(it->first);
12321238
// Assume each seed only satisfies one condition (necessarily true
12331239
// when conditions are mutually exclusive and their conjunction is
12341240
// a tautology).
1235-
for (std::vector<ExecutingSeed>::iterator siit = seeds.begin(),
1236-
siie = seeds.end();
1241+
for (seeds_ty::iterator siit = seeds.begin(), siie = seeds.end();
12371242
siit != siie; ++siit) {
12381243
unsigned i;
12391244
for (i = 0; i < N; ++i) {
@@ -1254,7 +1259,7 @@ void Executor::branch(ExecutionState &state,
12541259

12551260
// Extra check in case we're replaying seeds with a max-fork
12561261
if (result[i]) {
1257-
seedMap->at(result[i]).push_back(*siit);
1262+
seedMap->at(result[i]).insert(*siit);
12581263
}
12591264
}
12601265
}
@@ -1360,8 +1365,8 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
13601365
bool isInternal = ifTrueBlock == ifFalseBlock;
13611366
PartialValidity res = PartialValidity::None;
13621367
bool isSeeding = current.isSeeded;
1363-
std::vector<ExecutingSeed> trueSeeds;
1364-
std::vector<ExecutingSeed> falseSeeds;
1368+
seeds_ty trueSeeds;
1369+
seeds_ty falseSeeds;
13651370
time::Span timeout = coreSolverTimeout;
13661371
bool shouldCheckTrueBlock = true, shouldCheckFalseBlock = true;
13671372

@@ -1385,13 +1390,11 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
13851390
}
13861391
}
13871392
} else {
1388-
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
1389-
seedMap->find(&current);
1393+
std::map<ExecutionState *, seeds_ty>::iterator it = seedMap->find(&current);
13901394
assert(it != seedMap->end());
13911395
assert(!it->second.empty());
13921396
timeout *= static_cast<unsigned>(it->second.size());
1393-
for (std::vector<ExecutingSeed>::iterator siit = it->second.begin(),
1394-
siie = it->second.end();
1397+
for (seeds_ty::iterator siit = it->second.begin(), siie = it->second.end();
13951398
siit != siie; ++siit) {
13961399
ref<ConstantExpr> result;
13971400
bool success = solver->getValue(current.constraints.cs(),
@@ -1400,9 +1403,9 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
14001403
assert(success && "FIXME: Unhandled solver failure");
14011404
(void)success;
14021405
if (result->isTrue()) {
1403-
trueSeeds.push_back(*siit);
1406+
trueSeeds.insert(*siit);
14041407
} else if (result->isFalse()) {
1405-
falseSeeds.push_back(*siit);
1408+
falseSeeds.insert(*siit);
14061409
}
14071410
}
14081411
if (!trueSeeds.empty() && falseSeeds.empty()) {
@@ -1737,13 +1740,11 @@ void Executor::executeGetValue(ExecutionState &state, ref<Expr> e,
17371740
(void)success;
17381741
bindLocal(target, state, value);
17391742
} else {
1740-
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
1741-
seedMap->find(&state);
1743+
std::map<ExecutionState *, seeds_ty>::iterator it = seedMap->find(&state);
17421744
assert(it != seedMap->end());
17431745
assert(!it->second.empty());
17441746
std::set<ref<Expr>> values;
1745-
for (std::vector<ExecutingSeed>::iterator siit = it->second.begin(),
1746-
siie = it->second.end();
1747+
for (seeds_ty::iterator siit = it->second.begin(), siie = it->second.end();
17471748
siit != siie; ++siit) {
17481749
ref<Expr> cond = siit->assignment.evaluate(e);
17491750
cond = optimizer.optimizeExpr(cond, true);
@@ -4562,16 +4563,14 @@ std::vector<ExecutingSeed> Executor::uploadNewSeeds() {
45624563

45634564
void Executor::initialSeed(ExecutionState &initialState,
45644565
std::vector<ExecutingSeed> usingSeeds) {
4565-
// FIX: better file managment when seeding + flag if all seeds are completed
4566-
45674566
if (usingSeeds.empty()) {
45684567
return;
45694568
}
4570-
std::vector<ExecutingSeed> &v = seedMap->at(&initialState);
4569+
seeds_ty &v = seedMap->at(&initialState);
45714570
for (std::vector<ExecutingSeed>::const_iterator it = usingSeeds.begin(),
45724571
ie = usingSeeds.end();
45734572
it != ie; ++it) {
4574-
v.push_back(*it);
4573+
v.insert(*it);
45754574
}
45764575
klee_message("Seeding began using %ld seeds!\n", usingSeeds.size());
45774576
objectManager->seed(&initialState);
@@ -4760,27 +4759,38 @@ bool Executor::reachedMaxSeedInstructions(ExecutionState *state) {
47604759
assert(state->isSeeded);
47614760
auto it = seedMap->find(state);
47624761
assert(it != seedMap->end());
4763-
if (it->second.size() != 1) {
4764-
return false;
4765-
}
47664762

4767-
std::vector<ExecutingSeed>::iterator siit = it->second.begin();
4763+
seeds_ty &seeds = it->second;
4764+
4765+
assert(!seeds.empty());
4766+
assert(seeds.begin()->maxInstructions >= state->steppedInstructions &&
4767+
"state stepped instructions exceeded seed max instructions");
4768+
4769+
seeds_ty::iterator siit = seeds.begin();
47684770
if (siit->maxInstructions &&
4769-
siit->maxInstructions <= state->steppedInstructions) {
4770-
assert(siit->maxInstructions == state->steppedInstructions &&
4771-
"state stepped instructions exceeded seed max instructions");
4772-
state->coveredNew = siit->coveredNew;
4773-
if (siit->coveredNewError) {
4774-
state->coveredNewError = siit->coveredNewError;
4775-
}
4776-
seedMap->erase(state);
4777-
objectManager->unseed(state);
4778-
if (seedMap->size() == 0) {
4779-
klee_message("Seeding done!\n");
4771+
siit->maxInstructions == state->steppedInstructions) {
4772+
if (seeds.size() == 1) {
4773+
state->coveredNew = siit->coveredNew;
4774+
if (siit->coveredNewError) {
4775+
state->coveredNewError = siit->coveredNewError;
4776+
}
47804777
}
4781-
return true;
4778+
seeds.erase(seeds.begin());
47824779
}
4783-
return false;
4780+
4781+
assert(seeds.empty() ||
4782+
seeds.begin()->maxInstructions != state->steppedInstructions);
4783+
4784+
if (!seeds.empty()) {
4785+
return false;
4786+
}
4787+
4788+
seedMap->erase(state);
4789+
objectManager->unseed(state);
4790+
if (seedMap->size() == 0) {
4791+
klee_message("Seeding done!\n");
4792+
}
4793+
return true;
47844794
}
47854795

47864796
void Executor::goForward(ref<ForwardAction> action) {
@@ -4799,7 +4809,6 @@ void Executor::goForward(ref<ForwardAction> action) {
47994809
if (targetManager) {
48004810
targetManager->pullGlobal(state);
48014811
}
4802-
48034812
if (targetCalculator && TrackCoverage != TrackCoverageBy::None &&
48044813
state.multiplexKF && functionsByModule.modules.size() > 1 &&
48054814
targetCalculator->isCovered(state.multiplexKF)) {
@@ -4815,7 +4824,7 @@ void Executor::goForward(ref<ForwardAction> action) {
48154824
} else if (state.isSymbolicCycled(MaxSymbolicCycles)) {
48164825
terminateStateEarly(state, "max-sym-cycles exceeded.",
48174826
StateTerminationType::MaxCycles);
4818-
} else if (!fa->state->isSeeded || !reachedMaxSeedInstructions(fa->state)) {
4827+
} else if (!state.isSeeded || !reachedMaxSeedInstructions(&state)) {
48194828
maxNewWriteableOSSize = 0;
48204829
maxNewStateStackSize = 0;
48214830

@@ -6801,14 +6810,13 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
68016810

68026811
if (state.isSeeded) { // In seed mode we need to add this as a
68036812
// binding.
6804-
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
6805-
seedMap->find(&state);
6813+
std::map<ExecutionState *, seeds_ty>::iterator it = seedMap->find(&state);
68066814
assert(it != seedMap->end());
68076815
assert(!it->second.empty());
6808-
for (std::vector<ExecutingSeed>::iterator siit = it->second.begin(),
6809-
siie = it->second.end();
6816+
for (seeds_ty::iterator siit = it->second.begin(),
6817+
siie = it->second.end();
68106818
siit != siie; ++siit) {
6811-
ExecutingSeed &si = *siit;
6819+
const ExecutingSeed &si = *siit;
68126820
KTestObject *obj = si.getNextInput(mo, NamedSeedMatching);
68136821

68146822
if (!obj) {

‎lib/Core/SeedInfo.cpp‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,8 @@ using namespace klee;
2424

2525
void ExecutingSeed::kTestDeleter(KTest *ktest) { kTest_free(ktest); }
2626

27-
KTestObject *ExecutingSeed::getNextInput(const MemoryObject *mo, bool byName) {
27+
KTestObject *ExecutingSeed::getNextInput(const MemoryObject *mo,
28+
bool byName) const {
2829
if (!input)
2930
return nullptr;
3031

‎lib/Core/SeedInfo.h‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -27,13 +27,13 @@ class MemoryObject;
2727

2828
class ExecutingSeed {
2929
public:
30-
Assignment assignment;
30+
mutable Assignment assignment;
3131
std::shared_ptr<KTest> input;
3232
unsigned maxInstructions = 0;
33-
std::set<struct KTestObject *> used;
33+
mutable std::set<struct KTestObject *> used;
3434
mutable std::deque<ref<box<bool>>> coveredNew;
3535
mutable ref<box<bool>> coveredNewError = nullptr;
36-
unsigned inputPosition = 0;
36+
mutable unsigned inputPosition = 0;
3737

3838
public:
3939
~ExecutingSeed() {}
@@ -52,7 +52,7 @@ class ExecutingSeed {
5252
: assignment(assignment), maxInstructions(maxInstructions),
5353
coveredNew(coveredNew), coveredNewError(coveredNewError) {}
5454

55-
KTestObject *getNextInput(const MemoryObject *mo, bool byName);
55+
KTestObject *getNextInput(const MemoryObject *mo, bool byName) const;
5656

5757
static void kTestDeleter(KTest *ktest);
5858
};

‎lib/Core/SeedMap.cpp‎

Lines changed: 9 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -8,54 +8,47 @@ SeedMap::SeedMap() {}
88
void SeedMap::update(ref<ObjectManager::Event> e) {
99
if (auto statesEvent = dyn_cast<ObjectManager::States>(e)) {
1010
for (const auto state : statesEvent->removed) {
11-
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
12-
seedMap.find(state);
11+
std::map<ExecutionState *, seeds_ty>::iterator it = seedMap.find(state);
1312
if (it != seedMap.end()) {
1413
seedMap.erase(it);
1514
}
1615
}
1716
}
1817
}
1918

20-
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator
19+
std::map<ExecutionState *, seeds_ty>::iterator
2120
SeedMap::upper_bound(ExecutionState *state) {
2221
return seedMap.upper_bound(state);
2322
}
2423

25-
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator
24+
std::map<ExecutionState *, seeds_ty>::iterator
2625
SeedMap::find(ExecutionState *state) {
2726
return seedMap.find(state);
2827
}
2928

30-
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator
31-
SeedMap::begin() {
29+
std::map<ExecutionState *, seeds_ty>::iterator SeedMap::begin() {
3230
return seedMap.begin();
3331
}
3432

35-
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator
36-
SeedMap::end() {
33+
std::map<ExecutionState *, seeds_ty>::iterator SeedMap::end() {
3734
return seedMap.end();
3835
}
3936

40-
void SeedMap::erase(
41-
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it) {
37+
void SeedMap::erase(std::map<ExecutionState *, seeds_ty>::iterator it) {
4238
seedMap.erase(it);
4339
}
4440

4541
void SeedMap::erase(ExecutionState *state) { seedMap.erase(state); }
4642

47-
void SeedMap::push_back(ExecutionState *state,
48-
std::vector<ExecutingSeed>::iterator siit) {
49-
seedMap[state].push_back(*siit);
43+
void SeedMap::insert(ExecutionState *state, seeds_ty::iterator siit) {
44+
seedMap[state].insert(*siit);
5045
}
5146

5247
std::size_t SeedMap::count(ExecutionState *state) {
5348
return seedMap.count(state);
5449
}
5550

56-
std::vector<ExecutingSeed> &SeedMap::at(ExecutionState *state) {
57-
return seedMap[state];
58-
}
51+
seeds_ty &SeedMap::at(ExecutionState *state) { return seedMap[state]; }
5952

6053
bool SeedMap::empty() { return seedMap.empty(); }
6154

‎lib/Core/SeedMap.h‎

Lines changed: 18 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -6,30 +6,36 @@
66
#include "SeedInfo.h"
77

88
#include <map>
9-
9+
#include <set>
1010
namespace klee {
11+
12+
struct SeedLess {
13+
bool operator()(const ExecutingSeed &a, const ExecutingSeed &b) const {
14+
return a.maxInstructions <= b.maxInstructions;
15+
}
16+
};
17+
18+
using seeds_ty = std::multiset<ExecutingSeed, SeedLess>;
19+
1120
class SeedMap : public Subscriber {
1221
private:
13-
std::map<ExecutionState *, std::vector<ExecutingSeed>> seedMap;
22+
std::map<ExecutionState *, seeds_ty> seedMap;
1423

1524
public:
1625
SeedMap();
1726

1827
void update(ref<ObjectManager::Event> e) override;
1928

20-
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator
29+
std::map<ExecutionState *, seeds_ty>::iterator
2130
upper_bound(ExecutionState *state);
22-
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator
23-
find(ExecutionState *state);
24-
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator end();
25-
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator begin();
26-
void
27-
erase(std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it);
31+
std::map<ExecutionState *, seeds_ty>::iterator find(ExecutionState *state);
32+
std::map<ExecutionState *, seeds_ty>::iterator end();
33+
std::map<ExecutionState *, seeds_ty>::iterator begin();
34+
void erase(std::map<ExecutionState *, seeds_ty>::iterator it);
2835
void erase(ExecutionState *state);
29-
void push_back(ExecutionState *state,
30-
std::vector<ExecutingSeed>::iterator siit);
36+
void insert(ExecutionState *state, seeds_ty::iterator siit);
3137
std::size_t count(ExecutionState *state);
32-
std::vector<ExecutingSeed> &at(ExecutionState *state);
38+
seeds_ty &at(ExecutionState *state);
3339
unsigned size() { return seedMap.size(); }
3440
bool empty();
3541

‎lib/Core/UserSearcher.cpp‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,6 @@
1616

1717
#include "llvm/Support/CommandLine.h"
1818

19-
#include <string>
20-
2119
using namespace llvm;
2220
using namespace klee;
2321

@@ -207,7 +205,8 @@ Searcher *klee::constructUserSearcher(Executor &executor) {
207205
} else {
208206
searcher = constructBaseSearcher(executor);
209207
}
210-
if(RunForever){
208+
if (RunForever || SeedOutFile.begin() != SeedOutFile.end() ||
209+
SeedOutDir.begin() != SeedOutDir.end()) {
211210
searcher = new SeededSearcher(searcher);
212211
}
213212
llvm::raw_ostream &os = executor.getHandler().getInfoStream();

0 commit comments

Comments
 (0)