add Branch instruction
MODIFY
ir/function.h
ir/function.h
@@ -29,6 +29,8 @@ public:
BasicBlock(std::string &&name) : name(std::move(name)) {}
BasicBlock(std::string_view name) : name(name) {}
+ const std::string& getName() const { return name; }
+
smt::expr getTypeConstraints(const Function &f) const;
void fixupTypes(const smt::Model &m);

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -394,6 +394,30 @@ expr CopyOp::getTypeConstraints(const Function &f) const {
}
+void Branch::print(ostream &os) const {
+ os << "br ";
+ if (cond)
+ os << *cond << ", ";
+ os << "label " << dst_true.getName();
+ if (dst_false)
+ os << ", label " << dst_false->getName();
+}
+
+StateValue Branch::toSMT(State &s) const {
+ if (cond) {
+ s.addCondJump(s[*cond], dst_true, *dst_false);
+ } else {
+ s.addJump(dst_true);
+ }
+ return {};
+}
+
+expr Branch::getTypeConstraints(const Function &f) const {
+ return cond->getType().enforceIntType() &&
+ cond->getType().sizeVar() == 1u;
+}
+
+
void Return::print(ostream &os) const {
os << "ret " << val;
}

MODIFY
ir/instr.h
ir/instr.h
@@ -115,6 +115,22 @@ public:
};
+class Branch final : public Instr {
+ Value *cond = nullptr;
+ const BasicBlock &dst_true, *dst_false = nullptr;
+public:
+ Branch(const BasicBlock &dst) : Instr(Type::voidTy, "br"), dst_true(dst) {}
+
+ Branch(Value &cond, const BasicBlock &dst_true, const BasicBlock &dst_false)
+ : Instr(Type::voidTy, "br"), cond(&cond), dst_true(dst_true),
+ dst_false(&dst_false) {}
+
+ void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
+ smt::expr getTypeConstraints(const Function &f) const override;
+};
+
+
class Return final : public Instr {
Value &val;
public:

MODIFY
ir/state.cpp
ir/state.cpp
@@ -94,10 +94,22 @@ bool State::startBB(const BasicBlock &bb) {
return !domain.isFalse();
}
-void State::addJump(const BasicBlock &bb) {
- auto p = domain_bbs.try_emplace(&bb, domain);
+void State::addJump(const BasicBlock &dst, expr &&domain) {
+ auto p = domain_bbs.try_emplace(&dst, move(domain));
if (!p.second)
- p.first->second |= domain;
+ p.first->second |= move(domain);
+}
+
+void State::addJump(const BasicBlock &dst) {
+ addJump(dst, expr(domain));
+ domain = false;
+}
+
+void State::addCondJump(const StateValue &cond, const BasicBlock &dst_true,
+ const BasicBlock &dst_false) {
+ addJump(dst_true, cond.value && cond.non_poison);
+ addJump(dst_false, !cond.value && cond.non_poison);
+ domain = false;
}
void State::addReturn(const StateValue &val) {
@@ -111,6 +123,7 @@ void State::addReturn(const StateValue &val) {
return_domain = domain;
return_val = { val, move(undef_vars) };
}
+ domain = false;
}
void State::addQuantVar(const expr &var) {

MODIFY
ir/state.h
ir/state.h
@@ -64,7 +64,9 @@ public:
const ValTy& at(const Value &val) const;
bool startBB(const BasicBlock &bb);
- void addJump(const BasicBlock &bb);
+ void addJump(const BasicBlock &dst);
+ void addCondJump(const StateValue &cond, const BasicBlock &dst_true,
+ const BasicBlock &dst_false);
void addReturn(const StateValue &val);
void addUB(smt::expr &&ub) { domain &= std::move(ub); }
void addUB(const smt::expr &ub) { domain &= ub; }
@@ -79,6 +81,9 @@ public:
bool fnReturned() const { return returned; }
auto& returnDomain() const { return return_domain; }
auto& returnVal() const { return return_val; }
+
+private:
+ void addJump(const BasicBlock &dst, smt::expr &&domain);
};
}

add Branch instruction