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 12:48:43 +0200
committerHoang M. Le <hle@informatik.uni-bremen.de>2016-06-10 12:48:43 +0200
commita3d7313ac9f844bd42d33f7e0dea08fee768a837 (patch)
treeaeed918e792cedb052bf6866c67f3412c51c99db /lib/Solver
parentd4f5d50f53b37223b62047782a3e86839922093b (diff)
downloadklee-a3d7313ac9f844bd42d33f7e0dea08fee768a837.tar.gz
remove bitmasking shift amount in constructAShrByConstant and make it return 0 when overshifting
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/MetaSMTBuilder.h15
1 files changed, 7 insertions, 8 deletions
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index c31ea8c8..9328a8f3 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -141,7 +141,7 @@ private:
     typename SolverContext::result_type eqExpr(typename SolverContext::result_type a, typename SolverContext::result_type b);
     
     typename SolverContext::result_type constructAShrByConstant(typename SolverContext::result_type expr, unsigned width, unsigned shift, 
-                                                                typename SolverContext::result_type isSigned, unsigned shiftBits);
+                                                                typename SolverContext::result_type isSigned);
     typename SolverContext::result_type constructMulByConstant(typename SolverContext::result_type expr, unsigned width, uint64_t x);
     typename SolverContext::result_type constructUDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d);
     typename SolverContext::result_type constructSDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d);
@@ -275,16 +275,15 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::eqExpr(typena
 }
 
 template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructAShrByConstant(typename SolverContext::result_type expr, unsigned width, unsigned amount,
-                                                                                           typename SolverContext::result_type isSigned, unsigned shiftBits) {
-    unsigned shift = amount & ((1 << shiftBits) - 1);
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructAShrByConstant(typename SolverContext::result_type expr, unsigned width, unsigned shift,
+                                                                                           typename SolverContext::result_type isSigned) {
     typename SolverContext::result_type res;
     
     if (shift == 0) {
         res = expr;
     }
     else if (shift >= width) {
-        res = evaluate(_solver, metaSMT::logic::Ite(isSigned, bvMinusOne(width), bvZero(width)));
+        res = bvZero(width);
     }
     else {
         res = evaluate(_solver, metaSMT::logic::Ite(isSigned,
@@ -545,14 +544,14 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarArithRig
     typename SolverContext::result_type signedBool = bvBoolExtract(expr, width - 1);
 
     //start with the result if shifting by width-1
-    typename SolverContext::result_type res =  constructAShrByConstant(expr, width, width - 1, signedBool, shiftBits);
+    typename SolverContext::result_type res =  constructAShrByConstant(expr, width, width - 1, signedBool);
 
     // construct a big if-then-elif-elif-... with one case per possible shift amount
     // XXX more efficient to move the ite on the sign outside all exprs?
     // XXX more efficient to sign extend, right shift, then extract lower bits?
     for (int i = width - 2; i >= 0; i--) {
         res = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits,i)),
-                                                    constructAShrByConstant(expr, width, i, signedBool, shiftBits),
+                                                    constructAShrByConstant(expr, width, i, signedBool),
                                                     res));
     }
     
@@ -1059,7 +1058,7 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu
 	    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) {
 	        unsigned shift = (unsigned) CE->getLimitedValue();
                 typename SolverContext::result_type signedBool = bvBoolExtract(left_expr, *width_out - 1);
-		res = constructAShrByConstant(left_expr, *width_out, shift, signedBool, getShiftBits(*width_out));	      
+        res = constructAShrByConstant(left_expr, *width_out, shift, signedBool);
 	    }
 	    else {
                 int shiftWidth = 0;