Merge pull request #855 from smowton/fix/lazy_methods_and_clinit

Lazy loading: load static initializers for needed classes. Fixes #846

Author: Daniel Kroening

regression/cbmc-java/lazyloading4/Main.class

@@ -0,0 +1,18 @@
+class Problem {
+  private static final Object[] DEFAULT = {};
+  private Object data;
+
+  Problem() {
+    this.data = DEFAULT;
+  }
+
+  void checkInvariant() {
+    assert data != null;
+  }
+}
+
+public class Main {
+  public static void main(String[] args) {
+    new Problem().checkInvariant();
+  }
+}

regression/cbmc-java/lazyloading4/Main.java

@@ -0,0 +1,6 @@
+CORE
+Main.class
+--lazy-methods
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL

regression/cbmc-java/lazyloading4/Problem.class

@@ -1,4 +1,5 @@
 SRC = bytecode_info.cpp \
+      ci_lazy_methods.cpp \
       expr2java.cpp \
       jar_file.cpp \
       java_bytecode_convert_class.cpp \

regression/cbmc-java/lazyloading4/test.desc

@@ -0,0 +1,53 @@
+/*******************************************************************\
+
+Module: Context-insensitive lazy methods container
+
+Author: Chris Smowton, chris.smowton@diffblue.com
+
+\*******************************************************************/
+
+#include <string>
+
+#include "ci_lazy_methods.h"
+
+/*******************************************************************\
+
+Function: ci_lazy_methodst::add_needed_method
+
+  Inputs: `method_symbol_name`: method name; must exist in symbol table.
+
+ Outputs:
+
+ Purpose: Notes `method_symbol_name` is referenced from some reachable
+          function, and should therefore be elaborated.
+
+\*******************************************************************/
+
+void ci_lazy_methodst::add_needed_method(const irep_idt &method_symbol_name)
+{
+  needed_methods.push_back(method_symbol_name);
+}
+
+/*******************************************************************\
+
+Function: java_bytecode_parsert::parse
+
+  Inputs: `class_symbol_name`: class name; must exist in symbol table.
+
+ Outputs: Returns true if `class_symbol_name` is new (not seen before).
+
+ Purpose: Notes class `class_symbol_name` will be instantiated, or
+          a static field belonging to it will be accessed. Also notes
+          that its static initializer is therefore reachable.
+
+\*******************************************************************/
+
+bool ci_lazy_methodst::add_needed_class(const irep_idt &class_symbol_name)
+{
+  if(!needed_classes.insert(class_symbol_name).second)
+    return false;
+  const irep_idt clinit_name(id2string(class_symbol_name)+".<clinit>:()V");
+  if(symbol_table.symbols.count(clinit_name))
+    add_needed_method(clinit_name);
+  return true;
+}

src/java_bytecode/Makefile

@@ -0,0 +1,46 @@
+/*******************************************************************\
+
+Module: Context-insensitive lazy methods container
+
+Author: Chris Smowton, chris.smowton@diffblue.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_JAVA_BYTECODE_CI_LAZY_METHODS_H
+#define CPROVER_JAVA_BYTECODE_CI_LAZY_METHODS_H
+
+#include <vector>
+#include <set>
+#include <util/symbol_table.h>
+
+class ci_lazy_methodst
+{
+public:
+  ci_lazy_methodst(
+    std::vector<irep_idt> &_needed_methods,
+    std::set<irep_idt> &_needed_classes,
+    symbol_tablet &_symbol_table):
+  needed_methods(_needed_methods),
+  needed_classes(_needed_classes),
+  symbol_table(_symbol_table)
+  {}
+
+  void add_needed_method(const irep_idt &);
+  // Returns true if new
+  bool add_needed_class(const irep_idt &);
+
+private:
+  // needed_methods is a vector because it's used as a work-list
+  // which is periodically cleared. It can't be relied upon to
+  // contain all methods that have previously been elaborated.
+  // It should be changed to a set if we develop the need to use
+  // it that way.
+  std::vector<irep_idt> &needed_methods;
+  // needed_classes on the other hand is a true set of every class
+  // found so far, so we can use a membership test to avoid
+  // repeatedly exploring a class hierarchy.
+  std::set<irep_idt> &needed_classes;
+  symbol_tablet &symbol_table;
+};
+
+#endif

src/java_bytecode/ci_lazy_methods.cpp

@@ -824,7 +824,7 @@ static void gather_symbol_live_ranges(
 
 /*******************************************************************\
 
-Function: java_bytecode_convert_methodt::convert_instructions
+Function: get_bytecode_type_width
 
   Inputs:
 
@@ -841,6 +841,18 @@ static unsigned get_bytecode_type_width(const typet &ty)
   return ty.get_unsigned_int(ID_width);
 }
 
+/*******************************************************************\
+
+Function: java_bytecode_convert_methodt::convert_instructions
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
 codet java_bytecode_convert_methodt::convert_instructions(
   const methodt &method,
   const code_typet &method_type)
@@ -1165,8 +1177,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
             if(as_string(arg0.get(ID_identifier))
                .find("<init>")!=std::string::npos)
             {
-              if(needed_classes)
-                needed_classes->insert(classname);
+              if(lazy_methods)
+                lazy_methods->add_needed_class(classname);
               code_type.set(ID_constructor, true);
             }
             else
@@ -1257,8 +1269,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
       {
         // static binding
         call.function()=symbol_exprt(arg0.get(ID_identifier), arg0.type());
-        if(needed_methods)
-          needed_methods->push_back(arg0.get(ID_identifier));
+        if(lazy_methods)
+          lazy_methods->add_needed_method(arg0.get(ID_identifier));
       }
 
       call.function().add_source_location()=loc;
@@ -1794,9 +1806,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
       symbol_exprt symbol_expr(arg0.type());
       const auto &field_name=arg0.get_string(ID_component_name);
       symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+field_name);
-      if(needed_classes && arg0.type().id()==ID_symbol)
+      if(lazy_methods && arg0.type().id()==ID_symbol)
       {
-        needed_classes->insert(
+        lazy_methods->add_needed_class(
           to_symbol_type(arg0.type()).get_identifier());
       }
       results[0]=java_bytecode_promotion(symbol_expr);
@@ -1816,9 +1828,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
       symbol_exprt symbol_expr(arg0.type());
       const auto &field_name=arg0.get_string(ID_component_name);
       symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+field_name);
-      if(needed_classes && arg0.type().id()==ID_symbol)
+      if(lazy_methods && arg0.type().id()==ID_symbol)
       {
-        needed_classes->insert(
+        lazy_methods->add_needed_class(
           to_symbol_type(arg0.type()).get_identifier());
       }
       c=code_assignt(symbol_expr, op[0]);
@@ -2413,15 +2425,13 @@ void java_bytecode_convert_method(
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
   size_t max_array_length,
-  safe_pointer<std::vector<irep_idt> > needed_methods,
-  safe_pointer<std::set<irep_idt> > needed_classes)
+  safe_pointer<ci_lazy_methodst> lazy_methods)
 {
   java_bytecode_convert_methodt java_bytecode_convert_method(
     symbol_table,
     message_handler,
     max_array_length,
-    needed_methods,
-    needed_classes);
+    lazy_methods);
 
   java_bytecode_convert_method(class_symbol, method);
 }

src/java_bytecode/ci_lazy_methods.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/safe_pointer.h>
 
 #include "java_bytecode_parse_tree.h"
+#include "ci_lazy_methods.h"
 
 class class_hierarchyt;
 
@@ -23,10 +24,8 @@ void java_bytecode_convert_method(
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
   size_t max_array_length,
-  safe_pointer<std::vector<irep_idt> > needed_methods,
-  safe_pointer<std::set<irep_idt> > needed_classes);
+  safe_pointer<ci_lazy_methodst> lazy_methods);
 
-// Must provide both the optional parameters or neither.
 inline void java_bytecode_convert_method(
   const symbolt &class_symbol,
   const java_bytecode_parse_treet::methodt &method,
@@ -40,8 +39,7 @@ inline void java_bytecode_convert_method(
     symbol_table,
     message_handler,
     max_array_length,
-    safe_pointer<std::vector<irep_idt> >::create_null(),
-    safe_pointer<std::set<irep_idt> >::create_null());
+    safe_pointer<ci_lazy_methodst>::create_null());
 }
 
 void java_bytecode_convert_method_lazy(

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <analyses/cfg_dominators.h>
 #include "java_bytecode_parse_tree.h"
 #include "java_bytecode_convert_class.h"
+#include "ci_lazy_methods.h"
 
 #include <vector>
 #include <list>
@@ -31,13 +32,11 @@ class java_bytecode_convert_methodt:public messaget
     symbol_tablet &_symbol_table,
     message_handlert &_message_handler,
     size_t _max_array_length,
-    safe_pointer<std::vector<irep_idt> > _needed_methods,
-    safe_pointer<std::set<irep_idt> > _needed_classes):
+    safe_pointer<ci_lazy_methodst> _lazy_methods):
     messaget(_message_handler),
     symbol_table(_symbol_table),
     max_array_length(_max_array_length),
-    needed_methods(_needed_methods),
-    needed_classes(_needed_classes)
+    lazy_methods(_lazy_methods)
   {
   }
 
@@ -55,8 +54,7 @@ class java_bytecode_convert_methodt:public messaget
 protected:
   symbol_tablet &symbol_table;
   const size_t max_array_length;
-  safe_pointer<std::vector<irep_idt> > needed_methods;
-  safe_pointer<std::set<irep_idt> > needed_classes;
+  safe_pointer<ci_lazy_methodst> lazy_methods;
 
   irep_idt method_id;
   irep_idt current_method;