Remove some more uses of getConstantValue.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74149 91177308-0d34-0410-b5e6-96231b3b80d8

2 files changed, 12 insertions, 9 deletions

diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index ae7bc819..e4bde44b 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -164,7 +164,7 @@ unsigned Expr::computeHash() {
 }
 
 unsigned ConstantExpr::computeHash() {
-  hashValue = getConstantValue() ^ (getWidth() * MAGIC_HASH_CONSTANT);
+  hashValue = value.getHashValue() ^ (getWidth() * MAGIC_HASH_CONSTANT);
   return hashValue;
 }
 
@@ -1001,12 +1001,11 @@ static ref<Expr> TryConstArrayOpt(const ref<ConstantExpr> &cl,
 }
 
 static ref<Expr> EqExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {  
-  uint64_t value = cl->getConstantValue();
   Expr::Width width = cl->getWidth();
 
   Expr::Kind rk = r->getKind();
   if (width == Expr::Bool) {
-    if (value) {
+    if (cl->isTrue()) {
       return r;
     } else {
       // 0 == ...
@@ -1033,12 +1032,12 @@ static ref<Expr> EqExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
     // (sext(a,T)==c) == (a==c)
     const SExtExpr *see = cast<SExtExpr>(r);
     Expr::Width fromBits = see->src->getWidth();
-    uint64_t trunc = bits64::truncateToNBits(value, fromBits);
+    ref<ConstantExpr> trunc = cl->ZExt(fromBits);
 
     // pathological check, make sure it is possible to
     // sext to this value *from any value*
-    if (value == ints::sext(trunc, width, fromBits)) {
-      return EqExpr::create(see->src, ConstantExpr::create(trunc, fromBits));
+    if (cl == trunc->SExt(width)) {
+      return EqExpr::create(see->src, trunc);
     } else {
       return ConstantExpr::create(0, Expr::Bool);
     }
@@ -1046,12 +1045,12 @@ static ref<Expr> EqExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
     // (zext(a,T)==c) == (a==c)
     const ZExtExpr *zee = cast<ZExtExpr>(r);
     Expr::Width fromBits = zee->src->getWidth();
-    uint64_t trunc = bits64::truncateToNBits(value, fromBits);
+    ref<ConstantExpr> trunc = cl->ZExt(fromBits);
     
     // pathological check, make sure it is possible to
     // zext to this value *from any value*
-    if (value == ints::zext(trunc, width, fromBits)) {
-      return EqExpr::create(zee->src, ConstantExpr::create(trunc, fromBits));
+    if (cl == trunc->ZExt(width)) {
+      return EqExpr::create(zee->src, trunc);
     } else {
       return ConstantExpr::create(0, Expr::Bool);
     }
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 5a2db747..74c068b0 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -101,6 +101,10 @@ private:
 
 public:
   ValueRange() : m_min(1),m_max(0) {}
+  ValueRange(const ref<ConstantExpr> &ce) {
+    // FIXME: Support large widths.
+    m_min = m_max = ce->getLimitedValue();
+  }
   ValueRange(uint64_t value) : m_min(value), m_max(value) {}
   ValueRange(uint64_t _min, uint64_t _max) : m_min(_min), m_max(_max) {}
   ValueRange(const ValueRange &b) : m_min(b.m_min), m_max(b.m_max) {}