diff options
author | Hoang M. Le <hle@informatik.uni-bremen.de> | 2016-06-10 13:01:46 +0200 |
---|---|---|
committer | Hoang M. Le <hle@informatik.uni-bremen.de> | 2016-06-10 13:01:46 +0200 |
commit | c068e3c8418d836ca88ba64a10cb5fce4e796b0d (patch) | |
tree | 54de9d65a0c524ffce942840cb3fcae69a936ba5 /lib/Solver | |
parent | a3d7313ac9f844bd42d33f7e0dea08fee768a837 (diff) | |
download | klee-c068e3c8418d836ca88ba64a10cb5fce4e796b0d.tar.gz |
remove bitmasking shift amount in bvVarLeftShift
Diffstat (limited to 'lib/Solver')
-rw-r--r-- | lib/Solver/MetaSMTBuilder.h | 13 |
1 files changed, 4 insertions, 9 deletions
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index 9328a8f3..b073b57c 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -114,7 +114,7 @@ public: //logical left and right shift (not arithmetic) typename SolverContext::result_type bvLeftShift(typename SolverContext::result_type expr, unsigned width, unsigned shift); typename SolverContext::result_type bvRightShift(typename SolverContext::result_type expr, unsigned width, unsigned shift); - typename SolverContext::result_type bvVarLeftShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width); + typename SolverContext::result_type bvVarLeftShift(typename SolverContext::result_type expr, typename SolverContext::result_type shift, unsigned width); typename SolverContext::result_type bvVarRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width); typename SolverContext::result_type bvVarArithRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width); @@ -480,24 +480,19 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvRightShift( // left shift by a variable amount on an expression of the specified width template<typename SolverContext> -typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarLeftShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width) { +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarLeftShift(typename SolverContext::result_type expr, typename SolverContext::result_type shift, unsigned width) { typename SolverContext::result_type res = bvZero(width); - - int shiftBits = getShiftBits(width); - - //get the shift amount (looking only at the bits appropriate for the given width) - typename SolverContext::result_type shift = evaluate(_solver, extract(shiftBits - 1, 0, amount)); //construct a big if-then-elif-elif-... with one case per possible shift amount for(int i = width - 1; i >= 0; i--) { - res = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits, i)), + res = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(width, i)), bvLeftShift(expr, width, i), res)); } // If overshifting, shift to zero - res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(shiftBits, width)), + res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(width, width)), res, bvZero(width))); |