aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Expr
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Expr')
-rw-r--r--lib/Expr/ArrayExprOptimizer.cpp17
-rw-r--r--lib/Expr/ArrayExprRewriter.cpp3
-rw-r--r--lib/Expr/ArrayExprVisitor.cpp6
-rw-r--r--lib/Expr/ExprBuilder.cpp2
-rw-r--r--lib/Expr/ExprEvaluator.cpp2
-rw-r--r--lib/Expr/ExprPPrinter.cpp4
-rw-r--r--lib/Expr/ExprSMTLIBPrinter.cpp2
-rw-r--r--lib/Expr/Updates.cpp6
8 files changed, 20 insertions, 22 deletions
diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp
index 8877efd5..a2367506 100644
--- a/lib/Expr/ArrayExprOptimizer.cpp
+++ b/lib/Expr/ArrayExprOptimizer.cpp
@@ -147,7 +147,7 @@ ref<Expr> ExprOptimizer::optimizeExpr(const ref<Expr> &e, bool valueOnly) {
result = ConstantExpr::create(0, Expr::Bool);
}
// Add new expression to cache
- if (result.get()) {
+ if (result) {
klee_warning("OPT_I: successful");
cacheExprOptimized[e] = result;
} else {
@@ -161,7 +161,7 @@ ref<Expr> ExprOptimizer::optimizeExpr(const ref<Expr> &e, bool valueOnly) {
}
// ----------------------- VALUE-BASED OPTIMIZATION -------------------------
if (OptimizeArray == VALUE ||
- (OptimizeArray == ALL && (!result.get() || valueOnly))) {
+ (OptimizeArray == ALL && (!result || valueOnly))) {
std::vector<const ReadExpr *> reads;
std::map<const ReadExpr *, std::pair<ref<Expr>, Expr::Width>> readInfo;
ArrayReadExprVisitor are(reads, readInfo);
@@ -175,7 +175,7 @@ ref<Expr> ExprOptimizer::optimizeExpr(const ref<Expr> &e, bool valueOnly) {
ref<Expr> selectOpt =
getSelectOptExpr(e, reads, readInfo, are.containsSymbolic());
- if (selectOpt.get()) {
+ if (selectOpt) {
klee_warning("OPT_V: successful");
result = selectOpt;
cacheExprOptimized[e] = result;
@@ -184,7 +184,7 @@ ref<Expr> ExprOptimizer::optimizeExpr(const ref<Expr> &e, bool valueOnly) {
cacheExprUnapplicable.insert(e);
}
}
- if (result.isNull())
+ if (!result)
return e;
return result;
}
@@ -204,12 +204,11 @@ bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e,
assert((idxt_v.getWidth() % arr->range == 0) && "Read is not aligned");
Expr::Width width = idxt_v.getWidth() / arr->range;
- if (idxt_v.getMul().get()) {
+ if (auto e = idxt_v.getMul()) {
// 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
- auto e = idxt_v.getMul();
auto ce = dyn_cast<ConstantExpr>(e);
assert(ce && "Not a constant expression");
uint64_t mulVal = (*ce->getAPValue().getRawData());
@@ -320,7 +319,7 @@ ref<Expr> ExprOptimizer::getSelectOptExpr(
ref<Expr> opt =
buildConstantSelectExpr(index, arrayValues, width, elementsInArray);
- if (opt.get()) {
+ if (opt) {
cacheReadExprOptimized[const_cast<ReadExpr *>(read)] = opt;
optimized.insert(std::make_pair(info.first, opt));
}
@@ -418,7 +417,7 @@ ref<Expr> ExprOptimizer::getSelectOptExpr(
// Build the dynamic select expression
ref<Expr> opt =
buildMixedSelectExpr(read, arrayValues, width, elementsInArray);
- if (opt.get()) {
+ if (opt) {
cacheReadExprOptimized[const_cast<ReadExpr *>(read)] = opt;
optimized.insert(std::make_pair(info.first, opt));
}
@@ -428,7 +427,7 @@ ref<Expr> ExprOptimizer::getSelectOptExpr(
toReturn = replacer.visit(e);
}
- return toReturn.get() ? toReturn : notFound;
+ return toReturn ? toReturn : notFound;
}
ref<Expr> ExprOptimizer::buildConstantSelectExpr(
diff --git a/lib/Expr/ArrayExprRewriter.cpp b/lib/Expr/ArrayExprRewriter.cpp
index 4de76d43..2732cdc4 100644
--- a/lib/Expr/ArrayExprRewriter.cpp
+++ b/lib/Expr/ArrayExprRewriter.cpp
@@ -44,12 +44,11 @@ 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().isNull()) {
+ if (auto e = idxt_v.getMul()) {
// 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
- auto e = idxt_v.getMul();
auto ce = dyn_cast<ConstantExpr>(e);
assert(ce && "Not a constant expression");
diff --git a/lib/Expr/ArrayExprVisitor.cpp b/lib/Expr/ArrayExprVisitor.cpp
index d3119754..c12689b3 100644
--- a/lib/Expr/ArrayExprVisitor.cpp
+++ b/lib/Expr/ArrayExprVisitor.cpp
@@ -132,7 +132,7 @@ ExprVisitor::Action ConstantArrayExprVisitor::visitRead(const ReadExpr &re) {
ExprVisitor::Action
IndexCompatibilityExprVisitor::visitRead(const ReadExpr &re) {
- if (!re.updates.head.isNull()) {
+ if (re.updates.head) {
compatible = false;
return Action::skipChildren();
} else if (re.updates.root->isConstantArray() &&
@@ -198,10 +198,10 @@ ExprVisitor::Action ArrayReadExprVisitor::inspectRead(ref<Expr> hash,
// pre(*): index is symbolic
if (!isa<ConstantExpr>(re.index)) {
if (readInfo.find(&re) == readInfo.end()) {
- if (re.updates.root->isSymbolicArray() && re.updates.head.isNull()) {
+ if (re.updates.root->isSymbolicArray() && !re.updates.head) {
return Action::doChildren();
}
- if (!re.updates.head.isNull()) {
+ if (re.updates.head) {
// Check preconditions on UpdateList nodes
bool hasConcreteValues = false;
for (const auto *un = re.updates.head.get(); un; un = un->next.get()) {
diff --git a/lib/Expr/ExprBuilder.cpp b/lib/Expr/ExprBuilder.cpp
index f8f57d35..2e5fcfbd 100644
--- a/lib/Expr/ExprBuilder.cpp
+++ b/lib/Expr/ExprBuilder.cpp
@@ -327,7 +327,7 @@ namespace {
const ref<Expr> &Index) {
// Roll back through writes when possible.
auto UN = Updates.head;
- while (!UN.isNull() && Eq(Index, UN->index)->isFalse())
+ while (UN && Eq(Index, UN->index)->isFalse())
UN = UN->next;
if (ConstantExpr *CE = dyn_cast<ConstantExpr>(Index))
diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp
index afd5d641..fb973def 100644
--- a/lib/Expr/ExprEvaluator.cpp
+++ b/lib/Expr/ExprEvaluator.cpp
@@ -13,7 +13,7 @@ using namespace klee;
ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul,
unsigned index) {
- for (auto un = ul.head; !un.isNull(); un = un->next) {
+ for (auto un = ul.head; un; un = un->next) {
ref<Expr> ui = visit(un->index);
if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ui)) {
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index ba0458ae..72544fbd 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -143,7 +143,7 @@ private:
auto head = updates.head;
// Special case empty list.
- if (head.isNull()) {
+ if (!head) {
// FIXME: We need to do something (assert, mangle, etc.) so that printing
// distinct arrays with the same name doesn't fail.
PC << updates.root->name;
@@ -154,7 +154,7 @@ private:
bool openedList = false, nextShouldBreak = false;
unsigned outerIndent = PC.pos;
unsigned middleIndent = 0;
- for (auto un = head; !un.isNull(); un = un->next) {
+ for (auto un = head; un; un = un->next) {
// We are done if we hit the cache.
std::map<const UpdateNode *, unsigned>::iterator it =
updateBindings.find(un.get());
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp
index 523e7f8c..8b651b04 100644
--- a/lib/Expr/ExprSMTLIBPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBPrinter.cpp
@@ -692,7 +692,7 @@ void ExprSMTLIBPrinter::printAction() {
}
void ExprSMTLIBPrinter::scan(const ref<Expr> &e) {
- assert(!(e.isNull()) && "found NULL expression");
+ assert(e && "found NULL expression");
if (isa<ConstantExpr>(e))
return; // we don't need to scan simple constants
diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp
index 4734f592..0ac832ad 100644
--- a/lib/Expr/Updates.cpp
+++ b/lib/Expr/Updates.cpp
@@ -25,7 +25,7 @@ UpdateNode::UpdateNode(const ref<UpdateNode> &_next, const ref<Expr> &_index,
"Update value should be 8-bit wide.");
*/
computeHash();
- size = next.isNull() ? 1 : 1 + next->size;
+ size = next ? next->size + 1 : 1;
}
extern "C" void vc_DeleteExpr(void*);
@@ -38,7 +38,7 @@ int UpdateNode::compare(const UpdateNode &b) const {
unsigned UpdateNode::computeHash() {
hashValue = index->hash() ^ value->hash();
- if (!next.isNull())
+ if (next)
hashValue ^= next->hash();
return hashValue;
}
@@ -88,7 +88,7 @@ unsigned UpdateList::hash() const {
unsigned res = 0;
for (unsigned i = 0, e = root->name.size(); i != e; ++i)
res = (res * Expr::MAGIC_HASH_CONSTANT) + root->name[i];
- if (head.get())
+ if (head)
res ^= head->hash();
return res;
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-14 14:12:59 +0000