consider all non-det vars in undef refinement formula
this could use some refactoring to rename things at least..
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2686,7 +2686,7 @@ static StateValue freeze_elems(State &s, const Type &ty, const StateValue &v) {
StateValue ret_type = ty.getDummyValue(true);
expr nondet = expr::mkFreshVar("nondet", ret_type.value);
- s.addQuantVar(nondet);
+ s.addFreezeVar(nondet);
return { expr::mkIf(v.non_poison, v.value, nondet),
std::move(ret_type.non_poison) };
}

MODIFY
ir/state.cpp
ir/state.cpp
@@ -461,7 +461,7 @@ const StateValue& State::operator[](const Value &val) {
if (is_non_undef) {
// We don't need to add uvar to undef_vars
- quantified_vars.insert(uvars.begin(), uvars.end());
+ freeze_vars.insert(uvars.begin(), uvars.end());
return simplify(sval, true);
}
@@ -1011,6 +1011,10 @@ void State::addQuantVar(const expr &var) {
quantified_vars.emplace(var);
}
+void State::addFreezeVar(const expr &var) {
+ freeze_vars.emplace(var);
+}
+
void State::addFnQuantVar(const expr &var) {
fn_call_qvars.emplace(var);
}
@@ -1020,7 +1024,7 @@ void State::addUndefVar(expr &&var) {
}
void State::resetUndefVars() {
- quantified_vars.insert(undef_vars.begin(), undef_vars.end());
+ freeze_vars.insert(undef_vars.begin(), undef_vars.end());
undef_vars.clear();
}

MODIFY
ir/state.h
ir/state.h
@@ -112,6 +112,7 @@ private:
std::set<std::pair<std::string,std::optional<smt::expr>>> used_approximations;
std::set<smt::expr> quantified_vars;
+ std::set<smt::expr> freeze_vars;
// var -> ((value, not_poison), ub, undef_vars)
std::unordered_map<const Value*, unsigned> values_map;
@@ -237,6 +238,7 @@ public:
auto& getApproximations() const { return used_approximations; }
void addQuantVar(const smt::expr &var);
+ void addFreezeVar(const smt::expr &var);
void addFnQuantVar(const smt::expr &var);
void addUndefVar(smt::expr &&var);
auto& getUndefVars() const { return undef_vars; }
@@ -259,6 +261,7 @@ public:
auto& getFnPre() const { return fn_call_pre; }
const auto& getValues() const { return values; }
const auto& getQuantVars() const { return quantified_vars; }
+ const auto& getFreezeVars() const { return freeze_vars; }
const auto& getFnQuantVars() const { return fn_call_qvars; }
void saveReturnedInput();

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -362,7 +362,10 @@ encode_undef_refinement_per_elem(const Type &ty, const StateValue &sva,
}
// Returns negation of refinement
-static expr encode_undef_refinement(const Type &type, const State::ValTy &a,
+static expr encode_undef_refinement(const State &src_state,
+ const State &tgt_state,
+ const Type &type,
+ const State::ValTy &a,
const State::ValTy &b) {
// Undef refinement: (src-nonpoison /\ src-nonundef) -> tgt-nonundef
//
@@ -379,7 +382,7 @@ static expr encode_undef_refinement(const Type &type, const State::ValTy &a,
// target is never undef
return false;
- auto subst = [](const auto &val) {
+ auto subst = [](const State &state, const auto &val) {
vector<pair<expr, expr>> repls;
for (auto &v : val.undef_vars) {
repls.emplace_back(v, expr::some(v));
@@ -387,18 +390,18 @@ static expr encode_undef_refinement(const Type &type, const State::ValTy &a,
// We need to consider fresh variables that are produced for specific
// expressions. Since we are now rewriting those expressions, those
- // variables *may* need to be refreshed. For now consider just NaNs.
+ // variables *may* need to be refreshed.
if (!repls.empty()) {
- for (auto &v : val.val.vars()) {
- if (v.fn_name().starts_with("#NaN!"))
+ for (auto &v : state.getQuantVars()) {
repls.emplace_back(v, expr::some(v));
}
}
return val.val.value.subst(repls);
};
- return encode_undef_refinement_per_elem(type, a.val, subst(a),
- expr(b.val.value), subst(b));
+ return encode_undef_refinement_per_elem(type, a.val, subst(src_state, a),
+ expr(b.val.value),
+ subst(tgt_state, b));
}
static void
@@ -416,6 +419,8 @@ check_refinement(Errors &errs, const Transform &t, State &src_state,
auto &uvars = ap.undef_vars;
auto qvars = src_state.getQuantVars();
qvars.insert(ap.undef_vars.begin(), ap.undef_vars.end());
+ auto &src_freeze_vars = src_state.getFreezeVars();
+ qvars.insert(src_freeze_vars.begin(), src_freeze_vars.end());
auto &fn_qvars = tgt_state.getFnQuantVars();
qvars.insert(fn_qvars.begin(), fn_qvars.end());
@@ -536,7 +541,7 @@ check_refinement(Errors &errs, const Transform &t, State &src_state,
print_value, "Target is more poisonous than source");
// 4. Check undef
- CHECK(dom && encode_undef_refinement(type, ap, bp),
+ CHECK(dom && encode_undef_refinement(src_state, tgt_state, type, ap, bp),
print_value, "Target's return value is more undefined");
// 5. Check value

consider all non-det vars in undef refinement formula
this could use some refactoring to rename things at least..