From 2fb4354ffb04ed33274edcd958dd424e58d4451d Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 11 Dec 2023 12:06:33 +0000 Subject: [PATCH] refinment: further reduce peak memory and duplicate unrolling queries --- smt/expr.cpp | 6 +-- tools/transform.cpp | 93 +++++++++++++++++++++++++-------------------- 2 files changed, 55 insertions(+), 44 deletions(-) diff --git a/smt/expr.cpp b/smt/expr.cpp index ed266e108..088044191 100644 --- a/smt/expr.cpp +++ b/smt/expr.cpp @@ -2075,7 +2075,7 @@ expr expr::mkForAll(const set &vars, expr &&val) { if (vars.empty() || val.isConst() || !val.isValid()) return std::move(val); - unique_ptr vars_ast(new Z3_app[vars.size()]); + auto vars_ast = make_unique(vars.size()); unsigned i = 0; for (auto &v : vars) { vars_ast[i++] = (Z3_app)v(); @@ -2137,8 +2137,8 @@ expr expr::subst(const vector> &repls) const { if (repls.empty()) return *this; - unique_ptr from(new Z3_ast[repls.size()]); - unique_ptr to(new Z3_ast[repls.size()]); + auto from = make_unique(repls.size()); + auto to = make_unique(repls.size()); unsigned i = 0; for (auto &p : repls) { diff --git a/tools/transform.cpp b/tools/transform.cpp index a76fd2991..42d1de299 100644 --- a/tools/transform.cpp +++ b/tools/transform.cpp @@ -501,51 +501,57 @@ check_refinement(Errors &errs, const Transform &t, State &src_state, axioms_expr = std::move(axioms)(); } - // note that precondition->toSMT() may add stuff to getPre, - // so order here matters - // FIXME: broken handling of transformation precondition - //src_state.startParsingPre(); - //expr pre = t.precondition ? t.precondition->toSMT(src_state) : true; - expr pre_src, pre_tgt; - { - auto pre_src_and = src_state.getPre(); - auto &pre_tgt_and = tgt_state.getPre(); - - // optimization: rewrite "tgt /\ (src -> foo)" to "tgt /\ foo" if src = tgt - pre_src_and.del(pre_tgt_and); - pre_src = std::move(pre_src_and)(); - pre_tgt = pre_tgt_and(); - } - - if (check_expr(axioms_expr && (pre_src && pre_tgt)).isUnsat()) { - errs.add("Precondition is always false", false); - return; - } - if (config::check_if_src_is_ub && check_expr(axioms_expr && fndom_a).isUnsat()) { errs.add("Source function is always UB", false); return; } - if (auto sink_src = src_state.sinkDomain(false); - !sink_src.isTrue() && check_expr(axioms_expr && !sink_src).isUnsat()) { - errs.add("The source program doesn't reach a return instruction.\n" - "Consider increasing the unroll factor if it has loops", false); - return; - } + bool eq_sink_src_tgt; + { + auto sink_src = src_state.sinkDomain(false); + if (!sink_src.isTrue() && check_expr(axioms_expr && !sink_src).isUnsat()) { + errs.add("The source program doesn't reach a return instruction.\n" + "Consider increasing the unroll factor if it has loops", false); + return; + } - if (auto sink_tgt = tgt_state.sinkDomain(false); - !sink_tgt.isTrue() && check_expr(axioms_expr && !sink_tgt).isUnsat()) { - errs.add("The target program doesn't reach a return instruction.\n" - "Consider increasing the unroll factor if it has loops", false); - return; + auto sink_tgt = tgt_state.sinkDomain(false); + eq_sink_src_tgt = sink_src.eq(sink_tgt); + sink_src = {}; + + if (!eq_sink_src_tgt && + !sink_tgt.isTrue() && check_expr(axioms_expr && !sink_tgt).isUnsat()) { + errs.add("The target program doesn't reach a return instruction.\n" + "Consider increasing the unroll factor if it has loops", false); + return; + } } - pre_tgt &= !tgt_state.sinkDomain(true); + // note that precondition->toSMT() may add stuff to getPre, + // so order here matters + // FIXME: broken handling of transformation precondition + //src_state.startParsingPre(); + //expr pre = t.precondition ? t.precondition->toSMT(src_state) : true; expr pre, pre_src_forall; { - vector> repls; + expr pre_src, pre_tgt; + { + auto pre_src_and = src_state.getPre(); + auto &pre_tgt_and = tgt_state.getPre(); + + // optimization: rewrite "tgt /\ (src -> foo)" to "tgt /\ foo" if src=tgt + pre_src_and.del(pre_tgt_and); + pre_src = std::move(pre_src_and)(); + pre_tgt = pre_tgt_and(); + } + + if (check_expr(axioms_expr && (pre_src && pre_tgt)).isUnsat()) { + errs.add("Precondition is always false", false); + return; + } + + vector> repls; auto vars_pre = pre_src.vars(); for (auto &v : qvars) { if (vars_pre.count(v)) @@ -557,10 +563,6 @@ check_refinement(Errors &errs, const Transform &t, State &src_state, } pre_src_forall &= tgt_state.getFnPre(); - // cleanup - pre_src = {}; - pre_tgt = {}; - auto mk_fml = [&](expr &&refines) -> expr { // from the check above we already know that // \exists v,v' . pre_tgt(v') && pre_src(v) is SAT (or timeout) @@ -608,9 +610,18 @@ check_refinement(Errors &errs, const Transform &t, State &src_state, [](ostream&, const Model&){}, "Target has reachable unreachable"); } - // 1. Check UB - CHECK(fndom_a.notImplies(fndom_b), - [](ostream&, const Model&){}, "Source is more defined than target"); + { + // avoid false-positives in refinement query 1 due to bounded unrolling + expr pre_old = pre; + if (!eq_sink_src_tgt) + pre &= !tgt_state.sinkDomain(true); + + // 1. Check UB + CHECK(fndom_a.notImplies(fndom_b), + [](ostream&, const Model&){}, "Source is more defined than target"); + + pre = std::move(pre_old); + } // 2. Check return domain (noreturn check) {