about summary refs log tree commit diff homepage
path: root/lib/Solver/MetaSMTBuilder.h
diff options
context:
space:
mode:
authorHoang M. Le <hle@informatik.uni-bremen.de>2016-06-10 12:26:17 +0200
committerHoang M. Le <hle@informatik.uni-bremen.de>2016-06-10 12:26:17 +0200
commit29bb394fa10cae48dda7c7c59c27f263fe1434ec (patch)
tree6535d029ddcf612856bc45fe200d64e255b00bdf /lib/Solver/MetaSMTBuilder.h
parent5adb60b974ff40d7a298b9de558e9feb6adf030f (diff)
downloadklee-29bb394fa10cae48dda7c7c59c27f263fe1434ec.tar.gz
remove bitmasking shift amount in bvLeftShift
Diffstat (limited to 'lib/Solver/MetaSMTBuilder.h')
-rw-r--r--lib/Solver/MetaSMTBuilder.h11
1 files changed, 5 insertions, 6 deletions
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index ebbfa814..a636586e 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -112,7 +112,7 @@ public:
     typename SolverContext::result_type bvSExtConst(unsigned width, uint64_t value);
     
     //logical left and right shift (not arithmetic)
-    typename SolverContext::result_type bvLeftShift(typename SolverContext::result_type expr, unsigned width, unsigned shift, unsigned shiftBits);
+    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 amount, unsigned shiftBits);
     typename SolverContext::result_type bvVarLeftShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width);
     typename SolverContext::result_type bvVarRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width);
@@ -317,7 +317,7 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructMulB
         if ((add & bit) || (sub & bit)) {
             assert(!((add & bit) && (sub & bit)) && "invalid mult constants");
 
-            typename SolverContext::result_type op = bvLeftShift(expr, width, j, shiftBits);
+            typename SolverContext::result_type op = bvLeftShift(expr, width, j);
 
             if (add & bit) {
                 if (!first) {
@@ -440,10 +440,9 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructSDiv
 }
 
 template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvLeftShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits) {
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvLeftShift(typename SolverContext::result_type expr, unsigned width, unsigned shift) {
     
     typename SolverContext::result_type res;    
-    unsigned shift = amount & ((1 << shiftBits) - 1);
 
     if (shift == 0) {
         res = expr;
@@ -495,7 +494,7 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarLeftShif
     //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)),
-                                                    bvLeftShift(expr, width, i, shiftBits),
+                                                    bvLeftShift(expr, width, i),
                                                     res));
     }
     
@@ -1017,7 +1016,7 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu
 	    assert(*width_out != 1 && "uncanonicalized shl");
 	    
 	    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(se->right)) {
-	        res =  bvLeftShift(left_expr, *width_out, (unsigned) CE->getLimitedValue(), getShiftBits(*width_out));
+            res =  bvLeftShift(left_expr, *width_out, (unsigned) CE->getLimitedValue());
             }
             else {
                 int shiftWidth = 0;