Java frontend: create static initialiser globals ahead of time

This creates the global variables that indicate whether a static initialiser
has already run during java_bytecode_languaget::typecheck, rather than introducing
them during method conversion as before.

This means that symex-driven lazy loading will be able to rely on the globals being
mentioned in __CPROVER_initialize, even if the first method to reference the static
initialiser is converted after _initialize has been created.

Author: smowton

src/java_bytecode/CMakeLists.txt

@@ -7,7 +7,6 @@ add_subdirectory(library)
 
 add_library(java_bytecode ${sources} ${headers} )
 add_dependencies(java_bytecode core_models_files)
-target_sources(java_bytecode PUBLIC ${sources} ${headers})
 
 generic_includes(java_bytecode)
 

src/java_bytecode/Makefile

@@ -23,6 +23,7 @@ SRC = bytecode_info.cpp \
       java_object_factory.cpp \
       java_pointer_casts.cpp \
       java_root_class.cpp \
+      java_static_initializers.cpp \
       java_string_library_preprocess.cpp \
       java_string_literals.cpp \
       java_types.cpp \

src/java_bytecode/ci_lazy_methods.cpp

@@ -111,9 +111,9 @@ bool ci_lazy_methodst::operator()(
   std::set<irep_idt> needed_classes;
 
   {
-    std::vector<irep_idt> needed_clinits;
+    std::vector<irep_idt> initial_needed_methods;
     ci_lazy_methods_neededt initial_lazy_methods(
-      needed_clinits,
+      initial_needed_methods,
       needed_classes,
       symbol_table);
     initialize_needed_classes(
@@ -122,8 +122,8 @@ bool ci_lazy_methodst::operator()(
       initial_lazy_methods);
     method_worklist2.insert(
       method_worklist2.end(),
-      needed_clinits.begin(),
-      needed_clinits.end());
+      initial_needed_methods.begin(),
+      initial_needed_methods.end());
   }
 
   std::set<irep_idt> methods_already_populated;

src/java_bytecode/ci_lazy_methods_needed.cpp

@@ -34,14 +34,12 @@ bool ci_lazy_methods_neededt::add_needed_class(
 {
   if(!needed_classes.insert(class_symbol_name).second)
     return false;
-  const std::string &class_name_string = id2string(class_symbol_name);
-  const irep_idt clinit_name(class_name_string + ".<clinit>:()V");
-  if(symbol_table.symbols.count(clinit_name))
-    add_needed_method(clinit_name);
 
+  const std::string &class_name_string = id2string(class_symbol_name);
   const irep_idt cprover_validate(
     class_name_string + ".cproverNondetInitialize:()V");
   if(symbol_table.symbols.count(cprover_validate))
     add_needed_method(cprover_validate);
+
   return true;
 }

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_bytecode_convert_method.h"
 #include "java_bytecode_convert_method_class.h"
 #include "bytecode_info.h"
+#include "java_static_initializers.h"
 #include "java_string_library_preprocess.h"
 #include "java_types.h"
 #include "java_utils.h"
@@ -930,156 +931,6 @@ void java_bytecode_convert_methodt::check_static_field_stub(
   }
 }
 
-/// Determine whether a `new` or static access against `classname` should be
-/// prefixed with a static initialization check.
-/// \param classname: Class name
-/// \return Returns true if the given class or one of its parents has a static
-///   initializer
-bool java_bytecode_convert_methodt::class_needs_clinit(
-  const irep_idt &classname)
-{
-  auto findit_any=any_superclass_has_clinit_method.insert({classname, false});
-  if(!findit_any.second)
-    return findit_any.first->second;
-
-  auto findit_here=class_has_clinit_method.insert({classname, false});
-  if(findit_here.second)
-  {
-    const irep_idt &clinit_name=id2string(classname)+".<clinit>:()V";
-    findit_here.first->second=symbol_table.symbols.count(clinit_name);
-  }
-  if(findit_here.first->second)
-  {
-    findit_any.first->second=true;
-    return true;
-  }
-  const auto maybe_symbol=symbol_table.lookup(classname);
-  // Stub class?
-  if(!maybe_symbol)
-  {
-    warning() << "SKIPPED: " << classname << eom;
-    return false;
-  }
-  const symbolt &class_symbol=*maybe_symbol;
-  for(const auto &base : to_class_type(class_symbol.type).bases())
-  {
-    if(class_needs_clinit(to_symbol_type(base.type()).get_identifier()))
-    {
-      findit_any.first->second=true;
-      return true;
-    }
-  }
-  return false;
-}
-
-/// Create a ::clinit_wrapper the first time a static initializer might be
-/// called. The wrapper method checks whether static init has already taken
-/// place, calls the actual <clinit> method if not, and initializes super-
-/// classes and interfaces.
-/// \param classname: Class name
-/// \return Returns a symbol_exprt pointing to the given class' clinit wrapper
-///   if one is required, or nil otherwise.
-exprt java_bytecode_convert_methodt::get_or_create_clinit_wrapper(
-  const irep_idt &classname)
-{
-  if(!class_needs_clinit(classname))
-    return static_cast<const exprt &>(get_nil_irep());
-
-  // if the symbol table already contains the clinit_wrapper() function, return
-  // it
-  const irep_idt &clinit_wrapper_name=
-    id2string(classname)+"::clinit_wrapper";
-  auto findit=symbol_table.symbols.find(clinit_wrapper_name);
-  if(findit!=symbol_table.symbols.end())
-    return findit->second.symbol_expr();
-
-  // Otherwise, assume that class C extends class C' and implements interfaces
-  // I1, ..., In. We now create the following function (possibly recursively
-  // creating the clinit_wrapper functions for C' and I1, ..., In):
-  //
-  // java::C::clinit_wrapper()
-  // {
-  //   if (java::C::clinit_already_run == false)
-  //   {
-  //     java::C::clinit_already_run = true; // before recursive calls!
-  //
-  //     java::C'::clinit_wrapper();
-  //     java::I1::clinit_wrapper();
-  //     java::I2::clinit_wrapper();
-  //     // ...
-  //     java::In::clinit_wrapper();
-  //
-  //     java::C::<clinit>();
-  //   }
-  // }
-  const irep_idt &already_run_name=
-    id2string(classname)+"::clinit_already_run";
-  symbolt already_run_symbol;
-  already_run_symbol.name=already_run_name;
-  already_run_symbol.pretty_name=already_run_name;
-  already_run_symbol.base_name="clinit_already_run";
-  already_run_symbol.type=bool_typet();
-  already_run_symbol.value=false_exprt();
-  already_run_symbol.is_lvalue=true;
-  already_run_symbol.is_state_var=true;
-  already_run_symbol.is_static_lifetime=true;
-  already_run_symbol.mode=ID_java;
-  symbol_table.add(already_run_symbol);
-
-  equal_exprt check_already_run(
-    already_run_symbol.symbol_expr(),
-    false_exprt());
-
-  // the entire body of the function is an if-then-else
-  code_ifthenelset wrapper_body;
-
-  // add the condition to the if
-  wrapper_body.cond()=check_already_run;
-
-  // add the "already-run = false" statement
-  code_blockt init_body;
-  code_assignt set_already_run(already_run_symbol.symbol_expr(), true_exprt());
-  init_body.move_to_operands(set_already_run);
-
-  // iterate through the base types and add recursive calls to the
-  // clinit_wrapper()
-  const symbolt &class_symbol=*symbol_table.lookup(classname);
-  for(const auto &base : to_class_type(class_symbol.type).bases())
-  {
-    const auto base_name=to_symbol_type(base.type()).get_identifier();
-    exprt base_init_routine=get_or_create_clinit_wrapper(base_name);
-    if(base_init_routine.is_nil())
-      continue;
-    code_function_callt call_base;
-    call_base.function()=base_init_routine;
-    init_body.move_to_operands(call_base);
-  }
-
-  // call java::C::<clinit>(), if the class has one static initializer
-  const irep_idt &real_clinit_name=id2string(classname)+".<clinit>:()V";
-  auto find_sym_it=symbol_table.symbols.find(real_clinit_name);
-  if(find_sym_it!=symbol_table.symbols.end())
-  {
-    code_function_callt call_real_init;
-    call_real_init.function()=find_sym_it->second.symbol_expr();
-    init_body.move_to_operands(call_real_init);
-  }
-  wrapper_body.then_case()=init_body;
-
-  // insert symbol in the symbol table
-  symbolt wrapper_method_symbol;
-  code_typet wrapper_method_type;
-  wrapper_method_type.return_type()=void_typet();
-  wrapper_method_symbol.name=clinit_wrapper_name;
-  wrapper_method_symbol.pretty_name=clinit_wrapper_name;
-  wrapper_method_symbol.base_name="clinit_wrapper";
-  wrapper_method_symbol.type=wrapper_method_type;
-  wrapper_method_symbol.value=wrapper_body;
-  wrapper_method_symbol.mode=ID_java;
-  symbol_table.add(wrapper_method_symbol);
-  return wrapper_method_symbol.symbol_expr();
-}
-
 /// Each static access to classname should be prefixed with a check for
 /// necessary static init; this returns a call implementing that check.
 /// \param classname: Class name
@@ -1088,12 +939,17 @@ exprt java_bytecode_convert_methodt::get_or_create_clinit_wrapper(
 codet java_bytecode_convert_methodt::get_clinit_call(
   const irep_idt &classname)
 {
-  exprt callee=get_or_create_clinit_wrapper(classname);
-  if(callee.is_nil())
+  auto findit = symbol_table.symbols.find(clinit_wrapper_name(classname));
+  if(findit == symbol_table.symbols.end())
     return code_skipt();
-  code_function_callt ret;
-  ret.function()=callee;
-  return ret;
+  else
+  {
+    code_function_callt ret;
+    ret.function() = findit->second.symbol_expr();
+    if(needed_lazy_methods)
+      needed_lazy_methods->add_needed_method(findit->second.name);
+    return ret;
+  }
 }
 
 static unsigned get_bytecode_type_width(const typet &ty)

src/java_bytecode/java_bytecode_language.cpp

@@ -31,6 +31,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_bytecode_parser.h"
 #include "java_class_loader.h"
 #include "java_string_literals.h"
+#include "java_static_initializers.h"
 #include "java_utils.h"
 #include <java_bytecode/ci_lazy_methods.h>
 #include <java_bytecode/generate_java_generic_type.h>
@@ -476,6 +477,11 @@ bool java_bytecode_languaget::typecheck(
            << " String or Class constant symbols"
            << messaget::eom;
 
+  // For each class that will require a static initializer wrapper, create a
+  // function named package.classname::clinit_wrapper, and a corresponding
+  // global tracking whether it has run or not:
+  create_static_initializer_wrappers(symbol_table);
+
   // Now incrementally elaborate methods
   // that are reachable from this entry point.
   if(lazy_methods_mode==LAZY_METHODS_MODE_CONTEXT_INSENSITIVE)
@@ -488,6 +494,25 @@ bool java_bytecode_languaget::typecheck(
   {
     journalling_symbol_tablet journalling_symbol_table =
       journalling_symbol_tablet::wrap(symbol_table);
+
+    {
+      // Convert all static initialisers:
+      std::vector<irep_idt> static_initialisers;
+
+      // Careful not to add symbols while iterating over the symbol table!
+      for(const auto &symbol : symbol_table.symbols)
+      {
+        if(is_clinit_wrapper_function(symbol.second.name))
+          static_initialisers.push_back(symbol.second.name);
+      }
+
+      for(const auto &static_init_wrapper_name : static_initialisers)
+      {
+        convert_single_method(
+          static_init_wrapper_name, journalling_symbol_table);
+      }
+    }
+
     // Convert all methods for which we have bytecode now
     for(const auto &method_sig : method_bytecode)
     {
@@ -633,6 +658,39 @@ void java_bytecode_languaget::convert_lazy_method(
     symbol_table, get_message_handler(), string_refinement_enabled);
 }
 
+/// Notify ci_lazy_methods, if present, of any static function calls made by
+/// the given function body.
+/// \param function_body: function body code
+/// \param needed_lazy_methods: optional ci_lazy_method_neededt interface. If
+///   not set, this is a no-op; otherwise, its add_needed_method function will
+///   be called for each function call in `function_body`.
+static void notify_static_method_calls(
+  const exprt &function_body,
+  optionalt<ci_lazy_methods_neededt> needed_lazy_methods)
+{
+  if(needed_lazy_methods)
+  {
+    for(const_depth_iteratort it = function_body.depth_cbegin();
+        it != function_body.depth_cend();
+        ++it)
+    {
+      if(it->id() == ID_code)
+      {
+        const auto fn_call = expr_try_dynamic_cast<code_function_callt>(*it);
+        if(!fn_call)
+          continue;
+        // Only support non-virtual function calls for now, if string solver
+        // starts to introduce virtual function calls then we will need to
+        // duplicate the behavior of java_bytecode_convert_method where it
+        // handles the invokevirtual instruction
+        const symbol_exprt &fn_sym =
+          expr_dynamic_cast<symbol_exprt>(fn_call->function());
+        needed_lazy_methods->add_needed_method(fn_sym.get_identifier());
+      }
+    }
+  }
+}
+
 /// \brief Convert a method (one whose type is known but whose body hasn't
 ///   been converted) but don't run typecheck, etc
 /// \remarks Amends the symbol table entry for function `function_id`, which
@@ -673,32 +731,21 @@ bool java_bytecode_languaget::convert_single_method(
       generated_code.is_not_nil(), "Couldn't retrieve code for string method");
     // String solver can make calls to functions that haven't yet been seen.
     // Add these to the needed_lazy_methods collection
-    if(needed_lazy_methods)
-    {
-      for(const_depth_iteratort it = generated_code.depth_cbegin();
-          it != generated_code.depth_cend();
-          ++it)
-      {
-        if(it->id() == ID_code)
-        {
-          const auto fn_call = expr_try_dynamic_cast<code_function_callt>(*it);
-          if(!fn_call)
-            continue;
-          // Only support non-virtual function calls for now, if string solver
-          // starts to introduce virtual function calls then we will need to
-          // duplicate the behavior of java_bytecode_convert_method where it
-          // handles the invokevirtual instruction
-          const symbol_exprt &fn_sym =
-            expr_dynamic_cast<symbol_exprt>(fn_call->function());
-          needed_lazy_methods->add_needed_method(fn_sym.get_identifier());
-        }
-      }
-    }
+    notify_static_method_calls(generated_code, needed_lazy_methods);
     symbol.value = generated_code;
     return false;
   }
+  else if(is_clinit_wrapper_function(function_id))
+  {
+    symbolt &symbol = symbol_table.get_writeable_ref(function_id);
+    symbol.value = get_clinit_wrapper_body(function_id, symbol_table);
+    // Notify lazy methods of other static init functions called:
+    notify_static_method_calls(symbol.value, needed_lazy_methods);
+    return false;
+  }
 
-  // No string solver implementation, check if have bytecode for it
+  // No string solver or static init wrapper implementation;
+  // check if have bytecode for it
   if(cmb)
   {
     java_bytecode_convert_method(