From 02fed84be089d81a5a9a812c2c8dd112f5e2fa71 Mon Sep 17 00:00:00 2001
From: Cristian Cadar <c.cadar@imperial.ac.uk>
Date: Fri, 3 Apr 2020 18:57:53 +0100
Subject: Removed include/klee/util and moved header files to appropriate
 places

---
 include/klee/ADT/BitArray.h                   |  42 ++++
 include/klee/ADT/Bits.h                       | 114 +++++++++++
 include/klee/ADT/Ref.h                        | 267 ++++++++++++++++++++++++++
 include/klee/Expr/ArrayExprOptimizer.h        |   2 +-
 include/klee/Expr/ArrayExprRewriter.h         |   2 +-
 include/klee/Expr/AssignmentGenerator.h       |   2 +-
 include/klee/Expr/Expr.h                      |   5 +-
 include/klee/Expr/ExprRangeEvaluator.h        |   2 +-
 include/klee/Expr/ExprSMTLIBPrinter.h         |   2 +-
 include/klee/Support/FloatEvaluation.h        |   5 +-
 include/klee/Support/IntEvaluation.h          |   2 +-
 include/klee/Support/PrintContext.h           | 102 ++++++++++
 include/klee/util/BitArray.h                  |  42 ----
 include/klee/util/Bits.h                      | 114 -----------
 include/klee/util/GetElementPtrTypeIterator.h | 154 ---------------
 include/klee/util/PrintContext.h              | 102 ----------
 include/klee/util/Ref.h                       | 267 --------------------------
 17 files changed, 536 insertions(+), 690 deletions(-)
 create mode 100644 include/klee/ADT/BitArray.h
 create mode 100644 include/klee/ADT/Bits.h
 create mode 100644 include/klee/ADT/Ref.h
 create mode 100644 include/klee/Support/PrintContext.h
 delete mode 100644 include/klee/util/BitArray.h
 delete mode 100644 include/klee/util/Bits.h
 delete mode 100644 include/klee/util/GetElementPtrTypeIterator.h
 delete mode 100644 include/klee/util/PrintContext.h
 delete mode 100644 include/klee/util/Ref.h

(limited to 'include')

diff --git a/include/klee/ADT/BitArray.h b/include/klee/ADT/BitArray.h
new file mode 100644
index 00000000..029e130f
--- /dev/null
+++ b/include/klee/ADT/BitArray.h
@@ -0,0 +1,42 @@
+//===-- BitArray.h ----------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_BITARRAY_H
+#define KLEE_BITARRAY_H
+
+namespace klee {
+
+  // XXX would be nice not to have
+  // two allocations here for allocated
+  // BitArrays
+class BitArray {
+private:
+  uint32_t *bits;
+  
+protected:
+  static uint32_t length(unsigned size) { return (size+31)/32; }
+
+public:
+  BitArray(unsigned size, bool value = false) : bits(new uint32_t[length(size)]) {
+    memset(bits, value?0xFF:0, sizeof(*bits)*length(size));
+  }
+  BitArray(const BitArray &b, unsigned size) : bits(new uint32_t[length(size)]) {
+    memcpy(bits, b.bits, sizeof(*bits)*length(size));
+  }
+  ~BitArray() { delete[] bits; }
+
+  bool get(unsigned idx) { return (bool) ((bits[idx/32]>>(idx&0x1F))&1); }
+  void set(unsigned idx) { bits[idx/32] |= 1<<(idx&0x1F); }
+  void unset(unsigned idx) { bits[idx/32] &= ~(1<<(idx&0x1F)); }
+  void set(unsigned idx, bool value) { if (value) set(idx); else unset(idx); }
+};
+
+} // End klee namespace
+
+#endif /* KLEE_BITARRAY_H */
diff --git a/include/klee/ADT/Bits.h b/include/klee/ADT/Bits.h
new file mode 100644
index 00000000..5f64e244
--- /dev/null
+++ b/include/klee/ADT/Bits.h
@@ -0,0 +1,114 @@
+//===-- Bits.h --------------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_BITS_H
+#define KLEE_BITS_H
+
+#include "klee/Config/Version.h"
+#include "llvm/Support/DataTypes.h"
+#include <assert.h>
+
+namespace klee {
+  namespace bits32 {
+    // @pre(0 <= N <= 32)
+    // @post(retval = max([truncateToNBits(i,N) for i in naturals()]))
+    inline unsigned maxValueOfNBits(unsigned N) {
+      assert(N <= 32);
+      if (N==0)
+        return 0;
+      return (UINT32_C(-1)) >> (32 - N);
+    }
+
+    // @pre(0 < N <= 32)
+    inline unsigned truncateToNBits(unsigned x, unsigned N) {
+      assert(N > 0 && N <= 32);
+      return x&((UINT32_C(-1)) >> (32 - N));
+    }
+
+    inline unsigned withoutRightmostBit(unsigned x) {
+      return x&(x-1);
+    }
+
+    inline unsigned isolateRightmostBit(unsigned x) {
+      return x&-x;
+    }
+
+    inline unsigned isPowerOfTwo(unsigned x) {
+      if (x==0) return 0;
+      return !(x&(x-1));
+    }
+
+    // @pre(withoutRightmostBit(x) == 0)
+    // @post((1 << retval) == x)
+    inline unsigned indexOfSingleBit(unsigned x) {
+      assert(withoutRightmostBit(x) == 0);
+      unsigned res = 0;
+      if (x&0xFFFF0000) res += 16;
+      if (x&0xFF00FF00) res += 8;
+      if (x&0xF0F0F0F0) res += 4;
+      if (x&0xCCCCCCCC) res += 2;
+      if (x&0xAAAAAAAA) res += 1;
+      assert(res < 32);
+      assert((UINT32_C(1) << res) == x);
+      return res;
+    } 
+
+    inline unsigned indexOfRightmostBit(unsigned x) {
+      return indexOfSingleBit(isolateRightmostBit(x));
+    }
+  }
+
+  namespace bits64 {
+    // @pre(0 <= N <= 64)
+    // @post(retval = max([truncateToNBits(i,N) for i in naturals()]))
+    inline uint64_t maxValueOfNBits(unsigned N) {
+      assert(N <= 64);
+      if (N==0)
+        return 0;
+      return ((UINT64_C(-1)) >> (64 - N));
+    }
+    
+    // @pre(0 < N <= 64)
+    inline uint64_t truncateToNBits(uint64_t x, unsigned N) {
+      assert(N > 0 && N <= 64);
+      return x&((UINT64_C(-1)) >> (64 - N));
+    }
+
+    inline uint64_t withoutRightmostBit(uint64_t x) {
+      return x&(x-1);
+    }
+
+    inline uint64_t isolateRightmostBit(uint64_t x) {
+      return x&-x;
+    }
+
+    inline uint64_t isPowerOfTwo(uint64_t x) {
+      if (x==0) return 0;
+      return !(x&(x-1));
+    }
+
+    // @pre((x&(x-1)) == 0)
+    // @post((1 << retval) == x)
+    inline unsigned indexOfSingleBit(uint64_t x) {
+      assert((x & (x - 1)) == 0);
+      unsigned res = bits32::indexOfSingleBit((unsigned) (x | (x>>32)));
+      if (x & (UINT64_C(0xFFFFFFFF) << 32))
+        res += 32;
+      assert(res < 64);
+      assert((UINT64_C(1) << res) == x);
+      return res;
+    } 
+
+    inline uint64_t indexOfRightmostBit(uint64_t x) {
+      return indexOfSingleBit(isolateRightmostBit(x));
+    }
+  }
+} // End klee namespace
+
+#endif /* KLEE_BITS_H */
diff --git a/include/klee/ADT/Ref.h b/include/klee/ADT/Ref.h
new file mode 100644
index 00000000..92fd1740
--- /dev/null
+++ b/include/klee/ADT/Ref.h
@@ -0,0 +1,267 @@
+//===-- Ref.h ---------------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+/**
+ * @file Ref.h
+ * @brief Implements smart-pointer ref<> used by KLEE.
+ *
+ * ## Basic usage:
+ *
+ * Add the following to your struct/class to enable ref<> pointer usage
+ * @code{.cpp}
+ *
+ * struct MyStruct{
+ *   ...
+ *   /// @brief Required by klee::ref-managed objects
+ *   class ReferenceCounter _refCount;
+ *   ...
+ * }
+ * @endcode
+ *
+ */
+
+#ifndef KLEE_REF_H
+#define KLEE_REF_H
+
+#include "llvm/Support/Casting.h"
+using llvm::isa;
+using llvm::cast;
+using llvm::cast_or_null;
+using llvm::dyn_cast;
+using llvm::dyn_cast_or_null;
+
+#include <cassert>
+#include <iosfwd> // FIXME: Remove this when LLVM 4.0 support is removed!!!
+
+namespace llvm {
+  class raw_ostream;
+} // namespace llvm
+
+namespace klee {
+
+template<class T>
+class ref;
+
+/// Reference counter to be used as part of a ref-managed struct or class
+class ReferenceCounter {
+  template<class T>
+  friend class ref;
+
+  /// Count how often the object has been referenced.
+  unsigned refCount = 0;
+
+public:
+  ReferenceCounter() = default;
+  ~ReferenceCounter() = default;
+
+  // Explicitly initialise reference counter with 0 again
+  // As this object is part of another object, the copy-constructor
+  // might be invoked as part of the other one.
+  ReferenceCounter(const ReferenceCounter& ) {}
+
+  /// Returns the number of parallel references of this objects
+  /// \return number of references on this object
+  unsigned getCount() {return refCount;}
+
+  // Copy assignment operator
+  ReferenceCounter &operator=(const ReferenceCounter &a) {
+    if (this == &a)
+      return *this;
+    // The new copy won't be referenced
+    refCount = 0;
+    return *this;
+  }
+
+  // Do not allow move operations for the reference counter
+  // as otherwise, references become incorrect.
+  ReferenceCounter(ReferenceCounter &&r) noexcept = delete;
+  ReferenceCounter &operator=(ReferenceCounter &&other) noexcept = delete;
+};
+
+template<class T>
+class ref {
+  T *ptr;
+
+public:
+  // default constructor: create a NULL reference
+  ref() : ptr(nullptr) {}
+  ~ref () { dec (); }
+
+private:
+  void inc() const {
+    if (ptr)
+      ++ptr->_refCount.refCount;
+  }
+
+  void dec() const {
+    if (ptr && --ptr->_refCount.refCount == 0)
+      delete ptr;
+  }
+
+public:
+  template<class U> friend class ref;
+
+  // constructor from pointer
+  ref(T *p) : ptr(p) {
+    inc();
+  }
+
+  // normal copy constructor
+  ref(const ref<T> &r) : ptr(r.ptr) {
+    inc();
+  }
+
+  // conversion constructor
+  template<class U>
+  ref (const ref<U> &r) : ptr(r.ptr) {
+    inc();
+  }
+
+  // normal move constructor: invoke the move assignment operator
+  ref(ref<T> &&r) noexcept : ptr(nullptr) { *this = std::move(r); }
+
+  // conversion move constructors: invoke the move assignment operator
+  template <class U> ref(ref<U> &&r) noexcept : ptr(nullptr) {
+    *this = std::move(r);
+  }
+
+  // pointer operations
+  T *get () const {
+    return ptr;
+  }
+
+  /* The copy assignment operator must also explicitly be defined,
+   * despite a redundant template. */
+  ref<T> &operator= (const ref<T> &r) {
+    r.inc();
+    // Create a copy of the pointer as the
+    // referenced object might get destroyed by the following dec(),
+    // like in the following example:
+    // ````````````````````````
+    //    Expr {
+    //        ref<Expr> next;
+    //    }
+    //
+    //    ref<Expr> root;
+    //    root = root->next;
+    // ````````````````````````
+    T *saved_ptr = r.ptr;
+    dec();
+    ptr = saved_ptr;
+
+    return *this;
+  }
+
+  template<class U> ref<T> &operator= (const ref<U> &r) {
+    r.inc();
+    // Create a copy of the pointer as the currently
+    // referenced object might get destroyed by the following dec(),
+    // like in the following example:
+    // ````````````````````````
+    //    Expr {
+    //        ref<Expr> next;
+    //    }
+    //
+    //    ref<Expr> root;
+    //    root = root->next;
+    // ````````````````````````
+
+    U *saved_ptr = r.ptr;
+    dec();
+    ptr = saved_ptr;
+
+    return *this;
+  }
+
+  // Move assignment operator
+  ref<T> &operator=(ref<T> &&r) noexcept {
+    if (this == &r)
+      return *this;
+    dec();
+    ptr = r.ptr;
+    r.ptr = nullptr;
+    return *this;
+  }
+
+  // Move assignment operator
+  template <class U> ref<T> &operator=(ref<U> &&r) noexcept {
+    if (static_cast<void *>(this) == static_cast<void *>(&r))
+      return *this;
+
+    // Do not swap as the types might be not compatible
+    // Decrement local counter to not hold reference anymore
+    dec();
+
+    // Assign to this ref
+    ptr = cast_or_null<T>(r.ptr);
+
+    // Invalidate old ptr
+    r.ptr = nullptr;
+
+    // Return this pointer
+    return *this;
+  }
+
+  T& operator*() const {
+    return *ptr;
+  }
+
+  T* operator->() const {
+    return ptr;
+  }
+
+  bool isNull() const { return ptr == nullptr; }
+
+  // assumes non-null arguments
+  int compare(const ref &rhs) const {
+    assert(!isNull() && !rhs.isNull() && "Invalid call to compare()");
+    return get()->compare(*rhs.get());
+  }
+
+  // assumes non-null arguments
+  bool operator<(const ref &rhs) const { return compare(rhs)<0; }
+  bool operator==(const ref &rhs) const { return compare(rhs)==0; }
+  bool operator!=(const ref &rhs) const { return compare(rhs)!=0; }
+};
+
+template<class T>
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const ref<T> &e) {
+  os << *e;
+  return os;
+}
+
+template<class T>
+inline std::stringstream &operator<<(std::stringstream &os, const ref<T> &e) {
+  os << *e;
+  return os;
+}
+
+} // 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.
+template<typename T>
+struct simplify_type<const ::klee::ref<T> > {
+  using SimpleType = T *;
+  static SimpleType getSimplifiedValue(const ::klee::ref<T> &Ref) {
+    return Ref.get();
+  }
+};
+
+template<typename T>
+struct simplify_type< ::klee::ref<T> >
+  : public simplify_type<const ::klee::ref<T> > {};
+}  // namespace llvm
+
+#endif /* KLEE_REF_H */
diff --git a/include/klee/Expr/ArrayExprOptimizer.h b/include/klee/Expr/ArrayExprOptimizer.h
index 8fc040e5..015ed1a2 100644
--- a/include/klee/Expr/ArrayExprOptimizer.h
+++ b/include/klee/Expr/ArrayExprOptimizer.h
@@ -17,9 +17,9 @@
 #include <utility>
 #include <vector>
 
+#include "klee/ADT/Ref.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Expr/ExprHashMap.h"
-#include "klee/util/Ref.h"
 
 namespace klee {
 
diff --git a/include/klee/Expr/ArrayExprRewriter.h b/include/klee/Expr/ArrayExprRewriter.h
index 098cb0a6..11627906 100644
--- a/include/klee/Expr/ArrayExprRewriter.h
+++ b/include/klee/Expr/ArrayExprRewriter.h
@@ -14,8 +14,8 @@
 #include <map>
 #include <vector>
 
+#include "klee/ADT/Ref.h"
 #include "klee/Expr/Expr.h"
-#include "klee/util/Ref.h"
 
 namespace klee {
 
diff --git a/include/klee/Expr/AssignmentGenerator.h b/include/klee/Expr/AssignmentGenerator.h
index 173b863e..cf656d91 100644
--- a/include/klee/Expr/AssignmentGenerator.h
+++ b/include/klee/Expr/AssignmentGenerator.h
@@ -10,8 +10,8 @@
 #ifndef KLEE_ASSIGNMENTGENERATOR_H
 #define KLEE_ASSIGNMENTGENERATOR_H
 
+#include "klee/ADT/Ref.h"
 #include "klee/Expr/Expr.h"
-#include "klee/util/Ref.h"
 
 #include <vector>
 
diff --git a/include/klee/Expr/Expr.h b/include/klee/Expr/Expr.h
index 374fc541..c5d1e7bb 100644
--- a/include/klee/Expr/Expr.h
+++ b/include/klee/Expr/Expr.h
@@ -10,9 +10,8 @@
 #ifndef KLEE_EXPR_H
 #define KLEE_EXPR_H
 
-#include "klee/util/Bits.h"
-#include "klee/util/Ref.h"
-
+#include "klee/ADT/Bits.h"
+#include "klee/ADT/Ref.h"
 #include "llvm/ADT/APFloat.h"
 #include "llvm/ADT/APInt.h"
 #include "llvm/ADT/DenseSet.h"
diff --git a/include/klee/Expr/ExprRangeEvaluator.h b/include/klee/Expr/ExprRangeEvaluator.h
index 540ccafd..a8a0f6b8 100644
--- a/include/klee/Expr/ExprRangeEvaluator.h
+++ b/include/klee/Expr/ExprRangeEvaluator.h
@@ -10,8 +10,8 @@
 #ifndef KLEE_EXPRRANGEEVALUATOR_H
 #define KLEE_EXPRRANGEEVALUATOR_H
 
+#include "klee/ADT/Bits.h"
 #include "klee/Expr/Expr.h"
-#include "klee/util/Bits.h"
 
 namespace klee {
 
diff --git a/include/klee/Expr/ExprSMTLIBPrinter.h b/include/klee/Expr/ExprSMTLIBPrinter.h
index 38ae2fa1..290caf7b 100644
--- a/include/klee/Expr/ExprSMTLIBPrinter.h
+++ b/include/klee/Expr/ExprSMTLIBPrinter.h
@@ -14,7 +14,7 @@
 #include "klee/Expr/Constraints.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Solver/Solver.h"
-#include "klee/util/PrintContext.h"
+#include "klee/Support/PrintContext.h"
 
 #include <map>
 #include <set>
diff --git a/include/klee/Support/FloatEvaluation.h b/include/klee/Support/FloatEvaluation.h
index 37392576..d6fcc73c 100644
--- a/include/klee/Support/FloatEvaluation.h
+++ b/include/klee/Support/FloatEvaluation.h
@@ -12,8 +12,9 @@
 #ifndef KLEE_FLOATEVALUATION_H
 #define KLEE_FLOATEVALUATION_H
 
-#include "klee/util/Bits.h"     //bits64::truncateToNBits
-#include "IntEvaluation.h" //ints::sext
+#include "IntEvaluation.h" // ints::sext
+
+#include "klee/ADT/Bits.h" // bits64::truncateToNBits
 
 #include "llvm/Support/ErrorHandling.h"
 #include "llvm/Support/MathExtras.h"
diff --git a/include/klee/Support/IntEvaluation.h b/include/klee/Support/IntEvaluation.h
index 27a8daf0..0e9a40d6 100644
--- a/include/klee/Support/IntEvaluation.h
+++ b/include/klee/Support/IntEvaluation.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_INTEVALUATION_H
 #define KLEE_INTEVALUATION_H
 
-#include "klee/util/Bits.h"
+#include "klee/ADT/Bits.h"
 
 #define MAX_BITS (sizeof(uint64_t) * 8)
 
diff --git a/include/klee/Support/PrintContext.h b/include/klee/Support/PrintContext.h
new file mode 100644
index 00000000..de9094da
--- /dev/null
+++ b/include/klee/Support/PrintContext.h
@@ -0,0 +1,102 @@
+//===-- PrintContext.h ------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_PRINTCONTEXT_H
+#define KLEE_PRINTCONTEXT_H
+
+#include "klee/Expr/Expr.h"
+
+#include "llvm/Support/raw_ostream.h"
+
+#include <sstream>
+#include <string>
+#include <stack>
+
+/// PrintContext - Helper class for pretty printing.
+/// It provides a basic wrapper around llvm::raw_ostream that keeps track of
+/// how many characters have been used on the current line.
+///
+/// It also provides an optional way keeping track of the various levels of indentation
+/// by using a stack.
+/// \sa breakLineI() , \sa pushIndent(), \sa popIndent()
+class PrintContext {
+private:
+  llvm::raw_ostream &os;
+  std::string newline;
+
+  ///This is used to keep track of the stack of indentations used by
+  /// \sa breakLineI()
+  /// \sa pushIndent()
+  /// \sa popIndent()
+  std::stack<unsigned int> indentStack;
+
+public:
+  /// Number of characters on the current line.
+  unsigned pos;
+
+  PrintContext(llvm::raw_ostream &_os) : os(_os), newline("\n"), indentStack(), pos()
+  {
+	  indentStack.push(pos);
+  }
+
+  void setNewline(const std::string &_newline) {
+    newline = _newline;
+  }
+
+  void breakLine(unsigned indent=0) {
+    os << newline;
+    if (indent)
+      os.indent(indent) << ' ';
+    pos = indent;
+  }
+
+  ///Break line using the indent on the top of the indent stack
+  /// \return The PrintContext object so the method is chainable
+  PrintContext& breakLineI()
+  {
+	  breakLine(indentStack.top());
+	  return *this;
+  }
+
+  ///Add the current position on the line to the top of the indent stack
+  /// \return The PrintContext object so the method is chainable
+  PrintContext& pushIndent()
+  {
+	  indentStack.push(pos);
+	  return *this;
+  }
+
+  ///Pop the top off the indent stack
+  /// \return The PrintContext object so the method is chainable
+  PrintContext& popIndent()
+  {
+	  indentStack.pop();
+	  return *this;
+  }
+
+  /// write - Output a string to the stream and update the
+  /// position. The stream should not have any newlines.
+  void write(const std::string &s) {
+    os << s;
+    pos += s.length();
+  }
+
+  template <typename T>
+  PrintContext &operator<<(T elt) {
+    std::string str;
+    llvm::raw_string_ostream ss(str);
+    ss << elt;
+    write(ss.str());
+    return *this;
+  }
+
+};
+
+
+#endif /* KLEE_PRINTCONTEXT_H */
diff --git a/include/klee/util/BitArray.h b/include/klee/util/BitArray.h
deleted file mode 100644
index 029e130f..00000000
--- a/include/klee/util/BitArray.h
+++ /dev/null
@@ -1,42 +0,0 @@
-//===-- BitArray.h ----------------------------------------------*- C++ -*-===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef KLEE_BITARRAY_H
-#define KLEE_BITARRAY_H
-
-namespace klee {
-
-  // XXX would be nice not to have
-  // two allocations here for allocated
-  // BitArrays
-class BitArray {
-private:
-  uint32_t *bits;
-  
-protected:
-  static uint32_t length(unsigned size) { return (size+31)/32; }
-
-public:
-  BitArray(unsigned size, bool value = false) : bits(new uint32_t[length(size)]) {
-    memset(bits, value?0xFF:0, sizeof(*bits)*length(size));
-  }
-  BitArray(const BitArray &b, unsigned size) : bits(new uint32_t[length(size)]) {
-    memcpy(bits, b.bits, sizeof(*bits)*length(size));
-  }
-  ~BitArray() { delete[] bits; }
-
-  bool get(unsigned idx) { return (bool) ((bits[idx/32]>>(idx&0x1F))&1); }
-  void set(unsigned idx) { bits[idx/32] |= 1<<(idx&0x1F); }
-  void unset(unsigned idx) { bits[idx/32] &= ~(1<<(idx&0x1F)); }
-  void set(unsigned idx, bool value) { if (value) set(idx); else unset(idx); }
-};
-
-} // End klee namespace
-
-#endif /* KLEE_BITARRAY_H */
diff --git a/include/klee/util/Bits.h b/include/klee/util/Bits.h
deleted file mode 100644
index 5f64e244..00000000
--- a/include/klee/util/Bits.h
+++ /dev/null
@@ -1,114 +0,0 @@
-//===-- Bits.h --------------------------------------------------*- C++ -*-===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef KLEE_BITS_H
-#define KLEE_BITS_H
-
-#include "klee/Config/Version.h"
-#include "llvm/Support/DataTypes.h"
-#include <assert.h>
-
-namespace klee {
-  namespace bits32 {
-    // @pre(0 <= N <= 32)
-    // @post(retval = max([truncateToNBits(i,N) for i in naturals()]))
-    inline unsigned maxValueOfNBits(unsigned N) {
-      assert(N <= 32);
-      if (N==0)
-        return 0;
-      return (UINT32_C(-1)) >> (32 - N);
-    }
-
-    // @pre(0 < N <= 32)
-    inline unsigned truncateToNBits(unsigned x, unsigned N) {
-      assert(N > 0 && N <= 32);
-      return x&((UINT32_C(-1)) >> (32 - N));
-    }
-
-    inline unsigned withoutRightmostBit(unsigned x) {
-      return x&(x-1);
-    }
-
-    inline unsigned isolateRightmostBit(unsigned x) {
-      return x&-x;
-    }
-
-    inline unsigned isPowerOfTwo(unsigned x) {
-      if (x==0) return 0;
-      return !(x&(x-1));
-    }
-
-    // @pre(withoutRightmostBit(x) == 0)
-    // @post((1 << retval) == x)
-    inline unsigned indexOfSingleBit(unsigned x) {
-      assert(withoutRightmostBit(x) == 0);
-      unsigned res = 0;
-      if (x&0xFFFF0000) res += 16;
-      if (x&0xFF00FF00) res += 8;
-      if (x&0xF0F0F0F0) res += 4;
-      if (x&0xCCCCCCCC) res += 2;
-      if (x&0xAAAAAAAA) res += 1;
-      assert(res < 32);
-      assert((UINT32_C(1) << res) == x);
-      return res;
-    } 
-
-    inline unsigned indexOfRightmostBit(unsigned x) {
-      return indexOfSingleBit(isolateRightmostBit(x));
-    }
-  }
-
-  namespace bits64 {
-    // @pre(0 <= N <= 64)
-    // @post(retval = max([truncateToNBits(i,N) for i in naturals()]))
-    inline uint64_t maxValueOfNBits(unsigned N) {
-      assert(N <= 64);
-      if (N==0)
-        return 0;
-      return ((UINT64_C(-1)) >> (64 - N));
-    }
-    
-    // @pre(0 < N <= 64)
-    inline uint64_t truncateToNBits(uint64_t x, unsigned N) {
-      assert(N > 0 && N <= 64);
-      return x&((UINT64_C(-1)) >> (64 - N));
-    }
-
-    inline uint64_t withoutRightmostBit(uint64_t x) {
-      return x&(x-1);
-    }
-
-    inline uint64_t isolateRightmostBit(uint64_t x) {
-      return x&-x;
-    }
-
-    inline uint64_t isPowerOfTwo(uint64_t x) {
-      if (x==0) return 0;
-      return !(x&(x-1));
-    }
-
-    // @pre((x&(x-1)) == 0)
-    // @post((1 << retval) == x)
-    inline unsigned indexOfSingleBit(uint64_t x) {
-      assert((x & (x - 1)) == 0);
-      unsigned res = bits32::indexOfSingleBit((unsigned) (x | (x>>32)));
-      if (x & (UINT64_C(0xFFFFFFFF) << 32))
-        res += 32;
-      assert(res < 64);
-      assert((UINT64_C(1) << res) == x);
-      return res;
-    } 
-
-    inline uint64_t indexOfRightmostBit(uint64_t x) {
-      return indexOfSingleBit(isolateRightmostBit(x));
-    }
-  }
-} // End klee namespace
-
-#endif /* KLEE_BITS_H */
diff --git a/include/klee/util/GetElementPtrTypeIterator.h b/include/klee/util/GetElementPtrTypeIterator.h
deleted file mode 100644
index cdbc36bc..00000000
--- a/include/klee/util/GetElementPtrTypeIterator.h
+++ /dev/null
@@ -1,154 +0,0 @@
-//===-- GetElementPtrTypeIterator.h -----------------------------*- C++ -*-===//
-//
-//                     The LLVM Compiler Infrastructure
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//
-// This file implements an iterator for walking through the types indexed by
-// getelementptr, insertvalue and extractvalue instructions.
-//
-// It is an enhanced version of llvm::gep_type_iterator which only handles
-// getelementptr.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef KLEE_GETELEMENTPTRTYPEITERATOR_H
-#define KLEE_GETELEMENTPTRTYPEITERATOR_H
-
-#include "llvm/IR/User.h"
-#include "llvm/IR/DerivedTypes.h"
-#include "llvm/IR/Instructions.h"
-#include "llvm/IR/Constants.h"
-
-#include "klee/Config/Version.h"
-
-namespace klee {
-template <typename ItTy = llvm::User::const_op_iterator>
-class generic_gep_type_iterator
-    : public std::iterator<std::forward_iterator_tag, llvm::Type *, ptrdiff_t> {
-  typedef std::iterator<std::forward_iterator_tag, llvm::Type *, ptrdiff_t>
-      super;
-
-    ItTy OpIt;
-    llvm::Type *CurTy;
-    generic_gep_type_iterator() {}
-
-    llvm::Value *asValue(llvm::Value *V) const { return V; }
-    llvm::Value *asValue(unsigned U) const {
-      return llvm::ConstantInt::get(CurTy->getContext(), llvm::APInt(32, U));
-    }
-
-  public:
-    static generic_gep_type_iterator begin(llvm::Type *Ty, ItTy It) {
-      generic_gep_type_iterator I;
-      I.CurTy = Ty;
-      I.OpIt = It;
-      return I;
-    }
-    static generic_gep_type_iterator end(ItTy It) {
-      generic_gep_type_iterator I;
-      I.CurTy = 0;
-      I.OpIt = It;
-      return I;
-    }
-
-    bool operator==(const generic_gep_type_iterator& x) const {
-      return OpIt == x.OpIt;
-    }
-    bool operator!=(const generic_gep_type_iterator& x) const {
-      return !operator==(x);
-    }
-
-    llvm::Type *operator*() const { return CurTy; }
-
-    llvm::Type *getIndexedType() const {
-      llvm::CompositeType *CT = cast<llvm::CompositeType>(CurTy);
-      return CT->getTypeAtIndex(getOperand());
-    }
-
-    // This is a non-standard operator->.  It allows you to call methods on the
-    // current type directly.
-    llvm::Type *operator->() const { return operator*(); }
-
-    llvm::Value *getOperand() const { return asValue(*OpIt); }
-
-    generic_gep_type_iterator& operator++() {   // Preincrement
-      if (llvm::CompositeType *CT = dyn_cast<llvm::CompositeType>(CurTy)) {
-        CurTy = CT->getTypeAtIndex(getOperand());
-#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
-      } else if (auto ptr = dyn_cast<llvm::PointerType>(CurTy)) {
-        CurTy = ptr->getElementType();
-#endif
-      } else {
-        CurTy = 0;
-      }
-      ++OpIt;
-      return *this;
-    }
-
-    generic_gep_type_iterator operator++(int) { // Postincrement
-      generic_gep_type_iterator tmp = *this; ++*this; return tmp;
-    }
-  };
-
-  typedef generic_gep_type_iterator<> gep_type_iterator;
-  typedef generic_gep_type_iterator<llvm::ExtractValueInst::idx_iterator> ev_type_iterator;
-  typedef generic_gep_type_iterator<llvm::InsertValueInst::idx_iterator> iv_type_iterator;
-  typedef generic_gep_type_iterator<llvm::SmallVector<unsigned, 4>::const_iterator> vce_type_iterator;
-
-  inline gep_type_iterator gep_type_begin(const llvm::User *GEP) {
-    return gep_type_iterator::begin(GEP->getOperand(0)->getType(),
-                                    GEP->op_begin()+1);
-  }
-  inline gep_type_iterator gep_type_end(const llvm::User *GEP) {
-    return gep_type_iterator::end(GEP->op_end());
-  }
-  inline gep_type_iterator gep_type_begin(const llvm::User &GEP) {
-    return gep_type_iterator::begin(GEP.getOperand(0)->getType(),
-                                    GEP.op_begin()+1);
-  }
-  inline gep_type_iterator gep_type_end(const llvm::User &GEP) {
-    return gep_type_iterator::end(GEP.op_end());
-  }
-
-  inline ev_type_iterator ev_type_begin(const llvm::ExtractValueInst *EV) {
-    return ev_type_iterator::begin(EV->getOperand(0)->getType(),
-                                   EV->idx_begin());
-  }
-  inline ev_type_iterator ev_type_end(const llvm::ExtractValueInst *EV) {
-    return ev_type_iterator::end(EV->idx_end());
-  }
-
-  inline iv_type_iterator iv_type_begin(const llvm::InsertValueInst *IV) {
-    return iv_type_iterator::begin(IV->getType(),
-                                   IV->idx_begin());
-  }
-  inline iv_type_iterator iv_type_end(const llvm::InsertValueInst *IV) {
-    return iv_type_iterator::end(IV->idx_end());
-  }
-
-  inline vce_type_iterator vce_type_begin(const llvm::ConstantExpr *CE) {
-    return vce_type_iterator::begin(CE->getOperand(0)->getType(),
-                                    CE->getIndices().begin());
-  }
-  inline vce_type_iterator vce_type_end(const llvm::ConstantExpr *CE) {
-    return vce_type_iterator::end(CE->getIndices().end());
-  }
-
-  template <typename ItTy>
-  inline generic_gep_type_iterator<ItTy> gep_type_begin(llvm::Type *Op0, ItTy I,
-                                                        ItTy E) {
-    return generic_gep_type_iterator<ItTy>::begin(Op0, I);
-  }
-
-  template <typename ItTy>
-  inline generic_gep_type_iterator<ItTy> gep_type_end(llvm::Type *Op0, ItTy I,
-                                                      ItTy E) {
-    return generic_gep_type_iterator<ItTy>::end(E);
-  }
-} // end namespace klee
-
-#endif /* KLEE_GETELEMENTPTRTYPEITERATOR_H */
diff --git a/include/klee/util/PrintContext.h b/include/klee/util/PrintContext.h
deleted file mode 100644
index de9094da..00000000
--- a/include/klee/util/PrintContext.h
+++ /dev/null
@@ -1,102 +0,0 @@
-//===-- PrintContext.h ------------------------------------------*- C++ -*-===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef KLEE_PRINTCONTEXT_H
-#define KLEE_PRINTCONTEXT_H
-
-#include "klee/Expr/Expr.h"
-
-#include "llvm/Support/raw_ostream.h"
-
-#include <sstream>
-#include <string>
-#include <stack>
-
-/// PrintContext - Helper class for pretty printing.
-/// It provides a basic wrapper around llvm::raw_ostream that keeps track of
-/// how many characters have been used on the current line.
-///
-/// It also provides an optional way keeping track of the various levels of indentation
-/// by using a stack.
-/// \sa breakLineI() , \sa pushIndent(), \sa popIndent()
-class PrintContext {
-private:
-  llvm::raw_ostream &os;
-  std::string newline;
-
-  ///This is used to keep track of the stack of indentations used by
-  /// \sa breakLineI()
-  /// \sa pushIndent()
-  /// \sa popIndent()
-  std::stack<unsigned int> indentStack;
-
-public:
-  /// Number of characters on the current line.
-  unsigned pos;
-
-  PrintContext(llvm::raw_ostream &_os) : os(_os), newline("\n"), indentStack(), pos()
-  {
-	  indentStack.push(pos);
-  }
-
-  void setNewline(const std::string &_newline) {
-    newline = _newline;
-  }
-
-  void breakLine(unsigned indent=0) {
-    os << newline;
-    if (indent)
-      os.indent(indent) << ' ';
-    pos = indent;
-  }
-
-  ///Break line using the indent on the top of the indent stack
-  /// \return The PrintContext object so the method is chainable
-  PrintContext& breakLineI()
-  {
-	  breakLine(indentStack.top());
-	  return *this;
-  }
-
-  ///Add the current position on the line to the top of the indent stack
-  /// \return The PrintContext object so the method is chainable
-  PrintContext& pushIndent()
-  {
-	  indentStack.push(pos);
-	  return *this;
-  }
-
-  ///Pop the top off the indent stack
-  /// \return The PrintContext object so the method is chainable
-  PrintContext& popIndent()
-  {
-	  indentStack.pop();
-	  return *this;
-  }
-
-  /// write - Output a string to the stream and update the
-  /// position. The stream should not have any newlines.
-  void write(const std::string &s) {
-    os << s;
-    pos += s.length();
-  }
-
-  template <typename T>
-  PrintContext &operator<<(T elt) {
-    std::string str;
-    llvm::raw_string_ostream ss(str);
-    ss << elt;
-    write(ss.str());
-    return *this;
-  }
-
-};
-
-
-#endif /* KLEE_PRINTCONTEXT_H */
diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h
deleted file mode 100644
index 92fd1740..00000000
--- a/include/klee/util/Ref.h
+++ /dev/null
@@ -1,267 +0,0 @@
-//===-- Ref.h ---------------------------------------------------*- C++ -*-===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-/**
- * @file Ref.h
- * @brief Implements smart-pointer ref<> used by KLEE.
- *
- * ## Basic usage:
- *
- * Add the following to your struct/class to enable ref<> pointer usage
- * @code{.cpp}
- *
- * struct MyStruct{
- *   ...
- *   /// @brief Required by klee::ref-managed objects
- *   class ReferenceCounter _refCount;
- *   ...
- * }
- * @endcode
- *
- */
-
-#ifndef KLEE_REF_H
-#define KLEE_REF_H
-
-#include "llvm/Support/Casting.h"
-using llvm::isa;
-using llvm::cast;
-using llvm::cast_or_null;
-using llvm::dyn_cast;
-using llvm::dyn_cast_or_null;
-
-#include <cassert>
-#include <iosfwd> // FIXME: Remove this when LLVM 4.0 support is removed!!!
-
-namespace llvm {
-  class raw_ostream;
-} // namespace llvm
-
-namespace klee {
-
-template<class T>
-class ref;
-
-/// Reference counter to be used as part of a ref-managed struct or class
-class ReferenceCounter {
-  template<class T>
-  friend class ref;
-
-  /// Count how often the object has been referenced.
-  unsigned refCount = 0;
-
-public:
-  ReferenceCounter() = default;
-  ~ReferenceCounter() = default;
-
-  // Explicitly initialise reference counter with 0 again
-  // As this object is part of another object, the copy-constructor
-  // might be invoked as part of the other one.
-  ReferenceCounter(const ReferenceCounter& ) {}
-
-  /// Returns the number of parallel references of this objects
-  /// \return number of references on this object
-  unsigned getCount() {return refCount;}
-
-  // Copy assignment operator
-  ReferenceCounter &operator=(const ReferenceCounter &a) {
-    if (this == &a)
-      return *this;
-    // The new copy won't be referenced
-    refCount = 0;
-    return *this;
-  }
-
-  // Do not allow move operations for the reference counter
-  // as otherwise, references become incorrect.
-  ReferenceCounter(ReferenceCounter &&r) noexcept = delete;
-  ReferenceCounter &operator=(ReferenceCounter &&other) noexcept = delete;
-};
-
-template<class T>
-class ref {
-  T *ptr;
-
-public:
-  // default constructor: create a NULL reference
-  ref() : ptr(nullptr) {}
-  ~ref () { dec (); }
-
-private:
-  void inc() const {
-    if (ptr)
-      ++ptr->_refCount.refCount;
-  }
-
-  void dec() const {
-    if (ptr && --ptr->_refCount.refCount == 0)
-      delete ptr;
-  }
-
-public:
-  template<class U> friend class ref;
-
-  // constructor from pointer
-  ref(T *p) : ptr(p) {
-    inc();
-  }
-
-  // normal copy constructor
-  ref(const ref<T> &r) : ptr(r.ptr) {
-    inc();
-  }
-
-  // conversion constructor
-  template<class U>
-  ref (const ref<U> &r) : ptr(r.ptr) {
-    inc();
-  }
-
-  // normal move constructor: invoke the move assignment operator
-  ref(ref<T> &&r) noexcept : ptr(nullptr) { *this = std::move(r); }
-
-  // conversion move constructors: invoke the move assignment operator
-  template <class U> ref(ref<U> &&r) noexcept : ptr(nullptr) {
-    *this = std::move(r);
-  }
-
-  // pointer operations
-  T *get () const {
-    return ptr;
-  }
-
-  /* The copy assignment operator must also explicitly be defined,
-   * despite a redundant template. */
-  ref<T> &operator= (const ref<T> &r) {
-    r.inc();
-    // Create a copy of the pointer as the
-    // referenced object might get destroyed by the following dec(),
-    // like in the following example:
-    // ````````````````````````
-    //    Expr {
-    //        ref<Expr> next;
-    //    }
-    //
-    //    ref<Expr> root;
-    //    root = root->next;
-    // ````````````````````````
-    T *saved_ptr = r.ptr;
-    dec();
-    ptr = saved_ptr;
-
-    return *this;
-  }
-
-  template<class U> ref<T> &operator= (const ref<U> &r) {
-    r.inc();
-    // Create a copy of the pointer as the currently
-    // referenced object might get destroyed by the following dec(),
-    // like in the following example:
-    // ````````````````````````
-    //    Expr {
-    //        ref<Expr> next;
-    //    }
-    //
-    //    ref<Expr> root;
-    //    root = root->next;
-    // ````````````````````````
-
-    U *saved_ptr = r.ptr;
-    dec();
-    ptr = saved_ptr;
-
-    return *this;
-  }
-
-  // Move assignment operator
-  ref<T> &operator=(ref<T> &&r) noexcept {
-    if (this == &r)
-      return *this;
-    dec();
-    ptr = r.ptr;
-    r.ptr = nullptr;
-    return *this;
-  }
-
-  // Move assignment operator
-  template <class U> ref<T> &operator=(ref<U> &&r) noexcept {
-    if (static_cast<void *>(this) == static_cast<void *>(&r))
-      return *this;
-
-    // Do not swap as the types might be not compatible
-    // Decrement local counter to not hold reference anymore
-    dec();
-
-    // Assign to this ref
-    ptr = cast_or_null<T>(r.ptr);
-
-    // Invalidate old ptr
-    r.ptr = nullptr;
-
-    // Return this pointer
-    return *this;
-  }
-
-  T& operator*() const {
-    return *ptr;
-  }
-
-  T* operator->() const {
-    return ptr;
-  }
-
-  bool isNull() const { return ptr == nullptr; }
-
-  // assumes non-null arguments
-  int compare(const ref &rhs) const {
-    assert(!isNull() && !rhs.isNull() && "Invalid call to compare()");
-    return get()->compare(*rhs.get());
-  }
-
-  // assumes non-null arguments
-  bool operator<(const ref &rhs) const { return compare(rhs)<0; }
-  bool operator==(const ref &rhs) const { return compare(rhs)==0; }
-  bool operator!=(const ref &rhs) const { return compare(rhs)!=0; }
-};
-
-template<class T>
-inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const ref<T> &e) {
-  os << *e;
-  return os;
-}
-
-template<class T>
-inline std::stringstream &operator<<(std::stringstream &os, const ref<T> &e) {
-  os << *e;
-  return os;
-}
-
-} // 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.
-template<typename T>
-struct simplify_type<const ::klee::ref<T> > {
-  using SimpleType = T *;
-  static SimpleType getSimplifiedValue(const ::klee::ref<T> &Ref) {
-    return Ref.get();
-  }
-};
-
-template<typename T>
-struct simplify_type< ::klee::ref<T> >
-  : public simplify_type<const ::klee::ref<T> > {};
-}  // namespace llvm
-
-#endif /* KLEE_REF_H */
-- 
cgit 1.4.1