From 72677f2b684d11b2e42828419b58a3e7eaeec24b Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 11 May 2017 20:21:28 +0100 Subject: [PATCH 1/4] Add regression test for runtime exceptions instrumentation --- .../ArrayIndexOutOfBoundsExceptionTest.class | Bin 0 -> 917 bytes .../ArrayIndexOutOfBoundsExceptionTest.java | 12 ++++++++++ .../ArrayIndexOutOfBoundsException/test.desc | 9 ++++++++ .../cbmc-java/ClassCastException1/A.class | Bin 0 -> 265 bytes .../cbmc-java/ClassCastException1/B.class | Bin 0 -> 265 bytes .../ClassCastExceptionTest.class | Bin 0 -> 976 bytes .../ClassCastExceptionTest.java | 13 +++++++++++ .../cbmc-java/ClassCastException1/test.desc | 9 ++++++++ .../cbmc-java/ClassCastException2/A.class | Bin 0 -> 249 bytes .../cbmc-java/ClassCastException2/B.class | Bin 0 -> 234 bytes .../cbmc-java/ClassCastException2/C.class | Bin 0 -> 234 bytes .../ClassCastExceptionTest.class | Bin 0 -> 902 bytes .../ClassCastExceptionTest.java | 21 ++++++++++++++++++ .../cbmc-java/ClassCastException2/test.desc | 8 +++++++ .../cbmc-java/NullPointerException2/A.class | Bin 0 -> 247 bytes .../cbmc-java/NullPointerException2/B.class | Bin 0 -> 241 bytes .../NullPointerException2/Test.class | Bin 0 -> 825 bytes .../cbmc-java/NullPointerException2/Test.java | 20 +++++++++++++++++ .../cbmc-java/NullPointerException2/test.desc | 9 ++++++++ .../cbmc-java/NullPointerException3/A.class | Bin 0 -> 247 bytes .../cbmc-java/NullPointerException3/B.class | Bin 0 -> 241 bytes .../NullPointerException3/Test.class | Bin 0 -> 835 bytes .../cbmc-java/NullPointerException3/Test.java | 20 +++++++++++++++++ .../cbmc-java/NullPointerException3/test.desc | 9 ++++++++ 24 files changed, 130 insertions(+) create mode 100644 regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.class create mode 100644 regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.java create mode 100644 regression/cbmc-java/ArrayIndexOutOfBoundsException/test.desc create mode 100644 regression/cbmc-java/ClassCastException1/A.class create mode 100644 regression/cbmc-java/ClassCastException1/B.class create mode 100644 regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.class create mode 100644 regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.java create mode 100644 regression/cbmc-java/ClassCastException1/test.desc create mode 100644 regression/cbmc-java/ClassCastException2/A.class create mode 100644 regression/cbmc-java/ClassCastException2/B.class create mode 100644 regression/cbmc-java/ClassCastException2/C.class create mode 100644 regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.class create mode 100644 regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.java create mode 100644 regression/cbmc-java/ClassCastException2/test.desc create mode 100644 regression/cbmc-java/NullPointerException2/A.class create mode 100644 regression/cbmc-java/NullPointerException2/B.class create mode 100644 regression/cbmc-java/NullPointerException2/Test.class create mode 100644 regression/cbmc-java/NullPointerException2/Test.java create mode 100644 regression/cbmc-java/NullPointerException2/test.desc create mode 100644 regression/cbmc-java/NullPointerException3/A.class create mode 100644 regression/cbmc-java/NullPointerException3/B.class create mode 100644 regression/cbmc-java/NullPointerException3/Test.class create mode 100644 regression/cbmc-java/NullPointerException3/Test.java create mode 100644 regression/cbmc-java/NullPointerException3/test.desc diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.class b/regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.class new file mode 100644 index 0000000000000000000000000000000000000000..4aeaf6432915086b1bbff6f6210a348e21fa04ad GIT binary patch literal 917 zcmaJr~Y8I9VrK*S`8OAE`qvt9Tou2dvv`5ISDPP4;2&vlAF2URgJV}^tDqp@z`W+eW z=ww2%8MvaiD?+9H^Pm~OQxT!sTn|I>am)AQpq0d}x6gva_oB^#D-Sj0j*Q|}#_kK{ z6J~1r%>(g4G@^+UVzaR0k7q z2<0pJ7q7J$hCxVJ7!ROjS*SZ$#zR7WgwyIANH^y99ECP|ybAmZo{Ur|z4Z$wo>83e z58i`4%=0GMykwLwYi)c>f#--RKBw7huqC$X`U&WmF9z~_W`;pRf$z@W1QbzXFNbTm z&JkVwiNOrE73+uHT((lJQy6bfkUDFALHY<2r^v8togEJm@{DY9g~p#{2C!!$%>pwV z%Q9CEb1YJGRyfaO<{8}J+5*chMPR!cBe7YFr24)26OBfsQdw1vCEqP literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.java b/regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.java new file mode 100644 index 00000000000..265b89ec489 --- /dev/null +++ b/regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.java @@ -0,0 +1,12 @@ +public class ArrayIndexOutOfBoundsExceptionTest { + public static void main(String args[]) { + try { + int[] a=new int[4]; + a[4]=0; + throw new RuntimeException(); + } + catch (ArrayIndexOutOfBoundsException exc) { + assert false; + } + } +} diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException/test.desc b/regression/cbmc-java/ArrayIndexOutOfBoundsException/test.desc new file mode 100644 index 00000000000..092cbf0b1f4 --- /dev/null +++ b/regression/cbmc-java/ArrayIndexOutOfBoundsException/test.desc @@ -0,0 +1,9 @@ +CORE +ArrayIndexOutOfBoundsExceptionTest.class +--java-throw-runtime-exceptions +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 9 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/ClassCastException1/A.class b/regression/cbmc-java/ClassCastException1/A.class new file mode 100644 index 0000000000000000000000000000000000000000..3618c09b4ef59667a868d72a16f83c799dc86ff5 GIT binary patch literal 265 zcmXX=yKcfj5S#@+2$+{!nv@9zZqfxIAuC8o7Aa!UpPf^3$gv~ef%q*dq!fGr9~H3& z6uUb!JNr2Q|D6E5AZ(+FzK?;AA%PUflHg5MsmzSfe0p9JoVfawgnpt*x!V3@vQ9-- zuo5O!E{e6NmF0KQG2cq_Xfl5#v_GnCoy&!?_EB62tz)6h+dh}SMpb1hwV7RkZP`Y-nY literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ClassCastException1/B.class b/regression/cbmc-java/ClassCastException1/B.class new file mode 100644 index 0000000000000000000000000000000000000000..e9257dc442776837ad9e9e3e5f111a6f8a1718aa GIT binary patch literal 265 zcmXYrziz@n48}i0NNCERl(kDo+JP)=AO<3kDn;!8V!xy(dQqC7+<|y4CZrBL01t)m zwHa*xzR&iZueaX|fH4L>n&^87JUkI7<9H{yQ&lK4BQ%Gv8-f#+Uy{&|RUtq2KZ&f? zBFWhq#APb-ji{8>wdt5|rFk`;PYC|1+*hewDm(rh literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.class b/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.class new file mode 100644 index 0000000000000000000000000000000000000000..de62bd5ca58363ea34481a67386f6eb76a94ba00 GIT binary patch literal 976 zcmZuvU2hUW6g{)Mu&^xhr4-v*t+q(17C)*lZH%V2Nt3N6(vY-1Ez1O_!qV(627if3 z|A5ccL=s7?&;BUmodsDNeAt<}bMHOp+_UrR_xB$FHu2Oz8f6`K4JfGSSkqB85R+Hy zNu+R3$9)4y8E+V<;en2a422cj_qi8{p6kC9zTNEb76UtGh;Iv51kV`M%36a#+v&A9 zL&g#=f7S0cxpydw8S+-ou{#ah6EdD$YQa0%{(G*E+V_uGIrixa}>;#|9EQO1*BLa7Q+>kCzjZ9@5DN4#UzvJ+tJJ*!J2a zt?(aShIBo!o%aX!X*dTt$B@`|Iuj?1dav&}d{4-^7iQ7rXd6&Fq*NV`O?o&_ zF6kNjOg2^al@YM1HLp)_>dmW6kw6K;lOKrWy92J;NM_8FS`6^YqtB}NR2`CNLk ILV<$SKh!SLn*aa+ literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.java b/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.java new file mode 100644 index 00000000000..bb7eacd1647 --- /dev/null +++ b/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.java @@ -0,0 +1,13 @@ +public class ClassCastExceptionTest { + public static void main(String args[]) { + try { + Object x = new Integer(0); + String y = (String)x; + throw new RuntimeException(); + } + catch (ClassCastException exc) { + assert false; + } + + } +} diff --git a/regression/cbmc-java/ClassCastException1/test.desc b/regression/cbmc-java/ClassCastException1/test.desc new file mode 100644 index 00000000000..983d5f730d8 --- /dev/null +++ b/regression/cbmc-java/ClassCastException1/test.desc @@ -0,0 +1,9 @@ +CORE +ClassCastExceptionTest.class +--java-throw-runtime-exceptions +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file ClassCastExceptionTest.java line 9 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/ClassCastException2/A.class b/regression/cbmc-java/ClassCastException2/A.class new file mode 100644 index 0000000000000000000000000000000000000000..5400c088442da1dc2e18fb898c5fdd4ef64a7bf7 GIT binary patch literal 249 zcmXYry>7xl5QJyJKVTe;($b^^3f!a%LP8c)R#F7fpPdt&W$egzM!Z(4NGW x7sw zWToAm`7|r-_4nrj;2EO;T|D?0`iKbLLRHEv3EjzbM{tt*LlUA?Rr0kxX0q9etYq?- z*10HmqEXiWL&qGH=F@cbLI~dLw#ns2+4wjqh1QACW_`}(r%`pamD<7o2_1gV7IAZsx5p~xZHYVk27R&Uz~|}RA)&`Q{0pFufE{6QPlY#< CC@&cR literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ClassCastException2/B.class b/regression/cbmc-java/ClassCastException2/B.class new file mode 100644 index 0000000000000000000000000000000000000000..57c02bfbefd2cf121d19be5c3ccef41f58cc1bbd GIT binary patch literal 234 zcmXX=O%K6P5S-O&srrbkiz5zP+=zsRQ{zJ1pL&TW)k@zZ{+5%(!4L4G#1@;(&g|@L zvak2!31EnZ2MbjfH5YY)GggT*6N1(0ZU}ae?j)feszff&$F0oPVjHv54AV%&8Tq#xn literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ClassCastException2/C.class b/regression/cbmc-java/ClassCastException2/C.class new file mode 100644 index 0000000000000000000000000000000000000000..3bff3313aa1ec28b55e0f9d2a44817e36a272510 GIT binary patch literal 234 zcmXX=Jr4m<5S-=Qan47y8YK!E9Z`6px@d_0IWO_#+{wL1{4JG4;RpCpVh@|l&g|@L zvak2!31Eb#k0NRw>K+;dccK$*r-Wj+w;?zp-6=vN)QMW2k6V?ktyL0)742PFat#ta=4_@BIp k!5e0m)sQ)NO8q1wK!N>Ngd906fnrTL1t6 literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.class b/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.class new file mode 100644 index 0000000000000000000000000000000000000000..503940e149abffa0c54dee4e007c706110245670 GIT binary patch literal 902 zcmZuv%Wl&^6g}fSoH$OK2MwVug+c;p3Js6!S|Qp{RxU`SRHCdLXB1o#r?MT?FJaLi zU|o=?L?p_Zk3yU=B|!=cd+xn+?m71{KYxAu4xovqfh_LmxNAUDXHCbNfrK*aX=Jdj zl%b`b8KIPzG@?8_kBB;UYxJ%Li~ zt#xF7up52b>owY;?|QvWr6(LJTiZm6j)+H(4ry&CP|$amy(S9P{D%dU#wQ1zO~AgNz=G&B_XPewroZcP$c&MuYh0W~Gz+BBnWRJ(DFYZt zMK#XxCP#@pDwI{ib;Nm>#Wfvu literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.java b/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.java new file mode 100644 index 00000000000..d8979415dbc --- /dev/null +++ b/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.java @@ -0,0 +1,21 @@ +class A {} + +class B extends A {} + +class C extends B {} + +public class ClassCastExceptionTest { + public static void main(String args[]) { + try { + A c = new C(); + B b = (B)c; + // TODO: an explicit throw is currently needed in order + // for CBMC to convert the exception handler + throw new RuntimeException(); + } + catch (ClassCastException exc) { + assert false; + } + + } +} diff --git a/regression/cbmc-java/ClassCastException2/test.desc b/regression/cbmc-java/ClassCastException2/test.desc new file mode 100644 index 00000000000..c593280efe5 --- /dev/null +++ b/regression/cbmc-java/ClassCastException2/test.desc @@ -0,0 +1,8 @@ +CORE +ClassCastExceptionTest.class +--java-throw-runtime-exceptions +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NullPointerException2/A.class b/regression/cbmc-java/NullPointerException2/A.class new file mode 100644 index 0000000000000000000000000000000000000000..19526643bf25706bad6f178a660ab3f724c8920b GIT binary patch literal 247 zcmXX=%MQU%5Iv*SQjg*bEV0my9g#E=iKJmc>~HIaE7c}d{>w^Y;RAe>m|I=U%sFSy zJU-vo8^8oT2L@al9UEN&DUKDvnyEzPbAmA#?g{21JxGEZs6?)Bmr!Oq5yq_af;1BG zUSvx1QZ)0Ey7Fk?PYKR8y=9SHDs8Xt literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NullPointerException2/B.class b/regression/cbmc-java/NullPointerException2/B.class new file mode 100644 index 0000000000000000000000000000000000000000..f29cbafef50e97fe2936695afa091c7f9c847cd4 GIT binary patch literal 241 zcmXX=Jx_!{5Pid^a45#o%2F+k#!h2_(TZ5y5&8u;x)<2Jz+(JcRwfqy0DqKm7M*0~ zedN7lzJETy09@fXg^$A+M=^3jbfdJgw*>$Eq9Fu#=1CIrN@@8x53L+)(e~_|RHhSs zBSz))zZuvUHF32nuLf9vGl tDx+}*kKb}byj)?7m=%o92`@iD?@T literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NullPointerException2/Test.class b/regression/cbmc-java/NullPointerException2/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..2644933a3a0cc875e9ea948ff2ebbc00121649f5 GIT binary patch literal 825 zcmZuuT~8B16g{)scKWf<(kfPzTD58crGC^Wh_NChCJUOBkcdy)?F0vxE!o`~eut0z z0iV$*i6rvwk5bPdSQFV~XXf5}?z!jQ`{U=g?*Q6(oJRqT9B$#Z#GO2BG$fii<)Y{*zh84>{Dkdd8=b`xa%rT7MQ)`=}=&@`NrM$-g~XU3%6R`B+}v5 zf?>DSo-a`UC%85Yf>#3_CMsIq^VP0VXo$RMi^P?4cqrQ=liML|tebfLyH#)ZM32Oj zM2m9}$S(T9XNyoMVl^iM(DiJ=3pE}!X4bl19CnSsEstAC(D6@F@fp`)j6B# zauf|Bsy6Hr4;?&0Tc9*TzU*x)KVg{;f6e~|XFLio1zZp3)>pBPRR1q8+e?NFa5tN{ z&g~YseNn0!C4AWsrVE}WS}op!cY5{^;(!ke6Ff5~PKh$#&L03OxIin1i~HIaE7c}d{>w^Y;RAe>m|I=U%sFSy zJU-vo8^8oT2L@al9UEN&DUKDvnyEzPbAmA#?g{21JxGEZs6?)Bmr!Oq5yq_af;1BG zUSvx1QZ)0Ey7Fk?PYKR8y=9SHDs8Xt literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NullPointerException3/B.class b/regression/cbmc-java/NullPointerException3/B.class new file mode 100644 index 0000000000000000000000000000000000000000..f29cbafef50e97fe2936695afa091c7f9c847cd4 GIT binary patch literal 241 zcmXX=Jx_!{5Pid^a45#o%2F+k#!h2_(TZ5y5&8u;x)<2Jz+(JcRwfqy0DqKm7M*0~ zedN7lzJETy09@fXg^$A+M=^3jbfdJgw*>$Eq9Fu#=1CIrN@@8x53L+)(e~_|RHhSs zBSz))zZuvUHF32nuLf9vGl tDx+}*kKb}byj)?7m=%o92`@iD?@T literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NullPointerException3/Test.class b/regression/cbmc-java/NullPointerException3/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..cd8ba9d445765df26cec3cd8ac74d3e3317cd1b5 GIT binary patch literal 835 zcmZuuT~8B16g{*3n0C9+(kfO(Kt(J?sUP(TG**PfWI>Y>67gxfoz%f)OLn)0-$H!% z88wnfBJchv^$egjk#0J7?wxbbJ@?)pKfiqk(8MDf13=E!1O<$^+6E4>gzC3(aN5$c8yX)=tVsisGP$`CXY;Ri?ES);`#5^yxkLB z5)%^lIS+x{k{_J)XSe%<$XBb{bdxuN7mP*+qbL&Y;1a6jd?qkC)P9~U2M$IAszX%k z&umwss2@?aVV8K|;31j10=W!{}r04lgZFOQ2DXT&6bAUZ`m zCEWQhupS>F_4*L$ Date: Mon, 12 Jun 2017 10:34:37 +0100 Subject: [PATCH 2/4] Refactoring the runtime exception instrumentation out of java_bytecode_convert Now the instrumentation for runtime exceptions is added in an independent pass (as described in java_bytecode_instrument.cpp), between the bytecode conversion and typechecking. --- .../ArrayIndexOutOfBoundsExceptionTest.class | Bin .../ArrayIndexOutOfBoundsExceptionTest.java | 0 .../test.desc | 0 src/cbmc/cbmc_parse_options.cpp | 1 + src/cbmc/cbmc_parse_options.h | 1 + src/java_bytecode/Makefile | 1 + .../java_bytecode_convert_method.cpp | 102 +--- .../java_bytecode_convert_method_class.h | 5 - .../java_bytecode_instrument.cpp | 528 ++++++++++++++++++ src/java_bytecode/java_bytecode_instrument.h | 19 + src/java_bytecode/java_bytecode_language.cpp | 8 + src/java_bytecode/java_bytecode_language.h | 1 + src/util/irep_ids.def | 2 + 13 files changed, 577 insertions(+), 91 deletions(-) rename regression/cbmc-java/{ArrayIndexOutOfBoundsException => ArrayIndexOutOfBoundsException1}/ArrayIndexOutOfBoundsExceptionTest.class (100%) rename regression/cbmc-java/{ArrayIndexOutOfBoundsException => ArrayIndexOutOfBoundsException1}/ArrayIndexOutOfBoundsExceptionTest.java (100%) rename regression/cbmc-java/{ArrayIndexOutOfBoundsException => ArrayIndexOutOfBoundsException1}/test.desc (100%) create mode 100644 src/java_bytecode/java_bytecode_instrument.cpp create mode 100644 src/java_bytecode/java_bytecode_instrument.h diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.class b/regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class similarity index 100% rename from regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.class rename to regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.java b/regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.java similarity index 100% rename from regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.java rename to regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.java diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException/test.desc b/regression/cbmc-java/ArrayIndexOutOfBoundsException1/test.desc similarity index 100% rename from regression/cbmc-java/ArrayIndexOutOfBoundsException/test.desc rename to regression/cbmc-java/ArrayIndexOutOfBoundsException1/test.desc diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index eac3893130d..d1dd4947e17 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -1070,6 +1070,7 @@ void cbmc_parse_optionst::help() // NOLINTNEXTLINE(whitespace/line_length) " --java-max-vla-length limit the length of user-code-created arrays\n" // NOLINTNEXTLINE(whitespace/line_length) + " --java-throw-runtime-exceptions Make implicit runtime exceptions explicit" " --java-cp-include-files regexp or JSON list of files to load (with '@' prefix)\n" " --java-unwind-enum-static try to unwind loops in static initialization of enums\n" "\n" diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 4f43637234a..145ff8e6e77 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -65,6 +65,7 @@ class optionst; "(graphml-witness):" \ "(java-max-vla-length):(java-unwind-enum-static)" \ "(java-cp-include-files):" \ + "(java-throw-runtime-exceptions)" \ "(localize-faults)(localize-faults-method):" \ "(lazy-methods)" \ "(test-invariant-failure)" \ diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index 0334b20595f..522218dc4f4 100644 --- a/src/java_bytecode/Makefile +++ b/src/java_bytecode/Makefile @@ -16,6 +16,7 @@ SRC = bytecode_info.cpp \ java_class_loader.cpp \ java_class_loader_limit.cpp \ java_entry_point.cpp \ + java_bytecode_instrument.cpp \ java_local_variable_table.cpp \ java_object_factory.cpp \ java_pointer_casts.cpp \ diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 14b67ba330f..ef6b1dd1bb3 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -509,39 +509,14 @@ static member_exprt to_member(const exprt &pointer, const exprt &fieldref) const dereference_exprt obj_deref(pointer2, class_type); - return member_exprt( + member_exprt member_expr( obj_deref, fieldref.get(ID_component_name), fieldref.type()); -} -codet java_bytecode_convert_methodt::get_array_bounds_check( - const exprt &arraystruct, - const exprt &idx, - const source_locationt &original_sloc) -{ - constant_exprt intzero=from_integer(0, java_int_type()); - binary_relation_exprt gezero(idx, ID_ge, intzero); - const member_exprt length_field(arraystruct, "length", java_int_type()); - binary_relation_exprt ltlength(idx, ID_lt, length_field); - code_blockt bounds_checks; - - bounds_checks.add(code_assertt(gezero)); - bounds_checks.operands().back().add_source_location()=original_sloc; - bounds_checks.operands().back().add_source_location() - .set_comment("Array index < 0"); - bounds_checks.operands().back().add_source_location() - .set_property_class("array-index-out-of-bounds-low"); - bounds_checks.add(code_assertt(ltlength)); - - bounds_checks.operands().back().add_source_location()=original_sloc; - bounds_checks.operands().back().add_source_location() - .set_comment("Array index >= length"); - bounds_checks.operands().back().add_source_location() - .set_property_class("array-index-out-of-bounds-high"); - - // TODO make this throw ArrayIndexOutOfBoundsException instead of asserting. - return bounds_checks; + // tag it so it's easy to identify during instrumentation + member_expr.set(ID_java_member_access, true); + return member_expr; } /// Find all goto statements in 'repl' that target 'old_label' and redirect them @@ -1256,50 +1231,26 @@ codet java_bytecode_convert_methodt::convert_instructions( else if(statement=="athrow") { assert(op.size()==1 && results.size()==1); - code_blockt block; - // TODO throw NullPointerException instead - const typecast_exprt lhs(op[0], pointer_typet(empty_typet())); - const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type()))); - const exprt not_equal_null( - binary_relation_exprt(lhs, ID_notequal, rhs)); - code_assertt check(not_equal_null); - check.add_source_location() - .set_comment("Throw null"); - check.add_source_location() - .set_property_class("null-pointer-exception"); - block.move_to_operands(check); side_effect_expr_throwt throw_expr; throw_expr.add_source_location()=i_it->source_location; throw_expr.copy_to_operands(op[0]); c=code_expressiont(throw_expr); results[0]=op[0]; - - block.move_to_operands(c); - c=block; } else if(statement=="checkcast") { // checkcast throws an exception in case a cast of object // on stack to given type fails. // The stack isn't modified. - // TODO: convert assertions to exceptions. assert(op.size()==1 && results.size()==1); binary_predicate_exprt check(op[0], ID_java_instanceof, arg0); code_assertt assert_class(check); assert_class.add_source_location().set_comment("Dynamic cast check"); assert_class.add_source_location().set_property_class("bad-dynamic-cast"); - // checkcast passes when the operand is null. - empty_typet voidt; - pointer_typet voidptr(voidt); - exprt null_check_op=op[0]; - if(null_check_op.type()!=voidptr) - null_check_op.make_typecast(voidptr); - code_ifthenelset conditional_check; - notequal_exprt op_not_null(null_check_op, null_pointer_exprt(voidptr)); - conditional_check.cond()=std::move(op_not_null); - conditional_check.then_case()=std::move(assert_class); - c=std::move(conditional_check); + // we add this assert such that we can recognise it + // during the instrumentation phase + c=std::move(assert_class); results[0]=op[0]; } else if(statement=="invokedynamic") @@ -1525,17 +1476,12 @@ codet java_bytecode_convert_methodt::convert_instructions( pointer_typet(java_type_from_char(type_char))); plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type()); + // tag it so it's easy to identify during instrumentation + data_plus_offset.set(ID_java_array_access, true); typet element_type=data_ptr.type().subtype(); const dereference_exprt element(data_plus_offset, element_type); - c=code_blockt(); - codet bounds_check= - get_array_bounds_check(deref, op[1], i_it->source_location); - bounds_check.add_source_location()=i_it->source_location; - c.move_to_operands(bounds_check); - code_assignt array_put(element, op[2]); - array_put.add_source_location()=i_it->source_location; - c.move_to_operands(array_put); + c=code_assignt(element, op[2]); c.add_source_location()=i_it->source_location; } else if(statement==patternt("?store")) @@ -1569,11 +1515,10 @@ codet java_bytecode_convert_methodt::convert_instructions( pointer_typet(java_type_from_char(type_char))); plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type()); + // tag it so it's easy to identify during instrumentation + data_plus_offset.set(ID_java_array_access, true); typet element_type=data_ptr.type().subtype(); dereference_exprt element(data_plus_offset, element_type); - - c=get_array_bounds_check(deref, op[1], i_it->source_location); - c.add_source_location()=i_it->source_location; results[0]=java_bytecode_promotion(element); } else if(statement==patternt("?load")) @@ -2136,14 +2081,6 @@ codet java_bytecode_convert_methodt::convert_instructions( java_new_array.add_source_location()=i_it->source_location; c=code_blockt(); - // TODO make this throw NegativeArrayIndexException instead. - constant_exprt intzero=from_integer(0, java_int_type()); - binary_relation_exprt gezero(op[0], ID_ge, intzero); - code_assertt check(gezero); - check.add_source_location().set_comment("Array size < 0"); - check.add_source_location() - .set_property_class("array-create-negative-size"); - c.move_to_operands(check); if(max_array_length!=0) { @@ -2175,15 +2112,7 @@ codet java_bytecode_convert_methodt::convert_instructions( if(!i_it->source_location.get_line().empty()) java_new_array.add_source_location()=i_it->source_location; - code_blockt checkandcreate; - // TODO make this throw NegativeArrayIndexException instead. - constant_exprt intzero=from_integer(0, java_int_type()); - binary_relation_exprt gezero(op[0], ID_ge, intzero); - code_assertt check(gezero); - check.add_source_location().set_comment("Array size < 0"); - check.add_source_location() - .set_property_class("array-create-negative-size"); - checkandcreate.move_to_operands(check); + code_blockt create; if(max_array_length!=0) { @@ -2191,11 +2120,12 @@ codet java_bytecode_convert_methodt::convert_instructions( from_integer(max_array_length, java_int_type()); binary_relation_exprt le_max_size(op[0], ID_le, size_limit); code_assumet assume_le_max_size(le_max_size); - checkandcreate.move_to_operands(assume_le_max_size); + create.move_to_operands(assume_le_max_size); } const exprt tmp=tmp_variable("newarray", ref_type); - c=code_assignt(tmp, java_new_array); + create.copy_to_operands(code_assignt(tmp, java_new_array)); + c=std::move(create); results[0]=tmp; } else if(statement=="arraylength") diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h index f44df98be49..85537034894 100644 --- a/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/src/java_bytecode/java_bytecode_convert_method_class.h @@ -123,11 +123,6 @@ class java_bytecode_convert_methodt:public messaget INST_INDEX_CONST=3 }; - codet get_array_bounds_check( - const exprt &arraystruct, - const exprt &idx, - const source_locationt &original_sloc); - // return corresponding reference of variable const variablet &find_variable_for_slot( size_t address, diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp new file mode 100644 index 00000000000..22072d9f823 --- /dev/null +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -0,0 +1,528 @@ +/*******************************************************************\ + +Module: Instrument codet with assertions/runtime exceptions + +Author: Cristina David + +Date: June 2017 + +\*******************************************************************/ + +#include +#include +#include +#include + +#include + +#include "java_bytecode_instrument.h" +#include "java_entry_point.h" +#include "java_object_factory.h" +#include "java_root_class.h" +#include "java_types.h" + +class java_bytecode_instrumentt +{ +public: + java_bytecode_instrumentt( + symbol_tablet &_symbol_table, + const bool _throw_runtime_exceptions, + const size_t _max_array_length): + symbol_table(_symbol_table), + throw_runtime_exceptions(_throw_runtime_exceptions), + max_array_length(_max_array_length) + { + } + + void operator()(exprt &expr); + +protected: + symbol_tablet &symbol_table; + bool throw_runtime_exceptions; + size_t max_array_length; + + codet throw_exception( + const exprt &cond, + const source_locationt &original_loc, + const irep_idt &exc_name); + + codet check_array_access( + const exprt &array_struct, + const exprt &idx, + const source_locationt &original_loc); + + codet check_null_dereference( + const exprt &expr, + const source_locationt &original_loc, + const bool assertion_enabled); + + codet check_class_cast( + const exprt &class1, + const exprt &class2, + const source_locationt &original_loc); + + codet check_array_length( + const exprt &length, + const source_locationt &original_loc); + + void instrument_code(exprt &expr); + codet instrument_expr(const exprt &expr); +}; + + +/// Creates a class stub for exc_name and generates a +/// conditional GOTO such that exc_name is thrown when +/// cond is met. +/// \par parameters: `cond`: condition to be met in order +/// to throw an exception +/// `original_loc`: source location in the original program +/// `exc_name`: the name of the exception to be thrown +/// \return Returns the code initialising the throwing the +/// exception +codet java_bytecode_instrumentt::throw_exception( + const exprt &cond, + const source_locationt &original_loc, + const irep_idt &exc_name) +{ + exprt exc; + code_blockt init_code; + const irep_idt &exc_obj_name= + id2string(goto_functionst::entry_point())+ + "::"+id2string(exc_name); + + if(!symbol_table.has_symbol(exc_obj_name)) + { + // for now, create a class stub + // TODO: model exceptions and use that model + class_typet class_type; + class_type.set_tag(exc_name); + class_type.set(ID_base_name, exc_name); + class_type.set(ID_incomplete_class, true); + + // produce class symbol + symbolt exc_symbol; + exc_symbol.base_name=exc_name; + exc_symbol.pretty_name=exc_name; + exc_symbol.name="java::"+id2string(exc_name); + class_type.set(ID_name, exc_symbol.name); + exc_symbol.type=class_type; + exc_symbol.mode=ID_java; + exc_symbol.is_type=true; + symbol_table.add(exc_symbol); + // create the class identifier + java_root_class(exc_symbol); + + // create the exception object + exc=object_factory( + pointer_typet(exc_symbol.type), + exc_name, + init_code, + false, + symbol_table, + max_array_length, + original_loc); + } + else + exc=symbol_table.lookup(exc_obj_name).symbol_expr(); + + side_effect_expr_throwt throw_expr; + throw_expr.add_source_location()=original_loc; + throw_expr.move_to_operands(exc); + + code_ifthenelset if_code; + if_code.add_source_location()=original_loc; + if_code.cond()=cond; + if_code.then_case()=code_expressiont(throw_expr); + + init_code.move_to_operands(if_code); + + return init_code; +} + +/// Checks whether the array access array_struct[idx] is out-of-bounds, +/// and throws ArrayIndexOutofBoundsException/generates an assertion +/// if necessary; Exceptions are thrown when the `throw_runtime_exceptions` +/// flag is set. Otherwise, assertions are emitted. +/// \par parameters: `array_struct`: the array being accessed +/// `idx`: index into the array +/// `original_loc: source location in the original code +/// \return Based on the value of the flag `throw_runtime_exceptions`, +/// it returns code that either throws an ArrayIndexOutPfBoundsException +/// or emits an assertion checking the array access +codet java_bytecode_instrumentt::check_array_access( + const exprt &array_struct, + const exprt &idx, + const source_locationt &original_loc) +{ + const constant_exprt &zero=from_integer(0, java_int_type()); + const binary_relation_exprt ge_zero(idx, ID_ge, zero); + const member_exprt length_field(array_struct, "length", java_int_type()); + const binary_relation_exprt lt_length(idx, ID_lt, length_field); + const and_exprt cond(ge_zero, lt_length); + + if(throw_runtime_exceptions) + return throw_exception( + not_exprt(cond), + original_loc, + "java.lang.ArrayIndexOutOfBoundsException"); + + code_blockt bounds_checks; + bounds_checks.add(code_assertt(ge_zero)); + bounds_checks.operands().back().add_source_location()=original_loc; + bounds_checks.operands().back().add_source_location() + .set_comment("Array index should be >= 0"); + bounds_checks.operands().back().add_source_location() + .set_property_class("array-index-out-of-bounds-low"); + + bounds_checks.add(code_assertt(lt_length)); + bounds_checks.operands().back().add_source_location()=original_loc; + bounds_checks.operands().back().add_source_location() + .set_comment("Array index should be < length"); + bounds_checks.operands().back().add_source_location() + .set_property_class("array-index-out-of-bounds-high"); + + return bounds_checks; +} + +/// Checks whether `class1` is an instance of `class2` and throws +/// ClassCastException/generates an assertion when necessary; +/// Exceptions are thrown when the `throw_runtime_exceptions` flag is set. +/// Otherwise, assertions are emitted. +/// \par parameters: `class1`: the subclass +/// `class2`: the super class +/// `original_loc: source location in the original code +/// \return Based on the value of the flag `throw_runtime_exceptions`, +/// it returns code that either throws an ClassCastException or emits an +/// assertion checking the subtype relation +codet java_bytecode_instrumentt::check_class_cast( + const exprt &class1, + const exprt &class2, + const source_locationt &original_loc) +{ + binary_predicate_exprt class_cast_check( + class1, ID_java_instanceof, class2); + + empty_typet voidt; + pointer_typet voidptr(voidt); + exprt null_check_op=class1; + if(null_check_op.type()!=voidptr) + null_check_op.make_typecast(voidptr); + notequal_exprt op_not_null(null_check_op, null_pointer_exprt(voidptr)); + + // checkcast passes when the operand is null + and_exprt and_expr(op_not_null, not_exprt(class_cast_check)); + + if(throw_runtime_exceptions) + return throw_exception( + and_expr, + original_loc, + "ClassCastException"); + + code_assertt assert_class(class_cast_check); + assert_class.add_source_location(). + set_comment("Dynamic cast check"); + assert_class.add_source_location(). + set_property_class("bad-dynamic-cast"); + + code_ifthenelset conditional_check; + conditional_check.cond()=std::move(op_not_null); + conditional_check.then_case()=std::move(assert_class); + return conditional_check; +} + +/// Checks whether `expr` is null and throws NullPointerException/ +/// generates an assertion when necessary; +/// Exceptions are thrown when the `throw_runtime_exceptions` flag is set. +/// Otherwise, assertions are emitted. +/// \par parameters: `expr`: the checked expression +/// `original_loc: source location in the original code +/// \return Based on the value of the flag `throw_runtime_exceptions`, +/// it returns code that either throws an NullPointerException or emits an +/// assertion checking the subtype relation +codet java_bytecode_instrumentt::check_null_dereference( + const exprt &expr, + const source_locationt &original_loc, + const bool assertion_enabled) +{ + exprt local_expr=expr; + empty_typet voidt; + pointer_typet voidptr(voidt); + + if(local_expr.type()!=voidptr) + local_expr.make_typecast(voidptr); + + const equal_exprt equal_expr( + local_expr, + null_pointer_exprt(voidptr)); + + if(throw_runtime_exceptions) + return throw_exception( + equal_expr, + original_loc, "java.lang.NullPointerException"); + + if(assertion_enabled) + { + code_assertt check((not_exprt(equal_expr))); + check.add_source_location() + .set_comment("Throw null"); + check.add_source_location() + .set_property_class("null-pointer-exception"); + return check; + } + + return code_skipt(); +} + +/// Checks whether `length`>=0 and throws NegativeArraySizeException/ +/// generates an assertion when necessary; +/// Exceptions are thrown when the `throw_runtime_exceptions` flag is set. +/// Otherwise, assertions are emitted. +/// \par parameters: `length`: the checked length +/// `original_loc: source location in the original code +/// \return Based on the value of the flag `throw_runtime_exceptions`, +/// it returns code that either throws an NegativeArraySizeException +/// or emits an assertion checking the subtype relation +codet java_bytecode_instrumentt::check_array_length( + const exprt &length, + const source_locationt &original_loc) +{ + const constant_exprt &zero=from_integer(0, java_int_type()); + const binary_relation_exprt ge_zero(length, ID_ge, zero); + + if(throw_runtime_exceptions) + return throw_exception( + not_exprt(ge_zero), + original_loc, + "java.lang.NegativeArraySizeException"); + + code_assertt check(ge_zero); + check.add_source_location().set_comment("Array size should be >= 0"); + check.add_source_location() + .set_property_class("array-create-negative-size"); + return check; +} + +/// Augments `expr` with instrumentation in the form of either +/// assertions or runtime exceptions +/// \par parameters: `expr`: the expression to be instrumented +void java_bytecode_instrumentt::instrument_code(exprt &expr) +{ + codet &code=to_code(expr); + + const irep_idt &statement=code.get_statement(); + + if(statement==ID_assign) + { + code_assignt code_assign=to_code_assign(code); + + code_blockt block; + block.copy_to_operands(instrument_expr(code_assign.lhs())); + block.copy_to_operands(instrument_expr(code_assign.rhs())); + block.copy_to_operands(code_assign); + + code=block; + } + else if(statement==ID_expression) + { + code_expressiont code_expression= + to_code_expression(code); + + code_blockt block; + block.copy_to_operands( + instrument_expr(code_expression.expression())); + block.copy_to_operands(code_expression); + code=block; + } + else if(statement==ID_assert) + { + code_assertt code_assert=to_code_assert(code); + + // does this correspond to checkcast? + if(code_assert.assertion().id()==ID_java_instanceof) + { + code_blockt block; + + INVARIANT( + code_assert.assertion().operands().size()==2, + "Instanceof should have 2 operands"); + + block.copy_to_operands( + check_class_cast( + code_assert.assertion().op0(), + code_assert.assertion().op1(), + code_assert.source_location())); + block.copy_to_operands(code_assert); + code=block; + } + } + else if(statement==ID_block) + { + Forall_operands(it, code) + instrument_code(to_code(*it)); + } + else if(statement==ID_label) + { + code_labelt &code_label=to_code_label(code); + instrument_code(code_label.code()); + } + else if(statement==ID_ifthenelse) + { + code_blockt block; + code_ifthenelset &code_ifthenelse=to_code_ifthenelse(code); + block.copy_to_operands(instrument_expr(code_ifthenelse.cond())); + instrument_code(code_ifthenelse.then_case()); + if(code_ifthenelse.else_case().is_not_nil()) + instrument_code(code_ifthenelse.else_case()); + block.copy_to_operands(code); + code=block; + } + else if(statement==ID_switch) + { + code_blockt block; + code_switcht &code_switch=to_code_switch(code); + block.copy_to_operands( + instrument_expr(code_switch.value())); + block.copy_to_operands( + instrument_expr(code_switch.body())); + block.copy_to_operands(code); + code=block; + } + else if(statement==ID_return) + { + if(code.operands().size()==1) + { + code_blockt block; + block.copy_to_operands(instrument_expr(code.op0())); + block.copy_to_operands(code); + code=block; + } + } + else if(statement==ID_function_call) + { + code_blockt block; + code_function_callt &code_function_call=to_code_function_call(code); + block.copy_to_operands(instrument_expr(code_function_call.lhs())); + block.copy_to_operands(instrument_expr(code_function_call.function())); + + for(code_function_callt::argumentst::iterator + a_it=code_function_call.arguments().begin(); + a_it!=code_function_call.arguments().end(); + a_it++) + block.copy_to_operands(instrument_expr(*a_it)); + + block.copy_to_operands(code); + code=block; + } +} + +/// Computes the instrumentation for `expr` in the form of +/// either assertions or runtime exceptions. +/// \par parameters: `expr`: the expression for which we compute +/// instrumentation +/// \return: The instrumentation required for `expr` +codet java_bytecode_instrumentt::instrument_expr( + const exprt &expr) +{ + if(expr.id()==ID_plus && + expr.get_bool(ID_java_array_access)) + { + // this corresponds to ?aload and ?astore so + // we check that 0<=index=0 + return check_array_length( + expr.op0(), + expr.source_location()); + } + else if(expr.id()==ID_member && + expr.get_bool(ID_java_member_access)) + { + // this corresponds to either getfield or putfield + // so we must check null pointer dereference + const member_exprt &member_expr=to_member_expr(expr); + if(member_expr.op0().id()==ID_dereference) + { + const dereference_exprt dereference_expr= + to_dereference_expr(member_expr.op0()); + codet null_dereference_check= + check_null_dereference( + dereference_expr.op0(), + dereference_expr.source_location(), + false); + return null_dereference_check; + } + } + + if(!expr.has_operands()) + return code_skipt(); + + code_blockt block; + forall_operands(it, expr) + { + block.copy_to_operands(instrument_expr(*it)); + } + return block; +} + +/// Instruments `expr` +/// \par parameters: `expr`: the expression to be instrumented +void java_bytecode_instrumentt::operator()(exprt &expr) +{ + instrument_code(expr); +} + +/// Instruments all the code in the symbol_table with +/// runtime exceptions or corresponding assertions. +/// Exceptions are thrown when the `throw_runtime_exceptions` flag is set. +/// Otherwise, assertions are emitted. +/// \par parameters: `symbol_table`: the symbol table to instrument +/// `throw_runtime_exceptions`: flag determining whether we instrument the code +/// with runtime exceptions or with assertions. The former applies if this flag +/// is set to true. +/// `max_array_length`: maximum array length; the only reason we need this is +/// in order to be able to call the object factory to create exceptions. +void java_bytecode_instrument( + symbol_tablet &symbol_table, + bool throw_runtime_exceptions, + size_t max_array_length) +{ + java_bytecode_instrumentt instrument( + symbol_table, + throw_runtime_exceptions, + max_array_length); + + Forall_symbols(s_it, symbol_table.symbols) + { + if(s_it->second.value.id()==ID_code) + instrument(s_it->second.value); + } +} diff --git a/src/java_bytecode/java_bytecode_instrument.h b/src/java_bytecode/java_bytecode_instrument.h new file mode 100644 index 00000000000..e382da7e7bd --- /dev/null +++ b/src/java_bytecode/java_bytecode_instrument.h @@ -0,0 +1,19 @@ +/*******************************************************************\ + +Module: Instrument codet with assertions/runtime exceptions + +Author: Cristina David + +Date: June 2017 + +\*******************************************************************/ + +#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INSTRUMENT_H +#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INSTRUMENT_H + +void java_bytecode_instrument( + symbol_tablet &symbol_table, + const bool throw_runtime_exceptions, + const size_t max_array_length); + +#endif diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index e024653bef7..3b1c2ba7dcf 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_bytecode_convert_class.h" #include "java_bytecode_convert_method.h" #include "java_bytecode_internal_additions.h" +#include "java_bytecode_instrument.h" #include "java_bytecode_typecheck.h" #include "java_entry_point.h" #include "java_bytecode_parser.h" @@ -36,6 +37,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) { assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null"); string_refinement_enabled=cmd.isset("refine-strings"); + throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions"); if(cmd.isset("java-max-input-array-length")) max_nondet_array_length= std::stoi(cmd.get_value("java-max-input-array-length")); @@ -438,6 +440,12 @@ bool java_bytecode_languaget::typecheck( } // Otherwise our caller is in charge of elaborating methods on demand. + // now instrument runtime exceptions + java_bytecode_instrument( + symbol_table, + throw_runtime_exceptions, + max_nondet_array_length); + // now typecheck all if(java_bytecode_typecheck( symbol_table, get_message_handler(), string_refinement_enabled)) diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index c107ffd0267..d0c9c0ba0f7 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -103,6 +103,7 @@ class java_bytecode_languaget:public languaget lazy_methodst lazy_methods; lazy_methods_modet lazy_methods_mode; bool string_refinement_enabled; + bool throw_runtime_exceptions; java_string_library_preprocesst string_preprocess; std::string java_cp_include_files; }; diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 8a22f226fc0..e24d7cd981f 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -815,6 +815,8 @@ IREP_ID_ONE(skip_initialize) IREP_ID_ONE(basic_block_covered_lines) IREP_ID_ONE(is_nondet_nullable) IREP_ID_ONE(array_replace) +IREP_ID_ONE(java_array_access) +IREP_ID_ONE(java_member_access) #undef IREP_ID_ONE #undef IREP_ID_TWO From a6d1084e3d5d46721acad20c56ae738baab1ffe4 Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 29 Jun 2017 14:10:58 +0100 Subject: [PATCH 3/4] Move generate_class_stub out of java_bytecode_convert_classt and to java_utils.cpp and use it to generate stubs for exceptions --- src/java_bytecode/Makefile | 2 +- .../java_bytecode_convert_class.cpp | 41 +++-------------- .../java_bytecode_instrument.cpp | 42 ++++++++--------- src/java_bytecode/java_bytecode_instrument.h | 2 +- src/java_bytecode/java_bytecode_language.cpp | 1 + src/java_bytecode/java_utils.cpp | 45 ++++++++++++++++++- src/java_bytecode/java_utils.h | 6 +++ 7 files changed, 75 insertions(+), 64 deletions(-) diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index 522218dc4f4..5125f2f6664 100644 --- a/src/java_bytecode/Makefile +++ b/src/java_bytecode/Makefile @@ -5,6 +5,7 @@ SRC = bytecode_info.cpp \ jar_file.cpp \ java_bytecode_convert_class.cpp \ java_bytecode_convert_method.cpp \ + java_bytecode_instrument.cpp \ java_bytecode_internal_additions.cpp \ java_bytecode_language.cpp \ java_bytecode_parse_tree.cpp \ @@ -16,7 +17,6 @@ SRC = bytecode_info.cpp \ java_class_loader.cpp \ java_class_loader_limit.cpp \ java_entry_point.cpp \ - java_bytecode_instrument.cpp \ java_local_variable_table.cpp \ java_object_factory.cpp \ java_pointer_casts.cpp \ diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index ada2468e924..9b6d53841e3 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_types.h" #include "java_bytecode_convert_method.h" #include "java_bytecode_language.h" +#include "java_utils.h" #include #include @@ -56,7 +57,10 @@ class java_bytecode_convert_classt:public messaget string_preprocess.add_string_type( parse_tree.parsed_class.name, symbol_table); else if(!loading_success) - generate_class_stub(parse_tree.parsed_class.name); + generate_class_stub( + parse_tree.parsed_class.name, + symbol_table, + get_message_handler()); } typedef java_bytecode_parse_treet::classt classt; @@ -73,7 +77,6 @@ class java_bytecode_convert_classt:public messaget void convert(const classt &c); void convert(symbolt &class_symbol, const fieldt &f); - void generate_class_stub(const irep_idt &class_name); void add_array_types(); }; @@ -171,40 +174,6 @@ void java_bytecode_convert_classt::convert(const classt &c) java_root_class(*class_symbol); } -void java_bytecode_convert_classt::generate_class_stub( - const irep_idt &class_name) -{ - class_typet class_type; - - class_type.set_tag(class_name); - class_type.set(ID_base_name, class_name); - - class_type.set(ID_incomplete_class, true); - - // produce class symbol - symbolt new_symbol; - new_symbol.base_name=class_name; - new_symbol.pretty_name=class_name; - new_symbol.name="java::"+id2string(class_name); - class_type.set(ID_name, new_symbol.name); - new_symbol.type=class_type; - new_symbol.mode=ID_java; - new_symbol.is_type=true; - - symbolt *class_symbol; - - if(symbol_table.move(new_symbol, class_symbol)) - { - warning() << "stub class symbol " << new_symbol.name - << " already exists" << eom; - } - else - { - // create the class identifier etc - java_root_class(*class_symbol); - } -} - void java_bytecode_convert_classt::convert( symbolt &class_symbol, const fieldt &f) diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index 22072d9f823..9ec9f3293b2 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -15,21 +15,25 @@ Date: June 2017 #include +#include "java_bytecode_convert_class.h" #include "java_bytecode_instrument.h" #include "java_entry_point.h" #include "java_object_factory.h" #include "java_root_class.h" #include "java_types.h" +#include "java_utils.h" -class java_bytecode_instrumentt +class java_bytecode_instrumentt:public messaget { public: java_bytecode_instrumentt( symbol_tablet &_symbol_table, const bool _throw_runtime_exceptions, + message_handlert &_message_handler, const size_t _max_array_length): symbol_table(_symbol_table), throw_runtime_exceptions(_throw_runtime_exceptions), + message_handler(_message_handler), max_array_length(_max_array_length) { } @@ -38,8 +42,9 @@ class java_bytecode_instrumentt protected: symbol_tablet &symbol_table; - bool throw_runtime_exceptions; - size_t max_array_length; + const bool throw_runtime_exceptions; + message_handlert &message_handler; + const size_t max_array_length; codet throw_exception( const exprt &cond, @@ -92,25 +97,12 @@ codet java_bytecode_instrumentt::throw_exception( if(!symbol_table.has_symbol(exc_obj_name)) { - // for now, create a class stub - // TODO: model exceptions and use that model - class_typet class_type; - class_type.set_tag(exc_name); - class_type.set(ID_base_name, exc_name); - class_type.set(ID_incomplete_class, true); - - // produce class symbol - symbolt exc_symbol; - exc_symbol.base_name=exc_name; - exc_symbol.pretty_name=exc_name; - exc_symbol.name="java::"+id2string(exc_name); - class_type.set(ID_name, exc_symbol.name); - exc_symbol.type=class_type; - exc_symbol.mode=ID_java; - exc_symbol.is_type=true; - symbol_table.add(exc_symbol); - // create the class identifier - java_root_class(exc_symbol); + generate_class_stub( + exc_name, + symbol_table, + get_message_handler()); + const symbolt &exc_symbol=symbol_table.lookup( + "java::"+id2string(exc_name)); // create the exception object exc=object_factory( @@ -512,12 +504,14 @@ void java_bytecode_instrumentt::operator()(exprt &expr) /// in order to be able to call the object factory to create exceptions. void java_bytecode_instrument( symbol_tablet &symbol_table, - bool throw_runtime_exceptions, - size_t max_array_length) + const bool throw_runtime_exceptions, + message_handlert &message_handler, + const size_t max_array_length) { java_bytecode_instrumentt instrument( symbol_table, throw_runtime_exceptions, + message_handler, max_array_length); Forall_symbols(s_it, symbol_table.symbols) diff --git a/src/java_bytecode/java_bytecode_instrument.h b/src/java_bytecode/java_bytecode_instrument.h index e382da7e7bd..0d987746bce 100644 --- a/src/java_bytecode/java_bytecode_instrument.h +++ b/src/java_bytecode/java_bytecode_instrument.h @@ -14,6 +14,6 @@ Date: June 2017 void java_bytecode_instrument( symbol_tablet &symbol_table, const bool throw_runtime_exceptions, + message_handlert &_message_handler, const size_t max_array_length); - #endif diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 3b1c2ba7dcf..297484ad82d 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -444,6 +444,7 @@ bool java_bytecode_languaget::typecheck( java_bytecode_instrument( symbol_table, throw_runtime_exceptions, + get_message_handler(), max_nondet_array_length); // now typecheck all diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index 9f8be11e4ad..5643d819a28 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -6,12 +6,13 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ - +#include +#include #include #include -#include #include +#include "java_root_class.h" #include "java_utils.h" #include "java_types.h" @@ -54,7 +55,47 @@ unsigned java_method_parameter_slots(const code_typet &t) return slots; } + const std::string java_class_to_package(const std::string &canonical_classname) { return trim_from_last_delimiter(canonical_classname, '.'); } + +void generate_class_stub( + const irep_idt &class_name, + symbol_tablet &symbol_table, + message_handlert &message_handler) +{ + class_typet class_type; + + class_type.set_tag(class_name); + class_type.set(ID_base_name, class_name); + + class_type.set(ID_incomplete_class, true); + + // produce class symbol + symbolt new_symbol; + new_symbol.base_name=class_name; + new_symbol.pretty_name=class_name; + new_symbol.name="java::"+id2string(class_name); + class_type.set(ID_name, new_symbol.name); + new_symbol.type=class_type; + new_symbol.mode=ID_java; + new_symbol.is_type=true; + + symbolt *class_symbol; + + if(symbol_table.move(new_symbol, class_symbol)) + { + messaget message(message_handler); + message.warning() << + "stub class symbol " << + new_symbol.name << + " already exists" << messaget::eom; + } + else + { + // create the class identifier etc + java_root_class(*class_symbol); + } +} diff --git a/src/java_bytecode/java_utils.h b/src/java_bytecode/java_utils.h index ef64ff9e18e..77cb35825b0 100644 --- a/src/java_bytecode/java_utils.h +++ b/src/java_bytecode/java_utils.h @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include "java_bytecode_parse_tree.h" @@ -16,6 +17,11 @@ Author: Daniel Kroening, kroening@kroening.com bool java_is_array_type(const typet &type); +void generate_class_stub( + const irep_idt &class_name, + symbol_tablet &symbol_table, + message_handlert &message_handler); + /// Returns the number of JVM local variables (slots) taken by a local variable /// that, when translated to goto, has type \p t. unsigned java_local_variable_slots(const typet &t); From 236e44231a1e0f2b3e64425bdace6d90c9154cd1 Mon Sep 17 00:00:00 2001 From: Cristina Date: Sun, 2 Jul 2017 17:09:36 +0100 Subject: [PATCH 4/4] Adjusted runtime exceptions regression tests --- .../cbmc-java/NullPointerException2/Test.class | Bin 825 -> 825 bytes .../cbmc-java/NullPointerException2/test.desc | 2 +- .../cbmc-java/NullPointerException3/Test.class | Bin 835 -> 835 bytes .../cbmc-java/NullPointerException3/test.desc | 2 +- 4 files changed, 2 insertions(+), 2 deletions(-) diff --git a/regression/cbmc-java/NullPointerException2/Test.class b/regression/cbmc-java/NullPointerException2/Test.class index 2644933a3a0cc875e9ea948ff2ebbc00121649f5..e49a2d70d61d80ae510fd2c7c04b3461001cf46e 100644 GIT binary patch delta 25 fcmdnVwv%ncLMC2527U$sAQWVfV-TLaj;R{}N$&+L delta 25 fcmdnVwv%ncLMC1w27U%U1_2-`#~?U)9aA>|NtXpA diff --git a/regression/cbmc-java/NullPointerException2/test.desc b/regression/cbmc-java/NullPointerException2/test.desc index 79cac6a9e9b..ed7e923ae16 100644 --- a/regression/cbmc-java/NullPointerException2/test.desc +++ b/regression/cbmc-java/NullPointerException2/test.desc @@ -3,7 +3,7 @@ Test.class --java-throw-runtime-exceptions ^EXIT=10$ ^SIGNAL=0$ -^.*assertion at file Test.java line 15 function.*: FAILURE$ +^.*assertion at file Test.java line 17 function.*: FAILURE$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc-java/NullPointerException3/Test.class b/regression/cbmc-java/NullPointerException3/Test.class index cd8ba9d445765df26cec3cd8ac74d3e3317cd1b5..77c124a4b869c9928a2fcd98c00f3c6e75d7bc1a 100644 GIT binary patch delta 25 fcmX@ic9?C$LMC2527U$sAQWVfV-TLaj%g|YOW6fV delta 25 fcmX@ic9?C$LMC1w27U%U1_2-`#~?U)9n(|*OMwMK diff --git a/regression/cbmc-java/NullPointerException3/test.desc b/regression/cbmc-java/NullPointerException3/test.desc index 79cac6a9e9b..ed7e923ae16 100644 --- a/regression/cbmc-java/NullPointerException3/test.desc +++ b/regression/cbmc-java/NullPointerException3/test.desc @@ -3,7 +3,7 @@ Test.class --java-throw-runtime-exceptions ^EXIT=10$ ^SIGNAL=0$ -^.*assertion at file Test.java line 15 function.*: FAILURE$ +^.*assertion at file Test.java line 17 function.*: FAILURE$ ^VERIFICATION FAILED$ -- ^warning: ignoring