Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Introduce floatbv_round_to_integral_exprt #8538

Open
wants to merge 1 commit into
base: develop
Choose a base branch
from
+601 −315
Open

Introduce floatbv_round_to_integral_exprt #8538

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 0 additions & 9 deletions regression/cbmc-library/__sort_of_CPROVER_round_to_integral-01/main.c
View file
Open in desktop

This file was deleted.

8 changes: 0 additions & 8 deletions regression/cbmc-library/__sort_of_CPROVER_round_to_integral-01/test.desc
View file
Open in desktop

This file was deleted.

9 changes: 0 additions & 9 deletions regression/cbmc-library/__sort_of_CPROVER_round_to_integralf-01/main.c
View file
Open in desktop

This file was deleted.

8 changes: 0 additions & 8 deletions regression/cbmc-library/__sort_of_CPROVER_round_to_integralf-01/test.desc
View file
Open in desktop

This file was deleted.

9 changes: 0 additions & 9 deletions regression/cbmc-library/__sort_of_CPROVER_round_to_integrall-01/main.c
View file
Open in desktop

This file was deleted.

8 changes: 0 additions & 8 deletions regression/cbmc-library/__sort_of_CPROVER_round_to_integrall-01/test.desc
View file
Open in desktop

This file was deleted.

78 changes: 78 additions & 0 deletions regression/smt2_solver/fp/roundToIntegral1.smt2
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
18 changes: 18 additions & 0 deletions src/ansi-c/c_typecheck_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3249,6 +3249,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;

Check warning on line 3261 in src/ansi-c/c_typecheck_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/ansi-c/c_typecheck_expr.cpp#L3259-L3261 

Added lines #L3259 - L3261 were not covered by tests
}

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" ||
Expand Down
3 changes: 3 additions & 0 deletions src/ansi-c/cprover_builtin_headers.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -94,6 +94,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);
Expand Down
Loading
Loading