From 6ad8ffd345f479637761e978fbc7abcd1dc4b7c5 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 1 Feb 2018 15:05:30 +0000 Subject: [PATCH] Fix Java ternary-compare against NaN This was supposed to check if either operand is NaN and respond appropriately, but using float-eq to do the test was incorrect, as NaN == x is false for any x, whether NaN or not. This patch uses the isnan exprt to do the test instead, and adds a regression test. --- regression/cbmc-java/isnan1/test.class | Bin 0 -> 1827 bytes regression/cbmc-java/isnan1/test.desc | 20 +++++ regression/cbmc-java/isnan1/test.java | 84 ++++++++++++++++++ .../java_bytecode_convert_method.cpp | 9 +- 4 files changed, 106 insertions(+), 7 deletions(-) create mode 100644 regression/cbmc-java/isnan1/test.class create mode 100644 regression/cbmc-java/isnan1/test.desc create mode 100644 regression/cbmc-java/isnan1/test.java diff --git a/regression/cbmc-java/isnan1/test.class b/regression/cbmc-java/isnan1/test.class new file mode 100644 index 0000000000000000000000000000000000000000..363c5f1b64c53fe29079e4cd349de2b5e4adb0b1 GIT binary patch literal 1827 zcmaKs%TE(g6vn^Xb~^2Jpi^GL_yT!YKtK>s5K**{U=*ULiMkrf1goWJTTEQBb)_p` z_=r2#Y9dAxb?sl|O8rjhV>Z)Sd~@cWbANO0IrrY*f4}_zFpfC`Z5Rw~{{q6>e>lX) zKnsqE42cYjjEEc;85J25IUzDGG9fZ4axzLerDMuK69#om8#s*_9cL7pdz?bS%@;G9 zxk4&aa8|SKnu5Be5T428GR0YiV6y*)Lg>QgnyV1Ml*zeETN|rx{+a~SvEgKLd?gnp ztYM|-r0-pJ?w7rK`i`5v=RQ!-k_!tG5h;!2WN6R1UaSnR*9NoI!R+4TRH`(2CY>#( zWvpy&<ndegFXF6t0oW(f>s}{Mude==e^LTCOLY4(qXj^j&nY_DJ zWwB1hEjn1;Tj*kc+Sp@dwaedW#i3*&)cyQA$hYEK8`y>VD1kUY4VMPFdIlV#%}_Ol z5On&UHU(1Vd<%jX<5QX)dXGp?_g84PR<^=+xNPaRUbZ53q-;fPtKv3ni~eZ4*8deT z+hW9?ZQ53}VmH{9QL!6sEA}2{DL($89BfI_fl|`>l4=MteT}I`5rN6woj{B=Fu8~Z z_NS5kh+_a2M(7#mzMVodW?82cTCvE;Wmf7sYjvA-a#*Q#&fFloz+yaNIks^ak6GC# zZ1iFNy#wYyPSaE%5DWrQK1PgBqsA1tUH0mSX{H%qcki#A4%h~bg^pi8-<#5yba^CuLhR7NAa=7n(IdA+qqvVWvIXpUk zoae9oITPeedO19OzMOadoGEgqy&N9kDksDpU+q_4@ zIlM-EId%FqPtJmu!<)#LQ>R~x arg2; + } + + public static void checkgeq(float arg1, float arg2) { + assert arg1 >= arg2; + } + + public static void checklt(float arg1, float arg2) { + assert arg1 < arg2; + } + + public static void checkleq(float arg1, float arg2) { + assert arg1 <= arg2; + } + + public static void checkeq(double arg1, double arg2) { + assert arg1 == arg2; + } + + public static void checkneq(double arg1, double arg2) { + assert arg1 != arg2; + } + + public static void checkgt(double arg1, double arg2) { + assert arg1 > arg2; + } + + public static void checkgeq(double arg1, double arg2) { + assert arg1 >= arg2; + } + + public static void checklt(double arg1, double arg2) { + assert arg1 < arg2; + } + + public static void checkleq(double arg1, double arg2) { + assert arg1 <= arg2; + } + +} diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 256f1131bb5..c1ee3a0bc3b 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -2048,11 +2048,6 @@ codet java_bytecode_convert_methodt::convert_instructions( else if(statement==patternt("?cmp?")) { assert(op.size()==2 && results.size()==1); - const floatbv_typet type( - to_floatbv_type(java_type_from_char(statement[0]))); - const ieee_float_spect spec(type); - const ieee_floatt nan(ieee_floatt::NaN(spec)); - const constant_exprt nan_expr(nan.to_expr()); const int nan_value(statement[4]=='l' ? -1 : 1); const typet result_type(java_int_type()); const exprt nan_result(from_integer(nan_value, result_type)); @@ -2062,8 +2057,8 @@ codet java_bytecode_convert_methodt::convert_instructions( // (value1 == NaN || value2 == NaN) ? // nan_value : value1 == value2 ? 0 : value1 < value2 -1 ? 1 : 0; - exprt nan_op0=ieee_float_equal_exprt(nan_expr, op[0]); - exprt nan_op1=ieee_float_equal_exprt(nan_expr, op[1]); + isnan_exprt nan_op0(op[0]); + isnan_exprt nan_op1(op[1]); exprt one=from_integer(1, result_type); exprt minus_one=from_integer(-1, result_type); results[0]=