From 26efb3c7f1c0812dcd141d5bb4da0a8af351b1c2 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 5 Apr 2013 12:45:28 +0100 Subject: [PATCH] FPA bugfixes for denormal numbers. Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/fpa2bv_converter.cpp | 139 +++++++++++++++++----------- src/tactic/fpa/fpa2bv_converter.h | 2 +- 2 files changed, 85 insertions(+), 56 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 838090045..6d39dbfc4 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -423,9 +423,9 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args, unsigned ebits = m_util.get_ebits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range()); - expr_ref a_sgn(m), a_sig(m), a_exp(m), b_sgn(m), b_sig(m), b_exp(m); - unpack(x, a_sgn, a_sig, a_exp, true); - unpack(y, b_sgn, b_sig, b_exp, false); + expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m); + unpack(x, a_sgn, a_sig, a_exp, a_lz, false); + unpack(y, b_sgn, b_sig, b_exp, b_lz, false); dbg_decouple("fpa2bv_add_unpack_a_sgn", a_sgn); dbg_decouple("fpa2bv_add_unpack_a_sig", a_sig); @@ -511,7 +511,7 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, mk_nzero(f, nzero); mk_pzero(f, pzero); mk_minus_inf(f, ninf); - mk_plus_inf(f, pinf); + mk_plus_inf(f, pinf); expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m); expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m); @@ -575,13 +575,21 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, unsigned sbits = m_util.get_sbits(f->get_range()); SASSERT(ebits <= sbits); - expr_ref a_sgn(m), a_sig(m), a_exp(m), b_sgn(m), b_sig(m), b_exp(m); - unpack(x, a_sgn, a_sig, a_exp, true); - unpack(y, b_sgn, b_sig, b_exp, true); + expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m); + unpack(x, a_sgn, a_sig, a_exp, a_lz, true); + unpack(y, b_sgn, b_sig, b_exp, b_lz, true); - expr_ref lz_a(m), lz_b(m); - mk_leading_zeros(a_sig, ebits+2, lz_a); - mk_leading_zeros(b_sig, ebits+2, lz_b); + dbg_decouple("fpa2bv_mul_a_sig", a_sig); + dbg_decouple("fpa2bv_mul_a_exp", a_exp); + dbg_decouple("fpa2bv_mul_b_sig", b_sig); + dbg_decouple("fpa2bv_mul_b_exp", b_exp); + + expr_ref a_lz_ext(m), b_lz_ext(m); + a_lz_ext = m_bv_util.mk_zero_extend(2, a_lz); + b_lz_ext = m_bv_util.mk_zero_extend(2, b_lz); + + dbg_decouple("fpa2bv_mul_lz_a", a_lz); + dbg_decouple("fpa2bv_mul_lz_b", b_lz); expr_ref a_sig_ext(m), b_sig_ext(m); a_sig_ext = m_bv_util.mk_zero_extend(sbits, a_sig); @@ -597,9 +605,9 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_mul_res_sgn", res_sgn); - res_exp = m_bv_util.mk_bv_sub( - m_bv_util.mk_bv_add(a_exp_ext, b_exp_ext), - m_bv_util.mk_bv_add(lz_a, lz_b)); + res_exp = m_bv_util.mk_bv_add( + m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext), + m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext)); expr_ref product(m); product = m_bv_util.mk_bv_mul(a_sig_ext, b_sig_ext); @@ -614,11 +622,11 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, if (sbits >= 4) { expr_ref sticky(m); - sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(sbits-4, 0, l_p)); - rbits = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits-1, sbits-3, l_p), sticky); + sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(sbits-4, 0, product)); + rbits = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits-1, sbits-3, product), sticky); } else - rbits = m_bv_util.mk_concat(l_p, m_bv_util.mk_numeral(0, 4 - m_bv_util.get_bv_size(l_p))); + rbits = m_bv_util.mk_concat(l_p, m_bv_util.mk_numeral(0, 4 - sbits)); SASSERT(m_bv_util.get_bv_size(rbits) == 4); res_sig = m_bv_util.mk_concat(h_p, rbits); @@ -719,9 +727,9 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, unsigned sbits = m_util.get_sbits(f->get_range()); SASSERT(ebits <= sbits); - expr_ref a_sgn(m), a_sig(m), a_exp(m), b_sgn(m), b_sig(m), b_exp(m); - unpack(x, a_sgn, a_sig, a_exp, true); - unpack(y, b_sgn, b_sig, b_exp, true); + expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m); + unpack(x, a_sgn, a_sig, a_exp, a_lz, true); + unpack(y, b_sgn, b_sig, b_exp, b_lz, true); unsigned extra_bits = sbits+2; expr_ref a_sig_ext(m), b_sig_ext(m); @@ -736,7 +744,13 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, expr * signs[2] = { a_sgn, b_sgn }; res_sgn = m_bv_util.mk_bv_xor(2, signs); - res_exp = m_bv_util.mk_bv_sub(a_exp_ext, b_exp_ext); + expr_ref a_lz_ext(m), b_lz_ext(m); + a_lz_ext = m_bv_util.mk_zero_extend(2, a_lz); + b_lz_ext = m_bv_util.mk_zero_extend(2, b_lz); + + res_exp = m_bv_util.mk_bv_sub( + m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext), + m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext)); expr_ref quotient(m); quotient = m.mk_app(m_bv_util.get_fid(), OP_BUDIV, a_sig_ext, b_sig_ext); @@ -829,10 +843,10 @@ void fpa2bv_converter::mk_remainder(func_decl * f, unsigned num, expr * const * unsigned ebits = m_util.get_ebits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range()); - expr_ref a_sgn(m), a_sig(m), a_exp(m); - expr_ref b_sgn(m), b_sig(m), b_exp(m); - unpack(x, a_sgn, a_sig, a_exp, true); - unpack(y, b_sgn, b_sig, b_exp, true); + expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m); + expr_ref b_sgn(m), b_sig(m), b_exp(m), b_lz(m); + unpack(x, a_sgn, a_sig, a_exp, a_lz, true); + unpack(y, b_sgn, b_sig, b_exp, b_lz, true); BVSLT(a_exp, b_exp, c6); v6 = x; @@ -1062,16 +1076,16 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar expr_ref rm_is_to_neg(m); mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); - expr_ref a_sgn(m), a_sig(m), a_exp(m); - expr_ref b_sgn(m), b_sig(m), b_exp(m); - expr_ref c_sgn(m), c_sig(m), c_exp(m); - unpack(x, a_sgn, a_sig, a_exp, true); - unpack(y, b_sgn, b_sig, b_exp, true); - unpack(z, c_sgn, c_sig, c_exp, false); + expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m); + expr_ref b_sgn(m), b_sig(m), b_exp(m), b_lz(m); + expr_ref c_sgn(m), c_sig(m), c_exp(m), c_lz(m); + unpack(x, a_sgn, a_sig, a_exp, a_lz, true); + unpack(y, b_sgn, b_sig, b_exp, b_lz, true); + unpack(z, c_sgn, c_sig, c_exp, c_lz, false); - expr_ref lz_a(m), lz_b(m); - mk_leading_zeros(a_sig, ebits+2, lz_a); - mk_leading_zeros(b_sig, ebits+2, lz_b); + expr_ref a_lz_ext(m), b_lz_ext(m); + a_lz_ext = m_bv_util.mk_zero_extend(2, a_lz); + b_lz_ext = m_bv_util.mk_zero_extend(2, b_lz); expr_ref a_sig_ext(m), b_sig_ext(m); a_sig_ext = m_bv_util.mk_zero_extend(sbits, a_sig); @@ -1089,7 +1103,7 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar mul_exp = m_bv_util.mk_bv_sub( m_bv_util.mk_bv_add(a_exp_ext, b_exp_ext), - m_bv_util.mk_bv_add(lz_a, lz_b)); + m_bv_util.mk_bv_add(a_lz_ext, b_lz_ext)); mul_sig = m_bv_util.mk_bv_mul(a_sig_ext, b_sig_ext); @@ -1209,8 +1223,11 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * unsigned sbits = m_util.get_sbits(f->get_range()); SASSERT(ebits < sbits); - expr_ref a_sgn(m), a_sig(m), a_exp(m); - unpack(x, a_sgn, a_sig, a_exp, true); + expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m); + unpack(x, a_sgn, a_sig, a_exp, a_lz, true); + + dbg_decouple("fpa2bv_r2i_unpacked_sig", a_sig); + dbg_decouple("fpa2bv_r2i_unpacked_exp", a_exp); expr_ref exp_is_small(m), exp_h(m), one_1(m); exp_h = m_bv_util.mk_extract(ebits-1, ebits-1, a_exp); @@ -1456,8 +1473,8 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a // otherwise: the actual conversion with rounding. sort * s = f->get_range(); - expr_ref sgn(m), sig(m), exp(m); - unpack(x, sgn, sig, exp, true); + expr_ref sgn(m), sig(m), exp(m), lz(m); + unpack(x, sgn, sig, exp, lz, true); expr_ref res_sgn(m), res_sig(m), res_exp(m); @@ -1818,7 +1835,7 @@ void fpa2bv_converter::mk_unbias(expr * e, expr_ref & result) { result = m_bv_util.mk_concat(n_leading, rest); } -void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp, bool normalize) { +void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & lz, bool normalize) { SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT)); SASSERT(to_app(e)->get_num_args() == 3); @@ -1837,23 +1854,29 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref expr_ref normal_sig(m), normal_exp(m); normal_sig = m_bv_util.mk_concat(m_bv_util.mk_numeral(1, 1), sig); mk_unbias(exp, normal_exp); + dbg_decouple("fpa2bv_unpack_normal_exp", normal_exp); expr_ref denormal_sig(m), denormal_exp(m); - denormal_sig = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 1), sig); + denormal_sig = m_bv_util.mk_zero_extend(1, sig); denormal_exp = m_bv_util.mk_numeral(1, ebits); mk_unbias(denormal_exp, denormal_exp); + dbg_decouple("fpa2bv_unpack_denormal_exp", denormal_exp); - dbg_decouple("fpa2bv_unpack_denormal_exp", denormal_exp); + expr_ref zero_e(m); + zero_e = m_bv_util.mk_numeral(0, ebits); if (normalize) { - expr_ref is_sig_zero(m), shift(m), lz(m), zero_s(m), zero_e(m); - zero_s = m_bv_util.mk_numeral(0, sbits-1); - zero_e = m_bv_util.mk_numeral(0, ebits); - m_simp.mk_eq(zero_s, sig, is_sig_zero); - mk_leading_zeros(sig, ebits, lz); - m_simp.mk_ite(is_sig_zero, zero_e, lz, shift); - SASSERT(is_well_sorted(m, is_sig_zero)); - SASSERT(is_well_sorted(m, lz)); + expr_ref lz_d(m); + mk_leading_zeros(denormal_sig, ebits, lz_d); + m_simp.mk_ite(is_normal, zero_e, lz_d, lz); + dbg_decouple("fpa2bv_unpack_lz", lz); + + expr_ref is_sig_zero(m), shift(m), zero_s(m); + zero_s = m_bv_util.mk_numeral(0, sbits); + m_simp.mk_eq(zero_s, denormal_sig, is_sig_zero); + m_simp.mk_ite(is_sig_zero, zero_e, lz, shift); + dbg_decouple("fpa2bv_unpack_shift", shift); + SASSERT(is_well_sorted(m, is_sig_zero)); SASSERT(is_well_sorted(m, shift)); SASSERT(m_bv_util.get_bv_size(shift) == ebits); if (ebits <= sbits) { @@ -1872,10 +1895,11 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref m_simp.mk_eq(zero_s, sh, is_sh_zero); short_shift = m_bv_util.mk_extract(sbits-1, 0, shift); m_simp.mk_ite(is_sh_zero, short_shift, sbits_s, sl); - denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, sl); - } - denormal_exp = m_bv_util.mk_bv_sub(denormal_exp, shift); + denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, sl); + } } + else + lz = zero_e; SASSERT(is_well_sorted(m, normal_sig)); SASSERT(is_well_sorted(m, denormal_sig)); @@ -2020,8 +2044,12 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & dbg_decouple("fpa2bv_rnd_beta", beta); - expr_ref sigma(m), sigma_add(m); - sigma_add = m_bv_util.mk_bv_add(exp, m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1), ebits+2)); + dbg_decouple("fpa2bv_rnd_e_min", e_min); + dbg_decouple("fpa2bv_rnd_e_max", e_max); + + expr_ref sigma(m), sigma_add(m), e_min_p2(m); + sigma_add = m_bv_util.mk_bv_sub(exp, m_bv_util.mk_sign_extend(2, e_min)); + sigma_add = m_bv_util.mk_bv_add(sigma_add, m_bv_util.mk_numeral(1, ebits+2)); m_simp.mk_ite(TINY, sigma_add, lz, sigma); dbg_decouple("fpa2bv_rnd_sigma", sigma); @@ -2034,7 +2062,8 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & unsigned sig_size = m_bv_util.get_bv_size(sig); SASSERT(sig_size == sbits+4); - unsigned sigma_size = m_bv_util.get_bv_size(sigma); + SASSERT(m_bv_util.get_bv_size(sigma) == ebits+2); + unsigned sigma_size = ebits+2; expr_ref sigma_neg(m), sigma_cap(m), sigma_neg_capped(m), sigma_lt_zero(m), sig_ext(m), rs_sig(m), ls_sig(m), big_sh_sig(m), sigma_le_cap(m); diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/tactic/fpa/fpa2bv_converter.h index 6ac1d2b8b..e5d546763 100644 --- a/src/tactic/fpa/fpa2bv_converter.h +++ b/src/tactic/fpa/fpa2bv_converter.h @@ -135,7 +135,7 @@ protected: void mk_bias(expr * e, expr_ref & result); void mk_unbias(expr * e, expr_ref & result); - void unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp, bool normalize); + void unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & lz, bool normalize); void round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & result); void add_core(unsigned sbits, unsigned ebits, expr_ref & rm,