More large integer support.

 - Allow constructing a ConstantExpr from an APInt, too painful otherwise.

 - Parser support for large integers.


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

7 files changed, 29 insertions, 35 deletions

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index e880719e..e3a57123 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -301,12 +301,6 @@ private:
 
   ConstantExpr(const llvm::APInt &v) : value(v) {}
 
-  static ref<ConstantExpr> alloc(const llvm::APInt &v) {
-    ref<ConstantExpr> r(new ConstantExpr(v));
-    r->computeHash();
-    return r;
-  }
-
 public:
   ~ConstantExpr() {};
   
@@ -353,12 +347,15 @@ public:
   static ref<Expr> fromMemory(void *address, Width w);
   void toMemory(void *address);
 
-  static ref<ConstantExpr> alloc(uint64_t v, Width w) {
-    // constructs an "optimized" ConstantExpr
-    ref<ConstantExpr> r(new ConstantExpr(llvm::APInt(w, v)));
+  static ref<ConstantExpr> alloc(const llvm::APInt &v) {
+    ref<ConstantExpr> r(new ConstantExpr(v));
     r->computeHash();
     return r;
   }
+
+  static ref<ConstantExpr> alloc(uint64_t v, Width w) {
+    return alloc(llvm::APInt(w, v));
+  }
   
   static ref<ConstantExpr> create(uint64_t v, Width w) {
     assert(v == bits64::truncateToNBits(v, w) &&
diff --git a/include/klee/ExprBuilder.h b/include/klee/ExprBuilder.h
index 18941876..2bbcf545 100644
--- a/include/klee/ExprBuilder.h
+++ b/include/klee/ExprBuilder.h
@@ -23,7 +23,7 @@ namespace klee {
 
     // Expressions
 
-    virtual ref<Expr> Constant(uint64_t Value, Expr::Width W) = 0;
+    virtual ref<Expr> Constant(const llvm::APInt &Value) = 0;
     virtual ref<Expr> NotOptimized(const ref<Expr> &Index) = 0;
     virtual ref<Expr> Read(const UpdateList &Updates, 
                            const ref<Expr> &Index) = 0;
@@ -67,6 +67,10 @@ namespace klee {
     ref<Expr> Not(const ref<Expr> &LHS) {
       return Eq(False(), LHS);
     }
+
+    ref<Expr> Constant(uint64_t Value, Expr::Width W) {
+      return Constant(llvm::APInt(W, Value));
+    }
   };
 
   /// createDefaultExprBuilder - Create an expression builder which does no
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 1db9efe7..8f5b3daa 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -931,21 +931,7 @@ ref<klee::ConstantExpr> Executor::evalConstant(Constant *c) {
     return evalConstantExpr(ce);
   } else {
     if (const ConstantInt *ci = dyn_cast<ConstantInt>(c)) {
-      const APInt &Val = ci->getValue();
-      unsigned W = Val.getBitWidth();
-      
-      if (W <= 64)
-        return ConstantExpr::create(Val.getZExtValue(), W);
-
-      assert(0 && "FIXME: Untested!");
-      ref<ConstantExpr> Res = ConstantExpr::create(0, W);
-      for (unsigned i = 0; i < Val.getNumWords(); ++i) {
-        ref<ConstantExpr> Tmp = ConstantExpr::alloc(Val.getRawData()[i], W);
-        Tmp = Tmp->Shl(ConstantExpr::alloc(i * 64, W));
-        Res = Res->Or(Tmp);
-      }
-
-      return Res;
+      return ConstantExpr::alloc(ci->getValue());
     } else if (const ConstantFP *cf = dyn_cast<ConstantFP>(c)) {      
       switch(cf->getType()->getTypeID()) {
       case Type::FloatTyID: {
diff --git a/lib/Expr/ExprBuilder.cpp b/lib/Expr/ExprBuilder.cpp
index 68a7fefd..009e621e 100644
--- a/lib/Expr/ExprBuilder.cpp
+++ b/lib/Expr/ExprBuilder.cpp
@@ -19,8 +19,8 @@ ExprBuilder::~ExprBuilder() {
 
 namespace {
   class DefaultExprBuilder : public ExprBuilder {
-    virtual ref<Expr> Constant(uint64_t Value, Expr::Width W) {
-      return ConstantExpr::alloc(Value, W);
+    virtual ref<Expr> Constant(const llvm::APInt &Value) {
+      return ConstantExpr::alloc(Value);
     }
 
     virtual ref<Expr> NotOptimized(const ref<Expr> &Index) {
@@ -164,8 +164,8 @@ namespace {
       : Builder(_Builder), Base(_Base) {}
     ~ChainedBuilder() { delete Base; }
 
-    ref<Expr> Constant(uint64_t Value, Expr::Width W) {
-      return Base->Constant(Value, W);
+    ref<Expr> Constant(const llvm::APInt &Value) {
+      return Base->Constant(Value);
     }
 
     ref<Expr> NotOptimized(const ref<Expr> &Index) {
@@ -307,8 +307,8 @@ namespace {
     ConstantSpecializedExprBuilder(ExprBuilder *Base) : Builder(this, Base) {}
     ~ConstantSpecializedExprBuilder() {}
 
-    virtual ref<Expr> Constant(uint64_t Value, Expr::Width W) {
-      return Builder.Constant(Value, W);
+    virtual ref<Expr> Constant(const llvm::APInt &Value) {
+      return Builder.Constant(Value);
     }
 
     virtual ref<Expr> NotOptimized(const ref<Expr> &Index) {
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 2b9777cb..42e8af03 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -1462,7 +1462,7 @@ ExprResult ParserImpl::ParseNumberToken(Expr::Width Type, const Token &Tok) {
   }
 
   // This is a simple but slow way to handle overflow.
-  APInt Val(std::max(64U, RadixBits * N), 0);
+  APInt Val(RadixBits * N, 0);
   APInt RadixVal(Val.getBitWidth(), Radix);
   APInt DigitVal(Val.getBitWidth(), 0);
   for (unsigned i=0; i<N; ++i) {
@@ -1496,9 +1496,11 @@ ExprResult ParserImpl::ParseNumberToken(Expr::Width Type, const Token &Tok) {
     Val = -Val;
 
   if (Type < Val.getBitWidth())
-    Val = Val.trunc(Type);
+    Val.trunc(Type);
+  else if (Type > Val.getBitWidth())
+    Val.zext(Type);
 
-  return ExprResult(Builder->Constant(Val.getZExtValue(), Type));
+  return ExprResult(Builder->Constant(Val));
 }
 
 /// ParseTypeSpecifier - Parse a type specifier.
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 2e313fb0..65ef24d1 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -479,7 +479,6 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
       return bvConst64(*width_out, CE->getZExtValue());
 
     // FIXME: Optimize?
-    assert(0 && "FIXME: Not tested!");
     ref<ConstantExpr> Tmp = CE;
     ExprHandle Res = bvConst64(64, Tmp->Extract(0, 64)->getZExtValue());
     for (unsigned i = (*width_out / 64) - 1; i; --i) {
diff --git a/test/Solver/LargeIntegers.pc b/test/Solver/LargeIntegers.pc
index b47f8918..99d1a61b 100644
--- a/test/Solver/LargeIntegers.pc
+++ b/test/Solver/LargeIntegers.pc
@@ -9,3 +9,9 @@ array a[64] : w32 -> w8 = symbolic
 # 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)))])
+
+# RUN: grep -A 1 \"Query 2\" %t > %t2
+# RUN: grep \"Array 0:\ta.16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0\" %t2
+(query [(Eq 0x0102030405060708090A0B0C0D0E0F10 (ReadLSB w128 0 a))] 
+       false 
+       [] [a])