Introduce floatbv_round_to_integral_exprt

This adds a new expression, floatbv_round_to_integral, which rounds an IEEE
754 floating-point number given as bit-vector to the nearest integer,
considering the explicitly given rounding mode.

Author: kroening

regression/cbmc-library/__sort_of_CPROVER_round_to_integral-01/main.c

@@ -0,0 +1,60 @@
+(set-logic FP)
+
+(assert (not (and
+
+  ; round up
+  (= (fp.roundToIntegral roundTowardPositive (_ NaN 11 53)) (_ NaN 11 53))
+  (= (fp.roundToIntegral roundTowardPositive (_ +oo 11 53)) (_ +oo 11 53))
+  (= (fp.roundToIntegral roundTowardPositive (_ -oo 11 53)) (_ -oo 11 53))
+  REQUIRE(ieee_floatt::from_double(up, 1).round_to_integral() == 1);
+  REQUIRE(ieee_floatt::from_double(up, 0.1).round_to_integral() == 1);
+  REQUIRE(ieee_floatt::from_double(up, -0.1).round_to_integral() == -0.0);
+  REQUIRE(ieee_floatt::from_double(up, 10.1).round_to_integral() == 11);
+  REQUIRE(ieee_floatt::from_double(up, -10.1).round_to_integral() == -10);
+  REQUIRE(ieee_floatt::from_double(up, dmax).round_to_integral() == dmax);
+
+  ; round down
+  (= (fp.roundToIntegral roundTowardNegative (_ NaN 11 53)) (_ NaN 11 53))
+  (= (fp.roundToIntegral roundTowardNegative (_ +oo 11 53)) (_ +oo 11 53))
+  (= (fp.roundToIntegral roundTowardNegative (_ -oo 11 53)) (_ -oo 11 53))
+  REQUIRE(ieee_floatt::from_double(down, 0).round_to_integral() == 0);
+  REQUIRE(ieee_floatt::from_double(down, -0.0).round_to_integral() == -0.0);
+  REQUIRE(ieee_floatt::from_double(down, 1).round_to_integral() == 1);
+  REQUIRE(ieee_floatt::from_double(down, 0.1).round_to_integral() == 0);
+  REQUIRE(ieee_floatt::from_double(down, -0.1).round_to_integral() == -1);
+  REQUIRE(ieee_floatt::from_double(down, 10.1).round_to_integral() == 10);
+  REQUIRE(ieee_floatt::from_double(down, -10.1).round_to_integral() == -11);
+  REQUIRE(ieee_floatt::from_double(down, 0x1.0p+52).round_to_integral() == 0x1.0p+52);
+  REQUIRE(ieee_floatt::from_double(down, dmax).round_to_integral() == dmax);
+
+  ; round to nearest ties to even
+  (= (fp.roundToIntegral roundNearestTiesToEven (_ NaN 11 53)) (_ NaN 11 53))
+  (= (fp.roundToIntegral roundNearestTiesToEven (_ +oo 11 53)) (_ +oo 11 53))
+  (= (fp.roundToIntegral roundNearestTiesToEven (_ -oo 11 53)) (_ -oo 11 53))
+  REQUIRE(ieee_floatt::from_double(even, 0).round_to_integral() == 0);
+  REQUIRE(ieee_floatt::from_double(even, -0.0).round_to_integral() == -0.0);
+  REQUIRE(ieee_floatt::from_double(even, 1).round_to_integral() == 1);
+  REQUIRE(ieee_floatt::from_double(even, 0.1).round_to_integral() == 0);
+  REQUIRE(ieee_floatt::from_double(even, -0.1).round_to_integral() == -0.0);
+  REQUIRE(ieee_floatt::from_double(even, 10.1).round_to_integral() == 10);
+  REQUIRE(ieee_floatt::from_double(even, -10.1).round_to_integral() == -10);
+  REQUIRE(ieee_floatt::from_double(even, 0x1.0p+52).round_to_integral() == 0x1.0p+52);
+  REQUIRE(ieee_floatt::from_double(even, dmax).round_to_integral() == dmax);
+
+  ; round to zero
+  (= (fp.roundToIntegral roundTowardZero (_ NaN 11 53)) (_ NaN 11 53))
+  (= (fp.roundToIntegral roundTowardZero (_ +oo 11 53)) (_ +oo 11 53))
+  (= (fp.roundToIntegral roundTowardZero (_ -oo 11 53)) (_ -oo 11 53))
+  REQUIRE(ieee_floatt::from_double(zero, 0).round_to_integral() == 0);
+  REQUIRE(ieee_floatt::from_double(zero, -0.0).round_to_integral() == -0.0);
+  REQUIRE(ieee_floatt::from_double(zero, 1).round_to_integral() == 1);
+  REQUIRE(ieee_floatt::from_double(zero, 0.1).round_to_integral() == 0);
+  REQUIRE(ieee_floatt::from_double(zero, -0.1).round_to_integral() == -0.0);
+  REQUIRE(ieee_floatt::from_double(zero, 10.1).round_to_integral() == 10);
+  REQUIRE(ieee_floatt::from_double(zero, -10.1).round_to_integral() == -10);
+  REQUIRE(ieee_floatt::from_double(zero, 0x1.0p+52).round_to_integral() == 0x1.0p+52);
+  REQUIRE(ieee_floatt::from_double(zero, dmax).round_to_integral() == dmax);
+)))
+
+; should be unsat
+(check-sat)

regression/cbmc-library/__sort_of_CPROVER_round_to_integral-01/test.desc

@@ -3237,6 +3237,24 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(infl_expr);
   }
+  else if(
+    identifier == CPROVER_PREFIX "round_to_integralf" ||
+    identifier == CPROVER_PREFIX "round_to_integrald" ||
+    identifier == CPROVER_PREFIX "round_to_integralld")
+  {
+    if(expr.arguments().size() != 2)
+    {
+      error().source_location = f_op.source_location();
+      error() << identifier << " expects two arguments" << eom;
+      throw 0;
+    }
+
+    auto round_to_integral_expr =
+      floatbv_round_to_integral_exprt{expr.arguments()[0], expr.arguments()[1]};
+    round_to_integral_expr.add_source_location() = source_location;
+
+    return std::move(round_to_integral_expr);
+  }
   else if(
     identifier == CPROVER_PREFIX "abs" || identifier == CPROVER_PREFIX "labs" ||
     identifier == CPROVER_PREFIX "llabs" ||

regression/cbmc-library/__sort_of_CPROVER_round_to_integralf-01/main.c

@@ -93,6 +93,9 @@ int __CPROVER_islessgreaterf(float f, float g);
 int __CPROVER_islessgreaterd(double f, double g);
 int __CPROVER_isunorderedf(float f, float g);
 int __CPROVER_isunorderedd(double f, double g);
+float __CPROVER_round_to_integralf(float, int);
+double __CPROVER_round_to_integrald(double, int);
+long double __CPROVER_round_to_integralld(long double, int);
 
 // absolute value
 int __CPROVER_abs(int x);