Merge pull request #3701 from tautschnig/fix-lshr-simplification

Fix simplification of logical right shift of signed bitvectors

Author: kroening

jbmc/regression/jbmc/shift1/shift1.class

@@ -0,0 +1,11 @@
+class shift1
+{
+  public static void main(String[] args)
+  {
+    assert (5 << 1) == 10;
+    assert (5 >> 1) == 2;
+    assert (-4 >> 1) == -2;
+    assert (-4 >>> 1) == 2147483646;
+  }
+}
+

jbmc/regression/jbmc/shift1/shift1.java

@@ -0,0 +1,8 @@
+CORE
+shift1.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

jbmc/regression/jbmc/shift1/test.desc

@@ -1008,6 +1008,8 @@ bool simplify_exprt::simplify_shifts(exprt &expr)
       }
       else if(distance>=0)
       {
+        if(value < 0)
+          value += power(2, width);
         value/=power(2, distance);
         expr=from_integer(value, expr.type());
         return false;

src/util/simplify_expr_int.cpp

@@ -155,3 +155,29 @@ TEST_CASE("Simplify extractbits")
   REQUIRE(!unmodified);
   REQUIRE(eb == from_integer(0xbe, unsignedbv_typet(8)));
 }
+
+TEST_CASE("Simplify shift")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns(symbol_table);
+
+  REQUIRE(
+    simplify_expr(shl_exprt(from_integer(5, signedbv_typet(8)), 1), ns) ==
+    from_integer(10, signedbv_typet(8)));
+
+  REQUIRE(
+    simplify_expr(ashr_exprt(from_integer(5, signedbv_typet(8)), 1), ns) ==
+    from_integer(2, signedbv_typet(8)));
+
+  REQUIRE(
+    simplify_expr(lshr_exprt(from_integer(5, unsignedbv_typet(8)), 1), ns) ==
+    from_integer(2, unsignedbv_typet(8)));
+
+  REQUIRE(
+    simplify_expr(ashr_exprt(from_integer(-4, signedbv_typet(8)), 1), ns) ==
+    from_integer(-2, signedbv_typet(8)));
+
+  REQUIRE(
+    simplify_expr(lshr_exprt(from_integer(-4, signedbv_typet(8)), 1), ns) ==
+    from_integer(126, signedbv_typet(8)));
+}