Extract some methods from ci lazy methods

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -98,34 +98,8 @@ bool ci_lazy_methodst::operator()(
   method_bytecodet &method_bytecode,
   const method_convertert &method_converter)
 {
-  std::unordered_set<irep_idt> methods_to_convert_later;
-
-  main_function_resultt main_function =
-    get_main_symbol(symbol_table, main_class, get_message_handler());
-  if(!main_function.is_success())
-  {
-    // Failed, mark all functions in the given main class(es)
-    // reachable.
-    std::vector<irep_idt> reachable_classes;
-    if(!main_class.empty())
-      reachable_classes.push_back(main_class);
-    else
-      reachable_classes = main_jar_classes;
-    for(const irep_idt &class_name : reachable_classes)
-    {
-      const auto &methods =
-        java_class_loader.get_original_class(class_name).parsed_class.methods;
-      for(const auto &method : methods)
-      {
-        const irep_idt methodid =
-          "java::" + id2string(class_name) + "." + id2string(method.name)
-            + ":" + id2string(method.descriptor);
-        methods_to_convert_later.insert(methodid);
-      }
-    }
-  }
-  else
-    methods_to_convert_later.insert(main_function.main_function.name);
+  std::unordered_set<irep_idt> methods_to_convert_later =
+    entry_point_methods(symbol_table);
 
   // Add any extra entry points specified; we should elaborate these in the
   // same way as the main function.
@@ -152,46 +126,30 @@ bool ci_lazy_methodst::operator()(
 
   bool any_new_classes = true;
   while(any_new_classes)
-  {bool any_new_methods = true;
-  while(any_new_methods)
   {
-    any_new_methods=false;
-    while(!methods_to_convert_later.empty())
+    bool any_new_methods = true;
+    while(any_new_methods)
     {
-      std::unordered_set<irep_idt> methods_to_convert;
-      std::swap(methods_to_convert, methods_to_convert_later);
-      for(const auto &mname : methods_to_convert)
+      any_new_methods = false;
+      while(!methods_to_convert_later.empty())
       {
-        if(!methods_already_populated.insert(mname).second)
-          continue;
-        debug() << "CI lazy methods: elaborate " << mname << eom;
-        if(
-          method_converter(
-            mname,
-            // Note this wraps *references* to methods_to_convert_later &
-            // instantiated_classes
-            ci_lazy_methods_neededt(
-              methods_to_convert_later, instantiated_classes, symbol_table)))
-        {
-          // Couldn't convert this function
-          continue;
-        }
-        const exprt &method_body = symbol_table.lookup_ref(mname).value;
-
-        gather_virtual_callsites(method_body, virtual_function_calls);
-
-        if(!class_initializer_seen && references_class_model(method_body))
+        std::unordered_set<irep_idt> methods_to_convert;
+        std::swap(methods_to_convert, methods_to_convert_later);
+        for(const auto &mname : methods_to_convert)
         {
-          class_initializer_seen = true;
-          irep_idt initializer_signature =
-            get_java_class_literal_initializer_signature();
-          if(symbol_table.has_symbol(initializer_signature))
-            methods_to_convert_later.insert(initializer_signature);
+          const auto conversion_result = convert_and_analyze_method(
+            method_converter,
+            methods_already_populated,
+            class_initializer_seen,
+            mname,
+            symbol_table,
+            methods_to_convert_later,
+            instantiated_classes,
+            virtual_function_calls);
+          any_new_methods |= conversion_result.new_method_seen;
+          class_initializer_seen |= conversion_result.class_initializer_seen;
         }
-
-        any_new_methods=true;
       }
-    }
 
       // Given the object types we now know may be created, populate more
       // possible virtual function call targets:
@@ -209,43 +167,11 @@ bool ci_lazy_methodst::operator()(
       }
     }
 
-    any_new_classes = false;
-
-    // Look for virtual callsites with no candidate targets. If we have
-    // invokevirtual A.f and we don't believe either A or any of its children
-    // may exist, we assume specifically A is somehow instantiated. Note this
-    // may result in an abstract class being classified as instantiated, which
-    // stands in for some unknown concrete subclass: in this case the called
-    // method will be a stub.
-    for(const exprt &virtual_function_call : virtual_function_calls)
-    {
-      std::unordered_set<irep_idt> candidate_target_methods;
-      get_virtual_method_targets(
-        virtual_function_call,
-        instantiated_classes,
-        candidate_target_methods,
-        symbol_table);
-
-      if(!candidate_target_methods.empty())
-        continue;
-
-      // Add the call class to instantiated_classes and assert that it
-      // didn't already exist
-      const irep_idt &call_class = virtual_function_call.get(ID_C_class);
-      auto ret_class = instantiated_classes.insert(call_class);
-      CHECK_RETURN(ret_class.second);
-      any_new_classes = true;
-
-      // Check that `get_virtual_method_target` returns a method now
-      const irep_idt &call_basename =
-        virtual_function_call.get(ID_component_name);
-      const irep_idt method_name = get_virtual_method_target(
-        instantiated_classes, call_basename, call_class, symbol_table);
-      CHECK_RETURN(!method_name.empty());
-
-      // Add what it returns to methods_to_convert_later
-      methods_to_convert_later.insert(method_name);
-    }
+    any_new_classes = handle_virtual_methods_with_no_callees(
+      methods_to_convert_later,
+      instantiated_classes,
+      virtual_function_calls,
+      symbol_table);
   }
 
   // cproverNondetInitialize has to be force-loaded for mocks to return valid
@@ -297,6 +223,143 @@ bool ci_lazy_methodst::operator()(
   return false;
 }
 
+/// Look for virtual callsites with no candidate targets. If we have
+/// invokevirtual A.f and we don't believe either A or any of its children
+/// may exist, we assume specifically A is somehow instantiated. Note this
+/// may result in an abstract class being classified as instantiated, which
+/// stands in for some unknown concrete subclass: in this case the called
+/// method will be a stub.
+/// \return whether a new class was encountered
+bool ci_lazy_methodst::handle_virtual_methods_with_no_callees(
+  std::unordered_set<irep_idt> &methods_to_convert_later,
+  std::unordered_set<irep_idt> &instantiated_classes,
+  const std::unordered_set<exprt, irep_hash> &virtual_function_calls,
+  symbol_tablet &symbol_table)
+{
+  bool any_new_classes = false;
+  for(const exprt &virtual_function_call : virtual_function_calls)
+  {
+    std::unordered_set<irep_idt> candidate_target_methods;
+    get_virtual_method_targets(
+      virtual_function_call,
+      instantiated_classes,
+      candidate_target_methods,
+      symbol_table);
+
+    if(!candidate_target_methods.empty())
+      continue;
+
+    // Add the call class to instantiated_classes and assert that it
+    // didn't already exist
+    const irep_idt &call_class = virtual_function_call.get(ID_C_class);
+    auto ret_class = instantiated_classes.insert(call_class);
+    CHECK_RETURN(ret_class.second);
+    any_new_classes = true;
+
+    // Check that `get_virtual_method_target` returns a method now
+    const irep_idt &call_basename =
+      virtual_function_call.get(ID_component_name);
+    const irep_idt method_name = get_virtual_method_target(
+      instantiated_classes, call_basename, call_class, symbol_table);
+    CHECK_RETURN(!method_name.empty());
+
+    // Add what it returns to methods_to_convert_later
+    methods_to_convert_later.insert(method_name);
+  }
+  return any_new_classes;
+}
+
+/// Convert a method, add it to the populated set, add needed methods to
+/// methods_to_convert_later and add virtual calls from the method to
+/// virtual_function_calls
+/// \return structure containing two Booleans:
+///     * class_initializer_seen which is true if the class_initializer_seen
+///       argument was false and the class_model is referenced in
+///       the body of the method
+///     * new_method_seen if the method was not converted before and was
+///       converted successfully here
+ci_lazy_methodst::convert_method_resultt
+ci_lazy_methodst::convert_and_analyze_method(
+  const method_convertert &method_converter,
+  std::unordered_set<irep_idt> &methods_already_populated,
+  const bool class_initializer_already_seen,
+  const irep_idt &method_name,
+  symbol_tablet &symbol_table,
+  std::unordered_set<irep_idt> &methods_to_convert_later,
+  std::unordered_set<irep_idt> &instantiated_classes,
+  std::unordered_set<exprt, irep_hash> &virtual_function_calls)
+{
+  convert_method_resultt result;
+  if(!methods_already_populated.insert(method_name).second)
+    return result;
+
+  debug() << "CI lazy methods: elaborate " << method_name << eom;
+
+  // Note this wraps *references* to methods_to_convert_later &
+  // instantiated_classes
+  ci_lazy_methods_neededt needed_methods(
+    methods_to_convert_later, instantiated_classes, symbol_table);
+
+  const bool could_not_convert_function =
+    method_converter(method_name, needed_methods);
+  if(could_not_convert_function)
+    return result;
+
+  const exprt &method_body = symbol_table.lookup_ref(method_name).value;
+  gather_virtual_callsites(method_body, virtual_function_calls);
+
+  if(!class_initializer_already_seen && references_class_model(method_body))
+  {
+    result.class_initializer_seen = true;
+    const irep_idt initializer_signature =
+      get_java_class_literal_initializer_signature();
+    if(symbol_table.has_symbol(initializer_signature))
+      methods_to_convert_later.insert(initializer_signature);
+  }
+  result.new_method_seen = true;
+  return result;
+}
+
+/// Entry point methods are either:
+///   * the "main" function of the `main_class` if it exists
+///   * all the methods of the main class if it is not empty
+///   * all the methods of the main jar file
+/// \return set of identifiers of entry point methods
+std::unordered_set<irep_idt>
+ci_lazy_methodst::entry_point_methods(const symbol_tablet &symbol_table)
+{
+  std::unordered_set<irep_idt> methods_to_convert_later;
+
+  const main_function_resultt main_function = get_main_symbol(
+    symbol_table, this->main_class, this->get_message_handler());
+  if(!main_function.is_success())
+  {
+    // Failed, mark all functions in the given main class(es)
+    // reachable.
+    std::vector<irep_idt> reachable_classes;
+    if(!this->main_class.empty())
+      reachable_classes.push_back(this->main_class);
+    else
+      reachable_classes = this->main_jar_classes;
+    for(const irep_idt &class_name : reachable_classes)
+    {
+      const auto &methods =
+        this->java_class_loader.get_original_class(class_name)
+          .parsed_class.methods;
+      for(const auto &method : methods)
+      {
+        const irep_idt methodid = "java::" + id2string(class_name) + "." +
+                                  id2string(method.name) + ":" +
+                                  id2string(method.descriptor);
+        methods_to_convert_later.insert(methodid);
+      }
+    }
+  }
+  else
+    methods_to_convert_later.insert(main_function.main_function.name);
+  return methods_to_convert_later;
+}
+
 /// Translates the given list of method names from human-readable to
 /// internal syntax.
 /// Expands any wildcards (entries ending in '.*') in the given method

jbmc/src/java_bytecode/ci_lazy_methods.h

@@ -169,6 +169,31 @@ class ci_lazy_methodst:public messaget
   const std::vector<irep_idt> &extra_instantiated_classes;
   const select_pointer_typet &pointer_type_selector;
   const synthetic_methods_mapt &synthetic_methods;
+
+  std::unordered_set<irep_idt>
+  entry_point_methods(const symbol_tablet &symbol_table);
+
+  struct convert_method_resultt
+  {
+    bool class_initializer_seen = false;
+    bool new_method_seen = false;
+  };
+
+  convert_method_resultt convert_and_analyze_method(
+    const method_convertert &method_converter,
+    std::unordered_set<irep_idt> &methods_already_populated,
+    const bool class_initializer_already_seen,
+    const irep_idt &method_name,
+    symbol_tablet &symbol_table,
+    std::unordered_set<irep_idt> &methods_to_convert_later,
+    std::unordered_set<irep_idt> &instantiated_classes,
+    std::unordered_set<exprt, irep_hash> &virtual_function_calls);
+
+  bool handle_virtual_methods_with_no_callees(
+    std::unordered_set<irep_idt> &methods_to_convert_later,
+    std::unordered_set<irep_idt> &instantiated_classes,
+    const std::unordered_set<exprt, irep_hash> &virtual_function_calls,
+    symbol_tablet &symbol_table);
 };
 
 #endif // CPROVER_JAVA_BYTECODE_GATHER_METHODS_LAZILY_H