Skip to content

Commit

Permalink
Fix after rebase
Browse files Browse the repository at this point in the history
  • Loading branch information
ladisgin committed Nov 17, 2023
1 parent bf38aa9 commit b818f5c
Showing 1 changed file with 43 additions and 49 deletions.
92 changes: 43 additions & 49 deletions lib/Core/Executor.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -609,28 +609,21 @@ llvm::Module *Executor::setModule(
specialFunctionHandler = new SpecialFunctionHandler(*this);
specialFunctionHandler->prepare(preservedFunctions);

preservedFunctions.push_back(opts.EntryPoint.c_str());

// Preserve the free-standing library calls
preservedFunctions.push_back("memset");
preservedFunctions.push_back("memcpy");
preservedFunctions.push_back("memcmp");
preservedFunctions.push_back("memmove");

if (FunctionCallReproduce != "") {
preservedFunctions.push_back(FunctionCallReproduce.c_str());
}

// prevent elimination of the preservedFunctions functions
for (auto pf : preservedFunctions) {
auto f = kmodule->module->getFunction(pf);
if (f) {
// prevent elimination of the function
auto f = kmodule->module->getFunction(FunctionCallReproduce);
if (f)
f->addFnAttr(Attribute::OptimizeNone);
f->addFnAttr(Attribute::NoInline);
}
}

// except the entry point
preservedFunctions.push_back(opts.EntryPoint.c_str());

kmodule->optimiseAndPrepare(opts, preservedFunctions);
kmodule->checkModule();

Expand Down Expand Up @@ -2949,46 +2942,47 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
prepareMockValue(state, "mockExternResult", ki);
}
} else {
ExecutionState *free = &state;
bool hasInvalid = false, first = true;

/* XXX This is wasteful, no need to do a full evaluate since we
have already got a value. But in the end the caches should
handle it for us, albeit with some overhead. */
do {
v = optimizer.optimizeExpr(v, true);
ref<ConstantExpr> value;
bool success = solver->getValue(free->constraints.cs(), v, value,
free->queryMetaData);
assert(success && "FIXME: Unhandled solver failure");
(void)success;
StatePair res =
forkInternal(*free, EqExpr::create(v, value), BranchType::Call);
if (res.first) {
uint64_t addr = value->getZExtValue();
auto it = legalFunctions.find(addr);
if (it != legalFunctions.end()) {
f = it->second;

// Don't give warning on unique resolution
if (res.second || !first)
klee_warning_once(reinterpret_cast<void *>(addr),
"resolved symbolic function pointer to: %s",
f->getName().data());

executeCall(*res.first, ki, f, arguments);
} else {
if (!hasInvalid) {
terminateStateOnExecError(state, "invalid function pointer");
hasInvalid = true;
ExecutionState *free = &state;
bool hasInvalid = false, first = true;

/* XXX This is wasteful, no need to do a full evaluate since we
have already got a value. But in the end the caches should
handle it for us, albeit with some overhead. */
do {
v = optimizer.optimizeExpr(v, true);
ref<ConstantExpr> value;
bool success = solver->getValue(free->constraints.cs(), v, value,
free->queryMetaData);
assert(success && "FIXME: Unhandled solver failure");
(void)success;
StatePair res =
forkInternal(*free, EqExpr::create(v, value), BranchType::Call);
if (res.first) {
uint64_t addr = value->getZExtValue();
auto it = legalFunctions.find(addr);
if (it != legalFunctions.end()) {
f = it->second;

// Don't give warning on unique resolution
if (res.second || !first)
klee_warning_once(reinterpret_cast<void *>(addr),
"resolved symbolic function pointer to: %s",
f->getName().data());

executeCall(*res.first, ki, f, arguments);
} else {
if (!hasInvalid) {
terminateStateOnExecError(state, "invalid function pointer");
hasInvalid = true;
}
}
}
}

first = false;
free = res.second;
timers.invoke();
} while (free && !haltExecution);
first = false;
free = res.second;
timers.invoke();
} while (free && !haltExecution);
}
}
break;
}
Expand Down

0 comments on commit b818f5c

Please sign in to comment.