[fix, bitwuzla] Model overshifts as 0.

S1eGa · Nov 20, 2023 · e498c61 · e498c61
1 parent eef8d8c
commit e498c61
Showing 1 changed file with 21 additions and 15 deletions.
diff --git a/lib/Solver/BitwuzlaBuilder.cpp b/lib/Solver/BitwuzlaBuilder.cpp
@@ -193,15 +193,25 @@ Term BitwuzlaBuilder::bvVarLeftShift(Term expr, Term shift) {
 Term BitwuzlaBuilder::bvVarRightShift(Term expr, Term shift) {
   Term exprAsBv = castToBitVector(expr);
   Term shiftAsBv = castToBitVector(shift);
-  return mk_term(Kind::BV_SHR, {exprAsBv, shiftAsBv});
+
+  Term overshiftCond = bvLeExpr(
+      shiftAsBv, bvConst64(getBVLength(shiftAsBv), getBVLength(exprAsBv)));
+
+  return iteExpr(overshiftCond, mk_term(Kind::BV_SHR, {exprAsBv, shiftAsBv}),
+                 bvZero(getBVLength(exprAsBv)));
 }
 
 // arithmetic right shift by a variable amount on an expression of the specified
 // width
 Term BitwuzlaBuilder::bvVarArithRightShift(Term expr, Term shift) {
   Term exprAsBv = castToBitVector(expr);
   Term shiftAsBv = castToBitVector(shift);
-  return mk_term(Kind::BV_ASHR, {exprAsBv, shiftAsBv});
+
+  Term overshiftCond = bvLeExpr(
+      shiftAsBv, bvConst64(getBVLength(shiftAsBv), getBVLength(exprAsBv)));
+
+  return iteExpr(overshiftCond, mk_term(Kind::BV_ASHR, {exprAsBv, shiftAsBv}),
+                 bvZero(getBVLength(exprAsBv)));
 }
 
 Term BitwuzlaBuilder::notExpr(Term expr) { return mk_term(Kind::NOT, {expr}); }
@@ -804,19 +814,15 @@ Term BitwuzlaBuilder::constructActual(ref<Expr> e, int *width_out) {
     Term left = castToBitVector(construct(ase->left, width_out));
     assert(*width_out != 1 && "uncanonicalized ashr");
 
-    int shiftWidth;
-    Term amount = construct(ase->right, &shiftWidth);
-    return bvVarArithRightShift(left, amount);
-
-    // if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) {
-    //   unsigned shift = (unsigned)CE->getLimitedValue();
-    //   Term signedBool = bvBoolExtract(left, *width_out - 1);
-    //   return constructAShrByConstant(left, shift, signedBool);
-    // } else {
-    //   int shiftWidth;
-    //   Term amount = construct(ase->right, &shiftWidth);
-    //   return bvVarArithRightShift(left, amount);
-    // }
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) {
+      unsigned shift = (unsigned)CE->getLimitedValue();
+      Term signedBool = bvBoolExtract(left, *width_out - 1);
+      return constructAShrByConstant(left, shift, signedBool);
+    } else {
+      int shiftWidth;
+      Term amount = construct(ase->right, &shiftWidth);
+      return bvVarArithRightShift(left, amount);
+    }
   }
 
     // Comparison