From 9dfc2bc61e73ab6498ff63786a360dd8947ae37c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 5 Mar 2016 16:47:08 +0000 Subject: [PATCH] Fixed memory leaks in fpa2bv converter. Fixes #480 --- src/ast/fpa/fpa2bv_converter.cpp | 117 +++++++++++++++++-------------- src/ast/fpa/fpa2bv_converter.h | 13 ---- src/tactic/fpa/fpa2bv_tactic.cpp | 1 - 3 files changed, 65 insertions(+), 66 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 40bb7efe8..0d90e1c5a 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -81,7 +81,7 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) { SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_INTERNAL_RM)); TRACE("fpa2bv", tout << "mk_eq_rm a=" << mk_ismt2_pp(a, m) << std::endl; - tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;); + tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;); m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), result); } @@ -113,9 +113,10 @@ void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * a result = m.mk_true(); for (unsigned i = 0; i < num; i++) { for (unsigned j = i+1; j < num; j++) { - expr_ref eq(m); + expr_ref eq(m), neq(m); mk_eq(args[i], args[j], eq); - m_simp.mk_and(result, m.mk_not(eq), result); + neq = m.mk_not(eq); + m_simp.mk_and(result, neq, result); } } } @@ -422,10 +423,11 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, if (log2(sbits + 2) < ebits + 2) { // cap the delta - expr_ref cap(m), cap_le_delta(m); + expr_ref cap(m), cap_le_delta(m), exp_delta_ext(m); cap = m_bv_util.mk_numeral(sbits + 2, ebits + 2); cap_le_delta = m_bv_util.mk_ule(cap, m_bv_util.mk_zero_extend(2, exp_delta)); - m_simp.mk_ite(cap_le_delta, cap, m_bv_util.mk_zero_extend(2, exp_delta), exp_delta); + exp_delta_ext = m_bv_util.mk_zero_extend(2, exp_delta); + m_simp.mk_ite(cap_le_delta, cap, exp_delta_ext, exp_delta); exp_delta = m_bv_util.mk_extract(ebits - 1, 0, exp_delta); dbg_decouple("fpa2bv_add_exp_cap", cap); } @@ -465,7 +467,7 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref eq_sgn(m); m_simp.mk_eq(c_sgn, d_sgn, eq_sgn); - // dbg_decouple("fpa2bv_add_eq_sgn", eq_sgn); + dbg_decouple("fpa2bv_add_eq_sgn", eq_sgn); TRACE("fpa2bv_add_core", tout << "EQ_SGN = " << mk_ismt2_pp(eq_sgn, m) << std::endl; ); // two extra bits for catching the overflow. @@ -478,11 +480,10 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, dbg_decouple("fpa2bv_add_c_sig", c_sig); dbg_decouple("fpa2bv_add_shifted_d_sig", shifted_d_sig); - expr_ref sum(m); - m_simp.mk_ite(eq_sgn, - m_bv_util.mk_bv_add(c_sig, shifted_d_sig), - m_bv_util.mk_bv_sub(c_sig, shifted_d_sig), - sum); + expr_ref sum(m), c_plus_d(m), c_minus_d(m); + c_plus_d = m_bv_util.mk_bv_add(c_sig, shifted_d_sig); + c_minus_d = m_bv_util.mk_bv_sub(c_sig, shifted_d_sig); + m_simp.mk_ite(eq_sgn, c_plus_d, c_minus_d, sum); SASSERT(is_well_sorted(m, sum)); @@ -594,7 +595,7 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args, c6 = y_is_zero; v6 = x; - // Actual addition. + //// Actual addition. unsigned ebits = m_util.get_ebits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range()); @@ -949,8 +950,11 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_div_res_sig_shift_amount", res_sig_shift_amount); expr_ref shift_cond(m); shift_cond = m_bv_util.mk_ule(res_sig_lz, m_bv_util.mk_numeral(1, sbits + 4)); - m_simp.mk_ite(shift_cond, res_sig, m_bv_util.mk_bv_shl(res_sig, res_sig_shift_amount), res_sig); - m_simp.mk_ite(shift_cond, res_exp, m_bv_util.mk_bv_sub(res_exp, m_bv_util.mk_extract(ebits+1, 0, res_sig_shift_amount)), res_exp); + expr_ref res_sig_shifted(m), res_exp_shifted(m); + res_sig_shifted = m_bv_util.mk_bv_shl(res_sig, res_sig_shift_amount); + res_exp_shifted = m_bv_util.mk_bv_sub(res_exp, m_bv_util.mk_extract(ebits + 1, 0, res_sig_shift_amount)); + m_simp.mk_ite(shift_cond, res_sig, res_sig_shifted, res_sig); + m_simp.mk_ite(shift_cond, res_exp, res_exp_shifted, res_exp); round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, v8); @@ -1374,8 +1378,9 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, // (x is 0) || (y is 0) -> z m_simp.mk_or(x_is_zero, y_is_zero, c7); - expr_ref ite_c(m); - m_simp.mk_and(z_is_zero, m.mk_not(rm_is_to_neg), ite_c); + expr_ref ite_c(m), rm_is_not_to_neg(m); + rm_is_not_to_neg = m.mk_not(rm_is_to_neg); + m_simp.mk_and(z_is_zero, rm_is_not_to_neg, ite_c); mk_ite(ite_c, pzero, z, v7); // else comes the fused multiplication. @@ -1512,11 +1517,10 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_fma_add_e_sig", e_sig); dbg_decouple("fpa2bv_fma_add_shifted_f_sig", shifted_f_sig); - expr_ref sum(m); - m_simp.mk_ite(eq_sgn, - m_bv_util.mk_bv_add(e_sig, shifted_f_sig), - m_bv_util.mk_bv_sub(e_sig, shifted_f_sig), - sum); + expr_ref sum(m), e_plus_f(m), e_minus_f(m); + e_plus_f = m_bv_util.mk_bv_add(e_sig, shifted_f_sig); + e_minus_f = m_bv_util.mk_bv_sub(e_sig, shifted_f_sig), + m_simp.mk_ite(eq_sgn, e_plus_f, e_minus_f, sum); SASSERT(is_well_sorted(m, sum)); @@ -1664,10 +1668,10 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_sqrt_e_is_odd", e_is_odd); dbg_decouple("fpa2bv_sqrt_real_exp", real_exp); - expr_ref sig_prime(m); - m_simp.mk_ite(e_is_odd, m_bv_util.mk_concat(a_sig, zero1), - m_bv_util.mk_concat(zero1, a_sig), - sig_prime); + expr_ref sig_prime(m), a_z(m), z_a(m); + a_z = m_bv_util.mk_concat(a_sig, zero1); + z_a = m_bv_util.mk_concat(zero1, a_sig); + m_simp.mk_ite(e_is_odd, a_z, z_a, sig_prime); SASSERT(m_bv_util.get_bv_size(sig_prime) == sbits+1); dbg_decouple("fpa2bv_sqrt_sig_prime", sig_prime); @@ -1696,21 +1700,22 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, SASSERT(m_bv_util.get_bv_size(S) == sbits + 5); SASSERT(m_bv_util.get_bv_size(T) == sbits + 6); - expr_ref t_lt_0(m); - m_simp.mk_eq(m_bv_util.mk_extract(sbits+5, sbits+5, T), one1, t_lt_0); + expr_ref t_lt_0(m), T_lsds5(m); + T_lsds5 = m_bv_util.mk_extract(sbits + 5, sbits + 5, T); + m_simp.mk_eq(T_lsds5, one1, t_lt_0); expr * or_args[2] = { Q, S }; - - m_simp.mk_ite(t_lt_0, Q, - m_bv_util.mk_bv_or(2, or_args), - Q); - m_simp.mk_ite(t_lt_0, m_bv_util.mk_concat(m_bv_util.mk_extract(sbits+3, 0, R), zero1), - m_bv_util.mk_extract(sbits+4, 0, T), - R); + expr_ref Q_or_S(m), R_shftd(m), T_lsds4(m); + Q_or_S = m_bv_util.mk_bv_or(2, or_args); + m_simp.mk_ite(t_lt_0, Q, Q_or_S, Q); + R_shftd = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits + 3, 0, R), zero1); + T_lsds4 = m_bv_util.mk_extract(sbits + 4, 0, T); + m_simp.mk_ite(t_lt_0, R_shftd, T_lsds4, R); } - expr_ref is_exact(m); - m_simp.mk_eq(R, m_bv_util.mk_numeral(0, sbits+5), is_exact); + expr_ref is_exact(m), zero_sbits5(m); + zero_sbits5 = m_bv_util.mk_numeral(0, sbits + 5); + m_simp.mk_eq(R, zero_sbits5, is_exact); dbg_decouple("fpa2bv_sqrt_is_exact", is_exact); expr_ref rest(m), last(m), q_is_odd(m), rest_ext(m); @@ -1719,10 +1724,10 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_sqrt_last", last); dbg_decouple("fpa2bv_sqrt_rest", rest); rest_ext = m_bv_util.mk_zero_extend(1, rest); - expr_ref sticky(m); - m_simp.mk_ite(is_exact, m_bv_util.mk_zero_extend(sbits+3, last), - m_bv_util.mk_numeral(1, sbits+4), - sticky); + expr_ref sticky(m), last_ext(m), one_sbits4(m); + last_ext = m_bv_util.mk_zero_extend(sbits + 3, last); + one_sbits4 = m_bv_util.mk_numeral(1, sbits + 4); + m_simp.mk_ite(is_exact, last_ext, one_sbits4, sticky); expr * or_args[2] = { rest_ext, sticky }; res_sig = m_bv_util.mk_bv_or(2, or_args); @@ -1813,8 +1818,11 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * mk_one(f, one_1, none); mk_ite(m.mk_eq(a_sgn, one_1), none, pone, xone); - m_simp.mk_eq(a_sig, m_bv_util.mk_numeral(fu().fm().m_powers2(sbits-1), sbits), t1); - m_simp.mk_eq(a_exp, m_bv_util.mk_numeral(-1, ebits), t2); + expr_ref pow_2_sbitsm1(m), m1(m); + pow_2_sbitsm1 = m_bv_util.mk_numeral(fu().fm().m_powers2(sbits - 1), sbits); + m1 = m_bv_util.mk_numeral(-1, ebits); + m_simp.mk_eq(a_sig, pow_2_sbitsm1, t1); + m_simp.mk_eq(a_exp, m1, t2); m_simp.mk_and(t1, t2, tie); dbg_decouple("fpa2bv_r2i_c42_tie", tie); @@ -1896,14 +1904,17 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * SASSERT(is_well_sorted(m, tie2_c)); SASSERT(is_well_sorted(m, v51)); - expr_ref c521(m), v52(m); - m_simp.mk_not(m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits+1)), c521); - m_simp.mk_and(c521, m.mk_eq(res_sgn, zero_1), c521); + expr_ref c521(m), v52(m), rem_eq_0(m), sgn_eq_zero(m); + rem_eq_0 = m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits + 1)); + sgn_eq_zero = m.mk_eq(res_sgn, zero_1); + m_simp.mk_not(rem_eq_0, c521); + m_simp.mk_and(c521, sgn_eq_zero, c521); m_simp.mk_ite(c521, div_p1, div, v52); - expr_ref c531(m), v53(m); - m_simp.mk_not(m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits+1)), c531); - m_simp.mk_and(c531, m.mk_eq(res_sgn, one_1), c531); + expr_ref c531(m), v53(m), sgn_eq_one(m); + sgn_eq_one = m.mk_eq(res_sgn, one_1); + m_simp.mk_not(rem_eq_0, c531); + m_simp.mk_and(c531, sgn_eq_one, c531); m_simp.mk_ite(c531, div_p1, div, v53); expr_ref c51(m), c52(m), c53(m); @@ -3377,9 +3388,10 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref zero_s = m_bv_util.mk_numeral(0, sbits); m_simp.mk_eq(zero_s, denormal_sig, is_sig_zero); - expr_ref lz_d(m); + expr_ref lz_d(m), norm_or_zero(m); mk_leading_zeros(denormal_sig, ebits, lz_d); - m_simp.mk_ite(m.mk_or(is_normal, is_sig_zero), zero_e, lz_d, lz); + norm_or_zero = m.mk_or(is_normal, is_sig_zero); + m_simp.mk_ite(norm_or_zero, zero_e, lz_d, lz); dbg_decouple("fpa2bv_unpack_lz", lz); expr_ref shift(m); @@ -3770,8 +3782,9 @@ void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_re dbg_decouple("fpa2bv_rnd_rm_is_to_pos", rm_is_to_pos); - expr_ref sgn_is_zero(m); - m_simp.mk_eq(sgn, m_bv_util.mk_numeral(0, 1), sgn_is_zero); + expr_ref sgn_is_zero(m), zero1(m); + zero1 = m_bv_util.mk_numeral(0, 1); + m_simp.mk_eq(sgn, zero1, sgn_is_zero); dbg_decouple("fpa2bv_rnd_sgn_is_zero", sgn_is_zero); expr_ref max_sig(m), max_exp(m), inf_sig(m), inf_exp(m); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 65d99d2c8..8dc3dc019 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -26,19 +26,6 @@ Notes: #include"bv_decl_plugin.h" #include"basic_simplifier_plugin.h" -struct func_decl_triple { - func_decl_triple () { f_sgn = 0; f_sig = 0; f_exp = 0; } - func_decl_triple (func_decl * sgn, func_decl * sig, func_decl * exp) - { - f_sgn = sgn; - f_sig = sig; - f_exp = exp; - } - func_decl * f_sgn; - func_decl * f_sig; - func_decl * f_exp; - }; - class fpa2bv_converter { protected: ast_manager & m; diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index aa9277e39..28597c6ec 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -91,7 +91,6 @@ class fpa2bv_tactic : public tactic { // that is (= e (fp #b0 #b1...1 #b0...01)), so that the value propagation // has a value to propagate. expr * sgn, *sig, *exp; - expr_ref top_exp(m); m_conv.split_fp(new_curr, sgn, exp, sig); result.back()->assert_expr(m.mk_eq(sgn, m_conv.bu().mk_numeral(0, 1))); result.back()->assert_expr(m.mk_eq(exp, m_conv.bu().mk_numeral(-1, m_conv.bu().get_bv_size(exp))));