Introduce floatbv_round_to_integral_exprt

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -358,13 +358,13 @@ assign_primitive_from_json(const exprt &expr, const jsont &json)
   }
   else if(expr.type() == java_double_type())
   {
-    ieee_floatt ieee_float(to_floatbv_type(expr.type()));
+    ieee_float_valuet ieee_float(to_floatbv_type(expr.type()));
     ieee_float.from_double(std::stod(json.value));
     result.add(code_frontend_assignt{expr, ieee_float.to_expr()});
   }
   else if(expr.type() == java_float_type())
   {
-    ieee_floatt ieee_float(to_floatbv_type(expr.type()));
+    ieee_float_valuet ieee_float(to_floatbv_type(expr.type()));
     ieee_float.from_float(std::stof(json.value));
     result.add(code_frontend_assignt{expr, ieee_float.to_expr()});
   }

jbmc/src/java_bytecode/expr2java.cpp

@@ -230,7 +230,7 @@ std::string expr2javat::convert_constant(
           (src.type()==java_double_type()))
   {
     // This converts NaNs to the canonical NaN
-    const ieee_floatt ieee_repr(to_constant_expr(src));
+    const ieee_float_valuet ieee_repr(to_constant_expr(src));
     if(ieee_repr.is_double())
       return floating_point_to_java_string(ieee_repr.to_double());
     return floating_point_to_java_string(ieee_repr.to_float());

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2181,16 +2181,19 @@
       is_float ? ieee_float_spect::single_precision()
                : ieee_float_spect::double_precision());
 
-    ieee_floatt value(spec);
     if(arg0.type().id() != ID_floatbv)
     {
+      // conversion from integer to float may need rounding
+      auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
       const mp_integer number = numeric_cast_v<mp_integer>(arg0);
+      ieee_floatt value(spec, rm);
       value.from_integer(number);
+      results[0] = value.to_expr();
     }
     else
-      value.from_expr(arg0);
-
-    results[0] = value.to_expr();
+    {
+      results[0] = ieee_float_valuet{arg0}.to_expr();
+    }
   }
   else
   {

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -782,7 +782,7 @@ void java_bytecode_parsert::rconstant_pool()
 
       case CONSTANT_Float:
       {
-        ieee_floatt value(ieee_float_spect::single_precision());
+        ieee_float_valuet value(ieee_float_spect::single_precision());
         value.unpack(entry.number);
         entry.expr = value.to_expr();
       }
@@ -794,7 +794,7 @@ void java_bytecode_parsert::rconstant_pool()
 
       case CONSTANT_Double:
       {
-        ieee_floatt value(ieee_float_spect::double_precision());
+        ieee_float_valuet value(ieee_float_spect::double_precision());
         value.unpack(entry.number);
         entry.expr = value.to_expr();
       }

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -938,7 +938,7 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
 
   // Expression representing 0.0
   const ieee_float_spect float_spec{to_floatbv_type(params[0].type())};
-  ieee_floatt zero_float(float_spec);
+  ieee_float_valuet zero_float(float_spec);
   zero_float.from_float(0.0);
   const constant_exprt zero = zero_float.to_expr();
 
@@ -996,16 +996,17 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
   string_expr_list.push_back(zero_string);
 
   // Case of -0.0
-  ieee_floatt minus_zero_float(float_spec);
+  ieee_float_valuet minus_zero_float(float_spec);
   minus_zero_float.from_float(-0.0f);
   condition_list.push_back(equal_exprt(arg, minus_zero_float.to_expr()));
   const refined_string_exprt minus_zero_string =
     string_literal_to_string_expr("-0.0", loc, symbol_table, code);
   string_expr_list.push_back(minus_zero_string);
 
   // Case of simple notation
-  ieee_floatt bound_inf_float(float_spec);
-  ieee_floatt bound_sup_float(float_spec);
+  auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+  ieee_floatt bound_inf_float(float_spec, rm);
+  ieee_floatt bound_sup_float(float_spec, rm);
   bound_inf_float.from_float(1e-3f);
   bound_sup_float.from_float(1e7f);
   bound_inf_float.change_spec(float_spec);

regression/smt2_solver/fp/roundToIntegral1.smt2

@@ -0,0 +1,78 @@
+(set-logic FP)
+
+(define-fun zero () (_ FloatingPoint 11 53) ((_ to_fp 11 53) RNE 0))
+(define-fun minus-zero () (_ FloatingPoint 11 53) (fp.neg zero))
+(define-fun one () (_ FloatingPoint 11 53) ((_ to_fp 11 53) RNE 1))
+(define-fun minus-one () (_ FloatingPoint 11 53) (fp.neg one))
+(define-fun zero-point-one () (_ FloatingPoint 11 53) ((_ to_fp 11 53) RNE 0.1))
+(define-fun minus-zero-point-one () (_ FloatingPoint 11 53) (fp.neg zero-point-one))
+(define-fun ten-point-one () (_ FloatingPoint 11 53) ((_ to_fp 11 53) RNE 10.1))
+(define-fun minus-ten-point-one () (_ FloatingPoint 11 53) (fp.neg ten-point-one))
+(define-fun ten () (_ FloatingPoint 11 53) ((_ to_fp 11 53) RNE 10))
+(define-fun minus-ten () (_ FloatingPoint 11 53) (fp.neg ten))
+(define-fun eleven () (_ FloatingPoint 11 53) ((_ to_fp 11 53) RNE 11))
+(define-fun minus-eleven () (_ FloatingPoint 11 53) (fp.neg eleven))
+(define-fun magic () (_ FloatingPoint 11 53) (fp #b0 #b10000110011 #x0000000000000))
+(define-fun dmax () (_ FloatingPoint 11 53) (fp #b0 #b11111111110 #xFFFFFFFFFFFFF))
+
+(assert (not (and
+
+  ; round up
+  (= (fp.roundToIntegral RTP (_ NaN 11 53)) (_ NaN 11 53))
+  (= (fp.roundToIntegral RTP (_ +oo 11 53)) (_ +oo 11 53))
+  (= (fp.roundToIntegral RTP (_ -oo 11 53)) (_ -oo 11 53))
+  (= (fp.roundToIntegral RTP zero) zero)
+  (= (fp.roundToIntegral RTP minus-zero) minus-zero)
+  (= (fp.roundToIntegral RTP one) one)
+  (= (fp.roundToIntegral RTP zero-point-one) one)
+  (= (fp.roundToIntegral RTP minus-zero-point-one) minus-zero)
+  (= (fp.roundToIntegral RTP ten-point-one) eleven)
+  (= (fp.roundToIntegral RTP minus-ten-point-one) minus-ten)
+  (= (fp.roundToIntegral RTP magic) magic)
+  (= (fp.roundToIntegral RTP dmax) dmax)
+
+  ; round down
+  (= (fp.roundToIntegral RTN (_ NaN 11 53)) (_ NaN 11 53))
+  (= (fp.roundToIntegral RTN (_ +oo 11 53)) (_ +oo 11 53))
+  (= (fp.roundToIntegral RTN (_ -oo 11 53)) (_ -oo 11 53))
+  (= (fp.roundToIntegral RTN zero) zero)
+  (= (fp.roundToIntegral RTN minus-zero) minus-zero)
+  (= (fp.roundToIntegral RTN one) one)
+  (= (fp.roundToIntegral RTN zero-point-one) zero)
+  (= (fp.roundToIntegral RTN minus-zero-point-one) minus-one)
+  (= (fp.roundToIntegral RTN ten-point-one) ten)
+  (= (fp.roundToIntegral RTN minus-ten-point-one) minus-eleven)
+  (= (fp.roundToIntegral RTN magic) magic)
+  (= (fp.roundToIntegral RTN dmax) dmax)
+
+  ; round to nearest ties to even
+  (= (fp.roundToIntegral RNE (_ NaN 11 53)) (_ NaN 11 53))
+  (= (fp.roundToIntegral RNE (_ +oo 11 53)) (_ +oo 11 53))
+  (= (fp.roundToIntegral RNE (_ -oo 11 53)) (_ -oo 11 53))
+  (= (fp.roundToIntegral RNE zero) zero)
+  (= (fp.roundToIntegral RNE minus-zero) minus-zero)
+  (= (fp.roundToIntegral RNE one) one)
+  (= (fp.roundToIntegral RNE zero-point-one) zero)
+  (= (fp.roundToIntegral RNE minus-zero-point-one) minus-zero)
+  (= (fp.roundToIntegral RNE ten-point-one) ten)
+  (= (fp.roundToIntegral RNE minus-ten-point-one) minus-ten)
+  (= (fp.roundToIntegral RNE magic) magic)
+  (= (fp.roundToIntegral RNE dmax) dmax)
+
+  ; round to zero
+  (= (fp.roundToIntegral RTZ (_ NaN 11 53)) (_ NaN 11 53))
+  (= (fp.roundToIntegral RTZ (_ +oo 11 53)) (_ +oo 11 53))
+  (= (fp.roundToIntegral RTZ (_ -oo 11 53)) (_ -oo 11 53))
+  (= (fp.roundToIntegral RTZ zero) zero)
+  (= (fp.roundToIntegral RTZ minus-zero) minus-zero)
+  (= (fp.roundToIntegral RTZ one) one)
+  (= (fp.roundToIntegral RTZ zero-point-one) zero)
+  (= (fp.roundToIntegral RTZ minus-zero-point-one) minus-zero)
+  (= (fp.roundToIntegral RTZ ten-point-one) ten)
+  (= (fp.roundToIntegral RTZ minus-ten-point-one) minus-ten)
+  (= (fp.roundToIntegral RTZ magic) magic)
+  (= (fp.roundToIntegral RTZ dmax) dmax)
+)))
+
+; should be unsat
+(check-sat)

src/analyses/interval_domain.cpp

@@ -288,7 +288,7 @@
     }
     else if(is_float(lhs.type()) && is_float(rhs.type()))
     {
-      ieee_floatt tmp(to_constant_expr(rhs));
+      ieee_float_valuet tmp(to_constant_expr(rhs));
       if(id==ID_lt)
         tmp.decrement();
       ieee_float_intervalt &fi=float_map[lhs_identifier];
@@ -313,7 +313,7 @@
     }
     else if(is_float(lhs.type()) && is_float(rhs.type()))
     {
-      ieee_floatt tmp(to_constant_expr(lhs));
+      ieee_float_valuet tmp(to_constant_expr(lhs));
       if(id==ID_lt)
         tmp.increment();
       ieee_float_intervalt &fi=float_map[rhs_identifier];

src/analyses/interval_domain.h

@@ -18,7 +18,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "ai_domain.h"
 
-typedef interval_templatet<ieee_floatt> ieee_float_intervalt;
+typedef interval_templatet<ieee_float_valuet> ieee_float_intervalt;
 
 class interval_domaint:public ai_domain_baset
 {

src/ansi-c/c_typecheck_expr.cpp

@@ -3237,6 +3237,24 @@
 
     return std::move(infl_expr);
   }
+  else if(
+    identifier == CPROVER_PREFIX "round_to_integralf" ||
+    identifier == CPROVER_PREFIX "round_to_integrald" ||
+    identifier == CPROVER_PREFIX "round_to_integralld")
+  {
+    if(expr.arguments().size() != 2)
+    {
+      error().source_location = f_op.source_location();
+      error() << identifier << " expects two arguments" << eom;
+      throw 0;
+    }
+
+    auto round_to_integral_expr =
+      floatbv_round_to_integral_exprt{expr.arguments()[0], expr.arguments()[1]};
+    round_to_integral_expr.add_source_location() = source_location;
+
+    return std::move(round_to_integral_expr);
+  }
   else if(
     identifier == CPROVER_PREFIX "abs" || identifier == CPROVER_PREFIX "labs" ||
     identifier == CPROVER_PREFIX "llabs" ||

src/ansi-c/cprover_builtin_headers.h

@@ -93,6 +93,9 @@ int __CPROVER_islessgreaterf(float f, float g);
 int __CPROVER_islessgreaterd(double f, double g);
 int __CPROVER_isunorderedf(float f, float g);
 int __CPROVER_isunorderedd(double f, double g);
+float __CPROVER_round_to_integralf(float, int);
+double __CPROVER_round_to_integrald(double, int);
+long double __CPROVER_round_to_integralld(long double, int);
 
 // absolute value
 int __CPROVER_abs(int x);

src/ansi-c/expr2c.cpp

@@ -1912,7 +1912,7 @@ std::string expr2ct::convert_constant(
   }
   else if(type.id()==ID_floatbv)
   {
-    dest=ieee_floatt(to_constant_expr(src)).to_ansi_c_string();
+    dest = ieee_float_valuet(to_constant_expr(src)).to_ansi_c_string();
 
     if(!dest.empty() && isdigit(dest[dest.size() - 1]))
     {

src/ansi-c/goto-conversion/goto_check_c.cpp

@@ -761,12 +761,13 @@
       else if(old_type.id() == ID_floatbv) // float -> signed
       {
         // Note that the fractional part is truncated!
-        ieee_floatt upper(to_floatbv_type(old_type));
+        auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+        ieee_floatt upper(to_floatbv_type(old_type), rm);
         upper.from_integer(power(2, new_width - 1));
         const binary_relation_exprt no_overflow_upper(
           op, ID_lt, upper.to_expr());
 
-        ieee_floatt lower(to_floatbv_type(old_type));
+        ieee_floatt lower(to_floatbv_type(old_type), rm);
         lower.from_integer(-power(2, new_width - 1) - 1);
         const binary_relation_exprt no_overflow_lower(
           op, ID_gt, lower.to_expr());
@@ -844,12 +845,13 @@
       else if(old_type.id() == ID_floatbv) // float -> unsigned
       {
         // Note that the fractional part is truncated!
-        ieee_floatt upper(to_floatbv_type(old_type));
+        auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+        ieee_floatt upper(to_floatbv_type(old_type), rm);
         upper.from_integer(power(2, new_width));
         const binary_relation_exprt no_overflow_upper(
           op, ID_lt, upper.to_expr());
 
-        ieee_floatt lower(to_floatbv_type(old_type));
+        ieee_floatt lower(to_floatbv_type(old_type), rm);
         lower.from_integer(-1);
         const binary_relation_exprt no_overflow_lower(
           op, ID_gt, lower.to_expr());
@@ -1295,8 +1297,8 @@
     // -inf + +inf = NaN and +inf + -inf = NaN,
     // i.e., signs differ
     ieee_float_spect spec = ieee_float_spect(to_floatbv_type(plus_expr.type()));
-    exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr();
-    exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr();
+    exprt plus_inf = ieee_float_valuet::plus_infinity(spec).to_expr();
+    exprt minus_inf = ieee_float_valuet::minus_infinity(spec).to_expr();
 
     isnan = or_exprt(
       and_exprt(
@@ -1315,8 +1317,8 @@
 
     ieee_float_spect spec =
       ieee_float_spect(to_floatbv_type(minus_expr.type()));
-    exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr();
-    exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr();
+    exprt plus_inf = ieee_float_valuet::plus_infinity(spec).to_expr();
+    exprt minus_inf = ieee_float_valuet::minus_infinity(spec).to_expr();
 
     isnan = or_exprt(
       and_exprt(