From e976d6f92d28ef1756d8326d4c72224f3efc969f Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 5 Feb 2018 17:11:29 +0000 Subject: [PATCH 1/4] Correctly handle wide iload commands These commands occur when there are >255 local variables. In these cases the index of the local variable is represented using a u2 rather than a u1. --- src/java_bytecode/java_bytecode_parser.cpp | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index edb251a0fa9..58bfc4f09b5 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -749,7 +749,6 @@ void java_bytecode_parsert::rbytecode( instruction.args.push_back(from_integer(c, signedbv_typet(8))); } address+=1; - break; case 'o': // two byte branch offset, signed @@ -776,10 +775,20 @@ void java_bytecode_parsert::rbytecode( case 'v': // local variable index (one byte) { - u1 v=read_u1(); - instruction.args.push_back(from_integer(v, unsignedbv_typet(8))); + if(wide_instruction) + { + u2 v = read_u2(); + instruction.args.push_back(from_integer(v, unsignedbv_typet(16))); + address += 2; + } + else + { + u1 v = read_u1(); + instruction.args.push_back(from_integer(v, unsignedbv_typet(8))); + address += 1; + } } - address+=1; + break; case 'V': From 5bdaa6418250e3d4f682a09097864e1f53bebe16 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 5 Feb 2018 17:46:17 +0000 Subject: [PATCH 2/4] Adding test demonstrating the too many variables problem --- .../TooManyLocals.class | Bin 0 -> 9993 bytes .../TooManyLocals.java | 518 ++++++++++++++++++ .../lots_of_local_variables/test.desc | 6 + 3 files changed, 524 insertions(+) create mode 100644 regression/cbmc-java/lots_of_local_variables/TooManyLocals.class create mode 100644 regression/cbmc-java/lots_of_local_variables/TooManyLocals.java create mode 100644 regression/cbmc-java/lots_of_local_variables/test.desc diff --git a/regression/cbmc-java/lots_of_local_variables/TooManyLocals.class b/regression/cbmc-java/lots_of_local_variables/TooManyLocals.class new file mode 100644 index 0000000000000000000000000000000000000000..b72240605da9ed95e51ee6bc79d5df9131031bb9 GIT binary patch literal 9993 zcmd^kg?|;-xBcETbH@^32G|rSR-lEnK$#>bNedKrcZUE0f=fbyBBi(%cXu!DUZA+U zyR^7_fBVe5@9%xy`xhR3K5MOWbJxCeV14eaGdcKq^L7A;!kji3n9+g|W-{=NI!Z9;PdtcRc%Ol+T+R2V_cou?LpR=h*= z1cX!-65A(KN^aLQp>qxSW`xugIy8%KTPwbEqFn#ii&|2v#4hsPH9B;t7~j6T|DG;C z@|dKAE=dSReA~8V+b8i`l=@{E62IpU^+f@>@+3q`h>{R3K}d*^5Gx^$FD$VD+Zfry z$RMJYdn0{sr03bu6ZAE zGPw$-$ehVlFhwR!u7W8tYrK+SlN3ymag(cHiVU1w1yf|?m?DEISHTn+O}PrD$Z*P4Fh$0b zS2CZHf+;egaurOG8I`MGicG0o1yf{Bc_o7?DVQRoDp$c28CJOprpUO;RWL;cR<436 zGP1mqnUxewk*SrdV2aGGTm@5Pa^)(R5@gp4vg-xe^@8krL3X_$yIzo8FUYPJWY-I_ z>jl~Mg6w)hcD*3GUXWcc$gUS;*9)@i1=;n2?0P|Vy&$_@kX!*AiG|WT`$P47i8B9vg-xe^@8krL3X_$yIzo8FUYPJWY-I_>jl~Mg6w)hcD*3G zUXWcc$gUS;*9)@i1=;n2?0P|Vy&$_@kX@1JWRv1)H_~ zuiK(sy+d;6W(lPd{hQ$bxX+2NNuW^zw!LZR6Xw%wP0Bx7(7PJ9p^J zAM!t(24)Y(uP_IK^WT=rO)6=OKB@-riIC}IQPDi#W)VATB=RY=J?Ja_}70*6-?xc@O{ zsmE1<&0*R?k-|wKQaUL` zDkqh297nj0D^feDMH(lKNb95(X1V5$QyVC?`rpJJCWoLc};RBG!o&aZa50!TCY_ z==>-OIt4``r;sS@6c#@@KZznv5mD4BDvCM9L~*CMDB+Y4C7qI@lv7HSc1nvfP8m_w zDJ#l3yr|$*5EY$@qLNcdRCX$hDozzq)u}3~In_jUr@E-&)DShDnxd9dOVoC1 zi#kpnQP-&}>N)j9eW$)?;4}~oora>3(?~RS8jB`Q6A|yki>6Lf(adQknmf%!f|DRx zI4wj=r=@7+v=WIB30y zy9>XIQ7()Uqg@y+#<(y>jCEnG80W$`G2VsoVuA}3#6%Y+ib*a^5|dq+ET*_HMND;J zs+i`&G%?+U>0*WpGsH|6W{O!Z%o4L*m@VeGFh|UFVXm0x!aOnGh52HE3k$?T7Z!>| zE-Vs@U05uZxUfVlbz!Mk=E5?u+=b<0g$pahA1?eMR=TiKta4$MSna}UvBrfpVyz2n z#X1+(iS;h57aLsIAU3+NQEYNyli2LSX0gSEEn=$+Tg5gPwu$X7Y!^FR*dcbhuv6@E zVVBtL!fx@W3xA3|F6)$4!dwz9C6`@ zIO@Vtam%v`e z&xL#9z6l!`GGIgAduj4q{SOigJR(@QBEe} z%W}RXzAz^F*oI5 z%tH~35%ewNxAYz3ca)bgFXdy*NBJ4^)Ax+uQvt>T!NMu?kgXtV-1wt5J2v z>QsZV2GwM&NwpYjQEkTBREMz+)n%+p^%(0>ea8CKfUyBJWNb){7#mSz#>Uiyu?fX9 z##2+qrqqnF88v5YP6><&)Pk`EwPb8btr%NTB4Z-8W^7Gu7~4==#5+ zJ5Wc)j?{^<6Ln_nOkEheP!eMjB{L>dSH`aNGvm+Hjj`i?b`_QkIBlw$_`bz3cze)Oy`bp|X{U!CM0g?vLKuH5>kfcF0Skhn`B54Q> zl{A!wNg77OB@L$$l19)-Nh9fZNx#!5Nuy}Aq|r1+(ij>mX)KMCG>*ng8c!1>O`wUA zCekEHlW4M}$uvdM6q+h&Dov9#jiyVQPBSFUpqY|p(kw}{Xtt!;G)K}Lnk#88&66~b z=1ZDS3nVR|g_0K1B1wyAv82VcMA8ykDrqS#leCPMOIl7VB(0!7B>h1vC9R}Yl2*}b zNvmm%q&2iw(pp+4X&tSXw4OFd+CUp6ZKO?-HqmBDn`w)rEwokAR@x?M8*P`gopwmt zK|3Ywq+ODB(QZk*=}$?2(jG~BXs@Kbv`^AL`b*MZv|rMGIw0u)9h7vC4oNyhhb0}R zBa)8LQAtPXn51KLT+(qmA?XC2lys6#NjgQRC7q@-lFrasNoVPtq;qs$(s{Zd=>lDp zbdfGexHU8XCNuFzFUSLvFhYjj=Gb-E$x2Hli&lWs}6MYkp0raO}E&|OJ)>7Jx} zbYIeadLZcm{VnNl`bW|~^ia}6dL-!)J(l#Co=AE^PbEF2XOf=Lb4kzXg`^ksQqoI$ zCFvEtmh_t5NP0tWCB3D0lHSpKN$=@{q!08_(ntCv=@WgH^qKyZ^zR-*sJt4KDUeYv z^F^rnnlR6Vuq~k0-2mDS*``(5rp=U!$~wfYTIUjOaQ!y9Ra@MsZAi^+ns}9g-7dP!Z;6h&hX#q$B(U2D6_+5n{9TbHxpd_S+vh1h`8KEjD<}c)_^LlaDLyZh#t@W23(8^&D2FbTM}i8-yTQy*3A00G%mr02 z4^+jxPz?(}b&Q4@7zZ`65Y)n=P#a4^9V`oVu_DyNs!$(mLIbP|4Y46K!gy$m3D5)+ zAs*X7Q|tuIFd3R-cSyiq&;t8HOB?{La0n#g2xyI?p$(3Qwm2Eu;dE$^v!MgdhmN=y zI^lBYjH{pvu7f1p1j)D!y5cVQ8TUdrJOJJC2=u@c@C%-So_GOz;T7nOH=qyRfnV_f z^utI~ahUV4$MFAjN>eN;nKr_?uTr2g8(1FkHz7Ba~b)Qi*`ymHaSD ziGtBe9E?#4!&s#_j8n?Mc%>ptP^!U1r8Z1b8o*>F9;PTQV5-svrYRj^x{?etlpZis z=>xNr{xDk^0&|p+FjpB1^OQ+2UzrXIlsT|aSqO`iWw2OT1xu9muvFOs%aon4T-ggN zl!Nexatu}~r(uTCE%{QwU&fJa&g9&0u{(Ne)vEiF9LGQe{!3%t;Bz)LMRywdW*Yt4fcUL7_QC26xsqzsV&1)+G=#Pjp%CIF}1b_(`W}Vt#%wqJB#VG%lL(M6Vq$= zF@yFPGiom}llC6J3;|{i>6j%Hj#)#gFWyBgKSqXzVpM1pMu#S# z2u;J7&>V~nEyB3a3j86o7Jm$F#)6@pSSYj)3x^KlPoa}oBy=8&hOT0<&}}Rp`Ws7x zo?^++Yb+J|h^2J}%jhPS)l*_QJuQ~kGhzij8&=f6#!C8kSXuY5iXMwq^}<+9FM-wd za#%yJf;IJ8SW9n!we_Z0M{k97_4Zg#Pr~|o4{V_SiVgLF*hn9ajrB3uM4yE5`V4HU z&%q5v7LSw+v^XpgZ>;l>Tj`= z{uw(P8g?;kOfnoyHqv2N<4gS6_zJrjxv{&E4|^C<_>1ua_B4uMFQXLpHY#8rqZBa9U|(pZPT z8(VRd@h6Tp4&oT&1dcV%<2d6QjyLY&1mh7-G+yE);{#4M6`W#PIMsA;n)wAzH?!aj zGZ)S@zr$H(B+fQ}z&U17oNJcBd1hstZ`Q&EWXV}-N9?tL%eRiz#G7yl;Pt z4{Q(rw&U<0y9hqCOXDNE5#kryBof=``{~kAilOo;2V1! zzO|>~J9`ekw-@6FdnJCfH{d6GJAStJ;=lG`1?*D_+7}hYzM-i0eMPgMC?Wf;qK6TG z`}0#ZJDl%?dYHp^_%z%N%&?Svk0*Z8X7lsHbgUEz53~7RPuw9=g&BOuC(s~un8x>g z;x0j9$ajC@Mv=k(#2tXRS7f%|aT6eJ7uoGs+y{s|MlSmqw*um(k;i_--GI1n$ zgu4Xs^;fhHaHAmJK~;M%_X^^_HSJy8E{OM1*WSh*gLp3u?M>V?i1!k2uj9T!yq5%f z6}JxJy(HSpxqA@rrJcQ)8wl}UI@$BNhY;^2*`Cd9gm^FA?djY}i1*UVp3KdJcrShJ z@!U^{_cFj9%`Js^FGK7R+*OG8GQu9hjfHqGqwN8Hlgb6-?Y`Vzi1#wt?!_I3crVlK z?%ZUE_cGf~<~~Ebm-%)lZZ*VvS!}oCZbQ76<#r-B9OAvKvJ<%H5btH39nWotcrTmm zhTM6G_p;5d%gu*)FT3oT+<%Dove&K(rC51zz^(|TSw+GTyDXGp6$K~klHBZw_j1NA z3guV{xL_B8@~mRuiX8_PSjEB(JDS@c@m}uO1)vhEAK-zV7b>&*5gyrjpbD#k@XXG| z4N*47S9W%&#;P#9vok|=RzJZfI|I~URRq!I|1nlYF=V??i&ZhS>=aO&RdGyVTTq8p z33TlcH%)?)NH#(}R;4h5^$F^;Dvg<~chG=U8O(0I;x#{0L@ud!J^g~Zneanu%vYYTCl2y zWvwI7l2vuAXdQr7tZHCYYcDrn-V4^Wc0p@awXm+W4cf4(jSa0$(3VvljJMWtJ0|Xs z3DzoT&#E3KTFapWtNPf^S_~aoHNZ~Rd~VRh-7?vl4V_sv!tT~|=)$To_Od2J600WI z*BZ|)o49ihutq~yR!wn;H3EKS)eJ{iL!cY0<~Z6Kz)hUEi;lPYLJw9gaI)14eqq%T zr(4~jC#zOC+e+rPPTW!FTb-actJb*KY6pE-wZY|9BK*p#Ev~W>xX}}L*L7Ar{Kl$1 zZn7FeKUN)Zn^hP3v+Bs-#WlJ06L;FZR#h0tsxyE8R)j&Uy6`t|Ss2VJiNAA8^2va> z>z=WS!cbOS`Fpky3}f{(f5XPXa8}*;yEU3m55yh#j#U6gvg&~kti13$t6%Vul?O(# z>WR;+TztYH?#8dI>@bE^Z+vHEhOw;r;3q2sjAQkyqF8D96hhEfF|1TDfz@wHxMjmc zR{a#$3c(~+{grh58;r@U1}K@#4={z*KqZ^`8m6)uq~tQ6!8BHbl?d}8pJs?Vc7F37 z%wRQCi861(Ojg5`IP(h3Vl`YTY@X*64{`S{Zk~cUtVSwj%%d=u)$dA0^8n0aHA<;w z?%`7raVM{B?tlfX#wZQU&9IQwSS8+E2a8yZQ(BlS`Q$|0)!Ud$VF{}VN=I`6EM+xO zNj7K0GFFq69_BPYT@iQqKITMN!D@=q-y8#fu$rn2F-O2kR@0P`=3qX75qJBsW@;h^7FG+Dy=GO|%4(5v(5%3xJ>oOMF|#ymXSGB*Z5D$atd=Sl z%tEk})iUL(8OtX^;QTA|!Gx%0F7LwRK8fjz8ND$mWFd}<^0vV6-|Qutk$Z!>F~*tV4WIfhQUEr>s80p;Sj40Dwzm}S#4A^8Xx)eNqh#$ zYP^A?tTwATjpuNT)fP36@d%Ey+N$O=?(+$i_-qns+=7#=wyUwmRXD|Jhg!(E0H;~) zRErs>`4mfhW+`nPgR`u5s}+ocaE{fVYE@$|oM*L1t!3=wlP>XDroOQSF0$IEHZj)2 zC02i_3C1e8%xb^d+E~V?Vd67R2V)^zWpz+ZGUmWFR)^H?#&o#O>ag0|n8YV$;Y94Rh=Z4`uB$hVC_d#ApSkWC z`QbIIo9aU&0^YE?r9Lxq!CO|h)z?NgeiA@@7W-gig7>WMYG9;;53KHKA%mZ`u)43= zMmRq$Ab6mqG7R|4>TfNrp}@ba{?Rh%pAc9*)Ut3-M^=xt9Qq4XSUuKq>yJ@o^+e07 zKR}JuQ_a(F^HT@nGhK{+4Ruz}wSwIH4OTC-qWT#$S-sRs>BsrW1o2s~ynYC6R Date: Tue, 6 Feb 2018 16:56:40 +0000 Subject: [PATCH 3/4] Adding handmade class file exhibiting the same problem --- .../ManyLocalVariables.class | Bin 0 -> 222 bytes .../ManyLocalVariables.j | 36 ++++++++++++++++++ .../lots_local_variables_manual/test.desc | 4 ++ 3 files changed, 40 insertions(+) create mode 100644 regression/cbmc-java/lots_local_variables_manual/ManyLocalVariables.class create mode 100644 regression/cbmc-java/lots_local_variables_manual/ManyLocalVariables.j create mode 100644 regression/cbmc-java/lots_local_variables_manual/test.desc diff --git a/regression/cbmc-java/lots_local_variables_manual/ManyLocalVariables.class b/regression/cbmc-java/lots_local_variables_manual/ManyLocalVariables.class new file mode 100644 index 0000000000000000000000000000000000000000..e33d34c568a37f08447ab0c7b411fb4b340e6f68 GIT binary patch literal 222 zcmZXOy$*sv5QJyt6vaYgq}NUhr6cwxCMNzA8fy-`7zjcFXyQBh1Qu3QJ{0F->lQmZ z*_|)@sa|gwn4wGPNAfP6SSA-|??);q2*a&R9-B0f@kwT(^kbFJBZ75EZ&{#LVXO$o zWV$AZWqM}Q+k}bQ-LAgMj`cY&3Y9Zy@J}+)HbEGp0}FK#PbLIwlidQA)~qApl5n*s hU51seu57Y(X%k9YSDxoRf5{g27AI>8|HRrr;|q Date: Thu, 8 Feb 2018 17:25:50 +0000 Subject: [PATCH 4/4] Adding invariant to check instruction is normal wide Only specific instructions can follow a wide byte. --- src/java_bytecode/java_bytecode_parser.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 58bfc4f09b5..85c63e263b5 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -711,6 +711,13 @@ void java_bytecode_parsert::rbytecode( wide_instruction=true; address++; bytecode=read_u1(); + // The only valid instructions following a wide byte are + // [ifald]load, [ifald]store, ret and iinc + // All of these have either format of v, or V + INVARIANT( + bytecodes[bytecode].format == 'v' || bytecodes[bytecode].format == 'V', + "Unexpected wide instruction: " + + id2string(bytecodes[bytecode].mnemonic)); } instructions.push_back(instructiont());