Merge pull request #5590 from peterschrammel/fix-jbmc-shl

Fix shl operator in JBMC

Author: peterschrammel

jbmc/regression/jbmc/shift1/shift1.class

@@ -1,11 +1,45 @@
 class shift1
 {
-  public static void main(String[] args)
+  public static void foo(int c, long x)
   {
-    assert (5 << 1) == 10;
-    assert (5 >> 1) == 2;
-    assert (-4 >> 1) == -2;
-    assert (-4 >>> 1) == 2147483646;
+    switch (c)
+    {
+    case 0:
+      if (x == 5L) assert ((int)x << 1) == 10;
+      break;
+    case 1:
+      if (x == 5L) assert ((int)x >> 1) == 2;
+      break;
+    case 2:
+      if (x == -4L) assert ((int)x >> 1) == -2;
+      break;
+    case 3:
+      if (x == -4L) assert ((int)x >>> 1) == 2147483646;
+      break;
+    case 4:
+      if (x == 1L) assert ((int)x << 0) == 1;
+      break;
+    case 5:
+      if (x == 1L) assert ((int)x << 31) == -2147483648;
+      break;
+    case 6:
+      if (x == 1L) assert ((int)x << 32) == 1;
+      break;
+    case 7:
+      if (x == 1L) assert ((int)x << 33) == 2;
+      break;
+    case 8:
+      if (x == 1L) assert (x << 0) == 1L;
+      break;
+    case 9:
+      if (x == 1L) assert (x << 63) == -9223372036854775808L;
+      break;
+    case 10:
+      if (x == 1L) assert (x << 64) == 1L;
+      break;
+    default:
+      if (x == 1L) assert (x << 65) == 2L;
+      break;
+    }
   }
 }
-

jbmc/regression/jbmc/shift1/shift1.java

@@ -1,5 +1,5 @@
 CORE
-shift1
+shift1.foo
 
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc/shift1/test.desc

@@ -1525,7 +1525,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
     else if(bytecode == patternt("?shl"))
     {
       PRECONDITION(op.size() == 2 && results.size() == 1);
-      results[0]=shl_exprt(op[0], op[1]);
+      results = convert_shl(statement, op, results);
     }
     else if(bytecode == patternt("?shr"))
     {
@@ -2749,6 +2749,23 @@ exprt::operandst &java_bytecode_convert_methodt::convert_cmp(
   return results;
 }
 
+exprt::operandst &java_bytecode_convert_methodt::convert_shl(
+  const irep_idt &statement,
+  const exprt::operandst &op,
+  exprt::operandst &results) const
+{
+  const typet type = java_type_from_char(statement[0]);
+
+  const std::size_t width = get_bytecode_type_width(type);
+
+  // According to JLS 15.19 Shift Operators
+  // a mask 0b11111 is applied for int and 0b111111 for long.
+  exprt mask = from_integer(width - 1, op[1].type());
+
+  results[0] = shl_exprt(op[0], bitand_exprt(op[1], mask));
+  return results;
+}
+
 exprt::operandst &java_bytecode_convert_methodt::convert_ushr(
   const irep_idt &statement,
   const exprt::operandst &op,

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -418,6 +418,11 @@ class java_bytecode_convert_methodt:public messaget
     const source_locationt &location,
     method_offsett address);
 
+  exprt::operandst &convert_shl(
+    const irep_idt &statement,
+    const exprt::operandst &op,
+    exprt::operandst &results) const;
+
   exprt::operandst &convert_ushr(
     const irep_idt &statement,
     const exprt::operandst &op,