Merge pull request #3014 from svorenova/mock-vararg-tg5038

Parse ACC_VARARGS method flag from bytecode [TG-5038]

Author: antlechner

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -373,6 +373,7 @@ void java_bytecode_convert_method_lazy(
   if(m.is_static)
     member_type.set(ID_is_static, true);
   member_type.set_native(m.is_native);
+  member_type.set_is_varargs(m.is_varargs);
 
   if(m.is_bridge)
     member_type.set(ID_is_bridge_method, m.is_bridge);

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -86,7 +86,7 @@ struct java_bytecode_parse_treet
   struct methodt : public membert
   {
     irep_idt base_name;
-    bool is_native, is_abstract, is_synchronized, is_bridge;
+    bool is_native, is_abstract, is_synchronized, is_bridge, is_varargs;
     source_locationt source_location;
 
     typedef std::vector<instructiont> instructionst;

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -452,7 +452,6 @@ bool java_bytecode_parsert::parse()
 #define ACC_FINAL        0x0010
 #define ACC_SYNCHRONIZED 0x0020
 #define ACC_BRIDGE       0x0040
-#define ACC_VARARGS      0x0080
 #define ACC_NATIVE       0x0100
 #define ACC_INTERFACE    0x0200
 #define ACC_ABSTRACT     0x0400
@@ -1777,6 +1776,7 @@ void java_bytecode_parsert::rmethods(classt &parsed_class)
 #define ACC_PROTECTED  0x0004
 #define ACC_STATIC     0x0008
 #define ACC_FINAL      0x0010
+#define ACC_VARARGS    0x0080
 #define ACC_SUPER      0x0020
 #define ACC_VOLATILE   0x0040
 #define ACC_TRANSIENT  0x0080
@@ -1803,6 +1803,7 @@ void java_bytecode_parsert::rmethod(classt &parsed_class)
   method.is_synchronized=(access_flags&ACC_SYNCHRONIZED)!=0;
   method.is_native=(access_flags&ACC_NATIVE)!=0;
   method.is_bridge = (access_flags & ACC_BRIDGE) != 0;
+  method.is_varargs = (access_flags & ACC_VARARGS) != 0;
   method.name=pool_entry(name_index).s;
   method.base_name=pool_entry(name_index).s;
   method.descriptor=id2string(pool_entry(descriptor_index).s);

jbmc/src/java_bytecode/java_types.h

@@ -298,6 +298,16 @@ class java_method_typet : public code_typet
   {
     set(ID_is_native_method, is_native);
   }
+
+  bool get_is_varargs() const
+  {
+    return get_bool(ID_is_varargs_method);
+  }
+
+  void set_is_varargs(bool is_varargs)
+  {
+    set(ID_is_varargs_method, is_varargs);
+  }
 };
 
 template <>

jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithVarArgsMethod.class

@@ -0,0 +1,8 @@
+public class ClassWithVarArgsMethod {
+  public int varArgsFunc(int... args) {
+    return 0;
+  }
+  public int nonVarArgsFunc(int[] args) {
+    return 0;
+  }
+}

jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithVarArgsMethod.java

@@ -141,3 +141,37 @@ SCENARIO(
     }
   }
 }
+
+SCENARIO(
+  "java_bytecode_convert_varargs_method",
+  "[core][java_bytecode][java_bytecode_convert_method]")
+{
+  GIVEN("A class with varargs and non-varargs methods")
+  {
+    const symbol_tablet symbol_table = load_java_class(
+      "ClassWithVarArgsMethod", "./java_bytecode/java_bytecode_convert_method");
+
+    WHEN("When parsing a method with a variable number of arguments")
+    {
+      const symbolt method_symbol = symbol_table.lookup_ref(
+        "java::ClassWithVarArgsMethod.varArgsFunc:([I)I");
+      const java_method_typet &method_type =
+        require_type::require_java_method(method_symbol.type);
+      THEN("The method should be marked as varargs")
+      {
+        REQUIRE(method_type.get_is_varargs());
+      }
+    }
+    WHEN("When parsing a method with constant number of arguments")
+    {
+      const symbolt method_symbol = symbol_table.lookup_ref(
+        "java::ClassWithVarArgsMethod.nonVarArgsFunc:([I)I");
+      const java_method_typet &method_type =
+        require_type::require_java_method(method_symbol.type);
+      THEN("The method should not be marked as varargs")
+      {
+        REQUIRE_FALSE(method_type.get_is_varargs());
+      }
+    }
+  }
+}

jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp

@@ -387,6 +387,7 @@ IREP_ID_ONE(is_inline)
 IREP_ID_ONE(is_extern)
 IREP_ID_ONE(is_synchronized)
 IREP_ID_ONE(is_native_method)
+IREP_ID_ONE(is_varargs_method)
 IREP_ID_ONE(is_global)
 IREP_ID_ONE(is_thread_local)
 IREP_ID_ONE(is_parameter)