diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 351d037cb..4d38327a5 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -118,9 +118,22 @@ void bv_decl_plugin::finalize() { DEC_REF(m_bv_redand); DEC_REF(m_bv_comp); + DEC_REF(m_bv_mul_no_ovfl); + DEC_REF(m_bv_smul_no_ovfl); + DEC_REF(m_bv_smul_no_udfl); + DEC_REF(m_bv_mul_ovfl); DEC_REF(m_bv_smul_ovfl); - DEC_REF(m_bv_smul_udfl); + + DEC_REF(m_bv_neg_ovfl); + + DEC_REF(m_bv_uadd_ovfl); + DEC_REF(m_bv_sadd_ovfl); + + DEC_REF(m_bv_usub_ovfl); + DEC_REF(m_bv_ssub_ovfl); + + DEC_REF(m_bv_sdiv_ovfl); DEC_REF(m_bv_shl); DEC_REF(m_bv_lshr); @@ -245,6 +258,16 @@ func_decl * bv_decl_plugin::mk_bv2int(unsigned bv_size, unsigned num_parameters, return m_bv2int[bv_size]; } +func_decl * bv_decl_plugin::mk_unary_pred(ptr_vector & decls, decl_kind k, char const * name, unsigned bv_size) { + force_ptr_array_size(decls, bv_size+1); + + if (decls[bv_size] == 0) { + decls[bv_size] = m_manager->mk_func_decl(symbol(name), get_bv_sort(bv_size), m_manager->mk_bool_sort(), func_decl_info(m_family_id, k)); + m_manager->inc_ref(decls[bv_size]); + } + return decls[bv_size]; +} + func_decl * bv_decl_plugin::mk_pred(ptr_vector & decls, decl_kind k, char const * name, unsigned bv_size) { force_ptr_array_size(decls, bv_size + 1); @@ -289,6 +312,7 @@ func_decl * bv_decl_plugin::mk_comp(unsigned bv_size) { func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned bv_size) { switch (k) { case OP_BNEG: return mk_unary(m_bv_neg, k, "bvneg", bv_size); + case OP_BNEG_OVFL: return mk_unary_pred(m_bv_neg_ovfl, k, "bvnego", bv_size); case OP_BADD: return mk_binary(m_bv_add, k, "bvadd", bv_size, true); case OP_BSUB: return mk_binary(m_bv_sub, k, "bvsub", bv_size, false); case OP_BMUL: return mk_binary(m_bv_mul, k, "bvmul", bv_size, true); @@ -327,9 +351,16 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned bv_size) { case OP_BREDOR: return mk_reduction(m_bv_redor, k, "bvredor", bv_size); case OP_BREDAND: return mk_reduction(m_bv_redand, k, "bvredand", bv_size); case OP_BCOMP: return mk_comp(bv_size); - case OP_BUMUL_NO_OVFL: return mk_pred(m_bv_mul_ovfl, k, "bvumul_noovfl", bv_size); - case OP_BSMUL_NO_OVFL: return mk_pred(m_bv_smul_ovfl, k, "bvsmul_noovfl", bv_size); - case OP_BSMUL_NO_UDFL: return mk_pred(m_bv_smul_udfl, k, "bvsmul_noudfl", bv_size); + case OP_BUMUL_NO_OVFL: return mk_pred(m_bv_mul_no_ovfl, k, "bvumul_noovfl", bv_size); + case OP_BSMUL_NO_OVFL: return mk_pred(m_bv_smul_no_ovfl, k, "bvsmul_noovfl", bv_size); + case OP_BSMUL_NO_UDFL: return mk_pred(m_bv_smul_no_udfl, k, "bvsmul_noudfl", bv_size); + case OP_BUMUL_OVFL: return mk_pred(m_bv_mul_ovfl, k, "bvumulo", bv_size); + case OP_BSMUL_OVFL: return mk_pred(m_bv_smul_ovfl, k, "bvsmulo", bv_size); + case OP_BSDIV_OVFL: return mk_pred(m_bv_sdiv_ovfl, k, "bvsdivo", bv_size); + case OP_BUADD_OVFL: return mk_pred(m_bv_uadd_ovfl, k, "bvuaddo", bv_size); + case OP_BSADD_OVFL: return mk_pred(m_bv_sadd_ovfl, k, "bvsaddo", bv_size); + case OP_BUSUB_OVFL: return mk_pred(m_bv_usub_ovfl, k, "bvusubo", bv_size); + case OP_BSSUB_OVFL: return mk_pred(m_bv_ssub_ovfl, k, "bvssubo", bv_size); case OP_BSHL: return mk_binary(m_bv_shl, k, "bvshl", bv_size, false); case OP_BLSHR: return mk_binary(m_bv_lshr, k, "bvlshr", bv_size, false); @@ -681,10 +712,18 @@ void bv_decl_plugin::get_op_names(svector & op_names, symbol const op_names.push_back(builtin_name("bit1",OP_BIT1)); op_names.push_back(builtin_name("bit0",OP_BIT0)); op_names.push_back(builtin_name("bvneg",OP_BNEG)); + op_names.push_back(builtin_name("bvnego", OP_BNEG_OVFL)); op_names.push_back(builtin_name("bvadd",OP_BADD)); + op_names.push_back(builtin_name("bvuaddo",OP_BUADD_OVFL)); + op_names.push_back(builtin_name("bvsaddo",OP_BSADD_OVFL)); op_names.push_back(builtin_name("bvsub",OP_BSUB)); + op_names.push_back(builtin_name("bvusubo",OP_BUSUB_OVFL)); + op_names.push_back(builtin_name("bvssubo",OP_BSSUB_OVFL)); op_names.push_back(builtin_name("bvmul",OP_BMUL)); + op_names.push_back(builtin_name("bvumulo",OP_BUMUL_OVFL)); + op_names.push_back(builtin_name("bvsmulo",OP_BSMUL_OVFL)); op_names.push_back(builtin_name("bvsdiv",OP_BSDIV)); + op_names.push_back(builtin_name("bvsdivo",OP_BSDIV_OVFL)); op_names.push_back(builtin_name("bvudiv",OP_BUDIV)); op_names.push_back(builtin_name("bvsrem",OP_BSREM)); op_names.push_back(builtin_name("bvurem",OP_BUREM)); diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index fc7e35245..51faca7ed 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -93,6 +93,19 @@ enum bv_op_kind { OP_BSMUL_NO_OVFL, // no signed multiplication overflow predicate OP_BSMUL_NO_UDFL, // no signed multiplication underflow predicate + OP_BUMUL_OVFL, // unsigned multiplication overflow predicate (negation of OP_BUMUL_NO_OVFL) + OP_BSMUL_OVFL, // signed multiplication over/underflow predicate + + OP_BSDIV_OVFL, // signed division overflow perdicate + + OP_BNEG_OVFL, // negation overflow predicate + + OP_BUADD_OVFL, // unsigned addition overflow predicate + OP_BSADD_OVFL, // signed addition overflow predicate + + OP_BUSUB_OVFL, // unsigned subtraction overflow predicate + OP_BSSUB_OVFL, // signed subtraction overflow predicate + OP_BIT2BOOL, // predicate OP_MKBV, // bools to bv OP_INT2BV, @@ -189,9 +202,22 @@ protected: ptr_vector m_bv_redand; ptr_vector m_bv_comp; - ptr_vector m_bv_mul_ovfl; - ptr_vector m_bv_smul_ovfl; - ptr_vector m_bv_smul_udfl; + ptr_vector m_bv_mul_no_ovfl; + ptr_vector m_bv_smul_no_ovfl; + ptr_vector m_bv_smul_no_udfl; + + ptr_vector m_bv_mul_ovfl; + ptr_vector m_bv_smul_ovfl; + + ptr_vector m_bv_sdiv_ovfl; + + ptr_vector m_bv_neg_ovfl; + + ptr_vector m_bv_uadd_ovfl; + ptr_vector m_bv_sadd_ovfl; + + ptr_vector m_bv_usub_ovfl; + ptr_vector m_bv_ssub_ovfl; ptr_vector m_bv_shl; ptr_vector m_bv_lshr; @@ -213,6 +239,7 @@ protected: func_decl * mk_unary(ptr_vector & decls, decl_kind k, char const * name, unsigned bv_size); func_decl * mk_pred(ptr_vector & decls, decl_kind k, char const * name, unsigned bv_size); + func_decl * mk_unary_pred(ptr_vector & decls, decl_kind k, char const * name, unsigned bv_size); func_decl * mk_reduction(ptr_vector & decls, decl_kind k, char const * name, unsigned bv_size); func_decl * mk_comp(unsigned bv_size); bool get_bv_size(sort * t, int & result); @@ -490,9 +517,19 @@ public: app * mk_bv2int(expr* e); + // TODO: all these binary ops commute (right?) but it'd be more logical to swap `n` & `m` in the `return` app * mk_bvsmul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_OVFL, n, m); } app * mk_bvsmul_no_udfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_UDFL, n, m); } app * mk_bvumul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_NO_OVFL, n, m); } + app * mk_bvsmul_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_OVFL, n, m); } + app * mk_bvumul_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_OVFL, n, m); } + app * mk_bvsdiv_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSDIV_OVFL, m, n); } + app * mk_bvneg_ovfl(expr* m) { return m_manager.mk_app(get_fid(), OP_BNEG_OVFL, m); } + app * mk_bvuadd_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUADD_OVFL, n, m); } + app * mk_bvsadd_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSADD_OVFL, n, m); } + app * mk_bvusub_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUSUB_OVFL, m, n); } + app * mk_bvssub_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSSUB_OVFL, m, n); } + app * mk_bit2bool(expr* e, unsigned idx) { parameter p(idx); return m_manager.mk_app(get_fid(), OP_BIT2BOOL, 1, &p, 1, &e); } private: diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 5f76d3fdd..751608e12 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -93,6 +93,10 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons case OP_BNEG: SASSERT(num_args == 1); return mk_uminus(args[0], result); + case OP_BNEG_OVFL: + SASSERT(num_args == 1); + return mk_bvneg_overflow(args[0], result); + case OP_BSHL: SASSERT(num_args == 2); return mk_bv_shl(args[0], args[1], result); @@ -199,6 +203,20 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons return mk_bvsmul_no_overflow(num_args, args, false, result); case OP_BUMUL_NO_OVFL: return mk_bvumul_no_overflow(num_args, args, result); + case OP_BSMUL_OVFL: + return mk_bvsmul_overflow(num_args, args, result); + case OP_BUMUL_OVFL: + return mk_bvumul_overflow(num_args, args, result); + case OP_BSDIV_OVFL: + return mk_bvsdiv_overflow(num_args, args, result); + case OP_BUADD_OVFL: + return mk_bvuadd_overflow(num_args, args, result); + case OP_BSADD_OVFL: + return mk_bvsadd_over_underflow(num_args, args, result); + case OP_BUSUB_OVFL: + return mk_bvusub_underflow(num_args, args, result); + case OP_BSSUB_OVFL: + return mk_bvssub_overflow(num_args, args, result); default: return BR_FAILED; } @@ -2921,6 +2939,21 @@ br_status bv_rewriter::mk_distinct(unsigned num_args, expr * const * args, expr_ return BR_DONE; } +br_status bv_rewriter::mk_bvsmul_overflow(unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + result = m.mk_or( + m.mk_not(m_util.mk_bvsmul_no_ovfl(args[0], args[1])), + m.mk_not(m_util.mk_bvsmul_no_udfl(args[0], args[1])) + ); + return BR_REWRITE_FULL; +} + +br_status bv_rewriter::mk_bvumul_overflow(unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + result = m.mk_not(m_util.mk_bvumul_no_ovfl(args[0], args[1])); + return BR_REWRITE2; +} + br_status bv_rewriter::mk_bvsmul_no_overflow(unsigned num, expr * const * args, bool is_overflow, expr_ref & result) { SASSERT(num == 2); unsigned bv_sz; @@ -2980,5 +3013,95 @@ br_status bv_rewriter::mk_bvumul_no_overflow(unsigned num, expr * const * args, return BR_FAILED; } +br_status bv_rewriter::mk_bvneg_overflow(expr * const arg, expr_ref & result) { + unsigned int sz = get_bv_size(arg); + auto maxUnsigned = mk_numeral(rational::power_of_two(sz)-1, sz); + result = m.mk_eq(arg, maxUnsigned); + return BR_REWRITE3; +} + +br_status bv_rewriter::mk_bvuadd_overflow(unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + SASSERT(get_bv_size(args[0]) == get_bv_size(args[1])); + unsigned sz = get_bv_size(args[0]); + auto a1 = mk_zero_extend(1, args[0]); + auto a2 = mk_zero_extend(1, args[1]); + auto r = mk_bv_add(a1, a2); + auto extract = m_mk_extract(sz, sz, r); + result = m.mk_eq(extract, mk_one(1)); + return BR_REWRITE_FULL; +} + +br_status bv_rewriter::mk_bvsadd_overflow(unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + SASSERT(get_bv_size(args[0]) == get_bv_size(args[1])); + unsigned sz = get_bv_size(args[0]); + auto zero = mk_zero(sz); + auto r = mk_bv_add(args[0], args[1]); + auto l1 = m_util.mk_slt(zero, args[0]); + auto l2 = m_util.mk_slt(zero, args[1]); + auto args_pos = m.mk_and(l1, l2); + auto non_pos_sum = m_util.mk_sle(r, zero); + result = m.mk_and(args_pos, non_pos_sum); + return BR_REWRITE_FULL; +} + +br_status bv_rewriter::mk_bvsadd_underflow(unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + SASSERT(get_bv_size(args[0]) == get_bv_size(args[1])); + unsigned sz = get_bv_size(args[0]); + auto zero = mk_zero(sz); + auto r = mk_bv_add(args[0], args[1]); + auto l1 = m_util.mk_slt(args[0], zero); + auto l2 = m_util.mk_slt(args[1], zero); + auto args_neg = m.mk_and(l1, l2); + expr_ref non_neg_sum{m}; + auto res_rewrite = mk_sge(r, zero, non_neg_sum); + SASSERT(res_rewrite != BR_FAILED); (void)res_rewrite; + result = m.mk_and(args_neg, non_neg_sum); + return BR_REWRITE_FULL; +} + +br_status bv_rewriter::mk_bvsadd_over_underflow(unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + SASSERT(get_bv_size(args[0]) == get_bv_size(args[1])); + expr_ref l1{m}; + expr_ref l2{m}; + (void)mk_bvsadd_overflow(2, args, l1); + (void)mk_bvsadd_underflow(2, args, l2); + result = m.mk_or(l1, l2); + return BR_REWRITE_FULL; +} + +br_status bv_rewriter::mk_bvusub_underflow(unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + SASSERT(get_bv_size(args[0]) == get_bv_size(args[1])); + br_status status = mk_ult(args[0], args[1], result); + SASSERT(status != BR_FAILED); + return status; +} + +br_status bv_rewriter::mk_bvssub_overflow(unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + SASSERT(get_bv_size(args[0]) == get_bv_size(args[1])); + auto sz = get_bv_size(args[0]); + auto minSigned = mk_numeral(-rational::power_of_two(sz-1), sz); + expr_ref bvsaddo {m}; + expr * args2[2] = { args[0], m_util.mk_bv_neg(args[1]) }; + auto bvsaddo_stat = mk_bvsadd_overflow(2, args2, bvsaddo); + SASSERT(bvsaddo_stat != BR_FAILED); (void)bvsaddo_stat; + auto first_arg_ge_zero = m_util.mk_sle(mk_zero(sz), args[0]); + result = m.mk_ite(m.mk_eq(args[1], minSigned), first_arg_ge_zero, bvsaddo); + return BR_REWRITE_FULL; +} +br_status bv_rewriter::mk_bvsdiv_overflow(unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + SASSERT(get_bv_size(args[0]) == get_bv_size(args[1])); + auto sz = get_bv_size(args[1]); + auto minSigned = mk_numeral(-rational::power_of_two(sz-1), sz); + auto minusOne = mk_numeral(rational::power_of_two(sz) - 1, sz); + result = m.mk_and(m.mk_eq(args[0], minSigned), m.mk_eq(args[1], minusOne)); + return BR_REWRITE_FULL; +} template class poly_rewriter; diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index 25bd65b61..09e7996c2 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -139,6 +139,22 @@ class bv_rewriter : public poly_rewriter { br_status mk_mkbv(unsigned num, expr * const * args, expr_ref & result); br_status mk_bvsmul_no_overflow(unsigned num, expr * const * args, bool is_overflow, expr_ref & result); br_status mk_bvumul_no_overflow(unsigned num, expr * const * args, expr_ref & result); + + br_status mk_bvsmul_overflow(unsigned num, expr * const * args, expr_ref & result); + br_status mk_bvumul_overflow(unsigned num, expr * const * args, expr_ref & result); + + br_status mk_bvsdiv_overflow(unsigned num, expr * const * args, expr_ref & result); + + br_status mk_bvneg_overflow(expr * const arg, expr_ref & result); + + br_status mk_bvuadd_overflow(unsigned num, expr * const * args, expr_ref & result); + br_status mk_bvsadd_overflow(unsigned num, expr * const * args, expr_ref & result); + br_status mk_bvsadd_underflow(unsigned num, expr * const * args, expr_ref & result); + br_status mk_bvsadd_over_underflow(unsigned num, expr * const * args, expr_ref & result); + + br_status mk_bvusub_underflow(unsigned num, expr * const * args, expr_ref & result); + br_status mk_bvssub_overflow(unsigned num, expr * const * args, expr_ref & result); + bool is_minus_one_times_t(expr * arg); void mk_t1_add_t2_eq_c(expr * t1, expr * t2, expr * c, expr_ref & result);