From 1a9662670ebdef07269e1abfc3f0315bdb33277c Mon Sep 17 00:00:00 2001 From: Andrea Mattavelli Date: Wed, 22 Nov 2017 18:01:29 +0000 Subject: Added support for KLEE value-based array optimization --- lib/Core/Executor.cpp | 113 +++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 102 insertions(+), 11 deletions(-) (limited to 'lib/Core/Executor.cpp') diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 613c51ae..506fa12f 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1085,11 +1085,19 @@ ref Executor::toUnique(const ExecutionState &state, if (!isa(e)) { ref value; bool isTrue = false; - + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa(e)) { + ref res; + optimizer.optimizeExpr(e, res, true); + if (res.get()) { + e = res; + } + } solver->setTimeout(coreSolverTimeout); if (solver->getValue(state, e, value)) { ref cond = EqExpr::create(e, value); - if (OptimizeArray == INDEX && + if ((OptimizeArray == ALL || OptimizeArray == VALUE || + OptimizeArray == INDEX) && !isa(cond)) { ref res; optimizer.optimizeExpr(cond, res); @@ -1146,6 +1154,14 @@ void Executor::executeGetValue(ExecutionState &state, seedMap.find(&state); if (it==seedMap.end() || isa(e)) { ref value; + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa(e)) { + ref result; + optimizer.optimizeExpr(e, result, true); + if (result.get()) { + e = result; + } + } bool success = solver->getValue(state, e, value); assert(success && "FIXME: Unhandled solver failure"); (void) success; @@ -1154,9 +1170,17 @@ void Executor::executeGetValue(ExecutionState &state, std::set< ref > values; for (std::vector::iterator siit = it->second.begin(), siie = it->second.end(); siit != siie; ++siit) { + ref cond = siit->assignment.evaluate(e); + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa(cond)) { + ref result; + optimizer.optimizeExpr(cond, result, true); + if (result.get()) { + cond = result; + } + } ref value; - bool success = - solver->getValue(state, siit->assignment.evaluate(e), value); + bool success = solver->getValue(state, cond, value); assert(success && "FIXME: Unhandled solver failure"); (void) success; values.insert(value); @@ -1584,7 +1608,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { "Wrong operand index!"); ref cond = eval(ki, 0, state).value; - if (OptimizeArray == INDEX && + if ((OptimizeArray == ALL || OptimizeArray == VALUE || + OptimizeArray == INDEX) && !isa(cond)) { ref result; optimizer.optimizeExpr(cond, result); @@ -1736,7 +1761,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { // Check if control flow could take this case bool result; - if (OptimizeArray == INDEX && + if ((OptimizeArray == ALL || OptimizeArray == VALUE || + OptimizeArray == INDEX) && !isa(match)) { ref result; optimizer.optimizeExpr(match, result); @@ -1770,7 +1796,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { } // Check if control could take the default case - if (OptimizeArray == INDEX && + if ((OptimizeArray == ALL || OptimizeArray == VALUE || + OptimizeArray == INDEX) && !isa(defaultValue)) { ref result; optimizer.optimizeExpr(defaultValue, result); @@ -1893,6 +1920,14 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { have already got a value. But in the end the caches should handle it for us, albeit with some overhead. */ do { + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa(v)) { + ref result; + optimizer.optimizeExpr(v, result, true); + if (result.get()) { + v = result; + } + } ref value; bool success = solver->getValue(*free, v, value); assert(success && "FIXME: Unhandled solver failure"); @@ -3126,6 +3161,14 @@ void Executor::callExternalFunction(ExecutionState &state, for (std::vector >::iterator ai = arguments.begin(), ae = arguments.end(); ai!=ae; ++ai) { if (AllowExternalSymCalls) { // don't bother checking uniqueness + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa(*ai)) { + ref result; + optimizer.optimizeExpr(*ai, result, true); + if (result.get()) { + *ai = result; + } + } ref ce; bool success = solver->getValue(state, *ai, ce); assert(success && "FIXME: Unhandled solver failure"); @@ -3312,6 +3355,15 @@ void Executor::executeAlloc(ExecutionState &state, // return argument first). This shows up in pcre when llvm // collapses the size expression with a select. + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa(size)) { + ref result; + optimizer.optimizeExpr(size, result, true); + if (result.get()) { + size = result; + } + } + ref example; bool success = solver->getValue(state, size, example); assert(success && "FIXME: Unhandled solver failure"); @@ -3382,6 +3434,14 @@ void Executor::executeAlloc(ExecutionState &state, void Executor::executeFree(ExecutionState &state, ref address, KInstruction *target) { + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa(address)) { + ref result; + optimizer.optimizeExpr(address, result, true); + if (result.get()) { + address = result; + } + } StatePair zeroPointer = fork(state, Expr::createIsZero(address), true); if (zeroPointer.first) { if (target) @@ -3413,6 +3473,14 @@ void Executor::resolveExact(ExecutionState &state, ref p, ExactResolutionList &results, const std::string &name) { + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa(p)) { + ref result; + optimizer.optimizeExpr(p, result, true); + if (result.get()) { + p = result; + } + } // XXX we may want to be capping this? ResolutionList rl; state.addressSpace.resolve(state, solver, p, rl); @@ -3454,6 +3522,14 @@ void Executor::executeMemoryOperation(ExecutionState &state, value = state.constraints.simplifyExpr(value); } + if ((OptimizeArray == VALUE) && !isa(address)) { + ref result; + optimizer.optimizeExpr(address, result, true); + if (result.get()) { + address = result; + } + } + // fast path: single in-bounds resolution ObjectPair op; bool success; @@ -3472,12 +3548,19 @@ void Executor::executeMemoryOperation(ExecutionState &state, } ref offset = mo->getOffsetExpr(address); + ref check = mo->getBoundsCheckOffset(offset, bytes); + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa(check)) { + ref result; + optimizer.optimizeExpr(check, result, true); + if (result.get()) { + check = result; + } + } bool inBounds; solver->setTimeout(coreSolverTimeout); - bool success = solver->mustBeTrue(state, - mo->getBoundsCheckOffset(offset, bytes), - inBounds); + bool success = solver->mustBeTrue(state, check, inBounds); solver->setTimeout(0); if (!success) { state.pc = state.prevPC; @@ -3510,7 +3593,15 @@ void Executor::executeMemoryOperation(ExecutionState &state, // we are on an error path (no resolution, multiple resolution, one // resolution with out of bounds) - + + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa(address)) { + ref result; + optimizer.optimizeExpr(address, result, true); + if (result.get()) { + address = result; + } + } ResolutionList rl; solver->setTimeout(coreSolverTimeout); bool incomplete = state.addressSpace.resolve(state, solver, address, rl, -- cgit 1.4.1