Function check_refinement

tools/transform.cpp:511–766

}

static void
check_refinement(Errors &errs, const Transform &t, State &src_state,
                 State &tgt_state, const Value *var, const Type &type,
                 const State::ValTy &ap, const State::ValTy &bp,
                 bool check_each_var) {
  auto fndom_a   = ap.domain();
  auto fndom_b   = bp.domain();
  auto &retdom_a = ap.return_domain;
  auto &retdom_b = bp.return_domain;
  auto &a = ap.val;
  auto &b = bp.val;

  auto &uvars = ap.undef_vars;
  auto qvars = src_state.getQuantVars();
  if (!config::disallow_ub_exploitation)
    qvars.insert(ap.undef_vars.begin(), ap.undef_vars.end());
  auto &src_nondet_vars = src_state.getNondetVars();
  qvars.insert(src_nondet_vars.begin(), src_nondet_vars.end());
  auto &fn_qvars = tgt_state.getFnQuantVars();
  qvars.insert(fn_qvars.begin(), fn_qvars.end());

  expr axioms_expr;
  {
    AndExpr axioms = src_state.getAxioms();
    axioms.add(tgt_state.getAxioms());
    axioms_expr = std::move(axioms)();
  }

  if (check_expr(axioms_expr && fndom_a, "ub_src").isUnsat()) {
    if (config::fail_if_src_is_ub) {
      errs.add("Source function is always UB", false);
      return;
    } else {
      errs.addWarning(
        "Source function is always UB.\n"
        "It can be refined by any target function.\n"
        "Please make sure this is what you wanted.");
    }
  }

  // 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;
  {
    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();
    }