Generate INITIALIZE_FUNCTION from convert_single_method

This allows for an external lazy methods driver to control when the
`INITIALIZE_FUNCTION` is generated.

Author: thomasspriggs

jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp

@@ -12,10 +12,26 @@ Author: Daniel Kroening, [email protected]
 #include "java_types.h"
 #include "remove_exceptions.h"
 
+#include <linking/static_lifetime_init.h>
 #include <util/std_types.h>
 #include <util/cprover_prefix.h>
 #include <util/c_types.h>
 
+void create_java_initialize(symbol_table_baset &symbol_table)
+{
+  // If __CPROVER_initialize already exists, replace it. It may already exist
+  // if a GOTO binary provided it. This behaviour mirrors the ANSI-C frontend.
+  symbol_table.remove(INITIALIZE_FUNCTION);
+
+  symbolt initialize;
+  initialize.name=INITIALIZE_FUNCTION;
+  initialize.base_name=INITIALIZE_FUNCTION;
+  initialize.mode=ID_java;
+
+  initialize.type = java_method_typet({}, java_void_type());
+  symbol_table.add(initialize);
+}
+
 void java_internal_additions(symbol_table_baset &dest)
 {
   // add __CPROVER_rounding_mode
@@ -58,4 +74,6 @@ void java_internal_additions(symbol_table_baset &dest)
     symbol.is_static_lifetime = true;
     dest.add(symbol);
   }
+
+  create_java_initialize(dest);
 }

jbmc/src/java_bytecode/java_bytecode_internal_additions.h

@@ -12,6 +12,10 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/symbol_table_base.h>
 
+/// Adds `__cprover_initialize` to the \p symbol_table but does not generate
+/// code for it yet.
+void create_java_initialize(symbol_table_baset &symbol_table);
+
 void java_internal_additions(symbol_table_baset &dest);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INTERNAL_ADDITIONS_H

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -10,6 +10,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <string>
 
+#include <linking/static_lifetime_init.h>
+
 #include <util/cmdline.h>
 #include <util/config.h>
 #include <util/expr_iterator.h>
@@ -942,6 +944,8 @@ bool java_bytecode_languaget::typecheck(
       convert_single_method(
         method_sig.first, journalling_symbol_table, class_to_declared_symbols);
     }
+    convert_single_method(
+      INITIALIZE_FUNCTION, journalling_symbol_table, class_to_declared_symbols);
     // Now convert all newly added string methods
     for(const auto &fn_name : journalling_symbol_table.get_inserted())
     {
@@ -1095,6 +1099,7 @@ void java_bytecode_languaget::methods_provided(
   // Add all synthetic methods to map
   for(const auto &kv : synthetic_methods)
     methods.insert(kv.first);
+  methods.insert(INITIALIZE_FUNCTION);
 }
 
 /// \brief Promote a lazy-converted method (one whose type is known but whose
@@ -1120,7 +1125,7 @@ void java_bytecode_languaget::convert_lazy_method(
   convert_single_method(function_id, symbol_table, class_to_declared_symbols);
 
   // Instrument runtime exceptions (unless symbol is a stub)
-  if(symbol.value.is_not_nil())
+  if(symbol.value.is_not_nil() && function_id != INITIALIZE_FUNCTION)
   {
     java_bytecode_instrument_symbol(
       symbol_table,
@@ -1201,6 +1206,20 @@ bool java_bytecode_languaget::convert_single_method(
   // Nothing to do if body is already loaded
   if(symbol.value.is_not_nil())
     return false;
+
+  if(function_id == INITIALIZE_FUNCTION)
+  {
+    java_static_lifetime_init(
+      symbol_table,
+      symbol.location,
+      language_options->assume_inputs_non_null,
+      object_factory_parameters,
+      *pointer_type_selector,
+      language_options->string_refinement_enabled,
+      get_message_handler());
+    return false;
+  }
+
   INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
 
   bool ret = convert_single_method_code(

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -41,22 +41,6 @@ static codet record_exception(
   const symbolt &function,
   const symbol_table_baset &symbol_table);
 
-void create_java_initialize(symbol_table_baset &symbol_table)
-{
-  // If __CPROVER_initialize already exists, replace it. It may already exist
-  // if a GOTO binary provided it. This behaviour mirrors the ANSI-C frontend.
-  symbol_table.remove(INITIALIZE_FUNCTION);
-
-  symbolt initialize;
-  initialize.name=INITIALIZE_FUNCTION;
-  initialize.base_name=INITIALIZE_FUNCTION;
-  initialize.mode=ID_java;
-
-  initialize.type = java_method_typet({}, java_void_type());
-
-  symbol_table.add(initialize);
-}
-
 static bool should_init_symbol(const symbolt &sym)
 {
   if(sym.type.id()!=ID_code &&
@@ -104,7 +88,7 @@ static constant_exprt constant_bool(bool val)
   return from_integer(val ? 1 : 0, java_boolean_type());
 }
 
-static void java_static_lifetime_init(
+void java_static_lifetime_init(
   symbol_table_baset &symbol_table,
   const source_locationt &source_location,
   bool assume_init_pointers_not_null,
@@ -115,6 +99,7 @@ static void java_static_lifetime_init(
 {
   symbolt &initialize_symbol =
     symbol_table.get_writeable_ref(INITIALIZE_FUNCTION);
+  PRECONDITION(initialize_symbol.value.is_nil());
   code_blockt code_block;
 
   const symbol_exprt rounding_mode =
@@ -590,17 +575,6 @@ bool java_entry_point(
 
   assert(symbol.type.id()==ID_code);
 
-  create_java_initialize(symbol_table);
-
-  java_static_lifetime_init(
-    symbol_table,
-    symbol.location,
-    assume_init_pointers_not_null,
-    object_factory_parameters,
-    pointer_type_selector,
-    string_refinement_enabled,
-    message_handler);
-
   return generate_java_start_function(
     symbol,
     symbol_table,

jbmc/src/java_bytecode/java_entry_point.h

@@ -186,8 +186,14 @@ std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
   const select_pointer_typet &pointer_type_selector,
   message_handlert &message_handler);
 
-/// Adds `__cprover_initialize` to the \p symbol_table but does not generate
-/// code for it yet.
-void create_java_initialize(symbol_table_baset &symbol_table);
+/// Adds the body to __CPROVER_initialize
+void java_static_lifetime_init(
+  symbol_table_baset &symbol_table,
+  const source_locationt &source_location,
+  bool assume_init_pointers_not_null,
+  java_object_factory_parameterst object_factory_parameters,
+  const select_pointer_typet &pointer_type_selector,
+  bool string_refinement_enabled,
+  message_handlert &message_handler);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H

jbmc/unit/java_bytecode/java_string_literals.cpp

@@ -6,7 +6,7 @@ Author: Diffblue Limited
 
 \*******************************************************************/
 
-#include <java_bytecode/java_entry_point.h>
+#include <java_bytecode/java_bytecode_internal_additions.h>
 #include <java_bytecode/java_string_literals.h>
 #include <java_bytecode/java_types.h>
 #include <java_bytecode/java_utils.h>