Merge pull request #64 from delcypher/overshift-fix

Overshift fixes

12 files changed, 369 insertions, 67 deletions

diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 90252656..ad0df3c2 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -174,14 +174,13 @@ ExprHandle STPBuilder::eqExpr(ExprHandle a, ExprHandle b) {
 }
 
 // logical right shift
-ExprHandle STPBuilder::bvRightShift(ExprHandle expr, unsigned amount, unsigned shiftBits) {
+ExprHandle STPBuilder::bvRightShift(ExprHandle expr, unsigned shift) {
   unsigned width = vc_getBVLength(vc, expr);
-  unsigned shift = amount & ((1<<shiftBits) - 1);
 
   if (shift==0) {
     return expr;
   } else if (shift>=width) {
-    return bvZero(width);
+    return bvZero(width); // Overshift to zero
   } else {
     return vc_bvConcatExpr(vc,
                            bvZero(shift),
@@ -190,14 +189,13 @@ ExprHandle STPBuilder::bvRightShift(ExprHandle expr, unsigned amount, unsigned s
 }
 
 // logical left shift
-ExprHandle STPBuilder::bvLeftShift(ExprHandle expr, unsigned amount, unsigned shiftBits) {
+ExprHandle STPBuilder::bvLeftShift(ExprHandle expr, unsigned shift) {
   unsigned width = vc_getBVLength(vc, expr);
-  unsigned shift = amount & ((1<<shiftBits) - 1);
 
   if (shift==0) {
     return expr;
   } else if (shift>=width) {
-    return bvZero(width);
+    return bvZero(width); // Overshift to zero
   } else {
     // stp shift does "expr @ [0 x s]" which we then have to extract,
     // rolling our own gives slightly smaller exprs
@@ -208,96 +206,97 @@ ExprHandle STPBuilder::bvLeftShift(ExprHandle expr, unsigned amount, unsigned sh
 }
 
 // left shift by a variable amount on an expression of the specified width
-ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle amount, unsigned width) {
+ExprHandle STPBuilder::bvVarLeftShift(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)),
-                     bvLeftShift(expr, i, shiftBits),
+                     eqExpr(shift, bvConst32(width, i)),
+                     bvLeftShift(expr, i),
                      res);
   }
+
+  // If overshifting, shift to zero
+  res = vc_iteExpr(vc,
+                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
+                   res,
+                   bvZero(width));
   return res;
 }
 
 // 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),
                      res);
   }
 
+  // If overshifting, shift to zero
+  res = vc_iteExpr(vc,
+                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
+                   res,
+                   bvZero(width));
   return res;
 }
 
 // arithmetic right shift by a variable amount on an expression of the specified width
-ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle amount, unsigned 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 );
+ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) {
+  unsigned width = vc_getBVLength(vc, expr);
 
   //get the sign bit to fill with
   ExprHandle signedBool = bvBoolExtract(expr, width-1);
 
   //start with the result if shifting by width-1
-  ExprHandle res = constructAShrByConstant(expr, width-1, signedBool, shiftBits);
+  ExprHandle res = constructAShrByConstant(expr, 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 = vc_iteExpr(vc,
-                     eqExpr(shift, bvConst32(shiftBits,i)),
+                     eqExpr(shift, bvConst32(width,i)),
                      constructAShrByConstant(expr, 
                                              i, 
-                                             signedBool, 
-                                             shiftBits),
+                                             signedBool),
                      res);
   }
 
+  // If overshifting, shift to zero
+  res = vc_iteExpr(vc,
+                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
+                   res,
+                   bvZero(width));
   return res;
 }
 
 ExprHandle STPBuilder::constructAShrByConstant(ExprHandle expr,
-                                               unsigned amount,
-                                               ExprHandle isSigned, 
-                                               unsigned shiftBits) {
+                                               unsigned shift,
+                                               ExprHandle isSigned) {
   unsigned width = vc_getBVLength(vc, expr);
-  unsigned shift = amount & ((1<<shiftBits) - 1);
 
   if (shift==0) {
     return expr;
   } else if (shift>=width-1) {
-    return vc_iteExpr(vc, isSigned, bvMinusOne(width), bvZero(width));
+    return bvZero(width); // Overshift to zero
   } else {
     return vc_iteExpr(vc,
                       isSigned,
                       ExprHandle(vc_bvConcatExpr(vc,
                                                  bvMinusOne(shift),
                                                  bvExtract(expr, width - 1, shift))),
-                      bvRightShift(expr, shift, shiftBits));
+                      bvRightShift(expr, shift));
   }
 }
 
 ExprHandle STPBuilder::constructMulByConstant(ExprHandle expr, unsigned width, uint64_t x) {
-  unsigned shiftBits = getShiftBits(width);
   uint64_t add, sub;
   ExprHandle res = 0;
 
@@ -313,7 +312,7 @@ ExprHandle STPBuilder::constructMulByConstant(ExprHandle expr, unsigned width, u
 
     if ((add&bit) || (sub&bit)) {
       assert(!((add&bit) && (sub&bit)) && "invalid mult constants");
-      ExprHandle op = bvLeftShift(expr, j, shiftBits);
+      ExprHandle op = bvLeftShift(expr, j);
       
       if (add&bit) {
         if (res) {
@@ -367,9 +366,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 +406,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
@@ -659,8 +658,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
       
         if (bits64::isPowerOfTwo(divisor)) {
           return bvRightShift(left,
-                              bits64::indexOfSingleBit(divisor),
-                              getShiftBits(*width_out));
+                              bits64::indexOfSingleBit(divisor));
         } else if (optimizeDivides) {
           if (*width_out == 32) //only works for 32-bit division
             return constructUDivByConstant( left, *width_out, 
@@ -810,28 +808,25 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized shl");
 
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(se->right)) {
-      return bvLeftShift(left, (unsigned) CE->getLimitedValue(), 
-                         getShiftBits(*width_out));
+      return bvLeftShift(left, (unsigned) CE->getLimitedValue());
     } else {
       int shiftWidth;
       ExprHandle amount = construct(se->right, &shiftWidth);
-      return bvVarLeftShift( left, amount, *width_out );
+      return bvVarLeftShift( left, amount);
     }
   }
 
   case Expr::LShr: {
     LShrExpr *lse = cast<LShrExpr>(e);
     ExprHandle left = construct(lse->left, width_out);
-    unsigned shiftBits = getShiftBits(*width_out);
     assert(*width_out!=1 && "uncanonicalized lshr");
 
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(lse->right)) {
-      return bvRightShift(left, (unsigned) CE->getLimitedValue(), 
-                          shiftBits);
+      return bvRightShift(left, (unsigned) CE->getLimitedValue());
     } else {
       int shiftWidth;
       ExprHandle amount = construct(lse->right, &shiftWidth);
-      return bvVarRightShift( left, amount, *width_out );
+      return bvVarRightShift( left, amount);
     }
   }
 
@@ -843,12 +838,11 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) {
       unsigned shift = (unsigned) CE->getLimitedValue();
       ExprHandle signedBool = bvBoolExtract(left, *width_out-1);
-      return constructAShrByConstant(left, shift, signedBool, 
-                                     getShiftBits(*width_out));
+      return constructAShrByConstant(left, shift, signedBool);
     } else {
       int shiftWidth;
       ExprHandle amount = construct(ase->right, &shiftWidth);
-      return bvVarArithRightShift( left, amount, *width_out );
+      return bvVarArithRightShift( left, amount);
     }
   }
 
diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h
index 0a99b753..ef1cd8b3 100644
--- a/lib/Solver/STPBuilder.h
+++ b/lib/Solver/STPBuilder.h
@@ -79,13 +79,6 @@ class STPBuilder {
   STPArrayExprHash _arr_hash;
 
 private:  
-  unsigned getShiftBits(unsigned amount) {
-    unsigned bits = 1;
-    amount--;
-    while (amount >>= 1)
-      bits++;
-    return bits;
-  }
 
   ExprHandle bvOne(unsigned width);
   ExprHandle bvZero(unsigned width);
@@ -100,14 +93,14 @@ private:
   ExprHandle eqExpr(ExprHandle a, ExprHandle b);
 
   //logical left and right shift (not arithmetic)
-  ExprHandle bvLeftShift(ExprHandle expr, unsigned shift, unsigned shiftBits);
-  ExprHandle bvRightShift(ExprHandle expr, unsigned amount, unsigned shiftBits);
-  ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle amount, unsigned width);
-  ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle amount, unsigned width);
-  ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle amount, unsigned width);
+  ExprHandle bvLeftShift(ExprHandle expr, unsigned shift);
+  ExprHandle bvRightShift(ExprHandle expr, unsigned shift);
+  ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle shift);
+  ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle shift);
+  ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle shift);
 
   ExprHandle constructAShrByConstant(ExprHandle expr, unsigned shift, 
-                                     ExprHandle isSigned, unsigned shiftBits);
+                                     ExprHandle isSigned);
   ExprHandle constructMulByConstant(ExprHandle expr, unsigned width, uint64_t x);
   ExprHandle constructUDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d);
   ExprHandle constructSDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d);
diff --git a/test/Feature/arithmetic-right-overshift-sym-conc.c b/test/Feature/arithmetic-right-overshift-sym-conc.c
new file mode 100644
index 00000000..81995b2b
--- /dev/null
+++ b/test/Feature/arithmetic-right-overshift-sym-conc.c
@@ -0,0 +1,65 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: %klee -use-cex-cache=1 -check-overshift=0 %t.bc
+// RUN: not grep "ASSERTION FAIL" %T/klee-last/messages.txt
+// RUN: grep "KLEE: done: explored paths = 1" %T/klee-last/info
+#include <stdio.h>
+#include <assert.h>
+
+typedef enum
+{
+    TO_ZERO,
+    MASKED,
+    UNKNOWN
+} overshift_t;
+
+// We're using signed ints so should be doing
+// arithmetic right shift.
+int overshift(volatile unsigned int y, const char * type)
+{
+    overshift_t ret;
+    volatile signed int x=15;
+    unsigned int limit = sizeof(x)*8;
+
+    volatile signed int result;
+    result = x >> y; // Potential overshift
+
+    if (result ==0)
+    {
+        printf("%s : Overshift to zero\n", type);
+        ret = TO_ZERO;
+    }
+    else if (result == ( x >> (y % limit)) )
+    {
+        printf("%s : Bitmasked overshift\n", type);
+        ret = MASKED;
+    }
+    else
+    {
+        printf("%s : Unrecognised behaviour.\n", type);
+        ret = UNKNOWN;
+    }
+
+    return ret;
+}
+
+int main(int argc, char** argv)
+{
+    // Concrete overshift
+    volatile unsigned int y = sizeof(unsigned int)*8;
+    overshift_t conc = overshift(y, "Concrete");
+    assert( conc == TO_ZERO);
+
+    // Symbolic overshift
+    volatile unsigned int y2;
+    klee_make_symbolic(&y2,sizeof(y),"y2");
+    // Add constraints so only one value possible
+    klee_assume(y2 > (y-1));
+    klee_assume(y2 < (y+1));
+    overshift_t sym = overshift(y2, "Symbolic");
+    assert( sym == TO_ZERO);
+
+    // Concrete and symbolic behaviour should be the same
+    assert( conc == sym);
+
+    return 0;
+}
diff --git a/test/Feature/left-overshift-sym-conc.c b/test/Feature/left-overshift-sym-conc.c
new file mode 100644
index 00000000..e962fa28
--- /dev/null
+++ b/test/Feature/left-overshift-sym-conc.c
@@ -0,0 +1,63 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: %klee -use-cex-cache=1 -check-overshift=0 %t.bc
+// RUN: not grep "ASSERTION FAIL" %T/klee-last/messages.txt
+// RUN: grep "KLEE: done: explored paths = 1" %T/klee-last/info
+#include <stdio.h>
+#include <assert.h>
+
+typedef enum
+{
+    TO_ZERO,
+    MASKED,
+    UNKNOWN
+} overshift_t;
+
+int overshift(volatile unsigned int y, const char * type)
+{
+    overshift_t ret;
+    volatile unsigned int x=15;
+    unsigned int limit = sizeof(x)*8;
+
+    volatile unsigned int result;
+    result = x << y; // Potential overshift
+
+    if (result ==0)
+    {
+        printf("%s : Overshift to zero\n", type);
+        ret = TO_ZERO;
+    }
+    else if (result == ( x << (y % limit)) )
+    {
+        printf("%s : Bitmasked overshift\n", type);
+        ret = MASKED;
+    }
+    else
+    {
+        printf("%s : Unrecognised behaviour.\n", type);
+        ret = UNKNOWN;
+    }
+
+    return ret;
+}
+
+int main(int argc, char** argv)
+{
+    // Concrete overshift
+    volatile unsigned int y = sizeof(unsigned int)*8;
+    overshift_t conc = overshift(y, "Concrete");
+    assert( conc == TO_ZERO);
+
+    // Symbolic overshift
+    volatile unsigned int y2;
+    klee_make_symbolic(&y2,sizeof(y),"y2");
+    // Add constraints so only one value possible
+    klee_assume(y2 > (y-1));
+    klee_assume(y2 < (y+1));
+    overshift_t sym = overshift(y2, "Symbolic");
+    assert( sym == TO_ZERO);
+
+    // Concrete and symbolic behaviour should be the same
+    assert( conc == sym);
+
+    return 0;
+}
diff --git a/test/Feature/logical-right-overshift-sym-conc.c b/test/Feature/logical-right-overshift-sym-conc.c
new file mode 100644
index 00000000..00281ec4
--- /dev/null
+++ b/test/Feature/logical-right-overshift-sym-conc.c
@@ -0,0 +1,65 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: %klee -use-cex-cache=1 -check-overshift=0 %t.bc
+// RUN: not grep "ASSERTION FAIL" %T/klee-last/messages.txt
+// RUN: grep "KLEE: done: explored paths = 1" %T/klee-last/info
+#include <stdio.h>
+#include <assert.h>
+
+typedef enum
+{
+    TO_ZERO,
+    MASKED,
+    UNKNOWN
+} overshift_t;
+
+// We're using unsigned ints so should be doing
+// logical right shift.
+int overshift(volatile unsigned int y, const char * type)
+{
+    overshift_t ret;
+    volatile unsigned int x=15;
+    unsigned int limit = sizeof(x)*8;
+
+    volatile unsigned int result;
+    result = x >> y; // Potential overshift
+
+    if (result ==0)
+    {
+        printf("%s : Overshift to zero\n", type);
+        ret = TO_ZERO;
+    }
+    else if (result == ( x >> (y % limit)) )
+    {
+        printf("%s : Bitmasked overshift\n", type);
+        ret = MASKED;
+    }
+    else
+    {
+        printf("%s : Unrecognised behaviour.\n", type);
+        ret = UNKNOWN;
+    }
+
+    return ret;
+}
+
+int main(int argc, char** argv)
+{
+    // Concrete overshift
+    volatile unsigned int y = sizeof(unsigned int)*8;
+    overshift_t conc = overshift(y, "Concrete");
+    assert( conc == TO_ZERO);
+
+    // Symbolic overshift
+    volatile unsigned int y2;
+    klee_make_symbolic(&y2,sizeof(y),"y2");
+    // Add constraints so only one value possible
+    klee_assume(y2 > (y-1));
+    klee_assume(y2 < (y+1));
+    overshift_t sym = overshift(y2, "Symbolic");
+    assert( sym == TO_ZERO);
+
+    // Concrete and symbolic behaviour should be the same
+    assert( conc == sym);
+
+    return 0;
+}
diff --git a/test/Solver/lit.local.cfg b/test/Solver/lit.local.cfg
new file mode 100644
index 00000000..d64daf29
--- /dev/null
+++ b/test/Solver/lit.local.cfg
@@ -0,0 +1,2 @@
+# Look for .kquery files too
+config.suffixes.add('.kquery')
diff --git a/test/Solver/overshift-aright-by-constant.kquery b/test/Solver/overshift-aright-by-constant.kquery
new file mode 100644
index 00000000..c21889e2
--- /dev/null
+++ b/test/Solver/overshift-aright-by-constant.kquery
@@ -0,0 +1,14 @@
+# RUN: %kleaver %s > %t
+# RUN: not grep INVALID %t
+array x[4] : w32 -> w8 = symbolic
+# ∀ x. x > 0 → ( ((signed int) x) >> 32  = 0 )
+# Check we overshift to zero for when shifting for all 32-bit values >0
+
+(query [ (Ult  (w32 0) (ReadLSB w32 (w32 0) x)) ]
+    (Eq
+        (AShr w32
+            (ReadLSB w32 (w32 0) x)
+            (w32 32)
+        )
+        (w32 0)
+    ) [ ] [x] )
diff --git a/test/Solver/overshift-aright-by-symbolic.kquery b/test/Solver/overshift-aright-by-symbolic.kquery
new file mode 100644
index 00000000..af563ea3
--- /dev/null
+++ b/test/Solver/overshift-aright-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 → ( ( ( (signed int)2 ) >> x) = 0 )
+# Check we arithmetic right overshift to zero when shifting a constant ALWAYS!
+
+(query [ (Ule  (w32 32) (ReadLSB w32 (w32 0) shift)) ]
+    (Eq
+        (AShr w32 (w32 2)
+            (ReadLSB w32 (w32 0) shift)
+        )
+        (w32 0)
+    ) [ ] [shift] )
+
+# 64-bit version
+# ∀ x. x >= 64 → ( (((signed int) 2) >> x) = 0 )
+array shift64[8] : w32 -> w8 = symbolic
+
+(query [ (Ule  (w64 64) (ReadLSB w64 (w32 0) shift64)) ]
+    (Eq
+        (AShr w64 (w64 2)
+            (ReadLSB w64 (w32 0) shift64)
+        )
+        (w64 0)
+    ) [ ] [shift64] )
diff --git a/test/Solver/overshift-left-by-constant.kquery b/test/Solver/overshift-left-by-constant.kquery
new file mode 100644
index 00000000..e0709100
--- /dev/null
+++ b/test/Solver/overshift-left-by-constant.kquery
@@ -0,0 +1,14 @@
+# RUN: %kleaver %s > %t
+# RUN: not grep INVALID %t
+array x[4] : w32 -> w8 = symbolic
+# ∀ x. x > 0 → ( x << 32  = 0 )
+# Check we overshift to zero for when shifting for all 32-bit values >0
+
+(query [ (Ult  (w32 0) (ReadLSB w32 (w32 0) x)) ]
+    (Eq
+        (Shl w32
+            (ReadLSB w32 (w32 0) x)
+            (w32 32)
+        )
+        (w32 0)
+    ) [ ] [x] )
diff --git a/test/Solver/overshift-left-by-symbolic.kquery b/test/Solver/overshift-left-by-symbolic.kquery
new file mode 100644
index 00000000..9d0d272c
--- /dev/null
+++ b/test/Solver/overshift-left-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 left overshift to zero when shifting a constant ALWAYS!
+
+(query [ (Ule  (w32 32) (ReadLSB w32 (w32 0) shift)) ]
+    (Eq
+        (Shl 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
+        (Shl w64 (w64 2)
+            (ReadLSB w64 (w32 0) shift64)
+        )
+        (w64 0)
+    ) [ ] [shift64] )
diff --git a/test/Solver/overshift-lright-by-constant.kquery b/test/Solver/overshift-lright-by-constant.kquery
new file mode 100644
index 00000000..cb223dd5
--- /dev/null
+++ b/test/Solver/overshift-lright-by-constant.kquery
@@ -0,0 +1,14 @@
+# RUN: %kleaver %s > %t
+# RUN: not grep INVALID %t
+array x[4] : w32 -> w8 = symbolic
+# ∀ x. x > 0 → ( x >> 32  = 0 )
+# Check we overshift to zero for when shifting for all 32-bit values >0
+
+(query [ (Ult  (w32 0) (ReadLSB w32 (w32 0) x)) ]
+    (Eq
+        (LShr w32
+            (ReadLSB w32 (w32 0) x)
+            (w32 32)
+        )
+        (w32 0)
+    ) [ ] [x] )
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] )