add switch instruction
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -442,6 +442,43 @@ expr Branch::getTypeConstraints(const Function &f) const {
}
+void Switch::addTarget(Value &val, const BasicBlock &target) {
+ targets.emplace_back(val, target);
+}
+
+void Switch::print(ostream &os) const {
+ os << "switch " << value << ", label " << default_target.getName() << " [\n";
+ for (auto &[val, target] : targets) {
+ os << " " << val << ", label " << target.getName() << '\n';
+ }
+ os << "]";
+}
+
+StateValue Switch::toSMT(State &s) const {
+ auto val = s[value];
+ expr default_cond(true);
+
+ for (auto &p : targets) {
+ auto target = s[p.first];
+ assert(target.non_poison.isTrue());
+ s.addJump({ val.value == target.value, expr(val.non_poison) }, p.second);
+ default_cond &= val.value != target.value;
+ }
+
+ s.addJump({ move(default_cond), move(val.non_poison) }, default_target);
+ s.addUB(false);
+ return {};
+}
+
+expr Switch::getTypeConstraints(const Function &f) const {
+ expr typ = value.getType().enforceIntType();
+ for (auto &p : targets) {
+ typ &= p.first.getType().enforceIntType();
+ }
+ return typ;
+}
+
+
void Return::print(ostream &os) const {
os << "ret " << val;
}

MODIFY
ir/instr.h
ir/instr.h
@@ -132,6 +132,24 @@ public:
};
+class Switch final : public Instr {
+ Value &value;
+ const BasicBlock &default_target;
+ std::vector<std::pair<Value&, const BasicBlock&>> targets;
+
+public:
+ Switch(Value &value, const BasicBlock &default_target)
+ : Instr(Type::voidTy, "switch"), value(value),
+ default_target(default_target) {}
+
+ void addTarget(Value &val, const BasicBlock &target);
+
+ 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
@@ -109,6 +109,10 @@ void State::addJump(const BasicBlock &dst) {
domain = false;
}
+void State::addJump(StateValue &&cond, const BasicBlock &dst) {
+ addJump(dst, move(cond.value) && move(cond.non_poison));
+}
+
void State::addCondJump(const StateValue &cond, const BasicBlock &dst_true,
const BasicBlock &dst_false) {
addJump(dst_true, cond.value == 1 && cond.non_poison);

MODIFY
ir/state.h
ir/state.h
@@ -66,6 +66,9 @@ public:
bool startBB(const BasicBlock &bb);
void addJump(const BasicBlock &dst);
+ // boolean cond
+ void addJump(StateValue &&cond, const BasicBlock &dst);
+ // i1 cond
void addCondJump(const StateValue &cond, const BasicBlock &dst_true,
const BasicBlock &dst_false);
void addReturn(const StateValue &val);

add switch instruction