aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorJulian Büning <julian.buening@rwth-aachen.de>2020-10-10 15:13:06 +0200
committerCristian Cadar <c.cadar@imperial.ac.uk>2020-11-12 10:13:54 +0000
commitc763a4087f1d8fa4dbdfb9c8f30d545cdb66a0aa (patch)
tree5d40c27ecfb16230aa3e714a3e7690b44b322860 /lib
parentacdb9a692d9eee8dd102befa4e101bfa5f028b0e (diff)
downloadklee-c763a4087f1d8fa4dbdfb9c8f30d545cdb66a0aa.tar.gz
Ref: implement operator bool()
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/ExecutionState.cpp2
-rw-r--r--lib/Core/Executor.cpp6
-rw-r--r--lib/Core/Memory.cpp6
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp2
-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
-rw-r--r--lib/Solver/IndependentSolver.cpp2
13 files changed, 29 insertions, 31 deletions
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 62376db6..97f97a8b 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -283,7 +283,7 @@ bool ExecutionState::merge(const ExecutionState &b) {
for (unsigned i=0; i<af.kf->numRegisters; i++) {
ref<Expr> &av = af.locals[i].value;
const ref<Expr> &bv = bf.locals[i].value;
- if (av.isNull() || bv.isNull()) {
+ if (!av || !bv) {
// if one is null then by implication (we are at same pc)
// we cannot reuse this local, so just ignore
} else {
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index e3e33aa2..13c25076 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -3048,11 +3048,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
r = ExtractExpr::create(agg, rOffset, agg->getWidth() - rOffset);
ref<Expr> result;
- if (!l.isNull() && !r.isNull())
+ if (l && r)
result = ConcatExpr::create(r, ConcatExpr::create(val, l));
- else if (!l.isNull())
+ else if (l)
result = ConcatExpr::create(val, l);
- else if (!r.isNull())
+ else if (r)
result = ConcatExpr::create(r, val);
else
result = val;
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index bf00ee4b..86b06701 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -135,7 +135,7 @@ ObjectState::~ObjectState() {
}
ArrayCache *ObjectState::getArrayCache() const {
- assert(!object.isNull() && "object was NULL");
+ assert(object && "object was NULL");
return object->parent->getArrayCache();
}
@@ -149,7 +149,7 @@ const UpdateList &ObjectState::getUpdates() const {
// FIXME: We should be able to do this more efficiently, we just need to be
// careful to get the interaction with the cache right. In particular we
// should avoid creating UpdateNode instances we never use.
- unsigned NumWrites = updates.head.isNull() ? 0 : updates.head->getSize();
+ unsigned NumWrites = updates.head ? updates.head->getSize() : 0;
std::vector< std::pair< ref<Expr>, ref<Expr> > > Writes(NumWrites);
const auto *un = updates.head.get();
for (unsigned i = NumWrites; i != 0; un = un->next.get()) {
@@ -219,7 +219,7 @@ void ObjectState::makeConcrete() {
}
void ObjectState::makeSymbolic() {
- assert(updates.head.isNull() &&
+ assert(!updates.head &&
"XXX makeSymbolic of objects with symbolic values is unsupported");
// XXX simplify this, can just delete various arrays I guess
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 6d54eb22..153619d3 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -464,7 +464,7 @@ void SpecialFunctionHandler::handleEhUnwindRaiseExceptionImpl(
"invalid number of arguments to _klee_eh_Unwind_RaiseException_impl");
ref<ConstantExpr> exceptionObject = dyn_cast<ConstantExpr>(arguments[0]);
- if (!exceptionObject.get()) {
+ if (!exceptionObject) {
executor.terminateStateOnError(state,
"Internal error: Symbolic exception pointer",
Executor::Unhandled);
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;
}
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 62632cd0..ed36816c 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -120,7 +120,7 @@ public:
const Array *array = re->updates.root;
// Reads of a constant array don't alias.
- if (re->updates.root->isConstantArray() && re->updates.head.isNull())
+ if (re->updates.root->isConstantArray() && !re->updates.head)
continue;
if (!wholeObjects.count(array)) {