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-06-10 13:01:46 +0200
committerHoang M. Le <hle@informatik.uni-bremen.de>2016-06-10 13:01:46 +0200
commitc068e3c8418d836ca88ba64a10cb5fce4e796b0d (patch)
tree54de9d65a0c524ffce942840cb3fcae69a936ba5 /lib/Solver
parenta3d7313ac9f844bd42d33f7e0dea08fee768a837 (diff)
downloadklee-c068e3c8418d836ca88ba64a10cb5fce4e796b0d.tar.gz
remove bitmasking shift amount in bvVarLeftShift
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/MetaSMTBuilder.h13
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)));