Merge pull request #274 from MartinNowack/fix_sdiv_1

Fix signed division by constant 1/ -1

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(&dividend, sizeof dividend, "Dividend");
+  if ((3 ^ (dividend & 2)) / 1)
+    return 1;
+  if ((3 ^ (dividend & 2)) / -1)
+    return 1;
+  return 0;
+}