Don't add undef vars if analysis says it's never undef
MODIFY
ir/state.cpp
ir/state.cpp
@@ -186,6 +186,9 @@ const StateValue& State::operator[](const Value &val) {
auto &[sval, uvars] = val_uvars;
(void)var;
+ auto undef_itr = analysis.non_undef_vals.find(&val);
+ bool is_non_undef = undef_itr != analysis.non_undef_vals.end();
+
auto simplify = [&](StateValue &sv0, bool use_new_slot) -> StateValue&{
StateValue *sv = &sv0;
if (analysis.non_poison_vals.count(&val)) {
@@ -201,8 +204,7 @@ const StateValue& State::operator[](const Value &val) {
sv = &sv_new;
}
- auto undef_itr = analysis.non_undef_vals.find(&val);
- if (undef_itr != analysis.non_undef_vals.end()) {
+ if (is_non_undef) {
if (use_new_slot) {
assert(i_tmp_values < tmp_values.size());
tmp_values[i_tmp_values++] = *sv;
@@ -215,6 +217,15 @@ const StateValue& State::operator[](const Value &val) {
return *sv;
};
+ if (is_non_undef) {
+ // We don't need to add uvar to undef_vars
+ // We add it to quantified_vars as a safety net because the current
+ // encoding of function call may lose uvars to be quantified, currently.
+ // They should be optimized ideally if never used.
+ quantified_vars.insert(uvars.begin(), uvars.end());
+ return simplify(sval, true);
+ }
+
if (uvars.empty() || !used || disable_undef_rewrite) {
used = true;
undef_vars.insert(uvars.begin(), uvars.end());

MODIFY
ir/state.h
ir/state.h
@@ -136,6 +136,7 @@ public:
static void resetGlobals();
+ /*--- Get values or update registers ---*/
const StateValue& exec(const Value &v);
const StateValue& operator[](const Value &val);
const StateValue& getAndAddUndefs(const Value &val);
@@ -143,9 +144,10 @@ public:
const StateValue& getAndAddPoisonUB(const Value &val, bool undef_ub = false);
const ValTy& at(const Value &val) const;
- const smt::OrExpr* jumpCondFrom(const BasicBlock &bb) const;
bool isUndef(const smt::expr &e, const Value *used_by = nullptr) const;
+ /*--- Control flow ---*/
+ const smt::OrExpr* jumpCondFrom(const BasicBlock &bb) const;
bool startBB(const BasicBlock &bb);
void addJump(const BasicBlock &dst);
// boolean cond
@@ -155,6 +157,7 @@ public:
const BasicBlock &dst_false);
void addReturn(StateValue &&val);
+ /*--- Axioms, preconditions, domains ---*/
void addAxiom(smt::AndExpr &&ands) { axioms.add(std::move(ands)); }
void addAxiom(smt::expr &&axiom) { axioms.add(std::move(axiom)); }
void addPre(smt::expr &&cond) { precondition.add(std::move(cond)); }

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -305,6 +305,7 @@ encode_undef_refinement_per_elem(const Type &ty, const StateValue &sva,
return result;
}
+// Returns negation of refinement
static expr encode_undef_refinement(const Type &type, const State::ValTy &a,
const State::ValTy &b) {
// Undef refinement: (src-nonpoison /\ src-nonundef) -> tgt-nonundef
@@ -316,6 +317,9 @@ static expr encode_undef_refinement(const Type &type, const State::ValTy &a,
if (dynamic_cast<const VoidType *>(&type))
return false;
+ if (b.second.empty())
+ // target is never undef
+ return false;
auto subst = [](const auto &val) {
vector<pair<expr, expr>> repls;

Don't add undef vars if analysis says it's never undef (#491)