stub out trivial implementation of phi
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -226,7 +226,6 @@ StateValue BinOp::toSMT(State &s) const {
val = a.ctlz();
not_poison &= (b == 0u || a != 0u);
break;
-
}
return { move(val), move(not_poison) };
}
@@ -503,8 +502,20 @@ void Phi::print(ostream &os) const {
}
StateValue Phi::toSMT(State &s) const {
- // TODO
- return {};
+ StateValue ret;
+ bool first = true;
+
+ for (auto &[val, bb] : values) {
+ auto v = s[val];
+ if (first) {
+ ret = v;
+ first = false;
+ } else {
+ expr pre = s.jumpCondFrom(s.getFn().getBB(bb));
+ ret = StateValue::mkIf(pre, v, ret);
+ }
+ }
+ return ret;
}
expr Phi::getTypeConstraints(const Function &f) const {

MODIFY
ir/state.cpp
ir/state.cpp
@@ -22,7 +22,7 @@ ostream& operator<<(ostream &os, const StateValue &val) {
}
State::State(const Function &f) : f(f) {
- domain_bbs.try_emplace(&f.getFirstBB(), true, set<expr>());
+ predecessor_domain[&f.getFirstBB()].try_emplace(nullptr, true, set<expr>());
}
const StateValue& State::exec(const Value &v) {
@@ -67,14 +67,28 @@ const State::ValTy& State::at(const Value &val) const {
return values[values_map.at(&val)].second;
}
+const expr& State::jumpCondFrom(const BasicBlock &bb) const {
+ return predecessor_domain.at(current_bb).at(&bb).first;
+}
+
bool State::startBB(const BasicBlock &bb) {
assert(undef_vars.empty());
- seen_bbs.emplace(&bb);
- auto I = domain_bbs.find(&bb);
- if (I == domain_bbs.end())
+ ENSURE(seen_bbs.emplace(&bb).second);
+ current_bb = &bb;
+
+ auto I = predecessor_domain.find(&bb);
+ if (I == predecessor_domain.end())
return false;
- domain = move(I->second);
+ domain.first = false;
+ domain.second.clear();
+
+ for (auto &[src, data] : I->second) {
+ (void)src;
+ auto &[d, vars] = data;
+ domain.first |= d;
+ domain.second.insert(vars.begin(), vars.end());
+ }
return !domain.first.isFalse();
}
@@ -83,7 +97,8 @@ void State::addJump(const BasicBlock &dst, expr &&cond) {
throw LoopInCFGDetected();
cond &= domain.first;
- auto p = domain_bbs.try_emplace(&dst, move(cond), undef_vars);
+ auto p = predecessor_domain[&dst].try_emplace(current_bb, move(cond),
+ undef_vars);
if (!p.second) {
p.first->second.first |= move(cond);
p.first->second.second.insert(undef_vars.begin(), undef_vars.end());

MODIFY
ir/state.h
ir/state.h
@@ -51,19 +51,23 @@ public:
private:
const Function &f;
+ const BasicBlock *current_bb;
std::set<smt::expr> quantified_vars;
// var -> ((value, not_poison), undef_vars)
std::unordered_map<const Value*, unsigned> values_map;
std::vector<std::pair<const Value*, ValTy>> values;
- std::unordered_map<const BasicBlock*, DomainTy> domain_bbs;
+ // dst BB -> src BB -> domain data
+ std::unordered_map<const BasicBlock*,
+ std::unordered_map<const BasicBlock*, DomainTy>>
+ predecessor_domain;
std::unordered_set<const BasicBlock*> seen_bbs;
// temp state
DomainTy domain;
std::set<smt::expr> undef_vars;
- std::array<StateValue, 4> tmp_values;
+ std::array<StateValue, 8> tmp_values;
unsigned i_tmp_values = 0; // next available position in tmp_values
smt::expr return_domain;
@@ -77,6 +81,7 @@ public:
const StateValue& exec(const Value &v);
const StateValue& operator[](const Value &val);
const ValTy& at(const Value &val) const;
+ const smt::expr& jumpCondFrom(const BasicBlock &bb) const;
bool startBB(const BasicBlock &bb);
void addJump(const BasicBlock &dst);

stub out trivial implementation of phi