Skip to content

Commit

Permalink
feat: Add MaxCoreSolverMemory (only for Bitwuzla)
Browse files Browse the repository at this point in the history
  • Loading branch information
@misonijnik
misonijnik committed Nov 16, 2024
1 parent ada9c9a commit 3c4ea29
Show file tree
Hide file tree
Showing 28 changed files with 135 additions and 90 deletions.
2 changes: 1 addition & 1 deletion include/klee/Solver/IncompleteSolver.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ class StagedSolverImpl : public SolverImpl {
bool &hasSolution);
SolverRunStatus getOperationStatusCode();
std::string getConstraintLog(const Query &) final;
void setCoreSolverTimeout(time::Span timeout);
void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit);
void notifyStateTermination(std::uint32_t id);
};

Expand Down
2 changes: 1 addition & 1 deletion include/klee/Solver/Solver.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,7 +191,7 @@ class Solver {
getRange(const Query &, time::Span timeout = time::Span());

virtual std::string getConstraintLog(const Query &query);
virtual void setCoreSolverTimeout(time::Span timeout);
virtual void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit);

/// @brief Notify the solver that the state with specified id has been
/// terminated
Expand Down
2 changes: 2 additions & 0 deletions include/klee/Solver/SolverCmdLine.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,8 @@ extern llvm::cl::opt<bool> LogTimedOutQueries;

extern llvm::cl::opt<std::string> MaxCoreSolverTime;

extern llvm::cl::opt<unsigned> MaxCoreSolverMemory;

extern llvm::cl::opt<bool> UseForkedCoreSolver;

extern llvm::cl::opt<bool> CoreSolverOptimizeDivides;
Expand Down
2 changes: 1 addition & 1 deletion include/klee/Solver/SolverImpl.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,7 @@ class SolverImpl {
return {};
}

virtual void setCoreSolverTimeout(time::Span) {}
virtual void setCoreSolverLimits(time::Span, unsigned) {}

virtual void notifyStateTermination(std::uint32_t id) = 0;
};
Expand Down
86 changes: 45 additions & 41 deletions lib/Core/Executor.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -543,8 +543,10 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
}

coreSolverTimeout = time::Span{MaxCoreSolverTime};
if (coreSolverTimeout)
if (coreSolverTimeout) {
UseForkedCoreSolver = true;
}
coreSolverMemoryLimit = MaxCoreSolverMemory;
std::unique_ptr<Solver> coreSolver = klee::createCoreSolver(CoreSolverToUse);
if (!coreSolver) {
klee_error("Failed to create core solver\n");
Expand Down Expand Up @@ -1358,16 +1360,18 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
condition = maxStaticPctChecks(current, condition);

time::Span timeout = coreSolverTimeout;
unsigned memoryLimit = coreSolverMemoryLimit;
if (isSeeding)
timeout *= static_cast<unsigned>(it->second.size());
solver->setTimeout(timeout);
solver->setLimits(timeout, memoryLimit);

bool shouldCheckTrueBlock = true, shouldCheckFalseBlock = true;
if (!isInternal) {
shouldCheckTrueBlock = canReachSomeTargetFromBlock(current, ifTrueBlock);
shouldCheckFalseBlock = canReachSomeTargetFromBlock(current, ifFalseBlock);
}
PartialValidity res = PartialValidity::None;

bool terminateEverything = false, success = true;
if (!shouldCheckTrueBlock) {
bool mayBeFalse = false;
Expand Down Expand Up @@ -1402,7 +1406,7 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
success = solver->evaluate(current.constraints.cs(), condition, res,
current.queryMetaData);
}
solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);
if (!success) {
current.pc = current.prevPC;
terminateStateOnSolverError(current, "Query timed out (fork).");
Expand Down Expand Up @@ -1614,11 +1618,11 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
siie = it->second.end();
siit != siie; ++siit) {
bool res;
solver->setTimeout(coreSolverTimeout);
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
bool success = solver->mustBeFalse(state.constraints.cs(),
siit->assignment.evaluate(condition),
res, state.queryMetaData);
solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);
assert(success && "FIXME: Unhandled solver failure");
(void)success;
if (res) {
Expand Down Expand Up @@ -1687,9 +1691,9 @@ void Executor::bindArgument(KFunction *kf, unsigned index,

ref<Expr> Executor::toUnique(const ExecutionState &state, ref<Expr> e) {
ref<Expr> result = e;
solver->setTimeout(coreSolverTimeout);
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
solver->tryGetUnique(state.constraints.cs(), e, result, state.queryMetaData);
solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);
return result;
}

Expand Down Expand Up @@ -5493,11 +5497,11 @@ void Executor::executeAlloc(ExecutionState &state, ref<Expr> size, bool isLocal,
/* If size greater then upper bound for size, then we will follow
the malloc semantic and return NULL. Otherwise continue execution. */
PartialValidity inBounds;
solver->setTimeout(coreSolverTimeout);
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
bool success =
solver->evaluate(state.constraints.cs(), upperBoundSizeConstraint,
inBounds, state.queryMetaData);
solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);
if (!success) {
terminateStateOnSolverError(state, "Query timed out (resolve)");
return;
Expand Down Expand Up @@ -5798,21 +5802,21 @@ bool Executor::computeSizes(
objects = constraints.gatherSymcretizedArrays();
findObjects(symbolicSizesSum, objects);

solver->setTimeout(coreSolverTimeout);
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
bool success = solver->getResponse(
constraints,
UgtExpr::create(symbolicSizesSum,
ConstantExpr::create(SymbolicAllocationThreshold,
symbolicSizesSum->getWidth())),
response, metaData);
solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);

if (!response->tryGetInitialValuesFor(objects, values)) {
/* Receive model with a smallest sum as possible. */
solver->setTimeout(coreSolverTimeout);
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
success = solver->getMinimalUnsignedValue(constraints, symbolicSizesSum,
minimalSumValue, metaData);
solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);
assert(success);

/* We can simply query the solver to get value of size, but
Expand All @@ -5822,9 +5826,9 @@ bool Executor::computeSizes(
ConstraintSet minimized = constraints;
minimized.addConstraint(EqExpr::create(symbolicSizesSum, minimalSumValue));

solver->setTimeout(coreSolverTimeout);
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
success = solver->getInitialValues(minimized, objects, values, metaData);
solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);
}
return success;
}
Expand Down Expand Up @@ -6005,10 +6009,10 @@ bool Executor::resolveMemoryObjects(
if (!onlyLazyInitialize || !mayLazyInitialize) {
ResolutionList rl;

solver->setTimeout(coreSolverTimeout);
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
incomplete = state.addressSpace.resolve(state, solver.get(), basePointer,
rl, 0, coreSolverTimeout);
solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);

for (ResolutionList::iterator i = rl.begin(), ie = rl.end(); i != ie;
++i) {
Expand All @@ -6023,10 +6027,10 @@ bool Executor::resolveMemoryObjects(
}

if (mayLazyInitialize) {
solver->setTimeout(coreSolverTimeout);
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
bool success = solver->mayBeTrue(state.constraints.cs(), checkOutOfBounds,
mayLazyInitialize, state.queryMetaData);
solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);
if (!success) {
return false;
} else if (mayLazyInitialize) {
Expand Down Expand Up @@ -6091,10 +6095,10 @@ bool Executor::checkResolvedMemoryObjects(
.simplified;

PartialValidity result;
solver->setTimeout(coreSolverTimeout);
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
bool success = solver->evaluate(state.constraints.cs(), inBounds, result,
state.queryMetaData);
solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);
if (!success) {
return false;
}
Expand Down Expand Up @@ -6155,10 +6159,10 @@ bool Executor::checkResolvedMemoryObjects(
.simplified;

bool mayBeInBounds;
solver->setTimeout(coreSolverTimeout);
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
bool success = solver->mayBeTrue(state.constraints.cs(), inBounds,
mayBeInBounds, state.queryMetaData);
solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);
if (!success) {
return false;
}
Expand All @@ -6180,10 +6184,10 @@ bool Executor::checkResolvedMemoryObjects(
}

if (mayBeOutOfBound) {
solver->setTimeout(coreSolverTimeout);
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
bool success = solver->mayBeTrue(state.constraints.cs(), checkOutOfBounds,
mayBeOutOfBound, state.queryMetaData);
solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);
if (!success) {
return false;
}
Expand All @@ -6210,10 +6214,10 @@ bool Executor::makeGuard(ExecutionState &state,
}
}

solver->setTimeout(coreSolverTimeout);
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
bool success = solver->mayBeTrue(state.constraints.cs(), guard, mayBeInBounds,
state.queryMetaData);
solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);
if (!success) {
return false;
}
Expand Down Expand Up @@ -6318,7 +6322,7 @@ void Executor::executeMemoryOperation(
idFastResult = *state->resolvedPointers[base].begin();
} else {
ObjectPair idFastOp;
solver->setTimeout(coreSolverTimeout);
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);

if (!state->addressSpace.resolveOne(*state, solver.get(), address, idFastOp,
success, haltExecution)) {
Expand All @@ -6327,7 +6331,7 @@ void Executor::executeMemoryOperation(
cast<ConstantPointerExpr>(address), idFastOp);
}

solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);

if (success) {
idFastResult = idFastOp.first;
Expand All @@ -6352,16 +6356,16 @@ void Executor::executeMemoryOperation(
.simplified;

ref<SolverResponse> response;
solver->setTimeout(coreSolverTimeout);
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
bool success = solver->getResponse(state->constraints.cs(), inBounds,
response, state->queryMetaData);
solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);
if (!success) {
state->pc = state->prevPC;
terminateStateOnSolverError(*state, "Query timed out (bounds check).");
return;
}
solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);

bool mustBeInBounds = !isa<InvalidResponse>(response);
if (mustBeInBounds) {
Expand Down Expand Up @@ -6414,10 +6418,10 @@ void Executor::executeMemoryOperation(
allLeafsAreConstant(address)) {
ObjectPair idFastOp;

solver->setTimeout(coreSolverTimeout);
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
state->addressSpace.resolveOne(*state, solver.get(), basePointer, idFastOp,
success, haltExecution);
solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);

if (!success) {
terminateStateOnTargetError(*state, ReachWithError::UseAfterFree);
Expand Down Expand Up @@ -6684,11 +6688,11 @@ ref<const MemoryObject> Executor::lazyInitializeObject(
sizeExpr, Expr::createPointer(MaxSymbolicAllocationSize));
}
bool mayBeInBounds;
solver->setTimeout(coreSolverTimeout);
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
bool success = solver->mayBeTrue(state.constraints.cs(),
AndExpr::create(lowerBound, upperBound),
mayBeInBounds, state.queryMetaData);
solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);
if (!success) {
return nullptr;
}
Expand Down Expand Up @@ -7430,7 +7434,7 @@ bool isMakeSymbolicSymbol(const klee::Symbolic &symb) {
}

bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
solver->setTimeout(coreSolverTimeout);
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);

PathConstraints extendedConstraints(state.constraints);

Expand Down Expand Up @@ -7504,11 +7508,11 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
std::vector<const Array *> objects(objectSet.begin(), objectSet.end());

ref<SolverResponse> response;
solver->setTimeout(coreSolverTimeout);
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
bool success =
solver->getResponse(extendedConstraints.cs(), Expr::createFalse(),
response, state.queryMetaData);
solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);
if (!success || !isa<InvalidResponse>(response)) {
klee_warning("unable to compute initial values (invalid constraints?)!");
ExprPPrinter::printQuery(llvm::errs(), state.constraints.cs(),
Expand Down Expand Up @@ -7588,14 +7592,14 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {

ref<Expr> concretizationCondition = Expr::createFalse();
for (const auto &concretization : concretizations) {
solver->setTimeout(coreSolverTimeout);
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
success = solver->getResponse(
extendedConstraints.cs(),
OrExpr::create(Expr::createIsZero(EqExpr::create(
concretization.first, concretization.second)),
concretizationCondition),
response, state.queryMetaData);
solver->setTimeout(time::Span());
solver->setLimits(time::Span(), 0);

if (auto invalidResponse = dyn_cast<InvalidResponse>(response)) {
concretizationCondition =
Expand Down
4 changes: 4 additions & 0 deletions lib/Core/Executor.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -224,6 +224,10 @@ class Executor : public Interpreter {
/// (e.g. for a single STP query)
time::Span coreSolverTimeout;

/// The soft maximum memory to allow for a core SMT-sovler to use.
/// (e.g. for a single STP query)
unsigned coreSolverMemoryLimit;

/// Maximum time to allow for a single instruction.
time::Span maxInstructionTime;

Expand Down
4 changes: 3 additions & 1 deletion lib/Core/TimingSolver.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,9 @@ class TimingSolver {
: solver(std::move(solver)), optimizer(optimizer),
simplifyExprs(_simplifyExprs) {}

void setTimeout(time::Span t) { solver->setCoreSolverTimeout(t); }
void setLimits(time::Span t, unsigned m) {
solver->setCoreSolverLimits(t, m);
}

std::string getConstraintLog(const Query &query) {
return solver->getConstraintLog(query);
Expand Down
7 changes: 4 additions & 3 deletions lib/Solver/AlphaEquivalenceSolver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ class AlphaEquivalenceSolver : public SolverImpl {
bool &isValid);
SolverRunStatus getOperationStatusCode();
std::string getConstraintLog(const Query &);
void setCoreSolverTimeout(time::Span timeout);
void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit);
void notifyStateTermination(std::uint32_t id);
ValidityCore changeVersion(const ValidityCore &validityCore,
AlphaBuilder &builder);
Expand Down Expand Up @@ -213,8 +213,9 @@ std::string AlphaEquivalenceSolver::getConstraintLog(const Query &query) {
return solver->impl->getConstraintLog(query);
}

void AlphaEquivalenceSolver::setCoreSolverTimeout(time::Span timeout) {
solver->impl->setCoreSolverTimeout(timeout);
void AlphaEquivalenceSolver::setCoreSolverLimits(time::Span timeout,
unsigned memoryLimit) {
solver->impl->setCoreSolverLimits(timeout, memoryLimit);
}

void AlphaEquivalenceSolver::notifyStateTermination(std::uint32_t id) {
Expand Down
Loading

0 comments on commit 3c4ea29

Please sign in to comment.