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 +-
 2 files changed, 7 insertions(+), 10 deletions(-)

(limited to 'lib/Solver')

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