From fe739552af3c241cff862f4d9110b46f1b1c0d50 Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Tue, 3 Jul 2018 15:43:04 +0100 Subject: [PATCH] Captures information for static inner classes. --- .../java_bytecode_convert_class.cpp | 1 + .../java_bytecode/java_bytecode_parse_tree.h | 1 + .../java_bytecode/java_bytecode_parser.cpp | 2 + jbmc/src/java_bytecode/java_types.h | 11 +++ .../StaticInnerClass$1.class | Bin 0 -> 387 bytes ...ticInnerClass$1LocalClassInNonStatic.class | Bin 0 -> 467 bytes ...StaticInnerClass$1LocalClassInStatic.class | Bin 0 -> 381 bytes .../StaticInnerClass$2.class | Bin 0 -> 464 bytes ...InnerClass$PublicNonStaticInnerClass.class | Bin 0 -> 430 bytes ...ticInnerClass$PublicStaticInnerClass.class | Bin 0 -> 353 bytes .../StaticInnerClass$SomeInterface.class | Bin 0 -> 241 bytes .../StaticInnerClass.class | Bin 0 -> 996 bytes .../StaticInnerClass.java | 33 +++++++ .../parse_java_attributes.cpp | 88 ++++++++++++++++++ 14 files changed, 136 insertions(+) create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$1.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$1LocalClassInNonStatic.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$1LocalClassInStatic.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$2.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$PublicNonStaticInnerClass.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$PublicStaticInnerClass.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$SomeInterface.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass.java diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 8eb9cae4d81..650dbb6d93e 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -277,6 +277,7 @@ void java_bytecode_convert_classt::convert( class_type.set(ID_synthetic, c.is_synthetic); class_type.set_final(c.is_final); class_type.set_is_inner_class(c.is_inner_class); + class_type.set_is_static_class(c.is_static_class); if(c.is_enum) { if(max_array_length != 0 && c.enum_elements > max_array_length) diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h index 5d48175fd96..6a8c4a46fbc 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h @@ -218,6 +218,7 @@ class java_bytecode_parse_treet bool is_synthetic = false; bool is_annotation = false; bool is_inner_class = false; + bool is_static_class = false; bool attribute_bootstrapmethods_read = false; size_t enum_elements=0; diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index aa86988ebc4..74b5e977616 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -1622,6 +1622,7 @@ void java_bytecode_parsert::rinner_classes_attribute( bool is_private = (inner_class_access_flags & ACC_PRIVATE) != 0; bool is_public = (inner_class_access_flags & ACC_PUBLIC) != 0; bool is_protected = (inner_class_access_flags & ACC_PROTECTED) != 0; + bool is_static = (inner_class_access_flags & ACC_STATIC) != 0; // If the original parsed class name matches the inner class name, // the parsed class is an inner class, so overwrite the parsed class' @@ -1632,6 +1633,7 @@ void java_bytecode_parsert::rinner_classes_attribute( parsed_class.is_inner_class = is_inner_class; if(!is_inner_class) continue; + parsed_class.is_static_class = is_static; // Note that if outer_class_info_index == 0, the inner class is an anonymous // or local class, and is treated as private. if(outer_class_info_index == 0) diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 1a8579f3b69..92afbde3ccd 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -121,6 +121,17 @@ class java_class_typet:public class_typet return set(ID_is_inner_class, is_inner_class); } + const bool get_is_static_class() const + { + return get_bool(ID_is_static); + } + + void set_is_static_class(const bool &is_static_class) + { + return set(ID_is_static, is_static_class); + } + + bool get_final() { return get_bool(ID_final); diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$1.class b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$1.class new file mode 100644 index 0000000000000000000000000000000000000000..6495bd34e7500c5a0d3c01c9b293f6c93ba3d123 GIT binary patch literal 387 zcmZWlyH3ME5S)!2A9ft#7y?vONI(h#h!W96AX(y37}1}dBV6R1CHumEQ6MA=K7fxx ztkWQwV)ik&GuplHpU*D<7uXBnBJ$y2C=d&53ycV)841C=)JEGYf^&5IL~y6&Oc4gR z+Nk^0GE>!~%nD|Lv|LrWy3tKDO0BdyPmEF3w2*auvXHNmW!EMz%37QGow6_GOkg*} z2K*2n1R-wA4$cVSpNpyqQR6fzq?u11vW3bmVgH{jEte`WR#ne3=XLt6K57ea%GbLf zbQydz1pf>%csI@gSBL1VncnyVG>*>S(Ro`B^*9Fn2n^XGW}}en4*J;S>|(%iixD&D MaBfVy%7U(rYIC@T~xZCrb9a=oj@}6zg!f-g&*KY ziFe{ciMY6&Gxu@so%8Ye_730*CuP{!aZ$vsVKoPP4(bd{QuG;0dM?w(1w(Z((p<~1 zuaro75l_==s@_N?^({lK`M2B}GuXX&Dj58MRARVVPDJv=ClO`bQM^h*aWBoImX|(X z@MlhAcPfnHRI1s7(DQie;LyVnjy-Ik?7=mx1c%`)FVMIg#37HeJNs%FtM3L{^-tdW z`Ikr;0&_q&;%e4?oGe7BDV5*BP|+gQzr+j8))=Q`W0AbIK>ol1g20?h8Ajn^lh7m9 wp$?1CZ+F&U?N?ZBdyT?N)>z3}P5FRE>nLE0xCI{pp^a@+sbb{FW5Rvl3#XrE9smFU literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$1LocalClassInStatic.class b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$1LocalClassInStatic.class new file mode 100644 index 0000000000000000000000000000000000000000..6fa9b79bf13290e5d60a82cb23b9810b56b2ed1a GIT binary patch literal 381 zcmZutO-lnY5PjKhyLMgehgQ8P9*Wo=EJBasr6?>^Jyg7B(@;}l0-MzTi_t@|l)@9WsZN`F>HM0; zDV-pulhEJ8HdTbM9N{LRGei^t>F@(=Sbsu+_JLF^RqJ{mc Kh7L)75BLRZrBC_* literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$2.class b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$2.class new file mode 100644 index 0000000000000000000000000000000000000000..e4abe97b8da47aa14db3f776bb138a9c28baf17d GIT binary patch literal 464 zcmZWlO;5r=5Pe$;l~QCys^V8XaDZyW7;hRcL=zI!1BUxjR#;NDNxS&JJP;EP{s4cJ zamvM{OfvK4>rGzf=lAOyzzt5yu(9i+h(?zA4)z=zIA}63Mc!v9nVCvkR}A&R&tbjLHD159pw<)^od4t$K3aC-X0>=)ajXK4B@;dcw!purk9hS;}hAUxa literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$PublicNonStaticInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$PublicNonStaticInnerClass.class new file mode 100644 index 0000000000000000000000000000000000000000..57219cf2e2e849ae146414c26f7b186ca783eab7 GIT binary patch literal 430 zcmaJ-O-sW-5Pg%Rjg4s%tF2bN2tCvY#)CJ-OF;;fDpb60;-XvP2J+$m@=yd1{s4cJ zIO#=*Aj{6zdpkSxzP>*`0bJm)2Md9N4tAPoU}Mk5K7kb9n9!}BRXI5)4Cc#9R4R?N zmc=X+WqHZymC~xZCXA+k;rQf%V9oMJN$}@N%SHW?$l_ik8CRTTUKgpnQB5*z_dZ*R zSK(p{Jr@oRTy$aE7!$%ab8=TFnMxPAZX<;8KbZTwh%5;~^I?<;{S@6ME16aVbJ{Er zwAtKoB&8a)l-1X}8(BoJGtq+56$?8Wg_62#?k<-!{ZPTWSW`X{ykR_gW;fftXhL^k ztX@`ciOx4F$v7j|yDCrh+|;1IE>&sL*jk;>GF220TlKC22wVp^Lrb7fxNnl~o~k4> zX){e2{8tE08+1Vk>n-C<+1K$Z+3K_;xWoGDusIXAEY@T3tg=4nFA``o_8CQR*Z>)Q kf})!}oR1?%^55ZJuojQmKAVGc#ts7X*h`+^qKixTzh!1gvH$=8 literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$SomeInterface.class b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$SomeInterface.class new file mode 100644 index 0000000000000000000000000000000000000000..8588826f47b47e3ce5217613eaeeeb40d83dc1b8 GIT binary patch literal 241 zcmZ8bF%E)25S#<$1VL>qY^*X|%^GLYE$65FQA7xx=Oel6Xv$Hdq z_viTnaKKU`k;nu@%~J|wMQfcW>(69*9r6OGs#Ti`k-tVt^;e-h{*c|%xf zwk`ftU0{-`c0Y&L z^0RdD05!g}9rRwB$f1k-*!o-e$VJseHta-pnYx`&>Z{KC!L{-eLfb}p|9Qdve}HW_ zVaIkYj+o#r0gmQhaS|mgGcLg9CS7eVJ?nAn0uBD4MgGMZmOK_dkr^E8ET4G7EFZFU zklH}GeFJLWB6G=ymG8)YO;fg6n%{5Iv#79qG)t|eUXI*B^9%sCne*`ijGfD{I=8qp zgYBj)!0Ih>mp90NgRtwC8S;cHWl)F9`ZWYMSHLQ>mRPSb?>g&^d=X`iZ}Ps!yTaRC K!K_>=3x5E#MCnif literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass.java b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass.java new file mode 100644 index 00000000000..118f36e0777 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass.java @@ -0,0 +1,33 @@ +public class StaticInnerClass { + public static interface SomeInterface { + public int i = 0; + } + public static class PublicStaticInnerClass { + public int i; + public PublicStaticInnerClass(int i) { + this.i = i; + } + } + public class PublicNonStaticInnerClass { + public int i; + public PublicNonStaticInnerClass(int i) { + this.i = i; + } + } + public static SomeInterface staticAnonymousClass = new SomeInterface() { + public int i = 50; + }; + public SomeInterface anonymousClass = new SomeInterface() { + public int i = 25; + }; + public void testNonStatic() { + class LocalClassInNonStatic { + public int i = 1; + } + } + public static void testStatic() { + class LocalClassInStatic { + public int i = 2; + } + } +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp index 737ad516577..b431593857f 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp @@ -266,4 +266,92 @@ SCENARIO( } } } + + const symbol_tablet &new_symbol_table = + load_java_class("StaticInnerClass", "./java_bytecode/java_bytecode_parser"); + GIVEN("Some class with a static inner class") + { + WHEN("Parsing the InnerClasses attribute for a static inner class ") + { + THEN("The class should be marked as static") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::StaticInnerClass$PublicStaticInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_is_static_class()); + } + } + WHEN("Parsing the InnerClasses attribute for a non-static inner class ") + { + THEN("The class should not be marked as static") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::StaticInnerClass$PublicNonStaticInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE_FALSE(java_class.get_is_static_class()); + } + } + } + GIVEN("Some class with a static anonymous class") + { + WHEN("Parsing the InnerClasses attribute for a static anonymous class ") + { + THEN("The class should be marked as static") + { + const symbolt &class_symbol = + new_symbol_table.lookup_ref("java::StaticInnerClass$1"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_is_static_class()); + } + } + WHEN("Parsing the InnerClasses attribute for a non-static anonymous class ") + { + THEN("The class should not be marked as static") + { + const symbolt &class_symbol = + new_symbol_table.lookup_ref("java::StaticInnerClass$2"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE_FALSE(java_class.get_is_static_class()); + } + } + } + GIVEN("Some method containing a local class") + { + WHEN( + "Parsing the InnerClasses attribute for a local class in a static " + "method ") + { + THEN("The local class should be marked as static") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::StaticInnerClass$1LocalClassInStatic"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE_FALSE(java_class.get_is_static_class()); + } + } + WHEN( + "Parsing the InnerClasses attribute for a local class in a non-static " + "method ") + { + THEN("The local class should not be marked as static") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::StaticInnerClass$1LocalClassInNonStatic"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE_FALSE(java_class.get_is_static_class()); + } + } + } }