Replace calls to array.clone in values for Enum

For Enum classes this replaces calls to clone via a specialized clone method
call that allows for explicit unwind bounds depending on the number of enum
elements.

Author: Matthias Güdemann

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2106,6 +2106,21 @@ void java_bytecode_convert_methodt::convert_invoke(
   code_typet &code_type = to_code_type(arg0.type());
   code_typet::parameterst &parameters(code_type.parameters());
 
+  const std::string full_method_name = id2string(method_id);
+  const size_t method_separator = id2string(method_id).rfind(':');
+  const std::string method_name = full_method_name.substr(0, method_separator);
+
+  const size_t class_separator = method_name.rfind('.');
+  const std::string calling_class_name = method_name.substr(0, class_separator);
+
+  std::string class_type_name = calling_class_name.substr(6);
+  std::replace(class_type_name.begin(), class_type_name.end(), '.', '/');
+  const auto &enum_clone_symbol = symbol_table.lookup_ref(calling_class_name);
+  const bool is_enum_values_clone_call =
+    enum_clone_symbol.type.get_bool(ID_enumeration) &&
+    (full_method_name ==
+     (calling_class_name + ".values:()[L" + class_type_name + ";"));
+
   if(use_this)
   {
     if(parameters.empty() || !parameters[0].get_this())
@@ -2197,7 +2212,7 @@ void java_bytecode_convert_methodt::convert_invoke(
   //   generate code that may wrongly assume that such a method is
   //   accessible if we assume that its access attribute is "more
   //   accessible" than it actually is.
-  irep_idt id = arg0.get(ID_identifier);
+  const irep_idt id = arg0.get(ID_identifier);
   if(
     symbol_table.symbols.find(id) == symbol_table.symbols.end() &&
     !(is_virtual &&
@@ -2220,7 +2235,13 @@ void java_bytecode_convert_methodt::convert_invoke(
     symbol_table.add(symbol);
   }
 
-  if(is_virtual)
+  if(is_enum_values_clone_call)
+  {
+    const std::string clone_name =
+      "java::array[" + calling_class_name + "].clone:()Ljava/lang/Object;";
+    call.function() = symbol_exprt(clone_name, arg0.type());
+  }
+  else if(is_virtual)
   {
     // dynamic binding
     assert(use_this);