From c520331e5f568735999f3d006a09c6654a9f8109 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 28 Mar 2018 13:19:28 +0100 Subject: [PATCH 1/5] Unit test to show java.lang.Object can be loaded from an explicit model --- .../java/lang/Object.class | Bin 0 -> 1108 bytes .../java/lang/Object.java | 33 ++++++++++++++++++ .../provide_object_implementation/test.desc | 8 +++++ 3 files changed, 41 insertions(+) create mode 100644 regression/cbmc-java/provide_object_implementation/java/lang/Object.class create mode 100644 regression/cbmc-java/provide_object_implementation/java/lang/Object.java create mode 100644 regression/cbmc-java/provide_object_implementation/test.desc diff --git a/regression/cbmc-java/provide_object_implementation/java/lang/Object.class b/regression/cbmc-java/provide_object_implementation/java/lang/Object.class new file mode 100644 index 0000000000000000000000000000000000000000..868d3dbea58d74c6cc1256577c88936f3e4d3bbd GIT binary patch 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 new file mode 100644 index 00000000000..325fd5f007f --- /dev/null +++ b/regression/cbmc-java/provide_object_implementation/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +java/lang/Object.class + +^EXIT=6$ +^SIGNAL=0$ +^the program has no entry point$ +-- +^failed to add class symbol java::java\.lang\.Object$ From 3c95aa1dc6d6feb913ac104b8ecc79a73ea41b8a Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 28 Mar 2018 11:57:59 +0100 Subject: [PATCH 2/5] Prevent attempting to load any class more than once --- .../cbmc-java/provide_object_implementation/test.desc | 2 +- src/java_bytecode/java_bytecode_convert_class.cpp | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/regression/cbmc-java/provide_object_implementation/test.desc b/regression/cbmc-java/provide_object_implementation/test.desc index 325fd5f007f..2edcd31244e 100644 --- a/regression/cbmc-java/provide_object_implementation/test.desc +++ b/regression/cbmc-java/provide_object_implementation/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE java/lang/Object.class ^EXIT=6$ diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 996d54985ba..fe393c6fcf5 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -185,6 +185,12 @@ 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); From 6749fd06ee473c2783db20df31460aad4da02f8e Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 28 Mar 2018 15:19:48 +0100 Subject: [PATCH 3/5] Tests to ensure invalid values in the classpath are ignored --- regression/cbmc-java/invalid_classpath/Test.class | Bin 0 -> 228 bytes regression/cbmc-java/invalid_classpath/Test.java | 3 +++ .../cbmc-java/invalid_classpath/test-jar.desc | 7 +++++++ .../cbmc-java/invalid_classpath/test-path.desc | 7 +++++++ 4 files changed, 17 insertions(+) create mode 100644 regression/cbmc-java/invalid_classpath/Test.class create mode 100644 regression/cbmc-java/invalid_classpath/Test.java create mode 100644 regression/cbmc-java/invalid_classpath/test-jar.desc create mode 100644 regression/cbmc-java/invalid_classpath/test-path.desc diff --git a/regression/cbmc-java/invalid_classpath/Test.class b/regression/cbmc-java/invalid_classpath/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..aaa01c760f28cd1b395b9b0710afe3558ea2fa39 GIT binary patch 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@ literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/invalid_classpath/Test.java b/regression/cbmc-java/invalid_classpath/Test.java new file mode 100644 index 00000000000..e3957a5157d --- /dev/null +++ b/regression/cbmc-java/invalid_classpath/Test.java @@ -0,0 +1,3 @@ +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 new file mode 100644 index 00000000000..2f8388be821 --- /dev/null +++ b/regression/cbmc-java/invalid_classpath/test-jar.desc @@ -0,0 +1,7 @@ +KNOWNBUG +Test.class +--classpath ./NotHere.jar +^EXIT=6$ +^SIGNAL=0$ +^the program has no entry point$ +^failed to load class `Test'$ diff --git a/regression/cbmc-java/invalid_classpath/test-path.desc b/regression/cbmc-java/invalid_classpath/test-path.desc new file mode 100644 index 00000000000..a9de0070126 --- /dev/null +++ b/regression/cbmc-java/invalid_classpath/test-path.desc @@ -0,0 +1,7 @@ +CORE +Test.class +--classpath ./NotHere +^EXIT=6$ +^SIGNAL=0$ +^the program has no entry point$ +^failed to load class `Test'$ From eae194f5f741b7d6c6a1c0dfe346ec431231501f Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 28 Mar 2018 14:38:23 +0100 Subject: [PATCH 4/5] Allow incorrect paths for jar files on the classpath without crashing --- .../cbmc-java/invalid_classpath/test-jar.desc | 2 +- src/java_bytecode/java_class_loader.cpp | 29 +++++++++++-------- src/java_bytecode/java_class_loader.h | 1 + 3 files changed, 19 insertions(+), 13 deletions(-) diff --git a/regression/cbmc-java/invalid_classpath/test-jar.desc b/regression/cbmc-java/invalid_classpath/test-jar.desc index 2f8388be821..ad17341c100 100644 --- a/regression/cbmc-java/invalid_classpath/test-jar.desc +++ b/regression/cbmc-java/invalid_classpath/test-jar.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE Test.class --classpath ./NotHere.jar ^EXIT=6$ diff --git a/src/java_bytecode/java_class_loader.cpp b/src/java_bytecode/java_class_loader.cpp index e44cf8d3052..2196b9b7bbf 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,9 +112,11 @@ java_class_loadert::get_parse_tree( // First add all given JAR files for(const auto &jar_file : jar_files) { - read_jar_file(class_loader_limit, jar_file); + jar_index_optcreft index = read_jar_file(class_loader_limit, jar_file); + if(!index) + continue; optionalt parse_tree = - get_class_from_jar(class_name, jar_file, class_loader_limit); + get_class_from_jar(class_name, jar_file, *index, class_loader_limit); if(parse_tree) parse_trees.push_back(*parse_tree); } @@ -130,12 +132,14 @@ java_class_loadert::get_parse_tree( // This does not read from the jar file but from the jar_filet object we // just created - 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); + 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); + } } // Then add everything on the class path @@ -143,10 +147,11 @@ java_class_loadert::get_parse_tree( { if(has_suffix(cp_entry, ".jar")) { - read_jar_file(class_loader_limit, cp_entry); - + jar_index_optcreft index = read_jar_file(class_loader_limit, cp_entry); + if(!index) + continue; optionalt parse_tree = - get_class_from_jar(class_name, cp_entry, class_loader_limit); + get_class_from_jar(class_name, cp_entry, *index, 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 cfc098e899c..6f46072aaa2 100644 --- a/src/java_bytecode/java_class_loader.h +++ b/src/java_bytecode/java_class_loader.h @@ -160,6 +160,7 @@ 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); }; From 81ac2590a6568f85f6592c95a6dd49b0159a19db Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 28 Mar 2018 15:30:49 +0100 Subject: [PATCH 5/5] Prevent test running on symex-driven lazy loading Currently symex-driven lazy loading doesn't emit the required warning but it should. --- regression/cbmc-java/invalid_classpath/test-jar.desc | 5 ++++- regression/cbmc-java/invalid_classpath/test-path.desc | 5 ++++- regression/cbmc-java/provide_object_implementation/test.desc | 4 +++- 3 files changed, 11 insertions(+), 3 deletions(-) diff --git a/regression/cbmc-java/invalid_classpath/test-jar.desc b/regression/cbmc-java/invalid_classpath/test-jar.desc index ad17341c100..ad020054856 100644 --- a/regression/cbmc-java/invalid_classpath/test-jar.desc +++ b/regression/cbmc-java/invalid_classpath/test-jar.desc @@ -1,7 +1,10 @@ -CORE +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 index a9de0070126..282ae0209f8 100644 --- a/regression/cbmc-java/invalid_classpath/test-path.desc +++ b/regression/cbmc-java/invalid_classpath/test-path.desc @@ -1,7 +1,10 @@ -CORE +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/test.desc b/regression/cbmc-java/provide_object_implementation/test.desc index 2edcd31244e..381ae109d1e 100644 --- a/regression/cbmc-java/provide_object_implementation/test.desc +++ b/regression/cbmc-java/provide_object_implementation/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure java/lang/Object.class ^EXIT=6$ @@ -6,3 +6,5 @@ java/lang/Object.class ^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