Merge pull request #8597 from diffblue/fixup-8538

kroening · web-flow · commit f55f63666bbf · 2025-03-02T07:31:30.000-08:00
fixup #8538 -- correct rounding modes for `floor`, `trunc`
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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)
 {

Original file line number	Diff line number	Diff line change
`@@ -3,7 +3,10 @@`
`3`	`3`
`4`	`4`	`int main()`
`5`	`5`	`{`
`6`		`- floor();`
`7`		`- assert(0);`
	`6`	`+ assert(floor(1.1) == 1.0);`
	`7`	`+ assert(floor(1.9) == 1.0);`
	`8`	`+ assert(floor(-1.1) == -2.0);`
	`9`	`+ assert(floor(-1.9) == -2.0);`
	`10`	`+ assert(signbit(floor(-0.0)));`
`8`	`11`	`return 0;`
`9`	`12`	`}`
Original file line number	Diff line number	Diff line change
`@@ -3,7 +3,10 @@`
`3`	`3`
`4`	`4`	`int main()`
`5`	`5`	`{`
`6`		`- floorf();`
`7`		`- assert(0);`
	`6`	`+ assert(floorf(1.1f) == 1.0f);`
	`7`	`+ assert(floorf(1.9f) == 1.0f);`
	`8`	`+ assert(floorf(-1.1f) == -2.0f);`
	`9`	`+ assert(floorf(-1.9f) == -2.0f);`
	`10`	`+ assert(signbit(floorf(-0.0f)));`
`8`	`11`	`return 0;`
`9`	`12`	`}`
Original file line number	Diff line number	Diff line change
`@@ -3,7 +3,12 @@`
`3`	`3`
`4`	`4`	`int main()`
`5`	`5`	`{`
`6`		`- round();`
`7`		`- assert(0);`
	`6`	`+ assert(round(1.1) == 1.0);`
	`7`	`+ assert(round(1.5) == 2.0);`
	`8`	`+ assert(round(1.9) == 2.0);`
	`9`	`+ assert(round(-1.1) == -1.0);`
	`10`	`+ assert(round(-1.5) == -2.0);`
	`11`	`+ assert(round(-1.9) == -2.0);`
	`12`	`+ assert(signbit(round(-0.0)));`
`8`	`13`	`return 0;`
`9`	`14`	`}`
Original file line number	Diff line number	Diff line change
`@@ -3,7 +3,12 @@`
`3`	`3`
`4`	`4`	`int main()`
`5`	`5`	`{`
`6`		`- roundf();`
`7`		`- assert(0);`
	`6`	`+ assert(roundf(1.1f) == 1.0f);`
	`7`	`+ assert(roundf(1.5f) == 2.0f);`
	`8`	`+ assert(roundf(1.9f) == 2.0f);`
	`9`	`+ assert(roundf(-1.1f) == -1.0f);`
	`10`	`+ assert(roundf(-1.5f) == -2.0f);`
	`11`	`+ assert(roundf(-1.9f) == -2.0f);`
	`12`	`+ assert(signbit(roundf(-0.0f)));`
`8`	`13`	`return 0;`
`9`	`14`	`}`