Skip to content

Commit 75f357a

Browse files
dim8artdim8art
committed
f
1 parent e764f37 commit 75f357a

4 files changed

Lines changed: 69 additions & 32 deletions

File tree

‎lib/Core/Executor.cpp‎

Lines changed: 51 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -1270,9 +1270,11 @@ void Executor::branch(ExecutionState &state,
12701270
}
12711271
}
12721272

1273-
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
1274-
seedMap->find(&state);
1275-
if (it != seedMap->end()) {
1273+
if (state.isSeeded) {
1274+
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
1275+
seedMap->find(&state);
1276+
assert(it != seedMap->end());
1277+
assert(!it->second.empty());
12761278
std::vector<ExecutingSeed> seeds = it->second;
12771279
seedMap->erase(it);
12781280
objectManager->unseed(it->first);
@@ -1410,11 +1412,8 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
14101412
KBlock *ifTrueBlock, KBlock *ifFalseBlock,
14111413
BranchType reason) {
14121414
bool isInternal = ifTrueBlock == ifFalseBlock;
1413-
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
1414-
seedMap->find(&current);
1415-
bool isSeeding = it != seedMap->end();
14161415
PartialValidity res = PartialValidity::None;
1417-
1416+
bool isSeeding = current.isSeeded;
14181417
std::vector<ExecutingSeed> trueSeeds;
14191418
std::vector<ExecutingSeed> falseSeeds;
14201419
time::Span timeout = coreSolverTimeout;
@@ -1438,7 +1437,11 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
14381437
addConstraint(current, Expr::createIsZero(condition));
14391438
}
14401439
}
1441-
} else if (!it->second.empty()) {
1440+
} else {
1441+
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
1442+
seedMap->find(&current);
1443+
assert(it != seedMap->end());
1444+
assert(!it->second.empty());
14421445
timeout *= static_cast<unsigned>(it->second.size());
14431446
for (std::vector<ExecutingSeed>::iterator siit = it->second.begin(),
14441447
siie = it->second.end();
@@ -1646,9 +1649,11 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
16461649
}
16471650

16481651
// Check to see if this constraint violates seeds.
1649-
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
1650-
seedMap->find(&state);
1651-
if (PatchSeeds && it != seedMap->end()) {
1652+
if (PatchSeeds && state.isSeeded) {
1653+
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
1654+
seedMap->find(&state);
1655+
assert(it != seedMap->end());
1656+
assert(!it->second.empty());
16521657
bool warn = false;
16531658
for (std::vector<ExecutingSeed>::iterator siit = it->second.begin(),
16541659
siie = it->second.end();
@@ -1796,10 +1801,7 @@ Executor::toConstantPointer(ExecutionState &state, ref<PointerExpr> e,
17961801
void Executor::executeGetValue(ExecutionState &state, ref<Expr> e,
17971802
KInstruction *target) {
17981803
e = Simplificator::simplifyExpr(state.constraints.cs(), e).simplified;
1799-
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
1800-
seedMap->find(&state);
1801-
if (it == seedMap->end() || isa<ConstantExpr>(e) ||
1802-
isa<ConstantPointerExpr>(e)) {
1804+
if (!state.isSeeded || isa<ConstantExpr>(e) || isa<ConstantPointerExpr>(e)) {
18031805
ref<Expr> value;
18041806
e = optimizer.optimizeExpr(e, true);
18051807
bool success =
@@ -1808,6 +1810,10 @@ void Executor::executeGetValue(ExecutionState &state, ref<Expr> e,
18081810
(void)success;
18091811
bindLocal(target, state, value);
18101812
} else {
1813+
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
1814+
seedMap->find(&state);
1815+
assert(it != seedMap->end());
1816+
assert(!it->second.empty());
18111817
std::set<ref<Expr>> values;
18121818
for (std::vector<ExecutingSeed>::iterator siit = it->second.begin(),
18131819
siie = it->second.end();
@@ -4497,7 +4503,8 @@ Executor::MemoryUsage Executor::checkMemoryUsage() {
44974503
arr.push_back(state);
44984504
}
44994505
}
4500-
auto toKill = std::min(arr.size(), numStates - numStates * MaxMemory / totalUsage);
4506+
auto toKill =
4507+
std::min(arr.size(), numStates - numStates * MaxMemory / totalUsage);
45014508

45024509
if (toKill != 0) {
45034510
klee_warning("killing %lu states (over memory cap: %luMB)", toKill,
@@ -4670,16 +4677,22 @@ void Executor::initialSeed(ExecutionState &initialState,
46704677
objectManager->updateSubscribers();
46714678
}
46724679

4673-
ExecutingSeed Executor::storeState(const ExecutionState &state,
4674-
bool isCompleted) {
4675-
KTest *ktest = 0;
4676-
ktest = (KTest *)calloc(1, sizeof(*ktest));
4677-
bool success = getSymbolicSolution(state, ktest);
4678-
if (!success)
4680+
bool Executor::storeState(const ExecutionState &state, bool isCompleted,
4681+
ExecutingSeed &res) {
4682+
solver->setTimeout(coreSolverTimeout);
4683+
auto arrays = state.constraints.cs().gatherArrays();
4684+
std::vector<SparseStorageImpl<unsigned char>> values;
4685+
bool success = solver->getInitialValues(state.constraints.cs(), arrays,
4686+
values, state.queryMetaData);
4687+
if (!success) {
46794688
klee_warning("unable to get symbolic solution, losing test case");
4680-
ExecutingSeed seed(ktest, state.steppedInstructions, isCompleted,
4689+
return false;
4690+
}
4691+
Assignment assignment(arrays, values);
4692+
ExecutingSeed seed(assignment, state.steppedInstructions, isCompleted,
46814693
state.coveredNew, state.coveredNewError);
4682-
return seed;
4694+
res = seed;
4695+
return true;
46834696
}
46844697

46854698
void Executor::reportProgressTowardsTargets(std::string prefix,
@@ -5063,8 +5076,11 @@ void Executor::terminateStateEarly(ExecutionState &state, const Twine &message,
50635076
(AlwaysOutputSeeds && seedMap->count(&state))) {
50645077
state.clearCoveredNew();
50655078
if (StoreSeedsLocally) {
5066-
storedSeeds->push_back(
5067-
storeState(state, !(reason <= StateTerminationType::EARLY)));
5079+
ExecutingSeed seed;
5080+
bool success = storeState(state, !(reason <= StateTerminationType::EARLY), seed);
5081+
if (success) {
5082+
storedSeeds->push_back(seed);
5083+
}
50685084
} else {
50695085
interpreterHandler->processTestCase(
50705086
state, (message + "\n").str().c_str(),
@@ -6899,17 +6915,22 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
68996915
}
69006916
state.addSymbolic(mo, array, type);
69016917

6902-
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
6903-
seedMap->find(&state);
6904-
if (it != seedMap->end()) { // In seed mode we need to add this as a
6905-
// binding.
6918+
if (state.isSeeded) { // In seed mode we need to add this as a
6919+
// binding.
6920+
std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
6921+
seedMap->find(&state);
6922+
assert(it != seedMap->end());
6923+
assert(!it->second.empty());
69066924
for (std::vector<ExecutingSeed>::iterator siit = it->second.begin(),
69076925
siie = it->second.end();
69086926
siit != siie; ++siit) {
69096927
ExecutingSeed &si = *siit;
69106928
KTestObject *obj = si.getNextInput(mo, NamedSeedMatching);
69116929

69126930
if (!obj) {
6931+
if (si.assignment.bindings.count(array) != 0) {
6932+
continue;
6933+
}
69136934
if (ZeroSeedExtension) {
69146935
si.assignment.bindings.replace(
69156936
{array, SparseStorageImpl<unsigned char>(0)});

‎lib/Core/Executor.h‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -267,9 +267,11 @@ class Executor : public Interpreter {
267267
void getKTestFilesInDir(std::string directoryPath,
268268
std::vector<std::string> &results);
269269
std::vector<ExecutingSeed> uploadNewSeeds();
270-
void initialSeed(ExecutionState &initialState, std::vector<ExecutingSeed> usingSeeds);
270+
void initialSeed(ExecutionState &initialState,
271+
std::vector<ExecutingSeed> usingSeeds);
271272

272-
ExecutingSeed storeState(const ExecutionState &state, bool isCompleted);
273+
bool storeState(const ExecutionState &state, bool isCompleted,
274+
ExecutingSeed &res);
273275

274276
void run(ExecutionState *initialState);
275277

‎lib/Core/SeedInfo.cpp‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,9 @@ ExecutingSeed::ExecutingSeed(std::string _path)
3737
}
3838

3939
KTestObject *ExecutingSeed::getNextInput(const MemoryObject *mo, bool byName) {
40+
if (!input)
41+
return nullptr;
42+
4043
if (byName) {
4144
unsigned i;
4245

‎lib/Core/SeedInfo.h‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,13 +40,24 @@ class ExecutingSeed {
4040
public:
4141
~ExecutingSeed() {}
4242

43+
ExecutingSeed() {}
44+
4345
explicit ExecutingSeed(KTest *input, unsigned maxInstructions,
4446
bool isCompleted,
4547
std::deque<ref<box<bool>>> coveredNew,
4648
ref<box<bool>> coveredNewError)
4749
: input(input, kTestDeleter), maxInstructions(maxInstructions),
4850
isCompleted(isCompleted), coveredNew(coveredNew),
4951
coveredNewError(coveredNewError) {}
52+
53+
explicit ExecutingSeed(Assignment assignment, unsigned maxInstructions,
54+
bool isCompleted,
55+
std::deque<ref<box<bool>>> coveredNew,
56+
ref<box<bool>> coveredNewError)
57+
: assignment(assignment), maxInstructions(maxInstructions),
58+
isCompleted(isCompleted), coveredNew(coveredNew),
59+
coveredNewError(coveredNewError) {}
60+
5061
ExecutingSeed(std::string _path);
5162

5263
KTestObject *getNextInput(const MemoryObject *mo, bool byName);

0 commit comments

Comments
 (0)