From ddf2d283508c056d3270d6f50112662fb60f6cac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 16 Feb 2024 09:58:24 +0700 Subject: [PATCH] add tests for evaluation --- src/ast/sls/bv_sls_eval.cpp | 333 +++++++++++++++++++++++++--------- src/ast/sls/bv_sls_eval.h | 14 +- src/ast/sls/sls_valuation.cpp | 13 +- src/ast/sls/sls_valuation.h | 7 + src/test/CMakeLists.txt | 1 + src/test/main.cpp | 1 + src/test/sls_test.cpp | 203 +++++++++++++++++++++ 7 files changed, 484 insertions(+), 88 deletions(-) create mode 100644 src/test/sls_test.cpp diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index fa4b60538..bb54e0c55 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -89,12 +89,14 @@ namespace bv { sls_valuation* sls_eval::alloc_valuation(unsigned bit_width) { auto* r = alloc(sls_valuation, bit_width); - while (m_tmp.size() < r->nw) { + while (m_tmp.size() < 2 * r->nw) { m_tmp.push_back(0); - m_tmp2.push_back(0); - m_tmp2.push_back(0); + m_tmp2.push_back(0); + m_tmp3.push_back(0); + m_tmp4.push_back(0); m_zero.push_back(0); m_one.push_back(0); + m_minus_one.push_back(~0); m_one[0] = 1; } return r; @@ -195,9 +197,11 @@ namespace bv { auto& b = wval0(e->get_arg(1)); unsigned c; a.set(m_zero, a.bw - 1, true); - mpn.add(a.bits.data(), a.nw, m_zero.data(), a.nw, m_tmp.data(), a.nw, &c); - mpn.add(b.bits.data(), a.nw, m_zero.data(), a.nw, m_tmp2.data(), a.nw, &c); + mpn.add(a.bits.data(), a.nw, m_zero.data(), a.nw, m_tmp.data(), a.nw + 1, &c); + mpn.add(b.bits.data(), a.nw, m_zero.data(), a.nw, m_tmp2.data(), a.nw + 1, &c); a.set(m_zero, a.bw - 1, false); + a.clear_overflow_bits(m_tmp); + a.clear_overflow_bits(m_tmp2); return f(mpn.compare(m_tmp.data(), a.nw, m_tmp2.data(), b.nw)); }; @@ -209,8 +213,7 @@ namespace bv { for (unsigned i = a.nw; i < 2 * a.nw; ++i) if (m_tmp2[i] != 0) return true; - return !a.has_overflow(m_tmp); - return true; + return a.has_overflow(m_tmp2); }; switch (e->get_decl_kind()) { @@ -246,7 +249,7 @@ namespace bv { auto const& a = wval0(e->get_arg(0)); auto const& b = wval0(e->get_arg(1)); digit_t c = 0; - mpn.add(a.bits.data(), a.nw, b.bits.data(), b.nw, m_tmp.data(), a.nw, &c); + mpn.add(a.bits.data(), a.nw, b.bits.data(), b.nw, m_tmp.data(), a.nw + 1, &c); return c != 0 || a.has_overflow(m_tmp); } case OP_BNEG_OVFL: @@ -295,6 +298,63 @@ namespace bv { val.set(wval0(e).bits); return; } + auto set_sdiv = [&]() { + // d = udiv(abs(x), abs(y)) + // y = 0, x > 0 -> -1 + // y = 0, x <= 0 -> -1 + // x = 0, y != 0 -> 0 + // x > 0, y < 0 -> -d + // x < 0, y > 0 -> -d + // x > 0, y > 0 -> d + // x < 0, y < 0 -> d + auto& a = wval0(e->get_arg(0)); + auto& b = wval0(e->get_arg(1)); + if (a.is_zero() && b.is_zero()) + val.set(m_minus_one); + else if (a.is_zero()) + val.set(m_zero); + else if (b.is_zero()) + val.set(m_minus_one); + else if (!a.sign() && b.is_zero()) + val.set(m_one); + else { + bool sign_a = a.sign(); + bool sign_b = b.sign(); + digit_t c; + + if (sign_a) + mpn.sub(m_zero.data(), a.nw, a.bits.data(), a.nw, m_tmp.data(), &c); + else + a.get(m_tmp); + val.clear_overflow_bits(m_tmp); + + if (sign_b) + mpn.sub(m_zero.data(), a.nw, b.bits.data(), a.nw, m_tmp2.data(), &c); + else + b.get(m_tmp2); + val.clear_overflow_bits(m_tmp2); + + mpn.div(m_tmp.data(), a.nw, m_tmp2.data(), a.nw, m_tmp3.data(), m_tmp4.data()); + if (sign_a == sign_b) + val.set(m_tmp3); + else + mpn.sub(m_zero.data(), a.nw, m_tmp3.data(), a.nw, m_tmp.data(), &c), + val.set(m_tmp); + } + }; + + auto mk_rotate_left = [&](unsigned n) { + auto& a = wval0(e->get_arg(0)); + if (n == 0 || a.bw == 1) + val.set(a.bits); + else { + for (unsigned i = a.bw - n; i < a.bw; ++i) + val.set(val.bits, i + n - a.bw, a.get(a.bits, i)); + for (unsigned i = 0; i < a.bw - n; ++i) + val.set(val.bits, i + a.bw - n, a.get(a.bits, i)); + } + }; + SASSERT(e->get_family_id() == bv.get_fid()); switch (e->get_decl_kind()) { case OP_BV_NUM: { @@ -307,7 +367,7 @@ namespace bv { SASSERT(e->get_num_args() == 2); auto const& a = wval0(e->get_arg(0)); auto const& b = wval0(e->get_arg(1)); - for (unsigned i = 0; i < a.bw; ++i) + for (unsigned i = 0; i < a.nw; ++i) val.bits[i] = a.bits[i] & b.bits[i]; break; } @@ -315,7 +375,7 @@ namespace bv { SASSERT(e->get_num_args() == 2); auto const& a = wval0(e->get_arg(0)); auto const& b = wval0(e->get_arg(1)); - for (unsigned i = 0; i < a.bw; ++i) + for (unsigned i = 0; i < a.nw; ++i) val.bits[i] = a.bits[i] | b.bits[i]; break; } @@ -323,7 +383,7 @@ namespace bv { SASSERT(e->get_num_args() == 2); auto const& a = wval0(e->get_arg(0)); auto const& b = wval0(e->get_arg(1)); - for (unsigned i = 0; i < a.bw; ++i) + for (unsigned i = 0; i < a.nw; ++i) val.bits[i] = a.bits[i] ^ b.bits[i]; break; } @@ -331,7 +391,7 @@ namespace bv { SASSERT(e->get_num_args() == 2); auto const& a = wval0(e->get_arg(0)); auto const& b = wval0(e->get_arg(1)); - for (unsigned i = 0; i < a.bw; ++i) + for (unsigned i = 0; i < a.nw; ++i) val.bits[i] = ~(a.bits[i] & b.bits[i]); break; } @@ -340,7 +400,15 @@ namespace bv { auto const& a = wval0(e->get_arg(0)); auto const& b = wval0(e->get_arg(1)); digit_t c; - mpn.add(a.bits.data(), a.nw, b.bits.data(), b.nw, val.bits.data(), val.nw, &c); + mpn.add(a.bits.data(), a.nw, b.bits.data(), b.nw, val.bits.data(), val.nw + 1, &c); + break; + } + case OP_BSUB: { + SASSERT(e->get_num_args() == 2); + auto const& a = wval0(e->get_arg(0)); + auto const& b = wval0(e->get_arg(1)); + digit_t c; + mpn.sub(a.bits.data(), a.nw, b.bits.data(), b.nw, val.bits.data(), &c); break; } case OP_BMUL: { @@ -393,17 +461,13 @@ namespace bv { auto& a = wval0(e->get_arg(0)); auto& b = wval0(e->get_arg(1)); auto sh = b.to_nat(b.bits, b.bw); - if (sh == 0) { - for (unsigned i = 0; i < a.nw; ++i) - val.bits[i] = a.bits[i]; - } - else if (sh >= b.bw) { - for (unsigned i = 0; i < a.nw; ++i) - val.bits[i] = 0; - } + if (sh == 0) + val.set(a.bits); + else if (sh >= b.bw) + val.set_zero(); else { for (unsigned i = 0; i < a.bw; ++i) - val.set(val.bits, i, i >= sh && b.get(b.bits, i - sh)); + val.set(val.bits, i, i >= sh && a.get(a.bits, i - sh)); } break; } @@ -411,17 +475,13 @@ namespace bv { auto& a = wval0(e->get_arg(0)); auto& b = wval0(e->get_arg(1)); auto sh = b.to_nat(b.bits, b.bw); - if (sh == 0) { - for (unsigned i = 0; i < a.nw; ++i) - val.bits[i] = a.bits[i]; - } - else if (sh >= b.bw) { - for (unsigned i = 0; i < a.nw; ++i) - val.bits[i] = 0; - } + if (sh == 0) + val.set(a.bits); + else if (sh >= b.bw) + val.set_zero(); else { for (unsigned i = 0; i < a.bw; ++i) - val.set(val.bits, i, i + sh < a.bw && b.get(b.bits, i + sh)); + val.set(val.bits, i, i + sh < a.bw && a.get(a.bits, i + sh)); } break; } @@ -429,33 +489,31 @@ namespace bv { auto& a = wval0(e->get_arg(0)); auto& b = wval0(e->get_arg(1)); auto sh = b.to_nat(b.bits, b.bw); - auto sign = a.get(a.bits, a.bw - 1); - if (sh == 0) { - for (unsigned i = 0; i < a.nw; ++i) - val.bits[i] = a.bits[i]; - } + auto sign = a.sign(); + if (sh == 0) + val.set(a.bits); else if (sh >= b.bw) { for (unsigned i = 0; i < a.nw; ++i) val.bits[i] = sign ? ~0 : 0; } else { - for (unsigned i = 0; i < a.bw; ++i) - val.set(val.bits, i, i + sh < a.bw && b.get(b.bits, i + sh)); + for (unsigned i = 0; i < a.bw; ++i) + val.set(val.bits, i, i + sh < a.bw && a.get(a.bits, i + sh)); if (sign) - val.set_range(val.bits, 0, a.bw - sh, true); + val.set_range(val.bits, a.bw - sh, a.bw, true); } break; } case OP_SIGN_EXT: { auto& a = wval0(e->get_arg(0)); - a.set(val.bits); - bool sign = a.get(a.bits, a.bw - 1); + val.set(a.bits); + bool sign = a.sign(); val.set_range(val.bits, a.bw, val.bw, sign); break; } case OP_ZERO_EXT: { auto& a = wval0(e->get_arg(0)); - a.set(val.bits); + val.set(a.bits); val.set_range(val.bits, a.bw, val.bw, false); break; } @@ -505,7 +563,7 @@ namespace bv { mpn.sub(b.bits.data(), a.nw, m_tmp2.data(), a.nw, m_tmp.data(), &c), val.set(m_tmp); else if (b.sign()) - mpn.add(b.bits.data(), a.nw, m_tmp2.data(), a.nw, m_tmp.data(), a.nw, &c), + mpn.add(b.bits.data(), a.nw, m_tmp2.data(), a.nw, m_tmp.data(), a.nw + 1, &c), val.set(m_tmp); else val.set(m_tmp2); @@ -518,11 +576,8 @@ namespace bv { // x div 0 = -1 auto& a = wval0(e->get_arg(0)); auto& b = wval0(e->get_arg(1)); - if (b.is_zero()) { - val.set(m_zero); - for (unsigned i = 0; i < a.nw; ++i) - val.bits[i] = ~val.bits[i]; - } + if (b.is_zero()) + val.set(m_minus_one); else { mpn.div(a.bits.data(), a.nw, b.bits.data(), b.nw, @@ -535,17 +590,57 @@ namespace bv { case OP_BSDIV: case OP_BSDIV_I: - case OP_BSDIV0: - // d = udiv(abs(x), abs(y)) - // y = 0, x > 0 -> 1 - // y = 0, x <= 0 -> -1 - // x = 0, y != 0 -> 0 - // x > 0, y < 0 -> -d - // x < 0, y > 0 -> -d - // x > 0, y > 0 -> d - // x < 0, y < 0 -> d - - + case OP_BSDIV0: { + set_sdiv(); + break; + } + case OP_BSREM: + case OP_BSREM0: + case OP_BSREM_I: { + // y = 0 -> x + // else x - sdiv(x, y) * y + // + auto& a = wval0(e->get_arg(0)); + auto& b = wval0(e->get_arg(1)); + if (b.is_zero()) + val.set(a.bits); + else { + digit_t c; + set_sdiv(); + mpn.mul(val.bits.data(), a.nw, b.bits.data(), a.nw, m_tmp.data()); + mpn.sub(a.bits.data(), a.nw, m_tmp.data(), a.nw, m_tmp2.data(), &c); + val.set(m_tmp2); + } + break; + } + case OP_ROTATE_LEFT: { + unsigned n = e->get_parameter(0).get_int() % val.bw; + mk_rotate_left(n); + break; + } + case OP_ROTATE_RIGHT: { + unsigned n = e->get_parameter(0).get_int() % val.bw; + mk_rotate_left(val.bw - n); + break; + } + case OP_EXT_ROTATE_LEFT: { + auto& b = wval0(e->get_arg(1)); + rational n; + b.get_value(b.bits, n); + n = mod(n, rational(val.bw)); + SASSERT(n.is_unsigned()); + mk_rotate_left(n.get_unsigned()); + break; + } + case OP_EXT_ROTATE_RIGHT: { + auto& b = wval0(e->get_arg(1)); + rational n; + b.get_value(b.bits, n); + n = mod(n, rational(val.bw)); + SASSERT(n.is_unsigned()); + mk_rotate_left(val.bw - n.get_unsigned()); + break; + } case OP_BREDAND: case OP_BREDOR: case OP_BXNOR: @@ -693,22 +788,37 @@ namespace bv { VERIFY(bv.is_bit2bool(e, arg, idx)); return try_repair_bit2bool(wval0(e, 0), idx); } + case OP_BSDIV: + case OP_BSDIV_I: + case OP_BSDIV0: + return try_repair_sdiv(wval0(e), wval0(e, 0), wval0(e, 1), i); + case OP_BUDIV: + case OP_BUDIV_I: + case OP_BUDIV0: + return try_repair_udiv(wval0(e), wval0(e, 0), wval0(e, 1), i); + case OP_BUREM: + case OP_BUREM_I: + case OP_BUREM0: + return try_repair_urem(wval0(e), wval0(e, 0), wval0(e, 1), i); + case OP_BSREM: + case OP_BSREM_I: + case OP_BSREM0: + return try_repair_srem(wval0(e), wval0(e, 0), wval0(e, 1), i); + case OP_BSMOD: + case OP_BSMOD_I: + case OP_BSMOD0: + return try_repair_smod(wval0(e), wval0(e, 0), wval0(e, 1), i); + case OP_ROTATE_LEFT: + return try_repair_rotate_left(wval0(e), wval0(e, 0), e->get_parameter(0).get_int()); + case OP_ROTATE_RIGHT: + return try_repair_rotate_left(wval0(e), wval0(e, 0), wval0(e).bw - e->get_parameter(0).get_int()); + case OP_EXT_ROTATE_LEFT: + return try_repair_rotate_left(wval0(e), wval0(e, 0), wval0(e, 1), i); + case OP_EXT_ROTATE_RIGHT: case OP_BCOMP: case OP_BNAND: case OP_BREDAND: case OP_BREDOR: - case OP_BSDIV: - case OP_BSDIV_I: - case OP_BSDIV0: - case OP_BUDIV: - case OP_BUDIV_I: - case OP_BUDIV0: - case OP_BUREM: - case OP_BUREM_I: - case OP_BUREM0: - case OP_BSMOD: - case OP_BSMOD_I: - case OP_BSMOD0: case OP_BXNOR: case OP_BNEG_OVFL: case OP_BSADD_OVFL: @@ -883,7 +993,7 @@ namespace bv { return a.try_set(b.bits); else { digit_t c; - mpn.add(b.bits.data(), a.nw, m_one.data(), a.nw, &c, a.nw, m_tmp.data()); + mpn.add(b.bits.data(), a.nw, m_one.data(), a.nw, &c, a.nw + 1, m_tmp.data()); return a.try_set(m_tmp); } } @@ -918,9 +1028,8 @@ namespace bv { unsigned sh = b.to_nat(b.bits, b.bw); if (sh == 0) return a.try_set(e.bits); - else if (sh >= b.bw) { - return false; - } + else if (sh >= b.bw) + return false; else { // // e = a << sh @@ -936,29 +1045,91 @@ namespace bv { } } else { + // NB. blind sub-range of possible values for b SASSERT(i == 1); + unsigned sh = m_rand(a.bw + 1); + b.set(m_tmp, sh); + return b.try_set(m_tmp); } return false; } bool sls_eval::try_repair_ashr(bvval const& e, bvval & a, bvval& b, unsigned i) { if (i == 0) { - + unsigned sh = b.to_nat(b.bits, b.bw); + if (sh == 0) + return a.try_set(e.bits); + else if (sh >= b.bw) + return false; + else { + // e = a >> sh + // a[bw-1:sh] = e[bw-sh-1:0] + // a[sh-1:0] = a[sh-1:0] + // ignore sign + for (unsigned i = 0; i < a.bw - sh; ++i) + a.set(m_tmp, i + sh, e.get(e.bits, i)); + for (unsigned i = 0; i < sh; ++i) + a.set(m_tmp, i, a.get(a.bits, i)); + return a.try_set(m_tmp); + } } else { - + // NB. blind sub-range of possible values for b + SASSERT(i == 1); + unsigned sh = m_rand(a.bw + 1); + b.set(m_tmp, sh); + return b.try_set(m_tmp); } return false; } bool sls_eval::try_repair_lshr(bvval const& e, bvval& a, bvval& b, unsigned i) { - if (i == 0) { + return try_repair_ashr(e, a, b, i); + } + bool sls_eval::try_repair_sdiv(bvval const& e, bvval& a, bvval& b, unsigned i) { + return false; + } + + bool sls_eval::try_repair_udiv(bvval const& e, bvval& a, bvval& b, unsigned i) { + return false; + } + + bool sls_eval::try_repair_smod(bvval const& e, bvval& a, bvval& b, unsigned i) { + return false; + } + + bool sls_eval::try_repair_urem(bvval const& e, bvval& a, bvval& b, unsigned i) { + return false; + } + + bool sls_eval::try_repair_srem(bvval const& e, bvval& a, bvval& b, unsigned i) { + return false; + } + + bool sls_eval::try_repair_rotate_left(bvval const& e, bvval& a, unsigned n) { + // a := rotate_right(e, n) + n = (n % a.bw) - n; + for (unsigned i = a.bw - n; i < a.bw; ++i) + a.set(m_tmp, i + n - a.bw, e.get(e.bits, i)); + for (unsigned i = 0; i < a.bw - n; ++i) + a.set(m_tmp, i + a.bw - n, e.get(e.bits, i)); + return a.try_set(m_tmp); + } + + bool sls_eval::try_repair_rotate_left(bvval const& e, bvval& a, bvval& b, unsigned i) { + if (i == 0) { + rational n; + b.get_value(b.bits, n); + n = mod(n, rational(b.bw)); + return try_repair_rotate_left(e, a, n.get_unsigned()); } else { - - } - return false; + SASSERT(i == 1); + unsigned sh = m_rand(b.bw); + b.set(m_tmp, sh); + return b.try_set(m_tmp); + } } void sls_eval::repair_up(expr* e) { diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h index 85be65377..7d487ea7c 100644 --- a/src/ast/sls/bv_sls_eval.h +++ b/src/ast/sls/bv_sls_eval.h @@ -27,10 +27,11 @@ namespace bv { class sls_eval { friend class sls_fixed; + friend class sls_test; ast_manager& m; bv_util bv; sls_fixed m_fix; - mutable mpn_manager mpn; + mutable mpn_manager mpn; ptr_vector m_todo; random_gen m_rand; @@ -38,7 +39,7 @@ namespace bv { bool_vector m_eval; // expr-id -> boolean valuation bool_vector m_fixed; // expr-id -> is Boolean fixed - mutable svector m_tmp, m_tmp2, m_zero, m_one; + mutable svector m_tmp, m_tmp2, m_tmp3, m_tmp4, m_zero, m_one, m_minus_one; using bvval = sls_valuation; @@ -82,6 +83,14 @@ namespace bv { bool try_repair_ashr(bvval const& e, bvval& a, bvval& b, unsigned i); bool try_repair_lshr(bvval const& e, bvval& a, bvval& b, unsigned i); bool try_repair_bit2bool(bvval& a, unsigned idx); + bool try_repair_sdiv(bvval const& e, bvval& a, bvval& b, unsigned i); + bool try_repair_udiv(bvval const& e, bvval& a, bvval& b, unsigned i); + bool try_repair_smod(bvval const& e, bvval& a, bvval& b, unsigned i); + bool try_repair_urem(bvval const& e, bvval& a, bvval& b, unsigned i); + bool try_repair_srem(bvval const& e, bvval& a, bvval& b, unsigned i); + bool try_repair_rotate_left(bvval const& e, bvval& a, unsigned n); + bool try_repair_rotate_left(bvval const& e, bvval& a, bvval& b, unsigned i); + sls_valuation& wval0(app* e, unsigned i) { return wval0(e->get_arg(i)); } @@ -123,7 +132,6 @@ namespace bv { m_eval[e->get_id()] = b; } - /* * Try to invert value of child to repair value assignment of parent. */ diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp index a45602899..e2c58a47c 100644 --- a/src/ast/sls/sls_valuation.cpp +++ b/src/ast/sls/sls_valuation.cpp @@ -25,10 +25,10 @@ namespace bv { sls_valuation::sls_valuation(unsigned bw): bw(bw) { nw = (bw + sizeof(digit_t) * 8 - 1) / (8 * sizeof(digit_t)); unsigned num_bytes = nw * sizeof(digit_t); - lo.reserve(nw); - hi.reserve(nw); - bits.reserve(nw); - fixed.reserve(nw); + lo.reserve(nw + 1); + hi.reserve(nw + 1); + bits.reserve(nw + 1); + fixed.reserve(nw + 1); // have lo, hi bits, fixed point to memory allocated within this of size num_bytes each allocated for (unsigned i = 0; i < nw; ++i) lo[i] = 0, hi[i] = 0, bits[i] = 0, fixed[i] = 0; @@ -84,6 +84,11 @@ namespace bv { } } + void sls_valuation::get(svector& dst) const { + for (unsigned i = 0; i < nw; ++i) + dst[i] = bits[i]; + } + void sls_valuation::set1(svector& bits) { for (unsigned i = 0; i < bw; ++i) set(bits, i, true); diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h index 4caf1612a..60139f53e 100644 --- a/src/ast/sls/sls_valuation.h +++ b/src/ast/sls/sls_valuation.h @@ -40,8 +40,10 @@ namespace bv { void set_value(svector& bits, rational const& r); void get_value(svector const& bits, rational& r) const; + void get(svector& dst) const; void add_range(rational lo, rational hi); void set1(svector& bits); + void clear_overflow_bits(svector& bits) const; bool can_set(svector const& bits) const; @@ -90,6 +92,11 @@ namespace bv { clear_overflow_bits(bits); } + void set_zero() { + for (unsigned i = 0; i < nw; ++i) + bits[i] = 0; + } + void set_fixed(svector const& src) { for (unsigned i = nw; i-- > 0; ) diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 14b51f822..4ddc1b8cb 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -108,6 +108,7 @@ add_executable(test-z3 simple_parser.cpp simplex.cpp simplifier.cpp + sls_test.cpp small_object_allocator.cpp smt2print_parse.cpp smt_context.cpp diff --git a/src/test/main.cpp b/src/test/main.cpp index 3f073abf2..0c3d0e01a 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -267,4 +267,5 @@ int main(int argc, char ** argv) { TST(distribution); TST(euf_bv_plugin); TST(euf_arith_plugin); + TST(sls_test); } diff --git a/src/test/sls_test.cpp b/src/test/sls_test.cpp new file mode 100644 index 000000000..197fa96c9 --- /dev/null +++ b/src/test/sls_test.cpp @@ -0,0 +1,203 @@ + +#include "ast/sls/bv_sls_eval.h" +#include "ast/rewriter/th_rewriter.h" +#include "ast/reg_decl_plugins.h" +#include "ast/ast_pp.h" + +namespace bv { + class sls_test { + ast_manager& m; + bv_util bv; + + public: + sls_test(ast_manager& m): + m(m), + bv(m) + {} + + void check_eval(expr* e) { + std::function value = [](expr*, unsigned) { + return false; + }; + expr_ref_vector es(m); + bv_util bv(m); + es.push_back(e); + sls_eval ev(m); + ev.init_eval(es, value); + th_rewriter rw(m); + expr_ref r(e, m); + rw(r); + + if (bv.is_bv(e)) { + auto const& val = ev.wval0(e); + rational n1, n2; + + val.get_value(val.bits, n1); + + VERIFY(bv.is_numeral(r, n2)); + if (n1 != n2) { + verbose_stream() << mk_pp(e, m) << " computed value " << val << "\n"; + verbose_stream() << "should be " << n2 << "\n"; + } + SASSERT(n1 == n2); + VERIFY(n1 == n2); + } + else if (m.is_bool(e)) { + auto val1 = ev.bval0(e); + auto val2 = m.is_true(r) ? true : false; + if (val1 != val2) { + verbose_stream() << mk_pp(e, m) << " computed value " << val1 << " at odds with definition\n"; + } + SASSERT(val1 == val2); + VERIFY(val1 == val2); + } + } + + void check(expr* a, expr* b) { + expr_ref e(m); + auto& validator = *this; + e = bv.mk_bv_add(a, b); + validator.check_eval(e); + + e = bv.mk_bv_mul(a, b); + validator.check_eval(e); + + e = bv.mk_bv_sub(a, b); + validator.check_eval(e); + + e = bv.mk_bv_udiv(a, b); + validator.check_eval(e); + + e = bv.mk_bv_sdiv(a, b); + validator.check_eval(e); + + e = bv.mk_bv_srem(a, b); + validator.check_eval(e); + + e = bv.mk_bv_urem(a, b); + validator.check_eval(e); + + e = bv.mk_bv_smod(a, b); + validator.check_eval(e); + + e = bv.mk_bv_shl(a, b); + validator.check_eval(e); + + e = bv.mk_bv_ashr(a, b); + validator.check_eval(e); + + e = bv.mk_bv_lshr(a, b); + validator.check_eval(e); + + e = bv.mk_bv_and(a, b); + validator.check_eval(e); + + e = bv.mk_bv_or(a, b); + validator.check_eval(e); + + e = bv.mk_bv_xor(a, b); + validator.check_eval(e); + + e = bv.mk_bv_neg(a); + validator.check_eval(e); + + e = bv.mk_bv_not(a); + validator.check_eval(e); + + e = bv.mk_bvumul_ovfl(a, b); + validator.check_eval(e); + + e = bv.mk_bvumul_no_ovfl(a, b); + validator.check_eval(e); + + e = bv.mk_zero_extend(3, a); + validator.check_eval(e); + + e = bv.mk_sign_extend(3, a); + validator.check_eval(e); + + e = bv.mk_ule(a, b); + validator.check_eval(e); + + e = bv.mk_sle(a, b); + validator.check_eval(e); + + e = bv.mk_concat(a, b); + validator.check_eval(e); + + e = bv.mk_extract(6, 3, a); + validator.check_eval(e); + + e = bv.mk_bvuadd_ovfl(a, b); + validator.check_eval(e); + + +#if 0 + + e = bv.mk_bvsadd_ovfl(a, b); + validator.check_eval(e); + + e = bv.mk_bvneg_ovfl(a); + validator.check_eval(e); + + e = bv.mk_bvsmul_no_ovfl(a, b); + validator.check_eval(e); + + e = bv.mk_bvsmul_no_udfl(a, b); + validator.check_eval(e); + + e = bv.mk_bvsmul_ovfl(a, b); + validator.check_eval(e); + + e = bv.mk_bvsdiv_ovfl(a, b); + validator.check_eval(e); + +#endif + +#if 0 + e = bv.mk_rotate_left(a, b); + validator.check_eval(e); + + e = bv.mk_rotate_right(a, b); + validator.check_eval(e); + + e = bv.mk_rotate_left_ext(a, b); + validator.check_eval(e); + + e = bv.mk_rotate_right_ext(a, b); + validator.check_eval(e); + +#endif + } + }; +} + + +static void test_eval1() { + ast_manager m; + reg_decl_plugins(m); + bv_util bv(m); + + expr_ref e(m); + + bv::sls_test validator(m); + + unsigned k = 0; + for (unsigned i = 0; i < 256; ++i) { + expr_ref a(bv.mk_numeral(rational(i), 8), m); + for (unsigned j = 0; j < 256; ++j) { + expr_ref b(bv.mk_numeral(rational(j), 8), m); + + ++k; + if (k % 1000 == 0) + verbose_stream() << "tests " << k << "\n"; + + validator.check(a, b); + + } + } +} + +void tst_sls_test() { + test_eval1(); +}