From fabd71bf0a6dd89ce6fb8cea48380a52aad7edc4 Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Thu, 25 Jun 2009 00:02:11 +0000 Subject: 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 --- lib/Solver/STPBuilder.cpp | 31 ++++++++++++++++++++++--------- 1 file changed, 22 insertions(+), 9 deletions(-) (limited to 'lib/Solver/STPBuilder.cpp') 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 e, int *width_out) { switch (e->getKind()) { case Expr::Constant: { - uint64_t asUInt64 = cast(e)->getConstantValue(); - *width_out = e->getWidth(); - - if (*width_out > 64) - assert(0 && "constructActual: width > 64"); + ConstantExpr *CE = cast(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 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 -- cgit 1.4.1