Returns negation of refinement
| 469 | |
| 470 | // Returns negation of refinement |
| 471 | static expr encode_undef_refinement(const State &src_state, |
| 472 | const State &tgt_state, |
| 473 | const Type &type, |
| 474 | const State::ValTy &a, |
| 475 | const State::ValTy &b) { |
| 476 | // Undef refinement: (src-nonpoison /\ src-nonundef) -> tgt-nonundef |
| 477 | // |
| 478 | // Full refinement formula: |
| 479 | // forall I . |
| 480 | // (forall N . src_nonpoison(I, N) /\ retval_src(I, N) == retval_src(I, 0)) |
| 481 | // -> (forall N . retval_tgt(I, N) == retval_tgt(I, 0) |
| 482 | // FIXME? this is an approximation. Instead of 0, it should be N' because |
| 483 | // 0 may fail a precondition. |
| 484 | |
| 485 | if (dynamic_cast<const VoidType *>(&type)) |
| 486 | return false; |
| 487 | if (!config::disallow_ub_exploitation && b.undef_vars.empty()) |
| 488 | // target is never undef |
| 489 | return false; |
| 490 | |
| 491 | auto subst = [](const State &state, const auto &val) { |
| 492 | vector<pair<expr, expr>> repls; |
| 493 | for (auto &v : val.undef_vars) { |
| 494 | repls.emplace_back(v, expr::some(v)); |
| 495 | } |
| 496 | |
| 497 | // We need to consider fresh variables that are produced for specific |
| 498 | // expressions. Since we are now rewriting those expressions, those |
| 499 | // variables *may* need to be refreshed. |
| 500 | for (auto &v : state.getNondetVars()) { |
| 501 | repls.emplace_back(v, expr::some(v)); |
| 502 | } |
| 503 | return val.val.value.subst(repls); |
| 504 | }; |
| 505 | |
| 506 | return encode_undef_refinement_per_elem(type, a.val, subst(src_state, a), |
| 507 | expr(b.val.value), |
| 508 | subst(tgt_state, b)); |
| 509 | } |
| 510 | |
| 511 | static void |
| 512 | check_refinement(Errors &errs, const Transform &t, State &src_state, |
no test coverage detected