From cd9b839337ca8b39e1db442e6e12961d7b71bda2 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Thu, 29 Mar 2018 17:09:32 +0100 Subject: [PATCH] Revert "Merge pull request #1982 from NathanJPhillips/bugfix/load-object-once" This reverts commit 772b6038a3c3f29e74ef48114006a288a28ccd8f, reversing changes made to 05a7b4a90795c2a6848c9bfa3fe7f6f73aff0e6d. --- .../cbmc-java/invalid_classpath/Test.class | Bin 228 -> 0 bytes .../cbmc-java/invalid_classpath/Test.java | 3 -- .../cbmc-java/invalid_classpath/test-jar.desc | 10 ------ .../invalid_classpath/test-path.desc | 10 ------ .../java/lang/Object.class | Bin 1108 -> 0 bytes .../java/lang/Object.java | 33 ------------------ .../provide_object_implementation/test.desc | 10 ------ .../java_bytecode_convert_class.cpp | 6 ---- src/java_bytecode/java_class_loader.cpp | 29 +++++++-------- src/java_bytecode/java_class_loader.h | 1 - 10 files changed, 12 insertions(+), 90 deletions(-) delete mode 100644 regression/cbmc-java/invalid_classpath/Test.class delete mode 100644 regression/cbmc-java/invalid_classpath/Test.java delete mode 100644 regression/cbmc-java/invalid_classpath/test-jar.desc delete mode 100644 regression/cbmc-java/invalid_classpath/test-path.desc delete mode 100644 regression/cbmc-java/provide_object_implementation/java/lang/Object.class delete mode 100644 regression/cbmc-java/provide_object_implementation/java/lang/Object.java delete mode 100644 regression/cbmc-java/provide_object_implementation/test.desc diff --git a/regression/cbmc-java/invalid_classpath/Test.class b/regression/cbmc-java/invalid_classpath/Test.class deleted file mode 100644 index aaa01c760f28cd1b395b9b0710afe3558ea2fa39..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 228 zcmZ9Fs}90I5Jm6wNlSTH1Of*LYLEm&f+8Sj@Y}K>+w_r?mj6PLAou`2iZEM&V8qPM zxhJ#l&+`RfiM|gLT^E6i9>H0uLe*=6Ih~yd)}}m5!eFNgxo`4VR*{G^CRQ#~LGX`d zQzde%H1i^Ptrw}di2xRCmNXy?H3~CPT*5<~%B02w27ju{0Bf+hJG_l~5>I>n0NwdP YaJf4z)KTZBj@p!se@$QXI5gmY0WqT?_W%F@ diff --git a/regression/cbmc-java/invalid_classpath/Test.java b/regression/cbmc-java/invalid_classpath/Test.java deleted file mode 100644 index e3957a5157d..00000000000 --- a/regression/cbmc-java/invalid_classpath/Test.java +++ /dev/null @@ -1,3 +0,0 @@ -public class Test { - public void main() {} -} diff --git a/regression/cbmc-java/invalid_classpath/test-jar.desc b/regression/cbmc-java/invalid_classpath/test-jar.desc deleted file mode 100644 index ad020054856..00000000000 --- a/regression/cbmc-java/invalid_classpath/test-jar.desc +++ /dev/null @@ -1,10 +0,0 @@ -CORE symex-driven-lazy-loading-expected-failure -Test.class ---classpath ./NotHere.jar -^EXIT=6$ -^SIGNAL=0$ -^the program has no entry point$ -^failed to load class `Test'$ --- --- -symex-driven lazy loading should emit "the program has no entry point" but currently doesn't diff --git a/regression/cbmc-java/invalid_classpath/test-path.desc b/regression/cbmc-java/invalid_classpath/test-path.desc deleted file mode 100644 index 282ae0209f8..00000000000 --- a/regression/cbmc-java/invalid_classpath/test-path.desc +++ /dev/null @@ -1,10 +0,0 @@ -CORE symex-driven-lazy-loading-expected-failure -Test.class ---classpath ./NotHere -^EXIT=6$ -^SIGNAL=0$ -^the program has no entry point$ -^failed to load class `Test'$ --- --- -symex-driven lazy loading should emit "the program has no entry point" but currently doesn't diff --git a/regression/cbmc-java/provide_object_implementation/java/lang/Object.class b/regression/cbmc-java/provide_object_implementation/java/lang/Object.class deleted file mode 100644 index 868d3dbea58d74c6cc1256577c88936f3e4d3bbd..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1108 zcmah{T~E_s7(H)4wyxU*#{dN#15vk`z>Rkhq9K}$AYP1+=v_C;R;=yp-irEz^u`Ol z(L@uy_eU8|Kio%+VN3gVPtSSId7iUhzrXzea38HaZkZ6+G;lkQJ0>)2n#kjB9u0xq zuH!j!Pe5%nPXx4m|I`+kJ9IqzD16zqgJY}fvSRdYx$jz|k-$Qud3bKUwzgf%>u<-! z9f3l}>3fz81A>?SMeMfr2r>rNXpl%yuT6RTRcN_vy4aZN`Lug(_vB9Vxj?xit=@|# z)-d&<_gvqjM0G|YB?y?0-t_FDbbOCJ4e57e;CTHkJgL%8&hw>n_LlCGhlj4q9b8zB z}V2b#Z!RfdX)iKBS^W-FL$9VN)25%5i!9t4LB2yuv z*t+)~dF=zVn4n-{#6*<<9ZKN=6Tl*tQcrcBktgFj#IvtZerA-)SY|~dCi-6EsEN1L z_&1 getClass() { - return null; - } - - public int hashCode() { return 0; } - - public boolean equals(Object obj) { return (this == obj); } - - protected Object clone() throws CloneNotSupportedException { - throw new CloneNotSupportedException(); - } - - public String toString() { return "object"; } - - public final void notify() {} - - public final void notifyAll() {} - - public final void wait(long timeout) throws InterruptedException { - throw new InterruptedException(); - } - - public final void wait(long timeout, int nanos) throws InterruptedException { - wait(timeout); - } - - public final void wait() throws InterruptedException { wait(0); } - - protected void finalize() throws Throwable { } -} diff --git a/regression/cbmc-java/provide_object_implementation/test.desc b/regression/cbmc-java/provide_object_implementation/test.desc deleted file mode 100644 index 381ae109d1e..00000000000 --- a/regression/cbmc-java/provide_object_implementation/test.desc +++ /dev/null @@ -1,10 +0,0 @@ -CORE symex-driven-lazy-loading-expected-failure -java/lang/Object.class - -^EXIT=6$ -^SIGNAL=0$ -^the program has no entry point$ --- -^failed to add class symbol java::java\.lang\.Object$ --- -symex-driven lazy loading should emit "the program has no entry point" but currently doesn't diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index fe393c6fcf5..996d54985ba 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -185,12 +185,6 @@ void java_bytecode_convert_classt::operator()( PRECONDITION(!parse_trees.empty()); const irep_idt &class_name = parse_trees.front().parsed_class.name; - if(symbol_table.has_symbol("java::" + id2string(class_name))) - { - debug() << "Skip class " << class_name << " (already loaded)" << eom; - return; - } - // Add array types to the symbol table add_array_types(symbol_table); diff --git a/src/java_bytecode/java_class_loader.cpp b/src/java_bytecode/java_class_loader.cpp index 2196b9b7bbf..e44cf8d3052 100644 --- a/src/java_bytecode/java_class_loader.cpp +++ b/src/java_bytecode/java_class_loader.cpp @@ -81,9 +81,9 @@ java_class_loadert::parse_tree_with_overlayst &java_class_loadert::operator()( optionalt java_class_loadert::get_class_from_jar( const irep_idt &class_name, const std::string &jar_file, - const jar_indext &jar_index, java_class_loader_limitt &class_loader_limit) { + jar_indext &jar_index = jars_by_path.at(jar_file); auto jar_index_it = jar_index.find(class_name); if(jar_index_it == jar_index.end()) return {}; @@ -112,11 +112,9 @@ java_class_loadert::get_parse_tree( // First add all given JAR files for(const auto &jar_file : jar_files) { - jar_index_optcreft index = read_jar_file(class_loader_limit, jar_file); - if(!index) - continue; + read_jar_file(class_loader_limit, jar_file); optionalt parse_tree = - get_class_from_jar(class_name, jar_file, *index, class_loader_limit); + get_class_from_jar(class_name, jar_file, class_loader_limit); if(parse_tree) parse_trees.push_back(*parse_tree); } @@ -132,14 +130,12 @@ java_class_loadert::get_parse_tree( // This does not read from the jar file but from the jar_filet object we // just created - jar_index_optcreft index = read_jar_file(class_loader_limit, core_models); - if(index) - { - optionalt parse_tree = - get_class_from_jar(class_name, core_models, *index, class_loader_limit); - if(parse_tree) - parse_trees.push_back(*parse_tree); - } + read_jar_file(class_loader_limit, core_models); + + optionalt parse_tree = + get_class_from_jar(class_name, core_models, class_loader_limit); + if(parse_tree) + parse_trees.push_back(*parse_tree); } // Then add everything on the class path @@ -147,11 +143,10 @@ java_class_loadert::get_parse_tree( { if(has_suffix(cp_entry, ".jar")) { - jar_index_optcreft index = read_jar_file(class_loader_limit, cp_entry); - if(!index) - continue; + read_jar_file(class_loader_limit, cp_entry); + optionalt parse_tree = - get_class_from_jar(class_name, cp_entry, *index, class_loader_limit); + get_class_from_jar(class_name, cp_entry, class_loader_limit); if(parse_tree) parse_trees.push_back(*parse_tree); } diff --git a/src/java_bytecode/java_class_loader.h b/src/java_bytecode/java_class_loader.h index 6f46072aaa2..cfc098e899c 100644 --- a/src/java_bytecode/java_class_loader.h +++ b/src/java_bytecode/java_class_loader.h @@ -160,7 +160,6 @@ class java_class_loadert:public messaget optionalt get_class_from_jar( const irep_idt &class_name, const std::string &jar_file, - const jar_indext &jar_index, java_class_loader_limitt &class_loader_limit); };