Skip to content

Commit a87b4fa

Browse files
misonijnikmisonijnik
committed
feat: Add MaxCoreSolverMemory (only for Bitwuzla)
1 parent ceb6f98 commit a87b4fa

28 files changed

+136
-90
lines changed

Diff for: ‎include/klee/Solver/IncompleteSolver.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -79,7 +79,7 @@ class StagedSolverImpl : public SolverImpl {
7979
bool &hasSolution);
8080
SolverRunStatus getOperationStatusCode();
8181
std::string getConstraintLog(const Query &) final;
82-
void setCoreSolverTimeout(time::Span timeout);
82+
void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit);
8383
void notifyStateTermination(std::uint32_t id);
8484
};
8585

Diff for: ‎include/klee/Solver/Solver.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -191,7 +191,7 @@ class Solver {
191191
getRange(const Query &, time::Span timeout = time::Span());
192192

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

196196
/// @brief Notify the solver that the state with specified id has been
197197
/// terminated

Diff for: ‎include/klee/Solver/SolverCmdLine.h

+2
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,8 @@ extern llvm::cl::opt<bool> LogTimedOutQueries;
4141

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

44+
extern llvm::cl::opt<unsigned> MaxCoreSolverMemory;
45+
4446
extern llvm::cl::opt<bool> UseForkedCoreSolver;
4547

4648
extern llvm::cl::opt<bool> CoreSolverOptimizeDivides;

Diff for: ‎include/klee/Solver/SolverImpl.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -120,7 +120,7 @@ class SolverImpl {
120120
return {};
121121
}
122122

123-
virtual void setCoreSolverTimeout(time::Span) {}
123+
virtual void setCoreSolverLimits(time::Span, unsigned) {}
124124

125125
virtual void notifyStateTermination(std::uint32_t id) = 0;
126126
};

Diff for: ‎lib/Core/Executor.cpp

+45-41
Original file line numberDiff line numberDiff line change
@@ -543,8 +543,10 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
543543
}
544544

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

13601362
time::Span timeout = coreSolverTimeout;
1363+
unsigned memoryLimit = coreSolverMemoryLimit;
13611364
if (isSeeding)
13621365
timeout *= static_cast<unsigned>(it->second.size());
1363-
solver->setTimeout(timeout);
1366+
solver->setLimits(timeout, memoryLimit);
13641367

13651368
bool shouldCheckTrueBlock = true, shouldCheckFalseBlock = true;
13661369
if (!isInternal) {
13671370
shouldCheckTrueBlock = canReachSomeTargetFromBlock(current, ifTrueBlock);
13681371
shouldCheckFalseBlock = canReachSomeTargetFromBlock(current, ifFalseBlock);
13691372
}
13701373
PartialValidity res = PartialValidity::None;
1374+
13711375
bool terminateEverything = false, success = true;
13721376
if (!shouldCheckTrueBlock) {
13731377
bool mayBeFalse = false;
@@ -1402,7 +1406,7 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
14021406
success = solver->evaluate(current.constraints.cs(), condition, res,
14031407
current.queryMetaData);
14041408
}
1405-
solver->setTimeout(time::Span());
1409+
solver->setLimits(time::Span(), 0);
14061410
if (!success) {
14071411
current.pc = current.prevPC;
14081412
terminateStateOnSolverError(current, "Query timed out (fork).");
@@ -1614,11 +1618,11 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
16141618
siie = it->second.end();
16151619
siit != siie; ++siit) {
16161620
bool res;
1617-
solver->setTimeout(coreSolverTimeout);
1621+
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
16181622
bool success = solver->mustBeFalse(state.constraints.cs(),
16191623
siit->assignment.evaluate(condition),
16201624
res, state.queryMetaData);
1621-
solver->setTimeout(time::Span());
1625+
solver->setLimits(time::Span(), 0);
16221626
assert(success && "FIXME: Unhandled solver failure");
16231627
(void)success;
16241628
if (res) {
@@ -1687,9 +1691,9 @@ void Executor::bindArgument(KFunction *kf, unsigned index,
16871691

16881692
ref<Expr> Executor::toUnique(const ExecutionState &state, ref<Expr> e) {
16891693
ref<Expr> result = e;
1690-
solver->setTimeout(coreSolverTimeout);
1694+
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
16911695
solver->tryGetUnique(state.constraints.cs(), e, result, state.queryMetaData);
1692-
solver->setTimeout(time::Span());
1696+
solver->setLimits(time::Span(), 0);
16931697
return result;
16941698
}
16951699

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

5801-
solver->setTimeout(coreSolverTimeout);
5805+
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
58025806
bool success = solver->getResponse(
58035807
constraints,
58045808
UgtExpr::create(symbolicSizesSum,
58055809
ConstantExpr::create(SymbolicAllocationThreshold,
58065810
symbolicSizesSum->getWidth())),
58075811
response, metaData);
5808-
solver->setTimeout(time::Span());
5812+
solver->setLimits(time::Span(), 0);
58095813

58105814
if (!response->tryGetInitialValuesFor(objects, values)) {
58115815
/* Receive model with a smallest sum as possible. */
5812-
solver->setTimeout(coreSolverTimeout);
5816+
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
58135817
success = solver->getMinimalUnsignedValue(constraints, symbolicSizesSum,
58145818
minimalSumValue, metaData);
5815-
solver->setTimeout(time::Span());
5819+
solver->setLimits(time::Span(), 0);
58165820
assert(success);
58175821

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

5825-
solver->setTimeout(coreSolverTimeout);
5829+
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
58265830
success = solver->getInitialValues(minimized, objects, values, metaData);
5827-
solver->setTimeout(time::Span());
5831+
solver->setLimits(time::Span(), 0);
58285832
}
58295833
return success;
58305834
}
@@ -6005,10 +6009,10 @@ bool Executor::resolveMemoryObjects(
60056009
if (!onlyLazyInitialize || !mayLazyInitialize) {
60066010
ResolutionList rl;
60076011

6008-
solver->setTimeout(coreSolverTimeout);
6012+
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
60096013
incomplete = state.addressSpace.resolve(state, solver.get(), basePointer,
60106014
rl, 0, coreSolverTimeout);
6011-
solver->setTimeout(time::Span());
6015+
solver->setLimits(time::Span(), 0);
60126016

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

60256029
if (mayLazyInitialize) {
6026-
solver->setTimeout(coreSolverTimeout);
6030+
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
60276031
bool success = solver->mayBeTrue(state.constraints.cs(), checkOutOfBounds,
60286032
mayLazyInitialize, state.queryMetaData);
6029-
solver->setTimeout(time::Span());
6033+
solver->setLimits(time::Span(), 0);
60306034
if (!success) {
60316035
return false;
60326036
} else if (mayLazyInitialize) {
@@ -6091,10 +6095,10 @@ bool Executor::checkResolvedMemoryObjects(
60916095
.simplified;
60926096

60936097
PartialValidity result;
6094-
solver->setTimeout(coreSolverTimeout);
6098+
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
60956099
bool success = solver->evaluate(state.constraints.cs(), inBounds, result,
60966100
state.queryMetaData);
6097-
solver->setTimeout(time::Span());
6101+
solver->setLimits(time::Span(), 0);
60986102
if (!success) {
60996103
return false;
61006104
}
@@ -6155,10 +6159,10 @@ bool Executor::checkResolvedMemoryObjects(
61556159
.simplified;
61566160

61576161
bool mayBeInBounds;
6158-
solver->setTimeout(coreSolverTimeout);
6162+
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
61596163
bool success = solver->mayBeTrue(state.constraints.cs(), inBounds,
61606164
mayBeInBounds, state.queryMetaData);
6161-
solver->setTimeout(time::Span());
6165+
solver->setLimits(time::Span(), 0);
61626166
if (!success) {
61636167
return false;
61646168
}
@@ -6180,10 +6184,10 @@ bool Executor::checkResolvedMemoryObjects(
61806184
}
61816185

61826186
if (mayBeOutOfBound) {
6183-
solver->setTimeout(coreSolverTimeout);
6187+
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
61846188
bool success = solver->mayBeTrue(state.constraints.cs(), checkOutOfBounds,
61856189
mayBeOutOfBound, state.queryMetaData);
6186-
solver->setTimeout(time::Span());
6190+
solver->setLimits(time::Span(), 0);
61876191
if (!success) {
61886192
return false;
61896193
}
@@ -6210,10 +6214,10 @@ bool Executor::makeGuard(ExecutionState &state,
62106214
}
62116215
}
62126216

6213-
solver->setTimeout(coreSolverTimeout);
6217+
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
62146218
bool success = solver->mayBeTrue(state.constraints.cs(), guard, mayBeInBounds,
62156219
state.queryMetaData);
6216-
solver->setTimeout(time::Span());
6220+
solver->setLimits(time::Span(), 0);
62176221
if (!success) {
62186222
return false;
62196223
}
@@ -6318,7 +6322,7 @@ void Executor::executeMemoryOperation(
63186322
idFastResult = *state->resolvedPointers[base].begin();
63196323
} else {
63206324
ObjectPair idFastOp;
6321-
solver->setTimeout(coreSolverTimeout);
6325+
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
63226326

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

6330-
solver->setTimeout(time::Span());
6334+
solver->setLimits(time::Span(), 0);
63316335

63326336
if (success) {
63336337
idFastResult = idFastOp.first;
@@ -6352,16 +6356,16 @@ void Executor::executeMemoryOperation(
63526356
.simplified;
63536357

63546358
ref<SolverResponse> response;
6355-
solver->setTimeout(coreSolverTimeout);
6359+
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
63566360
bool success = solver->getResponse(state->constraints.cs(), inBounds,
63576361
response, state->queryMetaData);
6358-
solver->setTimeout(time::Span());
6362+
solver->setLimits(time::Span(), 0);
63596363
if (!success) {
63606364
state->pc = state->prevPC;
63616365
terminateStateOnSolverError(*state, "Query timed out (bounds check).");
63626366
return;
63636367
}
6364-
solver->setTimeout(time::Span());
6368+
solver->setLimits(time::Span(), 0);
63656369

63666370
bool mustBeInBounds = !isa<InvalidResponse>(response);
63676371
if (mustBeInBounds) {
@@ -6414,10 +6418,10 @@ void Executor::executeMemoryOperation(
64146418
allLeafsAreConstant(address)) {
64156419
ObjectPair idFastOp;
64166420

6417-
solver->setTimeout(coreSolverTimeout);
6421+
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
64186422
state->addressSpace.resolveOne(*state, solver.get(), basePointer, idFastOp,
64196423
success, haltExecution);
6420-
solver->setTimeout(time::Span());
6424+
solver->setLimits(time::Span(), 0);
64216425

64226426
if (!success) {
64236427
terminateStateOnTargetError(*state, ReachWithError::UseAfterFree);
@@ -6684,11 +6688,11 @@ ref<const MemoryObject> Executor::lazyInitializeObject(
66846688
sizeExpr, Expr::createPointer(MaxSymbolicAllocationSize));
66856689
}
66866690
bool mayBeInBounds;
6687-
solver->setTimeout(coreSolverTimeout);
6691+
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
66886692
bool success = solver->mayBeTrue(state.constraints.cs(),
66896693
AndExpr::create(lowerBound, upperBound),
66906694
mayBeInBounds, state.queryMetaData);
6691-
solver->setTimeout(time::Span());
6695+
solver->setLimits(time::Span(), 0);
66926696
if (!success) {
66936697
return nullptr;
66946698
}
@@ -7430,7 +7434,7 @@ bool isMakeSymbolicSymbol(const klee::Symbolic &symb) {
74307434
}
74317435

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

74357439
PathConstraints extendedConstraints(state.constraints);
74367440

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

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

75897593
ref<Expr> concretizationCondition = Expr::createFalse();
75907594
for (const auto &concretization : concretizations) {
7591-
solver->setTimeout(coreSolverTimeout);
7595+
solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
75927596
success = solver->getResponse(
75937597
extendedConstraints.cs(),
75947598
OrExpr::create(Expr::createIsZero(EqExpr::create(
75957599
concretization.first, concretization.second)),
75967600
concretizationCondition),
75977601
response, state.queryMetaData);
7598-
solver->setTimeout(time::Span());
7602+
solver->setLimits(time::Span(), 0);
75997603

76007604
if (auto invalidResponse = dyn_cast<InvalidResponse>(response)) {
76017605
concretizationCondition =

Diff for: ‎lib/Core/Executor.h

+4
Original file line numberDiff line numberDiff line change
@@ -224,6 +224,10 @@ class Executor : public Interpreter {
224224
/// (e.g. for a single STP query)
225225
time::Span coreSolverTimeout;
226226

227+
/// The soft maximum memory to allow for a core SMT-sovler to use.
228+
/// (e.g. for a single STP query)
229+
unsigned coreSolverMemoryLimit;
230+
227231
/// Maximum time to allow for a single instruction.
228232
time::Span maxInstructionTime;
229233

Diff for: ‎lib/Core/TimingSolver.h

+3-1
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,9 @@ class TimingSolver {
4444
: solver(std::move(solver)), optimizer(optimizer),
4545
simplifyExprs(_simplifyExprs) {}
4646

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

4951
std::string getConstraintLog(const Query &query) {
5052
return solver->getConstraintLog(query);

Diff for: ‎lib/Solver/AlphaEquivalenceSolver.cpp

+4-3
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ class AlphaEquivalenceSolver : public SolverImpl {
4141
bool &isValid);
4242
SolverRunStatus getOperationStatusCode();
4343
std::string getConstraintLog(const Query &);
44-
void setCoreSolverTimeout(time::Span timeout);
44+
void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit);
4545
void notifyStateTermination(std::uint32_t id);
4646
ValidityCore changeVersion(const ValidityCore &validityCore,
4747
AlphaBuilder &builder);
@@ -213,8 +213,9 @@ std::string AlphaEquivalenceSolver::getConstraintLog(const Query &query) {
213213
return solver->impl->getConstraintLog(query);
214214
}
215215

216-
void AlphaEquivalenceSolver::setCoreSolverTimeout(time::Span timeout) {
217-
solver->impl->setCoreSolverTimeout(timeout);
216+
void AlphaEquivalenceSolver::setCoreSolverLimits(time::Span timeout,
217+
unsigned memoryLimit) {
218+
solver->impl->setCoreSolverLimits(timeout, memoryLimit);
218219
}
219220

220221
void AlphaEquivalenceSolver::notifyStateTermination(std::uint32_t id) {

0 commit comments

Comments
 (0)