introduce __CPROVER_remainder functions

This adds the __CPROVER_remainder family of functions, which are mapped to
floatbv_rem.

Author: kroening

src/ansi-c/c_typecheck_expr.cpp

@@ -2591,6 +2591,30 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(fmod_expr);
   }
+  else if(
+    identifier == CPROVER_PREFIX "remainder" ||
+    identifier == CPROVER_PREFIX "remainderf" ||
+    identifier == CPROVER_PREFIX "remainderl")
+  {
+    if(expr.arguments().size() != 2)
+    {
+      error().source_location = f_op.source_location();
+      error() << "remainder-functions expect two operands" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    // The semantics of these functions is meant to match the
+    // "floating point remainder" operation as defined by IEEE.
+    // Note that these do not take a rounding mode.
+    binary_exprt floatbv_rem_expr(
+      expr.arguments()[0], ID_floatbv_rem, expr.arguments()[1]);
+
+    floatbv_rem_expr.add_source_location() = source_location;
+
+    return std::move(floatbv_rem_expr);
+  }
   else if(identifier==CPROVER_PREFIX "allocate")
   {
     if(expr.arguments().size()!=2)

src/ansi-c/cprover_builtin_headers.h

@@ -90,6 +90,9 @@ float __CPROVER_fabsf(float x);
 double __CPROVER_fmod(double, double);
 float __CPROVER_fmodf(float, float);
 long double __CPROVER_fmodl(long double, long double);
+double __CPROVER_remainder(double, double);
+float __CPROVER_remainderf(float, float);
+long double __CPROVER_remainderl(long double, long double);
 
 // arrays
 __CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);

src/ansi-c/library/cprover.h

@@ -121,6 +121,9 @@ float __CPROVER_fabsf(float);
 double __CPROVER_fmod(double, double);
 float __CPROVER_fmodf(float, float);
 long double __CPROVER_fmodl(long double, long double);
+double __CPROVER_remainder(double, double);
+float __CPROVER_remainderf(float, float);
+long double __CPROVER_remainderl(long double, long double);
 
 // arrays
 //__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);

src/solvers/flattening/boolbv.cpp

@@ -140,6 +140,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   }
   else if(expr.id() == ID_floatbv_mod)
     return convert_floatbv_mod_rem(to_binary_expr(expr));
+  else if(expr.id() == ID_floatbv_rem)
+    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/smt2/smt2_conv.cpp

@@ -1293,6 +1293,10 @@ void smt2_convt::convert_expr(const exprt &expr)
   {
     convert_floatbv_mult(to_ieee_float_op_expr(expr));
   }
+  else if(expr.id() == ID_floatbv_rem)
+  {
+    convert_floatbv_rem(to_binary_expr(expr));
+  }
   else if(expr.id()==ID_address_of)
   {
     const address_of_exprt &address_of_expr = to_address_of_expr(expr);
@@ -3631,6 +3635,29 @@ void smt2_convt::convert_floatbv_mult(const ieee_float_op_exprt &expr)
     convert_floatbv(expr);
 }
 
+void smt2_convt::convert_floatbv_rem(const binary_exprt &expr)
+{
+  DATA_INVARIANT(
+    expr.type().id() == ID_floatbv,
+    "type of ieee floating point expression shall be floatbv");
+
+  if(use_FPA_theory)
+  {
+    // Note that these do not have a rounding mode
+    out << "(fp.rem ";
+    convert_expr(expr.lhs());
+    out << " ";
+    convert_expr(expr.rhs());
+    out << ")";
+  }
+  else
+  {
+    SMT2_TODO(
+      "smt2_convt::convert_floatbv_rem to be implemented when not using "
+      "FPA_theory");
+  }
+}
+
 void smt2_convt::convert_with(const with_exprt &expr)
 {
   // get rid of "with" that has more than three operands

src/solvers/smt2/smt2_conv.h

@@ -119,6 +119,7 @@ class smt2_convt : public stack_decision_proceduret
   void convert_floatbv_minus(const ieee_float_op_exprt &expr);
   void convert_floatbv_div(const ieee_float_op_exprt &expr);
   void convert_floatbv_mult(const ieee_float_op_exprt &expr);
+  void convert_floatbv_rem(const binary_exprt &expr);
   void convert_mod(const mod_exprt &expr);
   void convert_index(const index_exprt &expr);
   void convert_member(const member_exprt &expr);

src/solvers/smt2/smt2_parser.cpp

@@ -1217,6 +1217,27 @@ void smt2_parsert::setup_expressions()
     return function_application_ieee_float_op("fp.div", operands());
   };
 
+  expressions["fp.rem"] = [this] {
+    auto op = operands();
+
+    // Note that these do not have a rounding mode.
+    if(op.size() != 2)
+      throw error() << "fp.rem takes three operands";
+
+    if(op[0].type().id() != ID_floatbv || op[1].type().id() != ID_floatbv)
+      throw error() << "fp.rem takes FloatingPoint operands";
+
+    if(op[0].type() != op[1].type())
+    {
+      throw error()
+        << "fp.rem takes FloatingPoint operands with matching sort, "
+        << "but got " << smt2_format(op[0].type()) << " vs "
+        << smt2_format(op[1].type());
+    }
+
+    return binary_exprt(op[0], ID_floatbv_rem, op[1]);
+  };
+
   expressions["fp.eq"] = [this] {
     return function_application_ieee_float_eq(operands());
   };