Fix JBMC left shift operator

According to JLS 15.19 Shift Operators,
a bit mask is applied to the second operand
depending on the size of the first.

Author: peterschrammel

jbmc/regression/jbmc/shift1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 shift1.foo
 
 ^EXIT=0$

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -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_class.h

@@ -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,