From 7767a9c03b7dfbde3abdfe2565cc5833aca734df Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 27 May 2026 23:25:13 +0000 Subject: [PATCH 1/3] ansi-c: handle __builtin_isfinite and __builtin_finite{,f,l} GCC's macros expand isfinite(x) to __builtin_isfinite(x), yet c_typecheck_expr.cpp only recognised the __CPROVER_-prefixed helpers (__CPROVER_isfinite{f,d,ld}). As a result, on glibc systems where isfinite() goes through __builtin_isfinite, CBMC failed to lower the call to an isfinite_exprt and instead treated the call as a body-less function. Symptoms include a 'no body for callee __builtin_isfinite' warning and havocked nondet results that make assert(isfinite(...)) fail. Aligns with the existing handling of __builtin_isnan, __builtin_isinf, __builtin_isinf_sign, and __builtin_isnormal. Add the missing identifiers to the isfinite_exprt branch of c_typecheck_expr.cpp: __builtin_isfinite (modern variant) __builtin_finite (older glibc internal alias) __builtin_finitef (float variant) __builtin_finitel (long double variant) Also add fallback library bodies in library/math.c so that indirect calls (function pointers etc.) resolve correctly, mirroring the existing __builtin_isnan{,f} entries. Stub regression/cbmc-library/ test directories accompany each new library entry, as required by library_check.sh. Co-authored-by: Kiro --- .../cbmc-library/__builtin_finite/main.c | 9 ++++++ .../cbmc-library/__builtin_finite/test.desc | 8 ++++++ .../cbmc-library/__builtin_finitef/main.c | 9 ++++++ .../cbmc-library/__builtin_finitef/test.desc | 8 ++++++ .../cbmc-library/__builtin_finitel/main.c | 9 ++++++ .../cbmc-library/__builtin_finitel/test.desc | 8 ++++++ .../cbmc-library/__builtin_isfinite/main.c | 9 ++++++ .../cbmc-library/__builtin_isfinite/test.desc | 8 ++++++ src/ansi-c/c_typecheck_expr.cpp | 9 ++++-- src/ansi-c/library/math.c | 28 +++++++++++++++++++ 10 files changed, 102 insertions(+), 3 deletions(-) create mode 100644 regression/cbmc-library/__builtin_finite/main.c create mode 100644 regression/cbmc-library/__builtin_finite/test.desc create mode 100644 regression/cbmc-library/__builtin_finitef/main.c create mode 100644 regression/cbmc-library/__builtin_finitef/test.desc create mode 100644 regression/cbmc-library/__builtin_finitel/main.c create mode 100644 regression/cbmc-library/__builtin_finitel/test.desc create mode 100644 regression/cbmc-library/__builtin_isfinite/main.c create mode 100644 regression/cbmc-library/__builtin_isfinite/test.desc diff --git a/regression/cbmc-library/__builtin_finite/main.c b/regression/cbmc-library/__builtin_finite/main.c new file mode 100644 index 00000000000..b75766faa4f --- /dev/null +++ b/regression/cbmc-library/__builtin_finite/main.c @@ -0,0 +1,9 @@ +#include +#include + +int main() +{ + __builtin_finite(); + assert(0); + return 0; +} diff --git a/regression/cbmc-library/__builtin_finite/test.desc b/regression/cbmc-library/__builtin_finite/test.desc new file mode 100644 index 00000000000..9542d988e8d --- /dev/null +++ b/regression/cbmc-library/__builtin_finite/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c +--pointer-check --bounds-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-library/__builtin_finitef/main.c b/regression/cbmc-library/__builtin_finitef/main.c new file mode 100644 index 00000000000..36e957d6c2b --- /dev/null +++ b/regression/cbmc-library/__builtin_finitef/main.c @@ -0,0 +1,9 @@ +#include +#include + +int main() +{ + __builtin_finitef(); + assert(0); + return 0; +} diff --git a/regression/cbmc-library/__builtin_finitef/test.desc b/regression/cbmc-library/__builtin_finitef/test.desc new file mode 100644 index 00000000000..9542d988e8d --- /dev/null +++ b/regression/cbmc-library/__builtin_finitef/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c +--pointer-check --bounds-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-library/__builtin_finitel/main.c b/regression/cbmc-library/__builtin_finitel/main.c new file mode 100644 index 00000000000..faf765021b6 --- /dev/null +++ b/regression/cbmc-library/__builtin_finitel/main.c @@ -0,0 +1,9 @@ +#include +#include + +int main() +{ + __builtin_finitel(); + assert(0); + return 0; +} diff --git a/regression/cbmc-library/__builtin_finitel/test.desc b/regression/cbmc-library/__builtin_finitel/test.desc new file mode 100644 index 00000000000..9542d988e8d --- /dev/null +++ b/regression/cbmc-library/__builtin_finitel/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c +--pointer-check --bounds-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-library/__builtin_isfinite/main.c b/regression/cbmc-library/__builtin_isfinite/main.c new file mode 100644 index 00000000000..fe18866455a --- /dev/null +++ b/regression/cbmc-library/__builtin_isfinite/main.c @@ -0,0 +1,9 @@ +#include +#include + +int main() +{ + __builtin_isfinite(); + assert(0); + return 0; +} diff --git a/regression/cbmc-library/__builtin_isfinite/test.desc b/regression/cbmc-library/__builtin_isfinite/test.desc new file mode 100644 index 00000000000..9542d988e8d --- /dev/null +++ b/regression/cbmc-library/__builtin_isfinite/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c +--pointer-check --bounds-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index afc0f3ca884..1c8f3fceb80 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -3246,9 +3246,12 @@ exprt c_typecheck_baset::do_special_functions( return typecast_exprt::conditional_cast(isnan_expr, expr.type()); } - else if(identifier==CPROVER_PREFIX "isfinitef" || - identifier==CPROVER_PREFIX "isfinited" || - identifier==CPROVER_PREFIX "isfiniteld") + else if( + identifier == CPROVER_PREFIX "isfinitef" || + identifier == CPROVER_PREFIX "isfinited" || + identifier == CPROVER_PREFIX "isfiniteld" || + identifier == "__builtin_isfinite" || identifier == "__builtin_finite" || + identifier == "__builtin_finitef" || identifier == "__builtin_finitel") { if(expr.arguments().size()!=1) { diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c index 32b6afa9fa1..0ec251748d5 100644 --- a/src/ansi-c/library/math.c +++ b/src/ansi-c/library/math.c @@ -251,6 +251,34 @@ int __builtin_isnanf(float f) return __CPROVER_isnanf(f); } +/* FUNCTION: __builtin_isfinite */ + +int __builtin_isfinite(double d) +{ + return __CPROVER_isfinited(d); +} + +/* FUNCTION: __builtin_finite */ + +int __builtin_finite(double d) +{ + return __CPROVER_isfinited(d); +} + +/* FUNCTION: __builtin_finitef */ + +int __builtin_finitef(float f) +{ + return __CPROVER_isfinitef(f); +} + +/* FUNCTION: __builtin_finitel */ + +int __builtin_finitel(long double ld) +{ + return __CPROVER_isfiniteld(ld); +} + /* FUNCTION: __builtin_huge_valf */ float __builtin_huge_valf(void) From 564281f1561c2fb3f87247eeffd9c4c816e11563 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 27 May 2026 23:26:22 +0000 Subject: [PATCH 2/3] boolbv: fix fixedbv-type check in convert_rest for ID_isfinite The ID_isfinite branch in boolbvt::convert_rest tested 'op.id() == ID_fixedbv', but ID_fixedbv is a *type* id and op is the operand expression, not a type. The dead branch never matched and fixedbv operands fell through to SUB::convert_rest, which is not prepared to lower an isfinite expression and would yield an unexpected result or conversion failure. The neighbouring ID_isnan, ID_isinf, and ID_isnormal branches all correctly use 'op.type().id() == ID_fixedbv'. Bring ID_isfinite into line. Pre-existing typo, unrelated to the surrounding refactoring; fixed here because it sits in the immediate neighbourhood of changes to the floatbv branch and to keep the fixedbv handling consistent. Co-authored-by: Kiro --- src/solvers/flattening/boolbv.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 361c42e5d8b..bdeb176dd8f 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -461,7 +461,7 @@ literalt boolbvt::convert_rest(const exprt &expr) !float_utils.is_infinity(bv), !float_utils.is_NaN(bv)); } - else if(op.id() == ID_fixedbv) + else if(op.type().id() == ID_fixedbv) return const_literal(true); } else if(expr.id()==ID_isinf) From f1cae3dbcdff77daf17e9b34371bd62cfe41db2e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 28 Apr 2026 11:45:00 +0000 Subject: [PATCH 3/3] Align floating-point predicates across float_utilst and float_bvt - Add float_utilst::is_finite and use it (float_bvt already has is_finite). - Remove unused float_utilst::is_plus_inf, float_utilst::is_minus_inf (float_bvt does not have these either). - Switch the ID_isfinite floatbv branch in boolbvt::convert_rest to the new helper. Add a regression/cbmc/Float-predicates test exercising isfinite and isinf via against both the default SAT and the SMT (Z3) backends. Tagging the SMT test with smt-backend keeps it out of the default and paths-lifo profiles, matching the convention used by other tests that hard-code --smt2 --z3. Tests targeting predicates continue to pass. Co-authored-by: Kiro --- regression/cbmc/Float-predicates/main.c | 28 +++++++++++++++++++ regression/cbmc/Float-predicates/test.desc | 10 +++++++ .../cbmc/Float-predicates/test_smt.desc | 10 +++++++ src/solvers/flattening/boolbv.cpp | 4 +-- src/solvers/floatbv/float_utils.cpp | 23 ++++----------- src/solvers/floatbv/float_utils.h | 4 +-- 6 files changed, 56 insertions(+), 23 deletions(-) create mode 100644 regression/cbmc/Float-predicates/main.c create mode 100644 regression/cbmc/Float-predicates/test.desc create mode 100644 regression/cbmc/Float-predicates/test_smt.desc diff --git a/regression/cbmc/Float-predicates/main.c b/regression/cbmc/Float-predicates/main.c new file mode 100644 index 00000000000..ed832d662d0 --- /dev/null +++ b/regression/cbmc/Float-predicates/main.c @@ -0,0 +1,28 @@ +// Test floating-point classification predicates: isfinite, isinf (signed). + +#include +#include + +int main() +{ + float pos_inf = 1.0f / 0.0f; + float neg_inf = -1.0f / 0.0f; + float nan_val = 0.0f / 0.0f; + float normal = 1.5f; + float zero = 0.0f; + + // isfinite + assert(isfinite(normal)); + assert(isfinite(zero)); + assert(!isfinite(pos_inf)); + assert(!isfinite(neg_inf)); + assert(!isfinite(nan_val)); + + // isinf with sign + assert(isinf(pos_inf) && pos_inf > 0); + assert(isinf(neg_inf) && neg_inf < 0); + assert(!isinf(normal)); + assert(!isinf(nan_val)); + + return 0; +} diff --git a/regression/cbmc/Float-predicates/test.desc b/regression/cbmc/Float-predicates/test.desc new file mode 100644 index 00000000000..9334190d2a1 --- /dev/null +++ b/regression/cbmc/Float-predicates/test.desc @@ -0,0 +1,10 @@ +CORE no-new-smt +main.c +--floatbv +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Floating-point classification predicates. diff --git a/regression/cbmc/Float-predicates/test_smt.desc b/regression/cbmc/Float-predicates/test_smt.desc new file mode 100644 index 00000000000..fe763464c98 --- /dev/null +++ b/regression/cbmc/Float-predicates/test_smt.desc @@ -0,0 +1,10 @@ +CORE smt-backend no-new-smt +main.c +--smt2 --z3 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Floating-point classification predicates (SMT path). diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index bdeb176dd8f..4743932bfea 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -457,9 +457,7 @@ literalt boolbvt::convert_rest(const exprt &expr) if(op.type().id() == ID_floatbv) { float_utilst float_utils(prop, to_floatbv_type(op.type())); - return prop.land( - !float_utils.is_infinity(bv), - !float_utils.is_NaN(bv)); + return float_utils.is_finite(bv); } else if(op.type().id() == ID_fixedbv) return const_literal(true); diff --git a/src/solvers/floatbv/float_utils.cpp b/src/solvers/floatbv/float_utils.cpp index ba72bb09b21..464eb142360 100644 --- a/src/solvers/floatbv/float_utils.cpp +++ b/src/solvers/floatbv/float_utils.cpp @@ -813,15 +813,6 @@ literalt float_utilst::is_zero(const bvt &src) return bv_utils.is_zero(all_but_sign); } -literalt float_utilst::is_plus_inf(const bvt &src) -{ - bvt and_bv; - and_bv.push_back(!sign_bit(src)); - and_bv.push_back(exponent_all_ones(src)); - and_bv.push_back(fraction_all_zeros(src)); - return prop.land(and_bv); -} - literalt float_utilst::is_infinity(const bvt &src) { return prop.land( @@ -841,21 +832,17 @@ bvt float_utilst::get_fraction(const bvt &src) return bv_utils.extract(src, 0, spec.f-1); } -literalt float_utilst::is_minus_inf(const bvt &src) -{ - bvt and_bv; - and_bv.push_back(sign_bit(src)); - and_bv.push_back(exponent_all_ones(src)); - and_bv.push_back(fraction_all_zeros(src)); - return prop.land(and_bv); -} - literalt float_utilst::is_NaN(const bvt &src) { return prop.land(exponent_all_ones(src), !fraction_all_zeros(src)); } +literalt float_utilst::is_finite(const bvt &src) +{ + return !exponent_all_ones(src); +} + literalt float_utilst::exponent_all_ones(const bvt &src) { bvt exponent=src; diff --git a/src/solvers/floatbv/float_utils.h b/src/solvers/floatbv/float_utils.h index e277847e171..f5c9a29b811 100644 --- a/src/solvers/floatbv/float_utils.h +++ b/src/solvers/floatbv/float_utils.h @@ -107,9 +107,9 @@ class float_utilst literalt is_normal(const bvt &); literalt is_zero(const bvt &); // this returns true on both 0 and -0 literalt is_infinity(const bvt &); - literalt is_plus_inf(const bvt &); - literalt is_minus_inf(const bvt &); literalt is_NaN(const bvt &); + /// Returns true iff \p src is finite (not NaN and not infinity). + literalt is_finite(const bvt &); // add/sub virtual bvt add_sub(const bvt &src1, const bvt &src2, bool subtract);