java-unwind-enum-static: also unwind clone loop in Enum.values()

If an enumeration type's values() method clones an array, we assume it is cloning the array of
enumeration values and therefore is bounded by the enumeration's size, similar to the existing
handling of enumeration static initializers.

Author: smowton

jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp

@@ -14,11 +14,46 @@ Author: Chris Smowton, [email protected]
 #include <util/invariant.h>
 #include <util/suffix.h>
 
+/// Check if we may be in a function that loops over the cases of an
+/// enumeration (note we return a candidate function that matches a pattern;
+/// our caller must verify it really belongs to an enumeration).
+/// At the moment we know of two cases that definitely do so:
+/// * An enumeration type's static initialiser
+/// * The array[reference].clone() method when called from an enumeration type's
+///   'values()'  method
+/// \param context: the current call stack
+/// \return the name of an enclosing function that may be defined on the
+///   relevant enum type, or an empty string if we don't find one.
+static irep_idt
+find_enum_function_on_stack(const goto_symex_statet::call_stackt &context)
+{
+  static irep_idt reference_array_clone_id =
+    "java::array[reference].clone:()Ljava/lang/Object;";
+
+  PRECONDITION(!context.empty());
+  const irep_idt &current_function = context.back().function_identifier;
+
+  if(context.size() >= 2 && current_function == reference_array_clone_id)
+  {
+    const irep_idt &clone_caller =
+      context.at(context.size() - 2).function_identifier;
+    if(id2string(clone_caller).find(".values:()[L") != std::string::npos)
+      return clone_caller;
+    else
+      return irep_idt();
+  }
+  else if(has_suffix(id2string(current_function), ".<clinit>:()V"))
+    return current_function;
+  else
+    return irep_idt();
+}
+
 /// Unwind handler that special-cases the clinit (static initializer) functions
-/// of enumeration classes. When java_bytecode_convert_classt has annotated them
+/// of enumeration classes, and VALUES array cloning in their values() methods.
+/// When java_bytecode_convert_classt has annotated them
 /// with a size of the enumeration type, this forces unwinding of any loop in
 /// the static initializer to at least that many iterations, with intent to
-/// permit population of the enumeration's value array.
+/// permit population / copying of the enumeration's value array.
 /// \param function_id: function the loop is in
 /// \param loop_number: ordinal number of the loop (ignored)
 /// \param unwind_count: iteration count that is about to begin
@@ -29,17 +64,17 @@ Author: Chris Smowton, [email protected]
 ///   unwind_count is <= the enumeration size, or unknown (defer / no decision)
 ///   otherwise.
 tvt java_enum_static_init_unwind_handler(
-  const irep_idt &function_id,
+  const goto_symex_statet::call_stackt &context,
   unsigned loop_number,
   unsigned unwind_count,
   unsigned &unwind_max,
   const symbol_tablet &symbol_table)
 {
-  const std::string &function_str = id2string(function_id);
-  if(!has_suffix(function_str, ".<clinit>:()V"))
+  const irep_idt enum_function_id = find_enum_function_on_stack(context);
+  if(enum_function_id.empty())
     return tvt::unknown();
 
-  const symbolt &function_symbol = symbol_table.lookup_ref(function_str);
+  const symbolt &function_symbol = symbol_table.lookup_ref(enum_function_id);
   irep_idt class_id = function_symbol.type.get(ID_C_class);
   INVARIANT(
     !class_id.empty(), "functions should have their defining class annotated");

jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.h

@@ -12,11 +12,13 @@ Author: Chris Smowton, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_ENUM_STATIC_INIT_UNWIND_HANDLER_H
 #define CPROVER_JAVA_BYTECODE_JAVA_ENUM_STATIC_INIT_UNWIND_HANDLER_H
 
+#include <goto-symex/goto_symex_state.h>
+
 #include <util/symbol_table.h>
 #include <util/threeval.h>
 
 tvt java_enum_static_init_unwind_handler(
-  const irep_idt &function_id,
+  const goto_symex_statet::call_stackt &context,
   unsigned loop_number,
   unsigned unwind_count,
   unsigned &unwind_max,

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -485,11 +485,7 @@ int jbmc_parse_optionst::doit()
           unsigned unwind,
           unsigned &max_unwind) {
           return java_enum_static_init_unwind_handler(
-            context,
-            loop_number,
-            unwind,
-            max_unwind,
-            symbol_table);
+            context, loop_number, unwind, max_unwind, symbol_table);
         });
     };
   }

src/cbmc/symex_bmc.cpp

@@ -117,11 +117,7 @@ bool symex_bmct::get_unwind(
   for(auto handler : loop_unwind_handlers)
   {
     abort_unwind_decision =
-      handler(
-        context,
-        source.pc->loop_number,
-        unwind,
-        this_loop_limit);
+      handler(context, source.pc->loop_number, unwind, this_loop_limit);
     if(abort_unwind_decision.is_known())
       break;
   }