diff options
| -rw-r--r-- | lib/Core/Executor.cpp | 32 | ||||
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 31 | ||||
| -rw-r--r-- | test/Feature/ArbitraryBitWidths.ll | 5 |
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 |