mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-26 17:02:38 +00:00
Code Activity

Fix unsigned BV-to-FP exponent narrowing (#10189)

Browse source 
## Summary

Include the equal-width case in symbolic unsigned BV-to-FP exponent
saturation,
preventing positive exponents from being interpreted as negative by the
rounder.

Adds regression coverage for overflow and in-range values.

Fixes #7135.

## Testing

- `./build-review/test-z3 fpa`
- `./build-review/test-z3 /a` (92 passed)
- Symbolic-versus-numeral differential matrix (50 cases across five
width boundaries and all rounding modes)
- Exact-head fork `CI` and `OCaml Binding CI` workflows (passed)
This commit is contained in:
1sgtpepper 2026-07-23 23:57:15 +08:00 • committed by GitHub
parent df8d23960e
commit 53fa8f9cc4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 48 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -3237,8 +3237,9 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
// exp < bv_sz (+sign bit which is [0])
unsigned exp_worst_case_sz = (unsigned)((log((double)bv_sz) / log((double)2)) + 1.0);
if (exp_sz < exp_worst_case_sz) {
// exp_sz < exp_worst_case_sz and exp >= 0.
if (exp_sz <= exp_worst_case_sz) {
// round() interprets exp as signed, so replace positive values that
// cannot be represented before it consumes the narrowed exponent.
// Take the maximum legal exponent; this
// allows us to keep the most precision.
expr_ref max_exp(m), max_exp_bvsz(m), zero_sig_sz(m);

45
src/test/fpa.cpp
View file

@ -82,6 +82,49 @@ static void test_to_fp_from_real_interval() {
true);
}
// Preserve the signed value of the internal exponent when converting a symbolic
// unsigned bit-vector. In-range values must not take the overflow path.
static void test_to_fp_unsigned_exponent_width_boundary() {
run_fp_test(
"(set-logic QF_BVFP)\n"
"(set-option :model_validate true)\n"
"(declare-const high (_ BitVec 13))\n"
"(assert (or (= high #b1111111111110) (= high #b1111111111111)))\n"
"(assert (= ((_ to_fp_unsigned 2 11) RTN high) (fp #b0 #b10 #b1111111111)))\n"
"(assert (= ((_ to_fp_unsigned 2 11) RTZ high) (fp #b0 #b10 #b1111111111)))\n"
"(assert (= ((_ to_fp_unsigned 2 11) RTP high) (_ +oo 2 11)))\n"
"(assert (= ((_ to_fp_unsigned 2 11) RNE high) (_ +oo 2 11)))\n"
"(assert (= ((_ to_fp_unsigned 2 11) RNA high) (_ +oo 2 11)))\n"
"(declare-const small (_ BitVec 13))\n"
"(assert (or (= small #b0000000000001) (= small #b0000000000010)))\n"
"(assert (= ((_ to_fp_unsigned 2 11) RTN small)\n"
" (ite (= small #b0000000000001)\n"
" (fp #b0 #b01 #b0000000000)\n"
" (fp #b0 #b10 #b0000000000))))\n"
"(check-sat)\n",
true);
}
static void test_to_fp_unsigned_common_widths() {
run_fp_test(
"(set-logic QF_BVFP)\n"
"(set-option :model_validate true)\n"
"(declare-const high (_ BitVec 32))\n"
"(assert (or (= high #xfffffffe) (= high #xffffffff)))\n"
"(assert (= ((_ to_fp_unsigned 8 24) RTN high)\n"
" (fp #b0 #b10011110 #b11111111111111111111111)))\n"
"(assert (= ((_ to_fp_unsigned 8 24) RTZ high)\n"
" (fp #b0 #b10011110 #b11111111111111111111111)))\n"
"(assert (= ((_ to_fp_unsigned 8 24) RTP high)\n"
" (fp #b0 #b10011111 #b00000000000000000000000)))\n"
"(assert (= ((_ to_fp_unsigned 8 24) RNE high)\n"
" (fp #b0 #b10011111 #b00000000000000000000000)))\n"
"(assert (= ((_ to_fp_unsigned 8 24) RNA high)\n"
" (fp #b0 #b10011111 #b00000000000000000000000)))\n"
"(check-sat)\n",
true);
}
static void test_recfun_defined_function_soundness() {
run_fp_test(
"(set-option :model_validate true)\n"
@ -98,5 +141,7 @@ static void test_recfun_defined_function_soundness() {
void tst_fpa() {
test_fp_to_real_denormal();
test_to_fp_from_real_interval();
test_to_fp_unsigned_exponent_width_boundary();
test_to_fp_unsigned_common_widths();
test_recfun_defined_function_soundness();
}