Several fixes

build.sh

@@ -31,7 +31,7 @@ LLVM_VERSION=14
 ENABLE_OPTIMIZED=1
 ENABLE_DEBUG=0
 DISABLE_ASSERTIONS=1
-REQUIRES_RTTI=0
+REQUIRES_RTTI=1
 
 ## Solvers Required options
 # SOLVERS=STP

include/klee/ADT/DisjointSetUnion.h

@@ -21,7 +21,7 @@ DISABLE_WARNING_POP
 #include <vector>
 
 namespace klee {
-using ExprEitherSymcrete = either<Expr, Symcrete>;
+using ExprOrSymcrete = either<Expr, Symcrete>;
 
 template <typename ValueType, typename SetType,
           typename HASH = std::hash<ValueType>,

include/klee/ADT/Either.h

@@ -46,7 +46,6 @@ template <class T1, class T2> class either {
   virtual EitherKind getKind() const = 0;
 
   static bool classof(const either<T1, T2> *) { return true; }
-  // virtual unsigned hash() = 0;
   virtual int compare(const either<T1, T2> &b) = 0;
   virtual bool equals(const either<T1, T2> &b) = 0;
 
@@ -83,7 +82,6 @@ template <class T1, class T2> class either_left : public either<T1, T2> {
   }
   static bool classof(const either_left<T1, T2> *) { return true; }
 
-  // virtual unsigned hash() override { return value_->hash(); };
   virtual int compare(const either<T1, T2> &b) override {
     if (b.getKind() != getKind()) {
       return b.getKind() < getKind() ? -1 : 1;
@@ -134,7 +132,6 @@ template <class T1, class T2> class either_right : public either<T1, T2> {
   }
   static bool classof(const either_right<T1, T2> *) { return true; }
 
-  // virtual unsigned hash() override { return value_->hash(); };
   virtual int compare(const either<T1, T2> &b) override {
     if (b.getKind() != getKind()) {
       return b.getKind() < getKind() ? -1 : 1;

include/klee/ADT/SparseStorage.h

@@ -75,7 +75,7 @@ class SparseStorage {
     for (auto i : internalStorage) {
       sizeOfRange = std::max(i.first, sizeOfRange);
     }
-    return sizeOfRange;
+    return internalStorage.empty() ? 0 : sizeOfRange + 1;
   }
 
   bool operator==(const SparseStorage<ValueType> &another) const {

include/klee/Core/Interpreter.h

@@ -177,6 +177,8 @@ class Interpreter {
 
   virtual void setHaltExecution(HaltExecution::Reason value) = 0;
 
+  virtual HaltExecution::Reason getHaltExecution() = 0;
+
   virtual void setInhibitForking(bool value) = 0;
 
   virtual void prepareForEarlyExit() = 0;

include/klee/Core/TerminationTypes.h

@@ -97,6 +97,7 @@ enum Reason {
   CovCheck,
   NoMoreStates,
   ReachedTarget,
+  UnreachedTarget,
   ErrorOnWhichShouldExit,
   Interrupt,
   MaxDepth,

include/klee/Expr/AlphaBuilder.h

@@ -25,6 +25,7 @@ class AlphaBuilder final : public ExprVisitor {
 private:
   ArrayCache &arrayCache;
   unsigned index = 0;
+  bool reverse = false;
 
   const Array *visitArray(const Array *arr);
   UpdateList visitUpdateList(UpdateList u);
@@ -36,6 +37,7 @@ class AlphaBuilder final : public ExprVisitor {
   constraints_ty visitConstraints(constraints_ty cs);
   ref<Expr> build(ref<Expr> v);
   const Array *buildArray(const Array *arr) { return visitArray(arr); }
+  ref<Expr> reverseBuild(ref<Expr> v);
 };
 
 } // namespace klee

include/klee/Expr/IndependentConstraintSetUnion.h

@@ -8,11 +8,11 @@
 
 namespace klee {
 class IndependentConstraintSetUnion
-    : public DisjointSetUnion<ref<ExprEitherSymcrete>, IndependentConstraintSet,
-                              ExprEitherSymcreteHash, ExprEitherSymcreteCmp> {
+    : public DisjointSetUnion<ref<ExprOrSymcrete>, IndependentConstraintSet,
+                              ExprOrSymcreteHash, ExprOrSymcreteCmp> {
 public:
   Assignment concretization;
-  std::vector<ref<ExprEitherSymcrete>> constraintQueue;
+  std::vector<ref<ExprOrSymcrete>> constraintQueue;
   Assignment updateQueue;
   Assignment removeQueue;
 

include/klee/Expr/IndependentSet.h

@@ -22,17 +22,15 @@ DISABLE_WARNING_POP
 #include <vector>
 
 namespace klee {
-using ExprEitherSymcrete = either<Expr, Symcrete>;
+using ExprOrSymcrete = either<Expr, Symcrete>;
 
-struct ExprEitherSymcreteHash {
-  unsigned operator()(const ref<ExprEitherSymcrete> &e) const {
-    return e->hash();
-  }
+struct ExprOrSymcreteHash {
+  unsigned operator()(const ref<ExprOrSymcrete> &e) const { return e->hash(); }
 };
 
-struct ExprEitherSymcreteCmp {
-  bool operator()(const ref<ExprEitherSymcrete> &a,
-                  const ref<ExprEitherSymcrete> &b) const {
+struct ExprOrSymcreteCmp {
+  bool operator()(const ref<ExprOrSymcrete> &a,
+                  const ref<ExprOrSymcrete> &b) const {
     return a == b;
   }
 };
@@ -100,8 +98,8 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
 class IndependentConstraintSet {
 private:
   using InnerSetUnion =
-      DisjointSetUnion<ref<ExprEitherSymcrete>, IndependentConstraintSet,
-                       ExprEitherSymcreteHash, ExprEitherSymcreteCmp>;
+      DisjointSetUnion<ref<ExprOrSymcrete>, IndependentConstraintSet,
+                       ExprOrSymcreteHash, ExprOrSymcreteCmp>;
 
   void initIndependentConstraintSet(ref<Expr> e);
   void initIndependentConstraintSet(ref<Symcrete> s);
@@ -137,7 +135,7 @@ class IndependentConstraintSet {
                         Assignment &assign) const;
 
   IndependentConstraintSet();
-  explicit IndependentConstraintSet(ref<ExprEitherSymcrete> v);
+  explicit IndependentConstraintSet(ref<ExprOrSymcrete> v);
   IndependentConstraintSet(const IndependentConstraintSet &ics);
 
   void print(llvm::raw_ostream &os) const;

include/klee/Module/KModule.h

@@ -197,6 +197,12 @@ struct KBlockCompare {
   }
 };
 
+struct KFunctionCompare {
+  bool operator()(const KFunction *a, const KFunction *b) const {
+    return a->id < b->id;
+  }
+};
+
 class KConstant {
 public:
   /// Actual LLVM constant this represents.

lib/ADT/SparseStorage.cpp

@@ -18,7 +18,7 @@ void SparseStorage<unsigned char>::print(llvm::raw_ostream &os,
       if (firstPrinted) {
         os << ", ";
       }
-      os << element.first << ": " << element.second;
+      os << element.first << ": " << llvm::utostr(element.second);
       firstPrinted = true;
     }
     os << "} default: ";
@@ -35,7 +35,7 @@ void SparseStorage<unsigned char>::print(llvm::raw_ostream &os,
     }
     os << "] default: ";
   }
-  os << defaultValue;
+  os << llvm::utostr(defaultValue);
 }
 
 template <>

lib/Core/AddressManager.cpp

@@ -25,9 +25,15 @@ void *AddressManager::allocate(ref<Expr> address, uint64_t size) {
     }
   } else {
     if (sizeLocation == objects.end() || !sizeLocation->second) {
-      uint64_t newSize = (uint64_t)1
-                         << (sizeof(size) * CHAR_BIT -
-                             __builtin_clzll(std::max((uint64_t)1, size)));
+      uint64_t newSize = std::max((uint64_t)1, size);
+      int clz = __builtin_clzll(std::max((uint64_t)1, newSize));
+      int popcount = __builtin_popcountll(std::max((uint64_t)1, newSize));
+      if (popcount > 1) {
+        newSize = (uint64_t)1 << (sizeof(newSize) * CHAR_BIT - clz);
+      }
+      if (newSize > maxSize) {
+        newSize = std::max((uint64_t)1, size);
+      }
       assert(!objects.empty());
       MemoryObject *mo = objects.begin()->second;
       newMO = memory->allocate(newSize, mo->isLocal, mo->isGlobal,

lib/Core/ExecutionState.cpp

@@ -75,6 +75,7 @@ void ExecutionStack::pushFrame(KInstIterator caller, KFunction *kf) {
   ++stackBalance;
   assert(valueStack_.size() == callStack_.size());
   assert(valueStack_.size() == infoStack_.size());
+  stackSize += kf->getNumRegisters();
 }
 
 void ExecutionStack::popFrame() {
@@ -94,6 +95,7 @@ void ExecutionStack::popFrame() {
   --stackBalance;
   assert(valueStack_.size() == callStack_.size());
   assert(valueStack_.size() == infoStack_.size());
+  stackSize -= kf->getNumRegisters();
 }
 
 bool CallStackFrame::equals(const CallStackFrame &other) const {

lib/Core/ExecutionState.h

@@ -37,6 +37,7 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/IR/Function.h"
 DISABLE_WARNING_POP
 
+#include <cstddef>
 #include <deque>
 #include <map>
 #include <memory>
@@ -119,6 +120,7 @@ struct ExecutionStack {
   call_stack_ty callStack_;
   info_stack_ty infoStack_;
   call_stack_ty uniqueFrames_;
+  size_t stackSize = 0;
   unsigned stackBalance = 0;
 
 public:
@@ -133,6 +135,7 @@ struct ExecutionStack {
   inline const call_stack_ty &uniqueFrames() const { return uniqueFrames_; }
 
   inline unsigned size() const { return callStack_.size(); }
+  inline size_t stackRegisterSize() const { return stackSize; }
   inline bool empty() const { return callStack_.empty(); }
 };
 
@@ -377,7 +380,7 @@ class ExecutionState {
 
   ExprHashMap<std::pair<ref<Expr>, llvm::Type *>> gepExprBases;
 
-  ReachWithError error = ReachWithError::None;
+  mutable ReachWithError error = ReachWithError::None;
   std::atomic<HaltExecution::Reason> terminationReasonType{
       HaltExecution::NotHalt};