diff options
author | Martin Nowack <m.nowack@imperial.ac.uk> | 2018-10-17 22:39:06 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-10-23 18:53:46 +0300 |
commit | 713c1a3744aa8c0bfadf85a76377dd2c7dd63519 (patch) | |
tree | 6083e195f3d27791598bbf7a1976ef2a2379c84c | |
parent | ca1a1083a8a9cce249dd46511072c00676a4c3d5 (diff) | |
download | klee-713c1a3744aa8c0bfadf85a76377dd2c7dd63519.tar.gz |
optimizeExpr: return the result as return value instead as function argument
simplifies code a lot.
-rw-r--r-- | include/klee/ArrayExprOptimizer.h | 6 | ||||
-rw-r--r-- | lib/Core/Executor.cpp | 90 | ||||
-rw-r--r-- | lib/Expr/ArrayExprOptimizer.cpp | 22 |
3 files changed, 31 insertions, 87 deletions
diff --git a/include/klee/ArrayExprOptimizer.h b/include/klee/ArrayExprOptimizer.h index 36c26484..5c02e44b 100644 --- a/include/klee/ArrayExprOptimizer.h +++ b/include/klee/ArrayExprOptimizer.h @@ -72,7 +72,11 @@ private: unordered_map<unsigned, ref<Expr>> cacheReadExprOptimized; public: - void optimizeExpr(const ref<Expr> &e, ref<Expr> &result, bool valueOnly); + /// Returns the optimised version of e. + /// @param e expression to optimise + /// @param valueOnly XXX document + /// @return optimised expression + ref<Expr> optimizeExpr(const ref<Expr> &e, bool valueOnly); private: bool diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index f0335812..35178106 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1087,11 +1087,7 @@ ref<Expr> Executor::toUnique(const ExecutionState &state, bool isTrue = false; if ((OptimizeArray == ALL || OptimizeArray == VALUE) && !isa<ConstantExpr>(e)) { - ref<Expr> res; - optimizer.optimizeExpr(e, res, true); - if (res.get()) { - e = res; - } + e = optimizer.optimizeExpr(e, true); } solver->setTimeout(coreSolverTimeout); if (solver->getValue(state, e, value)) { @@ -1099,11 +1095,7 @@ ref<Expr> Executor::toUnique(const ExecutionState &state, if ((OptimizeArray == ALL || OptimizeArray == VALUE || OptimizeArray == INDEX) && !isa<ConstantExpr>(cond)) { - ref<Expr> res; - optimizer.optimizeExpr(cond, res, false); - if (res.get()) { - cond = res; - } + cond = optimizer.optimizeExpr(cond, false); } if (solver->mustBeTrue(state, cond, isTrue) && isTrue) result = value; @@ -1156,11 +1148,7 @@ void Executor::executeGetValue(ExecutionState &state, ref<ConstantExpr> value; if ((OptimizeArray == ALL || OptimizeArray == VALUE) && !isa<ConstantExpr>(e)) { - ref<Expr> result; - optimizer.optimizeExpr(e, result, true); - if (result.get()) { - e = result; - } + e = optimizer.optimizeExpr(e, true); } bool success = solver->getValue(state, e, value); assert(success && "FIXME: Unhandled solver failure"); @@ -1173,11 +1161,7 @@ void Executor::executeGetValue(ExecutionState &state, ref<Expr> cond = siit->assignment.evaluate(e); if ((OptimizeArray == ALL || OptimizeArray == VALUE) && !isa<ConstantExpr>(cond)) { - ref<Expr> result; - optimizer.optimizeExpr(cond, result, true); - if (result.get()) { - cond = result; - } + cond = optimizer.optimizeExpr(cond, true); } ref<ConstantExpr> value; bool success = solver->getValue(state, cond, value); @@ -1611,11 +1595,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if ((OptimizeArray == ALL || OptimizeArray == VALUE || OptimizeArray == INDEX) && !isa<ConstantExpr>(cond)) { - ref<Expr> result; - optimizer.optimizeExpr(cond, result, false); - if (result.get()) { - cond = result; - } + cond = optimizer.optimizeExpr(cond, false); } Executor::StatePair branches = fork(state, cond, false); @@ -1764,11 +1744,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if ((OptimizeArray == ALL || OptimizeArray == VALUE || OptimizeArray == INDEX) && !isa<ConstantExpr>(match)) { - ref<Expr> result; - optimizer.optimizeExpr(match, result, false); - if (result.get()) { - match = result; - } + match = optimizer.optimizeExpr(match, false); } bool success = solver->mayBeTrue(state, match, result); assert(success && "FIXME: Unhandled solver failure"); @@ -1799,11 +1775,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if ((OptimizeArray == ALL || OptimizeArray == VALUE || OptimizeArray == INDEX) && !isa<ConstantExpr>(defaultValue)) { - ref<Expr> result; - optimizer.optimizeExpr(defaultValue, result, false); - if (result.get()) { - defaultValue = result; - } + defaultValue = optimizer.optimizeExpr(defaultValue, false); } bool res; bool success = solver->mayBeTrue(state, defaultValue, res); @@ -1922,11 +1894,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { do { if ((OptimizeArray == ALL || OptimizeArray == VALUE) && !isa<ConstantExpr>(v)) { - ref<Expr> result; - optimizer.optimizeExpr(v, result, true); - if (result.get()) { - v = result; - } + v = optimizer.optimizeExpr(v, true); } ref<ConstantExpr> value; bool success = solver->getValue(*free, v, value); @@ -3163,11 +3131,7 @@ void Executor::callExternalFunction(ExecutionState &state, if (AllowExternalSymCalls) { // don't bother checking uniqueness if ((OptimizeArray == ALL || OptimizeArray == VALUE) && !isa<ConstantExpr>(*ai)) { - ref<Expr> result; - optimizer.optimizeExpr(*ai, result, true); - if (result.get()) { - *ai = result; - } + *ai = optimizer.optimizeExpr(*ai, true); } ref<ConstantExpr> ce; bool success = solver->getValue(state, *ai, ce); @@ -3357,11 +3321,7 @@ void Executor::executeAlloc(ExecutionState &state, if ((OptimizeArray == ALL || OptimizeArray == VALUE) && !isa<ConstantExpr>(size)) { - ref<Expr> result; - optimizer.optimizeExpr(size, result, true); - if (result.get()) { - size = result; - } + size = optimizer.optimizeExpr(size, true); } ref<ConstantExpr> example; @@ -3436,11 +3396,7 @@ void Executor::executeFree(ExecutionState &state, KInstruction *target) { if ((OptimizeArray == ALL || OptimizeArray == VALUE) && !isa<ConstantExpr>(address)) { - ref<Expr> result; - optimizer.optimizeExpr(address, result, true); - if (result.get()) { - address = result; - } + address = optimizer.optimizeExpr(address, true); } StatePair zeroPointer = fork(state, Expr::createIsZero(address), true); if (zeroPointer.first) { @@ -3475,11 +3431,7 @@ void Executor::resolveExact(ExecutionState &state, const std::string &name) { if ((OptimizeArray == ALL || OptimizeArray == VALUE) && !isa<ConstantExpr>(p)) { - ref<Expr> result; - optimizer.optimizeExpr(p, result, true); - if (result.get()) { - p = result; - } + p = optimizer.optimizeExpr(p, true); } // XXX we may want to be capping this? ResolutionList rl; @@ -3523,11 +3475,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, } if ((OptimizeArray == VALUE) && !isa<ConstantExpr>(address)) { - ref<Expr> result; - optimizer.optimizeExpr(address, result, true); - if (result.get()) { - address = result; - } + address = optimizer.optimizeExpr(address, true); } // fast path: single in-bounds resolution @@ -3551,11 +3499,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, ref<Expr> check = mo->getBoundsCheckOffset(offset, bytes); if ((OptimizeArray == ALL || OptimizeArray == VALUE) && !isa<ConstantExpr>(check)) { - ref<Expr> result; - optimizer.optimizeExpr(check, result, true); - if (result.get()) { - check = result; - } + check = optimizer.optimizeExpr(check, true); } bool inBounds; @@ -3596,11 +3540,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, if ((OptimizeArray == ALL || OptimizeArray == VALUE) && !isa<ConstantExpr>(address)) { - ref<Expr> result; - optimizer.optimizeExpr(address, result, true); - if (result.get()) { - address = result; - } + address = optimizer.optimizeExpr(address, true); } ResolutionList rl; solver->setTimeout(coreSolverTimeout); diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp index 3a071665..2d817e83 100644 --- a/lib/Expr/ArrayExprOptimizer.cpp +++ b/lib/Expr/ArrayExprOptimizer.cpp @@ -42,20 +42,17 @@ llvm::cl::opt<double> ArrayValueSymbRatio( llvm::cl::init(1.0), llvm::cl::value_desc("Symbolic Values / Array Size")); }; -void ExprOptimizer::optimizeExpr(const ref<Expr> &e, ref<Expr> &result, - bool valueOnly) { +ref<Expr> ExprOptimizer::optimizeExpr(const ref<Expr> &e, bool valueOnly) { unsigned hash = e->hash(); - if (cacheExprUnapplicable.find(hash) != cacheExprUnapplicable.end()) { - return; - } + if (cacheExprUnapplicable.find(hash) != cacheExprUnapplicable.end()) + return e; // Find cached expressions auto cached = cacheExprOptimized.find(hash); - if (cached != cacheExprOptimized.end()) { - result = cached->second; - return; - } + if (cached != cacheExprOptimized.end()) + return cached->second; + ref<Expr> result; // ----------------------- INDEX-BASED OPTIMIZATION ------------------------- if (!valueOnly && (OptimizeArray == ALL || OptimizeArray == INDEX)) { array2idx_ty arrays; @@ -69,7 +66,7 @@ void ExprOptimizer::optimizeExpr(const ref<Expr> &e, ref<Expr> &result, // when we are not combining the optimizations if (OptimizeArray == INDEX) { cacheExprUnapplicable.insert(hash); - return; + return e; } } else { mapIndexOptimizedExpr_ty idx_valIdx; @@ -107,7 +104,7 @@ void ExprOptimizer::optimizeExpr(const ref<Expr> &e, ref<Expr> &result, if (reads.size() == 0 || are.isIncompatible()) { cacheExprUnapplicable.insert(hash); - return; + return e; } ref<Expr> selectOpt = @@ -121,6 +118,9 @@ void ExprOptimizer::optimizeExpr(const ref<Expr> &e, ref<Expr> &result, cacheExprUnapplicable.insert(hash); } } + if (result.isNull()) + return e; + return result; } bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e, |