make 'br undef' UB
MODIFY
ir/globals.cpp
ir/globals.cpp
@@ -43,4 +43,11 @@ bool isUndef(const expr &e) {
return string_view(name).substr(0, 6) == "undef!";
}
+bool isTyVar(const expr &ty, const expr &var) {
+ auto ty_name = ty.fn_name();
+ auto var_name = var.fn_name();
+ return string_view(ty_name).substr(0, 3) == "ty_" &&
+ string_view(ty_name).substr(3) == var_name;
+}
+
}

MODIFY
ir/globals.h
ir/globals.h
@@ -71,5 +71,6 @@ extern unsigned heap_block_alignment;
bool isUndef(const smt::expr &e);
+bool isTyVar(const smt::expr &ty, const smt::expr &var);
}

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1627,9 +1627,35 @@ void Branch::print(ostream &os) const {
os << ", label " << dst_false->getName();
}
+static pair<expr,expr> // <condition, not_undef>
+jump_undef_condition(State &s, const Value &val, const expr &e) {
+ if (isUndef(e))
+ return { expr::mkUInt(0, 1), false };
+
+ expr c, a, b, lhs, rhs, ty;
+ unsigned h, l;
+ uint64_t n;
+
+ // (ite (= ((_ extract 0 0) ty_%var) #b0) %var undef!0)
+ if (e.isIf(c, a, b) && isUndef(b) && c.isEq(lhs, rhs)) {
+ if (lhs.isUInt(n))
+ swap(lhs, rhs);
+
+ if (rhs.isUInt(n) && n == 0 &&
+ lhs.isExtract(ty, h, l) && h == 0 && l == 0 && isTyVar(ty, a))
+ return { move(a), c };
+ }
+
+ return { e, e == s[val].value };
+}
+
StateValue Branch::toSMT(State &s) const {
if (cond) {
- s.addCondJump(s[*cond], dst_true, *dst_false);
+ auto &c = s[*cond];
+ auto [cond_val, not_undef] = jump_undef_condition(s, *cond, c.value);
+ s.addUB(c.non_poison);
+ s.addUB(not_undef);
+ s.addCondJump(cond_val, dst_true, *dst_false);
} else {
s.addJump(dst_true);
}
@@ -1682,14 +1708,19 @@ StateValue Switch::toSMT(State &s) const {
auto &val = s[*value];
expr default_cond(true);
+ auto [cond_val, not_undef] = jump_undef_condition(s, *value, val.value);
+ s.addUB(val.non_poison);
+ s.addUB(not_undef);
+
for (auto &[value_cond, bb] : targets) {
auto &target = s[*value_cond];
assert(target.non_poison.isTrue());
- s.addJump({ val.value == target.value, expr(val.non_poison) }, bb);
- default_cond &= val.value != target.value;
+ expr cmp = cond_val == target.value;
+ default_cond &= !cmp;
+ s.addJump(move(cmp), bb);
}
- s.addJump({ move(default_cond), expr(val.non_poison) }, default_target);
+ s.addJump(move(default_cond), default_target);
s.addUB(expr(false));
return {};
}

MODIFY
ir/state.cpp
ir/state.cpp
@@ -163,16 +163,14 @@ void State::addJump(const BasicBlock &dst) {
addUB(expr(false));
}
-void State::addJump(StateValue &&cond, const BasicBlock &dst) {
- addUB(move(cond.non_poison));
- addJump(dst, move(cond.value));
+void State::addJump(expr &&cond, const BasicBlock &dst) {
+ addJump(dst, move(cond));
}
-void State::addCondJump(const StateValue &cond, const BasicBlock &dst_true,
+void State::addCondJump(const expr &cond, const BasicBlock &dst_true,
const BasicBlock &dst_false) {
- addUB(cond.non_poison);
- addJump(dst_true, cond.value == 1);
- addJump(dst_false, cond.value == 0);
+ addJump(dst_true, cond == 1);
+ addJump(dst_false, cond == 0);
addUB(expr(false));
}
@@ -188,11 +186,13 @@ void State::addReturn(const StateValue &val) {
void State::addUB(expr &&ub) {
domain.UB.add(move(ub));
+ if (!ub.isConst())
domain.undef_vars.insert(undef_vars.begin(), undef_vars.end());
}
void State::addUB(const expr &ub) {
domain.UB.add(ub);
+ if (!ub.isConst())
domain.undef_vars.insert(undef_vars.begin(), undef_vars.end());
}

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

ADD
tests/alive-tv/br-undef.srctgt.ll
+define i8 @src() {
+ br i1 undef, label %a, label %b
+
+a:
+ ret i8 0
+
+b:
+ ret i8 3
+}
+
+define i8 @tgt() {
+ unreachable
+}

ADD
tests/alive-tv/br-undef2.srctgt.ll
+define i8 @src(i1 %c) {
+ br i1 %c, label %a, label %b
+
+a:
+ ret i8 1
+
+b:
+ ret i8 0
+}
+
+define i8 @tgt(i1 %c) {
+ %ext = zext i1 %c to i8
+ ret i8 %ext
+}

make 'br undef' UB