Kill off last getConstantValue uses.

 - ConstantExpr should now fully support arbitrary width operations.

 - Still numerous holes in parsing, solver, etc. to plug.


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

3 files changed, 19 insertions, 12 deletions

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index bfe839d8..e880719e 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -316,8 +316,6 @@ public:
   unsigned getNumKids() const { return 0; }
   ref<Expr> getKid(unsigned i) const { return 0; }
 
-  uint64_t getConstantValue() const { return value.getZExtValue(); }
-
   /// getZExtValue - Return the constant value for a limited number of bits.
   ///
   /// This routine should be used in situations where the width of the constant
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index e4bde44b..d4042e3f 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -347,23 +347,21 @@ void ConstantExpr::toMemory(void *address) {
 }
 
 void ConstantExpr::toString(std::string &Res) const {
-  std::stringstream os;
-  os << *this;
-  Res = os.str();
+  Res = value.toString(10, false);
 }
 
 ref<ConstantExpr> ConstantExpr::Concat(const ref<ConstantExpr> &RHS) {
   Expr::Width W = getWidth() + RHS->getWidth();
-  assert(W <= 64 && "FIXME: Support arbitrary bit-widths!");
-  
-  uint64_t res = (getConstantValue() << RHS->getWidth()) + 
-    RHS->getConstantValue();
-  return ConstantExpr::create(res, W);
+  APInt Tmp(value);
+  Tmp.zext(W);
+  Tmp <<= RHS->getWidth();
+  Tmp |= APInt(RHS->value).zext(W);
+
+  return ConstantExpr::alloc(Tmp);
 }
 
 ref<ConstantExpr> ConstantExpr::Extract(unsigned Offset, Width W) {
-  return ConstantExpr::create(ints::trunc(getConstantValue() >> Offset, W, 
-                                          getWidth()), W);
+  return ConstantExpr::alloc(APInt(value.ashr(Offset)).zextOrTrunc(W));
 }
 
 ref<ConstantExpr> ConstantExpr::ZExt(Width W) {
diff --git a/test/Solver/LargeIntegers.pc b/test/Solver/LargeIntegers.pc
new file mode 100644
index 00000000..b47f8918
--- /dev/null
+++ b/test/Solver/LargeIntegers.pc
@@ -0,0 +1,11 @@
+# RUN: %kleaver %s > %t
+
+array a[64] : w32 -> w8 = symbolic
+
+# RUN: grep -A 1 \"Query 0\" %t > %t2
+# RUN: grep \"Expr 0:\t18446744073709551618\" %t2
+(query [] false [(Concat w128 (w64 1) (w64 2))])
+
+# RUN: grep -A 1 \"Query 1\" %t > %t2
+# RUN: grep \"Expr 0:\t16\" %t2
+(query [] false [(Extract w5 60 (Concat w128 (w64 1) (w64 2)))])