about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--include/klee/Expr.h19
-rw-r--r--lib/Expr/Expr.cpp12
2 files changed, 14 insertions, 17 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 31bed1a8..49d612cc 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -14,6 +14,7 @@
 #include "klee/util/Bits.h"
 #include "klee/util/Ref.h"
 
+#include "llvm/ADT/APInt.h"
 #include "llvm/ADT/SmallVector.h"
 #include "llvm/Support/Streams.h"
 
@@ -296,9 +297,9 @@ public:
   static const unsigned numKids = 0;
 
 private:
-  uint64_t value;
+  llvm::APInt value;
 
-  ConstantExpr(uint64_t v, Width w) : value(v), width(w) {}
+  ConstantExpr(uint64_t v, Width w) : value(w, v), width(w) {}
 
 public:
   Width width;
@@ -312,7 +313,7 @@ public:
   unsigned getNumKids() const { return 0; }
   ref<Expr> getKid(unsigned i) const { return 0; }
 
-  uint64_t getConstantValue() const { return value; }
+  uint64_t getConstantValue() const { return value.getZExtValue(); }
 
   /// getZExtValue - Return the constant value for a limited number of bits.
   ///
@@ -320,13 +321,13 @@ public:
   /// is known to be limited to a certain number of bits.
   uint64_t getZExtValue(unsigned bits = 64) const {
     assert(getWidth() <= bits && "Value may be out of range!");
-    return value;
+    return value.getZExtValue();
   }
 
   /// getLimitedValue - If this value is smaller than the specified limit,
   /// return it, otherwise return the limit value.
   uint64_t getLimitedValue(uint64_t Limit = ~0ULL) const {
-    return (value > Limit) ? Limit :  getZExtValue();
+    return value.getLimitedValue(Limit);
   }
 
   /// toString - Return the constant value as a decimal string.
@@ -335,13 +336,9 @@ public:
   int compareContents(const Expr &b) const { 
     const ConstantExpr &cb = static_cast<const ConstantExpr&>(b);
     if (width != cb.width) return width < cb.width ? -1 : 1;
-    if (value < cb.value) {
-      return -1;
-    } else if (value > cb.value) {
-      return 1;
-    } else {
+    if (value == cb.value)
       return 0;
-    }
+    return value.ult(cb.value) ? -1 : 1;
   }
 
   virtual ref<Expr> rebuild(ref<Expr> kids[]) const { 
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index a89163f2..2d41a579 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -164,7 +164,7 @@ unsigned Expr::computeHash() {
 }
 
 unsigned ConstantExpr::computeHash() {
-  hashValue = value ^ (width * MAGIC_HASH_CONSTANT);
+  hashValue = getConstantValue() ^ (width * MAGIC_HASH_CONSTANT);
   return hashValue;
 }
 
@@ -338,11 +338,11 @@ ref<Expr> ConstantExpr::fromMemory(void *address, Width width) {
 void ConstantExpr::toMemory(void *address) {
   switch (width) {
   default: assert(0 && "invalid type");
-  case  Expr::Bool: *(( uint8_t*) address) = value; break;
-  case  Expr::Int8: *(( uint8_t*) address) = value; break;
-  case Expr::Int16: *((uint16_t*) address) = value; break;
-  case Expr::Int32: *((uint32_t*) address) = value; break;
-  case Expr::Int64: *((uint64_t*) address) = value; break;
+  case  Expr::Bool: *(( uint8_t*) address) = getConstantValue(); break;
+  case  Expr::Int8: *(( uint8_t*) address) = getConstantValue(); break;
+  case Expr::Int16: *((uint16_t*) address) = getConstantValue(); break;
+  case Expr::Int32: *((uint32_t*) address) = getConstantValue(); break;
+  case Expr::Int64: *((uint64_t*) address) = getConstantValue(); break;
   }
 }