From adc9fd438bda4eb48c302ede5d36e9c1a035a73f Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 8 Feb 2018 14:15:34 +0000 Subject: [PATCH 1/2] Java frontend: clean up unused clinit symbols Previously clinit wrappers that had been generated but never actually called would remain in the GOTO program as empty, uncalled functions. Now they are cleaned up in the same way as unused user functions. --- src/java_bytecode/ci_lazy_methods.cpp | 9 ++++++--- src/java_bytecode/ci_lazy_methods.h | 5 ++++- src/java_bytecode/java_bytecode_language.cpp | 3 ++- 3 files changed, 12 insertions(+), 5 deletions(-) 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); } From 19d622b5f6045bb3b51873de2ffa3846a2b1ec6a Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 14 Feb 2018 15:00:37 +0000 Subject: [PATCH 2/2] Add tests to verify that synthetic method removal is performed These check that direct and indirect clinit wrappers, as well as stub class synthetic static initialisers, are removed if they are generated but not subsequently called. --- .../Test.class | Bin 0 -> 251 bytes .../Test.java | 22 +++++++++++++++ .../Unused.class | Bin 0 -> 268 bytes .../check_clinit_normally_present.desc | 6 ++++ .../check_clinit_removed_by_lazy_loading.desc | 6 ++++ .../check_runs_with_lazy_loading.desc | 5 ++++ .../Test.class | Bin 0 -> 252 bytes .../Test.java | 26 ++++++++++++++++++ .../Unused1.class | Bin 0 -> 176 bytes .../Unused2.class | Bin 0 -> 269 bytes .../check_clinit_normally_present.desc | 7 +++++ .../check_clinit_removed_by_lazy_loading.desc | 7 +++++ .../check_runs_with_lazy_loading.desc | 5 ++++ .../Test.class | Bin 0 -> 333 bytes .../Test.java | 22 +++++++++++++++ .../check_clinit_normally_present.desc | 5 ++++ .../check_clinit_removed_by_lazy_loading.desc | 6 ++++ .../check_runs_with_lazy_loading.desc | 5 ++++ 18 files changed, 122 insertions(+) create mode 100644 regression/cbmc-java/lazyloading_synthetic_method_cleanup1/Test.class create mode 100644 regression/cbmc-java/lazyloading_synthetic_method_cleanup1/Test.java create mode 100644 regression/cbmc-java/lazyloading_synthetic_method_cleanup1/Unused.class create mode 100644 regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc create mode 100644 regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc create mode 100644 regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc create mode 100644 regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Test.class create mode 100644 regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Test.java create mode 100644 regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Unused1.class create mode 100644 regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Unused2.class create mode 100644 regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc create mode 100644 regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc create mode 100644 regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc create mode 100644 regression/cbmc-java/lazyloading_synthetic_method_cleanup3/Test.class create mode 100644 regression/cbmc-java/lazyloading_synthetic_method_cleanup3/Test.java create mode 100644 regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc create mode 100644 regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc create mode 100644 regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc 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 0000000000000000000000000000000000000000..1550bbf2a510f6348e37f0a2cf58947fab0a5bd0 GIT binary patch literal 251 zcmZXOy$%6E6ot>-f9q$rRVZ{QXmms)QEezJ{p^~^2(t;h-b*D>cmNM2?kF@SnRCy4 z_uQL#y&q2iW5gkBG<~#uLqE^X9T;~-x8d8v6F--QCcpmQzp-; z$c{{$lTexvu8ZoN%Y`zmmdZ;xJcz4kz=O{r0|>D}qodIK(JDL0yhIlk{{bMr4qR4? nJ5QWdgn3y!i)VdYwu61EHF2zluAV^)P-6!!Pku*Ynq_0(62wnI9K2+&R z5M9ij!@1v_nakhr8Ne7_8#-JI4RlO+CLRUy&6){}Nu0*TRM2>N{S@eL`;8KG=5eY% z%CAsms~}A1v?ft{rE|cZv92L zQ&E9uUZL|UMpi79#^NX)i>l8q?9Jf`@\(\) + 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 0000000000000000000000000000000000000000..3461be021113741c613d77521221063d6330dfac GIT binary patch literal 252 zcmZXOy$ZrW5QJxwm}vY?IL5EI|aO0e(&d?<0x!p4J} zo%?onx!3#g1TaD1!$#9X%R`$$C84(3>GC3v<0-+NDXoe*!R`b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZ8IoFDqL-CemdL}v!obSNz#f`cTAZ3<2xl2F vC@?Sq?EwKsAO@-e(riGMERY6?uxf2*VB83nW(SgNU_m}0$pPdsF>nF^pywS6 literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..45ca30da9b42674ea76d341e14ab3407b189875b GIT binary patch literal 269 zcmYL@&1%9>5QWdgn3&tN{%q<-&|TX_1?e($Qz#UQT{Lx{#EV=>ub_$eTGEB!!Uyo7 zN>4&*7c+A>^Ucrs`*;HIfS!Vjs{jqOeRO|y^fPKr_+kE{FhYkt8$&`XH)q>tT)B|GT9~}e6&I|;R*Z?TW<7xBIs1Dah}-4 z_$^)PtiX_OxO|H{E11e*aF$L$HDDFi=G_6Zrw}M+uQq$cF8\(\) + 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 0000000000000000000000000000000000000000..7edbf4cecd947417877501b1981fcc85c7e697fa GIT binary patch literal 333 zcmZWjyGlbr5Ivjw@?NhdK0(mJF0n9;onj+c1ydO8_a>ukxY=lu^}C{tVBrV&QQ{dT zAUF#%a~^Zp&#(6n0B6`Q5Mwh(6Riwe8MY153+LV9(jaPg?hN9q=|~KkJ?G^nOe&cT zY*mwqC)Rn|gAa2V85HeKum5PDf}9iFPQz>{*G`@JK<10nv3<5B5~LY+O6+2f5h@t8 zRO;5&KXm)mScat1-z0?SBGGqLN$#8{ct:\(\)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 +