fix crash with switch with a must-branch case
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2928,8 +2928,7 @@ StateValue Switch::toSMT(State &s) const {
s.addJump(std::move(cmp), *bb);
}
- s.addJump(std::move(default_cond), *default_target);
- s.addUB(expr(false));
+ s.addJump(std::move(default_cond), *default_target, true);
return {};
}

MODIFY
ir/state.cpp
ir/state.cpp
@@ -668,10 +668,10 @@ bool State::startBB(const BasicBlock &bb) {
}
void State::addJump(const BasicBlock &dst0, expr &&cond, bool always_jump) {
- always_jump = always_jump || cond.isTrue();
+ always_jump |= cond.isTrue();
cond &= domain.path;
- if (cond.isFalse())
+ if (cond.isFalse() || !domain)
return;
auto dst = &dst0;
@@ -693,15 +693,17 @@ void State::addJump(const BasicBlock &dst0, expr &&cond, bool always_jump) {
data.path.add(std::move(cond));
data.undef_vars.insert(undef_vars.begin(), undef_vars.end());
data.undef_vars.insert(domain.undef_vars.begin(), domain.undef_vars.end());
+
+ if (always_jump)
+ addUB(expr(false));
}
void State::addJump(const BasicBlock &dst) {
addJump(dst, true, true);
- addUB(expr(false));
}
-void State::addJump(expr &&cond, const BasicBlock &dst) {
- addJump(dst, std::move(cond));
+void State::addJump(expr &&cond, const BasicBlock &dst, bool last_jump) {
+ addJump(dst, std::move(cond), last_jump);
}
void State::addCondJump(const expr &cond, const BasicBlock &dst_true,

MODIFY
ir/state.h
ir/state.h
@@ -215,7 +215,7 @@ public:
bool startBB(const BasicBlock &bb);
void addJump(const BasicBlock &dst);
// boolean cond
- void addJump(smt::expr &&cond, const BasicBlock &dst);
+ void addJump(smt::expr &&cond, const BasicBlock &dst, bool last_jump = false);
// i1 cond
void addCondJump(const smt::expr &cond, const BasicBlock &dst_true,
const BasicBlock &dst_false);

ADD
tests/alive-tv/loops/switch-unreach.srctgt.ll
+declare void @c1()
+
+define i8 @src(i8 %spec.select) {
+ br label %4
+
+1:
+ call void @c1()
+ br label %3
+
+.unreachabledefault:
+ unreachable
+
+2:
+ ret i8 0
+
+3:
+ %.2 = phi i8 [ 0, %1 ], [ %.48, %4 ]
+ switch i8 %.2, label %4 [
+ i8 0, label %1
+ i8 1, label %2
+ ]
+
+4:
+ %.48 = phi i8 [ 0, %3 ], [ %spec.select, %0 ]
+ switch i8 %.48, label %.unreachabledefault [
+ i8 0, label %3
+ i8 1, label %1
+ ]
+}
+
+define i8 @tgt(i8 %spec.select) {
+ br label %1
+
+1:
+ call void @c1()
+ br label %1
+}

fix #872: crash with switch with a must-branch case