Convert Java methods only when they have a caller.

Author: smowton

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -28,11 +28,13 @@ class java_bytecode_convert_classt:public messaget
     symbol_tablet &_symbol_table,
     message_handlert &_message_handler,
     const bool &_disable_runtime_checks,
-    int _max_array_length):
+    int _max_array_length,
+    lazy_methodst& _lm):
     messaget(_message_handler),
     symbol_table(_symbol_table),
     disable_runtime_checks(_disable_runtime_checks),
-    max_array_length(_max_array_length)
+    max_array_length(_max_array_length),
+    lazy_methods(_lm)
   {
   }
 
@@ -53,6 +55,7 @@ class java_bytecode_convert_classt:public messaget
   symbol_tablet &symbol_table;
   const bool &disable_runtime_checks;
   int max_array_length;
+  lazy_methodst &lazy_methods;
 
   // conversion
   void convert(const classt &c);
@@ -134,10 +137,18 @@ void java_bytecode_convert_classt::convert(const classt &c)
     convert(*class_symbol, it);
 
   // now do methods
+  
   for(const auto & it : c.methods)
-    java_bytecode_convert_method(
-      *class_symbol, it, symbol_table, get_message_handler(), 
-      disable_runtime_checks, max_array_length);
+  {
+    const irep_idt method_identifier=
+      id2string(qualified_classname)+"."+id2string(it.name)+":"+it.signature;
+    java_bytecode_convert_method_lazy(
+      *class_symbol,method_identifier,it,symbol_table);
+    lazy_methods[method_identifier]=std::make_pair(class_symbol,&it);
+  }
+  //java_bytecode_convert_method(
+  //  *class_symbol, it, symbol_table, get_message_handler(), 
+  //  disable_runtime_checks, max_array_length);
 
   // is this a root class?
   if(c.extends.empty())
@@ -317,13 +328,15 @@ bool java_bytecode_convert_class(
   const bool &disable_runtime_checks,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  int max_array_length)
+  int max_array_length,
+  lazy_methodst& lazy_methods)
 {
   java_bytecode_convert_classt java_bytecode_convert_class(
 			       symbol_table, 
 			       message_handler, 
 			       disable_runtime_checks,
-			       max_array_length);
+			       max_array_length,
+			       lazy_methods);
 
   try
   {

src/java_bytecode/java_bytecode_convert_class.h

@@ -14,12 +14,16 @@ Author: Daniel Kroening, [email protected]
 
 #include "java_bytecode_parse_tree.h"
 
+typedef std::map<irep_idt, std::pair<const symbolt*, const java_bytecode_parse_treet::methodt*> >
+  lazy_methodst;
+
 bool java_bytecode_convert_class(
   const java_bytecode_parse_treet &parse_tree,
   const bool &disable_runtime_checks,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  int max_array_length);
+  int max_array_length,
+  lazy_methodst&);
 
 #endif
 

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/expr_util.h>
 
 #include <goto-programs/cfg.h>
+#include <goto-programs/class_hierarchy.h>
 #include <analyses/cfg_dominators.h>
 
 #include "java_bytecode_convert_method.h"
@@ -91,11 +92,15 @@ java_bytecode_convert_methodt::java_bytecode_convert_methodt(
   symbol_tablet &_symbol_table,
   message_handlert &_message_handler,
   const bool &_disable_runtime_checks,
-  int _max_array_length):
+  int _max_array_length,
+  std::vector<irep_idt>& _needed_methods,
+  const class_hierarchyt& _ch) :
   messaget(_message_handler),
   symbol_table(_symbol_table),
   disable_runtime_checks(_disable_runtime_checks),
-  max_array_length(_max_array_length)
+  max_array_length(_max_array_length),
+  needed_methods(_needed_methods),
+  class_hierarchy(_ch)
 {
 }
 
@@ -181,6 +186,35 @@ void java_bytecode_convert_methodt::push(const exprt::operandst &o)
     stack[stack.size()-o.size()+i]=o[i];
 }
 
+void java_bytecode_convert_method_lazy(
+  const symbolt& class_symbol,
+  const irep_idt method_identifier,
+  const java_bytecode_parse_treet::methodt &m,
+  symbol_tablet& symbol_table)
+{
+  symbolt method_symbol;
+  typet member_type=java_type_from_string(m.signature);
+
+  method_symbol.name=method_identifier;
+  method_symbol.base_name=m.base_name;
+  method_symbol.mode=ID_java;
+  method_symbol.location=m.source_location;
+  method_symbol.location.set_function(method_identifier);
+  
+  if(method_symbol.base_name=="<init>")
+  {
+    method_symbol.pretty_name=id2string(class_symbol.pretty_name)+"."+
+                              id2string(class_symbol.base_name)+"()";
+    member_type.set(ID_constructor,true);
+  }
+  else
+    method_symbol.pretty_name=id2string(class_symbol.pretty_name)+"."+
+      id2string(m.base_name)+"()";
+
+  method_symbol.type=member_type;
+  symbol_table.add(method_symbol);
+}
+  
 /*******************************************************************\
 
 Function: java_bytecode_convert_methodt::convert
@@ -346,9 +380,9 @@ void java_bytecode_convert_methodt::convert(
   if(!m.is_abstract)
     method_symbol.value=convert_instructions(m, code_type);
 
-  // do we have the method symbol already?
+  // Replace the existing stub symbol with the real deal:
   const auto s_it=symbol_table.symbols.find(method.get_name());
-  if(s_it!=symbol_table.symbols.end())
+  assert(s_it!=symbol_table.symbols.end());
     symbol_table.symbols.erase(s_it); // erase, we stubbed it
 
   symbol_table.add(method_symbol);
@@ -991,13 +1025,26 @@ codet java_bytecode_convert_methodt::convert_instructions(
 	  id2string(fn_basename) + "()";
       auto fn_type=arg0.type();
       check_stub_function(id,fn_basename,fn_prettyname,fn_type);
+
+      needed_methods.push_back(arg0.get(ID_identifier));
 
       if(is_virtual)
       {
         // dynamic binding
         assert(use_this);
         assert(!call.arguments().empty());
         call.function()=arg0;
+	const auto& call_class=arg0.get(ID_C_class);
+	assert(call_class!=irep_idt());
+	const auto& call_basename=arg0.get(ID_component_name);
+	assert(call_basename!=irep_idt());
+	auto child_classes=class_hierarchy.get_children_trans(call_class);
+	for(const auto& child_class : child_classes)
+	{
+	  auto methodid=id2string(child_class)+"."+id2string(call_basename);
+	  if(symbol_table.has_symbol(methodid))
+	    needed_methods.push_back(methodid);
+	}
       }
       else
       {
@@ -1974,13 +2021,17 @@ void java_bytecode_convert_method(
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
   const bool &disable_runtime_checks,
-  int max_array_length)
+  int max_array_length,
+  std::vector<irep_idt>& needed_methods,
+  const class_hierarchyt& ch)
 {
   java_bytecode_convert_methodt java_bytecode_convert_method(
 				symbol_table, 
 				message_handler, 
 				disable_runtime_checks, 
-				max_array_length);
+				max_array_length,
+				needed_methods,
+				ch);
 
   java_bytecode_convert_method(class_symbol, method);
 }

src/java_bytecode/java_bytecode_convert_method.h

@@ -14,13 +14,23 @@ Author: Daniel Kroening, [email protected]
 
 #include "java_bytecode_parse_tree.h"
 
+class class_hierarchyt;
+
 void java_bytecode_convert_method(
   const symbolt &class_symbol,
   const java_bytecode_parse_treet::methodt &,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
   const bool &enable_runtime_checks,
-  int max_array_length);
+  int max_array_length,
+  std::vector<irep_idt>& needed_methods,
+  const class_hierarchyt&);
+
+void java_bytecode_convert_method_lazy(
+  const symbolt &class_symbol,
+  const irep_idt method_identifier,
+  const java_bytecode_parse_treet::methodt &,
+  symbol_tablet &symbol_table);
 
 #endif
 

src/java_bytecode/java_bytecode_convert_method_class.h

@@ -8,12 +8,14 @@
 #include <util/std_expr.h>
 #include <analyses/cfg_dominators.h>
 #include "java_bytecode_parse_tree.h"
+#include "java_bytecode_convert_class.h"
 
 #include <vector>
 #include <list>
 
 class symbol_tablet;
 class symbolt;
+class class_hierarchyt;
 
 class java_bytecode_convert_methodt:public messaget
 {
@@ -22,7 +24,9 @@ class java_bytecode_convert_methodt:public messaget
     symbol_tablet &_symbol_table,
     message_handlert &_message_handler,
     const bool &_disable_runtime_checks,
-    int _max_array_length);
+    int _max_array_length,
+    std::vector<irep_idt>& _needed_methods,
+    const class_hierarchyt& _ch);
 
   typedef java_bytecode_parse_treet::methodt methodt;
   typedef java_bytecode_parse_treet::instructiont instructiont;
@@ -53,6 +57,8 @@ class java_bytecode_convert_methodt:public messaget
   symbol_tablet &symbol_table;
   const bool &disable_runtime_checks;
   int max_array_length;
+  std::vector<irep_idt>& needed_methods;
+  const class_hierarchyt& class_hierarchy;
 
   irep_idt current_method;
   typet method_return_type;

src/java_bytecode/java_bytecode_language.cpp

@@ -12,8 +12,11 @@ Author: Daniel Kroening, [email protected]
 #include <util/cmdline.h>
 #include <util/string2int.h>
 
+#include <goto-programs/class_hierarchy.h>
+
 #include "java_bytecode_language.h"
 #include "java_bytecode_convert_class.h"
+#include "java_bytecode_convert_method.h"
 #include "java_bytecode_internal_additions.h"
 #include "java_bytecode_typecheck.h"
 #include "java_entry_point.h"
@@ -181,10 +184,15 @@ Function: java_bytecode_languaget::typecheck
 
 \*******************************************************************/
 
+
+
 bool java_bytecode_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module)
 {
+  std::map<irep_idt, std::pair<const symbolt*, const java_bytecode_parse_treet::methodt*> >
+    lazy_methods;
+  
   // first convert all
   for(java_class_loadert::class_mapt::const_iterator
       c_it=java_class_loader.class_map.begin();
@@ -201,10 +209,74 @@ bool java_bytecode_languaget::typecheck(
 	 disable_runtime_checks,
 	 symbol_table, 
 	 get_message_handler(),
-	 max_user_array_length))
+	 max_user_array_length,
+	 lazy_methods
+	 ))
       return true;
   }
 
+  // Now incrementally elaborate methods that are reachable from this entry point:
+
+  // Convert-method will need this to find virtual function targets.
+  class_hierarchyt ch;
+  ch(symbol_table);
+  
+  std::vector<irep_idt> worklist1;
+  std::vector<irep_idt> worklist2;
+
+  auto main_function=get_main_symbol(symbol_table,main_class,get_message_handler(),true);
+  if(std::get<2>(main_function))
+  {
+    // Failed, mark all functions in the given main class reachable.
+    const auto& methods=java_class_loader.class_map.at(main_class).parsed_class.methods;
+    for(const auto& method : methods)
+    {
+      const irep_idt methodid="java::"+id2string(main_class)+"."+
+	id2string(method.name)+":"+
+	id2string(method.signature);
+      worklist2.push_back(methodid);
+    }
+  }
+  else
+    worklist2.push_back(std::get<0>(main_function).name);
+  
+  std::set<irep_idt> already_populated;
+  while(worklist2.size()!=0)
+  {
+    std::swap(worklist1,worklist2);
+    for(const auto& mname : worklist1)
+    {
+      if(!already_populated.insert(mname).second)
+	continue;
+      auto findit=lazy_methods.find(mname);
+      if(findit==lazy_methods.end())
+      {
+	debug() << "Skip " << mname << eom;
+	continue;
+      }
+      debug() << "Lazy methods: elaborate " << mname << eom;      
+      const auto& parsed_method=findit->second;
+      java_bytecode_convert_method(*parsed_method.first,*parsed_method.second,
+				   symbol_table,get_message_handler(),
+				   disable_runtime_checks,max_user_array_length,worklist2,ch);
+    }
+    worklist1.clear();
+  }
+
+  // Remove symbols for methods that were declared but never used:
+  symbol_tablet keep_symbols;
+
+  for(const auto& sym : symbol_table.symbols)
+  {
+    if(lazy_methods.count(sym.first) && !already_populated.count(sym.first))
+      continue;
+    keep_symbols.add(sym.second);
+  }
+
+  debug() << "Lazy methods: removed " << symbol_table.symbols.size() - keep_symbols.symbols.size() << " unreachable methods" << eom;
+
+  symbol_table.swap(keep_symbols);
+    
   // now typecheck all
   if(java_bytecode_typecheck(
        symbol_table, get_message_handler()))

src/java_bytecode/java_entry_point.cpp

@@ -327,7 +327,8 @@ void java_record_outputs(
 
 std::tuple<symbolt, bool, bool> get_main_symbol(symbol_tablet &symbol_table,
                                                 const irep_idt &main_class,
-                                                message_handlert &message_handler)
+                                                message_handlert &message_handler,
+						bool allow_no_body)
 {
   symbolt symbol;
 
@@ -449,7 +450,7 @@ std::tuple<symbolt, bool, bool> get_main_symbol(symbol_tablet &symbol_table,
     symbol=symbol_table.symbols.find(*matches.begin())->second;
 
     // check if it has a body
-    if(symbol.value.is_nil())
+    if(symbol.value.is_nil() && !allow_no_body)
     {
       message.error() << "main method `" << main_class
                       << "' has no body" << messaget::eom;

src/java_bytecode/java_entry_point.h

@@ -22,6 +22,7 @@ bool java_entry_point(
 
 std::tuple<symbolt, bool, bool> get_main_symbol(symbol_tablet &symbol_table,
                                                 const irep_idt &main_class,
-                                                message_handlert &);
+                                                message_handlert &,
+						bool allow_no_body = false);
 
 #endif