Merge pull request #796 from smowton/smowton/feature/clinit_on_demand

Run clinit methods on demand. Fixes commons-io coverage.

Author: peterschrammel

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

regression/cbmc-java/static_init1/A.class

@@ -0,0 +1,32 @@
+public class static_init {
+
+  // A should be initialised first, then B will begin init
+  // after A.x is set.
+  public static void main() {
+    assert(A.x == 1 && B.x == 1 && B.y == 2 && A.y == 2);
+  }
+
+}
+
+class A {
+
+  public static int x;
+  public static int y;
+  static {
+    x = 1;
+    y = B.y;
+  }
+
+}
+
+class B {
+
+  public static int x;
+  public static int y;
+  static {
+    x = A.x;
+    y = 2;
+
+  }
+
+}

regression/cbmc-java/static_init1/B.class

@@ -0,0 +1,8 @@
+CORE
+static_init.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/static_init1/static_init.class

@@ -0,0 +1,32 @@
+public class static_init {
+
+  // B will begin init first, but then begin A init before it
+  // has set B.y, leading to the unintuitive result given here.
+  public static void main() {
+    assert(B.x == 1 && B.y == 2 && A.x == 1 && A.y == 0);
+  }
+
+}
+
+class A {
+
+  public static int x;
+  public static int y;
+  static {
+    x = 1;
+    y = B.y;
+  }
+
+}
+
+class B {
+
+  public static int x;
+  public static int y;
+  static {
+    x = A.x;
+    y = 2;
+
+  }
+
+}

regression/cbmc-java/static_init1/static_init.java

@@ -0,0 +1,8 @@
+CORE
+static_init.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/static_init1/test.desc

@@ -34,10 +34,10 @@ bool instanceof(const typet &lhs, const typet &rhs, const namespacet &ns)
   if (type_eq(lhs, rhs, ns)) return true;
   assert(ID_class == lhs.id());
   const class_typet &lhs_class=to_class_type(lhs);
-  const irept::subt &bases=lhs_class.bases();
-  for (const irept &base : bases)
+  const class_typet::basest &bases=lhs_class.bases();
+  for(const exprt &base : bases)
   {
-    const typet &type=static_cast<const typet &>(base.find(ID_type));
+    const typet &type=base.type();
     if (instanceof(ns.follow(type), rhs, ns)) return true;
   }
   return false;

regression/cbmc-java/static_init2/A.class

@@ -171,21 +171,7 @@ void java_bytecode_convert_classt::convert(const classt &c)
       method_identifier,
       method,
       symbol_table);
-    if(lazy_methods_mode==LAZY_METHODS_MODE_EAGER)
-    {
-      // Upgrade to a fully-realized symbol now:
-      java_bytecode_convert_method(
-        *class_symbol,
-        method,
-        symbol_table,
-        get_message_handler(),
-        max_array_length);
-    }
-    else
-    {
-      // Wait for our caller to decide what needs elaborating.
-      lazy_methods[method_identifier]=std::make_pair(class_symbol, &method);
-    }
+    lazy_methods[method_identifier]=std::make_pair(class_symbol, &method);
   }
 
   // is this a root class?

regression/cbmc-java/static_init2/B.class

@@ -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" ||

regression/cbmc-java/static_init2/static_init.class

@@ -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