about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorMartin Nowack <m.nowack@imperial.ac.uk>2018-10-17 22:39:06 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2018-10-23 18:53:46 +0300
commit713c1a3744aa8c0bfadf85a76377dd2c7dd63519 (patch)
tree6083e195f3d27791598bbf7a1976ef2a2379c84c
parentca1a1083a8a9cce249dd46511072c00676a4c3d5 (diff)
downloadklee-713c1a3744aa8c0bfadf85a76377dd2c7dd63519.tar.gz
optimizeExpr: return the result as return value instead as function argument
simplifies code a lot.
-rw-r--r--include/klee/ArrayExprOptimizer.h6
-rw-r--r--lib/Core/Executor.cpp90
-rw-r--r--lib/Expr/ArrayExprOptimizer.cpp22
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,