Java frontend: clean up unused clinit symbols

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/Test.java

@@ -0,0 +1,22 @@
+public class Test {
+
+  // Refers to, but never instantiates or refers to static fields of, Unused.
+  // Thus a clinit-wrapper for Unused should be created, but subsequently
+  // discarded.
+  Unused u;
+
+  public static void main() {
+
+  }
+
+}
+
+class Unused {
+
+  static int x;
+
+  static {
+    x = 1;
+  }
+
+}

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--show-goto-functions
+java::Unused::clinit_wrapper
+Unused\.<clinit>\(\)
+

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--lazy-methods --show-goto-functions
+--
+java::Unused::clinit_wrapper
+Unused\.<clinit>\(\)

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc

@@ -0,0 +1,5 @@
+CORE
+Test.class
+--lazy-methods
+VERIFICATION SUCCESSFUL
+

regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Test.java

@@ -0,0 +1,26 @@
+public class Test {
+
+  // Refers to, but never instantiates or refers to static fields of, Unused.
+  // Thus a clinit-wrapper for Unused should be created, but subsequently
+  // discarded.
+  Unused1 u;
+
+  public static void main() {
+
+  }
+
+}
+
+class Unused1 extends Unused2 {
+
+}
+
+class Unused2 {
+
+  static int x;
+
+  static {
+    x = 1;
+  }
+
+}

regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc

@@ -0,0 +1,7 @@
+CORE
+Test.class
+--show-goto-functions
+java::Unused1::clinit_wrapper
+java::Unused2::clinit_wrapper
+Unused2\.<clinit>\(\)
+

regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc

@@ -0,0 +1,7 @@
+CORE
+Test.class
+--lazy-methods --show-goto-functions
+--
+java::Unused1::clinit_wrapper
+java::Unused2::clinit_wrapper
+Unused2\.<clinit>\(\)

regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc

@@ -0,0 +1,5 @@
+CORE
+Test.class
+--lazy-methods
+VERIFICATION SUCCESSFUL
+

regression/cbmc-java/lazyloading_synthetic_method_cleanup3/Test.java

@@ -0,0 +1,22 @@
+public class Test {
+
+  public static void main() {
+
+  }
+
+  public static Opaque unused() {
+
+    // Should cause jbmc to create a synthetic static initialiser for Opaque,
+    // but because this function isn't called by main() it should then be
+    // cleaned up as unused.
+    return Opaque.field;
+
+  }
+
+}
+
+class Opaque {
+
+  public static Opaque field;
+
+}

regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc

@@ -0,0 +1,5 @@
+CORE
+Test.class
+--show-goto-functions
+java::Opaque\.<clinit>:\(\)V
+java::Opaque::clinit_wrapper

regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--lazy-methods --show-goto-functions
+--
+java::Opaque\.<clinit>:\(\)V
+java::Opaque::clinit_wrapper

regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc

@@ -0,0 +1,5 @@
+CORE
+Test.class
+--lazy-methods
+VERIFICATION SUCCESSFUL
+

src/java_bytecode/ci_lazy_methods.cpp

@@ -36,14 +36,16 @@ ci_lazy_methodst::ci_lazy_methodst(
   java_class_loadert &java_class_loader,
   const std::vector<irep_idt> &extra_needed_classes,
   const select_pointer_typet &pointer_type_selector,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  const synthetic_methods_mapt &synthetic_methods)
   : messaget(message_handler),
     main_class(main_class),
     main_jar_classes(main_jar_classes),
     lazy_methods_extra_entry_points(lazy_methods_extra_entry_points),
     java_class_loader(java_class_loader),
     extra_needed_classes(extra_needed_classes),
-    pointer_type_selector(pointer_type_selector)
+    pointer_type_selector(pointer_type_selector),
+    synthetic_methods(synthetic_methods)
 {
   // build the class hierarchy
   class_hierarchy(symbol_table);
@@ -196,7 +198,8 @@ bool ci_lazy_methodst::operator()(
       // Don't keep functions that belong to this language that we haven't
       // converted above
       if(
-        method_bytecode.contains_method(sym.first) &&
+        (method_bytecode.contains_method(sym.first) ||
+         synthetic_methods.count(sym.first)) &&
         !methods_already_populated.count(sym.first))
       {
         continue;

src/java_bytecode/ci_lazy_methods.h

@@ -23,6 +23,7 @@
 #include <java_bytecode/java_class_loader.h>
 #include <java_bytecode/ci_lazy_methods_needed.h>
 #include <java_bytecode/select_pointer_type.h>
+#include <java_bytecode/synthetic_methods_map.h>
 
 class java_string_library_preprocesst;
 
@@ -99,7 +100,8 @@ class ci_lazy_methodst:public messaget
     java_class_loadert &java_class_loader,
     const std::vector<irep_idt> &extra_needed_classes,
     const select_pointer_typet &pointer_type_selector,
-    message_handlert &message_handler);
+    message_handlert &message_handler,
+    const synthetic_methods_mapt &synthetic_methods);
 
   // not const since messaget
   bool operator()(
@@ -164,6 +166,7 @@ class ci_lazy_methodst:public messaget
   java_class_loadert &java_class_loader;
   const std::vector<irep_idt> &extra_needed_classes;
   const select_pointer_typet &pointer_type_selector;
+  const synthetic_methods_mapt &synthetic_methods;
 };
 
 #endif // CPROVER_JAVA_BYTECODE_GATHER_METHODS_LAZILY_H

src/java_bytecode/java_bytecode_language.cpp

@@ -688,7 +688,8 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion(
     java_class_loader,
     java_load_classes,
     get_pointer_type_selector(),
-    get_message_handler());
+    get_message_handler(),
+    synthetic_methods);
 
   return method_gather(symbol_table, method_bytecode, method_converter);
 }