Added support for KLEE value-based array optimization

4 files changed, 691 insertions, 12 deletions

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<Expr> Executor::toUnique(const ExecutionState &state,
   if (!isa<ConstantExpr>(e)) {
     ref<ConstantExpr> value;
     bool isTrue = false;
-
+    if ((OptimizeArray == ALL || OptimizeArray == VALUE) &&
+        !isa<ConstantExpr>(e)) {
+      ref<Expr> res;
+      optimizer.optimizeExpr(e, res, true);
+      if (res.get()) {
+        e = res;
+      }
+    }
     solver->setTimeout(coreSolverTimeout);
     if (solver->getValue(state, e, value)) {
       ref<Expr> cond = EqExpr::create(e, value);
-      if (OptimizeArray == INDEX &&
+      if ((OptimizeArray == ALL || OptimizeArray == VALUE ||
+           OptimizeArray == INDEX) &&
           !isa<ConstantExpr>(cond)) {
         ref<Expr> res;
         optimizer.optimizeExpr(cond, res);
@@ -1146,6 +1154,14 @@ void Executor::executeGetValue(ExecutionState &state,
     seedMap.find(&state);
   if (it==seedMap.end() || isa<ConstantExpr>(e)) {
     ref<ConstantExpr> value;
+    if ((OptimizeArray == ALL || OptimizeArray == VALUE) &&
+        !isa<ConstantExpr>(e)) {
+      ref<Expr> 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<Expr> > values;
     for (std::vector<SeedInfo>::iterator siit = it->second.begin(), 
            siie = it->second.end(); siit != siie; ++siit) {
+      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;
+        }
+      }
       ref<ConstantExpr> 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<Expr> cond = eval(ki, 0, state).value;
 
-      if (OptimizeArray == INDEX &&
+      if ((OptimizeArray == ALL || OptimizeArray == VALUE ||
+           OptimizeArray == INDEX) &&
           !isa<ConstantExpr>(cond)) {
         ref<Expr> 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<ConstantExpr>(match)) {
           ref<Expr> 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<ConstantExpr>(defaultValue)) {
         ref<Expr> 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<ConstantExpr>(v)) {
+          ref<Expr> result;
+          optimizer.optimizeExpr(v, result, true);
+          if (result.get()) {
+            v = result;
+          }
+        }
         ref<ConstantExpr> 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<ref<Expr> >::iterator ai = arguments.begin(), 
        ae = arguments.end(); ai!=ae; ++ai) {
     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;
+        }
+      }
       ref<ConstantExpr> 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<ConstantExpr>(size)) {
+      ref<Expr> result;
+      optimizer.optimizeExpr(size, result, true);
+      if (result.get()) {
+        size = result;
+      }
+    }
+
     ref<ConstantExpr> 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<Expr> address,
                            KInstruction *target) {
+  if ((OptimizeArray == ALL || OptimizeArray == VALUE) &&
+      !isa<ConstantExpr>(address)) {
+    ref<Expr> 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<Expr> p,
                             ExactResolutionList &results, 
                             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;
+    }
+  }
   // 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<ConstantExpr>(address)) {
+    ref<Expr> 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<Expr> offset = mo->getOffsetExpr(address);
+    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;
+      }
+    }
 
     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<ConstantExpr>(address)) {
+    ref<Expr> 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,
diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp
index d3e8cbab..86c19a81 100644
--- a/lib/Expr/ArrayExprOptimizer.cpp
+++ b/lib/Expr/ArrayExprOptimizer.cpp
@@ -11,11 +11,26 @@ namespace klee {
 llvm::cl::opt<ArrayOptimizationType> OptimizeArray(
     "optimize-array",
     llvm::cl::values(
+        clEnumValN(ALL, "all", "Combining index and value transformations"),
         clEnumValN(INDEX, "index", "Index-based transformation"),
+        clEnumValN(VALUE, "value", "Value-based transformation at branch (both "
+                                   "concrete and concrete/symbolic)"),
         clEnumValEnd),
     llvm::cl::init(NONE),
     llvm::cl::desc("Optimize accesses to either concrete or concrete/symbolic "
                    "arrays. (default=off)"));
+
+llvm::cl::opt<double> ArrayValueRatio(
+    "array-value-ratio",
+    llvm::cl::desc("Maximum ratio of unique values to array size for which the "
+                   "value-based transformations are applied."),
+    llvm::cl::init(1.0), llvm::cl::value_desc("Unique Values / Array Size"));
+
+llvm::cl::opt<double> ArrayValueSymbRatio(
+    "array-value-symb-ratio",
+    llvm::cl::desc("Maximum ratio of symbolic values to array size for which "
+                   "the mixed value-based transformations are applied."),
+    llvm::cl::init(1.0), llvm::cl::value_desc("Symbolic Values / Array Size"));
 };
 
 void ExprOptimizer::optimizeExpr(const ref<Expr> &e, ref<Expr> &result,
@@ -33,7 +48,7 @@ void ExprOptimizer::optimizeExpr(const ref<Expr> &e, ref<Expr> &result,
   }
 
   // ----------------------- INDEX-BASED OPTIMIZATION -------------------------
-  if (!valueOnly && OptimizeArray == INDEX) {
+  if (!valueOnly && (OptimizeArray == ALL || OptimizeArray == INDEX)) {
     array2idx_ty arrays;
     ConstantArrayExprVisitor aev(arrays);
     aev.visit(e);
@@ -72,6 +87,31 @@ void ExprOptimizer::optimizeExpr(const ref<Expr> &e, ref<Expr> &result,
       }
     }
   }
+  // ----------------------- VALUE-BASED OPTIMIZATION -------------------------
+  if (OptimizeArray == VALUE ||
+      (OptimizeArray == ALL && (!result.get() || valueOnly))) {
+    std::vector<const ReadExpr *> reads;
+    std::map<const ReadExpr *, std::pair<unsigned, Expr::Width> > readInfo;
+    ArrayReadExprVisitor are(reads, readInfo);
+    are.visit(e);
+    std::reverse(reads.begin(), reads.end());
+
+    if (reads.size() == 0 || are.isIncompatible()) {
+      cacheExprUnapplicable.insert(hash);
+      return;
+    }
+
+    ref<Expr> selectOpt =
+        getSelectOptExpr(e, reads, readInfo, are.containsSymbolic());
+    if (selectOpt.get()) {
+      klee_warning("OPT_V: successful");
+      result = selectOpt;
+      cacheExprOptimized[hash] = result;
+    } else {
+      klee_warning("OPT_V: unsuccessful");
+      cacheExprUnapplicable.insert(hash);
+    }
+  }
 }
 
 bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e,
@@ -133,3 +173,417 @@ bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e,
   }
   return success;
 }
+
+ref<Expr> ExprOptimizer::getSelectOptExpr(
+    const ref<Expr> &e, std::vector<const ReadExpr *> &reads,
+    std::map<const ReadExpr *, std::pair<unsigned, Expr::Width> > &readInfo,
+    bool isSymbolic) {
+  ref<Expr> notFound;
+  ref<Expr> toReturn;
+
+  // Array is concrete
+  if (!isSymbolic) {
+    std::map<unsigned, ref<Expr> > optimized;
+    for (auto &read : reads) {
+      auto info = readInfo[read];
+      auto cached = cacheReadExprOptimized.find(read->hash());
+      if (cached != cacheReadExprOptimized.end()) {
+        optimized.insert(std::make_pair(info.first, (*cached).second));
+        continue;
+      }
+      Expr::Width width = read->getWidth();
+      if (info.second > width) {
+        width = info.second;
+      }
+      unsigned size = read->updates.root->getSize();
+      unsigned bytesPerElement = width / 8;
+      unsigned elementsInArray = size / bytesPerElement;
+
+      // Note: we already filtered the ReadExpr, so here we can safely
+      // assume that the UpdateNodes contain ConstantExpr indexes and values
+      assert(read->updates.root->isConstantArray() &&
+             "Expected concrete array, found symbolic array");
+      auto arrayConstValues = read->updates.root->constantValues;
+      for (const UpdateNode *un = read->updates.head; un; un = un->next) {
+        ConstantExpr *ce = static_cast<ConstantExpr *>(un->index.get());
+        uint64_t index = ce->getAPValue().getZExtValue();
+        assert(index < arrayConstValues.size());
+        ConstantExpr *arrayValue = static_cast<ConstantExpr *>(un->value.get());
+        arrayConstValues[index] = arrayValue;
+      }
+      std::vector<uint64_t> arrayValues;
+      // Get the concrete values from the array
+      for (unsigned i = 0; i < elementsInArray; i++) {
+        uint64_t val = 0;
+        for (unsigned j = 0; j < bytesPerElement; j++) {
+          val |= (*(
+                       arrayConstValues[(i * bytesPerElement) + j]
+                           .get()
+                           ->getAPValue()
+                           .getRawData())
+                  << (j * 8));
+        }
+        arrayValues.push_back(val);
+      }
+
+      ref<Expr> index = read->index;
+      IndexCleanerVisitor ice;
+      ice.visit(index);
+      if (ice.getIndex().get()) {
+        index = ice.getIndex();
+      }
+
+      ref<Expr> opt =
+          buildConstantSelectExpr(index, arrayValues, width, elementsInArray);
+      if (opt.get()) {
+        cacheReadExprOptimized[read->hash()] = opt;
+        optimized.insert(std::make_pair(info.first, opt));
+      }
+    }
+    ArrayValueOptReplaceVisitor replacer(optimized);
+    toReturn = replacer.visit(e);
+  }
+
+  // Array is mixed concrete/symbolic
+  // \pre: array is concrete && updatelist contains at least one symbolic value
+  // OR
+  //       array is symbolic && updatelist contains at least one concrete value
+  else {
+    std::map<unsigned, ref<Expr> > optimized;
+    for (auto &read : reads) {
+      auto info = readInfo[read];
+      auto cached = cacheReadExprOptimized.find(read->hash());
+      if (cached != cacheReadExprOptimized.end()) {
+        optimized.insert(std::make_pair(info.first, (*cached).second));
+        continue;
+      }
+      Expr::Width width = read->getWidth();
+      if (info.second > width) {
+        width = info.second;
+      }
+      unsigned size = read->updates.root->getSize();
+      unsigned bytesPerElement = width / 8;
+      unsigned elementsInArray = size / bytesPerElement;
+      bool symbArray = read->updates.root->isSymbolicArray();
+
+      BitArray ba(size, symbArray);
+      // Note: we already filtered the ReadExpr, so here we can safely
+      // assume that the UpdateNodes contain ConstantExpr indexes, but in
+      // this case we *cannot* assume anything on the values
+      auto arrayConstValues = read->updates.root->constantValues;
+      if (arrayConstValues.size() < size) {
+        // We need to "force" initialization of the values
+        for (size_t i = arrayConstValues.size(); i < size; i++) {
+          arrayConstValues.push_back(ConstantExpr::create(0, Expr::Int8));
+        }
+      }
+      for (const UpdateNode *un = read->updates.head; un; un = un->next) {
+        ConstantExpr *ce = static_cast<ConstantExpr *>(un->index.get());
+        uint64_t index = ce->getAPValue().getLimitedValue();
+        if (!isa<ConstantExpr>(un->value)) {
+          ba.set(index);
+        } else {
+          ba.unset(index);
+          ConstantExpr *arrayValue =
+              static_cast<ConstantExpr *>(un->value.get());
+          arrayConstValues[index] = arrayValue;
+        }
+      }
+
+      std::vector<std::pair<uint64_t, bool> > arrayValues;
+      unsigned symByteNum = 0;
+      for (unsigned i = 0; i < elementsInArray; i++) {
+        uint64_t val = 0;
+        bool elementIsConcrete = true;
+        for (unsigned j = 0; j < bytesPerElement; j++) {
+          if (ba.get((i * bytesPerElement) + j)) {
+            elementIsConcrete = false;
+            break;
+          } else {
+            val |= (*(
+                         arrayConstValues[(i * bytesPerElement) + j]
+                             .get()
+                             ->getAPValue()
+                             .getRawData())
+                    << (j * 8));
+          }
+        }
+        if (elementIsConcrete) {
+          arrayValues.push_back(std::make_pair(val, true));
+        } else {
+          symByteNum++;
+          arrayValues.push_back(std::make_pair(0, false));
+        }
+      }
+
+      if (((double)symByteNum / (double)elementsInArray) <= ArrayValueSymbRatio) {
+        // If the optimization can be applied we apply it
+        // Build the dynamic select expression
+        ref<Expr> opt =
+            buildMixedSelectExpr(read, arrayValues, width, elementsInArray);
+        if (opt.get()) {
+          cacheReadExprOptimized[read->hash()] = opt;
+          optimized.insert(std::make_pair(info.first, opt));
+        }
+      }
+    }
+    ArrayValueOptReplaceVisitor replacer(optimized, false);
+    toReturn = replacer.visit(e);
+  }
+
+  return toReturn.get() ? toReturn : notFound;
+}
+
+ref<Expr> ExprOptimizer::buildConstantSelectExpr(
+    const ref<Expr> &index, std::vector<uint64_t> &arrayValues,
+    Expr::Width width, unsigned arraySize) const {
+  std::vector<std::pair<uint64_t, uint64_t> > ranges;
+  std::vector<uint64_t> values;
+  std::set<uint64_t> unique_array_values;
+  ExprBuilder *builder = createDefaultExprBuilder();
+  Expr::Width valWidth = width;
+  ref<Expr> result;
+
+  ref<Expr> actualIndex;
+  if (index->getWidth() > Expr::Int32) {
+    actualIndex = ExtractExpr::alloc(index, 0, Expr::Int32);
+  } else {
+    actualIndex = index;
+  }
+  Expr::Width idxWidth = actualIndex->getWidth();
+
+  // Calculate the repeating values ranges in the constant array
+  unsigned curr_idx = 0;
+  uint64_t curr_val = arrayValues[0];
+  for (unsigned i = 0; i < arraySize; i++) {
+    uint64_t temp = arrayValues[i];
+    unique_array_values.insert(curr_val);
+    if (temp != curr_val) {
+      ranges.push_back(std::make_pair(curr_idx, i));
+      values.push_back(curr_val);
+      curr_val = temp;
+      curr_idx = i;
+      if (i == (arraySize - 1)) {
+        ranges.push_back(std::make_pair(curr_idx, i + 1));
+        values.push_back(curr_val);
+      }
+    } else if (i == (arraySize - 1)) {
+      ranges.push_back(std::make_pair(curr_idx, i + 1));
+      values.push_back(curr_val);
+    }
+  }
+
+  if (((double)unique_array_values.size() / (double)(arraySize)) >= ArrayValueRatio) {
+    return result;
+  }
+
+  std::map<uint64_t, std::vector<std::pair<uint64_t, uint64_t> > > exprMap;
+  for (size_t i = 0; i < ranges.size(); i++) {
+    if (exprMap.find(values[i]) != exprMap.end()) {
+      exprMap[values[i]]
+          .push_back(std::make_pair(ranges[i].first, ranges[i].second));
+    } else {
+      if (exprMap.find(values[i]) == exprMap.end()) {
+        exprMap.insert(std::make_pair(
+            values[i], std::vector<std::pair<uint64_t, uint64_t> >()));
+      }
+      exprMap.find(values[i])
+          ->second.push_back(std::make_pair(ranges[i].first, ranges[i].second));
+    }
+  }
+
+  int ct = 0;
+  // For each range appropriately build the Select expression.
+  for (auto range : exprMap) {
+    ref<Expr> temp;
+    if (ct == 0) {
+      temp = builder->Constant(llvm::APInt(valWidth, range.first, false));
+    } else {
+      if (range.second.size() == 1) {
+        if (range.second[0].first == (range.second[0].second - 1)) {
+          temp = SelectExpr::create(
+              EqExpr::create(actualIndex,
+                             builder->Constant(llvm::APInt(
+                                 idxWidth, range.second[0].first, false))),
+              builder->Constant(llvm::APInt(valWidth, range.first, false)),
+              result);
+
+        } else {
+          temp = SelectExpr::create(
+              AndExpr::create(
+                  SgeExpr::create(actualIndex,
+                                  builder->Constant(llvm::APInt(
+                                      idxWidth, range.second[0].first, false))),
+                  SltExpr::create(
+                      actualIndex,
+                      builder->Constant(llvm::APInt(
+                          idxWidth, range.second[0].second, false)))),
+              builder->Constant(llvm::APInt(valWidth, range.first, false)),
+              result);
+        }
+
+      } else {
+        ref<Expr> currOr;
+        if (range.second[0].first == (range.second[0].second - 1)) {
+          currOr = EqExpr::create(actualIndex,
+                                  builder->Constant(llvm::APInt(
+                                      idxWidth, range.second[0].first, false)));
+        } else {
+          currOr = AndExpr::create(
+              SgeExpr::create(actualIndex,
+                              builder->Constant(llvm::APInt(
+                                  idxWidth, range.second[0].first, false))),
+              SltExpr::create(actualIndex,
+                              builder->Constant(llvm::APInt(
+                                  idxWidth, range.second[0].second, false))));
+        }
+        for (size_t i = 1; i < range.second.size(); i++) {
+          ref<Expr> tempOr;
+          if (range.second[i].first == (range.second[i].second - 1)) {
+            tempOr = OrExpr::create(
+                EqExpr::create(actualIndex,
+                               builder->Constant(llvm::APInt(
+                                   idxWidth, range.second[i].first, false))),
+                currOr);
+
+          } else {
+            tempOr = OrExpr::create(
+                AndExpr::create(
+                    SgeExpr::create(
+                        actualIndex,
+                        builder->Constant(llvm::APInt(
+                            idxWidth, range.second[i].first, false))),
+                    SltExpr::create(
+                        actualIndex,
+                        builder->Constant(llvm::APInt(
+                            idxWidth, range.second[i].second, false)))),
+                currOr);
+          }
+          currOr = tempOr;
+        }
+        temp = SelectExpr::create(currOr, builder->Constant(llvm::APInt(
+                                              valWidth, range.first, false)),
+                                  result);
+      }
+    }
+    result = temp;
+    ct++;
+  }
+
+  delete (builder);
+
+  return result;
+}
+
+ref<Expr> ExprOptimizer::buildMixedSelectExpr(
+    const ReadExpr *re, std::vector<std::pair<uint64_t, bool> > &arrayValues,
+    Expr::Width width, unsigned elementsInArray) const {
+  ExprBuilder *builder = createDefaultExprBuilder();
+  std::vector<uint64_t> values;
+  std::vector<std::pair<uint64_t, uint64_t> > ranges;
+  std::vector<uint64_t> holes;
+  std::set<uint64_t> unique_array_values;
+
+  unsigned arraySize = elementsInArray;
+  unsigned curr_idx = 0;
+  uint64_t curr_val = arrayValues[0].first;
+
+  bool emptyRange = true;
+  // Calculate Range values
+  for (size_t i = 0; i < arrayValues.size(); i++) {
+    // If the value is concrete
+    if (arrayValues[i].second) {
+      // The range contains a concrete value
+      emptyRange = false;
+      uint64_t temp = arrayValues[i].first;
+      unique_array_values.insert(temp);
+      if (temp != curr_val) {
+        ranges.push_back(std::make_pair(curr_idx, i));
+        values.push_back(curr_val);
+        curr_val = temp;
+        curr_idx = i;
+        if (i == (arraySize - 1)) {
+          ranges.push_back(std::make_pair(curr_idx, curr_idx + 1));
+          values.push_back(curr_val);
+        }
+      } else if (i == (arraySize - 1)) {
+        ranges.push_back(std::make_pair(curr_idx, i + 1));
+        values.push_back(curr_val);
+      }
+    } else {
+      holes.push_back(i);
+      // If this is not an empty range
+      if (!emptyRange) {
+        ranges.push_back(std::make_pair(curr_idx, i));
+        values.push_back(curr_val);
+      }
+      curr_val = arrayValues[i + 1].first;
+      curr_idx = i + 1;
+      emptyRange = true;
+    }
+  }
+
+  assert(unique_array_values.size() > 0 && "No unique values");
+  assert(ranges.size() > 0 && "No ranges");
+
+  ref<Expr> result;
+  if (((double)unique_array_values.size() / (double)(arraySize)) <= ArrayValueRatio) {
+    // The final "else" expression will be the original unoptimized array read
+    // expression
+    unsigned range_start = 0;
+    if (holes.size() == 0) {
+      result = builder->Constant(llvm::APInt(width, values[0], false));
+      range_start = 1;
+    } else {
+      ref<Expr> firstIndex = MulExpr::create(
+          ConstantExpr::create(holes[0], re->index->getWidth()),
+          ConstantExpr::create(width / 8, re->index->getWidth()));
+      result = ReadExpr::extendRead(re->updates, firstIndex, width);
+      for (size_t i = 1; i < holes.size(); i++) {
+        ref<Expr> temp_idx = MulExpr::create(
+            ConstantExpr::create(holes[i], re->index->getWidth()),
+            ConstantExpr::create(width / 8, re->index->getWidth()));
+        ref<Expr> cond = EqExpr::create(
+            re->index, ConstantExpr::create(holes[i], re->index->getWidth()));
+        ref<Expr> temp = SelectExpr::create(
+            cond, ReadExpr::extendRead(re->updates, temp_idx, width), result);
+        result = temp;
+      }
+    }
+
+    ref<Expr> new_index = re->index;
+    IndexCleanerVisitor ice;
+    ice.visit(new_index);
+    if (ice.getIndex().get()) {
+      new_index = ice.getIndex();
+    }
+
+    int new_index_width = new_index->getWidth();
+    // Iterate through all the ranges
+    for (size_t i = range_start; i < ranges.size(); i++) {
+      ref<Expr> temp;
+      if (ranges[i].second - 1 == ranges[i].first) {
+        ref<Expr> cond = EqExpr::create(
+            new_index, ConstantExpr::create(ranges[i].first, new_index_width));
+        ref<Expr> t = ConstantExpr::create(values[i], width);
+        ref<Expr> f = result;
+        temp = SelectExpr::create(cond, t, f);
+      } else {
+        // Create the select constraint
+        ref<Expr> cond = AndExpr::create(
+            SgeExpr::create(new_index, ConstantExpr::create(ranges[i].first,
+                                                            new_index_width)),
+            SltExpr::create(new_index, ConstantExpr::create(ranges[i].second,
+                                                            new_index_width)));
+        ref<Expr> t = ConstantExpr::create(values[i], width);
+        ref<Expr> f = result;
+        temp = SelectExpr::create(cond, t, f);
+      }
+      result = temp;
+    }
+  }
+
+  delete (builder);
+
+  return result;
+}
diff --git a/lib/Expr/ArrayExprVisitor.cpp b/lib/Expr/ArrayExprVisitor.cpp
index 26ddbb95..fa92b66c 100644
--- a/lib/Expr/ArrayExprVisitor.cpp
+++ b/lib/Expr/ArrayExprVisitor.cpp
@@ -169,3 +169,96 @@ ExprVisitor::Action IndexTransformationExprVisitor::visitMul(const MulExpr &e) {
     mul = e.getKid(1);
   return Action::doChildren();
 }
+
+//-------------------------- VALUE-BASED OPTIMIZATION------------------------//
+ExprVisitor::Action ArrayReadExprVisitor::visitConcat(const ConcatExpr &ce) {
+  ReadExpr *base = ArrayExprHelper::hasOrderedReads(ce);
+  if (base) {
+    return inspectRead(ce.hash(), ce.getWidth(), *base);
+  }
+  return Action::doChildren();
+}
+ExprVisitor::Action ArrayReadExprVisitor::visitRead(const ReadExpr &re) {
+  return inspectRead(re.hash(), re.getWidth(), re);
+}
+// This method is a mess because I want to avoid looping over the UpdateList
+// values twice
+ExprVisitor::Action ArrayReadExprVisitor::inspectRead(unsigned hash,
+                                                      Expr::Width width,
+                                                      const ReadExpr &re) {
+  // pre(*): index is symbolic
+  if (!isa<ConstantExpr>(re.index)) {
+    if (readInfo.find(&re) == readInfo.end()) {
+      if (re.updates.root->isSymbolicArray() && !re.updates.head) {
+        return Action::doChildren();
+      }
+      if (re.updates.head) {
+        // Check preconditions on UpdateList nodes
+        bool hasConcreteValues = false;
+        for (const UpdateNode *un = re.updates.head; un; un = un->next) {
+          // Symbolic case - \inv(update): index is concrete
+          if (!isa<ConstantExpr>(un->index)) {
+            incompatible = true;
+            break;
+          } else if (!isa<ConstantExpr>(un->value)) {
+            // We tell the optimization that there is a symbolic value,
+            // otherwise we rely on the concrete optimization procedure
+            symbolic = true;
+          } else if (re.updates.root->isSymbolicArray() &&
+                     isa<ConstantExpr>(un->value)) {
+            // We can optimize symbolic array, but only if they have
+            // at least one concrete value
+            hasConcreteValues = true;
+          }
+        }
+        // Symbolic case - if array is symbolic, then we need at least one
+        // concrete value
+        if (re.updates.root->isSymbolicArray()) {
+          if (hasConcreteValues)
+            symbolic = true;
+          else
+            incompatible = true;
+        }
+
+        if (incompatible)
+          return Action::skipChildren();
+      }
+      symbolic |= re.updates.root->isSymbolicArray();
+      reads.push_back(&re);
+      readInfo.emplace(&re, std::make_pair(hash, width));
+    }
+    return Action::skipChildren();
+  }
+  return Action::doChildren();
+}
+
+ExprVisitor::Action
+ArrayValueOptReplaceVisitor::visitConcat(const ConcatExpr &ce) {
+  auto found = optimized.find(ce.hash());
+  if (found != optimized.end()) {
+    return Action::changeTo((*found).second.get());
+  }
+  return Action::doChildren();
+}
+ExprVisitor::Action ArrayValueOptReplaceVisitor::visitRead(const ReadExpr &re) {
+  auto found = optimized.find(re.hash());
+  if (found != optimized.end()) {
+    return Action::changeTo((*found).second.get());
+  }
+  return Action::doChildren();
+}
+
+ExprVisitor::Action IndexCleanerVisitor::visitMul(const MulExpr &e) {
+  if (mul) {
+    if (!isa<ConstantExpr>(e.getKid(0)))
+      index = e.getKid(0);
+    else if (!isa<ConstantExpr>(e.getKid(1)))
+      index = e.getKid(1);
+    mul = false;
+  }
+  return Action::doChildren();
+}
+ExprVisitor::Action IndexCleanerVisitor::visitRead(const ReadExpr &re) {
+  mul = false;
+  return Action::doChildren();
+}
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index a5c7f652..9e524f62 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -81,6 +81,47 @@ ref<Expr> Expr::createTempRead(const Array *array, Expr::Width w) {
   }
 }
 
+ref<Expr> ReadExpr::extendRead(const UpdateList &ul, const ref<Expr> index,
+                               Expr::Width w) {
+  switch (w) {
+  default:
+    assert(0 && "invalid width");
+  case Expr::Int8:
+    return ReadExpr::alloc(ul, index);
+  case Expr::Int16:
+    return ConcatExpr::create(
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)),
+        ReadExpr::alloc(ul, index));
+  case Expr::Int32:
+    return ConcatExpr::create4(
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(3, Expr::Int32), index)),
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(2, Expr::Int32), index)),
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)),
+        ReadExpr::alloc(ul, index));
+  case Expr::Int64:
+    return ConcatExpr::create8(
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(7, Expr::Int32), index)),
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(6, Expr::Int32), index)),
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(5, Expr::Int32), index)),
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(4, Expr::Int32), index)),
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(3, Expr::Int32), index)),
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(2, Expr::Int32), index)),
+        ReadExpr::alloc(
+            ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)),
+        ReadExpr::alloc(ul, index));
+  }
+}
+
 int Expr::compare(const Expr &b) const {
   static ExprEquivSet equivs;
   int r = compare(b, equivs);