1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 bv_rewriter.h 7 8 Abstract: 9 10 Basic rewriting rules for bit-vectors 11 12 Author: 13 14 Leonardo (leonardo) 2011-04-14 15 16 Notes: 17 18 --*/ 19 #pragma once 20 21 #include "ast/rewriter/poly_rewriter.h" 22 #include "ast/bv_decl_plugin.h" 23 #include "ast/arith_decl_plugin.h" 24 #include "ast/rewriter/mk_extract_proc.h" 25 26 class bv_rewriter_core { 27 protected: 28 typedef rational numeral; 29 bv_util m_util; m()30 ast_manager & m() const { return m_util.get_manager(); } get_fid()31 family_id get_fid() const { return m_util.get_family_id(); } 32 is_numeral(expr * n)33 bool is_numeral(expr * n) const { return m_util.is_numeral(n); } is_numeral(expr * n,numeral & r)34 bool is_numeral(expr * n, numeral & r) const { unsigned sz; return m_util.is_numeral(n, r, sz); } is_zero(expr * n)35 bool is_zero(expr * n) const { return m_util.is_zero(n); } is_minus_one(expr * n)36 bool is_minus_one(expr * n) const { return m_util.is_allone(n); } normalize(numeral & c,sort * s)37 void normalize(numeral & c, sort * s) { unsigned bv_size = m_util.get_bv_size(s); c = m_util.norm(c, bv_size); } mk_numeral(numeral const & r,sort * s)38 app * mk_numeral(numeral const & r, sort * s) { return m_util.mk_numeral(r, s); } add_decl_kind()39 decl_kind add_decl_kind() const { return OP_BADD; } mul_decl_kind()40 decl_kind mul_decl_kind() const { return OP_BMUL; } use_power()41 bool use_power() const { return false; } mk_power(expr * x,rational const & r,sort * s)42 app* mk_power(expr* x, rational const& r, sort* s) { UNREACHABLE(); return nullptr; } coerce(expr * x,sort * s)43 expr* coerce(expr* x, sort* s) { UNREACHABLE(); return nullptr; } power_decl_kind()44 decl_kind power_decl_kind() const { UNREACHABLE(); return static_cast<decl_kind>(UINT_MAX); } 45 46 public: bv_rewriter_core(ast_manager & m)47 bv_rewriter_core(ast_manager & m):m_util(m) {} 48 }; 49 50 class bv_rewriter : public poly_rewriter<bv_rewriter_core> { 51 mk_extract_proc m_mk_extract; 52 arith_util m_autil; 53 bool m_hi_div0; 54 bool m_elim_sign_ext; 55 bool m_mul2concat; 56 bool m_bit2bool; 57 bool m_blast_eq_value; 58 bool m_mkbv2num; 59 bool m_ite2id; 60 bool m_split_concat_eq; 61 bool m_bv_sort_ac; 62 bool m_extract_prop; 63 bool m_bvnot_simpl; 64 bool m_le_extra; 65 66 bool is_zero_bit(expr * x, unsigned idx); 67 68 br_status mk_ule(expr * a, expr * b, expr_ref & result); 69 br_status mk_uge(expr * a, expr * b, expr_ref & result); 70 br_status mk_ult(expr * a, expr * b, expr_ref & result); 71 br_status mk_sle(expr * a, expr * b, expr_ref & result); 72 br_status mk_sge(expr * a, expr * b, expr_ref & result); 73 br_status mk_slt(expr * a, expr * b, expr_ref & result); 74 br_status rw_leq_concats(bool is_signed, expr * a, expr * b, expr_ref & result); 75 bool are_eq_upto_num(expr * a, expr * b, expr_ref& common, numeral& a0_val, numeral& b0_val); 76 br_status rw_leq_overflow(bool is_signed, expr * _a, expr * _b, expr_ref & result); 77 br_status mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref & result); 78 79 br_status mk_concat(unsigned num_args, expr * const * args, expr_ref & result); 80 unsigned propagate_extract(unsigned high, expr * arg, expr_ref & result); 81 br_status mk_extract(unsigned high, unsigned low, expr * arg, expr_ref & result); 82 br_status mk_repeat(unsigned n, expr * arg, expr_ref & result); 83 br_status mk_zero_extend(unsigned n, expr * arg, expr_ref & result); 84 br_status mk_sign_extend(unsigned n, expr * arg, expr_ref & result); 85 bool is_negatable(expr * arg, expr_ref& x); 86 br_status mk_bv_not(expr * arg, expr_ref & result); 87 br_status mk_bv_or(unsigned num, expr * const * args, expr_ref & result); 88 br_status mk_bv_xor(unsigned num, expr * const * args, expr_ref & result); 89 br_status mk_bv_and(unsigned num, expr * const * args, expr_ref & result); 90 br_status mk_bv_nand(unsigned num, expr * const * args, expr_ref & result); 91 br_status mk_bv_nor(unsigned num, expr * const * args, expr_ref & result); 92 br_status mk_bv_xnor(unsigned num_args, expr * const * args, expr_ref & result); 93 br_status mk_bv_rotate_left(unsigned n, expr * arg, expr_ref & result); 94 br_status mk_bv_rotate_right(unsigned n, expr * arg, expr_ref & result); 95 br_status mk_bv_ext_rotate_left(expr * arg1, expr * arg2, expr_ref & result); 96 br_status mk_bv_ext_rotate_right(expr * arg1, expr * arg2, expr_ref & result); mk_bv_add(expr * a,expr * b,expr_ref & result)97 br_status mk_bv_add(expr* a, expr* b, expr_ref& result) { expr* args[2] = { a, b }; return mk_bv_add(2, args, result); } mk_bv_sub(expr * a,expr * b,expr_ref & result)98 br_status mk_bv_sub(expr* a, expr* b, expr_ref& result) { expr* args[2] = { a, b }; return mk_sub(2, args, result); } mk_bv_mul(expr * a,expr * b,expr_ref & result)99 br_status mk_bv_mul(expr* a, expr* b, expr_ref& result) { expr* args[2] = { a, b }; return mk_bv_mul(2, args, result); } 100 br_status mk_bv_add(unsigned num_args, expr * const * args, expr_ref & result); 101 br_status mk_bv_mul(unsigned num_args, expr * const * args, expr_ref & result); 102 br_status mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result); 103 br_status mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result); 104 br_status mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result); 105 bool distribute_concat(decl_kind op, unsigned n, expr* const* args, expr_ref& result); 106 bool is_minus_one_core(expr * arg) const; 107 bool is_x_minus_one(expr * arg, expr * & x); 108 bool is_add_no_overflow(expr* e); 109 bool is_mul_no_overflow(expr* e); 110 unsigned num_leading_zero_bits(expr* e); 111 112 br_status mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result); 113 br_status mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result); 114 br_status mk_bv_srem_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result); 115 br_status mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result); 116 br_status mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result); mk_bv_sdiv(expr * arg1,expr * arg2,expr_ref & result)117 br_status mk_bv_sdiv(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_sdiv_core(arg1, arg2, m_hi_div0, result); } mk_bv_udiv(expr * arg1,expr * arg2,expr_ref & result)118 br_status mk_bv_udiv(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_udiv_core(arg1, arg2, m_hi_div0, result); } mk_bv_srem(expr * arg1,expr * arg2,expr_ref & result)119 br_status mk_bv_srem(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_srem_core(arg1, arg2, m_hi_div0, result); } mk_bv_urem(expr * arg1,expr * arg2,expr_ref & result)120 br_status mk_bv_urem(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_urem_core(arg1, arg2, m_hi_div0, result); } mk_bv_smod(expr * arg1,expr * arg2,expr_ref & result)121 br_status mk_bv_smod(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_smod_core(arg1, arg2, m_hi_div0, result); } mk_bv_sdiv_i(expr * arg1,expr * arg2,expr_ref & result)122 br_status mk_bv_sdiv_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_sdiv_core(arg1, arg2, true, result); } mk_bv_udiv_i(expr * arg1,expr * arg2,expr_ref & result)123 br_status mk_bv_udiv_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_udiv_core(arg1, arg2, true, result); } mk_bv_srem_i(expr * arg1,expr * arg2,expr_ref & result)124 br_status mk_bv_srem_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_srem_core(arg1, arg2, true, result); } mk_bv_urem_i(expr * arg1,expr * arg2,expr_ref & result)125 br_status mk_bv_urem_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_urem_core(arg1, arg2, true, result); } mk_bv_smod_i(expr * arg1,expr * arg2,expr_ref & result)126 br_status mk_bv_smod_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_smod_core(arg1, arg2, true, result); } 127 br_status mk_int2bv(unsigned bv_size, expr * arg, expr_ref & result); 128 br_status mk_bv2int(expr * arg, expr_ref & result); 129 br_status mk_bv_redor(expr * arg, expr_ref & result); 130 br_status mk_bv_redand(expr * arg, expr_ref & result); 131 br_status mk_bv_comp(expr * arg1, expr * arg2, expr_ref & result); 132 br_status mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result); 133 br_status mk_bit2bool(expr * lhs, int idx, expr_ref & result); 134 br_status mk_blast_eq_value(expr * lhs, expr * rhs, expr_ref & result); 135 br_status mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result); 136 br_status mk_mkbv(unsigned num, expr * const * args, expr_ref & result); 137 br_status mk_bvsmul_no_overflow(unsigned num, expr * const * args, expr_ref & result); 138 br_status mk_bvumul_no_overflow(unsigned num, expr * const * args, expr_ref & result); 139 br_status mk_bvsmul_no_underflow(unsigned num, expr * const * args, expr_ref & result); 140 bool is_minus_one_times_t(expr * arg); 141 void mk_t1_add_t2_eq_c(expr * t1, expr * t2, expr * c, expr_ref & result); 142 143 bool is_concat_split_target(expr * t) const; 144 145 br_status mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result); 146 bool is_add_mul_const(expr* e) const; 147 bool isolate_term(expr* lhs, expr* rhs, expr_ref & result); 148 bool has_numeral(app* e) const; 149 bool is_concat_target(expr* lhs, expr* rhs) const; 150 151 void updt_local_params(params_ref const & p); 152 153 expr * concat(unsigned num_args, expr * const * args); 154 public: 155 bv_rewriter(ast_manager & m, params_ref const & p = params_ref()): 156 poly_rewriter<bv_rewriter_core>(m, p), 157 m_mk_extract(m_util), 158 m_autil(m) { 159 updt_local_params(p); 160 } 161 162 void updt_params(params_ref const & p); 163 164 static void get_param_descrs(param_descrs & r); 165 set_mkbv2num(bool f)166 void set_mkbv2num(bool f) { m_mkbv2num = f; } 167 get_bv_size(expr * t)168 unsigned get_bv_size(expr * t) const {return m_util.get_bv_size(t); } is_numeral(expr * t)169 bool is_numeral(expr * t) const { return m_util.is_numeral(t); } is_numeral(expr * t,numeral & r,unsigned & sz)170 bool is_numeral(expr * t, numeral & r, unsigned & sz) const { return m_util.is_numeral(t, r, sz); } is_bv(expr * t)171 bool is_bv(expr * t) const { return m_util.is_bv(t); } mk_numeral(numeral const & v,unsigned sz)172 expr * mk_numeral(numeral const & v, unsigned sz) { return m_util.mk_numeral(v, sz); } mk_numeral(unsigned v,unsigned sz)173 expr * mk_numeral(unsigned v, unsigned sz) { return m_util.mk_numeral(numeral(v), sz); } 174 175 br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); mk_app(func_decl * f,unsigned num_args,expr * const * args,expr_ref & result)176 void mk_app(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { 177 if (mk_app_core(f, num_args, args, result) == BR_FAILED) 178 result = m().mk_app(f, num_args, args); 179 } 180 181 bool is_urem_any(expr * e, expr * & dividend, expr * & divisor); 182 br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result); 183 br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & resul); 184 hi_div0()185 bool hi_div0() const { return m_hi_div0; } 186 get_util()187 bv_util & get_util() { return m_util; } 188 189 #define MK_BV_BINARY(OP) \ 190 expr_ref OP(expr* a, expr* b) { \ 191 expr_ref result(m()); \ 192 if (BR_FAILED == OP(a, b, result)) \ 193 result = m_util.OP(a, b); \ 194 return result; \ 195 } \ 196 mk_zero_extend(unsigned n,expr * arg)197 expr_ref mk_zero_extend(unsigned n, expr * arg) { 198 expr_ref result(m()); 199 if (BR_FAILED == mk_zero_extend(n, arg, result)) 200 result = m_util.mk_zero_extend(n, arg); 201 return result; 202 } 203 204 MK_BV_BINARY(mk_bv_urem); 205 MK_BV_BINARY(mk_ule); 206 MK_BV_BINARY(mk_bv_add); 207 MK_BV_BINARY(mk_bv_mul); 208 MK_BV_BINARY(mk_bv_sub); 209 210 mk_bv2int(expr * a)211 expr_ref mk_bv2int(expr* a) { 212 expr_ref result(m()); 213 if (BR_FAILED == mk_bv2int(a, result)) 214 result = m_util.mk_bv2int(a); 215 return result; 216 } 217 218 219 220 }; 221 222