introduce __CROVER_fmod functions

This will allow us to map the fmod family of library functions to
appropriate backend operators.

Author: kroening

src/ansi-c/c_typecheck_expr.cpp

@@ -2567,6 +2567,30 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(abs_expr);
   }
+  else if(
+    identifier == CPROVER_PREFIX "fmod" ||
+    identifier == CPROVER_PREFIX "fmodf" ||
+    identifier == CPROVER_PREFIX "fmodl")
+  {
+    if(expr.arguments().size() != 2)
+    {
+      error().source_location = f_op.source_location();
+      error() << "fmod-functions expect two operands" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    // Note that the semantics differ from the
+    // "floating point remainder" operation as defined by IEEE.
+    // Note that these do not take a rounding mode.
+    binary_exprt fmod_expr(
+      expr.arguments()[0], ID_floatbv_mod, expr.arguments()[1]);
+
+    fmod_expr.add_source_location() = source_location;
+
+    return std::move(fmod_expr);
+  }
   else if(identifier==CPROVER_PREFIX "allocate")
   {
     if(expr.arguments().size()!=2)

src/ansi-c/cprover_builtin_headers.h

@@ -86,6 +86,11 @@ double __CPROVER_fabs(double x);
 long double __CPROVER_fabsl(long double x);
 float __CPROVER_fabsf(float x);
 
+// modulo and remainder
+double __CPROVER_fmod(double, double);
+float __CPROVER_fmodf(float, float);
+long double __CPROVER_fmodl(long double, long double);
+
 // arrays
 __CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);
 // overwrite all of *dest (possibly using nondet values), even

src/ansi-c/library/cprover.h

@@ -117,6 +117,11 @@ double __CPROVER_fabs(double);
 long double __CPROVER_fabsl(long double);
 float __CPROVER_fabsf(float);
 
+// modulo and remainder
+double __CPROVER_fmod(double, double);
+float __CPROVER_fmodf(float, float);
+long double __CPROVER_fmodl(long double, long double);
+
 // arrays
 //__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);
 void __CPROVER_array_copy(const void *dest, const void *src);

src/ansi-c/library/math.c

@@ -2140,10 +2140,10 @@ long double __sort_of_CPROVER_remainderl (int rounding_mode, long double x, long
 #define __CPROVER_FENV_H_INCLUDED
 #endif
 
-double __sort_of_CPROVER_remainder (int rounding_mode, double x, double y);
-
-double fmod(double x, double y) { return __sort_of_CPROVER_remainder(FE_TOWARDZERO, x, y); }
-
+double fmod(double x, double y)
+{
+  return __CPROVER_fmod(x, y);
+}
 
 /* FUNCTION: fmodf */
 
@@ -2157,10 +2157,10 @@ double fmod(double x, double y) { return __sort_of_CPROVER_remainder(FE_TOWARDZE
 #define __CPROVER_FENV_H_INCLUDED
 #endif
 
-float __sort_of_CPROVER_remainderf (int rounding_mode, float x, float y);
-
-float fmodf(float x, float y) { return __sort_of_CPROVER_remainderf(FE_TOWARDZERO, x, y); }
-
+float fmodf(float x, float y)
+{
+  return __CPROVER_fmodf(x, y);
+}
 
 /* FUNCTION: fmodl */
 
@@ -2174,11 +2174,10 @@ float fmodf(float x, float y) { return __sort_of_CPROVER_remainderf(FE_TOWARDZER
 #define __CPROVER_FENV_H_INCLUDED
 #endif
 
-long double __sort_of_CPROVER_remainderl (int rounding_mode, long double x, long double y);
-
-long double fmodl(long double x, long double y) { return __sort_of_CPROVER_remainderl(FE_TOWARDZERO, x, y); }
-
-
+long double fmodl(long double x, long double y)
+{
+  return __CPROVER_fmodl(x, y);
+}
 
 /* ISO 9899:2011
  *

src/solvers/Makefile

@@ -102,6 +102,7 @@ SRC = $(BOOLEFORCE_SRC) \
       flattening/boolbv_equality.cpp \
       flattening/boolbv_extractbit.cpp \
       flattening/boolbv_extractbits.cpp \
+      flattening/boolbv_floatbv_mod_rem.cpp \
       flattening/boolbv_floatbv_op.cpp \
       flattening/boolbv_get.cpp \
       flattening/boolbv_ieee_float_rel.cpp \

src/solvers/flattening/boolbv.cpp

@@ -132,12 +132,14 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr ||
           expr.id()==ID_rol || expr.id()==ID_ror)
     return convert_shift(to_shift_expr(expr));
-  else 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_rem)
+  else if(
+    expr.id() == ID_floatbv_plus || expr.id() == ID_floatbv_minus ||
+    expr.id() == ID_floatbv_mult || expr.id() == ID_floatbv_div)
   {
     return convert_floatbv_op(to_ieee_float_op_expr(expr));
   }
+  else if(expr.id() == ID_floatbv_mod)
+    return convert_floatbv_mod_rem(to_binary_expr(expr));
   else if(expr.id()==ID_floatbv_typecast)
     return convert_floatbv_typecast(to_floatbv_typecast_expr(expr));
   else if(expr.id()==ID_concatenation)

src/solvers/flattening/boolbv.h

@@ -168,6 +168,7 @@ class boolbvt:public arrayst
   virtual bvt convert_div(const div_exprt &expr);
   virtual bvt convert_mod(const mod_exprt &expr);
   virtual bvt convert_floatbv_op(const ieee_float_op_exprt &);
+  virtual bvt convert_floatbv_mod_rem(const binary_exprt &);
   virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr);
   virtual bvt convert_member(const member_exprt &expr);
   virtual bvt convert_with(const with_exprt &expr);

src/solvers/flattening/boolbv_floatbv_mod_rem.cpp

@@ -0,0 +1,33 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "boolbv.h"
+
+#include <util/bitvector_types.h>
+
+#include <solvers/floatbv/float_utils.h>
+
+bvt boolbvt::convert_floatbv_mod_rem(const binary_exprt &expr)
+{
+  // Note that the expressions do not have rounding modes
+  // but float_utils requires one.
+
+  float_utilst float_utils(prop);
+
+  auto rm = bv_utils.build_constant(ieee_floatt::ROUND_TO_EVEN, 32);
+  float_utils.set_rounding_mode(rm);
+
+  float_utils.spec = ieee_float_spect(to_floatbv_type(expr.type()));
+
+  bvt lhs_as_bv = convert_bv(expr.lhs());
+  bvt rhs_as_bv = convert_bv(expr.rhs());
+
+  // float_utilst::rem implements lhs-(lhs/rhs)*rhs, which matches
+  // neither fmod() nor IEEE
+  return float_utils.rem(lhs_as_bv, rhs_as_bv);
+}

src/solvers/flattening/boolbv_floatbv_op.cpp

@@ -111,8 +111,6 @@ bvt boolbvt::convert_floatbv_op(const ieee_float_op_exprt &expr)
       return float_utils.mul(lhs_as_bv, rhs_as_bv);
     else if(expr.id()==ID_floatbv_div)
       return float_utils.div(lhs_as_bv, rhs_as_bv);
-    else if(expr.id()==ID_floatbv_rem)
-      return float_utils.rem(lhs_as_bv, rhs_as_bv);
     else
       UNREACHABLE;
   }

src/util/ieee_float.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "arith_tools.h"
 #include "bitvector_types.h"
+#include "c_types.h"
 #include "invariant.h"
 #include "std_expr.h"
 
@@ -55,6 +56,11 @@ void ieee_float_spect::from_type(const floatbv_typet &type)
     e=e-1; // no hidden bit
 }
 
+constant_exprt ieee_floatt::rounding_mode_expr(rounding_modet rm)
+{
+  return ::from_integer(static_cast<int>(rm), unsigned_int_type());
+}
+
 void ieee_floatt::print(std::ostream &out) const
 {
   out << to_ansi_c_string();