Skip to content

Commit

Permalink
Fix after rebase 2
Browse files Browse the repository at this point in the history
  • Loading branch information
ladisgin committed Nov 17, 2023
1 parent b818f5c commit 26f93a7
Show file tree
Hide file tree
Showing 2 changed files with 33 additions and 24 deletions.
53 changes: 32 additions & 21 deletions lib/Core/Executor.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -609,21 +609,28 @@ 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 != "") {
// prevent elimination of the function
auto f = kmodule->module->getFunction(FunctionCallReproduce);
if (f)
preservedFunctions.push_back(FunctionCallReproduce.c_str());
}

// prevent elimination of the preservedFunctions functions
for (auto pf : preservedFunctions) {
auto f = kmodule->module->getFunction(pf);
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 @@ -2937,18 +2944,22 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
} else {
ref<Expr> v = eval(ki, 0, state).value;

if (!isa<ConstantExpr>(v) && interpreterOpts.Mock == MockPolicy::Failed) {
if (ki->inst->getType()->isSized()) {
prepareMockValue(state, "mockExternResult", ki);
}
} else {
ExecutionState *free = &state;
bool hasInvalid = false, first = 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 {
if (!isa<ConstantExpr>(v) &&
interpreterOpts.Mock == MockPolicy::Failed) {
if (ki->inst->getType()->isSized()) {
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,
Expand Down Expand Up @@ -2981,8 +2992,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
first = false;
free = res.second;
timers.invoke();
} while (free && !haltExecution);
}
}
} while (free && !haltExecution);
}
break;
}
Expand Down Expand Up @@ -6073,10 +6084,10 @@ void Executor::executeMemoryOperation(

ref<SolverResponse> response;
solver->setTimeout(coreSolverTimeout);
bool solverResponse = solver->getResponse(state->constraints.cs(), inBounds,
response, state->queryMetaData);
bool success = solver->getResponse(state->constraints.cs(), inBounds,
response, state->queryMetaData);
solver->setTimeout(time::Span());
if (!solverResponse) {
if (!success) {
state->pc = state->prevPC;
terminateStateOnSolverError(*state, "Query timed out (bounds check).");
return;
Expand Down
4 changes: 1 addition & 3 deletions lib/Module/Annotation.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -92,9 +92,7 @@ Deref::Deref(const std::string &str) : Unknown(str) {}
Kind Deref::getKind() const { return Kind::Deref; }

const std::map<std::string, InitNull::Type> initNullTypeMap = {
{"maybe", InitNull::Type::MAYBE},
{"must", InitNull::Type::MUST}
};
{"maybe", InitNull::Type::MAYBE}, {"must", InitNull::Type::MUST}};

InitNull::InitNull(const std::string &str) : Unknown(str) {
if (!rawValue.empty()) {
Expand Down

0 comments on commit 26f93a7

Please sign in to comment.