From 53fa8f9cc4759b3afa2122a25b51b183c4e70f51 Mon Sep 17 00:00:00 2001 From: 1sgtpepper Date: Thu, 23 Jul 2026 23:57:15 +0800 Subject: [PATCH] Fix unsigned BV-to-FP exponent narrowing (#10189) ## 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) --- src/ast/fpa/fpa2bv_converter.cpp | 5 ++-- src/test/fpa.cpp | 45 ++++++++++++++++++++++++++++++++ 2 files changed, 48 insertions(+), 2 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index d2431174e8..7f17935123 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -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); diff --git a/src/test/fpa.cpp b/src/test/fpa.cpp index 632865cee6..07fc86fb9f 100644 --- a/src/test/fpa.cpp +++ b/src/test/fpa.cpp @@ -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(); }