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.
diffblue · Jan 2, 2025 · 22b1e27 · 22b1e27
1 parent 1102fa1
commit 22b1e27
Show file tree

Hide file tree

Showing 25 changed files with 603 additions and 334 deletions.
diff --git a/regression/cbmc-library/__sort_of_CPROVER_round_to_integral-01/main.c b/regression/cbmc-library/__sort_of_CPROVER_round_to_integral-01/main.c
diff --git a/regression/cbmc-library/__sort_of_CPROVER_round_to_integral-01/test.desc b/regression/cbmc-library/__sort_of_CPROVER_round_to_integral-01/test.desc
diff --git a/regression/cbmc-library/__sort_of_CPROVER_round_to_integralf-01/main.c b/regression/cbmc-library/__sort_of_CPROVER_round_to_integralf-01/main.c
diff --git a/regression/cbmc-library/__sort_of_CPROVER_round_to_integralf-01/test.desc b/regression/cbmc-library/__sort_of_CPROVER_round_to_integralf-01/test.desc
diff --git a/regression/cbmc-library/__sort_of_CPROVER_round_to_integrall-01/main.c b/regression/cbmc-library/__sort_of_CPROVER_round_to_integrall-01/main.c
diff --git a/regression/cbmc-library/__sort_of_CPROVER_round_to_integrall-01/test.desc b/regression/cbmc-library/__sort_of_CPROVER_round_to_integrall-01/test.desc
diff --git a/regression/smt2_solver/fp/roundToIntegral1.smt2 b/regression/smt2_solver/fp/roundToIntegral1.smt2
@@ -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)
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -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" ||

diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h
@@ -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);