Invoke static initializers on demand

Previously these were run from CPROVER_init; now they are run on demand,
using the same rules as the JVM (in brief, when `new` is called, or
a static field accessed, or a static method called).

This means that a faulting static initializer no longer blocks all coverage,
instead blocking only paths that would necessarily call the problematic initializer,
and initializers are called in the correct order, which they sometimes depend
upon (e.g. a class initializer assuming an enumeration initializer has run before
it uses the `.values()` method)

For details, see http://docs.oracle.com/javase/specs/jls/se8/html/jls-12.html#jls-12.4

This commit also amends the covered1 test, whose precise results I think
are still correct, but are perturbed by this change.

Author: smowton

regression/cbmc-java/covered1/test.desc

@@ -11,9 +11,8 @@ covered1.class
 .*\"coveredLines\": \"28\",$
 .*\"coveredLines\": \"28\",$
 .*\"coveredLines\": \"29\",$
-.*\"coveredLines\": \"9,18\",$
 .*\"coveredLines\": \"18\",$
 .*\"coveredLines\": \"18\",$
-.*\"coveredLines\": \"18,35\",$
+.*\"coveredLines\": \"35\",$
 --
 ^warning: ignoring

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -911,6 +911,174 @@ void java_bytecode_convert_methodt::check_static_field_stub(
 
 /*******************************************************************\
 
+Function: java_bytecode_convert_methodt::class_needs_clinit
+
+  Inputs: classname: Class name
+
+ Outputs: Returns true if the given class or one of its parents
+          has a static initializer
+
+ Purpose: Determine whether a `new` or static access against `classname`
+          should be prefixed with a static initialization check.
+
+\*******************************************************************/
+
+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;
+  }
+  auto findit_symbol=symbol_table.symbols.find(classname);
+  // Stub class?
+  if(findit_symbol==symbol_table.symbols.end())
+  {
+    warning() << "SKIPPED: " << classname << eom;
+    return false;
+  }
+  const symbolt &class_symbol=symbol_table.lookup(classname);
+  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;
+}
+
+/*******************************************************************\
+
+Function: java_bytecode_convert_methodt::get_or_create_clinit_wrapper
+
+  Inputs: classname: Class name
+
+ Outputs: Returns a symbol_exprt pointing to the given class' clinit
+          wrapper if one is required, or nil otherwise.
+
+ Purpose: 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.
+
+\*******************************************************************/
+
+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());
+
+  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();
+
+  // Create the wrapper now:
+  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());
+
+  code_ifthenelset wrapper_body;
+  wrapper_body.cond()=check_already_run;
+  code_blockt init_body;
+  // Note already-run is set *before* calling clinit, in order to prevent
+  // recursion in clinit methods.
+  code_assignt set_already_run(already_run_symbol.symbol_expr(), true_exprt());
+  init_body.move_to_operands(set_already_run);
+  const irep_idt &real_clinit_name=id2string(classname)+".<clinit>:()V";
+  const symbolt &class_symbol=symbol_table.lookup(classname);
+
+  auto findsymit=symbol_table.symbols.find(real_clinit_name);
+  if(findsymit!=symbol_table.symbols.end())
+  {
+    code_function_callt call_real_init;
+    call_real_init.function()=findsymit->second.symbol_expr();
+    init_body.move_to_operands(call_real_init);
+  }
+
+  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);
+  }
+
+  wrapper_body.then_case()=init_body;
+
+  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();
+}
+
+/*******************************************************************\
+
+Function: java_bytecode_convert_methodt::get_clinit_call
+
+  Inputs: classname: Class name
+
+ Outputs: Returns a function call to the given class' static initializer
+          wrapper if one is needed, or a skip instruction otherwise.
+
+ Purpose: Each static access to classname should be prefixed with a check
+          for necessary static init; this returns a call implementing
+          that check.
+
+\*******************************************************************/
+
+codet java_bytecode_convert_methodt::get_clinit_call(
+  const irep_idt &classname)
+{
+  exprt callee=get_or_create_clinit_wrapper(classname);
+  if(callee.is_nil())
+    return code_skipt();
+  code_function_callt ret;
+  ret.function()=callee;
+  return ret;
+}
+
+/*******************************************************************\
+
 Function: java_bytecode_convert_methodt::convert_instructions
 
   Inputs:
@@ -1378,6 +1546,18 @@ codet java_bytecode_convert_methodt::convert_instructions(
 
       call.function().add_source_location()=loc;
       c=call;
+
+      if(!use_this)
+      {
+        codet clinit_call=get_clinit_call(arg0.get(ID_C_class));
+        if(clinit_call.get_statement()!=ID_skip)
+        {
+          code_blockt ret_block;
+          ret_block.move_to_operands(clinit_call);
+          ret_block.move_to_operands(c);
+          c=std::move(ret_block);
+        }
+      }
     }
     else if(statement=="return")
     {
@@ -1916,9 +2096,14 @@ codet java_bytecode_convert_methodt::convert_instructions(
       }
       results[0]=java_bytecode_promotion(symbol_expr);
 
-      // set $assertionDisabled to false
-      if(field_name.find("$assertionsDisabled")!=std::string::npos)
+      codet clinit_call=get_clinit_call(arg0.get_string(ID_class));
+      if(clinit_call.get_statement()!=ID_skip)
+        c=clinit_call;
+      else if(field_name.find("$assertionsDisabled")!=std::string::npos)
+      {
+        // set $assertionDisabled to false
         c=code_assignt(symbol_expr, false_exprt());
+      }
     }
     else if(statement=="putfield")
     {
@@ -1937,6 +2122,14 @@ codet java_bytecode_convert_methodt::convert_instructions(
           to_symbol_type(arg0.type()).get_identifier());
       }
       c=code_assignt(symbol_expr, op[0]);
+      codet clinit_call=get_clinit_call(arg0.get_string(ID_class));
+      if(clinit_call.get_statement()!=ID_skip)
+      {
+        code_blockt ret_block;
+        ret_block.move_to_operands(clinit_call);
+        ret_block.move_to_operands(c);
+        c=std::move(ret_block);
+      }
     }
     else if(statement==patternt("?2?")) // i2c etc.
     {
@@ -1955,6 +2148,15 @@ codet java_bytecode_convert_methodt::convert_instructions(
 
       const exprt tmp=tmp_variable("new", ref_type);
       c=code_assignt(tmp, java_new_expr);
+      codet clinit_call=
+        get_clinit_call(to_symbol_type(arg0.type()).get_identifier());
+      if(clinit_call.get_statement()!=ID_skip)
+      {
+        code_blockt ret_block;
+        ret_block.move_to_operands(clinit_call);
+        ret_block.move_to_operands(c);
+        c=std::move(ret_block);
+      }
       results[0]=tmp;
     }
     else if(statement=="newarray" ||

src/java_bytecode/java_bytecode_convert_method_class.h

@@ -94,6 +94,8 @@ class java_bytecode_convert_methodt:public messaget
   expanding_vectort<variablest> variables;
   std::set<symbol_exprt> used_local_names;
   bool method_has_this;
+  std::map<irep_idt, bool> class_has_clinit_method;
+  std::map<irep_idt, bool> any_superclass_has_clinit_method;
 
   typedef enum instruction_sizet
   {
@@ -221,6 +223,10 @@ class java_bytecode_convert_methodt:public messaget
   void check_static_field_stub(
     const symbol_exprt &se,
     const irep_idt &basename);
+
+  bool class_needs_clinit(const irep_idt &classname);
+  exprt get_or_create_clinit_wrapper(const irep_idt &classname);
+  codet get_clinit_call(const irep_idt &classname);
 };
 
 #endif

src/java_bytecode/java_entry_point.cpp

@@ -98,19 +98,6 @@ Function: java_static_lifetime_init
 
 \*******************************************************************/
 
-struct static_initializer_callt
-{
-  symbol_exprt initializer_symbol;
-  bool is_enum;
-};
-
-static bool static_initializer_call_enum_lt(
-  const static_initializer_callt &a,
-  const static_initializer_callt &b)
-{
-  return a.is_enum && !b.is_enum;
-}
-
 bool java_static_lifetime_init(
   symbol_tablet &symbol_table,
   const source_locationt &source_location,
@@ -169,50 +156,6 @@ bool java_static_lifetime_init(
     }
   }
 
-  // we now need to run all the <clinit> methods
-
-  std::vector<static_initializer_callt> clinits;
-
-  for(symbol_tablet::symbolst::const_iterator
-      it=symbol_table.symbols.begin();
-      it!=symbol_table.symbols.end();
-      it++)
-  {
-    if(it->second.base_name=="<clinit>" &&
-       it->second.type.id()==ID_code &&
-       it->second.mode==ID_java)
-    {
-      const irep_idt symbol_name=
-        it->second.symbol_expr().get_identifier();
-      const std::string &symbol_str=id2string(symbol_name);
-      const std::string suffix(".<clinit>:()V");
-      assert(has_suffix(symbol_str, suffix));
-      const std::string class_symbol_name=
-        symbol_str.substr(0, symbol_str.size()-suffix.size());
-      const symbolt &class_symbol=symbol_table.lookup(class_symbol_name);
-      clinits.push_back(
-        {
-          it->second.symbol_expr(),
-          class_symbol.type.get_bool(ID_enumeration)
-        });
-    }
-  }
-
-  // Call enumeration initialisers before anything else.
-  // Really we should be calling them the first time they're referenced,
-  // as acccording to the JVM spec, but this ought to do the trick for
-  // most cases with much less effort.
-  std::sort(clinits.begin(), clinits.end(), static_initializer_call_enum_lt);
-
-  for(const auto &clinit : clinits)
-  {
-    code_function_callt function_call;
-    function_call.lhs()=nil_exprt();
-    function_call.function()=clinit.initializer_symbol;
-    function_call.add_source_location()=source_location;
-    code_block.add(function_call);
-  }
-
   return false;
 }