From a0999723543fab1efb1314b577e31752e5b95d3d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Dec 2021 10:20:53 -0800 Subject: [PATCH] fix #5714 It is not unlike other fuzz bugs: it exercises some behavior that applications are unlikely to expose. In this case, a rule body expanded into a conjunction with more than 1M formulas (with a lot of repetition). The original rule representation assumed silently that the number of constraints in a body would fit within 20 bits, but reality allowed bodies with as many as 2^{32} - 1 constraints. So "minimizing" the bug as @agurfinkel asks for seems not to make too much sense. Just running the samples in debug mode points to the root cause. Since fuzz bugs are not from applications and fuzz tools have the potential for creating a large number of issues, I find it reasonable to push some basic pro-active asks on filers: - reproduce bug in debug builds to assess whether a debug assert triggers. - minimize or keep it simpler when possible (in this case it does not apply) - perform basic diagnostics/triage. I am basically asking to push this part of the work on to the fuzzer. Otherwise, addressing random bugs doesn't scale. Triaging should have pointed to the root cause. Now, there tends to be something to learn from bugs. In this case, the question was: "can we avoid constraints with duplications"? In particular, it points to a basic inefficiency of extracting conjunctions (and disjunctions). The function didn't deduplicate. So I added deduplication into this function. It is used throughout z3 code base so could expose latent issues. We will see. --- src/ast/ast_util.cpp | 46 ++++++++++++++++++++++++---------------- src/muz/base/dl_rule.cpp | 18 +++++++--------- src/muz/base/dl_rule.h | 13 ++++++------ 3 files changed, 42 insertions(+), 35 deletions(-) diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp index 993831d64..bec80240f 100644 --- a/src/ast/ast_util.cpp +++ b/src/ast/ast_util.cpp @@ -260,39 +260,44 @@ expr_ref mk_distinct(expr_ref_vector const& args) { void flatten_and(expr_ref_vector& result) { ast_manager& m = result.get_manager(); expr* e1, *e2, *e3; + expr_fast_mark1 seen; for (unsigned i = 0; i < result.size(); ++i) { - if (m.is_and(result.get(i))) { - app* a = to_app(result.get(i)); + expr* e = result.get(i); + if (seen.is_marked(e)) + continue; + seen.mark(e); + if (m.is_and(e)) { + app* a = to_app(e); for (expr* arg : *a) result.push_back(arg); result[i] = result.back(); result.pop_back(); --i; } - else if (m.is_not(result.get(i), e1) && m.is_not(e1, e2)) { + else if (m.is_not(e, e1) && m.is_not(e1, e2)) { result[i] = e2; --i; } - else if (m.is_not(result.get(i), e1) && m.is_or(e1)) { + else if (m.is_not(e, e1) && m.is_or(e1)) { app* a = to_app(e1); for (expr* arg : *a) result.push_back(m.mk_not(arg)); result[i] = result.back(); result.pop_back(); --i; } - else if (m.is_not(result.get(i), e1) && m.is_implies(e1,e2,e3)) { + else if (m.is_not(e, e1) && m.is_implies(e1, e2, e3)) { result.push_back(e2); result[i] = m.mk_not(e3); --i; } - else if (m.is_true(result.get(i)) || - (m.is_not(result.get(i), e1) && + else if (m.is_true(e) || + (m.is_not(e, e1) && m.is_false(e1))) { result[i] = result.back(); result.pop_back(); --i; } - else if (m.is_false(result.get(i)) || - (m.is_not(result.get(i), e1) && + else if (m.is_false(e) || + (m.is_not(e, e1) && m.is_true(e1))) { result.reset(); result.push_back(m.mk_false()); @@ -317,39 +322,44 @@ void flatten_and(expr_ref& fml) { void flatten_or(expr_ref_vector& result) { ast_manager& m = result.get_manager(); expr* e1, *e2, *e3; + expr_fast_mark1 seen; for (unsigned i = 0; i < result.size(); ++i) { - if (m.is_or(result.get(i))) { - app* a = to_app(result.get(i)); + expr* e = result.get(i); + if (seen.is_marked(e)) + continue; + seen.mark(e); + if (m.is_or(e)) { + app* a = to_app(e); for (expr* arg : *a) result.push_back(arg); result[i] = result.back(); result.pop_back(); --i; } - else if (m.is_not(result.get(i), e1) && m.is_not(e1, e2)) { + else if (m.is_not(e, e1) && m.is_not(e1, e2)) { result[i] = e2; --i; } - else if (m.is_not(result.get(i), e1) && m.is_and(e1)) { + else if (m.is_not(e, e1) && m.is_and(e1)) { app* a = to_app(e1); for (expr* arg : *a) result.push_back(m.mk_not(arg)); result[i] = result.back(); result.pop_back(); --i; } - else if (m.is_implies(result.get(i),e2,e3)) { + else if (m.is_implies(e,e2,e3)) { result.push_back(e3); result[i] = m.mk_not(e2); --i; } - else if (m.is_false(result.get(i)) || - (m.is_not(result.get(i), e1) && + else if (m.is_false(e) || + (m.is_not(e, e1) && m.is_true(e1))) { result[i] = result.back(); result.pop_back(); --i; } - else if (m.is_true(result.get(i)) || - (m.is_not(result.get(i), e1) && + else if (m.is_true(e) || + (m.is_not(e, e1) && m.is_false(e1))) { result.reset(); result.push_back(m.mk_true()); diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index 2baaf57b9..9bd7a7adf 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -178,7 +178,7 @@ namespace datalog { m_ctx.register_predicate(m_hnf.get_fresh_predicates()[i], false); } for (unsigned i = 0; i < fmls.size(); ++i) { - mk_horn_rule(fmls[i].get(), prs[i].get(), rules, name); + mk_horn_rule(fmls.get(i), prs.get(i), rules, name); } } @@ -190,12 +190,10 @@ namespace datalog { hoist_compound_predicates(index, m_head, m_body); TRACE("dl_rule", tout << mk_pp(m_head, m) << " :- "; - for (unsigned i = 0; i < m_body.size(); ++i) { - tout << mk_pp(m_body[i].get(), m) << " "; - } + for (expr* b : m_body) + tout << mk_pp(b, m) << " "; tout << "\n";); - mk_negations(m_body, m_neg); check_valid_rule(m_head, m_body.size(), m_body.data()); @@ -241,9 +239,8 @@ namespace datalog { m_args.reset(); head = ensure_app(e2); flatten_and(e1, m_args); - for (unsigned i = 0; i < m_args.size(); ++i) { - body.push_back(ensure_app(m_args[i].get())); - } + for (expr* a : m_args) + body.push_back(ensure_app(a)); } else { head = ensure_app(fml); @@ -255,7 +252,7 @@ namespace datalog { unsigned sz = body.size(); hoist_compound(index, head, body); for (unsigned i = 0; i < sz; ++i) { - app_ref b(body[i].get(), m); + app_ref b(body.get(i), m); hoist_compound(index, b, body); body[i] = b; } @@ -949,7 +946,8 @@ namespace datalog { } bool rule::has_negation() const { - for (unsigned i = 0; i < get_uninterpreted_tail_size(); ++i) { + unsigned sz = get_uninterpreted_tail_size(); + for (unsigned i = 0; i < sz; ++i) { if (is_neg_tail(i)) { return true; } diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 044260f12..02d13c1ca 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -287,13 +287,12 @@ namespace datalog { class rule : public accounted_object { friend class rule_manager; - app* m_head{ nullptr }; - proof* m_proof{ nullptr }; - unsigned m_tail_size:20; - // unsigned m_reserve:12; - unsigned m_ref_cnt{ 0 }; - unsigned m_positive_cnt{ 0 }; - unsigned m_uninterp_cnt{ 0 }; + app* m_head = nullptr; + proof* m_proof = nullptr; + unsigned m_tail_size = 0; + unsigned m_ref_cnt = 0; + unsigned m_positive_cnt = 0; + unsigned m_uninterp_cnt = 0; symbol m_name; /** The following field is an array of tagged pointers.