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 · Dec 21, 2024 · 9c6589a · 9c6589a
1 parent d5cf498
commit 9c6589a
Show file tree

Hide file tree

Showing 24 changed files with 514 additions and 328 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/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);