Implement proposed smtlib2 bitvector overflow predicates (#6715)

* Logical names for function declarations in c++

Currently, for example, the function declaration symbol member for
checking whether multiplication *does not* overflow is called
`m_bv_smul_ovfl`.  Since we are introducing the upcoming smtlib2 symbols
that check that multpliciation *does* overflow, the not overflow check
symbols are renamed to `m_bv_smul_no_ovfl` etc.

* Implement smtlib overflow preds for multiplication

Smtlib2 is being extended to include overflow predicates for bit
vectors (see https://groups.google.com/u/1/g/smt-lib/c/J4D99wT0aKI).
This commit introduces the predicates `bvumulo` and `bvsmulo` that
return `true` if the unsigned multiplication overflows or the signed
multiplication underflows or overflows, respectively.

* Move mul overflow predicates to BV logic

* Add a todo on illogical argument order

* Implement mk_unary_pred for bv

* Implement bvnego

* Implement bvuaddo

* Implement bvsaddo

* Implement bvusubo

* Implement bvssubo

* Implement bvsdivo

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<func_decl> & 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<func_decl> & 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<builtin_name> & 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));

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 @@ class bv_decl_plugin : public decl_plugin {
     ptr_vector<func_decl>  m_bv_redand;
     ptr_vector<func_decl>  m_bv_comp;
 
-    ptr_vector<func_decl>  m_bv_mul_ovfl;
-    ptr_vector<func_decl>  m_bv_smul_ovfl;
-    ptr_vector<func_decl>  m_bv_smul_udfl;
+    ptr_vector<func_decl>  m_bv_mul_no_ovfl;
+    ptr_vector<func_decl>  m_bv_smul_no_ovfl;
+    ptr_vector<func_decl>  m_bv_smul_no_udfl;
+
+    ptr_vector<func_decl> m_bv_mul_ovfl;
+    ptr_vector<func_decl> m_bv_smul_ovfl;
+
+    ptr_vector<func_decl> m_bv_sdiv_ovfl;
+
+    ptr_vector<func_decl> m_bv_neg_ovfl;
+
+    ptr_vector<func_decl> m_bv_uadd_ovfl;
+    ptr_vector<func_decl> m_bv_sadd_ovfl;
+
+    ptr_vector<func_decl> m_bv_usub_ovfl;
+    ptr_vector<func_decl> m_bv_ssub_ovfl;
 
     ptr_vector<func_decl>  m_bv_shl;
     ptr_vector<func_decl>  m_bv_lshr;
@@ -213,6 +239,7 @@ class bv_decl_plugin : public decl_plugin {
     func_decl * mk_unary(ptr_vector<func_decl> & decls, decl_kind k, char const * name, unsigned bv_size);
     func_decl * mk_pred(ptr_vector<func_decl> & decls, decl_kind k,
                         char const * name, unsigned bv_size);
+    func_decl * mk_unary_pred(ptr_vector<func_decl> & decls, decl_kind k, char const * name, unsigned bv_size);
     func_decl * mk_reduction(ptr_vector<func_decl> & 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 @@ class bv_util : public bv_recognizers {
 
     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:

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<bv_rewriter_core>;

src/ast/rewriter/bv_rewriter.h

@@ -139,6 +139,22 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     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);