aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Expr
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Expr')
-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 v1.2.3 (git 2.25.1) at 2026-01-23 05:33:15 +0000