diff options
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 12 | ||||
| -rw-r--r-- | test/regression/2015-08-30-sdiv-1.c | 19 |
2 files changed, 27 insertions, 4 deletions
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index a5e4c5ad..c2f23c0a 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -382,6 +382,7 @@ ExprHandle STPBuilder::constructUDivByConstant(ExprHandle expr_n, unsigned width * @return n/d without doing explicit division */ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d) { + // Refactor using APInt::ms APInt::magic(); assert(width==32 && "can only compute udiv constants for 32-bit division"); // Compute the constants needed to compute n/d for constant d w/o division by d. @@ -673,11 +674,14 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { assert(*width_out!=1 && "uncanonicalized sdiv"); if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) - if (optimizeDivides) - if (*width_out == 32) //only works for 32-bit division - return constructSDivByConstant( left, *width_out, + if (optimizeDivides) { + llvm::APInt divisor = CE->getAPValue(); + if (divisor != llvm::APInt(CE->getWidth(),1, false /*unsigned*/) && + divisor != llvm::APInt(CE->getWidth(), -1, true /*signed*/)) + if (*width_out == 32) //only works for 32-bit division + return constructSDivByConstant( left, *width_out, CE->getZExtValue(32)); - + } // XXX need to test for proper handling of sign, not sure I // trust STP ExprHandle right = construct(de->right, width_out); diff --git a/test/regression/2015-08-30-sdiv-1.c b/test/regression/2015-08-30-sdiv-1.c new file mode 100644 index 00000000..a90df308 --- /dev/null +++ b/test/regression/2015-08-30-sdiv-1.c @@ -0,0 +1,19 @@ +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -exit-on-error -solver-optimize-divides=true %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -exit-on-error -solver-optimize-divides=false %t.bc + +/* Division by constant can be optimized.using mul/shift + * For signed division, div by 1 or -1 cannot be optimized like that. + */ +#include <stdint.h> +int main() { + int32_t dividend; + klee_make_symbolic(÷nd, sizeof dividend, "Dividend"); + if ((3 ^ (dividend & 2)) / 1) + return 1; + if ((3 ^ (dividend & 2)) / -1) + return 1; + return 0; +} |