about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Expr/ArrayExprOptimizer.cpp56
-rw-r--r--lib/Expr/ArrayExprOptimizer.h4
-rw-r--r--lib/Expr/ArrayExprRewriter.cpp10
-rw-r--r--lib/Expr/ArrayExprRewriter.h4
-rw-r--r--lib/Expr/ArrayExprVisitor.cpp8
-rw-r--r--lib/Expr/ArrayExprVisitor.h48
6 files changed, 64 insertions, 66 deletions
diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp
index 63a9fb96..cadd9588 100644
--- a/lib/Expr/ArrayExprOptimizer.cpp
+++ b/lib/Expr/ArrayExprOptimizer.cpp
@@ -11,11 +11,11 @@
 
 #include <algorithm>
 #include <cassert>
+#include <cstddef>
 #include <llvm/ADT/APInt.h>
 #include <llvm/Support/Casting.h>
 #include <llvm/Support/CommandLine.h>
 #include <set>
-#include <stddef.h>
 
 #include "ArrayExprRewriter.h"
 #include "ArrayExprVisitor.h"
@@ -79,7 +79,7 @@ ref<Expr> ExprOptimizer::optimizeExpr(const ref<Expr> &e, bool valueOnly) {
     ConstantArrayExprVisitor aev(arrays);
     aev.visit(e);
 
-    if (arrays.size() == 0 || aev.isIncompatible()) {
+    if (arrays.empty() || aev.isIncompatible()) {
       // We do not optimize expressions other than those with concrete
       // arrays with a symbolic index
       // If we cannot optimize the expression, we return a failure only
@@ -93,7 +93,7 @@ ref<Expr> ExprOptimizer::optimizeExpr(const ref<Expr> &e, bool valueOnly) {
 
       // Compute those indexes s.t. orig_expr =equisat= (k==i|k==j|..)
       if (computeIndexes(arrays, e, idx_valIdx)) {
-        if (idx_valIdx.size() > 0) {
+        if (!idx_valIdx.empty()) {
           // Create new expression on indexes
           result = ExprRewriter::createOptExpr(e, arrays, idx_valIdx);
         } else {
@@ -122,7 +122,7 @@ ref<Expr> ExprOptimizer::optimizeExpr(const ref<Expr> &e, bool valueOnly) {
     are.visit(e);
     std::reverse(reads.begin(), reads.end());
 
-    if (reads.size() == 0 || are.isIncompatible()) {
+    if (reads.empty() || are.isIncompatible()) {
       cacheExprUnapplicable.insert(hash);
       return e;
     }
@@ -164,7 +164,7 @@ bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e,
       // In fact, they will be rejected by the MulExpr interpreter since it
       // will not find any integer solution
       Expr &e = *idxt_v.getMul();
-      ConstantExpr &ce = static_cast<ConstantExpr &>(e);
+      auto &ce = static_cast<ConstantExpr &>(e);
       uint64_t mulVal = (*ce.getAPValue().getRawData());
       // So far we try to limit this optimization, but we may try some more
       // aggressive conditions (i.e. mulVal > width)
@@ -174,7 +174,7 @@ bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e,
 
     // For each concrete value 'i' stored in the array
     for (size_t aIdx = 0; aIdx < arr->constantValues.size(); aIdx += width) {
-      Assignment *a = new Assignment();
+      auto *a = new Assignment();
       std::vector<const Array *> objects;
       std::vector<std::vector<unsigned char>> values;
 
@@ -193,8 +193,8 @@ bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e,
           if (idx_valIdx.find(idx) == idx_valIdx.end()) {
             idx_valIdx.insert(std::make_pair(idx, std::vector<ref<Expr>>()));
           }
-          idx_valIdx[idx]
-              .push_back(ConstantExpr::alloc(aIdx, arr->getDomain()));
+          idx_valIdx[idx].emplace_back(
+              ConstantExpr::alloc(aIdx, arr->getDomain()));
         }
       }
       delete a;
@@ -234,10 +234,10 @@ ref<Expr> ExprOptimizer::getSelectOptExpr(
              "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());
+        auto *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());
+        auto *arrayValue = static_cast<ConstantExpr *>(un->value.get());
         arrayConstValues[index] = arrayValue;
       }
       std::vector<uint64_t> arrayValues;
@@ -307,14 +307,13 @@ ref<Expr> ExprOptimizer::getSelectOptExpr(
         }
       }
       for (const UpdateNode *un = read->updates.head; un; un = un->next) {
-        ConstantExpr *ce = static_cast<ConstantExpr *>(un->index.get());
+        auto *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());
+          auto *arrayValue = static_cast<ConstantExpr *>(un->value.get());
           arrayConstValues[index] = arrayValue;
         }
       }
@@ -338,10 +337,10 @@ ref<Expr> ExprOptimizer::getSelectOptExpr(
           }
         }
         if (elementIsConcrete) {
-          arrayValues.push_back(std::make_pair(val, true));
+          arrayValues.emplace_back(val, true);
         } else {
           symByteNum++;
-          arrayValues.push_back(std::make_pair(0, false));
+          arrayValues.emplace_back(0, false);
         }
       }
 
@@ -389,16 +388,16 @@ ref<Expr> ExprOptimizer::buildConstantSelectExpr(
     uint64_t temp = arrayValues[i];
     unique_array_values.insert(curr_val);
     if (temp != curr_val) {
-      ranges.push_back(std::make_pair(curr_idx, i));
+      ranges.emplace_back(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));
+        ranges.emplace_back(curr_idx, i + 1);
         values.push_back(curr_val);
       }
     } else if (i == (arraySize - 1)) {
-      ranges.push_back(std::make_pair(curr_idx, i + 1));
+      ranges.emplace_back(curr_idx, i + 1);
       values.push_back(curr_val);
     }
   }
@@ -411,15 +410,14 @@ ref<Expr> ExprOptimizer::buildConstantSelectExpr(
   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));
+      exprMap[values[i]].emplace_back(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));
+      exprMap.find(values[i])->second.emplace_back(ranges[i].first,
+                                                   ranges[i].second);
     }
   }
 
@@ -529,23 +527,23 @@ ref<Expr> ExprOptimizer::buildMixedSelectExpr(
       uint64_t temp = arrayValues[i].first;
       unique_array_values.insert(temp);
       if (temp != curr_val) {
-        ranges.push_back(std::make_pair(curr_idx, i));
+        ranges.emplace_back(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));
+          ranges.emplace_back(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));
+        ranges.emplace_back(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));
+        ranges.emplace_back(curr_idx, i);
         values.push_back(curr_val);
       }
       curr_val = arrayValues[i + 1].first;
@@ -554,8 +552,8 @@ ref<Expr> ExprOptimizer::buildMixedSelectExpr(
     }
   }
 
-  assert(unique_array_values.size() > 0 && "No unique values");
-  assert(ranges.size() > 0 && "No ranges");
+  assert(!unique_array_values.empty() && "No unique values");
+  assert(!ranges.empty() && "No ranges");
 
   ref<Expr> result;
   if (((double)unique_array_values.size() / (double)(arraySize)) <=
@@ -563,7 +561,7 @@ ref<Expr> ExprOptimizer::buildMixedSelectExpr(
     // The final "else" expression will be the original unoptimized array read
     // expression
     unsigned range_start = 0;
-    if (holes.size() == 0) {
+    if (holes.empty()) {
       result = builder->Constant(llvm::APInt(width, values[0], false));
       range_start = 1;
     } else {
diff --git a/lib/Expr/ArrayExprOptimizer.h b/lib/Expr/ArrayExprOptimizer.h
index 7d895a48..40199821 100644
--- a/lib/Expr/ArrayExprOptimizer.h
+++ b/lib/Expr/ArrayExprOptimizer.h
@@ -24,8 +24,8 @@ namespace klee {
 
 enum ArrayOptimizationType { NONE, ALL, INDEX, VALUE };
 
-typedef std::map<const Array *, std::vector<ref<Expr>>> array2idx_ty;
-typedef std::map<ref<Expr>, std::vector<ref<Expr>>> mapIndexOptimizedExpr_ty;
+using array2idx_ty = std::map<const Array *, std::vector<ref<Expr>>>;
+using mapIndexOptimizedExpr_ty = std::map<ref<Expr>, std::vector<ref<Expr>>>;
 
 class ExprOptimizer {
 private:
diff --git a/lib/Expr/ArrayExprRewriter.cpp b/lib/Expr/ArrayExprRewriter.cpp
index 507ea753..7bbadd61 100644
--- a/lib/Expr/ArrayExprRewriter.cpp
+++ b/lib/Expr/ArrayExprRewriter.cpp
@@ -43,13 +43,13 @@ ref<Expr> ExprRewriter::rewrite(const ref<Expr> &e, const array2idx_ty &arrays,
            "Read is not aligned");
 
     Expr::Width width = idxt_v.getWidth() / element.first->range;
-    if (idxt_v.getMul().get()) {
+    if (!idxt_v.getMul().isNull()) {
       // If we have a MulExpr in the index, we can optimize our search by
       // skipping all those indexes that are not multiple of such value.
       // In fact, they will be rejected by the MulExpr interpreter since it
       // will not find any integer solution
       Expr &e = *idxt_v.getMul();
-      ConstantExpr &ce = static_cast<ConstantExpr &>(e);
+      auto &ce = static_cast<ConstantExpr &>(e);
       llvm::APInt val = ce.getAPValue();
       uint64_t mulVal = val.getZExtValue();
       // So far we try to limit this optimization, but we may try some more
@@ -64,7 +64,7 @@ ref<Expr> ExprRewriter::rewrite(const ref<Expr> &e, const array2idx_ty &arrays,
         continue;
       }
       auto opt_indexes = idx_valIdx.at((*index_it));
-      if (opt_indexes.size() == 0) {
+      if (opt_indexes.empty()) {
         // We continue with other solutions
         continue;
       } else if (opt_indexes.size() == 1) {
@@ -76,7 +76,7 @@ ref<Expr> ExprRewriter::rewrite(const ref<Expr> &e, const array2idx_ty &arrays,
         unsigned set = 0;
         BitArray ba(arr->size / width);
         for (auto &vals : opt_indexes) {
-          ConstantExpr &ce = static_cast<ConstantExpr &>(*vals);
+          auto &ce = static_cast<ConstantExpr &>(*vals);
           llvm::APInt v = ce.getAPValue();
           ba.set(v.getZExtValue() / width);
           set++;
@@ -120,7 +120,7 @@ ref<Expr> ExprRewriter::rewrite(const ref<Expr> &e, const array2idx_ty &arrays,
       }
     }
   }
-  if (eqExprs.size() == 0) {
+  if (eqExprs.empty()) {
     return notFound;
   } else if (eqExprs.size() == 1) {
     if (isa<AndExpr>(eqExprs[0])) {
diff --git a/lib/Expr/ArrayExprRewriter.h b/lib/Expr/ArrayExprRewriter.h
index 310ae8dd..2a7da998 100644
--- a/lib/Expr/ArrayExprRewriter.h
+++ b/lib/Expr/ArrayExprRewriter.h
@@ -19,8 +19,8 @@
 
 namespace klee {
 
-typedef std::map<const Array *, std::vector<ref<Expr>>> array2idx_ty;
-typedef std::map<ref<Expr>, std::vector<ref<Expr>>> mapIndexOptimizedExpr_ty;
+using array2idx_ty = std::map<const Array *, std::vector<ref<Expr>>>;
+using mapIndexOptimizedExpr_ty = std::map<ref<Expr>, std::vector<ref<Expr>>>;
 
 class ExprRewriter {
 public:
diff --git a/lib/Expr/ArrayExprVisitor.cpp b/lib/Expr/ArrayExprVisitor.cpp
index 407c4c64..e4ea9a1c 100644
--- a/lib/Expr/ArrayExprVisitor.cpp
+++ b/lib/Expr/ArrayExprVisitor.cpp
@@ -30,7 +30,7 @@ ReadExpr *ArrayExprHelper::hasOrderedReads(const ConcatExpr &ce) {
   // right now, all Reads are byte reads but some
   // transformations might change this
   if (!base || base->getWidth() != Expr::Int8)
-    return NULL;
+    return nullptr;
 
   // Get stride expr in proper index width.
   Expr::Width idxWidth = base->index->getWidth();
@@ -43,13 +43,13 @@ ReadExpr *ArrayExprHelper::hasOrderedReads(const ConcatExpr &ce) {
   while (e->getKind() == Expr::Concat) {
     offset = AddExpr::create(offset, strideExpr);
     if (!isReadExprAtOffset(e->getKid(0), base, offset))
-      return NULL;
+      return nullptr;
     e = e->getKid(1);
   }
 
   offset = AddExpr::create(offset, strideExpr);
   if (!isReadExprAtOffset(e, base, offset))
-    return NULL;
+    return nullptr;
 
   return cast<ReadExpr>(e.get());
 }
@@ -268,7 +268,7 @@ ExprVisitor::Action IndexCleanerVisitor::visitMul(const MulExpr &e) {
   return Action::doChildren();
 }
 
-ExprVisitor::Action IndexCleanerVisitor::visitRead(const ReadExpr &re) {
+ExprVisitor::Action IndexCleanerVisitor::visitRead(const ReadExpr &) {
   mul = false;
   return Action::doChildren();
 }
diff --git a/lib/Expr/ArrayExprVisitor.h b/lib/Expr/ArrayExprVisitor.h
index c1eb7f58..467b5dd3 100644
--- a/lib/Expr/ArrayExprVisitor.h
+++ b/lib/Expr/ArrayExprVisitor.h
@@ -32,35 +32,35 @@ public:
 //--------------------------- INDEX-BASED OPTIMIZATION-----------------------//
 class ConstantArrayExprVisitor : public ExprVisitor {
 private:
-  typedef std::map<const Array *, std::vector<ref<Expr>>> bindings_ty;
+  using bindings_ty = std::map<const Array *, std::vector<ref<Expr>>>;
   bindings_ty &arrays;
   // Avoids adding the same index twice
   std::unordered_set<unsigned> addedIndexes;
   bool incompatible;
 
 protected:
-  Action visitConcat(const ConcatExpr &);
-  Action visitRead(const ReadExpr &);
+  Action visitConcat(const ConcatExpr &) override;
+  Action visitRead(const ReadExpr &) override;
 
 public:
-  ConstantArrayExprVisitor(bindings_ty &_arrays)
+  explicit ConstantArrayExprVisitor(bindings_ty &_arrays)
       : arrays(_arrays), incompatible(false) {}
   inline bool isIncompatible() { return incompatible; }
 };
 
 class IndexCompatibilityExprVisitor : public ExprVisitor {
 private:
-  bool compatible;
-  bool inner;
+  bool compatible{true};
+  bool inner{false};
 
 protected:
-  Action visitRead(const ReadExpr &);
-  Action visitURem(const URemExpr &);
-  Action visitSRem(const SRemExpr &);
-  Action visitOr(const OrExpr &);
+  Action visitRead(const ReadExpr &) override;
+  Action visitURem(const URemExpr &) override;
+  Action visitSRem(const SRemExpr &) override;
+  Action visitOr(const OrExpr &) override;
 
 public:
-  IndexCompatibilityExprVisitor() : compatible(true), inner(false) {}
+  IndexCompatibilityExprVisitor() = default;
 
   inline bool isCompatible() { return compatible; }
   inline bool hasInnerReads() { return inner; }
@@ -73,11 +73,11 @@ private:
   ref<Expr> mul;
 
 protected:
-  Action visitConcat(const ConcatExpr &);
-  Action visitMul(const MulExpr &);
+  Action visitConcat(const ConcatExpr &) override;
+  Action visitMul(const MulExpr &) override;
 
 public:
-  IndexTransformationExprVisitor(const Array *_array)
+  explicit IndexTransformationExprVisitor(const Array *_array)
       : array(_array), width(Expr::InvalidWidth) {}
 
   inline Expr::Width getWidth() {
@@ -97,8 +97,8 @@ private:
   Action inspectRead(unsigned hash, Expr::Width width, const ReadExpr &);
 
 protected:
-  Action visitConcat(const ConcatExpr &);
-  Action visitRead(const ReadExpr &);
+  Action visitConcat(const ConcatExpr &) override;
+  Action visitRead(const ReadExpr &) override;
 
 public:
   ArrayReadExprVisitor(
@@ -116,26 +116,26 @@ private:
   std::map<unsigned, ref<Expr>> optimized;
 
 protected:
-  Action visitConcat(const ConcatExpr &);
-  Action visitRead(const ReadExpr &re);
+  Action visitConcat(const ConcatExpr &) override;
+  Action visitRead(const ReadExpr &re) override;
 
 public:
-  ArrayValueOptReplaceVisitor(std::map<unsigned, ref<Expr>> &_optimized,
-                              bool recursive = true)
+  explicit ArrayValueOptReplaceVisitor(
+      std::map<unsigned, ref<Expr>> &_optimized, bool recursive = true)
       : ExprVisitor(recursive), optimized(_optimized) {}
 };
 
 class IndexCleanerVisitor : public ExprVisitor {
 private:
-  bool mul;
+  bool mul{true};
   ref<Expr> index;
 
 protected:
-  Action visitMul(const MulExpr &);
-  Action visitRead(const ReadExpr &);
+  Action visitMul(const MulExpr &) override;
+  Action visitRead(const ReadExpr &) override;
 
 public:
-  IndexCleanerVisitor() : ExprVisitor(true), mul(true) {}
+  IndexCleanerVisitor() : ExprVisitor(true) {}
   inline ref<Expr> getIndex() { return index; }
 };
 } // namespace klee
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-25 08:16:58 +0000