Introduce floatbv_round_to_integral_exprt

This adds a new expression, floatbv_round_to_integral, which rounds an IEEE
754 floating-point number given as bit-vector to the nearest integer,
considering the explicitly given rounding mode.

Author: kroening

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

@@ -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)

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

@@ -3237,6 +3237,24 @@ exprt c_typecheck_baset::do_special_functions(
 
     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" ||

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

@@ -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);