Add poison analysis
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -249,7 +249,7 @@ void BinOp::print(ostream &os) const {
static void div_ub(State &s, const expr &a, const expr &b, const expr &ap,
const expr &bp, bool sign) {
- s.addUB(bp);
+ // addUB(bp) is not needed because it is registered by getAndAddPoisonUB.
s.addUB(b != 0);
if (sign)
s.addUB((ap && a != expr::IntSMin(b.bits())) || b != expr::mkInt(-1, b));
@@ -637,7 +637,7 @@ StateValue BinOp::toSMT(State &s) const {
}
auto &a = s[*lhs];
- auto &b = s[*rhs];
+ auto &b = isDivOrRem(op) ? s.getAndAddPoisonUB(*rhs) : s[*rhs];
if (lhs->getType().isVectorType()) {
auto retty = getType().getAsAggregateType();
@@ -746,6 +746,18 @@ unique_ptr<Instr> BinOp::dup(const string &suffix) const {
fmath);
}
+bool BinOp::isDivOrRem(const Op op) {
+ switch (op) {
+ case Op::SDiv:
+ case Op::SRem:
+ case Op::UDiv:
+ case Op::URem:
+ return true;
+ default:
+ return false;
+ }
+}
+
vector<Value*> UnaryOp::operands() const {
return { val };
@@ -2543,8 +2555,7 @@ void Free::print(std::ostream &os) const {
}
StateValue Free::toSMT(State &s) const {
- auto &[p, np] = s[*ptr];
- s.addUB(np);
+ auto &p = s.getAndAddPoisonUB(*ptr).value;
// If not heaponly, don't encode constraints
s.getMemory().free(p, !heaponly);
@@ -2719,8 +2730,7 @@ void Load::print(std::ostream &os) const {
}
StateValue Load::toSMT(State &s) const {
- auto &[p, np] = s[*ptr];
- s.addUB(np);
+ auto &p = s.getAndAddPoisonUB(*ptr).value;
auto [sv, ub] = s.getMemory().load(p, getType(), align);
s.addUB(move(ub));
return sv;
@@ -2761,8 +2771,7 @@ void Store::print(std::ostream &os) const {
}
StateValue Store::toSMT(State &s) const {
- auto &[p, np] = s[*ptr];
- s.addUB(np);
+ auto &p = s.getAndAddPoisonUB(*ptr).value;
auto &v = s[*val];
s.getMemory().store(p, v, val->getType(), align, s.getUndefVars());
return {};
@@ -3012,8 +3021,7 @@ void Strlen::print(ostream &os) const {
}
StateValue Strlen::toSMT(State &s) const {
- auto &[eptr, np_ptr] = s[*ptr];
- s.addUB(np_ptr);
+ auto &eptr = s.getAndAddPoisonUB(*ptr).value;
Pointer p(s.getMemory(), eptr);
Type &ty = getType();

MODIFY
ir/instr.h
ir/instr.h
@@ -66,6 +66,8 @@ public:
StateValue toSMT(State &s) const override;
smt::expr getTypeConstraints(const Function &f) const override;
std::unique_ptr<Instr> dup(const std::string &suffix) const override;
+
+ static bool isDivOrRem(const Op op);
};

MODIFY
ir/state.cpp
ir/state.cpp
@@ -32,6 +32,18 @@ expr State::DomainPreds::operator()() const {
return path() && *UB();
}
+void State::ValueAnalysis::intersect(const State::ValueAnalysis &other) {
+ set<const Value*> results;
+ set_intersection(non_poison_vals.begin(), non_poison_vals.end(),
+ other.non_poison_vals.begin(), other.non_poison_vals.end(),
+ inserter(results, results.begin()));
+ non_poison_vals = move(results);
+}
+
+void State::ValueAnalysis::reset() {
+ non_poison_vals.clear();
+}
+
State::State(Function &f, bool source)
: f(f), source(source), memory(*this),
@@ -60,10 +72,25 @@ const StateValue& State::operator[](const Value &val) {
auto &[sval, uvars] = val_uvars;
(void)var;
+ auto simplify = [&](StateValue &sv, bool use_new_slot) -> StateValue& {
+ if (analysis.non_poison_vals.count(&val)) {
+ if (use_new_slot) {
+ assert(i_tmp_values < tmp_values.size());
+ tmp_values[i_tmp_values++] = sv;
+ }
+ assert(i_tmp_values > 0);
+ StateValue &sv_new = tmp_values[i_tmp_values - 1];
+ const expr &np = sv_new.non_poison;
+ sv_new.non_poison = np.isBool() ? true : expr::mkUInt(0, np.bits());
+ return sv_new;
+ }
+ return sv;
+ };
+
if (uvars.empty() || !used || disable_undef_rewrite) {
used = true;
undef_vars.insert(uvars.begin(), uvars.end());
- return sval;
+ return simplify(sval, true);
}
vector<pair<expr, expr>> repls;
@@ -85,7 +112,8 @@ const StateValue& State::operator[](const Value &val) {
}
assert(i_tmp_values < tmp_values.size());
- return tmp_values[i_tmp_values++] = move(sval_new);
+ tmp_values[i_tmp_values++] = move(sval_new);
+ return simplify(tmp_values[i_tmp_values - 1], false);
}
const StateValue& State::getAndAddUndefs(const Value &val) {
@@ -95,6 +123,18 @@ const StateValue& State::getAndAddUndefs(const Value &val) {
return v;
}
+const StateValue& State::getAndAddPoisonUB(const Value &val) {
+ auto &v = (*this)[val];
+ if (!analysis.non_poison_vals.insert(&val).second)
+ return v;
+
+ // If val is an aggregate, all elements should be non-poison
+ addUB(v.non_poison.isBool() ? v.non_poison : v.non_poison == 0);
+ assert(i_tmp_values < tmp_values.size());
+ return tmp_values[i_tmp_values++] = { expr(v.value),
+ v.non_poison.isBool() ? true : expr::mkUInt(0, v.non_poison.bits()) };
+}
+
const State::ValTy& State::at(const Value &val) const {
return get<1>(values[values_map.at(&val)]);
}
@@ -102,7 +142,7 @@ const State::ValTy& State::at(const Value &val) const {
const OrExpr* State::jumpCondFrom(const BasicBlock &bb) const {
auto &pres = predecessor_data.at(current_bb);
auto I = pres.find(&bb);
- return I == pres.end() ? nullptr : &I->second.first.path;
+ return I == pres.end() ? nullptr : &I->second.domain.path;
}
bool State::isUndef(const expr &e) const {
@@ -115,6 +155,7 @@ bool State::startBB(const BasicBlock &bb) {
current_bb = &bb;
domain.reset();
+ analysis.reset();
if (&f.getFirstBB() == &bb)
return true;
@@ -127,14 +168,21 @@ bool State::startBB(const BasicBlock &bb) {
DisjointExpr<expr> UB;
OrExpr path;
+ bool isFirst = true;
for (auto &[src, data] : I->second) {
(void)src;
- auto &[dom, mem] = data;
+ auto &[dom, anlys, mem] = data;
path.add(dom.path);
expr p = dom.path();
UB.add_disj(dom.UB, p);
in_memory.add_disj(mem, move(p));
domain.undef_vars.insert(dom.undef_vars.begin(), dom.undef_vars.end());
+
+ if (isFirst)
+ analysis = anlys;
+ else
+ analysis.intersect(anlys);
+ isFirst = false;
}
domain.path = path();
@@ -155,12 +203,13 @@ void State::addJump(const BasicBlock &dst0, expr &&cond) {
cond &= domain.path;
auto &data = predecessor_data[dst][current_bb];
- data.second.add(memory, cond);
- data.first.UB.add(domain.UB(), cond);
- data.first.path.add(move(cond));
- data.first.undef_vars.insert(undef_vars.begin(), undef_vars.end());
- data.first.undef_vars.insert(domain.undef_vars.begin(),
+ data.mem.add(memory, cond);
+ data.domain.UB.add(domain.UB(), cond);
+ data.domain.path.add(move(cond));
+ data.domain.undef_vars.insert(undef_vars.begin(), undef_vars.end());
+ data.domain.undef_vars.insert(domain.undef_vars.begin(),
domain.undef_vars.end());
+ data.analysis = analysis;
}
void State::addJump(const BasicBlock &dst) {
@@ -333,7 +382,7 @@ expr State::sinkDomain() const {
OrExpr ret;
for (auto &[src, data] : I->second) {
(void)src;
- ret.add(data.first.path());
+ ret.add(data.domain.path());
}
return ret();
}

MODIFY
ir/state.h
ir/state.h
@@ -47,6 +47,19 @@ private:
smt::expr operator()() const;
};
+ struct ValueAnalysis {
+ std::set<const Value *> non_poison_vals; // vars that are not poison
+
+ void intersect(const ValueAnalysis &other);
+ void reset();
+ };
+
+ struct BasicBlockInfo {
+ DomainPreds domain;
+ ValueAnalysis analysis;
+ smt::DisjointExpr<Memory> mem;
+ };
+
// TODO: make this const again
Function &f;
bool source;
@@ -62,11 +75,9 @@ private:
std::unordered_map<const Value*, unsigned> values_map;
std::vector<std::tuple<const Value*, ValTy, bool>> values;
- // dst BB -> src BB -> (domain data, memory)
- std::unordered_map<const BasicBlock*,
+ // dst BB -> src BB -> BasicBlockInfo
std::unordered_map<const BasicBlock*,
- std::pair<DomainPreds,
- smt::DisjointExpr<Memory>>>>
+ std::unordered_map<const BasicBlock*, BasicBlockInfo>>
predecessor_data;
std::unordered_set<const BasicBlock*> seen_bbs;
@@ -77,6 +88,7 @@ private:
CurrentDomain domain;
Memory memory;
std::set<smt::expr> undef_vars;
+ ValueAnalysis analysis;
std::array<StateValue, 64> tmp_values;
unsigned i_tmp_values = 0; // next available position in tmp_values
@@ -116,6 +128,7 @@ public:
const StateValue& exec(const Value &v);
const StateValue& operator[](const Value &val);
const StateValue& getAndAddUndefs(const Value &val);
+ const StateValue& getAndAddPoisonUB(const Value &val);
const ValTy& at(const Value &val) const;
const smt::OrExpr* jumpCondFrom(const BasicBlock &bb) const;
bool isUndef(const smt::expr &e) const;

Add poison analysis (#472)