refinment: further reduce peak memory and duplicate unrolling queries

AliveToolkit · Dec 11, 2023 · 2fb4354 · 2fb4354
1 parent fa7614f
commit 2fb4354
Show file tree

Hide file tree

Showing 2 changed files with 55 additions and 44 deletions.
diff --git a/smt/expr.cpp b/smt/expr.cpp
@@ -2075,7 +2075,7 @@ expr expr::mkForAll(const set<expr> &vars, expr &&val) {
   if (vars.empty() || val.isConst() || !val.isValid())
     return std::move(val);
 
-  unique_ptr<Z3_app[]> vars_ast(new Z3_app[vars.size()]);
+  auto vars_ast = make_unique<Z3_app[]>(vars.size());
   unsigned i = 0;
   for (auto &v : vars) {
     vars_ast[i++] = (Z3_app)v();
@@ -2137,8 +2137,8 @@ expr expr::subst(const vector<pair<expr, expr>> &repls) const {
   if (repls.empty())
     return *this;
 
-  unique_ptr<Z3_ast[]> from(new Z3_ast[repls.size()]);
-  unique_ptr<Z3_ast[]> to(new Z3_ast[repls.size()]);
+  auto from = make_unique<Z3_ast[]>(repls.size());
+  auto to   = make_unique<Z3_ast[]>(repls.size());
 
   unsigned i = 0;
   for (auto &p : repls) {

diff --git 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<pair<expr,expr>> 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<pair<expr, expr>> 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)
   {