Merge pull request #407 from smowton/java_basic_lazy_conversion

Java basic lazy method conversion

Author: Daniel Kroening

regression/cbmc-java/lazyloading1/A.class

@@ -0,0 +1,8 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.main
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::A\.f:\(\)V
+--
+elaborate java::B\.g:\(\)V

regression/cbmc-java/lazyloading1/B.class

@@ -0,0 +1,21 @@
+// The most basic lazy loading test: A::f is directly called, B::g should be unreachable
+
+public class test
+{
+  A a;
+  B b;
+  public static void main()
+  {
+    A.f();
+  }
+}
+
+class A
+{
+  public static void f() {}
+}
+
+class B
+{
+  public static void g() {}
+}

regression/cbmc-java/lazyloading1/test.class

@@ -0,0 +1,8 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.main
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::A\.f:\(\)V
+--
+elaborate java::B\.g:\(\)V

regression/cbmc-java/lazyloading1/test.desc

@@ -0,0 +1,23 @@
+// This test checks that because A is instantiated in main and B is not,
+// A::f is reachable and B::g is not
+
+public class test
+{
+  A a;
+  B b;
+  public static void main()
+  {
+    A a = new A();
+    a.f();
+  }
+}
+
+class A
+{
+  public void f() {}
+}
+
+class B
+{
+  public void g() {}
+}

regression/cbmc-java/lazyloading1/test.java

@@ -0,0 +1,8 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.main
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::A\.f:\(\)V
+--
+elaborate java::B\.g:\(\)V

regression/cbmc-java/lazyloading2/A.class

@@ -0,0 +1,30 @@
+// This test checks that because `main` has a parameter of type C, which has a field of type A,
+// A::f is considered reachable, but B::g is not.
+
+public class test
+{
+  public static void main(C c)
+  {
+    c.a.f();
+  }
+}
+
+class A
+{
+  public void f() {}
+}
+
+class B
+{
+  public void g() {}
+}
+
+class C
+{
+  A a;
+}
+
+class D
+{
+  B b;
+}

regression/cbmc-java/lazyloading2/B.class

@@ -4,23 +4,25 @@
 
 open LOG,"<tests.log" or die "Failed to open tests.log\n";
 
-my $ignore = 1;
+my $printed_this_test = 1;
 my $current_test = "";
 
 while (<LOG>) {
   chomp;
   if (/^Test '(.+)'/) {
     $current_test = $1;
-    $ignore = 0;
-  } elsif (1 == $ignore) {
-    next;
+    $printed_this_test = 0;
   } elsif (/\[FAILED\]\s*$/) {
-    $ignore = 1;
-    print "Failed test: $current_test\n";
-    my $outf = `sed -n '2p' $current_test/test.desc`;
-    $outf =~ s/\..*$/.out/;
-    system("cat $current_test/$outf");
-    print "\n\n";
+    if(0 == $printed_this_test) {
+      $printed_this_test = 1;
+      print "\n\n";
+      print "Failed test: $current_test\n";
+      my $outf = `sed -n '2p' $current_test/test.desc`;
+      $outf =~ s/\..*$/.out/;
+      system("cat $current_test/$outf");
+      print "\n\nFailed test.desc lines:\n";
+    }
+    print "$_\n";
   }
 }
 

regression/cbmc-java/lazyloading2/test.class

@@ -56,6 +56,7 @@ class optionst;
   "(graphml-witness):" \
   "(java-max-vla-length):(java-unwind-enum-static)" \
   "(localize-faults)(localize-faults-method):" \
+  "(lazy-methods)" \
   "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 
 class cbmc_parse_optionst:

regression/cbmc-java/lazyloading2/test.desc

@@ -544,8 +544,8 @@ bool compilet::parse(const std::string &file_name)
 
   language_filet language_file;
 
-  std::pair<language_filest::filemapt::iterator, bool>
-  res=language_files.filemap.insert(
+  std::pair<language_filest::file_mapt::iterator, bool>
+  res=language_files.file_map.insert(
     std::pair<std::string, language_filet>(file_name, language_file));
 
   language_filet &lf=res.first->second;
@@ -736,7 +736,7 @@ bool compilet::parse_source(const std::string &file_name)
     return true;
 
   // so we remove it from the list afterwards
-  language_files.filemap.erase(file_name);
+  language_files.file_map.erase(file_name);
   return false;
 }
 

regression/cbmc-java/lazyloading2/test.java

@@ -75,8 +75,8 @@ bool get_goto_modelt::operator()(const std::vector<std::string> &files)
           return true;
         }
 
-        std::pair<language_filest::filemapt::iterator, bool>
-          result=language_files.filemap.insert(
+        std::pair<language_filest::file_mapt::iterator, bool>
+          result=language_files.file_map.insert(
             std::pair<std::string, language_filet>(filename, language_filet()));
 
         language_filet &lf=result.first->second;

regression/cbmc-java/lazyloading3/A.class

@@ -339,7 +339,8 @@ void remove_virtual_functionst::get_functions(
     component_name,
     functions);
 
-  functions.push_back(root_function);
+  if(root_function.symbol_expr!=symbol_exprt())
+    functions.push_back(root_function);
 }
 
 /*******************************************************************\

regression/cbmc-java/lazyloading3/B.class

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_root_class.h"
 #include "java_types.h"
 #include "java_bytecode_convert_method.h"
+#include "java_bytecode_language.h"
 
 #include <util/namespace.h>
 #include <util/std_expr.h>
@@ -27,11 +28,15 @@ class java_bytecode_convert_classt:public messaget
     symbol_tablet &_symbol_table,
     message_handlert &_message_handler,
     bool _disable_runtime_checks,
-    size_t _max_array_length):
+    size_t _max_array_length,
+    lazy_methodst& _lazy_methods,
+    lazy_methods_modet _lazy_methods_mode):
     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(_lazy_methods),
+    lazy_methods_mode(_lazy_methods_mode)
   {
   }
 
@@ -52,6 +57,8 @@ class java_bytecode_convert_classt:public messaget
   symbol_tablet &symbol_table;
   const bool disable_runtime_checks;
   const size_t max_array_length;
+  lazy_methodst &lazy_methods;
+  lazy_methods_modet lazy_methods_mode;
 
   // conversion
   void convert(const classt &c);
@@ -75,6 +82,13 @@ Function: java_bytecode_convert_classt::convert
 
 void java_bytecode_convert_classt::convert(const classt &c)
 {
+  std::string qualified_classname="java::"+id2string(c.name);
+  if(symbol_table.has_symbol(qualified_classname))
+  {
+    debug() << "Skip class " << c.name << " (already loaded)" << eom;
+    return;
+  }
+
   class_typet class_type;
 
   class_type.set_tag(c.name);
@@ -107,7 +121,7 @@ void java_bytecode_convert_classt::convert(const classt &c)
   symbolt new_symbol;
   new_symbol.base_name=c.name;
   new_symbol.pretty_name=c.name;
-  new_symbol.name="java::"+id2string(c.name);
+  new_symbol.name=qualified_classname;
   class_type.set(ID_name, new_symbol.name);
   new_symbol.type=class_type;
   new_symbol.mode=ID_java;
@@ -128,13 +142,35 @@ void java_bytecode_convert_classt::convert(const classt &c)
 
   // now do methods
   for(const auto &method : c.methods)
-    java_bytecode_convert_method(
+  {
+    const irep_idt method_identifier=
+      id2string(qualified_classname)+
+      "."+id2string(method.name)+
+      ":"+method.signature;
+    // Always run the lazy pre-stage, as it symbol-table
+    // registers the function.
+    java_bytecode_convert_method_lazy(
       *class_symbol,
+      method_identifier,
       method,
-      symbol_table,
-      get_message_handler(),
-      disable_runtime_checks,
-      max_array_length);
+      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(),
+        disable_runtime_checks,
+        max_array_length);
+    }
+    else
+    {
+      // Wait for our caller to decide what needs elaborating.
+      lazy_methods[method_identifier]=std::make_pair(class_symbol, &method);
+    }
+  }
 
   // is this a root class?
   if(c.extends.empty())
@@ -322,13 +358,17 @@ bool java_bytecode_convert_class(
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
   bool disable_runtime_checks,
-  size_t max_array_length)
+  size_t max_array_length,
+  lazy_methodst &lazy_methods,
+  lazy_methods_modet lazy_methods_mode)
 {
   java_bytecode_convert_classt java_bytecode_convert_class(
     symbol_table,
     message_handler,
     disable_runtime_checks,
-    max_array_length);
+    max_array_length,
+    lazy_methods,
+    lazy_methods_mode);
 
   try
   {

regression/cbmc-java/lazyloading3/C.class

@@ -13,12 +13,15 @@ Author: Daniel Kroening, [email protected]
 #include <util/message.h>
 
 #include "java_bytecode_parse_tree.h"
+#include "java_bytecode_language.h"
 
 bool java_bytecode_convert_class(
   const java_bytecode_parse_treet &parse_tree,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
   bool disable_runtime_checks,
-  size_t max_array_length);
+  size_t max_array_length,
+  lazy_methodst &,
+  lazy_methods_modet);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H