remove include/klee/Support/IntEvaluation.h

4 files changed, 5 insertions, 171 deletions

diff --git a/include/klee/Support/IntEvaluation.h b/include/klee/Support/IntEvaluation.h
deleted file mode 100644
index 0e9a40d6..00000000
--- a/include/klee/Support/IntEvaluation.h
+++ /dev/null
@@ -1,164 +0,0 @@
-//===-- 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/ADT/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/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp
index 6e5a52dc..4128a2dc 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -15,7 +15,6 @@
 #include "klee/Expr/Expr.h"
 #include "klee/Expr/ExprUtil.h"
 #include "klee/Solver/Solver.h"
-#include "klee/Support/IntEvaluation.h" // FIXME: Use APInt
 
 #include <map>
 #include <set>
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index d82cbee3..2d3670d8 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -12,9 +12,6 @@
 #include "klee/Config/Version.h"
 #include "klee/Expr/ExprPPrinter.h"
 #include "klee/Support/OptionCategories.h"
-// FIXME: We shouldn't need this once fast constant support moves into
-// Core. If we need to do arithmetic, we probably want to use APInt.
-#include "klee/Support/IntEvaluation.h"
 
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/Hashing.h"
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 382774ce..34a44c3e 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -17,8 +17,8 @@
 #include "klee/Expr/ExprVisitor.h"
 #include "klee/Solver/IncompleteSolver.h"
 #include "klee/Support/Debug.h"
-#include "klee/Support/IntEvaluation.h" // FIXME: Use APInt
 
+#include "llvm/ADT/APInt.h"
 #include "llvm/Support/raw_ostream.h"
 
 #include <cassert>
@@ -260,6 +260,7 @@ public:
   }
   
   std::int64_t minSigned(unsigned bits) const {
+    assert(bits >= 2 && bits <= 64);
     assert((m_min >> bits) == 0 && (m_max >> bits) == 0 &&
            "range is outside given number of bits");
 
@@ -269,13 +270,14 @@ public:
 
     std::uint64_t smallest = (static_cast<std::uint64_t>(1) << (bits - 1));
     if (m_max >= smallest) {
-      return ints::sext(smallest, 64, bits);
+      return llvm::APInt::getSignedMinValue(bits).getSExtValue();
     } else {
       return m_min;
     }
   }
 
   std::int64_t maxSigned(unsigned bits) const {
+    assert(bits >= 2 && bits <= 64);
     assert((m_min >> bits) == 0 && (m_max >> bits) == 0 &&
            "range is outside given number of bits");
 
@@ -288,7 +290,7 @@ public:
     if (m_min < smallest && m_max >= smallest) {
       return smallest - 1;
     } else {
-      return ints::sext(m_max, 64, bits);
+      return llvm::APInt(bits, m_max, true).getSExtValue();
     }
   }
 };