Removed the Internal directory from include/klee

9 files changed, 769 insertions, 0 deletions

diff --git a/include/klee/Support/CompressionStream.h b/include/klee/Support/CompressionStream.h
new file mode 100644
index 00000000..bc9119dd
--- /dev/null
+++ b/include/klee/Support/CompressionStream.h
@@ -0,0 +1,46 @@
+//===-- CompressionStream.h --------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_COMPRESSIONSTREAM_H
+#define KLEE_COMPRESSIONSTREAM_H
+
+#include "llvm/Support/raw_ostream.h"
+#include "zlib.h"
+
+namespace klee {
+const size_t BUFSIZE = 128 * 1024;
+
+class compressed_fd_ostream : public llvm::raw_ostream {
+  int FD;
+  uint8_t buffer[BUFSIZE];
+  z_stream strm;
+  uint64_t pos;
+
+  /// write_impl - See raw_ostream::write_impl.
+  virtual void write_impl(const char *Ptr, size_t Size);
+  void write_file(const char *Ptr, size_t Size);
+
+  virtual uint64_t current_pos() const { return pos; }
+
+  void flush_compressed_data();
+  void writeFullCompressedData();
+
+public:
+  /// compressed_fd_ostream - Open the specified file for writing. If an error
+  /// occurs, information about the error is put into ErrorInfo, and the stream
+  /// should be immediately destroyed; the string will be empty if no error
+  /// occurred. This allows optional flags to control how the file will be
+  /// opened.
+  compressed_fd_ostream(const std::string &Filename, std::string &ErrorInfo);
+
+  ~compressed_fd_ostream();
+};
+}
+
+#endif /* KLEE_COMPRESSIONSTREAM_H */
diff --git a/include/klee/Support/Debug.h b/include/klee/Support/Debug.h
new file mode 100644
index 00000000..0fe7906a
--- /dev/null
+++ b/include/klee/Support/Debug.h
@@ -0,0 +1,27 @@
+//===-- Debug.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_DEBUG_H
+#define KLEE_DEBUG_H
+
+#include "klee/Config/config.h"
+#include "llvm/Support/Debug.h"
+
+// We define wrappers around the LLVM DEBUG macros that are conditionalized on
+// whether the LLVM we are building against has the symbols needed by these
+// checks.
+
+#ifdef ENABLE_KLEE_DEBUG
+#define KLEE_DEBUG_WITH_TYPE(TYPE, X) DEBUG_WITH_TYPE(TYPE, X)
+#else
+#define KLEE_DEBUG_WITH_TYPE(TYPE, X) do { } while (0)
+#endif
+#define KLEE_DEBUG(X) KLEE_DEBUG_WITH_TYPE(DEBUG_TYPE, X)
+
+#endif /* KLEE_DEBUG_H */
diff --git a/include/klee/Support/ErrorHandling.h b/include/klee/Support/ErrorHandling.h
new file mode 100644
index 00000000..92762c03
--- /dev/null
+++ b/include/klee/Support/ErrorHandling.h
@@ -0,0 +1,51 @@
+//===-- ErrorHandling.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_ERRORHANDLING_H
+#define KLEE_ERRORHANDLING_H
+
+#ifdef __CYGWIN__
+#ifndef WINDOWS
+#define WINDOWS
+#endif
+#endif
+
+#include <stdio.h>
+
+namespace klee {
+
+extern FILE *klee_warning_file;
+extern FILE *klee_message_file;
+
+/// Print "KLEE: ERROR: " followed by the msg in printf format and a
+/// newline on stderr and to warnings.txt, then exit with an error.
+void klee_error(const char *msg, ...)
+    __attribute__((format(printf, 1, 2), noreturn));
+
+/// Print "KLEE: " followed by the msg in printf format and a
+/// newline on stderr and to messages.txt.
+void klee_message(const char *msg, ...) __attribute__((format(printf, 1, 2)));
+
+/// Print "KLEE: " followed by the msg in printf format and a
+/// newline to messages.txt.
+void klee_message_to_file(const char *msg, ...)
+    __attribute__((format(printf, 1, 2)));
+
+/// Print "KLEE: WARNING: " followed by the msg in printf format and a
+/// newline on stderr and to warnings.txt.
+void klee_warning(const char *msg, ...) __attribute__((format(printf, 1, 2)));
+
+/// Print "KLEE: WARNING: " followed by the msg in printf format and a
+/// newline on stderr and to warnings.txt. However, the warning is only
+/// printed once for each unique (id, msg) pair (as pointers).
+void klee_warning_once(const void *id, const char *msg, ...)
+    __attribute__((format(printf, 2, 3)));
+}
+
+#endif /* KLEE_ERRORHANDLING_H */
diff --git a/include/klee/Support/FileHandling.h b/include/klee/Support/FileHandling.h
new file mode 100644
index 00000000..90ce20b3
--- /dev/null
+++ b/include/klee/Support/FileHandling.h
@@ -0,0 +1,27 @@
+//===-- FileHandling.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_FILEHANDLING_H
+#define KLEE_FILEHANDLING_H
+
+#include "llvm/Support/raw_ostream.h"
+#include <memory>
+#include <string>
+
+namespace klee {
+std::unique_ptr<llvm::raw_fd_ostream>
+klee_open_output_file(const std::string &path, std::string &error);
+
+#ifdef HAVE_ZLIB_H
+std::unique_ptr<llvm::raw_ostream>
+klee_open_compressed_output_file(const std::string &path, std::string &error);
+#endif
+} // namespace klee
+
+#endif /* KLEE_FILEHANDLING_H */
diff --git a/include/klee/Support/FloatEvaluation.h b/include/klee/Support/FloatEvaluation.h
new file mode 100644
index 00000000..37392576
--- /dev/null
+++ b/include/klee/Support/FloatEvaluation.h
@@ -0,0 +1,263 @@
+//===-- FloatEvaluation.h ---------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+// FIXME: Ditch this and use APFloat.
+
+#ifndef KLEE_FLOATEVALUATION_H
+#define KLEE_FLOATEVALUATION_H
+
+#include "klee/util/Bits.h"     //bits64::truncateToNBits
+#include "IntEvaluation.h" //ints::sext
+
+#include "llvm/Support/ErrorHandling.h"
+#include "llvm/Support/MathExtras.h"
+
+#include <cassert>
+
+namespace klee {
+namespace floats {
+
+// ********************************** //
+// *** Pack uint64_t into FP types ** //
+// ********************************** //
+
+// interpret the 64 bits as a double instead of a uint64_t
+inline double UInt64AsDouble( uint64_t bits ) {
+  double ret;
+  assert( sizeof(bits) == sizeof(ret) );
+  memcpy( &ret, &bits, sizeof bits );
+  return ret;
+}
+
+// interpret the first 32 bits as a float instead of a uint64_t
+inline float UInt64AsFloat( uint64_t bits ) {
+  uint32_t tmp = bits; // ensure that we read correct bytes
+  float ret;
+  assert( sizeof(tmp) == sizeof(ret) );
+  memcpy( &ret, &tmp, sizeof tmp );
+  return ret;
+}
+
+
+// ********************************** //
+// *** Pack FP types into uint64_t ** //
+// ********************************** //
+
+// interpret the 64 bits as a uint64_t instead of a double
+inline uint64_t DoubleAsUInt64( double d ) {
+  uint64_t ret;
+  assert( sizeof(d) == sizeof(ret) );
+  memcpy( &ret, &d, sizeof d );
+  return ret;
+}
+
+// interpret the 32 bits as a uint64_t instead of as a float (add 32 0s)
+inline uint64_t FloatAsUInt64( float f ) {
+  uint32_t tmp;
+  assert( sizeof(tmp) == sizeof(f) );
+  memcpy( &tmp, &f, sizeof f );
+  return (uint64_t)tmp;
+}
+
+
+// ********************************** //
+// ************ Constants *********** //
+// ********************************** //
+
+const unsigned FLT_BITS = 32;
+const unsigned DBL_BITS = 64;
+
+
+
+// ********************************** //
+// ***** LLVM Binary Operations ***** //
+// ********************************** //
+
+// add of l and r
+inline uint64_t add(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l)  + UInt64AsFloat(r)),  FLT_BITS);
+  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) + UInt64AsDouble(r)), DBL_BITS);
+  default: llvm::report_fatal_error("unsupported floating point width");
+  }
+}
+
+// difference of l and r
+inline uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l)  - UInt64AsFloat(r)),  FLT_BITS);
+  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) - UInt64AsDouble(r)), DBL_BITS);
+  default: llvm::report_fatal_error("unsupported floating point width");
+  }
+}
+
+// product of l and r
+inline uint64_t mul(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l)  * UInt64AsFloat(r)),  FLT_BITS);
+  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) * UInt64AsDouble(r)), DBL_BITS);
+  default: llvm::report_fatal_error("unsupported floating point width");
+  }
+}
+
+// signed divide of l by r
+inline uint64_t div(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l)  / UInt64AsFloat(r)),  FLT_BITS);
+  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) / UInt64AsDouble(r)), DBL_BITS);
+  default: llvm::report_fatal_error("unsupported floating point width");
+  }
+}
+
+// signed modulo of l by r
+inline uint64_t mod(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64( fmod(UInt64AsFloat(l),  UInt64AsFloat(r)) ), FLT_BITS);
+  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64( fmod(UInt64AsDouble(l), UInt64AsDouble(r)) ), DBL_BITS);
+  default: llvm::report_fatal_error("unsupported floating point width");
+  }
+}
+
+
+// ********************************** //
+// *** LLVM Comparison Operations *** //
+// ********************************** //
+
+// determine if l represents NaN
+inline bool isNaN(uint64_t l, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS:
+    return std::isnan(UInt64AsFloat(l));
+  case DBL_BITS:
+    return std::isnan(UInt64AsDouble(l));
+  default: llvm::report_fatal_error("unsupported floating point width");
+  }
+}
+
+inline uint64_t eq(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return UInt64AsFloat(l)  == UInt64AsFloat(r);
+  case DBL_BITS: return UInt64AsDouble(l) == UInt64AsDouble(r);
+  default: llvm::report_fatal_error("unsupported floating point width");
+  }
+}
+
+inline uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return UInt64AsFloat(l)  != UInt64AsFloat(r);
+  case DBL_BITS: return UInt64AsDouble(l) != UInt64AsDouble(r);
+  default: llvm::report_fatal_error("unsupported floating point width");
+  }
+}
+
+inline uint64_t lt(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return UInt64AsFloat(l)  < UInt64AsFloat(r);
+  case DBL_BITS: return UInt64AsDouble(l) < UInt64AsDouble(r);
+  default: llvm::report_fatal_error("unsupported floating point width");
+  }
+}
+
+inline uint64_t le(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return UInt64AsFloat(l)  <= UInt64AsFloat(r);
+  case DBL_BITS: return UInt64AsDouble(l) <= UInt64AsDouble(r);
+  default: llvm::report_fatal_error("unsupported floating point width");
+  }
+}
+
+inline uint64_t gt(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return UInt64AsFloat(l)  > UInt64AsFloat(r);
+  case DBL_BITS: return UInt64AsDouble(l) > UInt64AsDouble(r);
+  default: llvm::report_fatal_error("unsupported floating point width");
+  }
+}
+
+inline uint64_t ge(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return UInt64AsFloat(l)  >= UInt64AsFloat(r);
+  case DBL_BITS: return UInt64AsDouble(l) >= UInt64AsDouble(r);
+  default: llvm::report_fatal_error("unsupported floating point width");
+  }
+}
+
+
+// ********************************** //
+// *** LLVM Conversion Operations *** //
+// ********************************** //
+
+// truncation of l (which must be a double) to float (casts a double to a float)
+inline uint64_t trunc(uint64_t l, unsigned outWidth, unsigned inWidth) {
+  // FIXME: Investigate this, should this not happen? Was a quick
+  // patch for busybox.
+  if (inWidth==64 && outWidth==64) {
+    return l;
+  } else {
+    assert(inWidth==64 && "can only truncate from a 64-bit double");
+    assert(outWidth==32 && "can only truncate to a 32-bit float");
+    float trunc = (float)UInt64AsDouble(l);
+    return bits64::truncateToNBits(FloatAsUInt64(trunc), outWidth);
+  }
+}
+
+// extension of l (which must be a float) to double (casts a float to a double)
+inline uint64_t ext(uint64_t l, unsigned outWidth, unsigned inWidth) {
+  // FIXME: Investigate this, should this not happen? Was a quick
+  // patch for busybox.
+  if (inWidth==64 && outWidth==64) {
+    return l;
+  } else {
+    assert(inWidth==32 && "can only extend from a 32-bit float");
+    assert(outWidth==64 && "can only extend to a 64-bit double");
+    double ext = (double)UInt64AsFloat(l);
+    return bits64::truncateToNBits(DoubleAsUInt64(ext), outWidth);
+  }
+}
+
+// conversion of l to an unsigned integer, rounding towards zero
+inline uint64_t toUnsignedInt( uint64_t l, unsigned outWidth, unsigned inWidth ) {
+  switch( inWidth ) {
+  case FLT_BITS: return bits64::truncateToNBits((uint64_t)UInt64AsFloat(l),  outWidth );
+  case DBL_BITS: return bits64::truncateToNBits((uint64_t)UInt64AsDouble(l), outWidth );
+  default: llvm::report_fatal_error("unsupported floating point width");
+  }
+}
+
+// conversion of l to a signed integer, rounding towards zero
+inline uint64_t toSignedInt( uint64_t l, unsigned outWidth, unsigned inWidth ) {
+  switch( inWidth ) {
+  case FLT_BITS: return bits64::truncateToNBits((int64_t)UInt64AsFloat(l),  outWidth);
+  case DBL_BITS: return bits64::truncateToNBits((int64_t)UInt64AsDouble(l), outWidth);
+  default: llvm::report_fatal_error("unsupported floating point width");
+  }
+}
+
+// conversion of l, interpreted as an unsigned int, to a floating point number
+inline uint64_t UnsignedIntToFP( uint64_t l, unsigned outWidth ) {
+  switch( outWidth ) {
+  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64((float)l),  outWidth);
+  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64((double)l), outWidth);
+  default: llvm::report_fatal_error("unsupported floating point width");
+  }
+}
+
+// conversion of l, interpreted as a signed int, to a floating point number
+inline uint64_t SignedIntToFP( uint64_t l, unsigned outWidth, unsigned inWidth ) {
+  switch( outWidth ) {
+  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64((float)(int64_t)ints::sext(l, 64, inWidth)), outWidth);
+  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64((double)(int64_t)ints::sext(l,64, inWidth)), outWidth);
+  default: llvm::report_fatal_error("unsupported floating point width");
+  }
+}
+
+} // end namespace ints
+} // end namespace klee
+
+#endif /* KLEE_FLOATEVALUATION_H */
diff --git a/include/klee/Support/IntEvaluation.h b/include/klee/Support/IntEvaluation.h
new file mode 100644
index 00000000..27a8daf0
--- /dev/null
+++ b/include/klee/Support/IntEvaluation.h
@@ -0,0 +1,164 @@
+//===-- IntEvaluation.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_INTEVALUATION_H
+#define KLEE_INTEVALUATION_H
+
+#include "klee/util/Bits.h"
+
+#define MAX_BITS (sizeof(uint64_t) * 8)
+
+// ASSUMPTION: invalid bits in each uint64_t are 0. the trade-off here is
+// between making trunc/zext/sext fast and making operations that depend
+// on the invalid bits being 0 fast. 
+
+namespace klee {
+namespace ints {
+
+// add of l and r
+inline uint64_t add(uint64_t l, uint64_t r, unsigned inWidth) {
+  return bits64::truncateToNBits(l + r, inWidth);
+}
+
+// difference of l and r
+inline uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth) {
+  return bits64::truncateToNBits(l - r, inWidth);
+}
+
+// product of l and r
+inline uint64_t mul(uint64_t l, uint64_t r, unsigned inWidth) {
+  return bits64::truncateToNBits(l * r, inWidth);
+}
+
+// truncation of l to outWidth bits
+inline uint64_t trunc(uint64_t l, unsigned outWidth, unsigned inWidth) {
+  return bits64::truncateToNBits(l, outWidth);
+}
+
+// zero-extension of l from inWidth to outWidth bits
+inline uint64_t zext(uint64_t l, unsigned outWidth, unsigned inWidth) {
+  return l;
+}
+
+// sign-extension of l from inWidth to outWidth bits
+inline uint64_t sext(uint64_t l, unsigned outWidth, unsigned inWidth) {
+  uint32_t numInvalidBits = MAX_BITS - inWidth;
+  return bits64::truncateToNBits(((int64_t)(l << numInvalidBits)) >> numInvalidBits, outWidth);
+}
+
+// unsigned divide of l by r
+inline uint64_t udiv(uint64_t l, uint64_t r, unsigned inWidth) {
+  return bits64::truncateToNBits(l / r, inWidth);
+}
+
+// unsigned mod of l by r
+inline uint64_t urem(uint64_t l, uint64_t r, unsigned inWidth) {
+  return bits64::truncateToNBits(l % r, inWidth);
+}
+
+// signed divide of l by r
+inline uint64_t sdiv(uint64_t l, uint64_t r, unsigned inWidth) {
+  // sign extend operands so that signed operation on 64-bits works correctly
+  int64_t sl = sext(l, MAX_BITS, inWidth);
+  int64_t sr = sext(r, MAX_BITS, inWidth);
+  return bits64::truncateToNBits(sl / sr, inWidth);
+}
+
+// signed mod of l by r
+inline uint64_t srem(uint64_t l, uint64_t r, unsigned inWidth) {
+  // sign extend operands so that signed operation on 64-bits works correctly
+  int64_t sl = sext(l, MAX_BITS, inWidth);
+  int64_t sr = sext(r, MAX_BITS, inWidth);
+  return bits64::truncateToNBits(sl % sr, inWidth);
+}
+
+// arithmetic shift right of l by r bits
+inline uint64_t ashr(uint64_t l, uint64_t shift, unsigned inWidth) {
+  int64_t sl = sext(l, MAX_BITS, inWidth);
+  return bits64::truncateToNBits(sl >> shift, inWidth);
+}
+
+// logical shift right of l by r bits
+inline uint64_t lshr(uint64_t l, uint64_t shift, unsigned inWidth) {
+  return l >> shift;
+}
+
+// shift left of l by r bits
+inline uint64_t shl(uint64_t l, uint64_t shift, unsigned inWidth) {
+  return bits64::truncateToNBits(l << shift, inWidth);
+}
+
+// logical AND of l and r
+inline uint64_t land(uint64_t l, uint64_t r, unsigned inWidth) {
+  return l & r;
+}
+
+// logical OR of l and r
+inline uint64_t lor(uint64_t l, uint64_t r, unsigned inWidth) {
+  return l | r;
+}
+
+// logical XOR of l and r
+inline uint64_t lxor(uint64_t l, uint64_t r, unsigned inWidth) {
+  return l ^ r;
+}
+
+// comparison operations
+inline uint64_t eq(uint64_t l, uint64_t r, unsigned inWidth) {
+  return l == r;
+}
+
+inline uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth) {
+  return l != r;
+}
+
+inline uint64_t ult(uint64_t l, uint64_t r, unsigned inWidth) {
+  return l < r;
+}
+
+inline uint64_t ule(uint64_t l, uint64_t r, unsigned inWidth) {
+  return l <= r;
+}
+
+inline uint64_t ugt(uint64_t l, uint64_t r, unsigned inWidth) {
+  return l > r;
+}
+
+inline uint64_t uge(uint64_t l, uint64_t r, unsigned inWidth) {
+  return l >= r;
+}
+
+inline uint64_t slt(uint64_t l, uint64_t r, unsigned inWidth) {
+  int64_t sl = sext(l, MAX_BITS, inWidth);
+  int64_t sr = sext(r, MAX_BITS, inWidth);
+  return sl < sr;
+}
+
+inline uint64_t sle(uint64_t l, uint64_t r, unsigned inWidth) {
+  int64_t sl = sext(l, MAX_BITS, inWidth);
+  int64_t sr = sext(r, MAX_BITS, inWidth);
+  return sl <= sr;
+}
+
+inline uint64_t sgt(uint64_t l, uint64_t r, unsigned inWidth) {
+  int64_t sl = sext(l, MAX_BITS, inWidth);
+  int64_t sr = sext(r, MAX_BITS, inWidth);
+  return sl > sr;
+}
+
+inline uint64_t sge(uint64_t l, uint64_t r, unsigned inWidth) {
+  int64_t sl = sext(l, MAX_BITS, inWidth);
+  int64_t sr = sext(r, MAX_BITS, inWidth);
+  return sl >= sr;
+}
+
+} // end namespace ints
+} // end namespace klee
+
+#endif /* KLEE_INTEVALUATION_H */
diff --git a/include/klee/Support/ModuleUtil.h b/include/klee/Support/ModuleUtil.h
new file mode 100644
index 00000000..e80fc673
--- /dev/null
+++ b/include/klee/Support/ModuleUtil.h
@@ -0,0 +1,70 @@
+//===-- ModuleUtil.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_MODULEUTIL_H
+#define KLEE_MODULEUTIL_H
+
+#include "klee/Config/Version.h"
+
+#include "llvm/IR/CallSite.h"
+#include "llvm/IR/Module.h"
+
+#include <memory>
+#include <string>
+#include <vector>
+
+namespace klee {
+
+/// Links all the modules together into one and returns it.
+///
+/// All the modules which are used for resolving entities are freed,
+/// all the remaining ones are preserved.
+///
+/// @param modules List of modules to link together: if resolveOnly true,
+/// everything is linked against the first entry.
+/// @param entryFunction if set, missing functions of the module containing the
+/// entry function will be solved.
+/// @return final module or null in this case errorMsg is set
+std::unique_ptr<llvm::Module>
+linkModules(std::vector<std::unique_ptr<llvm::Module>> &modules,
+            llvm::StringRef entryFunction, std::string &errorMsg);
+
+/// Return the Function* target of a Call or Invoke instruction, or
+/// null if it cannot be determined (should be only for indirect
+/// calls, although complicated constant expressions might be
+/// another possibility).
+///
+/// If `moduleIsFullyLinked` is set to true it will be assumed that the
+///  module containing the `llvm::CallSite` is fully linked. This assumption
+///  allows resolution of functions that are marked as overridable.
+llvm::Function *getDirectCallTarget(llvm::CallSite, bool moduleIsFullyLinked);
+
+/// Return true iff the given Function value is used in something
+/// other than a direct call (or a constant expression that
+/// terminates in a direct call).
+bool functionEscapes(const llvm::Function *f);
+
+/// Loads the file libraryName and reads all possible modules out of it.
+///
+/// Different file types are possible:
+/// * .bc binary file
+/// * .ll IR file
+/// * .a archive containing .bc and .ll files
+///
+/// @param libraryName library to read
+/// @param modules contains extracted modules
+/// @param errorMsg contains the error description in case the file could not be
+/// loaded
+/// @return true if successful otherwise false
+bool loadFile(const std::string &libraryName, llvm::LLVMContext &context,
+              std::vector<std::unique_ptr<llvm::Module>> &modules,
+              std::string &errorMsg);
+}
+
+#endif /* KLEE_MODULEUTIL_H */
diff --git a/include/klee/Support/PrintVersion.h b/include/klee/Support/PrintVersion.h
new file mode 100644
index 00000000..fbd20e39
--- /dev/null
+++ b/include/klee/Support/PrintVersion.h
@@ -0,0 +1,25 @@
+//===-- PrintVersion.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_PRINTVERSION_H
+#define KLEE_PRINTVERSION_H
+
+#include "llvm/Support/raw_ostream.h"
+
+#include "klee/Config/Version.h"
+
+namespace klee {
+#if LLVM_VERSION_CODE >= LLVM_VERSION(6, 0)
+  void printVersion(llvm::raw_ostream &OS);
+#else
+  void printVersion();
+#endif
+}
+
+#endif /* KLEE_PRINTVERSION_H */
diff --git a/include/klee/Support/Timer.h b/include/klee/Support/Timer.h
new file mode 100644
index 00000000..48cbbdea
--- /dev/null
+++ b/include/klee/Support/Timer.h
@@ -0,0 +1,96 @@
+//===-- Timer.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_TIMER_H
+#define KLEE_TIMER_H
+
+#include "klee/System/Time.h"
+
+#include "llvm/ADT/SmallVector.h"
+
+#include <functional>
+#include <memory>
+
+namespace klee {
+
+  /**
+   * A WallTimer stores its creation time.
+   */
+  class WallTimer {
+    const time::Point start;
+  public:
+    WallTimer();
+
+    /// Return the delta since the timer was created
+    time::Span delta() const;
+  };
+
+
+  /**
+   * A Timer repeatedly executes a `callback` after a specified `interval`.
+   * An object of this class is _passive_ and only keeps track of the next invocation time.
+   * _Passive_ means, that it has to be `invoke`d by an external caller with the current time.
+   * Only when the time span between the current time and the last invocation exceeds the
+   * specified `interval`, the `callback` will be executed.
+   * Multiple timers are typically managed by a TimerGroup.
+   */
+  class Timer {
+    /// Approximate interval between callback invocations.
+    time::Span interval;
+    /// Wall time for next invocation.
+    time::Point nextInvocationTime;
+    /// The event callback.
+    std::function<void()> run;
+  public:
+    /// \param interval The time span between callback invocations.
+    /// \param callback The event callback.
+    Timer(const time::Span &interval, std::function<void()> &&callback);
+
+    /// Return specified `interval` between invocations.
+    time::Span getInterval() const;
+    /// Execute `callback` if invocation time exceeded.
+    void invoke(const time::Point &currentTime);
+    /// Set new invocation time to `currentTime + interval`.
+    void reset(const time::Point &currentTime);
+  };
+
+
+  /**
+   * A TimerGroup manages multiple timers.
+   *
+   * TimerGroup simplifies the handling of multiple Timer objects by offering a unifying
+   * Timer-like interface. Additionally, it serves as a barrier and prevents timers from
+   * being invoked too often by defining a minimum invocation interval (MI).
+   * All registered timer intervals should be larger than MI and also be multiples of MI.
+   * Similar to Timer, a TimerGroup is _passive_ and needs to be `invoke`d by an external
+   * caller.
+   */
+  class TimerGroup {
+    /// Registered timers.
+    llvm::SmallVector<std::unique_ptr<Timer>, 4> timers;
+    /// Timer that invokes all registered timers after minimum interval.
+    Timer invocationTimer;
+    /// Time of last `invoke` call.
+    time::Point currentTime;
+  public:
+    /// \param minInterval The minimum interval between invocations of registered timers.
+    explicit TimerGroup(const time::Span &minInterval);
+
+    /// Add a timer to be executed periodically.
+    ///
+    /// \param timer The timer object to register.
+    void add(std::unique_ptr<Timer> timer);
+    /// Invoke registered timers with current time only if minimum interval exceeded.
+    void invoke();
+    /// Reset all timers.
+    void reset();
+  };
+
+} // klee
+#endif /* KLEE_TIMER_H */