From 5ec200c95558aa7635e3e67b9112f00c7ff31a28 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 27 May 2020 14:00:23 +0100 Subject: [PATCH 1/6] Add support for lambdas with implicit boxing Turns out the usual lambda metafactory can apply boxing/unboxing, so you might see a situation like int myMethod(int i) { ... } interface MyLambdaType { Integer f(Integer i); } MyLambdaType mlt = SomeType::myMethod; And contrary to my prior expectations, the compiler doesn't generate a method stub to do the type conversion, it just directly requests an invokestatic lambda pointed at myMethod, regardless of the int vs. Integer clash. The lambda metafactory (which re-implement in JBMC) is then responsible for adding the necessary conversions. --- .../jbmc/lambda-boxing/Boolean.desc | 9 + .../BoxingLambda$TakesBoxedBoolean.class | Bin 0 -> 252 bytes .../BoxingLambda$TakesBoxedByte.class | Bin 0 -> 240 bytes .../BoxingLambda$TakesBoxedCharacter.class | Bin 0 -> 260 bytes .../BoxingLambda$TakesBoxedDouble.class | Bin 0 -> 248 bytes .../BoxingLambda$TakesBoxedFloat.class | Bin 0 -> 244 bytes .../BoxingLambda$TakesBoxedInteger.class | Bin 0 -> 252 bytes .../BoxingLambda$TakesBoxedLong.class | Bin 0 -> 240 bytes .../BoxingLambda$TakesBoxedShort.class | Bin 0 -> 244 bytes .../BoxingLambda$TakesUnboxedBoolean.class | Bin 0 -> 220 bytes .../BoxingLambda$TakesUnboxedByte.class | Bin 0 -> 214 bytes .../BoxingLambda$TakesUnboxedCharacter.class | Bin 0 -> 224 bytes .../BoxingLambda$TakesUnboxedDouble.class | Bin 0 -> 218 bytes .../BoxingLambda$TakesUnboxedFloat.class | Bin 0 -> 216 bytes .../BoxingLambda$TakesUnboxedInteger.class | Bin 0 -> 220 bytes .../BoxingLambda$TakesUnboxedLong.class | Bin 0 -> 214 bytes .../BoxingLambda$TakesUnboxedShort.class | Bin 0 -> 216 bytes .../jbmc/lambda-boxing/BoxingLambda.class | Bin 0 -> 9108 bytes .../jbmc/lambda-boxing/BoxingLambda.java | 171 ++++++++++++++++++ jbmc/regression/jbmc/lambda-boxing/Byte.desc | 9 + .../jbmc/lambda-boxing/Character.desc | 9 + .../regression/jbmc/lambda-boxing/Double.desc | 9 + jbmc/regression/jbmc/lambda-boxing/Float.desc | 9 + .../jbmc/lambda-boxing/Integer.desc | 9 + jbmc/regression/jbmc/lambda-boxing/Long.desc | 9 + jbmc/regression/jbmc/lambda-boxing/Short.desc | 9 + jbmc/src/java_bytecode/java_utils.cpp | 66 +++++++ jbmc/src/java_bytecode/java_utils.h | 30 +++ jbmc/src/java_bytecode/lambda_synthesis.cpp | 112 +++++++++++- 29 files changed, 445 insertions(+), 6 deletions(-) create mode 100644 jbmc/regression/jbmc/lambda-boxing/Boolean.desc create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedBoolean.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedByte.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedCharacter.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedDouble.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedFloat.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedInteger.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedLong.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedShort.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedBoolean.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedByte.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedCharacter.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedDouble.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedFloat.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedInteger.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedLong.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedShort.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingLambda.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingLambda.java create mode 100644 jbmc/regression/jbmc/lambda-boxing/Byte.desc create mode 100644 jbmc/regression/jbmc/lambda-boxing/Character.desc create mode 100644 jbmc/regression/jbmc/lambda-boxing/Double.desc create mode 100644 jbmc/regression/jbmc/lambda-boxing/Float.desc create mode 100644 jbmc/regression/jbmc/lambda-boxing/Integer.desc create mode 100644 jbmc/regression/jbmc/lambda-boxing/Long.desc create mode 100644 jbmc/regression/jbmc/lambda-boxing/Short.desc diff --git a/jbmc/regression/jbmc/lambda-boxing/Boolean.desc b/jbmc/regression/jbmc/lambda-boxing/Boolean.desc new file mode 100644 index 00000000000..69b7c9d8516 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/Boolean.desc @@ -0,0 +1,9 @@ +CORE +BoxingLambda +--function BoxingLambda.testBoolean --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::BoxingLambda\.testBoolean:\(\)V\.assertion\.1\] line 73 assertion at file BoxingLambda\.java line 73 function java::BoxingLambda\.testBoolean:\(\)V bytecode-index 25: SUCCESS +\[java::BoxingLambda\.testBoolean:\(\)V\.assertion\.2\] line 74 assertion at file BoxingLambda\.java line 74 function java::BoxingLambda\.testBoolean:\(\)V bytecode-index 35: SUCCESS +\[java::BoxingLambda\.testBoolean:\(\)V\.assertion\.3\] line 75 assertion at file BoxingLambda\.java line 75 function java::BoxingLambda\.testBoolean:\(\)V bytecode-index 47: SUCCESS +\[java::BoxingLambda\.testBoolean:\(\)V\.assertion\.4\] line 76 assertion at file BoxingLambda\.java line 76 function java::BoxingLambda\.testBoolean:\(\)V bytecode-index 53: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedBoolean.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedBoolean.class new file mode 100644 index 0000000000000000000000000000000000000000..595e1c325784efb9440c1267257a457e11a3cd24 GIT binary patch literal 252 zcmZvXK?;Ik5QX2EshL4tpj8XoN26D>@Bkjl__2}D>}+0k zCo}KQ^95jqfeFh*pJ0eEqQ$7>_c%aL*6DC6UJU~Px9Co z=O7Zx`q_j-m^AV1C{8RD;i&c`4BNojk literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedCharacter.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedCharacter.class new file mode 100644 index 0000000000000000000000000000000000000000..04a62a6d4df8ffb36d1d8db570f8433c91e01961 GIT binary patch literal 260 zcmZvXK@P!S5QX1RZB-@21uQH`gpHk@CK8Fnf(uOlPO4QUZHcp4IDkWmp9NiXGjH-` z^5xC*b$4so&?1340y-Mn?(o`}p;XId|(D@hJ_^~M6)-9_|fKbza Y=`;v+7<#Lr@tr0dosPaBSZJE|8|TwRdjJ3c literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedDouble.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedDouble.class new file mode 100644 index 0000000000000000000000000000000000000000..274866094f874a99110bf08d4006cb1170e7ac5f GIT binary patch literal 248 zcmZXP!3u&<6h!BmJDm^8$*jwjSpm;HDB7(Eet0Lr0qL?sP=C>q^ zeR&EZIr{`ya0$aY9v$S7OHDZX<3HlF!=@9$Aw6AIt11vB;4*&oF literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedInteger.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedInteger.class new file mode 100644 index 0000000000000000000000000000000000000000..120eda659ff6a5ea9d554c980410fb2cf7dea76d GIT binary patch literal 252 zcmZvX!3u&<5Jm5p`OFOJ2U@kTO>Ww?D+mOkMg7222hr>qYSFi~=mYww=oLXO+{_&g zGnadxulobQ5+eayU`ViJ9P_y$cwU&xtMm)0Qa?})r(CV(9gN`Y%S#pWHY=DgS(mp= zrJ+1UiClav1YE+jjb{gWe$M)@gSmlHTx|+j*IX0E|3JGa=UAt7+qM=!FmxZS WCZPvYZwC6`X~EIz=nI0tz_Q;P|3P;E literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedLong.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedLong.class new file mode 100644 index 0000000000000000000000000000000000000000..8360e9315c9859786460c831baa3b0b66aff0ad4 GIT binary patch literal 240 zcmZ9Hu?oUK5JYEVyo)i4)^=i{jcM%c6a*n)p+9iB93e4YB&XuHS@;2dlz6c**z7Ei z-C^eSemnsz(Btqpx&$VqRObs}JdJX36Ja5A8b+l~m$QFB@b~4ll4_F`iZEQ2_e`ge zIK_#W*UuaQVbsKvgE%TxyEs?UCJUN|3?MkRgH@N% Uf@?Pi?eAppt@`$Yz|mpe2h8w1a{vGU literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedShort.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedShort.class new file mode 100644 index 0000000000000000000000000000000000000000..235a272437bdb18b0c483481965ff4705dbc98c8 GIT binary patch literal 244 zcmZXPu?~Vj5JYDYIYf-wTT*Bvjh&q)CMF~n_yfmrK@h=kX#6${KfsSNo-~rs>}+0k zCo}KQ^95jq5rfSzBv@Psd94ZFJjnQ+`#CQXKRlIHy9+bg$M9ZVss_AdGi?N z_k7(S02UYs1Oj~qPD<%>!{ATlOfrPK>QXDc%1g~Kl2x0VY(u9crFlVD5{MYazw~5J zM{N%#sal=NTjOlQe=1rVqw8f!)@th%pRBkflf~Pl(8~2kzo8sp@Z3^|K0^n-`#f~N Omm_o-It7D3j|Xqn+cP-; literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedCharacter.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedCharacter.class new file mode 100644 index 0000000000000000000000000000000000000000..990243e903a36c62814d6f839de87b1b3d4edf8c GIT binary patch literal 224 zcmZ{eK@P!C7=-7qYN<+CxPVx&(Tx*mB9TZeaDczBe@fM>ydutK;Q$UL9;4Y|5)qvN#k%=+DdhL1!yIB`HsHzOj#xFs$Rz zmXA{HbW+|WjrVL=UBnOue|WgmT1;GURY^tYeOIG`br!9YT$Fth*5^Hd;MmXBT|xt{ SO%9qr^$=JOY=hvV?X^D6O*c0H literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedDouble.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedDouble.class new file mode 100644 index 0000000000000000000000000000000000000000..dcd9dcb4b6d8fcd4d4bb88c0bbde9b43ce81374e GIT binary patch literal 218 zcmZurF%E)I6zfyuBVwXnz{NoqSv-Lf6B82$^#Bj}As~JXUkqn+@Bkjl_;F%zX`7~P z`u;p$09F_ZI06HL%~2$8cY-w!76HLM7F8L^ZJJBMcwN+~O7?sWV_s(bU;&RXZQHXG zU!*>(u&8Am6jj(1C;v=ur<5!=IcqI7VbtvTIjh7!gqe)Y2d_PB1B8xwYuF-mVHwpy Q?}s*A!>&mX1p2n~1p#6-&j0`b literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedFloat.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedFloat.class new file mode 100644 index 0000000000000000000000000000000000000000..b7222a457aa88319510782ea869c132e4417dcae GIT binary patch literal 216 zcmZvWF%E)26h!AE0wN}I0V@k_r11orY+_w32>0ezXHt|(65^FXFoaVf!_|85e!lY|Y z4}6l%QKzPrxlo2JEB@m}8?9x%R@^kQA&kGYM6oWCU0TV^wxTZ90|<`YYSkt5;M&hY Q|93rvRzsU0_!xM>2W`DH2LJ#7 literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedInteger.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedInteger.class new file mode 100644 index 0000000000000000000000000000000000000000..f0c458d48394dcbe57a1eadb9f543437b8e84fba GIT binary patch literal 220 zcmZvWF$%&!6h!C8n8X-C@d6eW+L*=@CZgB20eq z^dL`cjykDYPK9nbYEXJkOS-eXMR`x~oJM94k$NshM5;|~g Sa?t&%htPUx8w4LcFL(p2rZvF; literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedLong.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedLong.class new file mode 100644 index 0000000000000000000000000000000000000000..cb74f270447bbd7311acee2f0e468f6c5052ab39 GIT binary patch literal 214 zcmZWj!3x4K6w8~lopXYIfHx0%aTmWpL2wK_s2|XEWo*t?R+W952S31%600Y{OA?ElpeMA{D1B7xPNo1V=;||Jswi zI4XP4nQ2v?8eI^E|5mioS~aU$SgWi{e7fRV=px=`m6C2h`YmMu!E;X?`-BdBr#y7O O$PhXXU4p>TW5FBV7c)Ts literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedShort.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedShort.class new file mode 100644 index 0000000000000000000000000000000000000000..bf4c10a377e3543d9ac3ac0a52f5ba35a3bbaafc GIT binary patch literal 216 zcmZvWF$%&!6h!B1+>J4Uxqy|0Hm30e3W6Y5L=UjpEHN?eN>(Ljv+w{ON?ff{*!=kn zGmm+_A5Q=a3^{y`0f7lA)#Xa?rpYWJ1c|xTQmu~oC%95k09V`0dg&VC^y{d$@$`VFjT3iX8$Gfyt(zU`imH~v0+v?OKbm6(L RgWm5l1Wp5&AaL}V{{fbpG*tiq literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda.class new file mode 100644 index 0000000000000000000000000000000000000000..f1b83277ee26704dcea36cbfea4857945815b557 GIT binary patch literal 9108 zcmbVS33yc175+~$sC#$*6xe7t*zZ#Tf4WmcCocu+uHv3zGd!Y7Qe52A9K$;_uT)T^WSsN zJMY1Z?;ZIxfa!8Lh&DWLQ~sQiK5s+tB^zbg>M8A#PcC^ z;hQ$f@ogIceAmVhd_RaE;D;fs#gCNq;}9;wPi$1+XErSS!bT;26~wRcn-Esxw@Uh5 z2&?dW8&&wDP0&Bv2;r|myotYsumXQq(pwdC=$ZNx!gBn>Mi~FJF%T5gWD)w=rBs+NhP$K^Y@Qh0q~m zl{9XMb3YJnp^UdNLMGT4DM#BFCC3EiSUE0)1=6UbrV!>yvn7**GDVKJWU3|81U1W| zn_|7^CA(7FVm+N3Qt6B!+@4Iv(yfVTZ*Q#Ek`n~g+N#C3vE)QS#9Z2uO0Ku$B*Cz( zsiQktFx<3kPiA84V`)pKdw18kzWNkT?K(9-k&0$4IW@-%S9zMiHnH1MeO-x|C8vAd zX=qRT0l^5Gd(2No0jbv;?Ky5)6vcJAUw-dDiMn&Et%y7 zq_JBZHH{k-zv)aomF#Vc_eSY>k3d!lDrUr!@eG%hH#RL71X@!)F-G4JPsSGaZSIPt zmnmb0-jV8#CYDFjadqt~1DOr+Ub@%8yTz01JEEJrdZLUXl!^6b{F?_eYTLC#f(bdc z4Vog;SFR3gdp9z{qyj5)!{(am>^@+^cK_=Sfz3GJYfs%oXdw}!gFH@Pn6z$_lOlhBA3`<&xj}3 z5}t0of9kB4*grK*)DrurEm%QxY0)IO)u<>5dcHIXjtNVcu61@oABG0Su%2lk-wll& z8>3sJ(-P6-`e}}RQ=W$Bl4q)>fWF4SR3S95PE9f)bzCN*ONAs@Sqwl|U2EXEL^p8% z8cj%V158v;M^EFdEe3FQ#*AO5M*~Z6PW(>Nn7Cf1$-3P5J^gUQUni3rm=edD?z#zX zqWb4TSn_PcS$|@rf$N{X20mY=n9%;rnI?KxOE$V$^o<*sbLQTu8s5N%TF%}nWe&1d z5VR|I?_9OHcW$L^;KMU#?_7N@s`E%-Dx3S}S@M9*=uWs#gkWc?FWnuRA6NCihG*6< z@l#b6hp_?N{s`A*dNb+hmPN75hEz{)b%o51pr6B>u*{W~u(V2BMCMgjp;9U4QwS^J ztT5Jr5Ap?JX_tl6pg$~UONU@|_LR)^o?G+M=~P-Rn-{^;1Ye}&#SvLTxEdv&Lt(fQ z&b4Hzg6!l4o({`0IZvsVMDRG*Em!jS5m`a=(Mn!P;V31nvg87_ZZ$9Pcvvo!i(7kDr%+hn^^_eOA- z>n>IDj)+`F^HY_4IfXNnu+x$&)VeEqfx}_BO0HJw%OW_$b=N5Q+K607^Vv$?MPaTI zc3X12T6Y64a40M{%1ugr9iP-@Qdn|xSoWyxi)6QNN!P|$H`}~A)6#kByUz|?1_k5t z4XE+k#PRvl?s`?r1Y`5(^>Sx+LjJ6~+AUZG9n=7&49urr@d$MF;^U~O4^AE811;Y| zyWq`F%Aa>V@CywexA{gI#4ssv9~Vc}mf~DGvjuM8t@gUj0-LRUaH~vEZjoDqXp!64 zenz{yV_TRYlNy_fH6TWDS|7{kR|Qrt+Go>DD_PS5jjNj2)V4LgA6B88<%U7Df-r-u z3IUnH5~e2WryGjE+8Ryt#g_0vHsArvw^m#K<`lfLQ#A_pLMjY zO|60jMWf9c7s7Mn$r=@b%Cjp3mV4Of-0&;|{vG&)Yiu=X@MpN7s++HhSuR=?7kk;& z7w5unWCD$CO>KgfqC~isg&cRI^RWtoEilBF=)Uk4i7o7#(%DD94CTF75FAkU--%pj{mKsk5HsdWBxb0i%#g3sQw zGM+SoZ&$(JS+cgdZ!Lkwg-r`f)i!Nc$Xhoc7pGKhD+-|lb^(mqrZlRyEi^-Q&8iZd z%u)LAO6y;n$j<@e_K%@u1(skAN*qJ#CEG16MAR9bhM;d+L_ zUiD=!8!#g<*1C`Hkv*~AcskbOxA**7lj-9Jz`Me7w;T%NS-uS5DYozU1bcCOl#MkW zW|xc)vE{}6>|b#Y4)L&LPg^{>HMJ==twXFxX?u{nEX$$e})I#Q`k zeOm-CnQwS5fb$-+Ae!t+#CjVX%QKA>?#!ggwyDWkxNQ5D*#9@_+_LmqlX3U9tNx^naL7Eg?swr4U3bvaR%(Sq>!e#s&U8g9x z+^67QE(JFpL9Ic-2!n!=9tCyHk!U|g4Pdn5U`(WIFbSh4N1_8bstoy4byMDFZBZiD zkchP;BC7XxHvg$-6=K}^b-01&Kqa`73)hl}otlVkB;pE9M1n-@G>MpP;Ytfv@%N|+ ziioRyBHm-#tFy4@2*w&jj5CNB?-5boT-}el0n{rVCe&i$fx&q{W^(lajxHys`E&JC z-fwkLE)wKoGr35Ti!GSLJYUUNcQW&DW@==)*v;8%G#5KKf34;sMJ}!}xtL?&It#n_ zJ9eVtVznTr>^cKbVP8lfwgOE<^sz_$j4V z7G+^OS-6xe>>vx5V;19I!TsLG+OUfonq}cCvT(g-p^q%wpjn8Mh3icgW?8t=!cF`g zQ?FRK*=ND14wDTQrWh<7@3Ek(!_)yxQ!Jd2R|Ir*II&oDD88;J1-nSWZc=bPDY%i< z;U-oGl>&RX#kU$1sOqpsQ=qEDEt&#V9rl{6nFYu80m1P!Nm-Ni7Y!qFH=`6Df zB1nkSf_$8uG8kd6fe>U=4`>ATn?8c$ghDtWu(lsl2P5ptL3oHvC?D9i7C>kUcd>j8 zM%bQ%@F+f_5!n6u2-zqmRCn`XFc=|`gYYqYTqCfFb`jcLDr*_Vm`L<6DkEJFV~Bo8 zDlDfPa@x2x239Sez>}O;-OUh`4Vx89!fg}FWnXUoZj@d2Gpw+{C3KjVc zs~cCC2<3Q=kY)H3+d#0&)vzsW!TgF!Ea2GAaUsXEId*Vd#BnjlB^=M;crM4K96LEK z<9Hs&vUtaY#8J9tG)FXMZz?p6F0uWH?E_&HwF(yRET zt9u=P!0TG~2L6OMwDdau;_BYUJ9t~`-o?N0u9n`$e;l0zWQYWmPAsVuOG^O>y1E*% hrAF&&WrWmfsYXV*x;m+sI<1>1lVqZn>ZC#H{s-zUHnIQ! literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda.java b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda.java new file mode 100644 index 00000000000..6a37fb9fbff --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda.java @@ -0,0 +1,171 @@ +public class BoxingLambda { + + interface TakesBoxedBoolean { + public Boolean accept(Boolean b); + } + + interface TakesUnboxedBoolean { + public boolean accept(boolean b); + } + + interface TakesBoxedByte { + public Byte accept(Byte b); + } + + interface TakesUnboxedByte { + public byte accept(byte b); + } + + interface TakesBoxedCharacter { + public Character accept(Character c); + } + + interface TakesUnboxedCharacter { + public char accept(char c); + } + + interface TakesBoxedDouble { + public Double accept(Double d); + } + + interface TakesUnboxedDouble { + public double accept(double d); + } + + interface TakesBoxedFloat { + public Float accept(Float f); + } + + interface TakesUnboxedFloat { + public float accept(float f); + } + + interface TakesBoxedInteger { + public Integer accept(Integer i); + } + + interface TakesUnboxedInteger { + public int accept(int i); + } + + interface TakesBoxedLong { + public Long accept(Long l); + } + + interface TakesUnboxedLong { + public long accept(long l); + } + + interface TakesBoxedShort { + public Short accept(Short s); + } + + interface TakesUnboxedShort { + public short accept(short s); + } + + public static void testBoolean() { + + TakesBoxedBoolean takesBoxed = b -> !b; + TakesUnboxedBoolean takesUnboxed = takesBoxed::accept; + TakesBoxedBoolean takesBoxedAgain = takesUnboxed::accept; + + assert takesBoxed.accept(true) == false; + assert takesUnboxed.accept(true) == false; + assert takesBoxedAgain.accept(true) == false; + assert false; + + } + + public static void testByte() { + + TakesBoxedByte takesBoxed = b -> (byte)(b + 1); + TakesUnboxedByte takesUnboxed = takesBoxed::accept; + TakesBoxedByte takesBoxedAgain = takesUnboxed::accept; + + assert takesBoxed.accept((byte)1) == 2; + assert takesUnboxed.accept((byte)1) == 2; + assert takesBoxedAgain.accept((byte)1) == 2; + assert false; + + } + + public static void testCharacter() { + + TakesBoxedCharacter takesBoxed = c -> c == 'a' ? 'b' : 'a'; + TakesUnboxedCharacter takesUnboxed = takesBoxed::accept; + TakesBoxedCharacter takesBoxedAgain = takesUnboxed::accept; + + assert takesBoxed.accept('a') == 'b'; + assert takesUnboxed.accept('a') == 'b'; + assert takesBoxedAgain.accept('a') == 'b'; + assert false; + + } + + public static void testDouble() { + + TakesBoxedDouble takesBoxed = d -> d + 1; + TakesUnboxedDouble takesUnboxed = takesBoxed::accept; + TakesBoxedDouble takesBoxedAgain = takesUnboxed::accept; + + assert takesBoxed.accept(1.0) == 2.0; + assert takesUnboxed.accept(1.0) == 2.0; + assert takesBoxedAgain.accept(1.0) == 2.0; + assert false; + + } + + public static void testFloat() { + + TakesBoxedFloat takesBoxed = f -> f + 1; + TakesUnboxedFloat takesUnboxed = takesBoxed::accept; + TakesBoxedFloat takesBoxedAgain = takesUnboxed::accept; + + assert takesBoxed.accept(1.0f) == 2.0f; + assert takesUnboxed.accept(1.0f) == 2.0f; + assert takesBoxedAgain.accept(1.0f) == 2.0f; + assert false; + + } + + public static void testInteger() { + + TakesBoxedInteger takesBoxed = i -> i + 1; + TakesUnboxedInteger takesUnboxed = takesBoxed::accept; + TakesBoxedInteger takesBoxedAgain = takesUnboxed::accept; + + assert takesBoxed.accept(1) == 2; + assert takesUnboxed.accept(1) == 2; + assert takesBoxedAgain.accept(1) == 2; + assert false; + + } + + public static void testLong() { + + TakesBoxedLong takesBoxed = l -> l + 1; + TakesUnboxedLong takesUnboxed = takesBoxed::accept; + TakesBoxedLong takesBoxedAgain = takesUnboxed::accept; + + assert takesBoxed.accept(1L) == 2L; + assert takesUnboxed.accept(1L) == 2L; + assert takesBoxedAgain.accept(1L) == 2L; + assert false; + + } + + public static void testShort() { + + TakesBoxedShort takesBoxed = s -> (short)(s + 1); + TakesUnboxedShort takesUnboxed = takesBoxed::accept; + TakesBoxedShort takesBoxedAgain = takesUnboxed::accept; + + assert takesBoxed.accept((short)1) == 2; + assert takesUnboxed.accept((short)1) == 2; + assert takesBoxedAgain.accept((short)1) == 2; + assert false; + + } + +} diff --git a/jbmc/regression/jbmc/lambda-boxing/Byte.desc b/jbmc/regression/jbmc/lambda-boxing/Byte.desc new file mode 100644 index 00000000000..988db9e9c02 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/Byte.desc @@ -0,0 +1,9 @@ +CORE +BoxingLambda +--function BoxingLambda.testByte --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::BoxingLambda\.testByte:\(\)V\.assertion\.1\] line 86 assertion at file BoxingLambda\.java line 86 function java::BoxingLambda\.testByte:\(\)V bytecode-index 26: SUCCESS +\[java::BoxingLambda\.testByte:\(\)V\.assertion\.2\] line 87 assertion at file BoxingLambda\.java line 87 function java::BoxingLambda\.testByte:\(\)V bytecode-index 37: SUCCESS +\[java::BoxingLambda\.testByte:\(\)V\.assertion\.3\] line 88 assertion at file BoxingLambda\.java line 88 function java::BoxingLambda\.testByte:\(\)V bytecode-index 50: SUCCESS +\[java::BoxingLambda\.testByte:\(\)V\.assertion\.4\] line 89 assertion at file BoxingLambda\.java line 89 function java::BoxingLambda\.testByte:\(\)V bytecode-index 56: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/Character.desc b/jbmc/regression/jbmc/lambda-boxing/Character.desc new file mode 100644 index 00000000000..1488fef62df --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/Character.desc @@ -0,0 +1,9 @@ +CORE +BoxingLambda +--function BoxingLambda.testCharacter --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::BoxingLambda\.testCharacter:\(\)V\.assertion\.1\] line 99 assertion at file BoxingLambda\.java line 99 function java::BoxingLambda\.testCharacter:\(\)V bytecode-index 26: SUCCESS +\[java::BoxingLambda\.testCharacter:\(\)V\.assertion\.2\] line 100 assertion at file BoxingLambda\.java line 100 function java::BoxingLambda\.testCharacter:\(\)V bytecode-index 37: SUCCESS +\[java::BoxingLambda\.testCharacter:\(\)V\.assertion\.3\] line 101 assertion at file BoxingLambda\.java line 101 function java::BoxingLambda\.testCharacter:\(\)V bytecode-index 50: SUCCESS +\[java::BoxingLambda\.testCharacter:\(\)V\.assertion\.4\] line 102 assertion at file BoxingLambda\.java line 102 function java::BoxingLambda\.testCharacter:\(\)V bytecode-index 56: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/Double.desc b/jbmc/regression/jbmc/lambda-boxing/Double.desc new file mode 100644 index 00000000000..605b9f7c8d9 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/Double.desc @@ -0,0 +1,9 @@ +CORE +BoxingLambda +--function BoxingLambda.testDouble --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::BoxingLambda\.testDouble:\(\)V\.assertion\.1\] line 112 assertion at file BoxingLambda\.java line 112 function java::BoxingLambda\.testDouble:\(\)V bytecode-index 27: SUCCESS +\[java::BoxingLambda\.testDouble:\(\)V\.assertion\.2\] line 113 assertion at file BoxingLambda\.java line 113 function java::BoxingLambda\.testDouble:\(\)V bytecode-index 39: SUCCESS +\[java::BoxingLambda\.testDouble:\(\)V\.assertion\.3\] line 114 assertion at file BoxingLambda\.java line 114 function java::BoxingLambda\.testDouble:\(\)V bytecode-index 53: SUCCESS +\[java::BoxingLambda\.testDouble:\(\)V\.assertion\.4\] line 115 assertion at file BoxingLambda\.java line 115 function java::BoxingLambda\.testDouble:\(\)V bytecode-index 59: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/Float.desc b/jbmc/regression/jbmc/lambda-boxing/Float.desc new file mode 100644 index 00000000000..e0062279f34 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/Float.desc @@ -0,0 +1,9 @@ +CORE +BoxingLambda +--function BoxingLambda.testFloat --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::BoxingLambda\.testFloat:\(\)V\.assertion\.1\] line 125 assertion at file BoxingLambda\.java line 125 function java::BoxingLambda\.testFloat:\(\)V bytecode-index 27: SUCCESS +\[java::BoxingLambda\.testFloat:\(\)V\.assertion\.2\] line 126 assertion at file BoxingLambda\.java line 126 function java::BoxingLambda\.testFloat:\(\)V bytecode-index 39: SUCCESS +\[java::BoxingLambda\.testFloat:\(\)V\.assertion\.3\] line 127 assertion at file BoxingLambda\.java line 127 function java::BoxingLambda\.testFloat:\(\)V bytecode-index 53: SUCCESS +\[java::BoxingLambda\.testFloat:\(\)V\.assertion\.4\] line 128 assertion at file BoxingLambda\.java line 128 function java::BoxingLambda\.testFloat:\(\)V bytecode-index 59: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/Integer.desc b/jbmc/regression/jbmc/lambda-boxing/Integer.desc new file mode 100644 index 00000000000..f0e61742adb --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/Integer.desc @@ -0,0 +1,9 @@ +CORE +BoxingLambda +--function BoxingLambda.testInteger --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::BoxingLambda\.testInteger:\(\)V\.assertion\.1\] line 138 assertion at file BoxingLambda\.java line 138 function java::BoxingLambda\.testInteger:\(\)V bytecode-index 26: SUCCESS +\[java::BoxingLambda\.testInteger:\(\)V\.assertion\.2\] line 139 assertion at file BoxingLambda\.java line 139 function java::BoxingLambda\.testInteger:\(\)V bytecode-index 37: SUCCESS +\[java::BoxingLambda\.testInteger:\(\)V\.assertion\.3\] line 140 assertion at file BoxingLambda\.java line 140 function java::BoxingLambda\.testInteger:\(\)V bytecode-index 50: SUCCESS +\[java::BoxingLambda\.testInteger:\(\)V\.assertion\.4\] line 141 assertion at file BoxingLambda\.java line 141 function java::BoxingLambda\.testInteger:\(\)V bytecode-index 56: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/Long.desc b/jbmc/regression/jbmc/lambda-boxing/Long.desc new file mode 100644 index 00000000000..ce8f0f79192 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/Long.desc @@ -0,0 +1,9 @@ +CORE +BoxingLambda +--function BoxingLambda.testLong --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::BoxingLambda\.testLong:\(\)V\.assertion\.1\] line 151 assertion at file BoxingLambda\.java line 151 function java::BoxingLambda\.testLong:\(\)V bytecode-index 27: SUCCESS +\[java::BoxingLambda\.testLong:\(\)V\.assertion\.2\] line 152 assertion at file BoxingLambda\.java line 152 function java::BoxingLambda\.testLong:\(\)V bytecode-index 39: SUCCESS +\[java::BoxingLambda\.testLong:\(\)V\.assertion\.3\] line 153 assertion at file BoxingLambda\.java line 153 function java::BoxingLambda\.testLong:\(\)V bytecode-index 53: SUCCESS +\[java::BoxingLambda\.testLong:\(\)V\.assertion\.4\] line 154 assertion at file BoxingLambda\.java line 154 function java::BoxingLambda\.testLong:\(\)V bytecode-index 59: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/Short.desc b/jbmc/regression/jbmc/lambda-boxing/Short.desc new file mode 100644 index 00000000000..7a969232ea7 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/Short.desc @@ -0,0 +1,9 @@ +CORE +BoxingLambda +--function BoxingLambda.testShort --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::BoxingLambda\.testShort:\(\)V\.assertion\.1\] line 164 assertion at file BoxingLambda\.java line 164 function java::BoxingLambda\.testShort:\(\)V bytecode-index 26: SUCCESS +\[java::BoxingLambda\.testShort:\(\)V\.assertion\.2\] line 165 assertion at file BoxingLambda\.java line 165 function java::BoxingLambda\.testShort:\(\)V bytecode-index 37: SUCCESS +\[java::BoxingLambda\.testShort:\(\)V\.assertion\.3\] line 166 assertion at file BoxingLambda\.java line 166 function java::BoxingLambda\.testShort:\(\)V bytecode-index 50: SUCCESS +\[java::BoxingLambda\.testShort:\(\)V\.assertion\.4\] line 167 assertion at file BoxingLambda\.java line 167 function java::BoxingLambda\.testShort:\(\)V bytecode-index 56: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index d91a5a00cae..2a0067fc9fa 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/jbmc/src/java_bytecode/java_utils.cpp @@ -38,6 +38,72 @@ bool is_java_string_type(const struct_typet &struct_type) struct_type.has_component("data"); } +const java_boxed_type_infot * +get_boxed_type_info_by_name(const irep_idt &type_name) +{ + static std::unordered_map type_info_by_name = + { + {"java::java.lang.Boolean", + {"java::java.lang.Boolean.booleanValue:()Z", java_boolean_type()}}, + {"java::java.lang.Byte", + {"java::java.lang.Byte.byteValue:()B", java_byte_type()}}, + {"java::java.lang.Character", + {"java::java.lang.Character.charValue:()C", java_char_type()}}, + {"java::java.lang.Double", + {"java::java.lang.Double.doubleValue:()D", java_double_type()}}, + {"java::java.lang.Float", + {"java::java.lang.Float.floatValue:()F", java_float_type()}}, + {"java::java.lang.Integer", + {"java::java.lang.Integer.intValue:()I", java_int_type()}}, + {"java::java.lang.Long", + {"java::java.lang.Long.longValue:()J", java_long_type()}}, + {"java::java.lang.Short", + {"java::java.lang.Short.shortValue:()S", java_short_type()}}, + }; + + auto found = type_info_by_name.find(type_name); + return found == type_info_by_name.end() ? nullptr : &found->second; +} + +const java_primitive_type_infot * +get_java_primitive_type_info(const typet &maybe_primitive_type) +{ + static std::unordered_map + type_info_by_primitive_type = { + {java_boolean_type(), + {"java::java.lang.Boolean", + "java::java.lang.Boolean.valueOf:(Z)Ljava/lang/Boolean;"}}, + {java_byte_type(), + {"java::java.lang.Byte", + "java::java.lang.Byte.valueOf:(B)Ljava/lang/Byte;"}}, + {java_char_type(), + {"java::java.lang.Character", + "java::java.lang.Character.valueOf:(C)" + "Ljava/lang/Character;"}}, + {java_double_type(), + {"java::java.lang.Double", + "java::java.lang.Double.valueOf:(D)" + "Ljava/lang/Double;"}}, + {java_float_type(), + {"java::java.lang.Float", + "java::java.lang.Float.valueOf:(F)" + "Ljava/lang/Float;"}}, + {java_int_type(), + {"java::java.lang.Integer", + "java::java.lang.Integer.valueOf:(I)" + "Ljava/lang/Integer;"}}, + {java_long_type(), + {"java::java.lang.Long", + "java::java.lang.Long.valueOf:(J)Ljava/lang/Long;"}}, + {java_short_type(), + {"java::java.lang.Short", + "java::java.lang.Short.valueOf:(S)" + "Ljava/lang/Short;"}}}; + + auto found = type_info_by_primitive_type.find(maybe_primitive_type); + return found == type_info_by_primitive_type.end() ? nullptr : &found->second; +} + bool is_primitive_wrapper_type_name(const std::string &type_name) { static const std::unordered_set primitive_wrapper_type_names = { diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h index 91644e4e88c..dd5d4f37762 100644 --- a/jbmc/src/java_bytecode/java_utils.h +++ b/jbmc/src/java_bytecode/java_utils.h @@ -32,6 +32,36 @@ bool java_is_array_type(const typet &type); /// and in particular may not have length and data fields. bool is_java_string_type(const struct_typet &struct_type); +/// Return type for get_java_primitive_type_info +struct java_primitive_type_infot +{ + /// Name, including java:: prefix, of the corresponding boxed type + const irep_idt boxed_type_name; + /// Full identifier of the boxed type's factory method that takes the + /// corresponding primitive as its sole argument + const irep_idt boxed_type_factory_method; +}; + +/// If \p primitive_type is a Java primitive type, return information about it, +/// otherwise return null +const java_primitive_type_infot * +get_java_primitive_type_info(const typet &maybe_primitive_type); + +/// Return type for get_boxed_type_info_by_name +struct java_boxed_type_infot +{ + /// Name of the function defined on the boxed type that returns the boxed + /// value + const irep_idt unboxing_function_name; + /// Primitive type that this boxed type contains + const typet corresponding_primitive_type; +}; + +/// If \p type_name is a Java boxed type tag, return information about it, +/// otherwise return null +const java_boxed_type_infot * +get_boxed_type_info_by_name(const irep_idt &type_name); + /// Returns true iff the argument is the fully qualified name of a Java /// primitive wrapper type. bool is_primitive_wrapper_type_name(const std::string &type_name); diff --git a/jbmc/src/java_bytecode/lambda_synthesis.cpp b/jbmc/src/java_bytecode/lambda_synthesis.cpp index 1e5975a8aad..89119d40c1c 100644 --- a/jbmc/src/java_bytecode/lambda_synthesis.cpp +++ b/jbmc/src/java_bytecode/lambda_synthesis.cpp @@ -610,6 +610,82 @@ static symbol_exprt instantiate_new_object( return new_instance_var; } +/// If \p expr needs (un)boxing to satisfy \p required_type, add the required +/// symbols to \p symbol_table and code to \p code_block, then return an +/// expression giving the adjusted expression. Otherwise return \p expr +/// unchanged. \p role is a suggested name prefix for any temporary variable +/// needed; \p function_id is the id of the function any created code it +/// added to. +exprt adjust_type_if_necessary( + exprt expr, + const typet &required_type, + code_blockt &code_block, + symbol_table_baset &symbol_table, + const irep_idt &function_id, + const std::string &role) +{ + const typet &original_type = expr.type(); + const bool original_is_pointer = can_cast_type(original_type); + const bool required_is_pointer = can_cast_type(required_type); + + if(original_is_pointer == required_is_pointer) + { + if(original_is_pointer && original_type != required_type) + return typecast_exprt{expr, required_type}; + else + return expr; + } + + // One is a pointer, the other a primitive -- box or unbox as necessary, and + // check the types are consistent: + if(original_is_pointer) + { + const irep_idt &boxed_type_id = + to_struct_tag_type(original_type.subtype()).get_identifier(); + const auto *boxed_type_info = get_boxed_type_info_by_name(boxed_type_id); + INVARIANT( + boxed_type_info != nullptr, + "Only boxed primitive types should participate in a pointer vs." + " primitive type disagreement"); + INVARIANT( + required_type == boxed_type_info->corresponding_primitive_type, + "Boxed types are only convertable to their corresponding unboxed type"); + + symbol_exprt fresh_local = create_and_declare_local( + function_id, role + "_unboxed", required_type, symbol_table, code_block); + const symbolt &unboxing_function_symbol = + symbol_table.lookup_ref(boxed_type_info->unboxing_function_name); + code_block.add(code_function_callt{ + fresh_local, unboxing_function_symbol.symbol_expr(), {expr}}); + + return std::move(fresh_local); + } + else + { + const irep_idt &boxed_type_id = + to_struct_tag_type(required_type.subtype()).get_identifier(); + const auto *primitive_type_info = + get_java_primitive_type_info(original_type); + INVARIANT( + primitive_type_info != nullptr, + "A Java non-pointer type involved in a type disagreement should" + " be a primitive"); + INVARIANT( + boxed_type_id == primitive_type_info->boxed_type_name, + "Boxed types are only convertable to their corresponding unboxed type"); + + symbol_exprt fresh_local = create_and_declare_local( + function_id, role + "_boxed", required_type, symbol_table, code_block); + const symbolt &boxed_type_factory_method = + symbol_table.lookup_ref(primitive_type_info->boxed_type_factory_method); + + code_block.add(code_function_callt{ + fresh_local, boxed_type_factory_method.symbol_expr(), {expr}}); + + return std::move(fresh_local); + } +} + /// Create the body for the synthetic method implementing an invokedynamic /// method. For most lambdas this means creating a simple function body like /// TR new_synthetic_method(T1 param1, T2 param2, ...) { @@ -642,7 +718,6 @@ codet invokedynamic_synthetic_method( const symbolt &function_symbol = ns.lookup(function_id); const auto &function_type = to_code_type(function_symbol.type); const auto ¶meters = function_type.parameters(); - const auto &return_type = function_type.return_type(); const symbolt &class_symbol = ns.lookup(*declaring_class(function_symbol)); const java_class_typet &class_type = to_java_class_type(class_symbol.type); @@ -707,12 +782,37 @@ codet invokedynamic_synthetic_method( else callee = lambda_method_symbol.symbol_expr(); - if(return_type != empty_typet() && !is_constructor_lambda) + // Adjust boxing if required: + const code_typet &callee_type = to_code_type(lambda_method_symbol.type); + const auto &callee_parameters = callee_type.parameters(); + const auto &callee_return_type = callee_type.return_type(); + INVARIANT( + callee_parameters.size() == lambda_method_args.size(), + "should have args for every parameter"); + for(unsigned i = 0; i < callee_parameters.size(); ++i) + { + lambda_method_args[i] = adjust_type_if_necessary( + std::move(lambda_method_args[i]), + callee_parameters[i].type(), + result, + symbol_table, + function_id, + "param" + std::to_string(i)); + } + + if(callee_return_type != empty_typet() && !is_constructor_lambda) { symbol_exprt result_local = create_and_declare_local( - function_id, "return_value", return_type, symbol_table, result); + function_id, "return_value", callee_return_type, symbol_table, result); result.add(code_function_callt(result_local, callee, lambda_method_args)); - result.add(code_returnt{result_local}); + exprt adjusted_local = adjust_type_if_necessary( + result_local, + function_type.return_type(), + result, + symbol_table, + function_id, + "retval"); + result.add(code_returnt{adjusted_local}); } else { @@ -722,8 +822,8 @@ codet invokedynamic_synthetic_method( if(is_constructor_lambda) { // Return the newly-created object. - result.add(code_returnt{ - typecast_exprt::conditional_cast(lambda_method_args.at(0), return_type)}); + result.add(code_returnt{typecast_exprt::conditional_cast( + lambda_method_args.at(0), function_type.return_type())}); } return std::move(result); From b73595498015192253178e6694344a9137e329a6 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 27 May 2020 14:47:48 +0100 Subject: [PATCH 2/6] Java frontend: support lambdas that implicitly box to Object This broadens our support for lambdas with implicit boxing/unboxing conversions to include those that use a method-reference to a method with type Object -> x to satisfy a functional interface of type primitive -> x (requiring boxing the parameter and then upcasting to Object), or a method with type x -> primitive satisfying an interface of type x -> Object (requiring the same conversion on the return value). --- ...xingWithOtherConversions$IntToObject.class | Bin 0 -> 263 bytes ...xingWithOtherConversions$ObjectToInt.class | Bin 0 -> 263 bytes ...gWithOtherConversions$ObjectToObject.class | Bin 0 -> 286 bytes .../BoxingWithOtherConversions.class | Bin 0 -> 2747 bytes .../BoxingWithOtherConversions.java | 33 ++++++++++++++++++ .../BroadenReturnTypeToObject.desc | 8 +++++ .../NarrowParameterToPrimitive.desc | 8 +++++ jbmc/src/java_bytecode/lambda_synthesis.cpp | 7 +--- 8 files changed, 50 insertions(+), 6 deletions(-) create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$IntToObject.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$ObjectToInt.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$ObjectToObject.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions.java create mode 100644 jbmc/regression/jbmc/lambda-boxing/BroadenReturnTypeToObject.desc create mode 100644 jbmc/regression/jbmc/lambda-boxing/NarrowParameterToPrimitive.desc diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$IntToObject.class b/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$IntToObject.class new file mode 100644 index 0000000000000000000000000000000000000000..2bd41109fa0e46e3a6f66e5fe6835927b944819d GIT binary patch literal 263 zcmZ{fy$ZrW5QJxAOkxtj#>U1*L>trC*(nGCA%%kV8IJrA?j&~xpUuJt@S((0D}^*W zyD;-H`*_~&0G8;x@LU80hovb$Yr=3A&vzwjSX42QMaik;sa_HMy}Z;Z-xd`ojMws7 zi0oMCJkdF?H&QgbR)rL5@y@yk3Db7dBo_K0zidMAbA_=GhFCGBxFQVxyAVe0Up#$4&7P_D5z&Gj}2f; literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$ObjectToInt.class b/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$ObjectToInt.class new file mode 100644 index 0000000000000000000000000000000000000000..d8feafc013fcd745c5f231a803a4057622c93013 GIT binary patch literal 263 zcmX^0Z`VEs1_l!bUUmi!b_Q-n2DZfH literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$ObjectToObject.class b/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$ObjectToObject.class new file mode 100644 index 0000000000000000000000000000000000000000..5483b2813f9d9984f2b58407d90710515c423694 GIT binary patch literal 286 zcmZ{fy$ZrW5QJwnCNV~_wy_a0jcM%c6a+y?pbPyYY_ literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions.class b/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions.class new file mode 100644 index 0000000000000000000000000000000000000000..18019ef4125d6875132efa89f6db17c07f2c9c41 GIT binary patch literal 2747 zcmbVOTUQfT6#fng83+lvSS@#28fges)M9M~t%6#qL8w73)T)Q%00UtLXC|nB#g{(z zr4O}T3oBi{Ja_dkwX5HmT)9P8A7;*N?{DvK?|t^nU;pm@4qzP5!#IYENzOmlvnxpm zOt&L}YhlE2y#w92p%1<=a5Ic{T?hpXc0Pu**UQz82`LDwIcoV<|1|c&2T+*GyL~ z7ga$(ED3}rP0REy3k1?5G!>k-3rZlCH7#|!w7IOD1uZO)%-VTbyeAz~uPd8DZ_RWC z`m$5@Gt*kVZ+dHU-Wr{=t!?GF+S-J`kf&Vlwsai(>AZC0rt*mTd`m6Z^NzV`dgeCq z1NJ#vV6+KRYA-1Q2TZM#Zl==^87f3`p3HB|$}Qi2hRP3LzxHp+v1LJ7ca&Fhtg?62 z;L$bn4Q8sY(cFZevf-lKTrS8|Q|Q!Lf#d1yy4;pyMQN>$m0>1EW|$i?OCCI8h#HWa z2Q_s@VE8cj!(as|woT@Xm1+p*?2?mLH%y)T!K2fAT00*>KL!NiQ?~87o+GzrmA7UW z+*k;Uah&I{6u~!m5W%;27{{YnI}E+?ID%gEMIf=Pm**qMgJs!O56IPO)m~@yI9ljY z9A^or^n8UtoqDpWUkqlVuE|WORYjFGkXg^s3=FJCuz@1|uWMIRKYX-atsH5Iac&~m zP=f*^O$4h|R35|FgcW8BVI_oQKCiZD=Tv&6S-I~;V8yqsD$j2f>;Y7*GxRqpa6CQJ zxLpR|{@te6YM-5^J~hxMuCXnPB{jDqaAL3JO2Q}-Qcp^<$i8yu-B{8g*%HXST_gzm z)@-zFQ!4vtGrXqd-P45p{>f__+ZSQdEGXA>RH0VN>_J|M?AUOZ3_OXzK`Fvd2+RMB zF5;m&glTQt8)_`;_Yz(zxgztP?L248XBVxm3_NAfvbMcZVqE@iyzv!)@_oE1twK?` zsj}omLowt$hwZy@XOE(8hyU-eY_hp-WBFCgPRn93XL^dg^qIiP0|7aVkHA24IlRxp zImR!vhFX)+k$DvH2A7&nkH zFgg$=m5*vvGy_fL(JuMcsYGj3M&CrGyF#{;Y`)t^^GF`O^tF#(_LIi|eI3L@vaIu1 z#3`KidCdBZ_VO4bmELGPtnUyh>U@rqh2R*@{E65O;=#v1aMhU9-iD-xaSk5?MBr7d zAY7;*L~964-H-b~Vhtcse4;_nh6}ZDj{8mkiDY62$rmt!-y<0K8LbCPOedxlEs-ni z4*1l!^BJ=U)?1J{P2hN_jsJ}abaCwF*u&AqHaxB-D3_t!By}(0G9Nv=iYY#N_9brd JDWA^b(tq<>zw-b9 literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions.java b/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions.java new file mode 100644 index 00000000000..727a448bdf7 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions.java @@ -0,0 +1,33 @@ +public class BoxingWithOtherConversions { + + interface ObjectToObject { + Object accept(Object o); + } + + interface IntToObject { + Object accept(int i); + } + + // Check we can narrow a parameter type down to a primitive + // which should be boxed and then upcast to Object by the + // generated lambda: + public static void testNarrowParameterTypeToPrimitive() { + ObjectToObject o2o = i -> ((Integer)i) + 1; + IntToObject i2o = o2o::accept; + assert o2o.accept(1).equals(2); + assert i2o.accept(1).equals(2); + assert false; + } + + interface ObjectToInt { + int accept(Object o); + } + + public static void testBroadenReturnTypeToObject() { + ObjectToInt o2i = o -> ((Integer)o).intValue() + 1; + ObjectToObject o2o = o2i::accept; + assert o2o.accept(1).equals(2); + assert o2i.accept(1) == 2; + assert false; + } +} diff --git a/jbmc/regression/jbmc/lambda-boxing/BroadenReturnTypeToObject.desc b/jbmc/regression/jbmc/lambda-boxing/BroadenReturnTypeToObject.desc new file mode 100644 index 00000000000..323f7e50e35 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/BroadenReturnTypeToObject.desc @@ -0,0 +1,8 @@ +CORE +BoxingWithOtherConversions +--function BoxingWithOtherConversions.testBroadenReturnTypeToObject --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^EXIT=10$ +^SIGNAL=0$ +\[java::BoxingWithOtherConversions\.testBroadenReturnTypeToObject:\(\)V.assertion\.1\] line 29 assertion at file BoxingWithOtherConversions\.java line 29 function java::BoxingWithOtherConversions\.testBroadenReturnTypeToObject:\(\)V bytecode-index 21: SUCCESS +\[java::BoxingWithOtherConversions\.testBroadenReturnTypeToObject:\(\)V.assertion\.2\] line 30 assertion at file BoxingWithOtherConversions\.java line 30 function java::BoxingWithOtherConversions\.testBroadenReturnTypeToObject:\(\)V bytecode-index 33: SUCCESS +\[java::BoxingWithOtherConversions\.testBroadenReturnTypeToObject:\(\)V.assertion\.3\] line 31 assertion at file BoxingWithOtherConversions\.java line 31 function java::BoxingWithOtherConversions\.testBroadenReturnTypeToObject:\(\)V bytecode-index 39: FAILURE diff --git a/jbmc/regression/jbmc/lambda-boxing/NarrowParameterToPrimitive.desc b/jbmc/regression/jbmc/lambda-boxing/NarrowParameterToPrimitive.desc new file mode 100644 index 00000000000..3e030f2708a --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/NarrowParameterToPrimitive.desc @@ -0,0 +1,8 @@ +CORE +BoxingWithOtherConversions +--function BoxingWithOtherConversions.testNarrowParameterTypeToPrimitive --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^EXIT=10$ +^SIGNAL=0$ +\[java::BoxingWithOtherConversions\.testNarrowParameterTypeToPrimitive:\(\)V.assertion.1\] line 17 assertion at file BoxingWithOtherConversions\.java line 17 function java::BoxingWithOtherConversions\.testNarrowParameterTypeToPrimitive:\(\)V bytecode-index 21: SUCCESS +\[java::BoxingWithOtherConversions\.testNarrowParameterTypeToPrimitive:\(\)V.assertion.2\] line 18 assertion at file BoxingWithOtherConversions\.java line 18 function java::BoxingWithOtherConversions\.testNarrowParameterTypeToPrimitive:\(\)V bytecode-index 34: SUCCESS +\[java::BoxingWithOtherConversions\.testNarrowParameterTypeToPrimitive:\(\)V.assertion.3\] line 19 assertion at file BoxingWithOtherConversions\.java line 19 function java::BoxingWithOtherConversions\.testNarrowParameterTypeToPrimitive:\(\)V bytecode-index 40: FAILURE diff --git a/jbmc/src/java_bytecode/lambda_synthesis.cpp b/jbmc/src/java_bytecode/lambda_synthesis.cpp index 89119d40c1c..75b04f9cf9e 100644 --- a/jbmc/src/java_bytecode/lambda_synthesis.cpp +++ b/jbmc/src/java_bytecode/lambda_synthesis.cpp @@ -662,17 +662,12 @@ exprt adjust_type_if_necessary( } else { - const irep_idt &boxed_type_id = - to_struct_tag_type(required_type.subtype()).get_identifier(); const auto *primitive_type_info = get_java_primitive_type_info(original_type); INVARIANT( primitive_type_info != nullptr, "A Java non-pointer type involved in a type disagreement should" " be a primitive"); - INVARIANT( - boxed_type_id == primitive_type_info->boxed_type_name, - "Boxed types are only convertable to their corresponding unboxed type"); symbol_exprt fresh_local = create_and_declare_local( function_id, role + "_boxed", required_type, symbol_table, code_block); @@ -682,7 +677,7 @@ exprt adjust_type_if_necessary( code_block.add(code_function_callt{ fresh_local, boxed_type_factory_method.symbol_expr(), {expr}}); - return std::move(fresh_local); + return typecast_exprt::conditional_cast(fresh_local, required_type); } } From 3942780f67a3be208650f74764e678ca8e18725b Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 27 May 2020 15:35:33 +0100 Subject: [PATCH 3/6] Java frontend: support lambda method references that imply primitive type widening For example, an int -> int method is a valid instantiation of a functional interface that expects a byte -> int, or one that expects an int -> long. In both cases it's down to the metafactory / our code that emulates its behaviour to add the widening cast. --- .../ByteToLong.desc | 7 ++ .../DoubleToFloat.desc | 7 ++ .../FloatToDouble.desc | 7 ++ .../IntToLong.desc | 7 ++ .../LongToByte.desc | 7 ++ .../LongToInt.desc | 7 ++ .../LongToShort.desc | 7 ++ .../ShortToLong.desc | 7 ++ .../Test$ByteToLong.class | Bin 0 -> 178 bytes .../Test$DoubleToDouble.class | Bin 0 -> 186 bytes .../Test$FloatToDouble.class | Bin 0 -> 184 bytes .../Test$IntToLong.class | Bin 0 -> 176 bytes .../Test$LongToLong.class | Bin 0 -> 178 bytes .../Test$ShortToInt.class | Bin 0 -> 178 bytes .../Test$ShortToLong.class | Bin 0 -> 180 bytes .../lambda-widening-conversions/Test.class | Bin 0 -> 3556 bytes .../lambda-widening-conversions/Test.java | 88 ++++++++++++++++++ jbmc/src/java_bytecode/lambda_synthesis.cpp | 29 ++++-- 18 files changed, 164 insertions(+), 9 deletions(-) create mode 100644 jbmc/regression/jbmc/lambda-widening-conversions/ByteToLong.desc create mode 100644 jbmc/regression/jbmc/lambda-widening-conversions/DoubleToFloat.desc create mode 100644 jbmc/regression/jbmc/lambda-widening-conversions/FloatToDouble.desc create mode 100644 jbmc/regression/jbmc/lambda-widening-conversions/IntToLong.desc create mode 100644 jbmc/regression/jbmc/lambda-widening-conversions/LongToByte.desc create mode 100644 jbmc/regression/jbmc/lambda-widening-conversions/LongToInt.desc create mode 100644 jbmc/regression/jbmc/lambda-widening-conversions/LongToShort.desc create mode 100644 jbmc/regression/jbmc/lambda-widening-conversions/ShortToLong.desc create mode 100644 jbmc/regression/jbmc/lambda-widening-conversions/Test$ByteToLong.class create mode 100644 jbmc/regression/jbmc/lambda-widening-conversions/Test$DoubleToDouble.class create mode 100644 jbmc/regression/jbmc/lambda-widening-conversions/Test$FloatToDouble.class create mode 100644 jbmc/regression/jbmc/lambda-widening-conversions/Test$IntToLong.class create mode 100644 jbmc/regression/jbmc/lambda-widening-conversions/Test$LongToLong.class create mode 100644 jbmc/regression/jbmc/lambda-widening-conversions/Test$ShortToInt.class create mode 100644 jbmc/regression/jbmc/lambda-widening-conversions/Test$ShortToLong.class create mode 100644 jbmc/regression/jbmc/lambda-widening-conversions/Test.class create mode 100644 jbmc/regression/jbmc/lambda-widening-conversions/Test.java diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/ByteToLong.desc b/jbmc/regression/jbmc/lambda-widening-conversions/ByteToLong.desc new file mode 100644 index 00000000000..52ac3ebd739 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-widening-conversions/ByteToLong.desc @@ -0,0 +1,7 @@ +CORE +Test +--function Test\.testByteToLong --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::Test\.testByteToLong:\(\)V.assertion\.1\] line 26 assertion at file Test\.java line 26 function java::Test\.testByteToLong:\(\)V bytecode-index 13: SUCCESS +\[java::Test\.testByteToLong:\(\)V.assertion\.2\] line 27 assertion at file Test\.java line 27 function java::Test\.testByteToLong:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/DoubleToFloat.desc b/jbmc/regression/jbmc/lambda-widening-conversions/DoubleToFloat.desc new file mode 100644 index 00000000000..d0efe27dff6 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-widening-conversions/DoubleToFloat.desc @@ -0,0 +1,7 @@ +CORE +Test +--function Test\.testDoubleToFloat --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::Test\.testDoubleToFloat:\(\)V.assertion\.1\] line 66 assertion at file Test\.java line 66 function java::Test\.testDoubleToFloat:\(\)V bytecode-index 13: SUCCESS +\[java::Test\.testDoubleToFloat:\(\)V.assertion\.2\] line 67 assertion at file Test\.java line 67 function java::Test\.testDoubleToFloat:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/FloatToDouble.desc b/jbmc/regression/jbmc/lambda-widening-conversions/FloatToDouble.desc new file mode 100644 index 00000000000..ad120047795 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-widening-conversions/FloatToDouble.desc @@ -0,0 +1,7 @@ +CORE +Test +--function Test\.testFloatToDouble --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::Test\.testFloatToDouble:\(\)V.assertion\.1\] line 44 assertion at file Test\.java line 44 function java::Test\.testFloatToDouble:\(\)V bytecode-index 13: SUCCESS +\[java::Test\.testFloatToDouble:\(\)V.assertion\.2\] line 45 assertion at file Test\.java line 45 function java::Test\.testFloatToDouble:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/IntToLong.desc b/jbmc/regression/jbmc/lambda-widening-conversions/IntToLong.desc new file mode 100644 index 00000000000..6d54e0e12fe --- /dev/null +++ b/jbmc/regression/jbmc/lambda-widening-conversions/IntToLong.desc @@ -0,0 +1,7 @@ +CORE +Test +--function Test\.testIntToLong --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::Test\.testIntToLong:\(\)V.assertion\.1\] line 38 assertion at file Test\.java line 38 function java::Test\.testIntToLong:\(\)V bytecode-index 13: SUCCESS +\[java::Test\.testIntToLong:\(\)V.assertion\.2\] line 39 assertion at file Test\.java line 39 function java::Test\.testIntToLong:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/LongToByte.desc b/jbmc/regression/jbmc/lambda-widening-conversions/LongToByte.desc new file mode 100644 index 00000000000..42ba4d87cc5 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-widening-conversions/LongToByte.desc @@ -0,0 +1,7 @@ +CORE +Test +--function Test\.testLongToByte --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::Test\.testLongToByte:\(\)V.assertion\.1\] line 72 assertion at file Test\.java line 72 function java::Test\.testLongToByte:\(\)V bytecode-index 13: SUCCESS +\[java::Test\.testLongToByte:\(\)V.assertion\.2\] line 73 assertion at file Test\.java line 73 function java::Test\.testLongToByte:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/LongToInt.desc b/jbmc/regression/jbmc/lambda-widening-conversions/LongToInt.desc new file mode 100644 index 00000000000..d29ecc6bf9d --- /dev/null +++ b/jbmc/regression/jbmc/lambda-widening-conversions/LongToInt.desc @@ -0,0 +1,7 @@ +CORE +Test +--function Test\.testLongToInt --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::Test\.testLongToInt:\(\)V.assertion\.1\] line 84 assertion at file Test\.java line 84 function java::Test\.testLongToInt:\(\)V bytecode-index 13: SUCCESS +\[java::Test\.testLongToInt:\(\)V.assertion\.2\] line 85 assertion at file Test\.java line 85 function java::Test\.testLongToInt:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/LongToShort.desc b/jbmc/regression/jbmc/lambda-widening-conversions/LongToShort.desc new file mode 100644 index 00000000000..5fe3458c69d --- /dev/null +++ b/jbmc/regression/jbmc/lambda-widening-conversions/LongToShort.desc @@ -0,0 +1,7 @@ +CORE +Test +--function Test\.testLongToShort --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::Test\.testLongToShort:\(\)V.assertion\.1\] line 78 assertion at file Test\.java line 78 function java::Test\.testLongToShort:\(\)V bytecode-index 13: SUCCESS +\[java::Test\.testLongToShort:\(\)V.assertion\.2\] line 79 assertion at file Test\.java line 79 function java::Test\.testLongToShort:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/ShortToLong.desc b/jbmc/regression/jbmc/lambda-widening-conversions/ShortToLong.desc new file mode 100644 index 00000000000..a43c99ea32c --- /dev/null +++ b/jbmc/regression/jbmc/lambda-widening-conversions/ShortToLong.desc @@ -0,0 +1,7 @@ +CORE +Test +--function Test\.testShortToLong --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::Test\.testShortToLong:\(\)V.assertion\.1\] line 32 assertion at file Test\.java line 32 function java::Test\.testShortToLong:\(\)V bytecode-index 13: SUCCESS +\[java::Test\.testShortToLong:\(\)V.assertion\.2\] line 33 assertion at file Test\.java line 33 function java::Test\.testShortToLong:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/Test$ByteToLong.class b/jbmc/regression/jbmc/lambda-widening-conversions/Test$ByteToLong.class new file mode 100644 index 0000000000000000000000000000000000000000..344354de37ad4405def45785b0c0c98cc0189a28 GIT binary patch literal 178 zcmYk0K?=e!5JmsgnAlp;L%7h5-FSiuf+D!E7l>gfmXb;n1+V7919&JgapmUE|L|t! zzdz3xfHfuxBZV;FRXT#;#4f1!5SAr6kf+59h)IcqlP(<>vqS@Mh+} zKhGC{EoKT6g(*QAYxy=1#Hw0X1bz1R-tzw1F(I!x44c+Gj6y+}r?@-sW`p&2R{Mfx9# y$~hhnz44wsVU=`cZ(LiR&K=v7kqjh(ki`}N3Bm*-UKyspDWT)m@q?g{%lr$X`6W>R literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/Test$ShortToLong.class b/jbmc/regression/jbmc/lambda-widening-conversions/Test$ShortToLong.class new file mode 100644 index 0000000000000000000000000000000000000000..9a489d6c4223c8cfebad906bc1f9a13f482983ce GIT binary patch literal 180 zcmY+8O$x#=5QX2=n%Ez~Lv*1VyYU8spa?G73&b!~OG%`O9?pda@K9pn&drLJ$Z^=mAhlm>>- zh=8C7zMuGZ)ESxLjQ;NUCpnJavzu%lWROZ{viIzH-1E8To_lxt=Ra3}2e1L(2Cxv1 zhAF2S&Cb4#aI|#j0dq8kNdaV-ar^WSV7!^ zi7@Ig6~yhB4#SVBFejN(@pJ&s;8_*Vsd!$&oR~Q=oG}unGb+&fvRNb7lhN~eBd_8G z1%UxGdo*FnQ^ku48hbOQZWSX`yriI^FH42v@v?$oe8kMTidQ&A_q4?v;-Fw|yUd-l z(q=XvOXqc_Pbp9iEAVekXVca;1>Q(>NP(}%Oc@HA2GUt$@5I=!kxPiPg7AQu)H6eR zE-mi`rOz5k=Q+nf!pK`)%$aeqIaQ=T+Rr3Y{BfL)#5{t%Y<8O||_;OzF@cN8` zW_#ZDl7T52J5r8G=rAY#zrD=QcV@rgc<(oT}8`0lbIzWxuy(%EVH5j|;{xoMubvC^B0ujQsP&C!W*1%E{bu9?7T z(%pJCl`-<|j%QbyTinW}c}mJOh0IQ1VtU;8e?}+e^<$&grtQ%)nRwbVcy7N@&~ZcS zQLyOxe*D6<^2-P)p#^d}DTVkE9>^%?x3tW4p>8H zph0$$8VO#*52c5rZ&5)1o@06Jys}sy*5gh)mJLuHySyp+V^!?@s@P3->}D5wl6eJs z-Bn4y=Vy2?Vc|;O416B6pzi!d1b>5i=nCrpux;*}EYNE&P`>eCW&Hfix8YVU>NYp2 zpNrdqyJ)|gzXo{zMw^PRMv7Z&F*H;#1ZK&wm<&tEu#^mK6%6-aTNT5-!mzy-L$HED znFko{p`aNXTPI!c_(giCzHPJFLWaBo?6l8s-rj8jOL|Pi0&-pu9Mu= z!CT6L>)h150IP#}2+sUa#l5W}_&zwN;6Sa)H316n^Y7y>hB5r$cu#9d_AO@=-)^j9$4j|Zw44hh5IS`71UieZopd&#hm z4Et|{;lWxA^KXhFPKE>-4w7N$zZvTBkjt=vO(lQL;nrWV;1X2dW%#_mzz=FT_^d>TlqGJ*`;8aWTgw9OYBe#&H?Pc8(n!mvj6AU*St$ wrH?WG0P3N0&S50^6KRCfh%Jp$8nvY?Ok`~-hdgq&G>IoLS&*J|rKd3YFHujx+W-In literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/Test.java b/jbmc/regression/jbmc/lambda-widening-conversions/Test.java new file mode 100644 index 00000000000..e986553b5ba --- /dev/null +++ b/jbmc/regression/jbmc/lambda-widening-conversions/Test.java @@ -0,0 +1,88 @@ +public class Test { + + // Tests for widening a parameter: + + public interface ByteToLong { + public long accept(byte b); + } + + public interface ShortToLong { + public long accept(short s); + } + + public interface IntToLong { + public long accept(int i); + } + + public interface FloatToDouble { + public double accept(float f); + } + + public static long longToLong(long x) { return x + 1L; } + public static double doubleToDouble(double x) { return x + 1.0; } + + public static void testByteToLong() { + ByteToLong b2l = Test::longToLong; + assert b2l.accept((byte)1) == 2L; + assert false; + } + + public static void testShortToLong() { + ShortToLong s2l = Test::longToLong; + assert s2l.accept((short)1) == 2L; + assert false; + } + + public static void testIntToLong() { + IntToLong i2l = Test::longToLong; + assert i2l.accept(1) == 2L; + assert false; + } + + public static void testFloatToDouble() { + FloatToDouble f2d = Test::doubleToDouble; + assert f2d.accept(1.0f) == 2.0; + assert false; + } + + // Tests for widening a return value: + + public interface LongToLong { + public long accept(long l); + } + + public static byte longToByte(long l) { return (byte)(l + 1); } + public static short longToShort(long l) { return (short)(l + 1); } + public static int longToInt(long l) { return (int)(l + 1); } + + public interface DoubleToDouble { + public double accept(double d); + } + + public static float doubleToFloat(double d) { return (float)(d + 1); } + + public static void testDoubleToFloat() { + DoubleToDouble d2d = Test::doubleToFloat; + assert d2d.accept(1.0) == 2.0; + assert false; + } + + public static void testLongToByte() { + LongToLong l2l = Test::longToByte; + assert l2l.accept(1L) == 2L; + assert false; + } + + public static void testLongToShort() { + LongToLong l2l = Test::longToShort; + assert l2l.accept(1L) == 2L; + assert false; + } + + public static void testLongToInt() { + LongToLong l2l = Test::longToInt; + assert l2l.accept(1L) == 2L; + assert false; + } + +} diff --git a/jbmc/src/java_bytecode/lambda_synthesis.cpp b/jbmc/src/java_bytecode/lambda_synthesis.cpp index 75b04f9cf9e..31c7e32fef8 100644 --- a/jbmc/src/java_bytecode/lambda_synthesis.cpp +++ b/jbmc/src/java_bytecode/lambda_synthesis.cpp @@ -616,7 +616,7 @@ static symbol_exprt instantiate_new_object( /// unchanged. \p role is a suggested name prefix for any temporary variable /// needed; \p function_id is the id of the function any created code it /// added to. -exprt adjust_type_if_necessary( +exprt box_or_unbox_type_if_necessary( exprt expr, const typet &required_type, code_blockt &code_block, @@ -630,10 +630,7 @@ exprt adjust_type_if_necessary( if(original_is_pointer == required_is_pointer) { - if(original_is_pointer && original_type != required_type) - return typecast_exprt{expr, required_type}; - else - return expr; + return expr; } // One is a pointer, the other a primitive -- box or unbox as necessary, and @@ -647,9 +644,6 @@ exprt adjust_type_if_necessary( boxed_type_info != nullptr, "Only boxed primitive types should participate in a pointer vs." " primitive type disagreement"); - INVARIANT( - required_type == boxed_type_info->corresponding_primitive_type, - "Boxed types are only convertable to their corresponding unboxed type"); symbol_exprt fresh_local = create_and_declare_local( function_id, role + "_unboxed", required_type, symbol_table, code_block); @@ -677,10 +671,27 @@ exprt adjust_type_if_necessary( code_block.add(code_function_callt{ fresh_local, boxed_type_factory_method.symbol_expr(), {expr}}); - return typecast_exprt::conditional_cast(fresh_local, required_type); + return std::move(fresh_local); } } +/// Box or unbox expr as per \ref box_or_unbox_type_if_necessary, then cast the +/// result to \p required_type. If the source is legal Java that should mean a +/// pointer upcast or primitive widening conversion, but this is not checked. +exprt adjust_type_if_necessary( + exprt expr, + const typet &required_type, + code_blockt &code_block, + symbol_table_baset &symbol_table, + const irep_idt &function_id, + const std::string &role) +{ + return typecast_exprt::conditional_cast( + box_or_unbox_type_if_necessary( + expr, required_type, code_block, symbol_table, function_id, role), + required_type); +} + /// Create the body for the synthetic method implementing an invokedynamic /// method. For most lambdas this means creating a simple function body like /// TR new_synthetic_method(T1 param1, T2 param2, ...) { From 200c9364052d62252ea863d3cdaefbdd287eab05 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 27 May 2020 16:17:49 +0100 Subject: [PATCH 4/6] Add tests for lambdas that perform simeltaneous primitive widening and boxing/unboxing --- .../jbmc/lambda-boxing/ByteToLong.desc | 7 ++ .../jbmc/lambda-boxing/DoubleToFloat.desc | 7 ++ .../jbmc/lambda-boxing/FloatToDouble.desc | 7 ++ .../jbmc/lambda-boxing/IntToLong.desc | 7 ++ .../jbmc/lambda-boxing/LongToByte.desc | 7 ++ .../jbmc/lambda-boxing/LongToInt.desc | 7 ++ .../jbmc/lambda-boxing/LongToShort.desc | 7 ++ ...imitiveWideningWithBoxing$ByteToLong.class | Bin 0 -> 277 bytes ...iveWideningWithBoxing$DoubleToDouble.class | Bin 0 -> 255 bytes ...tiveWideningWithBoxing$FloatToDouble.class | Bin 0 -> 286 bytes ...rimitiveWideningWithBoxing$IntToLong.class | Bin 0 -> 278 bytes ...imitiveWideningWithBoxing$LongToLong.class | Bin 0 -> 247 bytes ...mitiveWideningWithBoxing$ShortToLong.class | Bin 0 -> 280 bytes .../PrimitiveWideningWithBoxing.class | Bin 0 -> 4709 bytes .../PrimitiveWideningWithBoxing.java | 88 ++++++++++++++++++ .../jbmc/lambda-boxing/ShortToLong.desc | 7 ++ 16 files changed, 144 insertions(+) create mode 100644 jbmc/regression/jbmc/lambda-boxing/ByteToLong.desc create mode 100644 jbmc/regression/jbmc/lambda-boxing/DoubleToFloat.desc create mode 100644 jbmc/regression/jbmc/lambda-boxing/FloatToDouble.desc create mode 100644 jbmc/regression/jbmc/lambda-boxing/IntToLong.desc create mode 100644 jbmc/regression/jbmc/lambda-boxing/LongToByte.desc create mode 100644 jbmc/regression/jbmc/lambda-boxing/LongToInt.desc create mode 100644 jbmc/regression/jbmc/lambda-boxing/LongToShort.desc create mode 100644 jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$ByteToLong.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$DoubleToDouble.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$FloatToDouble.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$IntToLong.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$LongToLong.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$ShortToLong.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing.class create mode 100644 jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing.java create mode 100644 jbmc/regression/jbmc/lambda-boxing/ShortToLong.desc diff --git a/jbmc/regression/jbmc/lambda-boxing/ByteToLong.desc b/jbmc/regression/jbmc/lambda-boxing/ByteToLong.desc new file mode 100644 index 00000000000..98cb8352af9 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/ByteToLong.desc @@ -0,0 +1,7 @@ +CORE +PrimitiveWideningWithBoxing +--function PrimitiveWideningWithBoxing\.testByteToLong --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::PrimitiveWideningWithBoxing\.testByteToLong:\(\)V\.assertion\.1\] line 26 assertion at file PrimitiveWideningWithBoxing\.java line 26 function java::PrimitiveWideningWithBoxing\.testByteToLong:\(\)V bytecode-index 15: SUCCESS +\[java::PrimitiveWideningWithBoxing\.testByteToLong:\(\)V\.assertion\.2\] line 27 assertion at file PrimitiveWideningWithBoxing\.java line 27 function java::PrimitiveWideningWithBoxing\.testByteToLong:\(\)V bytecode-index 21: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/DoubleToFloat.desc b/jbmc/regression/jbmc/lambda-boxing/DoubleToFloat.desc new file mode 100644 index 00000000000..fdad63da3f0 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/DoubleToFloat.desc @@ -0,0 +1,7 @@ +CORE +PrimitiveWideningWithBoxing +--function PrimitiveWideningWithBoxing\.testDoubleToFloat --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::PrimitiveWideningWithBoxing\.testDoubleToFloat:\(\)V\.assertion\.1\] line 66 assertion at file PrimitiveWideningWithBoxing\.java line 66 function java::PrimitiveWideningWithBoxing\.testDoubleToFloat:\(\)V bytecode-index 13: SUCCESS +\[java::PrimitiveWideningWithBoxing\.testDoubleToFloat:\(\)V\.assertion\.2\] line 67 assertion at file PrimitiveWideningWithBoxing\.java line 67 function java::PrimitiveWideningWithBoxing\.testDoubleToFloat:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/FloatToDouble.desc b/jbmc/regression/jbmc/lambda-boxing/FloatToDouble.desc new file mode 100644 index 00000000000..be843d74d41 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/FloatToDouble.desc @@ -0,0 +1,7 @@ +CORE +PrimitiveWideningWithBoxing +--function PrimitiveWideningWithBoxing\.testFloatToDouble --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::PrimitiveWideningWithBoxing\.testFloatToDouble:\(\)V\.assertion\.1\] line 44 assertion at file PrimitiveWideningWithBoxing\.java line 44 function java::PrimitiveWideningWithBoxing\.testFloatToDouble:\(\)V bytecode-index 15: SUCCESS +\[java::PrimitiveWideningWithBoxing\.testFloatToDouble:\(\)V\.assertion\.2\] line 45 assertion at file PrimitiveWideningWithBoxing\.java line 45 function java::PrimitiveWideningWithBoxing\.testFloatToDouble:\(\)V bytecode-index 21: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/IntToLong.desc b/jbmc/regression/jbmc/lambda-boxing/IntToLong.desc new file mode 100644 index 00000000000..1b2ac0969bd --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/IntToLong.desc @@ -0,0 +1,7 @@ +CORE +PrimitiveWideningWithBoxing +--function PrimitiveWideningWithBoxing\.testIntToLong --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::PrimitiveWideningWithBoxing\.testIntToLong:\(\)V\.assertion\.1\] line 38 assertion at file PrimitiveWideningWithBoxing\.java line 38 function java::PrimitiveWideningWithBoxing\.testIntToLong:\(\)V bytecode-index 15: SUCCESS +\[java::PrimitiveWideningWithBoxing\.testIntToLong:\(\)V\.assertion\.2\] line 39 assertion at file PrimitiveWideningWithBoxing\.java line 39 function java::PrimitiveWideningWithBoxing\.testIntToLong:\(\)V bytecode-index 21: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/LongToByte.desc b/jbmc/regression/jbmc/lambda-boxing/LongToByte.desc new file mode 100644 index 00000000000..f1e6c90c057 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/LongToByte.desc @@ -0,0 +1,7 @@ +CORE +PrimitiveWideningWithBoxing +--function PrimitiveWideningWithBoxing\.testLongToByte --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::PrimitiveWideningWithBoxing\.testLongToByte:\(\)V\.assertion\.1\] line 72 assertion at file PrimitiveWideningWithBoxing\.java line 72 function java::PrimitiveWideningWithBoxing\.testLongToByte:\(\)V bytecode-index 13: SUCCESS +\[java::PrimitiveWideningWithBoxing\.testLongToByte:\(\)V\.assertion\.2\] line 73 assertion at file PrimitiveWideningWithBoxing\.java line 73 function java::PrimitiveWideningWithBoxing\.testLongToByte:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/LongToInt.desc b/jbmc/regression/jbmc/lambda-boxing/LongToInt.desc new file mode 100644 index 00000000000..cd2c541f4f1 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/LongToInt.desc @@ -0,0 +1,7 @@ +CORE +PrimitiveWideningWithBoxing +--function PrimitiveWideningWithBoxing\.testLongToInt --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::PrimitiveWideningWithBoxing\.testLongToInt:\(\)V\.assertion\.1\] line 84 assertion at file PrimitiveWideningWithBoxing\.java line 84 function java::PrimitiveWideningWithBoxing\.testLongToInt:\(\)V bytecode-index 13: SUCCESS +\[java::PrimitiveWideningWithBoxing\.testLongToInt:\(\)V\.assertion\.2\] line 85 assertion at file PrimitiveWideningWithBoxing\.java line 85 function java::PrimitiveWideningWithBoxing\.testLongToInt:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/LongToShort.desc b/jbmc/regression/jbmc/lambda-boxing/LongToShort.desc new file mode 100644 index 00000000000..ee538f24a55 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/LongToShort.desc @@ -0,0 +1,7 @@ +CORE +PrimitiveWideningWithBoxing +--function PrimitiveWideningWithBoxing\.testLongToShort --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::PrimitiveWideningWithBoxing\.testLongToShort:\(\)V\.assertion\.1\] line 78 assertion at file PrimitiveWideningWithBoxing\.java line 78 function java::PrimitiveWideningWithBoxing\.testLongToShort:\(\)V bytecode-index 13: SUCCESS +\[java::PrimitiveWideningWithBoxing\.testLongToShort:\(\)V\.assertion\.2\] line 79 assertion at file PrimitiveWideningWithBoxing\.java line 79 function java::PrimitiveWideningWithBoxing\.testLongToShort:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$ByteToLong.class b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$ByteToLong.class new file mode 100644 index 0000000000000000000000000000000000000000..1ae3abc95325ebdd8d12a82da749220e6b27aaaa GIT binary patch literal 277 zcmaKnK@Y(|5QX1RTZ+WpMMQ)P7dN*`BoYY;iSt^M+NQSBR>NO&@B{oPv323(GV^Bg z^39v)>;3>RLDNOmMV%m|Qhd$`-N7=Hxg1B*1Y`e}@pSmJSjHxp61+`(Nfgg@#DvZ| z(I=hhoOk-bMw?)#v!fqhtr`_97Y#!HkE>VQ*~SIjvVVuh!Wd3wkxWxg39WCm)jnip h^S1wR1%Xhqj{@Wn%5bbIq4KE$p6#A>5M0zm?G1eaOj7^= literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$DoubleToDouble.class b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$DoubleToDouble.class new file mode 100644 index 0000000000000000000000000000000000000000..689faea2b5e1e2187258de88807eb693eddbe5ab GIT binary patch literal 255 zcmaJ+zYf7*9K0XZYL(b61_K6NJOPcwL_*T}YyDDRQ(vY3;@J!yz(a`-o1x3y<#M^) zJzw_+fF=4Cx)yo_Q$!J8OM)@=XFkC>WK|yVMy5;{?{j&PrK~xSCstC$fh^Cf?55Qs z5w)=366Ou5iJw(r%E#=-gu%bzZk6JEorT4UJBRTq2Q>kX*gagq5``cSn3Sg%99EiFFF1(9FD< zy!__P{c*hk7$9&_aZw{UB98f(5!#*EUYtc=3BB!y%7|>({n|{-X{~rj@RsJ3#2iY+ zgytfV2bsw;M{>hj>TM*m-N;<5>b-C-d_wn+tCgQxnKz#h{LKDTYfi>Wq$#I_`X}Rj lz312lZ~UP<1VX`n3{Z(sM9HcG%6WC*+3r~f!9~@nJ^>QgPvZap literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$IntToLong.class b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$IntToLong.class new file mode 100644 index 0000000000000000000000000000000000000000..900fdb95cfa62fbb24f0048b997213b595e0755b GIT binary patch literal 278 zcmaKny$ZrW5QJy_$(g8NZ)2gLjW%}a6a+y~P)L2oC0>XZxtzggv+x0YDDkw>%4T;M zhHqyd&)Xfq6m5ZqK$GCfIOek@42G*zmU5CwolKV6a>6DY{dlWfCm|u&<`)z5LS;Y39#| z;W6|6JYN77=yP;AdITooSl&v4GYw}U!8@3H9?P}LBw@7A)m4?Ml94(~t#lHp^0G7! z>*lGb1cy(UG^EB`qm!el)w2H|f1|a`SD7dZSr7&_F35yVg54>Vv28SL;4%WCWv2k- V5ZZ98YoYT~2G3s4CI}oZbHBBiK}!Gt literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$ShortToLong.class b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$ShortToLong.class new file mode 100644 index 0000000000000000000000000000000000000000..8c7d5b4fee36086424ea5fc2ef2ab5c5e2937db2 GIT binary patch literal 280 zcmaKny$ZrW5QJx=Cgw-5w-FT7MjN|y3W5+&h>-e>M{*(FNfLw4X5j<)P~vH$Ha5Gn z%kb^&{c*hkn4@E%ZNVj&EROl9A`Hes#%eapnM`J3s*1{=d~E_H6QAIO>RiNpC2~&a zZwql0m8f|n4qOVEM50O;>Y~;31+(B0Mt@wx_o1D7(FyL)})XG5XT}?Q;JK908V4L<6**Zzd75;8^v(ufOB-pG#5-*4tV=A7?*_ndRjy_>iH zedP@RH{+i=Hef2pekqME%;+e?$zVHXb$l9?R(_Db77bM$X^~Wz(=m_FWYB}NIke!j zIzET{GT4UC=a9e`bbJwC%3uo~)bS9$oZ9ap068S_NCq46)f`%JK7$+aXbvfy&q2d^ z4Ug-10^iW^q=u&y+J~LF$&xkh_^pC5QZ8GSp^{mxT2&3-RM1DA^3=E^Zw=p4XggSP zOm|sB!_x}skuoQIiEk@p#-^Q0ZQ>b13@*5|Ap#25bPIOHwViTx*shv1UsO;h6;gZc zvhD6uNaTAa6p}+u(NgFbwaeDgxtU3;GA_ajxlyNJmL|-KE#qJ^=}y~Kg|5-#6??{Z z?Ro2jU9`$}dFq7iP7gX~*&860Qf)P~kU!jWn6}UIVcTA8a7Hpe+%wE?eA->B>V}t* znA}xT$j6!MuFKPM+n8$>&KxmkJ;EC3mkt39Ig2Z=3TjU*YDi%~1O445Ftrd6#1@ck zu^=^ZLNJ1>1tJny!kpU0z-*6&iKq~Y`4MKQKYH4nH~ULwd8%LHKhP7J5E*(# zk!?0K?a48X{7`wzRk$%0$rB<}+SlRg6t=`_P{f+DDiWCGuzQPX(DV02gtaFowCSB( zh;|?vIMW}EI{|2-D9+pw>&#`90Lb5<5*TsFxZ`^?QCd0ge0g~@B;3MYp81o3H@%ec zXFOl6+FK|En@=Be<|+m2peqAh<0lGh>M3$yxis8XsW_D^o)giZYIt7sekOzG zvUow-pKJJqO#V^^FJy6%rhX;;7d5;jA6}NhMGdbQcoo0SVt@j_k-1Cq8pvV~CoW5W zQC>1y;&Vk|UCg32yk_8a{FY0uvpzO?+A1*PdSev3qtR8^8Yf(jAge)~U}OU_cjIJh zd!EH1PA*hnR-joga5~<=n+^Nj+uq^*?q#IT1Mn>td$UlmX2ogw_;Odb!9CYrce=kF zw0W~MXB|7mb0t3*w&fX*D2Vl-LQIH~ch0cvM=Fb7NWwrKY1Y9NXoj3do*i|b!H(<9 zkA+cvI}OEVxh91L1M@vAn6Jf_##h&k2Z##S${wQjH ziUiWT6w#AKt7=!QVy#s1TzBVq_28}Lq=r8m_zT`Pup4^}d+>NscSW)9j6$z&6mY>qG)!f*qV z+l0x%W=z^6Ogfg3y?Q2F$Yd*-Y$KC=gvsqV)WBp!m>h1#WObd1v54Fft`R1kow)Yt zcO9MWWU_-Cc9Kb7gvlKkZD4Xln6R`2Ikr2<6Qh?Yp_`99!3=qcD&aicU4xWNKaP*` zds-^f|G;>15k@1%o~9TqYyrkC0gp_;V-X#V5VwXPGBp}3l}#WzI|`4}n~f0rA`l24BAYebBN6#z zGY)I(9P}kzFC4C7&)!ZBhsa@s(1#-&?!~7XIGDm=vKfbU?}@_^ayUv3#|VA=-Eb&0 z<8Z@!;xI-I|9q0Z7ekE#Y literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing.java b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing.java new file mode 100644 index 00000000000..0a0fc526362 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing.java @@ -0,0 +1,88 @@ +public class PrimitiveWideningWithBoxing { + + // Tests for widening a parameter, accompanied by boxing and unboxing: + + public interface ByteToLong { + public Long accept(Byte b); + } + + public interface ShortToLong { + public Long accept(Short s); + } + + public interface IntToLong { + public Long accept(Integer i); + } + + public interface FloatToDouble { + public Double accept(Float f); + } + + public static long longToLong(long x) { return x + 1L; } + public static double doubleToDouble(double x) { return x + 1.0; } + + public static void testByteToLong() { + ByteToLong b2l = PrimitiveWideningWithBoxing::longToLong; + assert b2l.accept((byte)1) == 2L; + assert false; + } + + public static void testShortToLong() { + ShortToLong s2l = PrimitiveWideningWithBoxing::longToLong; + assert s2l.accept((short)1) == 2L; + assert false; + } + + public static void testIntToLong() { + IntToLong i2l = PrimitiveWideningWithBoxing::longToLong; + assert i2l.accept(1) == 2L; + assert false; + } + + public static void testFloatToDouble() { + FloatToDouble f2d = PrimitiveWideningWithBoxing::doubleToDouble; + assert f2d.accept(1.0f) == 2.0; + assert false; + } + + // Tests for widening a return value, accompanied by boxing and unboxing: + + public interface LongToLong { + public long accept(long l); + } + + public static Byte longToByte(Long l) { return (byte)(l + 1); } + public static Short longToShort(Long l) { return (short)(l + 1); } + public static Integer longToInt(Long l) { return (int)(l + 1); } + + public interface DoubleToDouble { + public double accept(double d); + } + + public static Float doubleToFloat(Double d) { return (float)(d + 1); } + + public static void testDoubleToFloat() { + DoubleToDouble d2d = PrimitiveWideningWithBoxing::doubleToFloat; + assert d2d.accept(1.0) == 2.0; + assert false; + } + + public static void testLongToByte() { + LongToLong l2l = PrimitiveWideningWithBoxing::longToByte; + assert l2l.accept(1L) == 2L; + assert false; + } + + public static void testLongToShort() { + LongToLong l2l = PrimitiveWideningWithBoxing::longToShort; + assert l2l.accept(1L) == 2L; + assert false; + } + + public static void testLongToInt() { + LongToLong l2l = PrimitiveWideningWithBoxing::longToInt; + assert l2l.accept(1L) == 2L; + assert false; + } + +} diff --git a/jbmc/regression/jbmc/lambda-boxing/ShortToLong.desc b/jbmc/regression/jbmc/lambda-boxing/ShortToLong.desc new file mode 100644 index 00000000000..e147a202209 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/ShortToLong.desc @@ -0,0 +1,7 @@ +CORE +PrimitiveWideningWithBoxing +--function PrimitiveWideningWithBoxing\.testShortToLong --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::PrimitiveWideningWithBoxing\.testShortToLong:\(\)V\.assertion\.1\] line 32 assertion at file PrimitiveWideningWithBoxing\.java line 32 function java::PrimitiveWideningWithBoxing\.testShortToLong:\(\)V bytecode-index 15: SUCCESS +\[java::PrimitiveWideningWithBoxing\.testShortToLong:\(\)V\.assertion\.2\] line 33 assertion at file PrimitiveWideningWithBoxing\.java line 33 function java::PrimitiveWideningWithBoxing\.testShortToLong:\(\)V bytecode-index 21: FAILURE +^EXIT=10$ +^SIGNAL=0$ From dbe56e7b982d736c52167be093589c8a13fb4c78 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 27 May 2020 16:38:54 +0100 Subject: [PATCH 5/6] Clean up uses of is_primitive_wrapper_type_name that derive the name from a symbol-table id These users start with an irep_idt, so it's cheaper to look up by id than to create a derived string and then look up by that. --- jbmc/src/java_bytecode/assignments_from_json.cpp | 3 +-- jbmc/src/java_bytecode/java_utils.cpp | 5 +++++ jbmc/src/java_bytecode/java_utils.h | 6 +++++- 3 files changed, 11 insertions(+), 3 deletions(-) diff --git a/jbmc/src/java_bytecode/assignments_from_json.cpp b/jbmc/src/java_bytecode/assignments_from_json.cpp index 1ebe0f7b032..8a72fb858e2 100644 --- a/jbmc/src/java_bytecode/assignments_from_json.cpp +++ b/jbmc/src/java_bytecode/assignments_from_json.cpp @@ -544,8 +544,7 @@ static code_with_references_listt assign_struct_components_from_json( { const auto member_json = [&]() -> jsont { if( - is_primitive_wrapper_type_name(id2string( - strip_java_namespace_prefix(java_class_type.get_name()))) && + is_primitive_wrapper_type_id(java_class_type.get_name()) && id2string(component_name) == "value") { return get_untyped_primitive(json); diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index 2a0067fc9fa..6690c8799a6 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/jbmc/src/java_bytecode/java_utils.cpp @@ -104,6 +104,11 @@ get_java_primitive_type_info(const typet &maybe_primitive_type) return found == type_info_by_primitive_type.end() ? nullptr : &found->second; } +bool is_primitive_wrapper_type_id(const irep_idt &id) +{ + return get_boxed_type_info_by_name(id) != nullptr; +} + bool is_primitive_wrapper_type_name(const std::string &type_name) { static const std::unordered_set primitive_wrapper_type_names = { diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h index dd5d4f37762..ee4767c409a 100644 --- a/jbmc/src/java_bytecode/java_utils.h +++ b/jbmc/src/java_bytecode/java_utils.h @@ -62,8 +62,12 @@ struct java_boxed_type_infot const java_boxed_type_infot * get_boxed_type_info_by_name(const irep_idt &type_name); +/// Returns true iff the argument is the symbol-table identifier of a Java +/// primitive wrapper type (for example, java::java.lang.Byte) +bool is_primitive_wrapper_type_id(const irep_idt &id); + /// Returns true iff the argument is the fully qualified name of a Java -/// primitive wrapper type. +/// primitive wrapper type (for example, java.lang.Byte) bool is_primitive_wrapper_type_name(const std::string &type_name); void generate_class_stub( From 70f972963abc66b4be0e0f3ea5c03fa98feb17b2 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 27 May 2020 17:33:14 +0100 Subject: [PATCH 6/6] Java frontend: handle lambdas that adapt a method with a return type to an interface method returning void --- .../Test$IntToVoid.class | Bin 0 -> 177 bytes .../Test$IntegerToVoid.class | Bin 0 -> 203 bytes .../Test$ObjectToVoid.class | Bin 0 -> 200 bytes .../jbmc/lambda-void-return-type/Test.class | Bin 0 -> 1931 bytes .../jbmc/lambda-void-return-type/Test.java | 31 ++++++++++++++++++ .../jbmc/lambda-void-return-type/test.desc | 9 +++++ jbmc/src/java_bytecode/lambda_synthesis.cpp | 2 +- 7 files changed, 41 insertions(+), 1 deletion(-) create mode 100644 jbmc/regression/jbmc/lambda-void-return-type/Test$IntToVoid.class create mode 100644 jbmc/regression/jbmc/lambda-void-return-type/Test$IntegerToVoid.class create mode 100644 jbmc/regression/jbmc/lambda-void-return-type/Test$ObjectToVoid.class create mode 100644 jbmc/regression/jbmc/lambda-void-return-type/Test.class create mode 100644 jbmc/regression/jbmc/lambda-void-return-type/Test.java create mode 100644 jbmc/regression/jbmc/lambda-void-return-type/test.desc diff --git a/jbmc/regression/jbmc/lambda-void-return-type/Test$IntToVoid.class b/jbmc/regression/jbmc/lambda-void-return-type/Test$IntToVoid.class new file mode 100644 index 0000000000000000000000000000000000000000..e5bc44b5db115c2c692817d09cd1269001b0b026 GIT binary patch literal 177 zcmYjLI}XAy41F%4p`{=W!2k>SjAM?D|;(Xm(J+GA7VTu5E3o{kRVJTm?fD0W{R9K=L>FzEX}@ifF$7n literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-void-return-type/Test$IntegerToVoid.class b/jbmc/regression/jbmc/lambda-void-return-type/Test$IntegerToVoid.class new file mode 100644 index 0000000000000000000000000000000000000000..88e17290fb0add11061297e63e4664e5ed46973b GIT binary patch literal 203 zcmZ9G!3u&v7=-6HbJG;ULr>75E_vzJF$jd9L*jk2A5m-90(fFAuf6$)u60Oj6Zx$?bNP6M~cO+k*F1V<|sl)2#2hX4Qo literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-void-return-type/Test.class b/jbmc/regression/jbmc/lambda-void-return-type/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..8f97e53a0510cc1495c0fa0f88e3a3ee543d9d19 GIT binary patch literal 1931 zcmbVN&sQ5&7`-nUGRZJBAy7ooT9Il_$YLr3 z4bukB;k=I54Q{4X_>DXvrC#JPqX4ry<_s8^%0r-(M*<}S3%I0XQO9M0%(4?y+zr>R z37E@{BfZ7C<@?g-mWyD)+iC7gClCk_wro3cwYk47y@~=0uE*hj`ReEcv8M&9axif%h{PETE%(0H^i-N-;q@k9DfoPg^AJv<{~klOn4#E zAQ#p!Mz%;5B8~R(bob_*K;L>`Rrgk`M%V|Z5K5Y!sn%mLjCHr^Rpk|1wVqMkO{j`Z zJcD5q0~pk?Wa0`&S&uq3@eZyEJJ6Oq$5h%*y8`_k3`K~f)(@alM}8onSLqd6h=mrS`Hml!SRq6B4LYWiKF%{#lfLcATDv)l z9yDneI&DkGhbA_0)5Hn9XyPS|ns^yw0;3%s+c|Lez8{)Vgg|1J}Dtr|frj zIzCYjbltsXL*UOsm$hPoXckv3r&gE#ScEKf!PW!Mc6PcWPh70rZOH$37^Qsr-R@b$ zX&0?}eccXZNyn!Gr~V_zQT+&P5CIs) zhY-c&&q#b9-g=I2gJ&R4LlPrgnOv*r^LQbQbCxm7ERhPEDUOg~M7#AZHwh>bl@6p( z1Va%hCLkOqSsH)c$`LWud`xAwsD456yF+X}U2JBX&1|#LS~1&P%w~jai6gjDU0ki! zRFhF<8JucKB?{!ySjpFqp=~}y&-LQw1Eg*|f)12Vr+-B{fgg~$hk@cxNTk0(?_(GQ z_Ws@in!w7LoY6rJDrC+$0@??xp3P+sL$h7bFjqT=8e1|{e42v-`jDmp2Kj**K|iKw zf?4jCXo8y@|1P^~&;VcX^ec{2O{d82()bdugyS8==Xezb>Nv|^?l@No-kKn)z&xjk zABOffrgWUqarQ41+i#V5qNN%?gKGXje_nflWA~tI_n{?!M5g1j$RZ*n?Loqv=br{9 sc_)F_puUspdzfQ&{izJL@G(AO^6lDG?eF5)dd(dzB?Y91H=1z0PQOaK4? literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lambda-void-return-type/Test.java b/jbmc/regression/jbmc/lambda-void-return-type/Test.java new file mode 100644 index 00000000000..f6d32102cd2 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-void-return-type/Test.java @@ -0,0 +1,31 @@ +public class Test { + + public int lastArgument = 0; + public int intToInt(int x) { lastArgument = x; return x + 1; } + public Integer intToInteger(int x) { lastArgument = x; return x + 1; } + public Object intToObject(int x) { lastArgument = x; return -1; } + + public interface IntToVoid { + void consume(int x); + } + + public static void test() { + Test t = new Test(); + + IntToVoid intToVoid = t::intToInt; + intToVoid.consume(5); + assert t.lastArgument == 5; + + IntToVoid intToVoid2 = t::intToInteger; + intToVoid2.consume(10); + assert t.lastArgument == 10; + + IntToVoid intToVoid3 = t::intToObject; + intToVoid3.consume(15); + assert t.lastArgument == 15; + + assert false; // Check we got here + + } + +} diff --git a/jbmc/regression/jbmc/lambda-void-return-type/test.desc b/jbmc/regression/jbmc/lambda-void-return-type/test.desc new file mode 100644 index 00000000000..0d0d6f858eb --- /dev/null +++ b/jbmc/regression/jbmc/lambda-void-return-type/test.desc @@ -0,0 +1,9 @@ +CORE +Test +--function Test.test --classpath `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^EXIT=10$ +^SIGNAL=0$ +\[java::Test\.test:\(\)V\.assertion\.1\] line 17 assertion at file Test\.java line 17 function java::Test\.test:\(\)V bytecode-index 22: SUCCESS +\[java::Test\.test:\(\)V\.assertion\.2\] line 21 assertion at file Test\.java line 21 function java::Test\.test:\(\)V bytecode-index 41: SUCCESS +\[java::Test\.test:\(\)V\.assertion\.3\] line 25 assertion at file Test\.java line 25 function java::Test\.test:\(\)V bytecode-index 60: SUCCESS +\[java::Test\.test:\(\)V\.assertion\.4\] line 27 assertion at file Test\.java line 27 function java::Test\.test:\(\)V bytecode-index 66: FAILURE diff --git a/jbmc/src/java_bytecode/lambda_synthesis.cpp b/jbmc/src/java_bytecode/lambda_synthesis.cpp index 31c7e32fef8..49443eed7f0 100644 --- a/jbmc/src/java_bytecode/lambda_synthesis.cpp +++ b/jbmc/src/java_bytecode/lambda_synthesis.cpp @@ -806,7 +806,7 @@ codet invokedynamic_synthetic_method( "param" + std::to_string(i)); } - if(callee_return_type != empty_typet() && !is_constructor_lambda) + if(function_type.return_type() != empty_typet() && !is_constructor_lambda) { symbol_exprt result_local = create_and_declare_local( function_id, "return_value", callee_return_type, symbol_table, result);