Merge pull request #1788 from smowton/smowton/fix/java_tcmp_nan

[TG-1940] Fix Java ternary-compare against NaN

Author: smowton

regression/cbmc-java/isnan1/test.class

@@ -0,0 +1,20 @@
+CORE
+test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file test.java line 37 .*: FAILURE
+assertion at file test.java line 45 .*: FAILURE
+assertion at file test.java line 49 .*: FAILURE
+assertion at file test.java line 53 .*: FAILURE
+assertion at file test.java line 57 .*: FAILURE
+assertion at file test.java line 41 .*: SUCCESS
+assertion at file test.java line 61 .*: FAILURE
+assertion at file test.java line 69 .*: FAILURE
+assertion at file test.java line 73 .*: FAILURE
+assertion at file test.java line 77 .*: FAILURE
+assertion at file test.java line 81 .*: FAILURE
+assertion at file test.java line 65 .*: SUCCESS
+--
+^warning: ignoring

regression/cbmc-java/isnan1/test.desc

@@ -0,0 +1,84 @@
+public class test {
+
+  public static void main(int nondet) {
+
+    float nan = 0.0f / 0.0f;
+    float one = 1.0f;
+    double nand = 0.0 / 0.0;
+    double oned = 1.0;
+
+    if(nondet == 1)
+      checkeq(one, nan);
+    if(nondet == 2)
+      checkneq(one, nan);
+    if(nondet == 3)
+      checkgt(one, nan);
+    if(nondet == 4)
+      checkgeq(one, nan);
+    if(nondet == 5)
+      checklt(one, nan);
+    if(nondet == 6)
+      checkleq(one, nan);
+    if(nondet == 7)
+      checkeq(oned, nand);
+    if(nondet == 8)
+      checkneq(oned, nand);
+    if(nondet == 9)
+      checkgt(oned, nand);
+    if(nondet == 10)
+      checkgeq(oned, nand);
+    if(nondet == 11)
+      checklt(oned, nand);
+    else
+      checkleq(oned, nand);
+  }
+
+  public static void checkeq(float arg1, float arg2) {
+    assert arg1 == arg2;
+  }
+
+  public static void checkneq(float arg1, float arg2) {
+    assert arg1 != arg2;
+  }
+
+  public static void checkgt(float arg1, float arg2) {
+    assert arg1 > 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;
+  }
+
+}

regression/cbmc-java/isnan1/test.java

@@ -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]=