about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
authorHoang M. Le <hle@informatik.uni-bremen.de>2016-05-31 15:52:35 +0200
committerHoang M. Le <hle@informatik.uni-bremen.de>2016-06-10 12:15:39 +0200
commit5adb60b974ff40d7a298b9de558e9feb6adf030f (patch)
treedf322c0521acca35159c7c00d91be94cfaa0e868 /lib/Solver
parent05a7b4c79603c5803cff1cc0e82d3e666ff486a2 (diff)
downloadklee-5adb60b974ff40d7a298b9de558e9feb6adf030f.tar.gz
handle special cases of sdiv 1 and -1
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/MetaSMTBuilder.h12
1 files changed, 9 insertions, 3 deletions
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index 9aca9f83..ebbfa814 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -843,12 +843,18 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu
             typename SolverContext::result_type left_expr = construct(de->left, width_out);
             assert(*width_out != 1 && "uncanonicalized sdiv");
 
+            bool optimized = false;
             ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right);
             if (CE && _optimizeDivides && (*width_out == 32)) {
-                res = constructSDivByConstant(left_expr, *width_out, CE->getZExtValue(32));
+                llvm::APInt divisor = CE->getAPValue();
+                if (divisor != llvm::APInt(CE->getWidth(),  1, false /*unsigned*/) &&
+                    divisor != llvm::APInt(CE->getWidth(), -1, true /*signed*/)) {
+                  res = constructSDivByConstant(left_expr, *width_out, CE->getZExtValue(32));
+                  optimized = true;
+                }
             }
-            else {
-                res = evaluate(_solver, bvsdiv(left_expr, construct(de->right, width_out))); 
+            if (!optimized) {
+                res = evaluate(_solver, bvsdiv(left_expr, construct(de->right, width_out)));
             }
             break;
         }