about summary refs log tree commit diff homepage
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
parentacdb9a692d9eee8dd102befa4e101bfa5f028b0e (diff)
downloadklee-c763a4087f1d8fa4dbdfb9c8f30d545cdb66a0aa.tar.gz
Ref: implement operator bool()
-rw-r--r--include/klee/ADT/Ref.h13
-rw-r--r--include/klee/Expr/Expr.h4
-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
15 files changed, 37 insertions, 40 deletions
diff --git a/include/klee/ADT/Ref.h b/include/klee/ADT/Ref.h
index 92fd1740..7267f894 100644
--- a/include/klee/ADT/Ref.h
+++ b/include/klee/ADT/Ref.h
@@ -217,6 +217,7 @@ public:
   }
 
   bool isNull() const { return ptr == nullptr; }
+  explicit operator bool() const noexcept { return !isNull(); }
 
   // assumes non-null arguments
   int compare(const ref &rhs) const {
@@ -245,12 +246,12 @@ inline std::stringstream &operator<<(std::stringstream &os, const ref<T> &e) {
 } // end namespace klee
 
 namespace llvm {
-  // simplify_type implementation for ref<>, which allows dyn_cast from on a
-  // ref<> to apply to the wrapper type. Conceptually the result of such a
-  // dyn_cast should probably be a ref of the casted type, but that breaks the
-  // idiom of initializing a variable to the result of a dyn_cast inside an if
-  // condition, or we would have to implement operator(bool) for ref<> with
-  // isNull semantics, which doesn't seem like a good idea.
+// simplify_type implementation for ref<>, which allows dyn_cast on a
+// ref<> to apply to the wrapper type. Conceptually the result of such a
+// dyn_cast should probably be a ref of the casted type, which historically
+// was breaking the idiom of initializing a variable to the result of a dyn_cast
+// inside an if condition, as ref<> did not have an operator bool() with isNull
+// semantics.
 template<typename T>
 struct simplify_type<const ::klee::ref<T> > {
   using SimpleType = T *;
diff --git a/include/klee/Expr/Expr.h b/include/klee/Expr/Expr.h
index c5d1e7bb..b509294c 100644
--- a/include/klee/Expr/Expr.h
+++ b/include/klee/Expr/Expr.h
@@ -553,9 +553,7 @@ public:
   UpdateList &operator=(const UpdateList &b) = default;
 
   /// size of this update list
-  unsigned getSize() const {
-    return (head.get() != nullptr ? head->getSize() : 0);
-  }
+  unsigned getSize() const { return head ? head->getSize() : 0; }
 
   void extend(const ref<Expr> &index, const ref<Expr> &value);
 
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)) {