From ed963d407e5de9b09191324f5e277ea40e1aea0b Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 7 Nov 2013 11:52:18 +0000 Subject: Fixed overshifting an expression by a constant so that we overshift to zero. A test case was added for this. In addition the use to vc_bvExtract() was removed for shifting left by an expression because we don't want/need bitmasked behaviour anymore. --- lib/Solver/STPBuilder.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib/Solver/STPBuilder.h') diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h index 0a99b753..90061784 100644 --- a/lib/Solver/STPBuilder.h +++ b/lib/Solver/STPBuilder.h @@ -100,9 +100,9 @@ private: ExprHandle eqExpr(ExprHandle a, ExprHandle b); //logical left and right shift (not arithmetic) - ExprHandle bvLeftShift(ExprHandle expr, unsigned shift, unsigned shiftBits); + ExprHandle bvLeftShift(ExprHandle expr, unsigned shift); ExprHandle bvRightShift(ExprHandle expr, unsigned amount, unsigned shiftBits); - ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle amount, unsigned width); + ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle shift); ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle amount, unsigned width); ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle amount, unsigned width); -- cgit 1.4.1 From 71048bea167794f109b2f0b715b6cc1ba8b6eab9 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 7 Nov 2013 14:45:22 +0000 Subject: Fixed overshift of logical right shift by symbolic so that it overshifts to zero. Test case is included. --- lib/Solver/STPBuilder.cpp | 25 ++++++++++++------------ lib/Solver/STPBuilder.h | 2 +- test/Solver/overshift-lright-by-symbolic.kquery | 26 +++++++++++++++++++++++++ 3 files changed, 40 insertions(+), 13 deletions(-) create mode 100644 test/Solver/overshift-lright-by-symbolic.kquery (limited to 'lib/Solver/STPBuilder.h') diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 7e004445..24004c2a 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -228,22 +228,23 @@ ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle shift) { } // logical right shift by a variable amount on an expression of the specified width -ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle amount, unsigned width) { +ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle shift) { + unsigned width = vc_getBVLength(vc, expr); ExprHandle res = bvZero(width); - int shiftBits = getShiftBits( width ); - - //get the shift amount (looking only at the bits appropriate for the given width) - ExprHandle shift = vc_bvExtract( vc, amount, shiftBits - 1, 0 ); - //construct a big if-then-elif-elif-... with one case per possible shift amount for( int i=width-1; i>=0; i-- ) { res = vc_iteExpr(vc, - eqExpr(shift, bvConst32(shiftBits, i)), - bvRightShift(expr, i, shiftBits), + eqExpr(shift, bvConst32(width, i)), + bvRightShift(expr, i, width), res); } + // If overshifting, shift to zero + res = vc_iteExpr(vc, + vc_bvLtExpr(vc, shift, bvConst32(width, width)), + res, + bvZero(width)); return res; } @@ -367,9 +368,9 @@ ExprHandle STPBuilder::constructUDivByConstant(ExprHandle expr_n, unsigned width // n/d = (((n - t1) >> sh1) + t1) >> sh2; ExprHandle n_minus_t1 = vc_bvMinusExpr( vc, width, expr_n, t1 ); - ExprHandle shift_sh1 = bvVarRightShift( n_minus_t1, expr_sh1, 32 ); + ExprHandle shift_sh1 = bvVarRightShift( n_minus_t1, expr_sh1); ExprHandle plus_t1 = vc_bvPlusExpr( vc, width, shift_sh1, t1 ); - ExprHandle res = bvVarRightShift( plus_t1, expr_sh2, 32 ); + ExprHandle res = bvVarRightShift( plus_t1, expr_sh2); return res; } @@ -407,7 +408,7 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width // Improved variable arithmetic right shift: sign extend, shift, // extract. ExprHandle extend_npm = vc_bvSignExtend( vc, n_plus_mulsh, 64 ); - ExprHandle shift_npm = bvVarRightShift( extend_npm, expr_shpost, 64 ); + ExprHandle shift_npm = bvVarRightShift( extend_npm, expr_shpost); ExprHandle shift_shpost = vc_bvExtract( vc, shift_npm, 31, 0 ); //lower 32-bits // XSIGN(n) is -1 if n is negative, positive one otherwise @@ -830,7 +831,7 @@ ExprHandle STPBuilder::constructActual(ref e, int *width_out) { } else { int shiftWidth; ExprHandle amount = construct(lse->right, &shiftWidth); - return bvVarRightShift( left, amount, *width_out ); + return bvVarRightShift( left, amount); } } diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h index 90061784..828c267d 100644 --- a/lib/Solver/STPBuilder.h +++ b/lib/Solver/STPBuilder.h @@ -103,7 +103,7 @@ private: ExprHandle bvLeftShift(ExprHandle expr, unsigned shift); ExprHandle bvRightShift(ExprHandle expr, unsigned amount, unsigned shiftBits); ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle shift); - ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle amount, unsigned width); + ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle shift); ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle amount, unsigned width); ExprHandle constructAShrByConstant(ExprHandle expr, unsigned shift, diff --git a/test/Solver/overshift-lright-by-symbolic.kquery b/test/Solver/overshift-lright-by-symbolic.kquery new file mode 100644 index 00000000..7ca6d4d5 --- /dev/null +++ b/test/Solver/overshift-lright-by-symbolic.kquery @@ -0,0 +1,26 @@ +# RUN: %kleaver %s > %t +# RUN: not grep INVALID %t + +array shift[4] : w32 -> w8 = symbolic +# ∀ x. x >= 32 → ( (2 >> x) = 0 ) +# Check we logical right overshift to zero when shifting a constant ALWAYS! + +(query [ (Ule (w32 32) (ReadLSB w32 (w32 0) shift)) ] + (Eq + (LShr w32 (w32 2) + (ReadLSB w32 (w32 0) shift) + ) + (w32 0) + ) [ ] [shift] ) + +# 64-bit version +# ∀ x. x >= 64 → ( (2 >> x) = 0 ) +array shift64[8] : w32 -> w8 = symbolic + +(query [ (Ule (w64 64) (ReadLSB w64 (w32 0) shift64)) ] + (Eq + (LShr w64 (w64 2) + (ReadLSB w64 (w32 0) shift64) + ) + (w64 0) + ) [ ] [shift64] ) -- cgit 1.4.1 From 3be107cbf55f69f063795182690a5f9689e1d805 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 7 Nov 2013 14:59:37 +0000 Subject: Fixed overshift of logical right shift by constant so that it overshifts to zero. Test case is included. --- lib/Solver/STPBuilder.cpp | 16 ++++++---------- lib/Solver/STPBuilder.h | 2 +- test/Solver/overshift-lright-by-constant.kquery | 14 ++++++++++++++ 3 files changed, 21 insertions(+), 11 deletions(-) create mode 100644 test/Solver/overshift-lright-by-constant.kquery (limited to 'lib/Solver/STPBuilder.h') diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 24004c2a..a92b6f2b 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -174,14 +174,13 @@ ExprHandle STPBuilder::eqExpr(ExprHandle a, ExprHandle b) { } // logical right shift -ExprHandle STPBuilder::bvRightShift(ExprHandle expr, unsigned amount, unsigned shiftBits) { +ExprHandle STPBuilder::bvRightShift(ExprHandle expr, unsigned shift) { unsigned width = vc_getBVLength(vc, expr); - unsigned shift = amount & ((1<=width) { - return bvZero(width); + return bvZero(width); // Overshift to zero } else { return vc_bvConcatExpr(vc, bvZero(shift), @@ -236,7 +235,7 @@ ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle shift) { for( int i=width-1; i>=0; i-- ) { res = vc_iteExpr(vc, eqExpr(shift, bvConst32(width, i)), - bvRightShift(expr, i, width), + bvRightShift(expr, i), res); } @@ -294,7 +293,7 @@ ExprHandle STPBuilder::constructAShrByConstant(ExprHandle expr, ExprHandle(vc_bvConcatExpr(vc, bvMinusOne(shift), bvExtract(expr, width - 1, shift))), - bvRightShift(expr, shift, shiftBits)); + bvRightShift(expr, shift)); } } @@ -660,8 +659,7 @@ ExprHandle STPBuilder::constructActual(ref e, int *width_out) { if (bits64::isPowerOfTwo(divisor)) { return bvRightShift(left, - bits64::indexOfSingleBit(divisor), - getShiftBits(*width_out)); + bits64::indexOfSingleBit(divisor)); } else if (optimizeDivides) { if (*width_out == 32) //only works for 32-bit division return constructUDivByConstant( left, *width_out, @@ -822,12 +820,10 @@ ExprHandle STPBuilder::constructActual(ref e, int *width_out) { case Expr::LShr: { LShrExpr *lse = cast(e); ExprHandle left = construct(lse->left, width_out); - unsigned shiftBits = getShiftBits(*width_out); assert(*width_out!=1 && "uncanonicalized lshr"); if (ConstantExpr *CE = dyn_cast(lse->right)) { - return bvRightShift(left, (unsigned) CE->getLimitedValue(), - shiftBits); + return bvRightShift(left, (unsigned) CE->getLimitedValue()); } else { int shiftWidth; ExprHandle amount = construct(lse->right, &shiftWidth); diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h index 828c267d..48bddeed 100644 --- a/lib/Solver/STPBuilder.h +++ b/lib/Solver/STPBuilder.h @@ -101,7 +101,7 @@ private: //logical left and right shift (not arithmetic) ExprHandle bvLeftShift(ExprHandle expr, unsigned shift); - ExprHandle bvRightShift(ExprHandle expr, unsigned amount, unsigned shiftBits); + ExprHandle bvRightShift(ExprHandle expr, unsigned shift); ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle shift); ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle shift); ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle amount, unsigned width); diff --git a/test/Solver/overshift-lright-by-constant.kquery b/test/Solver/overshift-lright-by-constant.kquery new file mode 100644 index 00000000..cb223dd5 --- /dev/null +++ b/test/Solver/overshift-lright-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 → ( 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 + (LShr w32 + (ReadLSB w32 (w32 0) x) + (w32 32) + ) + (w32 0) + ) [ ] [x] ) -- cgit 1.4.1 From 7759c90744bae5c531f765b2faa2475e13f464fd Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 7 Nov 2013 15:21:43 +0000 Subject: Fixed overshift of arithmetic right shift by symbolic so that it overshifts to zero. Test case is included. --- lib/Solver/STPBuilder.cpp | 23 +++++++++++----------- lib/Solver/STPBuilder.h | 2 +- test/Feature/logical-right-overshift-sym-conc.c | 4 ++-- test/Solver/overshift-aright-by-symbolic.kquery | 26 +++++++++++++++++++++++++ 4 files changed, 41 insertions(+), 14 deletions(-) create mode 100644 test/Solver/overshift-aright-by-symbolic.kquery (limited to 'lib/Solver/STPBuilder.h') diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index a92b6f2b..84e88579 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -248,31 +248,33 @@ ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle shift) { } // arithmetic right shift by a variable amount on an expression of the specified width -ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle amount, unsigned width) { - int shiftBits = getShiftBits( width ); - - //get the shift amount (looking only at the bits appropriate for the given width) - ExprHandle shift = vc_bvExtract( vc, amount, shiftBits - 1, 0 ); +ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) { + unsigned width = vc_getBVLength(vc, expr); //get the sign bit to fill with ExprHandle signedBool = bvBoolExtract(expr, width-1); //start with the result if shifting by width-1 - ExprHandle res = constructAShrByConstant(expr, width-1, signedBool, shiftBits); + ExprHandle res = constructAShrByConstant(expr, width-1, signedBool, width); //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? // XXX more efficient to sign extend, right shift, then extract lower bits? for( int i=width-2; i>=0; i-- ) { res = vc_iteExpr(vc, - eqExpr(shift, bvConst32(shiftBits,i)), + eqExpr(shift, bvConst32(width,i)), constructAShrByConstant(expr, i, signedBool, - shiftBits), + width), res); } + // If overshifting, shift to zero + res = vc_iteExpr(vc, + vc_bvLtExpr(vc, shift, bvConst32(width, width)), + res, + bvZero(width)); return res; } @@ -839,12 +841,11 @@ ExprHandle STPBuilder::constructActual(ref e, int *width_out) { if (ConstantExpr *CE = dyn_cast(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, getShiftBits(*width_out)); } else { int shiftWidth; ExprHandle amount = construct(ase->right, &shiftWidth); - return bvVarArithRightShift( left, amount, *width_out ); + return bvVarArithRightShift( left, amount); } } diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h index 48bddeed..eaa41d5c 100644 --- a/lib/Solver/STPBuilder.h +++ b/lib/Solver/STPBuilder.h @@ -104,7 +104,7 @@ private: ExprHandle bvRightShift(ExprHandle expr, unsigned shift); ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle shift); ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle shift); - ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle amount, unsigned width); + ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle shift); ExprHandle constructAShrByConstant(ExprHandle expr, unsigned shift, ExprHandle isSigned, unsigned shiftBits); diff --git a/test/Feature/logical-right-overshift-sym-conc.c b/test/Feature/logical-right-overshift-sym-conc.c index 47e0959c..00281ec4 100644 --- a/test/Feature/logical-right-overshift-sym-conc.c +++ b/test/Feature/logical-right-overshift-sym-conc.c @@ -1,7 +1,7 @@ // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc // RUN: %klee -use-cex-cache=1 -check-overshift=0 %t.bc -// RUN: not grep "ASSERTION FAIL" klee-last/messages.txt -// RUN: grep "KLEE: done: explored paths = 1" klee-last/info +// RUN: not grep "ASSERTION FAIL" %T/klee-last/messages.txt +// RUN: grep "KLEE: done: explored paths = 1" %T/klee-last/info #include #include diff --git a/test/Solver/overshift-aright-by-symbolic.kquery b/test/Solver/overshift-aright-by-symbolic.kquery new file mode 100644 index 00000000..af563ea3 --- /dev/null +++ b/test/Solver/overshift-aright-by-symbolic.kquery @@ -0,0 +1,26 @@ +# RUN: %kleaver %s > %t +# RUN: not grep INVALID %t + +array shift[4] : w32 -> w8 = symbolic +# ∀ x. x >= 32 → ( ( ( (signed int)2 ) >> x) = 0 ) +# Check we arithmetic right overshift to zero when shifting a constant ALWAYS! + +(query [ (Ule (w32 32) (ReadLSB w32 (w32 0) shift)) ] + (Eq + (AShr w32 (w32 2) + (ReadLSB w32 (w32 0) shift) + ) + (w32 0) + ) [ ] [shift] ) + +# 64-bit version +# ∀ x. x >= 64 → ( (((signed int) 2) >> x) = 0 ) +array shift64[8] : w32 -> w8 = symbolic + +(query [ (Ule (w64 64) (ReadLSB w64 (w32 0) shift64)) ] + (Eq + (AShr w64 (w64 2) + (ReadLSB w64 (w32 0) shift64) + ) + (w64 0) + ) [ ] [shift64] ) -- cgit 1.4.1 From b6e9a1f1d3d1d1ddd9b5843c47b372352d259a16 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 7 Nov 2013 15:50:30 +0000 Subject: Fixed overshift of arithmetic right shift by constant so that it overshifts to zero. Test case is included. --- lib/Solver/STPBuilder.cpp | 15 ++++++--------- lib/Solver/STPBuilder.h | 2 +- test/Solver/overshift-aright-by-constant.kquery | 14 ++++++++++++++ 3 files changed, 21 insertions(+), 10 deletions(-) create mode 100644 test/Solver/overshift-aright-by-constant.kquery (limited to 'lib/Solver/STPBuilder.h') 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<=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 e, int *width_out) { if (ConstantExpr *CE = dyn_cast(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] ) -- cgit 1.4.1 From e70cd5b0764fe50f1e081a7d3e8e81fd623aa090 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 7 Nov 2013 16:11:02 +0000 Subject: Remove STPBuilder::getShiftBits() which is no longer used. --- lib/Solver/STPBuilder.h | 7 ------- 1 file changed, 7 deletions(-) (limited to 'lib/Solver/STPBuilder.h') diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h index 42ca9eaf..ef1cd8b3 100644 --- a/lib/Solver/STPBuilder.h +++ b/lib/Solver/STPBuilder.h @@ -79,13 +79,6 @@ class STPBuilder { STPArrayExprHash _arr_hash; private: - unsigned getShiftBits(unsigned amount) { - unsigned bits = 1; - amount--; - while (amount >>= 1) - bits++; - return bits; - } ExprHandle bvOne(unsigned width); ExprHandle bvZero(unsigned width); -- cgit 1.4.1