From 2ed059a195b0ce59aa578eb15a8d8becc00e0d5d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Fri, 27 Oct 2017 15:37:44 +0200 Subject: [PATCH 1/2] Support interface and class bound parsing in generics '::' is the separator for interface bounds in generic signatures, while ':' is the separator for class bounds. For example `` or ``. --- .../cbmc-java/generic_class_bound1/A.class | Bin 0 -> 84 bytes .../cbmc-java/generic_class_bound1/B.class | Bin 0 -> 84 bytes .../cbmc-java/generic_class_bound1/C.class | Bin 0 -> 84 bytes .../cbmc-java/generic_class_bound1/Gn.class | Bin 0 -> 831 bytes .../cbmc-java/generic_class_bound1/Gn.java | 15 +++++++++++++++ .../cbmc-java/generic_class_bound1/L.class | Bin 0 -> 183 bytes .../cbmc-java/generic_class_bound1/test.desc | 11 +++++++++++ src/java_bytecode/java_types.cpp | 17 +++++++++++++++-- 8 files changed, 41 insertions(+), 2 deletions(-) create mode 100644 regression/cbmc-java/generic_class_bound1/A.class create mode 100644 regression/cbmc-java/generic_class_bound1/B.class create mode 100644 regression/cbmc-java/generic_class_bound1/C.class create mode 100644 regression/cbmc-java/generic_class_bound1/Gn.class create mode 100644 regression/cbmc-java/generic_class_bound1/Gn.java create mode 100644 regression/cbmc-java/generic_class_bound1/L.class create mode 100644 regression/cbmc-java/generic_class_bound1/test.desc diff --git a/regression/cbmc-java/generic_class_bound1/A.class b/regression/cbmc-java/generic_class_bound1/A.class new file mode 100644 index 0000000000000000000000000000000000000000..91bb322316ec67839805440a666af2a60cfd0b4e GIT binary patch literal 84 zcmX^0Z`VEs1_l!bc6J6BohM*09W1+egFUf literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/generic_class_bound1/B.class b/regression/cbmc-java/generic_class_bound1/B.class new file mode 100644 index 0000000000000000000000000000000000000000..8e6e449cff33111750ab509ac98116fe70fe4cd0 GIT binary patch literal 84 zcmX^0Z`VEs1_l!bc6J6BohM*09XhRe*gdg literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/generic_class_bound1/C.class b/regression/cbmc-java/generic_class_bound1/C.class new file mode 100644 index 0000000000000000000000000000000000000000..7b228a9c4b515729fcc454b5634f01738c2c65fa GIT binary patch literal 84 zcmX^0Z`VEs1_l!bc6J6BohM*09Y~*fB*mh literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/generic_class_bound1/Gn.class b/regression/cbmc-java/generic_class_bound1/Gn.class new file mode 100644 index 0000000000000000000000000000000000000000..5513d09916cc9154b56515c9816de7cc53cb3888 GIT binary patch literal 831 zcmZuuO>fgc6r6QjJ9eG4BqV%8Y57PKXoQ4>)JBm2iChdta?}f_P2vQ%i5)o(qCX2H zK;poW13wBeYa5zK9K8E>=6Pn`?yuk9e*k!j0~;ppSTL|-;VyQI*t2mD_f0%7@lc@P ze|#dKyS?y8!197gD3fLE3z&pD%`Q=+6NEw1Wp88uguO4L5&11Q2>mz9*}#wcaxf)Q zaigJ}p2#>*=N#0N_rXG-zRsP`|MHfy>GzM6kv@(hhA|r|jj}3vi5#B2mh)W9R*VXj z=9tMKq;lh(dn!N3_Ed(GwwJ^~ILUY!Pv~6z4=u3M=^q}tZl~qGpmlde;dpTB4-=-b zy=WN^{a1mS&FqB-%Ef_$l7k{F6AcIZX!3qWqw!)iHqmnM2#*D{9&>G9gvun>An$yU z_%mK4l~PKHBISJYpewSH#(o$;G+YAACq#oS!vir zfi(xSrIp+nca6K<`iWw* z^#z*J)KkqewLuM?Q7i^g+V!kE*XDnDSmkoTDVL1fq+6Xehp_UAu2AeMu8~jyo>5TE lV|_-UqJPDP^4C&-JM}8jp}aDeh3mMH_GA}y6SvaS?LWPFkmvva literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/generic_class_bound1/Gn.java b/regression/cbmc-java/generic_class_bound1/Gn.java new file mode 100644 index 00000000000..5dfbf4da153 --- /dev/null +++ b/regression/cbmc-java/generic_class_bound1/Gn.java @@ -0,0 +1,15 @@ +interface A{} +interface B{} +interface C{} +interface L extends A,B,C{} + +public class Gn>{ + Gn ex1; + public void foo1(Gn ex1){ + if(ex1 != null) + this.ex1 = ex1; + } + public static void main(String[] args) { + System.out.println("ddfsdf"); + } +} diff --git a/regression/cbmc-java/generic_class_bound1/L.class b/regression/cbmc-java/generic_class_bound1/L.class new file mode 100644 index 0000000000000000000000000000000000000000..9c1bc26523e21d1c3c1bb6c76f6bf37e0fa0ef4a GIT binary patch literal 183 zcmX^0Z`VEs1_l!bes%^fb_Q;C1|D_>UUmjPMh4E{%=Em(lG377Mg~Kh5G$Xo#Ii*F zoW#6zegCAa)Z`LtJ4_)TM{6G^YaeH8Mh33n{L-T2RJY6=paJaed3qrIj0}uEj0^(k oMgfH#f!GO%o!J-|7#Wxtn1PUmffeXD1|Sb82qf7VIKVU~09yej9RL6T literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/generic_class_bound1/test.desc b/regression/cbmc-java/generic_class_bound1/test.desc new file mode 100644 index 00000000000..3ac218b6d84 --- /dev/null +++ b/regression/cbmc-java/generic_class_bound1/test.desc @@ -0,0 +1,11 @@ +CORE +Gn.class +--cover location +^EXIT=0$ +^SIGNAL=0$ +.*file Gn.java line 6 function java::Gn.\:\(\)V bytecode-index 1 block 1: FAILED +.*file Gn.java line 9 function java::Gn.foo1:\(LGn;\)V bytecode-index 1 block 1: FAILED +.*file Gn.java line 10 function java::Gn.foo1:\(LGn;\)V bytecode-index 4 block 2: FAILED +.*file Gn.java line 11 function java::Gn.foo1:\(LGn;\)V bytecode-index 5 block 3: FAILED +.*file Gn.java line 13 function java::Gn.main:\(\[Ljava/lang/String;\)V bytecode-index 2 block 1: SATISFIED +-- diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index 3f61e14ccba..ad928710f5b 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -599,6 +599,8 @@ char java_char_from_type(const typet &type) /// Converts the content of a generic class type into a vector of Java types, /// that is each type variable of the class has one entry in the returned /// vector. +/// This also supports parsing of bounds in the form of `` for classes +/// or `` for interfaces. /// /// For example for `HashMap` a vector with two elements would be returned /// @@ -607,8 +609,9 @@ std::vector java_generic_type_from_string( const std::string &class_name, const std::string &src) { - /// the class signature is of the form - size_t signature_end=find_closing_delimiter(src, 0, '<', '>'); + /// the class signature is of the form or of + /// the form if Bound_X is an interface + size_t signature_end = find_closing_delimiter(src, 0, '<', '>'); INVARIANT( src[0]=='<' && signature_end!=std::string::npos, "Class signature has unexpected format"); @@ -625,6 +628,16 @@ std::vector java_generic_type_from_string( { size_t bound_sep=signature.find(':'); INVARIANT(bound_sep!=std::string::npos, "No bound for type variable."); + + // is bound an interface? + // in this case the separator is '::' + if(signature[bound_sep + 1] == ':') + { + INVARIANT( + signature[bound_sep + 2] != ':', "Unknown bound for type variable."); + bound_sep++; + } + std::string type_var_name( "java::"+class_name+"::"+signature.substr(0, bound_sep)); std::string bound_type(signature.substr(bound_sep+1, var_sep-bound_sep)); From 6b88eb8bdd49eec55764ab36e9c44d9308f86061 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 1 Nov 2017 18:08:03 +0100 Subject: [PATCH 2/2] Add unit test for class / interface bound --- .../BoundedGenericClasses.java | 8 ++++++++ .../java_bytecode_parse_generics/C.class | Bin 0 -> 248 bytes .../java_bytecode_parse_generics/I.class | Bin 0 -> 103 bytes .../class_bound.class | Bin 0 -> 380 bytes .../interface_bound.class | Bin 0 -> 393 bytes 5 files changed, 8 insertions(+) create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/BoundedGenericClasses.java create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/C.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/I.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/class_bound.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/interface_bound.class diff --git a/unit/java_bytecode/java_bytecode_parse_generics/BoundedGenericClasses.java b/unit/java_bytecode/java_bytecode_parse_generics/BoundedGenericClasses.java new file mode 100644 index 00000000000..aef709de3cd --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/BoundedGenericClasses.java @@ -0,0 +1,8 @@ +class C{ +} +interface I{ +} +class interface_bound { +} +class class_bound { +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/C.class b/unit/java_bytecode/java_bytecode_parse_generics/C.class new file mode 100644 index 0000000000000000000000000000000000000000..4164c648fa15c547ae6e1d61f75a11c32399484a GIT binary patch literal 248 zcmXYry>7x#426$LNN5N@>d3^{c4!v1A_gMC61787_M60NFG_Eu{Pew;kQjIX9tz=0 zYsvOGpN=J8uBS7A1*QQUjC_oJObFgm8{Mu5&eL;BaO0|A!X(j#-@BiT>z&FP8`!DrRgId8O$&(>9E3NE&6xYl`Gs;1%Qb+3L^2p4?<#e}K# zQK`&V^pWj3Z!t$tzOzNr5|r(Uiey{Te>s8J--AK;G? z-$sSjg?(>kn78xT&#(0dfJ+=WFtBICv$4-$1yac-WH3(8<_u<3=7M1yOC|2x=TuY) zPYY7KxXgGl=atm_S2UX^Su>2{tl)M1n3k=|eTKtr@7v3t-`g|>N#cj(9?axI@usaP zZu!Azg~BA)hlV+bR>cQm=D-qq9VQCzPmU7U_IZU+6IxCi)D+ zjhz@K{~yE&dh`$aFuF8C-6C{NT`T?b71%og12$Ew6K(7ec7F^Qz#%r=Qe0v^jJmpu Han~o`OU+Xs literal 0 HcmV?d00001 diff --git a/unit/java_bytecode/java_bytecode_parse_generics/interface_bound.class b/unit/java_bytecode/java_bytecode_parse_generics/interface_bound.class new file mode 100644 index 0000000000000000000000000000000000000000..bf6552e0cfb2682bf44dee6520bc7552937d0961 GIT binary patch literal 393 zcmZ8dJx{|h5PfdahK4{tKpi?U0s~!`nkW)f0wF~(H0p|+#1vP-K~7SMpT&g4zz^U@ zA}_!uE>-(Gj7L=q M2b*|^-X`~d0U=>nI{*Lx literal 0 HcmV?d00001