diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/Test.class b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/Test.class new file mode 100644 index 00000000000..1550bbf2a51 Binary files /dev/null and b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/Test.class differ diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/Test.java b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/Test.java new file mode 100644 index 00000000000..a2e59289842 --- /dev/null +++ b/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; + } + +} diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/Unused.class b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/Unused.class new file mode 100644 index 00000000000..506904b40f0 Binary files /dev/null and b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/Unused.class differ diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc new file mode 100644 index 00000000000..c27723b09f9 --- /dev/null +++ b/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\.\(\) + diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc new file mode 100644 index 00000000000..f832b065f69 --- /dev/null +++ b/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\.\(\) diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc new file mode 100644 index 00000000000..a9222f08176 --- /dev/null +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc @@ -0,0 +1,5 @@ +CORE +Test.class +--lazy-methods +VERIFICATION SUCCESSFUL + diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Test.class b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Test.class new file mode 100644 index 00000000000..3461be02111 Binary files /dev/null and b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Test.class differ diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Test.java b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Test.java new file mode 100644 index 00000000000..b56a68a2f9f --- /dev/null +++ b/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; + } + +} diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Unused1.class b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Unused1.class new file mode 100644 index 00000000000..7a722015569 Binary files /dev/null and b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Unused1.class differ diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Unused2.class b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Unused2.class new file mode 100644 index 00000000000..45ca30da9b4 Binary files /dev/null and b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Unused2.class differ diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc new file mode 100644 index 00000000000..d3d2757212f --- /dev/null +++ b/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\.\(\) + diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc new file mode 100644 index 00000000000..0dcedea2911 --- /dev/null +++ b/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\.\(\) diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc new file mode 100644 index 00000000000..a9222f08176 --- /dev/null +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc @@ -0,0 +1,5 @@ +CORE +Test.class +--lazy-methods +VERIFICATION SUCCESSFUL + diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/Test.class b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/Test.class new file mode 100644 index 00000000000..7edbf4cecd9 Binary files /dev/null and b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/Test.class differ diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/Test.java b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/Test.java new file mode 100644 index 00000000000..894bd4fc34f --- /dev/null +++ b/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; + +} diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc new file mode 100644 index 00000000000..e412a962e54 --- /dev/null +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc @@ -0,0 +1,5 @@ +CORE +Test.class +--show-goto-functions +java::Opaque\.:\(\)V +java::Opaque::clinit_wrapper diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc new file mode 100644 index 00000000000..9b1fb07cc31 --- /dev/null +++ b/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\.:\(\)V +java::Opaque::clinit_wrapper diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc new file mode 100644 index 00000000000..a9222f08176 --- /dev/null +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc @@ -0,0 +1,5 @@ +CORE +Test.class +--lazy-methods +VERIFICATION SUCCESSFUL + diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp index 8ce9b93dd35..142a1f56cc7 100644 --- a/src/java_bytecode/ci_lazy_methods.cpp +++ b/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 &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; diff --git a/src/java_bytecode/ci_lazy_methods.h b/src/java_bytecode/ci_lazy_methods.h index 9b9b7dda3c4..c7503d94423 100644 --- a/src/java_bytecode/ci_lazy_methods.h +++ b/src/java_bytecode/ci_lazy_methods.h @@ -23,6 +23,7 @@ #include #include #include +#include class java_string_library_preprocesst; @@ -99,7 +100,8 @@ class ci_lazy_methodst:public messaget java_class_loadert &java_class_loader, const std::vector &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 &extra_needed_classes; const select_pointer_typet &pointer_type_selector; + const synthetic_methods_mapt &synthetic_methods; }; #endif // CPROVER_JAVA_BYTECODE_GATHER_METHODS_LAZILY_H diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index b63d5923e5f..e3803c7ff10 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/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); }