diff options
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 15 | ||||
| -rw-r--r-- | lib/Solver/STPBuilder.h | 2 | ||||
| -rw-r--r-- | test/Solver/overshift-aright-by-constant.kquery | 14 |
3 files changed, 21 insertions, 10 deletions
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 84e88579..9e3a9862 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -255,7 +255,7 @@ ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) { ExprHandle signedBool = bvBoolExtract(expr, width-1); //start with the result if shifting by width-1 - ExprHandle res = constructAShrByConstant(expr, width-1, signedBool, width); + ExprHandle res = constructAShrByConstant(expr, width-1, signedBool); //construct a big if-then-elif-elif-... with one case per possible shift amount // XXX more efficient to move the ite on the sign outside all exprs? @@ -265,8 +265,7 @@ ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) { eqExpr(shift, bvConst32(width,i)), constructAShrByConstant(expr, i, - signedBool, - width), + signedBool), res); } @@ -279,16 +278,14 @@ ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) { } ExprHandle STPBuilder::constructAShrByConstant(ExprHandle expr, - unsigned amount, - ExprHandle isSigned, - unsigned shiftBits) { + unsigned shift, + ExprHandle isSigned) { unsigned width = vc_getBVLength(vc, expr); - unsigned shift = amount & ((1<<shiftBits) - 1); if (shift==0) { return expr; } else if (shift>=width-1) { - return vc_iteExpr(vc, isSigned, bvMinusOne(width), bvZero(width)); + return bvZero(width); // Overshift to zero } else { return vc_iteExpr(vc, isSigned, @@ -841,7 +838,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) { unsigned shift = (unsigned) CE->getLimitedValue(); ExprHandle signedBool = bvBoolExtract(left, *width_out-1); - return constructAShrByConstant(left, shift, signedBool, getShiftBits(*width_out)); + return constructAShrByConstant(left, shift, signedBool); } else { int shiftWidth; ExprHandle amount = construct(ase->right, &shiftWidth); diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h index eaa41d5c..42ca9eaf 100644 --- a/lib/Solver/STPBuilder.h +++ b/lib/Solver/STPBuilder.h @@ -107,7 +107,7 @@ private: ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle shift); ExprHandle constructAShrByConstant(ExprHandle expr, unsigned shift, - ExprHandle isSigned, unsigned shiftBits); + ExprHandle isSigned); ExprHandle constructMulByConstant(ExprHandle expr, unsigned width, uint64_t x); ExprHandle constructUDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d); ExprHandle constructSDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d); diff --git a/test/Solver/overshift-aright-by-constant.kquery b/test/Solver/overshift-aright-by-constant.kquery new file mode 100644 index 00000000..c21889e2 --- /dev/null +++ b/test/Solver/overshift-aright-by-constant.kquery @@ -0,0 +1,14 @@ +# RUN: %kleaver %s > %t +# RUN: not grep INVALID %t +array x[4] : w32 -> w8 = symbolic +# ∀ x. x > 0 → ( ((signed int) x) >> 32 = 0 ) +# Check we overshift to zero for when shifting for all 32-bit values >0 + +(query [ (Ult (w32 0) (ReadLSB w32 (w32 0) x)) ] + (Eq + (AShr w32 + (ReadLSB w32 (w32 0) x) + (w32 32) + ) + (w32 0) + ) [ ] [x] ) |