Flesh out support for arbitrary bit widths in some key places (STP & constant

creation).
 - Not used yet.


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

3 files changed, 50 insertions, 18 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index aca9dd2a..1db9efe7 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -396,7 +396,15 @@ void Executor::initializeGlobalObject(ExecutionState &state, ObjectState *os,
       initializeGlobalObject(state, os, cs->getOperand(i), 
 			     offset + sl->getElementOffset(i));
   } else {
-    os->write(offset, evalConstant(c));
+    unsigned StoreBits = targetData->getTypeStoreSizeInBits(c->getType());
+    ref<ConstantExpr> C = evalConstant(c);
+
+    // Extend the constant if necessary;
+    assert(StoreBits >= C->getWidth() && "Invalid store size!");
+    if (StoreBits > C->getWidth())
+      C = ConstantExpr::alloc(0, StoreBits - C->getWidth())->Concat(C);
+
+    os->write(offset, C);
   }
 }
 
@@ -923,15 +931,21 @@ ref<klee::ConstantExpr> Executor::evalConstant(Constant *c) {
     return evalConstantExpr(ce);
   } else {
     if (const ConstantInt *ci = dyn_cast<ConstantInt>(c)) {
-      switch(ci->getBitWidth()) {
-      case  1: return ConstantExpr::create(ci->getZExtValue(), Expr::Bool);
-      case  8: return ConstantExpr::create(ci->getZExtValue(), Expr::Int8);
-      case 16: return ConstantExpr::create(ci->getZExtValue(), Expr::Int16);
-      case 32: return ConstantExpr::create(ci->getZExtValue(), Expr::Int32);
-      case 64: return ConstantExpr::create(ci->getZExtValue(), Expr::Int64);
-      default:
-        assert(0 && "XXX arbitrary bit width constants unhandled");
+      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;
     } else if (const ConstantFP *cf = dyn_cast<ConstantFP>(c)) {      
       switch(cf->getType()->getTypeID()) {
       case Type::FloatTyID: {
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 2c03c483..2e313fb0 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -465,17 +465,30 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
 
   switch (e->getKind()) {
   case Expr::Constant: {
-    uint64_t asUInt64 = cast<ConstantExpr>(e)->getConstantValue();
-    *width_out = e->getWidth();
-
-    if (*width_out > 64)
-      assert(0 && "constructActual: width > 64");
+    ConstantExpr *CE = cast<ConstantExpr>(e);
+    *width_out = CE->getWidth();
 
+    // Coerce to bool if necessary.
     if (*width_out == 1)
-      return asUInt64 ? getTrue() : getFalse();
-    else if (*width_out <= 32) 
-      return bvConst32(*width_out, asUInt64);
-    else return bvConst64(*width_out, asUInt64);
+      return CE->isTrue() ? getTrue() : getFalse();
+
+    // Fast path.
+    if (*width_out <= 32)
+      return bvConst32(*width_out, CE->getZExtValue(32));
+    if (*width_out <= 64)
+      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) {
+      Tmp = Tmp->LShr(ConstantExpr::alloc(64, Tmp->getWidth()));
+      Res = vc_bvConcatExpr(vc, bvConst64(std::min(64U, Tmp->getWidth()),
+                                          Tmp->Extract(0, 64)->getZExtValue()),
+                            Res);
+    }
+    return Res;
   }
     
   // Special
diff --git a/test/Feature/ArbitraryBitWidths.ll b/test/Feature/ArbitraryBitWidths.ll
new file mode 100644
index 00000000..34e3ee78
--- /dev/null
+++ b/test/Feature/ArbitraryBitWidths.ll
@@ -0,0 +1,5 @@
+@g0 = global i31 10
+
+define i32 @main() {
+       ret i32 0
+}
\ No newline at end of file