From 5009cbb129dffe68f0960b5afbc48e7cbc52bf66 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 23 Jan 2018 17:08:10 +0000 Subject: [PATCH 1/2] CI lazy methods: re-explore array types with different element types Previously upon encountering a second array this would truncate the search for available types, but since they may have different element types this could lead to missing the availability of one or more of the element classes. Now we search array::reference every time we encounter it. --- src/java_bytecode/ci_lazy_methods.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp index 12813caf12b..2aa62b01904 100644 --- a/src/java_bytecode/ci_lazy_methods.cpp +++ b/src/java_bytecode/ci_lazy_methods.cpp @@ -344,7 +344,10 @@ void ci_lazy_methodst::initialize_needed_classes_from_pointer( const symbol_typet &class_type=to_symbol_type(pointer_type.subtype()); const auto ¶m_classid=class_type.get_identifier(); - if(needed_lazy_methods.add_needed_class(param_classid)) + // Note here: different arrays may have different element types, so we should + // explore again even if we've seen this classid before in the array case. + if(needed_lazy_methods.add_needed_class(param_classid) || + is_java_array_tag(param_classid)) { gather_field_types(pointer_type.subtype(), ns, needed_lazy_methods); } From 1e11f6dc37efa9c3066623848ff9410afc91a4ce Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Wed, 24 Jan 2018 17:52:44 +0000 Subject: [PATCH 2/2] Add test for multiple array types in single method --- .../lazyloading_multiple_array_types/A.class | Bin 0 -> 226 bytes .../lazyloading_multiple_array_types/A.java | 7 +++++++ .../lazyloading_multiple_array_types/B.class | Bin 0 -> 226 bytes .../lazyloading_multiple_array_types/B.java | 7 +++++++ .../Test.class | Bin 0 -> 728 bytes .../lazyloading_multiple_array_types/Test.java | 17 +++++++++++++++++ .../lazyloading_multiple_array_types/test.desc | 8 ++++++++ 7 files changed, 39 insertions(+) create mode 100644 regression/cbmc-java/lazyloading_multiple_array_types/A.class create mode 100644 regression/cbmc-java/lazyloading_multiple_array_types/A.java create mode 100644 regression/cbmc-java/lazyloading_multiple_array_types/B.class create mode 100644 regression/cbmc-java/lazyloading_multiple_array_types/B.java create mode 100644 regression/cbmc-java/lazyloading_multiple_array_types/Test.class create mode 100644 regression/cbmc-java/lazyloading_multiple_array_types/Test.java create mode 100644 regression/cbmc-java/lazyloading_multiple_array_types/test.desc diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/A.class b/regression/cbmc-java/lazyloading_multiple_array_types/A.class new file mode 100644 index 0000000000000000000000000000000000000000..a1388a0f223c195eb6c254380d53377982415320 GIT binary patch literal 226 zcmZ9FF$;oF6ot>#r;zsN$}Symz(+$%W@yZ87Fl5AuEEr zE9x?lOQmBwoTSk;@*rR_6cW1n4zege2irK6NreFnZq#Fd8(^{8eD&Fh-5NhYcU}k% atNjc0tAQq~MtkfUHN@?Y6P&yHgVq--EFPTz literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/A.java b/regression/cbmc-java/lazyloading_multiple_array_types/A.java new file mode 100644 index 00000000000..71f8cf87a4f --- /dev/null +++ b/regression/cbmc-java/lazyloading_multiple_array_types/A.java @@ -0,0 +1,7 @@ +public class A { + + public int f() { + return 1; + } + +} diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/B.class b/regression/cbmc-java/lazyloading_multiple_array_types/B.class new file mode 100644 index 0000000000000000000000000000000000000000..3fd3527e72a3bce7725397b76c7d524c8c07044f GIT binary patch literal 226 zcmZ9FKMR6T6vfZ=&(qAZIcR9BhFlt>!5|2thN4~VA&M!8_NiK$f`&doA1b=fu{)e| z@3}uXpYQ7pU;)p84%b4@LZ2X(X_3||f_1*HT(X@8Js)ngYFM4MjoU9 literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/B.java b/regression/cbmc-java/lazyloading_multiple_array_types/B.java new file mode 100644 index 00000000000..0f49c7dba43 --- /dev/null +++ b/regression/cbmc-java/lazyloading_multiple_array_types/B.java @@ -0,0 +1,7 @@ +public class B { + + public int g() { + return 5; + } + +} diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/Test.class b/regression/cbmc-java/lazyloading_multiple_array_types/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..6e6b1b68d70994da2f2009afeec0a3f9f8f2e568 GIT binary patch literal 728 zcmYL{Pfrt36vcn9Gwrm)AT0=1Y4IOuX^|?{6%_^4grw*KVj^ywPDdQ5t(mqaeiYf5 zxN(h|l4ydvn)soJ_Z3PP@7{OrJMX@8?##cFU&la+dp09v5+um#Fk^F-Yc|)pq2W!7 zSsROt#hlG8Zd>FOF*gj|Ppb;^b!ByVfY3%rl z#LHg&ted^n?1Y~GEYNoo`o`j(`_Xk6XTrf@)ZqeS7V{2y3Kk0vcPKa{Nh#8rTCBT` z-Qwy%_R}zIhN4fmvRHH|a#xWYGGA2pe6KC0WD4qS-_M5ZWCm(i3=N6vb(w`?s^+(X z(661pAZFSfIgml@$g~sk6~K@sY9*otLo%&33NldIjKqtAvXYhLX#NOwC>zD3#8|&5 z6JUx~^cVB+wA95cpVqoW zA5Lf9tb8YSKq{MzePQG`)~h4pf3%KBU&oC6F~}-m^FWL}5>p#uYg0_QVk<4DHb#jP s3Q8&BTt2r}>U)6Hc%qAafMtHeG=2~pwjbEkZK6b+$9fo7`may_2YLW~`v3p{ literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/Test.java b/regression/cbmc-java/lazyloading_multiple_array_types/Test.java new file mode 100644 index 00000000000..959c215df68 --- /dev/null +++ b/regression/cbmc-java/lazyloading_multiple_array_types/Test.java @@ -0,0 +1,17 @@ +public class Test { + + A[] arrayA; + B[] arrayB; + + public static void check(Test t) { + if (t == null || t.arrayA == null || t.arrayB == null || + t.arrayA.length == 0 || t.arrayB.length == 0 || + t.arrayA[0] == null || t.arrayB[0] == null) + return; + int i = t.arrayA[0].f(); + int j = t.arrayB[0].g(); + int sum = i + j; + assert(sum == 6); + } + +} diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/test.desc b/regression/cbmc-java/lazyloading_multiple_array_types/test.desc new file mode 100644 index 00000000000..f15d1291c02 --- /dev/null +++ b/regression/cbmc-java/lazyloading_multiple_array_types/test.desc @@ -0,0 +1,8 @@ +CORE +Test.class +--lazy-methods --verbosity 10 --function Test.check +^EXIT=0$ +^SIGNAL=0$ +elaborate java::A\.f:\(\)I +elaborate java::B\.g:\(\)I +VERIFICATION SUCCESSFUL