Fixed overshift of logical right shift by symbolic so that it overshifts

to zero. Test case is included.

3 files changed, 40 insertions, 13 deletions

diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 7e004445..24004c2a 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -228,22 +228,23 @@ ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle shift) {
 }
 
 // logical right shift by a variable amount on an expression of the specified width
-ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle amount, unsigned width) {
+ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle shift) {
+  unsigned width = vc_getBVLength(vc, expr);
   ExprHandle res = bvZero(width);
 
-  int shiftBits = getShiftBits( width );
-
-  //get the shift amount (looking only at the bits appropriate for the given width)
-  ExprHandle shift = vc_bvExtract( vc, amount, shiftBits - 1, 0 ); 
-
   //construct a big if-then-elif-elif-... with one case per possible shift amount
   for( int i=width-1; i>=0; i-- ) {
     res = vc_iteExpr(vc,
-                     eqExpr(shift, bvConst32(shiftBits, i)),
-                     bvRightShift(expr, i, shiftBits),
+                     eqExpr(shift, bvConst32(width, i)),
+                     bvRightShift(expr, i, width),
                      res);
   }
 
+  // If overshifting, shift to zero
+  res = vc_iteExpr(vc,
+                   vc_bvLtExpr(vc, shift, bvConst32(width, width)),
+                   res,
+                   bvZero(width));
   return res;
 }
 
@@ -367,9 +368,9 @@ ExprHandle STPBuilder::constructUDivByConstant(ExprHandle expr_n, unsigned width
 
   // n/d = (((n - t1) >> sh1) + t1) >> sh2;
   ExprHandle n_minus_t1  = vc_bvMinusExpr( vc, width, expr_n, t1 );
-  ExprHandle shift_sh1   = bvVarRightShift( n_minus_t1, expr_sh1, 32 );
+  ExprHandle shift_sh1   = bvVarRightShift( n_minus_t1, expr_sh1);
   ExprHandle plus_t1     = vc_bvPlusExpr( vc, width, shift_sh1, t1 );
-  ExprHandle res         = bvVarRightShift( plus_t1, expr_sh2, 32 );
+  ExprHandle res         = bvVarRightShift( plus_t1, expr_sh2);
 
   return res;
 }
@@ -407,7 +408,7 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width
   // Improved variable arithmetic right shift: sign extend, shift,
   // extract.
   ExprHandle extend_npm   = vc_bvSignExtend( vc, n_plus_mulsh, 64 );
-  ExprHandle shift_npm    = bvVarRightShift( extend_npm, expr_shpost, 64 );
+  ExprHandle shift_npm    = bvVarRightShift( extend_npm, expr_shpost);
   ExprHandle shift_shpost = vc_bvExtract( vc, shift_npm, 31, 0 ); //lower 32-bits
 
   // XSIGN(n) is -1 if n is negative, positive one otherwise
@@ -830,7 +831,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     } else {
       int shiftWidth;
       ExprHandle amount = construct(lse->right, &shiftWidth);
-      return bvVarRightShift( left, amount, *width_out );
+      return bvVarRightShift( left, amount);
     }
   }
 
diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h
index 90061784..828c267d 100644
--- a/lib/Solver/STPBuilder.h
+++ b/lib/Solver/STPBuilder.h
@@ -103,7 +103,7 @@ private:
   ExprHandle bvLeftShift(ExprHandle expr, unsigned shift);
   ExprHandle bvRightShift(ExprHandle expr, unsigned amount, unsigned shiftBits);
   ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle shift);
-  ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle amount, unsigned width);
+  ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle shift);
   ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle amount, unsigned width);
 
   ExprHandle constructAShrByConstant(ExprHandle expr, unsigned shift, 
diff --git a/test/Solver/overshift-lright-by-symbolic.kquery b/test/Solver/overshift-lright-by-symbolic.kquery
new file mode 100644
index 00000000..7ca6d4d5
--- /dev/null
+++ b/test/Solver/overshift-lright-by-symbolic.kquery
@@ -0,0 +1,26 @@
+# RUN: %kleaver %s > %t
+# RUN: not grep INVALID %t
+
+array shift[4] : w32 -> w8 = symbolic
+# ∀ x. x >= 32 → ( (2 >> x) = 0 )
+# Check we logical right overshift to zero when shifting a constant ALWAYS!
+
+(query [ (Ule  (w32 32) (ReadLSB w32 (w32 0) shift)) ]
+    (Eq
+        (LShr w32 (w32 2)
+            (ReadLSB w32 (w32 0) shift)
+        )
+        (w32 0)
+    ) [ ] [shift] )
+
+# 64-bit version
+# ∀ x. x >= 64 → ( (2 >> x) = 0 )
+array shift64[8] : w32 -> w8 = symbolic
+
+(query [ (Ule  (w64 64) (ReadLSB w64 (w32 0) shift64)) ]
+    (Eq
+        (LShr w64 (w64 2)
+            (ReadLSB w64 (w32 0) shift64)
+        )
+        (w64 0)
+    ) [ ] [shift64] )