From 3160935d77c3fd6d24be7fddd5c570d6b3944c18 Mon Sep 17 00:00:00 2001
From: Paul Marinescu <paul.marinescu@imperial.ac.uk>
Date: Sun, 3 Nov 2013 19:07:20 +0000
Subject: Translate shl overshifts into 0

The other shift operators still need to be changed
---
 lib/Solver/STPBuilder.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 90252656..6cb7dd38 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -223,6 +223,10 @@ ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle amount, unsign
                      bvLeftShift(expr, i, shiftBits),
                      res);
   }
+  res = vc_iteExpr(vc,
+                   vc_bvLtExpr(vc, amount, bvConst32(32, width)),
+                   res,
+                   bvZero(width));
   return res;
 }
 
-- 
cgit 1.4.1


From 458eb00a569445b82decf5687cb4716217ad1ad6 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 7 Nov 2013 10:55:12 +0000
Subject: Added a test case for testing overshift behaviour of Shl and fixed a
 bug in the previous commit where 32-bit width was assumed.

---
 lib/Solver/STPBuilder.cpp                     |  4 +++-
 test/Solver/lit.local.cfg                     |  2 ++
 test/Solver/overshift-left-by-symbolic.kquery | 26 ++++++++++++++++++++++++++
 3 files changed, 31 insertions(+), 1 deletion(-)
 create mode 100644 test/Solver/lit.local.cfg
 create mode 100644 test/Solver/overshift-left-by-symbolic.kquery

diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 6cb7dd38..cdc30f85 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -223,8 +223,10 @@ ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle amount, unsign
                      bvLeftShift(expr, i, shiftBits),
                      res);
   }
+
+  // If overshifting, shift to zero
   res = vc_iteExpr(vc,
-                   vc_bvLtExpr(vc, amount, bvConst32(32, width)),
+                   vc_bvLtExpr(vc, amount, bvConst32(width, width)),
                    res,
                    bvZero(width));
   return res;
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-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] )
-- 
cgit 1.4.1


From ed963d407e5de9b09191324f5e277ea40e1aea0b Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 7 Nov 2013 11:52:18 +0000
Subject: Fixed overshifting an expression by a constant so that we overshift
 to zero. A test case was added for this.

In addition the use to vc_bvExtract()  was removed for shifting left by an
expression because we don't want/need bitmasked behaviour anymore.
---
 lib/Solver/STPBuilder.cpp                     | 27 ++++++++++-----------------
 lib/Solver/STPBuilder.h                       |  4 ++--
 test/Solver/overshift-left-by-constant.kquery | 14 ++++++++++++++
 3 files changed, 26 insertions(+), 19 deletions(-)
 create mode 100644 test/Solver/overshift-left-by-constant.kquery

diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index cdc30f85..7e004445 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -190,14 +190,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,25 +207,21 @@ 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, amount, bvConst32(width, width)),
+                   vc_bvLtExpr(vc, shift, bvConst32(width, width)),
                    res,
                    bvZero(width));
   return res;
@@ -303,7 +298,6 @@ ExprHandle STPBuilder::constructAShrByConstant(ExprHandle expr,
 }
 
 ExprHandle STPBuilder::constructMulByConstant(ExprHandle expr, unsigned width, uint64_t x) {
-  unsigned shiftBits = getShiftBits(width);
   uint64_t add, sub;
   ExprHandle res = 0;
 
@@ -319,7 +313,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) {
@@ -816,12 +810,11 @@ 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);
     }
   }
 
diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h
index 0a99b753..90061784 100644
--- a/lib/Solver/STPBuilder.h
+++ b/lib/Solver/STPBuilder.h
@@ -100,9 +100,9 @@ private:
   ExprHandle eqExpr(ExprHandle a, ExprHandle b);
 
   //logical left and right shift (not arithmetic)
-  ExprHandle bvLeftShift(ExprHandle expr, unsigned shift, unsigned shiftBits);
+  ExprHandle bvLeftShift(ExprHandle expr, unsigned shift);
   ExprHandle bvRightShift(ExprHandle expr, unsigned amount, unsigned shiftBits);
-  ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle amount, unsigned width);
+  ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle shift);
   ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle amount, unsigned width);
   ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle amount, unsigned width);
 
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] )
-- 
cgit 1.4.1


From 207d3aff50cc4bed2adf12819a96fc4254a3d6e6 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 7 Nov 2013 12:17:33 +0000
Subject: Added C test case that checks that concrete and symbolic overshift
 behaviour for left shift are identical.

---
 test/Feature/left-overshift-sym-conc.c | 63 ++++++++++++++++++++++++++++++++++
 1 file changed, 63 insertions(+)
 create mode 100644 test/Feature/left-overshift-sym-conc.c

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;
+}
-- 
cgit 1.4.1


From 71048bea167794f109b2f0b715b6cc1ba8b6eab9 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 7 Nov 2013 14:45:22 +0000
Subject: Fixed overshift of logical right shift by symbolic so that it
 overshifts to zero. Test case is included.

---
 lib/Solver/STPBuilder.cpp                       | 25 ++++++++++++------------
 lib/Solver/STPBuilder.h                         |  2 +-
 test/Solver/overshift-lright-by-symbolic.kquery | 26 +++++++++++++++++++++++++
 3 files changed, 40 insertions(+), 13 deletions(-)
 create mode 100644 test/Solver/overshift-lright-by-symbolic.kquery

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] )
-- 
cgit 1.4.1


From 3be107cbf55f69f063795182690a5f9689e1d805 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 7 Nov 2013 14:59:37 +0000
Subject: Fixed overshift of logical right shift by constant so that it
 overshifts to zero. Test case is included.

---
 lib/Solver/STPBuilder.cpp                       | 16 ++++++----------
 lib/Solver/STPBuilder.h                         |  2 +-
 test/Solver/overshift-lright-by-constant.kquery | 14 ++++++++++++++
 3 files changed, 21 insertions(+), 11 deletions(-)
 create mode 100644 test/Solver/overshift-lright-by-constant.kquery

diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 24004c2a..a92b6f2b 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),
@@ -236,7 +235,7 @@ ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle shift) {
   for( int i=width-1; i>=0; i-- ) {
     res = vc_iteExpr(vc,
                      eqExpr(shift, bvConst32(width, i)),
-                     bvRightShift(expr, i, width),
+                     bvRightShift(expr, i),
                      res);
   }
 
@@ -294,7 +293,7 @@ ExprHandle STPBuilder::constructAShrByConstant(ExprHandle expr,
                       ExprHandle(vc_bvConcatExpr(vc,
                                                  bvMinusOne(shift),
                                                  bvExtract(expr, width - 1, shift))),
-                      bvRightShift(expr, shift, shiftBits));
+                      bvRightShift(expr, shift));
   }
 }
 
@@ -660,8 +659,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, 
@@ -822,12 +820,10 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
   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);
diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h
index 828c267d..48bddeed 100644
--- a/lib/Solver/STPBuilder.h
+++ b/lib/Solver/STPBuilder.h
@@ -101,7 +101,7 @@ private:
 
   //logical left and right shift (not arithmetic)
   ExprHandle bvLeftShift(ExprHandle expr, unsigned shift);
-  ExprHandle bvRightShift(ExprHandle expr, unsigned amount, unsigned shiftBits);
+  ExprHandle bvRightShift(ExprHandle expr, unsigned shift);
   ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle shift);
   ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle shift);
   ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle amount, unsigned width);
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] )
-- 
cgit 1.4.1


From a480b43bf38d4b030d3ceda92549fb721800c026 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 7 Nov 2013 15:02:08 +0000
Subject: Added C test case that checks that concrete and symbolic overshift
 behaviour for logical right shift are identical.

---
 test/Feature/logical-right-overshift-sym-conc.c | 65 +++++++++++++++++++++++++
 1 file changed, 65 insertions(+)
 create mode 100644 test/Feature/logical-right-overshift-sym-conc.c

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..47e0959c
--- /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" klee-last/messages.txt
+// RUN: grep "KLEE: done: explored paths = 1" 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;
+}
-- 
cgit 1.4.1


From 7759c90744bae5c531f765b2faa2475e13f464fd Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 7 Nov 2013 15:21:43 +0000
Subject: Fixed overshift of arithmetic right shift by symbolic so that it
 overshifts to zero. Test case is included.

---
 lib/Solver/STPBuilder.cpp                       | 23 +++++++++++-----------
 lib/Solver/STPBuilder.h                         |  2 +-
 test/Feature/logical-right-overshift-sym-conc.c |  4 ++--
 test/Solver/overshift-aright-by-symbolic.kquery | 26 +++++++++++++++++++++++++
 4 files changed, 41 insertions(+), 14 deletions(-)
 create mode 100644 test/Solver/overshift-aright-by-symbolic.kquery

diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index a92b6f2b..84e88579 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -248,31 +248,33 @@ ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle shift) {
 }
 
 // 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, width);
 
   //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),
+                                             width),
                      res);
   }
 
+  // If overshifting, shift to zero
+  res = vc_iteExpr(vc,
+                   vc_bvLtExpr(vc, shift, bvConst32(width, width)),
+                   res,
+                   bvZero(width));
   return res;
 }
 
@@ -839,12 +841,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, getShiftBits(*width_out));
     } 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 48bddeed..eaa41d5c 100644
--- a/lib/Solver/STPBuilder.h
+++ b/lib/Solver/STPBuilder.h
@@ -104,7 +104,7 @@ private:
   ExprHandle bvRightShift(ExprHandle expr, unsigned shift);
   ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle shift);
   ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle shift);
-  ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle amount, unsigned width);
+  ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle shift);
 
   ExprHandle constructAShrByConstant(ExprHandle expr, unsigned shift, 
                                      ExprHandle isSigned, unsigned shiftBits);
diff --git a/test/Feature/logical-right-overshift-sym-conc.c b/test/Feature/logical-right-overshift-sym-conc.c
index 47e0959c..00281ec4 100644
--- a/test/Feature/logical-right-overshift-sym-conc.c
+++ b/test/Feature/logical-right-overshift-sym-conc.c
@@ -1,7 +1,7 @@
 // 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" klee-last/messages.txt
-// RUN: grep "KLEE: done: explored paths = 1" klee-last/info
+// 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>
 
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] )
-- 
cgit 1.4.1


From b6e9a1f1d3d1d1ddd9b5843c47b372352d259a16 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 7 Nov 2013 15:50:30 +0000
Subject: Fixed overshift of arithmetic right shift by constant so that it
 overshifts to zero. Test case is included.

---
 lib/Solver/STPBuilder.cpp                       | 15 ++++++---------
 lib/Solver/STPBuilder.h                         |  2 +-
 test/Solver/overshift-aright-by-constant.kquery | 14 ++++++++++++++
 3 files changed, 21 insertions(+), 10 deletions(-)
 create mode 100644 test/Solver/overshift-aright-by-constant.kquery

diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 84e88579..9e3a9862 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -255,7 +255,7 @@ ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) {
   ExprHandle signedBool = bvBoolExtract(expr, width-1);
 
   //start with the result if shifting by width-1
-  ExprHandle res = constructAShrByConstant(expr, width-1, signedBool, width);
+  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?
@@ -265,8 +265,7 @@ ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) {
                      eqExpr(shift, bvConst32(width,i)),
                      constructAShrByConstant(expr, 
                                              i, 
-                                             signedBool, 
-                                             width),
+                                             signedBool),
                      res);
   }
 
@@ -279,16 +278,14 @@ ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) {
 }
 
 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,
@@ -841,7 +838,7 @@ 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);
diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h
index eaa41d5c..42ca9eaf 100644
--- a/lib/Solver/STPBuilder.h
+++ b/lib/Solver/STPBuilder.h
@@ -107,7 +107,7 @@ private:
   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/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] )
-- 
cgit 1.4.1


From 8083ab1821790bf9d865e3a19e88987e50d152b5 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 7 Nov 2013 15:53:35 +0000
Subject: Added C test case that checks that concrete and symbolic overshift
 behaviour for arithmetic right shift are identical.

---
 test/Feature/arithmetic-right-overshift-sym-conc.c | 65 ++++++++++++++++++++++
 1 file changed, 65 insertions(+)
 create mode 100644 test/Feature/arithmetic-right-overshift-sym-conc.c

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;
+}
-- 
cgit 1.4.1


From e70cd5b0764fe50f1e081a7d3e8e81fd623aa090 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 7 Nov 2013 16:11:02 +0000
Subject: Remove STPBuilder::getShiftBits() which is no longer used.

---
 lib/Solver/STPBuilder.h | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h
index 42ca9eaf..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);
-- 
cgit 1.4.1


From 6e4e74b99a199ead458b0b919286d667bd8e8f28 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 14 Feb 2014 18:45:21 +0000
Subject: Explicitly get the width of the "shift" expression rather than
 assuming that is the samw width of the "expr" expression.

It probably is the same width (it defintely is in SMT-LIB but I'm not
sure about STP) but it is probably better to be explicit.
---
 lib/Solver/STPBuilder.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 9e3a9862..ad0df3c2 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -220,7 +220,7 @@ ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle shift) {
 
   // If overshifting, shift to zero
   res = vc_iteExpr(vc,
-                   vc_bvLtExpr(vc, shift, bvConst32(width, width)),
+                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
                    res,
                    bvZero(width));
   return res;
@@ -241,7 +241,7 @@ ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle shift) {
 
   // If overshifting, shift to zero
   res = vc_iteExpr(vc,
-                   vc_bvLtExpr(vc, shift, bvConst32(width, width)),
+                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
                    res,
                    bvZero(width));
   return res;
@@ -271,7 +271,7 @@ ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) {
 
   // If overshifting, shift to zero
   res = vc_iteExpr(vc,
-                   vc_bvLtExpr(vc, shift, bvConst32(width, width)),
+                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
                    res,
                    bvZero(width));
   return res;
-- 
cgit 1.4.1