Cleanup fmod vs IEEE remainder

1. Add tests for both the C and Java front-end.
2. Make sure we support both variants of the modulus operator on
floating-point values in the back-ends: the SMT back-end only supported
remainder (and only for FPA mode), the propositional back-end did not
distinguish between fmod and IEEE remainder.

Author: tautschnig

jbmc/regression/jbmc/farith2/farith2.class

@@ -0,0 +1,17 @@
+class farith2
+{
+  public static void main(String[] args)
+  {
+    // examples from
+    // https://stackoverflow.com/questions/2947044/how-do-i-use-modulus-for-float-double
+    // and
+    // https://stackoverflow.com/questions/25734144/difference-between-c-functions-remainder-and-fmod
+    double d1 = 0.5 % 0.3;
+    assert d1 == 0.2;
+    double d2 = (-0.5) % 0.3;
+    assert d2 == -0.2;
+    double x = 7.5, y = 2.1;
+    double xModY = x % y;
+    assert xModY > 1.19 && xModY < 1.21;
+  }
+}

jbmc/regression/jbmc/farith2/farith2.java

@@ -1,6 +1,6 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
+CORE
+farith2
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-library/__sort_of_CPROVER_remainder-01/test.desc renamed to jbmc/regression/jbmc/farith2/test.desc

@@ -3,7 +3,15 @@
 
 int main()
 {
-  fmod();
-  assert(0);
-  return 0;
+  // examples from
+  // https://stackoverflow.com/questions/2947044/how-do-i-use-modulus-for-float-double
+  // and
+  // https://stackoverflow.com/questions/25734144/difference-between-c-functions-remainder-and-fmod
+  double d1 = fmod(0.5, 0.3);
+  assert(d1 == 0.2);
+  double d2 = fmod(-0.5, 0.3);
+  assert(d2 == -0.2);
+  double x = 7.5, y = 2.1;
+  double xModY = fmod(x, y);
+  assert(xModY > 1.19 && xModY < 1.21);
 }

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

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--float-overflow-check --nan-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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

@@ -3,7 +3,15 @@
 
 int main()
 {
-  fmodf();
-  assert(0);
-  return 0;
+  // examples from
+  // https://stackoverflow.com/questions/2947044/how-do-i-use-modulus-for-float-double
+  // and
+  // https://stackoverflow.com/questions/25734144/difference-between-c-functions-remainder-and-fmod
+  float d1 = fmodf(0.5f, 0.3f);
+  assert(d1 == 0.2f);
+  float d2 = fmodf(-0.5f, 0.3f);
+  assert(d2 == -0.2f);
+  float x = 7.5f, y = 2.1f;
+  float xModY = fmodf(x, y);
+  assert(xModY > 1.19f && xModY < 1.21f);
 }

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

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--float-overflow-check --nan-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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

@@ -3,7 +3,15 @@
 
 int main()
 {
-  fmodl();
-  assert(0);
-  return 0;
+  // examples from
+  // https://stackoverflow.com/questions/2947044/how-do-i-use-modulus-for-float-double
+  // and
+  // https://stackoverflow.com/questions/25734144/difference-between-c-functions-remainder-and-fmod
+  long double d1 = fmodl(0.5l, 0.3l);
+  assert(d1 == 0.2l);
+  long double d2 = fmodl(-0.5l, 0.3l);
+  assert(d2 == -0.2l);
+  long double x = 7.5l, y = 2.1l;
+  long double xModY = fmodl(x, y);
+  assert(xModY > 1.19l && xModY < 1.21l);
 }

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

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--float-overflow-check --nan-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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

@@ -3,7 +3,9 @@
 
 int main()
 {
-  remainder();
-  assert(0);
-  return 0;
+  // example from
+  // https://stackoverflow.com/questions/25734144/difference-between-c-functions-remainder-and-fmod
+  double x = 7.5, y = 2.1;
+  double xModY = remainder(x, y);
+  assert(xModY > -0.91 && xModY < -0.89);
 }

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

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--float-overflow-check --nan-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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

@@ -3,7 +3,9 @@
 
 int main()
 {
-  remainderf();
-  assert(0);
-  return 0;
+  // example from
+  // https://stackoverflow.com/questions/25734144/difference-between-c-functions-remainder-and-fmod
+  float x = 7.5f, y = 2.1f;
+  float xModY = remainderf(x, y);
+  assert(xModY > -0.91f && xModY < -0.89f);
 }

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

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--float-overflow-check --nan-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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

@@ -3,7 +3,9 @@
 
 int main()
 {
-  remainderl();
-  assert(0);
-  return 0;
+  // example from
+  // https://stackoverflow.com/questions/25734144/difference-between-c-functions-remainder-and-fmod
+  long double x = 7.5l, y = 2.1l;
+  long double xModY = remainderl(x, y);
+  assert(xModY > -0.91l && xModY < -0.89l);
 }

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

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--float-overflow-check --nan-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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

@@ -4038,6 +4038,7 @@ optionalt<std::string> expr2ct::convert_function(const exprt &src)
     {ID_separate, "SEPARATE"},
     {ID_floatbv_div, "FLOAT/"},
     {ID_floatbv_minus, "FLOAT-"},
+    {ID_floatbv_mod, "fmod"},
     {ID_floatbv_mult, "FLOAT*"},
     {ID_floatbv_plus, "FLOAT+"},
     {ID_floatbv_rem, "FLOAT%"},

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

@@ -2186,60 +2186,6 @@ long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double
   return (x - *iptr);
 }
 
-
-
-/* FUNCTION: __sort_of_CPROVER_remainder */
-// TODO : Should be a real __CPROVER function to convert to SMT-LIB
-double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
-  
-double __sort_of_CPROVER_remainder (int rounding_mode, double x, double y)
-{
-  if (x == 0.0 || __CPROVER_isinfd(y))
-    return x;
-
-  // Extended precision helps... a bit...
-  long double div = x/y;
-  long double n = __sort_of_CPROVER_round_to_integral(rounding_mode,div);
-  long double res = (-y * n) + x;   // TODO : FMA would be an improvement
-  return res;
-}
-
-/* FUNCTION: __sort_of_CPROVER_remainderf */
-// TODO : Should be a real __CPROVER function to convert to SMT-LIB
-
-float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
-
-float __sort_of_CPROVER_remainderf (int rounding_mode, float x, float y)
-{
-  if (x == 0.0f || __CPROVER_isinff(y))
-    return x;
-
-  // Extended precision helps... a bit...
-  long double div = x/y;
-  long double n = __sort_of_CPROVER_round_to_integral(rounding_mode,div);
-  long double res = (-y * n) + x;   // TODO : FMA would be an improvement
-  return res;
-}
-
-/* FUNCTION: __sort_of_CPROVER_remainderl */
-// TODO : Should be a real __CPROVER function to convert to SMT-LIB
-
-long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
-
-long double __sort_of_CPROVER_remainderl (int rounding_mode, long double x, long double y)
-{
-  if (x == 0.0 || __CPROVER_isinfld(y))
-    return x;
-
-  // Extended precision helps... a bit...
-  long double div = x/y;
-  long double n = __sort_of_CPROVER_round_to_integral(rounding_mode,div);
-  long double res = (-y * n) + x;   // TODO : FMA would be an improvement
-  return res;
-}
-
-
-
 /* ISO 9899:2011
  *
  * The fmod functions return the value x - ny, for some
@@ -2320,15 +2266,10 @@ long double fmodl(long double x, long double y)
 #define __CPROVER_MATH_H_INCLUDED
 #endif
 
-#ifndef __CPROVER_FENV_H_INCLUDED
-#include <fenv.h>
-#define __CPROVER_FENV_H_INCLUDED
-#endif
-
-double __sort_of_CPROVER_remainder (int rounding_mode, double x, double y);
-
-double remainder(double x, double y) { return __sort_of_CPROVER_remainder(FE_TONEAREST, x, y); }
-
+double remainder(double x, double y)
+{
+  return __CPROVER_remainder(x, y);
+}
 
 /* FUNCTION: remainderf */
 
@@ -2337,15 +2278,10 @@ double remainder(double x, double y) { return __sort_of_CPROVER_remainder(FE_TON
 #define __CPROVER_MATH_H_INCLUDED
 #endif
 
-#ifndef __CPROVER_FENV_H_INCLUDED
-#include <fenv.h>
-#define __CPROVER_FENV_H_INCLUDED
-#endif
-
-float __sort_of_CPROVER_remainderf (int rounding_mode, float x, float y);
-
-float remainderf(float x, float y) { return __sort_of_CPROVER_remainderf(FE_TONEAREST, x, y); }
-
+float remainderf(float x, float y)
+{
+  return __CPROVER_remainderf(x, y);
+}
 
 /* FUNCTION: remainderl */
 
@@ -2354,17 +2290,10 @@ float remainderf(float x, float y) { return __sort_of_CPROVER_remainderf(FE_TONE
 #define __CPROVER_MATH_H_INCLUDED
 #endif
 
-#ifndef __CPROVER_FENV_H_INCLUDED
-#include <fenv.h>
-#define __CPROVER_FENV_H_INCLUDED
-#endif
-
-long double __sort_of_CPROVER_remainderl (int rounding_mode, long double x, long double y);
-
-long double remainderl(long double x, long double y) { return __sort_of_CPROVER_remainderl(FE_TONEAREST, x, y); }
-
-
-
+long double remainderl(long double x, long double y)
+{
+  return __CPROVER_remainderl(x, y);
+}
 
 /* ISO 9899:2011
  * The copysign functions produce a value with the magnitude of x and

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

@@ -31,13 +31,11 @@ irep_idt rounding_mode_identifier()
 /// yet.
 static bool have_to_adjust_float_expressions(const exprt &expr)
 {
-  if(expr.id()==ID_floatbv_plus ||
-     expr.id()==ID_floatbv_minus ||
-     expr.id()==ID_floatbv_mult ||
-     expr.id()==ID_floatbv_div ||
-     expr.id()==ID_floatbv_div ||
-     expr.id()==ID_floatbv_rem ||
-     expr.id()==ID_floatbv_typecast)
+  if(
+    expr.id() == ID_floatbv_plus || expr.id() == ID_floatbv_minus ||
+    expr.id() == ID_floatbv_mult || expr.id() == ID_floatbv_div ||
+    expr.id() == ID_floatbv_mod || expr.id() == ID_floatbv_rem ||
+    expr.id() == ID_floatbv_typecast)
     return false;
 
   const typet &type = expr.type();

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

@@ -19,7 +19,10 @@ bvt boolbvt::convert_floatbv_mod_rem(const binary_exprt &expr)
 
   float_utilst float_utils(prop);
 
-  auto rm = bv_utils.build_constant(ieee_floatt::ROUND_TO_EVEN, 32);
+  auto rm = bv_utils.build_constant(
+    expr.id() == ID_floatbv_rem ? ieee_floatt::ROUND_TO_EVEN
+                                : ieee_floatt::ROUND_TO_ZERO,
+    32);
   float_utils.set_rounding_mode(rm);
 
   float_utils.spec = ieee_float_spect(to_floatbv_type(expr.type()));