diff options
| author | Hoang M. Le <hle@informatik.uni-bremen.de> | 2016-05-31 15:52:35 +0200 |
|---|---|---|
| committer | Hoang M. Le <hle@informatik.uni-bremen.de> | 2016-06-10 12:15:39 +0200 |
| commit | 5adb60b974ff40d7a298b9de558e9feb6adf030f (patch) | |
| tree | df322c0521acca35159c7c00d91be94cfaa0e868 /lib | |
| parent | 05a7b4c79603c5803cff1cc0e82d3e666ff486a2 (diff) | |
| download | klee-5adb60b974ff40d7a298b9de558e9feb6adf030f.tar.gz | |
handle special cases of sdiv 1 and -1
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Solver/MetaSMTBuilder.h | 12 |
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; } |