From 8a0f1af7500e10dadd97300f242424917d2e9902 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Mon, 1 Apr 2019 14:08:43 +0100 Subject: Use constraint sets and separate metadata for timing solver invocation Decouple ExecutionState from TimingSolver Instead of providing an execution state to the timing solver use a set of constraints and an additional object for metadata. Fixes: * correct accounting of metadata to a specific state * accounting of all solver invocations (e.g. solver-getRange was not accounted) * allows to invoke the solver without a state (avoids costly copying of states/constraints) --- lib/Core/AddressSpace.cpp | 40 ++++++++------ lib/Core/ExecutionState.cpp | 1 - lib/Core/ExecutionState.h | 5 +- lib/Core/Executor.cpp | 103 +++++++++++++++++++++++------------- lib/Core/ExecutorTimers.cpp | 0 lib/Core/Memory.cpp | 4 +- lib/Core/Memory.h | 3 +- lib/Core/Searcher.cpp | 4 +- lib/Core/SeedInfo.cpp | 42 ++++++++------- lib/Core/SpecialFunctionHandler.cpp | 32 +++++------ lib/Core/TimingSolver.cpp | 81 ++++++++++++++-------------- lib/Core/TimingSolver.h | 78 ++++++++++++++------------- 12 files changed, 222 insertions(+), 171 deletions(-) delete mode 100644 lib/Core/ExecutorTimers.cpp (limited to 'lib') diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp index 82913aa7..f3462ca1 100644 --- a/lib/Core/AddressSpace.cpp +++ b/lib/Core/AddressSpace.cpp @@ -9,6 +9,7 @@ #include "AddressSpace.h" +#include "ExecutionState.h" #include "Memory.h" #include "TimingSolver.h" @@ -87,7 +88,7 @@ bool AddressSpace::resolveOne(ExecutionState &state, // try cheap search, will succeed for any inbounds pointer ref cex; - if (!solver->getValue(state, address, cex)) + if (!solver->getValue(state.constraints, address, cex, state.queryMetaData)) return false; uint64_t example = cex->getZExtValue(); MemoryObject hack(example); @@ -115,8 +116,9 @@ bool AddressSpace::resolveOne(ExecutionState &state, const auto &mo = oi->first; bool mayBeTrue; - if (!solver->mayBeTrue(state, - mo->getBoundsCheckPointer(address), mayBeTrue)) + if (!solver->mayBeTrue(state.constraints, + mo->getBoundsCheckPointer(address), mayBeTrue, + state.queryMetaData)) return false; if (mayBeTrue) { result.first = oi->first; @@ -125,9 +127,9 @@ bool AddressSpace::resolveOne(ExecutionState &state, return true; } else { bool mustBeTrue; - if (!solver->mustBeTrue(state, + if (!solver->mustBeTrue(state.constraints, UgeExpr::create(address, mo->getBaseExpr()), - mustBeTrue)) + mustBeTrue, state.queryMetaData)) return false; if (mustBeTrue) break; @@ -139,18 +141,18 @@ bool AddressSpace::resolveOne(ExecutionState &state, const auto &mo = oi->first; bool mustBeTrue; - if (!solver->mustBeTrue(state, + if (!solver->mustBeTrue(state.constraints, UltExpr::create(address, mo->getBaseExpr()), - mustBeTrue)) + mustBeTrue, state.queryMetaData)) return false; if (mustBeTrue) { break; } else { bool mayBeTrue; - if (!solver->mayBeTrue(state, - mo->getBoundsCheckPointer(address), - mayBeTrue)) + if (!solver->mayBeTrue(state.constraints, + mo->getBoundsCheckPointer(address), mayBeTrue, + state.queryMetaData)) return false; if (mayBeTrue) { result.first = oi->first; @@ -176,7 +178,8 @@ int AddressSpace::checkPointerInObject(ExecutionState &state, const MemoryObject *mo = op.first; ref inBounds = mo->getBoundsCheckPointer(p); bool mayBeTrue; - if (!solver->mayBeTrue(state, inBounds, mayBeTrue)) { + if (!solver->mayBeTrue(state.constraints, inBounds, mayBeTrue, + state.queryMetaData)) { return 1; } @@ -187,7 +190,8 @@ int AddressSpace::checkPointerInObject(ExecutionState &state, auto size = rl.size(); if (size == 1) { bool mustBeTrue; - if (!solver->mustBeTrue(state, inBounds, mustBeTrue)) + if (!solver->mustBeTrue(state.constraints, inBounds, mustBeTrue, + state.queryMetaData)) return 1; if (mustBeTrue) return 0; @@ -227,7 +231,7 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver, // just get this by inspection of the expr. ref cex; - if (!solver->getValue(state, p, cex)) + if (!solver->getValue(state.constraints, p, cex, state.queryMetaData)) return true; uint64_t example = cex->getZExtValue(); MemoryObject hack(example); @@ -254,8 +258,9 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver, return incomplete ? true : false; bool mustBeTrue; - if (!solver->mustBeTrue(state, UgeExpr::create(p, mo->getBaseExpr()), - mustBeTrue)) + if (!solver->mustBeTrue(state.constraints, + UgeExpr::create(p, mo->getBaseExpr()), mustBeTrue, + state.queryMetaData)) return true; if (mustBeTrue) break; @@ -268,8 +273,9 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver, return true; bool mustBeTrue; - if (!solver->mustBeTrue(state, UltExpr::create(p, mo->getBaseExpr()), - mustBeTrue)) + if (!solver->mustBeTrue(state.constraints, + UltExpr::create(p, mo->getBaseExpr()), mustBeTrue, + state.queryMetaData)) return true; if (mustBeTrue) break; diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 0b848f41..5e95ca9b 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -101,7 +101,6 @@ ExecutionState::ExecutionState(const ExecutionState& state): depth(state.depth), addressSpace(state.addressSpace), constraints(state.constraints), - queryCost(state.queryCost), pathOS(state.pathOS), symPathOS(state.symPathOS), coveredLines(state.coveredLines), diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 397b2364..03cad916 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -17,6 +17,7 @@ #include "klee/Expr/Constraints.h" #include "klee/Expr/Expr.h" #include "klee/Module/KInstIterator.h" +#include "klee/Solver/Solver.h" #include "klee/System/Time.h" #include @@ -96,8 +97,8 @@ public: /// Statistics and information - /// @brief Costs for all queries issued for this state, in seconds - mutable time::Span queryCost; + /// @brief Metadata utilized and collected by solvers for this state + mutable SolverQueryMetaData queryMetaData; /// @brief History of complete path: represents branches taken to /// reach/create this state (both concrete and symbolic) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index ceefc710..041a4e6a 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -915,9 +915,9 @@ void Executor::branch(ExecutionState &state, unsigned i; for (i=0; i res; - bool success = - solver->getValue(state, siit->assignment.evaluate(conditions[i]), - res); + bool success = solver->getValue( + state.constraints, siit->assignment.evaluate(conditions[i]), res, + state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; if (res->isTrue()) @@ -974,8 +974,9 @@ Executor::fork(ExecutionState ¤t, ref condition, bool isInternal) { (MaxStaticCPForkPct<1. && cpn && (cpn->statistics.getValue(stats::solverTime) > stats::solverTime*MaxStaticCPSolvePct))) { - ref value; - bool success = solver->getValue(current, condition, value); + ref value; + bool success = solver->getValue(current.constraints, condition, value, + current.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; addConstraint(current, EqExpr::create(value, condition)); @@ -987,7 +988,8 @@ Executor::fork(ExecutionState ¤t, ref condition, bool isInternal) { if (isSeeding) timeout *= static_cast(it->second.size()); solver->setTimeout(timeout); - bool success = solver->evaluate(current, condition, res); + bool success = solver->evaluate(current.constraints, condition, res, + current.queryMetaData); solver->setTimeout(time::Span()); if (!success) { current.pc = current.prevPC; @@ -1041,8 +1043,9 @@ Executor::fork(ExecutionState ¤t, ref condition, bool isInternal) { for (std::vector::iterator siit = it->second.begin(), siie = it->second.end(); siit != siie; ++siit) { ref res; - bool success = - solver->getValue(current, siit->assignment.evaluate(condition), res); + bool success = solver->getValue(current.constraints, + siit->assignment.evaluate(condition), res, + current.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; if (res->isTrue()) { @@ -1102,8 +1105,9 @@ Executor::fork(ExecutionState ¤t, ref condition, bool isInternal) { for (std::vector::iterator siit = seeds.begin(), siie = seeds.end(); siit != siie; ++siit) { ref res; - bool success = - solver->getValue(current, siit->assignment.evaluate(condition), res); + bool success = solver->getValue(current.constraints, + siit->assignment.evaluate(condition), + res, current.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; if (res->isTrue()) { @@ -1176,8 +1180,9 @@ void Executor::addConstraint(ExecutionState &state, ref condition) { for (std::vector::iterator siit = it->second.begin(), siie = it->second.end(); siit != siie; ++siit) { bool res; - bool success = - solver->mustBeFalse(state, siit->assignment.evaluate(condition), res); + bool success = solver->mustBeFalse(state.constraints, + siit->assignment.evaluate(condition), + res, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; if (res) { @@ -1233,10 +1238,12 @@ ref Executor::toUnique(const ExecutionState &state, bool isTrue = false; e = optimizer.optimizeExpr(e, true); solver->setTimeout(coreSolverTimeout); - if (solver->getValue(state, e, value)) { + if (solver->getValue(state.constraints, e, value, state.queryMetaData)) { ref cond = EqExpr::create(e, value); cond = optimizer.optimizeExpr(cond, false); - if (solver->mustBeTrue(state, cond, isTrue) && isTrue) + if (solver->mustBeTrue(state.constraints, cond, isTrue, + state.queryMetaData) && + isTrue) result = value; } solver->setTimeout(time::Span()); @@ -1257,7 +1264,8 @@ Executor::toConstant(ExecutionState &state, return CE; ref value; - bool success = solver->getValue(state, e, value); + bool success = + solver->getValue(state.constraints, e, value, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; @@ -1286,7 +1294,8 @@ void Executor::executeGetValue(ExecutionState &state, if (it==seedMap.end() || isa(e)) { ref value; e = optimizer.optimizeExpr(e, true); - bool success = solver->getValue(state, e, value); + bool success = + solver->getValue(state.constraints, e, value, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; bindLocal(target, state, value); @@ -1297,7 +1306,8 @@ void Executor::executeGetValue(ExecutionState &state, ref cond = siit->assignment.evaluate(e); cond = optimizer.optimizeExpr(cond, true); ref value; - bool success = solver->getValue(state, cond, value); + bool success = + solver->getValue(state.constraints, cond, value, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; values.insert(value); @@ -1856,7 +1866,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { // check feasibility bool result; - bool success __attribute__ ((unused)) = solver->mayBeTrue(state, e, result); + bool success __attribute__((unused)) = + solver->mayBeTrue(state.constraints, e, result, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); if (result) { targets.push_back(d); @@ -1865,7 +1876,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { } // check errorCase feasibility bool result; - bool success __attribute__ ((unused)) = solver->mayBeTrue(state, errorCase, result); + bool success __attribute__((unused)) = solver->mayBeTrue( + state.constraints, errorCase, result, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); if (result) { expressions.push_back(errorCase); @@ -1948,7 +1960,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { // Check if control flow could take this case bool result; match = optimizer.optimizeExpr(match, false); - bool success = solver->mayBeTrue(state, match, result); + bool success = solver->mayBeTrue(state.constraints, match, result, + state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; if (result) { @@ -1976,7 +1989,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { // Check if control could take the default case defaultValue = optimizer.optimizeExpr(defaultValue, false); bool res; - bool success = solver->mayBeTrue(state, defaultValue, res); + bool success = solver->mayBeTrue(state.constraints, defaultValue, res, + state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; if (res) { @@ -2095,7 +2109,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { do { v = optimizer.optimizeExpr(v, true); ref value; - bool success = solver->getValue(*free, v, value); + bool success = + solver->getValue(free->constraints, v, value, free->queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; StatePair res = fork(*free, EqExpr::create(v, value), true); @@ -3096,12 +3111,14 @@ std::string Executor::getAddressInfo(ExecutionState &state, example = CE->getZExtValue(); } else { ref value; - bool success = solver->getValue(state, address, value); + bool success = solver->getValue(state.constraints, address, value, + state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; example = value->getZExtValue(); info << "\texample: " << example << "\n"; - std::pair< ref, ref > res = solver->getRange(state, address); + std::pair, ref> res = + solver->getRange(state.constraints, address, state.queryMetaData); info << "\trange: [" << res.first << ", " << res.second <<"]\n"; } @@ -3322,7 +3339,8 @@ void Executor::callExternalFunction(ExecutionState &state, if (ExternalCalls == ExternalCallPolicy::All) { // don't bother checking uniqueness *ai = optimizer.optimizeExpr(*ai, true); ref ce; - bool success = solver->getValue(state, *ai, ce); + bool success = + solver->getValue(state.constraints, *ai, ce, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; ce->toMemory(&args[wordIndex]); @@ -3513,7 +3531,8 @@ void Executor::executeAlloc(ExecutionState &state, size = optimizer.optimizeExpr(size, true); ref example; - bool success = solver->getValue(state, size, example); + bool success = + solver->getValue(state.constraints, size, example, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; @@ -3522,7 +3541,9 @@ void Executor::executeAlloc(ExecutionState &state, while (example->Ugt(ConstantExpr::alloc(128, W))->isTrue()) { ref tmp = example->LShr(ConstantExpr::alloc(1, W)); bool res; - bool success = solver->mayBeTrue(state, EqExpr::create(tmp, size), res); + bool success = + solver->mayBeTrue(state.constraints, EqExpr::create(tmp, size), res, + state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; if (!res) @@ -3535,13 +3556,14 @@ void Executor::executeAlloc(ExecutionState &state, if (fixedSize.second) { // Check for exactly two values ref tmp; - bool success = solver->getValue(*fixedSize.second, size, tmp); + bool success = solver->getValue(fixedSize.second->constraints, size, tmp, + fixedSize.second->queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; bool res; - success = solver->mustBeTrue(*fixedSize.second, - EqExpr::create(tmp, size), - res); + success = solver->mustBeTrue(fixedSize.second->constraints, + EqExpr::create(tmp, size), res, + fixedSize.second->queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; if (res) { @@ -3681,7 +3703,8 @@ void Executor::executeMemoryOperation(ExecutionState &state, bool inBounds; solver->setTimeout(coreSolverTimeout); - bool success = solver->mustBeTrue(state, check, inBounds); + bool success = solver->mustBeTrue(state.constraints, check, inBounds, + state.queryMetaData); solver->setTimeout(time::Span()); if (!success) { state.pc = state.prevPC; @@ -3999,7 +4022,8 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, &res) { solver->setTimeout(coreSolverTimeout); - ExecutionState tmp(state); + ConstraintSet extendedConstraints(state.constraints); + ConstraintManager cm(extendedConstraints); // Go through each byte in every test case and attempt to restrict // it to the constraints contained in cexPreferences. (Note: @@ -4015,8 +4039,9 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, for (; pi != pie; ++pi) { bool mustBeTrue; // Attempt to bound byte to constraints held in cexPreferences - bool success = solver->mustBeTrue(tmp, Expr::createIsZero(*pi), - mustBeTrue); + bool success = + solver->mustBeTrue(extendedConstraints, Expr::createIsZero(*pi), + mustBeTrue, state.queryMetaData); // If it isn't possible to constrain this particular byte in the desired // way (normally this would mean that the byte can't be constrained to // be between 0 and 127 without making the entire constraint list UNSAT) @@ -4024,7 +4049,8 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, if (!success) break; // If the particular constraint operated on in this iteration through // the loop isn't implied then add it to the list of constraints. - if (!mustBeTrue) tmp.addConstraint(*pi); + if (!mustBeTrue) + cm.addConstraint(*pi); } if (pi!=pie) break; } @@ -4033,7 +4059,8 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, std::vector objects; for (unsigned i = 0; i != state.symbolics.size(); ++i) objects.push_back(state.symbolics[i].second); - bool success = solver->getInitialValues(tmp, objects, values); + bool success = solver->getInitialValues(extendedConstraints, objects, values, + state.queryMetaData); solver->setTimeout(time::Span()); if (!success) { klee_warning("unable to compute initial values (invalid constraints?)!"); @@ -4220,7 +4247,7 @@ void Executor::dumpStates() { *os << "{"; *os << "'depth' : " << es->depth << ", "; - *os << "'queryCost' : " << es->queryCost << ", "; + *os << "'queryCost' : " << es->queryMetaData.queryCost << ", "; *os << "'coveredNew' : " << es->coveredNew << ", "; *os << "'instsSinceCovNew' : " << es->instsSinceCovNew << ", "; *os << "'md2u' : " << md2u << ", "; diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp deleted file mode 100644 index e69de29b..00000000 diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index cb40cd81..bf00ee4b 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -10,6 +10,7 @@ #include "Memory.h" #include "Context.h" +#include "ExecutionState.h" #include "MemoryManager.h" #include "klee/ADT/BitArray.h" @@ -196,7 +197,8 @@ void ObjectState::flushToConcreteStore(TimingSolver *solver, for (unsigned i = 0; i < size; i++) { if (isByteKnownSymbolic(i)) { ref ce; - bool success = solver->getValue(state, read8(i), ce); + bool success = solver->getValue(state.constraints, read8(i), ce, + state.queryMetaData); if (!success) klee_warning("Solver timed out when getting a value for external call, " "byte %p+%u will have random value", diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h index 2ab7cd22..e88d5f55 100644 --- a/lib/Core/Memory.h +++ b/lib/Core/Memory.h @@ -26,10 +26,11 @@ namespace llvm { namespace klee { +class ArrayCache; class BitArray; +class ExecutionState; class MemoryManager; class Solver; -class ArrayCache; class MemoryObject { friend class STPBuilder; diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 6b7e9e49..765784c5 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -214,7 +214,9 @@ double WeightedRandomSearcher::getWeight(ExecutionState *es) { return inv; } case QueryCost: - return (es->queryCost.toSeconds() < .1) ? 1. : 1./ es->queryCost.toSeconds(); + return (es->queryMetaData.queryCost.toSeconds() < .1) + ? 1. + : 1. / es->queryMetaData.queryCost.toSeconds(); case CoveringNew: case MinDistToUncovered: { uint64_t md2u = computeMinDistToUncovered(es->pc, diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp index d3688313..55f4ed48 100644 --- a/lib/Core/SeedInfo.cpp +++ b/lib/Core/SeedInfo.cpp @@ -62,10 +62,9 @@ KTestObject *SeedInfo::getNextInput(const MemoryObject *mo, void SeedInfo::patchSeed(const ExecutionState &state, ref condition, TimingSolver *solver) { - std::vector< ref > required(state.constraints.begin(), - state.constraints.end()); - ExecutionState tmp(required); - tmp.addConstraint(condition); + ConstraintSet required(state.constraints); + ConstraintManager cm(required); + cm.addConstraint(condition); // Try and patch direct reads first, this is likely to resolve the // problem quickly and avoids long traversal of all seed @@ -98,26 +97,29 @@ void SeedInfo::patchSeed(const ExecutionState &state, ConstantExpr::alloc(it2->second[i], Expr::Int8)); bool res; - bool success = solver->mustBeFalse(tmp, isSeed, res); + bool success = + solver->mustBeFalse(required, isSeed, res, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; if (res) { ref value; - bool success = solver->getValue(tmp, read, value); + bool success = + solver->getValue(required, read, value, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; it2->second[i] = value->getZExtValue(8); - tmp.addConstraint(EqExpr::create(read, - ConstantExpr::alloc(it2->second[i], - Expr::Int8))); + cm.addConstraint(EqExpr::create( + read, ConstantExpr::alloc(it2->second[i], Expr::Int8))); } else { - tmp.addConstraint(isSeed); + cm.addConstraint(isSeed); } } } bool res; - bool success = solver->mayBeTrue(state, assignment.evaluate(condition), res); + bool success = + solver->mayBeTrue(state.constraints, assignment.evaluate(condition), res, + state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; if (res) @@ -135,20 +137,21 @@ void SeedInfo::patchSeed(const ExecutionState &state, ConstantExpr::alloc(it->second[i], Expr::Int8)); bool res; - bool success = solver->mustBeFalse(tmp, isSeed, res); + bool success = + solver->mustBeFalse(required, isSeed, res, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; if (res) { ref value; - bool success = solver->getValue(tmp, read, value); + bool success = + solver->getValue(required, read, value, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; it->second[i] = value->getZExtValue(8); - tmp.addConstraint(EqExpr::create(read, - ConstantExpr::alloc(it->second[i], - Expr::Int8))); + cm.addConstraint(EqExpr::create( + read, ConstantExpr::alloc(it->second[i], Expr::Int8))); } else { - tmp.addConstraint(isSeed); + cm.addConstraint(isSeed); } } } @@ -156,8 +159,9 @@ void SeedInfo::patchSeed(const ExecutionState &state, #ifndef NDEBUG { bool res; - bool success = - solver->mayBeTrue(state, assignment.evaluate(condition), res); + bool success = + solver->mayBeTrue(state.constraints, assignment.evaluate(condition), + res, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; assert(res && "seed patching failed"); diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index d6429883..57f059a4 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -249,7 +249,6 @@ SpecialFunctionHandler::readStringAtAddress(ExecutionState &state, Executor::TerminateReason::User); return ""; } - const MemoryObject *mo = op.first; const ObjectState *os = op.second; @@ -430,7 +429,8 @@ void SpecialFunctionHandler::handleMemalign(ExecutionState &state, } std::pair, ref> alignmentRangeExpr = - executor.solver->getRange(state, arguments[0]); + executor.solver->getRange(state.constraints, arguments[0], + state.queryMetaData); ref alignmentExpr = alignmentRangeExpr.first; auto alignmentConstExpr = dyn_cast(alignmentExpr); @@ -464,7 +464,8 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state, e = NeExpr::create(e, ConstantExpr::create(0, e->getWidth())); bool res; - bool success __attribute__ ((unused)) = executor.solver->mustBeFalse(state, e, res); + bool success __attribute__((unused)) = executor.solver->mustBeFalse( + state.constraints, e, res, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); if (res) { if (SilentKleeAssume) { @@ -579,19 +580,20 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state, if (!isa(arguments[1])) { // FIXME: Pull into a unique value method? ref value; - bool success __attribute__ ((unused)) = executor.solver->getValue(state, arguments[1], value); + bool success __attribute__((unused)) = executor.solver->getValue( + state.constraints, arguments[1], value, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); bool res; - success = executor.solver->mustBeTrue(state, - EqExpr::create(arguments[1], value), - res); + success = executor.solver->mustBeTrue(state.constraints, + EqExpr::create(arguments[1], value), + res, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); if (res) { llvm::errs() << " == " << value; } else { llvm::errs() << " ~= " << value; - std::pair< ref, ref > res = - executor.solver->getRange(state, arguments[1]); + std::pair, ref> res = executor.solver->getRange( + state.constraints, arguments[1], state.queryMetaData); llvm::errs() << " (in [" << res.first << ", " << res.second <<"])"; } } @@ -812,12 +814,12 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state, // FIXME: Type coercion should be done consistently somewhere. bool res; - bool success __attribute__ ((unused)) = - executor.solver->mustBeTrue(*s, - EqExpr::create(ZExtExpr::create(arguments[1], - Context::get().getPointerWidth()), - mo->getSizeExpr()), - res); + bool success __attribute__((unused)) = executor.solver->mustBeTrue( + s->constraints, + EqExpr::create( + ZExtExpr::create(arguments[1], Context::get().getPointerWidth()), + mo->getSizeExpr()), + res, s->queryMetaData); assert(success && "FIXME: Unhandled solver failure"); if (res) { diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp index cc0afff8..fc31e72d 100644 --- a/lib/Core/TimingSolver.cpp +++ b/lib/Core/TimingSolver.cpp @@ -23,8 +23,9 @@ using namespace llvm; /***/ -bool TimingSolver::evaluate(const ExecutionState& state, ref expr, - Solver::Validity &result) { +bool TimingSolver::evaluate(const ConstraintSet &constraints, ref expr, + Solver::Validity &result, + SolverQueryMetaData &metaData) { // Fast path, to avoid timer and OS overhead. if (ConstantExpr *CE = dyn_cast(expr)) { result = CE->isTrue() ? Solver::True : Solver::False; @@ -34,17 +35,17 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref expr, TimerStatIncrementer timer(stats::solverTime); if (simplifyExprs) - expr = ConstraintManager::simplifyExpr(state.constraints, expr); + expr = ConstraintManager::simplifyExpr(constraints, expr); - bool success = solver->evaluate(Query(state.constraints, expr), result); + bool success = solver->evaluate(Query(constraints, expr), result); - state.queryCost += timer.delta(); + metaData.queryCost += timer.delta(); return success; } -bool TimingSolver::mustBeTrue(const ExecutionState& state, ref expr, - bool &result) { +bool TimingSolver::mustBeTrue(const ConstraintSet &constraints, ref expr, + bool &result, SolverQueryMetaData &metaData) { // Fast path, to avoid timer and OS overhead. if (ConstantExpr *CE = dyn_cast(expr)) { result = CE->isTrue() ? true : false; @@ -54,40 +55,41 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref expr, TimerStatIncrementer timer(stats::solverTime); if (simplifyExprs) - expr = ConstraintManager::simplifyExpr(state.constraints, expr); + expr = ConstraintManager::simplifyExpr(constraints, expr); - bool success = solver->mustBeTrue(Query(state.constraints, expr), result); + bool success = solver->mustBeTrue(Query(constraints, expr), result); - state.queryCost += timer.delta(); + metaData.queryCost += timer.delta(); return success; } -bool TimingSolver::mustBeFalse(const ExecutionState& state, ref expr, - bool &result) { - return mustBeTrue(state, Expr::createIsZero(expr), result); +bool TimingSolver::mustBeFalse(const ConstraintSet &constraints, ref expr, + bool &result, SolverQueryMetaData &metaData) { + return mustBeTrue(constraints, Expr::createIsZero(expr), result, metaData); } -bool TimingSolver::mayBeTrue(const ExecutionState& state, ref expr, - bool &result) { +bool TimingSolver::mayBeTrue(const ConstraintSet &constraints, ref expr, + bool &result, SolverQueryMetaData &metaData) { bool res; - if (!mustBeFalse(state, expr, res)) + if (!mustBeFalse(constraints, expr, res, metaData)) return false; result = !res; return true; } -bool TimingSolver::mayBeFalse(const ExecutionState& state, ref expr, - bool &result) { +bool TimingSolver::mayBeFalse(const ConstraintSet &constraints, ref expr, + bool &result, SolverQueryMetaData &metaData) { bool res; - if (!mustBeTrue(state, expr, res)) + if (!mustBeTrue(constraints, expr, res, metaData)) return false; result = !res; return true; } -bool TimingSolver::getValue(const ExecutionState& state, ref expr, - ref &result) { +bool TimingSolver::getValue(const ConstraintSet &constraints, ref expr, + ref &result, + SolverQueryMetaData &metaData) { // Fast path, to avoid timer and OS overhead. if (ConstantExpr *CE = dyn_cast(expr)) { result = CE; @@ -97,36 +99,37 @@ bool TimingSolver::getValue(const ExecutionState& state, ref expr, TimerStatIncrementer timer(stats::solverTime); if (simplifyExprs) - expr = ConstraintManager::simplifyExpr(state.constraints, expr); + expr = ConstraintManager::simplifyExpr(constraints, expr); - bool success = solver->getValue(Query(state.constraints, expr), result); + bool success = solver->getValue(Query(constraints, expr), result); - state.queryCost += timer.delta(); + metaData.queryCost += timer.delta(); return success; } -bool -TimingSolver::getInitialValues(const ExecutionState& state, - const std::vector - &objects, - std::vector< std::vector > - &result) { +bool TimingSolver::getInitialValues( + const ConstraintSet &constraints, const std::vector &objects, + std::vector> &result, + SolverQueryMetaData &metaData) { if (objects.empty()) return true; TimerStatIncrementer timer(stats::solverTime); - bool success = solver->getInitialValues(Query(state.constraints, - ConstantExpr::alloc(0, Expr::Bool)), - objects, result); - - state.queryCost += timer.delta(); - + bool success = solver->getInitialValues( + Query(constraints, ConstantExpr::alloc(0, Expr::Bool)), objects, result); + + metaData.queryCost += timer.delta(); + return success; } -std::pair< ref, ref > -TimingSolver::getRange(const ExecutionState& state, ref expr) { - return solver->getRange(Query(state.constraints, expr)); +std::pair, ref> +TimingSolver::getRange(const ConstraintSet &constraints, ref expr, + SolverQueryMetaData &metaData) { + TimerStatIncrementer timer(stats::solverTime); + auto result = solver->getRange(Query(constraints, expr)); + metaData.queryCost += timer.delta(); + return result; } diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h index 9470bd31..1f179e54 100644 --- a/lib/Core/TimingSolver.h +++ b/lib/Core/TimingSolver.h @@ -19,54 +19,58 @@ #include namespace klee { - class ExecutionState; - class Solver; - - /// TimingSolver - A simple class which wraps a solver and handles - /// tracking the statistics that we care about. - class TimingSolver { - public: - std::unique_ptr solver; - bool simplifyExprs; - - public: - /// TimingSolver - Construct a new timing solver. - /// - /// \param _simplifyExprs - Whether expressions should be - /// simplified (via the constraint manager interface) prior to - /// querying. - TimingSolver(Solver *_solver, bool _simplifyExprs = true) +class ConstraintSet; +class Solver; + +/// TimingSolver - A simple class which wraps a solver and handles +/// tracking the statistics that we care about. +class TimingSolver { +public: + std::unique_ptr solver; + bool simplifyExprs; + +public: + /// TimingSolver - Construct a new timing solver. + /// + /// \param _simplifyExprs - Whether expressions should be + /// simplified (via the constraint manager interface) prior to + /// querying. + TimingSolver(Solver *_solver, bool _simplifyExprs = true) : solver(_solver), simplifyExprs(_simplifyExprs) {} - void setTimeout(time::Span t) { - solver->setCoreSolverTimeout(t); - } - - char *getConstraintLog(const Query& query) { - return solver->getConstraintLog(query); - } + void setTimeout(time::Span t) { solver->setCoreSolverTimeout(t); } - bool evaluate(const ExecutionState&, ref, Solver::Validity &result); + char *getConstraintLog(const Query &query) { + return solver->getConstraintLog(query); + } - bool mustBeTrue(const ExecutionState&, ref, bool &result); + bool evaluate(const ConstraintSet &, ref, Solver::Validity &result, + SolverQueryMetaData &metaData); - bool mustBeFalse(const ExecutionState&, ref, bool &result); + bool mustBeTrue(const ConstraintSet &, ref, bool &result, + SolverQueryMetaData &metaData); - bool mayBeTrue(const ExecutionState&, ref, bool &result); + bool mustBeFalse(const ConstraintSet &, ref, bool &result, + SolverQueryMetaData &metaData); - bool mayBeFalse(const ExecutionState&, ref, bool &result); + bool mayBeTrue(const ConstraintSet &, ref, bool &result, + SolverQueryMetaData &metaData); - bool getValue(const ExecutionState &, ref expr, - ref &result); + bool mayBeFalse(const ConstraintSet &, ref, bool &result, + SolverQueryMetaData &metaData); - bool getInitialValues(const ExecutionState&, - const std::vector &objects, - std::vector< std::vector > &result); + bool getValue(const ConstraintSet &, ref expr, + ref &result, SolverQueryMetaData &metaData); - std::pair< ref, ref > - getRange(const ExecutionState&, ref query); - }; + bool getInitialValues(const ConstraintSet &, + const std::vector &objects, + std::vector> &result, + SolverQueryMetaData &metaData); + std::pair, ref> getRange(const ConstraintSet &, + ref query, + SolverQueryMetaData &metaData); +}; } #endif /* KLEE_TIMINGSOLVER_H */ -- cgit 1.4.1