From 968c28fba7d359944ed75a88330ac9193752d695 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 19 Feb 2025 22:08:24 +0000
Subject: [PATCH] fixup #8538 -- correct rounding modes for floor, trunc

This fixes the rounding modes used for the floor and trunc C library functions.
---
 regression/cbmc-library/floor-01/main.c     |  7 +++++--
 regression/cbmc-library/floor-01/test.desc  |  4 ++--
 regression/cbmc-library/floorf-01/main.c    |  7 +++++--
 regression/cbmc-library/floorf-01/test.desc |  4 ++--
 regression/cbmc-library/floorl-01/main.c    | 11 +++++++++--
 regression/cbmc-library/floorl-01/test.desc |  4 ++--
 regression/cbmc-library/round-01/main.c     |  9 +++++++--
 regression/cbmc-library/round-01/test.desc  |  4 ++--
 regression/cbmc-library/roundf-01/main.c    |  9 +++++++--
 regression/cbmc-library/roundf-01/test.desc |  4 ++--
 regression/cbmc-library/roundl-01/main.c    | 13 ++++++++++--
 regression/cbmc-library/roundl-01/test.desc |  4 ++--
 regression/cbmc-library/trunc-01/main.c     |  7 +++++--
 regression/cbmc-library/trunc-01/test.desc  |  4 ++--
 regression/cbmc-library/truncf-01/main.c    |  7 +++++--
 regression/cbmc-library/truncf-01/test.desc |  4 ++--
 regression/cbmc-library/truncl-01/main.c    | 11 +++++++++--
 regression/cbmc-library/truncl-01/test.desc |  4 ++--
 src/ansi-c/library/math.c                   | 18 ++++++++---------
 src/util/simplify_expr.cpp                  |  5 +++++
 src/util/simplify_expr_class.h              |  3 +++
 src/util/simplify_expr_floatbv.cpp          | 22 +++++++++++++++++++++
 22 files changed, 120 insertions(+), 45 deletions(-)

diff --git a/regression/cbmc-library/floor-01/main.c b/regression/cbmc-library/floor-01/main.c
index bf33cf24a50..11e6add1b00 100644
--- a/regression/cbmc-library/floor-01/main.c
+++ b/regression/cbmc-library/floor-01/main.c
@@ -3,7 +3,10 @@
 
 int main()
 {
-  floor();
-  assert(0);
+  assert(floor(1.1) == 1.0);
+  assert(floor(1.9) == 1.0);
+  assert(floor(-1.1) == -2.0);
+  assert(floor(-1.9) == -2.0);
+  assert(signbit(floor(-0.0)));
   return 0;
 }
diff --git a/regression/cbmc-library/floor-01/test.desc b/regression/cbmc-library/floor-01/test.desc
index 9542d988e8d..9efefbc7362 100644
--- a/regression/cbmc-library/floor-01/test.desc
+++ b/regression/cbmc-library/floor-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/floorf-01/main.c b/regression/cbmc-library/floorf-01/main.c
index d5d6714694c..b963262b77c 100644
--- a/regression/cbmc-library/floorf-01/main.c
+++ b/regression/cbmc-library/floorf-01/main.c
@@ -3,7 +3,10 @@
 
 int main()
 {
-  floorf();
-  assert(0);
+  assert(floorf(1.1f) == 1.0f);
+  assert(floorf(1.9f) == 1.0f);
+  assert(floorf(-1.1f) == -2.0f);
+  assert(floorf(-1.9f) == -2.0f);
+  assert(signbit(floorf(-0.0f)));
   return 0;
 }
diff --git a/regression/cbmc-library/floorf-01/test.desc b/regression/cbmc-library/floorf-01/test.desc
index 9542d988e8d..9efefbc7362 100644
--- a/regression/cbmc-library/floorf-01/test.desc
+++ b/regression/cbmc-library/floorf-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/floorl-01/main.c b/regression/cbmc-library/floorl-01/main.c
index 2e86d233bde..9d75e4b0d52 100644
--- a/regression/cbmc-library/floorl-01/main.c
+++ b/regression/cbmc-library/floorl-01/main.c
@@ -3,7 +3,14 @@
 
 int main()
 {
-  floorl();
-  assert(0);
+  assert(floorl(1.1l) == 1.0l);
+  assert(floorl(1.9l) == 1.0l);
+  assert(floorl(-1.1l) == -2.0l);
+  assert(floorl(-1.9l) == -2.0l);
+
+#if !defined(__APPLE__) || __ENVIRONMENT_OS_VERSION_MIN_REQUIRED__ >= 150000
+  assert(signbit(floorl(-0.0l)));
+#endif
+
   return 0;
 }
diff --git a/regression/cbmc-library/floorl-01/test.desc b/regression/cbmc-library/floorl-01/test.desc
index 9542d988e8d..9efefbc7362 100644
--- a/regression/cbmc-library/floorl-01/test.desc
+++ b/regression/cbmc-library/floorl-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/round-01/main.c b/regression/cbmc-library/round-01/main.c
index 01fece69bf4..a87a5aad5af 100644
--- a/regression/cbmc-library/round-01/main.c
+++ b/regression/cbmc-library/round-01/main.c
@@ -3,7 +3,12 @@
 
 int main()
 {
-  round();
-  assert(0);
+  assert(round(1.1) == 1.0);
+  assert(round(1.5) == 2.0);
+  assert(round(1.9) == 2.0);
+  assert(round(-1.1) == -1.0);
+  assert(round(-1.5) == -2.0);
+  assert(round(-1.9) == -2.0);
+  assert(signbit(round(-0.0)));
   return 0;
 }
diff --git a/regression/cbmc-library/round-01/test.desc b/regression/cbmc-library/round-01/test.desc
index 9542d988e8d..9efefbc7362 100644
--- a/regression/cbmc-library/round-01/test.desc
+++ b/regression/cbmc-library/round-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/roundf-01/main.c b/regression/cbmc-library/roundf-01/main.c
index 6b19f92f531..c914954b994 100644
--- a/regression/cbmc-library/roundf-01/main.c
+++ b/regression/cbmc-library/roundf-01/main.c
@@ -3,7 +3,12 @@
 
 int main()
 {
-  roundf();
-  assert(0);
+  assert(roundf(1.1f) == 1.0f);
+  assert(roundf(1.5f) == 2.0f);
+  assert(roundf(1.9f) == 2.0f);
+  assert(roundf(-1.1f) == -1.0f);
+  assert(roundf(-1.5f) == -2.0f);
+  assert(roundf(-1.9f) == -2.0f);
+  assert(signbit(roundf(-0.0f)));
   return 0;
 }
diff --git a/regression/cbmc-library/roundf-01/test.desc b/regression/cbmc-library/roundf-01/test.desc
index 9542d988e8d..9efefbc7362 100644
--- a/regression/cbmc-library/roundf-01/test.desc
+++ b/regression/cbmc-library/roundf-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/roundl-01/main.c b/regression/cbmc-library/roundl-01/main.c
index 71a11dd6ea9..34f0acd5c3d 100644
--- a/regression/cbmc-library/roundl-01/main.c
+++ b/regression/cbmc-library/roundl-01/main.c
@@ -3,7 +3,16 @@
 
 int main()
 {
-  roundl();
-  assert(0);
+  assert(roundl(1.1l) == 1.0l);
+  assert(roundl(1.5l) == 2.0l);
+  assert(roundl(1.9l) == 2.0l);
+  assert(roundl(-1.1l) == -1.0l);
+  assert(roundl(-1.5l) == -2.0l);
+  assert(roundl(-1.9l) == -2.0l);
+
+#if !defined(__APPLE__) || __ENVIRONMENT_OS_VERSION_MIN_REQUIRED__ >= 150000
+  assert(signbit(roundl(-0.0l)));
+#endif
+
   return 0;
 }
diff --git a/regression/cbmc-library/roundl-01/test.desc b/regression/cbmc-library/roundl-01/test.desc
index 9542d988e8d..9efefbc7362 100644
--- a/regression/cbmc-library/roundl-01/test.desc
+++ b/regression/cbmc-library/roundl-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/trunc-01/main.c b/regression/cbmc-library/trunc-01/main.c
index 7e2576dc5f2..1285ff3087f 100644
--- a/regression/cbmc-library/trunc-01/main.c
+++ b/regression/cbmc-library/trunc-01/main.c
@@ -3,7 +3,10 @@
 
 int main()
 {
-  trunc();
-  assert(0);
+  assert(trunc(1.1) == 1.0);
+  assert(trunc(1.9) == 1.0);
+  assert(trunc(-1.1) == -1.0);
+  assert(trunc(-1.9) == -1.0);
+  assert(signbit(trunc(-0.0)));
   return 0;
 }
diff --git a/regression/cbmc-library/trunc-01/test.desc b/regression/cbmc-library/trunc-01/test.desc
index 9542d988e8d..9efefbc7362 100644
--- a/regression/cbmc-library/trunc-01/test.desc
+++ b/regression/cbmc-library/trunc-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/truncf-01/main.c b/regression/cbmc-library/truncf-01/main.c
index 1524df9816a..216a373b8d1 100644
--- a/regression/cbmc-library/truncf-01/main.c
+++ b/regression/cbmc-library/truncf-01/main.c
@@ -3,7 +3,10 @@
 
 int main()
 {
-  truncf();
-  assert(0);
+  assert(truncf(1.1f) == 1.0f);
+  assert(truncf(1.9f) == 1.0f);
+  assert(truncf(-1.1f) == -1.0f);
+  assert(truncf(-1.9f) == -1.0f);
+  assert(signbit(trunc(-0.0f)));
   return 0;
 }
diff --git a/regression/cbmc-library/truncf-01/test.desc b/regression/cbmc-library/truncf-01/test.desc
index 9542d988e8d..9efefbc7362 100644
--- a/regression/cbmc-library/truncf-01/test.desc
+++ b/regression/cbmc-library/truncf-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/truncl-01/main.c b/regression/cbmc-library/truncl-01/main.c
index 89e09332302..6dd14564a88 100644
--- a/regression/cbmc-library/truncl-01/main.c
+++ b/regression/cbmc-library/truncl-01/main.c
@@ -3,7 +3,14 @@
 
 int main()
 {
-  truncl();
-  assert(0);
+  assert(truncl(1.1l) == 1.0l);
+  assert(truncl(1.9l) == 1.0l);
+  assert(truncl(-1.1l) == -1.0l);
+  assert(truncl(-1.9l) == -1.0l);
+
+#if !defined(__APPLE__) || __ENVIRONMENT_OS_VERSION_MIN_REQUIRED__ >= 150000
+  assert(signbit(truncl(-0.0l)));
+#endif
+
   return 0;
 }
diff --git a/regression/cbmc-library/truncl-01/test.desc b/regression/cbmc-library/truncl-01/test.desc
index 9542d988e8d..9efefbc7362 100644
--- a/regression/cbmc-library/truncl-01/test.desc
+++ b/regression/cbmc-library/truncl-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index d707997972c..ac594c0e590 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -1322,7 +1322,7 @@ long double ceill(long double x)
 
 double floor(double x)
 {
-  return __CPROVER_round_to_integrald(x, 3); // FE_DOWNWARD
+  return __CPROVER_round_to_integrald(x, 1); // FE_DOWNWARD
 }
 
 /* FUNCTION: floorf */
@@ -1339,7 +1339,7 @@ double floor(double x)
 
 float floorf(float x)
 {
-  return __CPROVER_round_to_integralf(x, 3); // FE_DOWNWARD
+  return __CPROVER_round_to_integralf(x, 1); // FE_DOWNWARD
 }
 
 
@@ -1357,7 +1357,7 @@ float floorf(float x)
 
 long double floorl(long double x)
 {
-  return __CPROVER_round_to_integralld(x, 3); // FE_DOWNWARD
+  return __CPROVER_round_to_integralld(x, 1); // FE_DOWNWARD
 }
 
 
@@ -1381,7 +1381,7 @@ long double floorl(long double x)
 
 double trunc(double x)
 {
-  return __CPROVER_round_to_integrald(x, 0); // FE_TOWARDZERO
+  return __CPROVER_round_to_integrald(x, 3); // FE_TOWARDZERO
 }
 
 /* FUNCTION: truncf */
@@ -1398,7 +1398,7 @@ double trunc(double x)
 
 float truncf(float x)
 {
-  return __CPROVER_round_to_integralf(x, 0); // FE_TOWARDZERO
+  return __CPROVER_round_to_integralf(x, 3); // FE_TOWARDZERO
 }
 
 
@@ -1416,7 +1416,7 @@ float truncf(float x)
 
 long double truncl(long double x)
 {
-  return __CPROVER_round_to_integralld(x, 0); // FE_TOWARDZERO
+  return __CPROVER_round_to_integralld(x, 3); // FE_TOWARDZERO
 }
 
 
@@ -1889,7 +1889,7 @@ long long int llroundl(long double x)
 
 double modf(double x, double *iptr)
 {
-  *iptr = __CPROVER_round_to_integrald(x, 0); // FE_TOWARDZERO
+  *iptr = __CPROVER_round_to_integrald(x, 3); // FE_TOWARDZERO
   return (x - *iptr);
 }
 
@@ -1907,7 +1907,7 @@ double modf(double x, double *iptr)
 
 float modff(float x, float *iptr)
 {
-  *iptr = __CPROVER_round_to_integralf(x, 0); // FE_TOWARDZERO
+  *iptr = __CPROVER_round_to_integralf(x, 3); // FE_TOWARDZERO
   return (x - *iptr);
 }
 
@@ -1926,7 +1926,7 @@ float modff(float x, float *iptr)
 
 long double modfl(long double x, long double *iptr)
 {
-  *iptr = __CPROVER_round_to_integralld(x, 0); // FE_TOWARDZERO
+  *iptr = __CPROVER_round_to_integralld(x, 3); // FE_TOWARDZERO
   return (x - *iptr);
 }
 
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 1eaa54a4dea..8b14c8cb55e 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -2986,6 +2986,11 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(const exprt &node)
   {
     r = simplify_floatbv_op(to_ieee_float_op_expr(expr));
   }
+  else if(expr.id() == ID_floatbv_round_to_integral)
+  {
+    r = simplify_floatbv_round_to_integral(
+      to_floatbv_round_to_integral_expr(expr));
+  }
   else if(expr.id()==ID_floatbv_typecast)
   {
     r = simplify_floatbv_typecast(to_floatbv_typecast_expr(expr));
diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h
index 284a314fde2..1a9a1fe2998 100644
--- a/src/util/simplify_expr_class.h
+++ b/src/util/simplify_expr_class.h
@@ -45,6 +45,7 @@ class exprt;
 class extractbit_exprt;
 class extractbits_exprt;
 class find_first_set_exprt;
+class floatbv_round_to_integral_exprt;
 class floatbv_typecast_exprt;
 class function_application_exprt;
 class ieee_float_op_exprt;
@@ -162,6 +163,8 @@ class simplify_exprt
   [[nodiscard]] resultt<> simplify_minus(const minus_exprt &);
   [[nodiscard]] resultt<> simplify_floatbv_op(const ieee_float_op_exprt &);
   [[nodiscard]] resultt<>
+  simplify_floatbv_round_to_integral(const floatbv_round_to_integral_exprt &);
+  [[nodiscard]] resultt<>
   simplify_floatbv_typecast(const floatbv_typecast_exprt &);
   [[nodiscard]] resultt<> simplify_shifts(const shift_exprt &);
   [[nodiscard]] resultt<> simplify_power(const power_exprt &);
diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp
index b70ccb9b689..61ba1246560 100644
--- a/src/util/simplify_expr_floatbv.cpp
+++ b/src/util/simplify_expr_floatbv.cpp
@@ -135,6 +135,28 @@ bool simplify_exprt::simplify_sign(exprt &expr)
 }
 #endif
 
+simplify_exprt::resultt<> simplify_exprt::simplify_floatbv_round_to_integral(
+  const floatbv_round_to_integral_exprt &expr)
+{
+  auto &op = expr.op();
+  auto &rounding_mode = expr.rounding_mode();
+
+  // constant folding
+  if(op.is_constant() && rounding_mode.is_constant())
+  {
+    const auto rounding_mode_index =
+      numeric_cast_v<std::size_t>(to_constant_expr(rounding_mode));
+
+    ieee_floatt op_value{
+      to_constant_expr(op),
+      static_cast<ieee_floatt::rounding_modet>(rounding_mode_index)};
+
+    return op_value.round_to_integral().to_expr();
+  }
+
+  return unchanged(expr);
+}
+
 simplify_exprt::resultt<>
 simplify_exprt::simplify_floatbv_typecast(const floatbv_typecast_exprt &expr)
 {