[fix, bitwuzla] Replaced implementations for shifts.

S1eGa · Nov 20, 2023 · 5f702ee · 5f702ee
1 parent e498c61
commit 5f702ee
Showing 1 changed file with 48 additions and 9 deletions.
diff --git a/lib/Solver/BitwuzlaBuilder.cpp b/lib/Solver/BitwuzlaBuilder.cpp
@@ -185,7 +185,21 @@ Term BitwuzlaBuilder::bvLeftShift(Term expr, unsigned shift) {
 Term BitwuzlaBuilder::bvVarLeftShift(Term expr, Term shift) {
   Term exprAsBv = castToBitVector(expr);
   Term shiftAsBv = castToBitVector(shift);
-  return mk_term(Kind::BV_SHL, {exprAsBv, shiftAsBv});
+
+  unsigned width = getBVLength(exprAsBv);
+  Term res = bvZero(width);
+
+  // construct a big if-then-elif-elif-... with one case per possible shift
+  // amount
+  for (int i = width - 1; i >= 0; i--) {
+    res = iteExpr(eqExpr(shiftAsBv, bvConst32(width, i)),
+                  bvLeftShift(exprAsBv, i), res);
+  }
+
+  // If overshifting, shift to zero
+  Term ex = bvLtExpr(shiftAsBv, bvConst32(getBVLength(shiftAsBv), width));
+  res = iteExpr(ex, res, bvZero(width));
+  return res;
 }
 
 // logical right shift by a variable amount on an expression of the specified
@@ -194,11 +208,20 @@ Term BitwuzlaBuilder::bvVarRightShift(Term expr, Term shift) {
   Term exprAsBv = castToBitVector(expr);
   Term shiftAsBv = castToBitVector(shift);
 
-  Term overshiftCond = bvLeExpr(
-      shiftAsBv, bvConst64(getBVLength(shiftAsBv), getBVLength(exprAsBv)));
+  unsigned width = getBVLength(exprAsBv);
+  Term res = bvZero(width);
 
-  return iteExpr(overshiftCond, mk_term(Kind::BV_SHR, {exprAsBv, shiftAsBv}),
-                 bvZero(getBVLength(exprAsBv)));
+  // construct a big if-then-elif-elif-... with one case per possible shift
+  // amount
+  for (int i = width - 1; i >= 0; i--) {
+    res = iteExpr(eqExpr(shiftAsBv, bvConst32(width, i)),
+                  bvRightShift(exprAsBv, i), res);
+  }
+
+  // If overshifting, shift to zero
+  Term ex = bvLtExpr(shiftAsBv, bvConst32(getBVLength(shiftAsBv), width));
+  res = iteExpr(ex, res, bvZero(width));
+  return res;
 }
 
 // arithmetic right shift by a variable amount on an expression of the specified
@@ -207,11 +230,27 @@ Term BitwuzlaBuilder::bvVarArithRightShift(Term expr, Term shift) {
   Term exprAsBv = castToBitVector(expr);
   Term shiftAsBv = castToBitVector(shift);
 
-  Term overshiftCond = bvLeExpr(
-      shiftAsBv, bvConst64(getBVLength(shiftAsBv), getBVLength(exprAsBv)));
+  unsigned width = getBVLength(exprAsBv);
+
+  // get the sign bit to fill with
+  Term signedBool = bvBoolExtract(exprAsBv, width - 1);
+
+  // start with the result if shifting by width-1
+  Term res = constructAShrByConstant(exprAsBv, 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 = iteExpr(eqExpr(shiftAsBv, bvConst32(width, i)),
+                  constructAShrByConstant(exprAsBv, i, signedBool), res);
+  }
 
-  return iteExpr(overshiftCond, mk_term(Kind::BV_ASHR, {exprAsBv, shiftAsBv}),
-                 bvZero(getBVLength(exprAsBv)));
+  // If overshifting, shift to zero
+  Term ex = bvLtExpr(shiftAsBv, bvConst32(getBVLength(shiftAsBv), width));
+  res = iteExpr(ex, res, bvZero(width));
+  return res;
 }
 
 Term BitwuzlaBuilder::notExpr(Term expr) { return mk_term(Kind::NOT, {expr}); }