STPBuilder: fix bv{Zero,One,MinusOne} for the case where width>64

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

1 files changed, 17 insertions, 3 deletions

diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 28b5c1a5..b5dddad1 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -107,13 +107,13 @@ ExprHandle STPBuilder::getFalse() {
   return vc_falseExpr(vc);
 }
 ExprHandle STPBuilder::bvOne(unsigned width) {
-  return bvConst32(width, 1);
+  return bvZExtConst(width, 1);
 }
 ExprHandle STPBuilder::bvZero(unsigned width) {
-  return bvConst32(width, 0);
+  return bvZExtConst(width, 0);
 }
 ExprHandle STPBuilder::bvMinusOne(unsigned width) {
-  return bvConst64(width, (int64_t) -1);
+  return bvSExtConst(width, (int64_t) -1);
 }
 ExprHandle STPBuilder::bvConst32(unsigned width, uint32_t value) {
   return vc_bvConstExprFromInt(vc, width, value);
@@ -121,6 +121,20 @@ ExprHandle STPBuilder::bvConst32(unsigned width, uint32_t value) {
 ExprHandle STPBuilder::bvConst64(unsigned width, uint64_t value) {
   return vc_bvConstExprFromLL(vc, width, value);
 }
+ExprHandle STPBuilder::bvZExtConst(unsigned width, uint64_t value) {
+  if (width <= 64)
+    return bvConst64(width, value);
+
+  ExprHandle expr = bvConst64(64, value), zero = bvConst64(64, 0);
+  for (width -= 64; width > 64; width -= 64)
+    expr = vc_bvConcatExpr(vc, zero, expr);
+  return vc_bvConcatExpr(vc, bvConst64(width, 0), expr);
+}
+ExprHandle STPBuilder::bvSExtConst(unsigned width, uint64_t value) {
+  if (width <= 64)
+    return bvConst64(width, value);
+  return vc_bvSignExtend(vc, bvConst64(64, value), width);
+}
 
 ExprHandle STPBuilder::bvBoolExtract(ExprHandle expr, int bit) {
   return vc_eqExpr(vc, bvExtract(expr, bit, bit), bvOne(1));