recognize add pattern in strip_undef_and_add_ub
MODIFY
ir/state.cpp
ir/state.cpp
@@ -151,6 +151,31 @@ expr State::strip_undef_and_add_ub(const Value &val, const expr &e) {
is_undef_cond(not_undef, var);
};
+ // e2: stripped expression
+ auto is_if_undef_or_add = [&](const expr &e, expr &var, expr &not_undef,
+ expr &e2) {
+ // when e = (ite (= #b0 isundef_%var) %var undef):
+ // var = %var, e2 = %var
+ // when e = (bvadd const (ite (= #b0 isundef_%var) %var undef))
+ // var = %var, e2 = const + %var
+ if (is_if_undef(e, var, not_undef)) {
+ e2 = var;
+ return true;
+ }
+
+ expr a, b;
+ if (e.isAdd(a, b)) {
+ if (b.isConst() && is_if_undef(a, var, not_undef)) {
+ e2 = b + var;
+ return true;
+ } else if (a.isConst() && is_if_undef(b, var, not_undef)) {
+ e2 = a + var;
+ return true;
+ }
+ }
+ return false;
+ };
+
expr c, a, b, lhs, rhs;
// two variants
@@ -177,76 +202,99 @@ expr State::strip_undef_and_add_ub(const Value &val, const expr &e) {
};
if (e.isIf(c, a, b) && a.isConst() && b.isConst()) {
- expr val, val2, not_undef, not_undef2;
+ expr val, val2, newe, newe2, not_undef, not_undef2;
// (ite (= val (ite (= #b0 isundef_%var) %var undef)) #b1 #b0)
+ // (ite (= val (bvadd c (ite (= #b0 isundef_%var) %var undef)) #b1 #b0)
if (c.isEq(lhs, rhs)) {
- if (is_if_undef(lhs, val, not_undef) && !has_undef(rhs)) {
+ if (is_if_undef_or_add(lhs, val, not_undef, newe) && !has_undef(rhs)) {
addUB(move(not_undef));
mark_notundef(val);
- return expr::mkIf(val == rhs, a, b);
+ // %var == rhs
+ // (bvadd c %var) == rhs
+ return expr::mkIf(newe == rhs, a, b);
}
- if (is_if_undef(rhs, val, not_undef) && !has_undef(lhs)) {
+ if (is_if_undef_or_add(rhs, val, not_undef, newe) && !has_undef(lhs)) {
addUB(move(not_undef));
mark_notundef(val);
- return expr::mkIf(lhs == val, a, b);
+ return expr::mkIf(lhs == newe, a, b);
}
- if (is_if_undef(lhs, val, not_undef) &&
- is_if_undef(rhs, val2, not_undef2)) {
+ if (is_if_undef_or_add(lhs, val, not_undef, newe) &&
+ is_if_undef_or_add(rhs, val2, not_undef2, newe2)) {
addUB(move(not_undef));
addUB(move(not_undef2));
mark_notundef(val);
mark_notundef(val2);
- return expr::mkIf(val == val2, a, b);
+ return expr::mkIf(newe == newe2, a, b);
}
}
if (c.isSLE(lhs, rhs)) {
// (ite (bvsle val (ite (= #b0 isundef_%var) %var undef)) #b1 #b0)
- if (is_if_undef(rhs, val, not_undef) && !has_undef(lhs)) {
- addUB(not_undef || lhs == expr::IntSMin(lhs.bits()));
+ // (ite (bvsle val (bvadd c (ite (= #b0 isundef_%var) %var undef))
+ // #b1 #b0)
+ if (is_if_undef_or_add(rhs, val, not_undef, newe) && !has_undef(lhs)) {
+ expr cond = lhs == expr::IntSMin(lhs.bits());
+ addUB(not_undef || cond);
+ if (cond.isFalse())
mark_notundef(val);
- return expr::mkIf(lhs.sle(val), a, b);
+ // lhs <=s %var
+ // lhs <=s (bvadd c %var)
+ return expr::mkIf(lhs.sle(newe), a, b);
}
// (ite (bvsle (ite (= #b0 isundef_%var) %var undef) val) #b1 #b0)
- if (is_if_undef(lhs, val, not_undef) && !has_undef(rhs)) {
- addUB(not_undef || rhs == expr::IntSMax(rhs.bits()));
+ // (ite (bvsle (bvadd c (ite (= #b0 isundef_%var) %var undef)) val)
+ // #b1 #b0)
+ if (is_if_undef_or_add(lhs, val, not_undef, newe) && !has_undef(rhs)) {
+ expr cond = rhs == expr::IntSMax(rhs.bits());
+ addUB(not_undef || cond);
+ if (cond.isFalse())
mark_notundef(val);
- return expr::mkIf(val.sle(rhs), a, b);
+ return expr::mkIf(newe.sle(rhs), a, b);
}
// undef <= undef
- if (is_if_undef(lhs, val, not_undef) &&
- is_if_undef(rhs, val2, not_undef2)) {
+ if (is_if_undef_or_add(lhs, val, not_undef, newe) &&
+ is_if_undef_or_add(rhs, val2, not_undef2, newe2)) {
addUB((not_undef && not_undef2) ||
- (not_undef && val == expr::IntSMin(lhs.bits())) ||
- (not_undef2 && val2 == expr::IntSMax(rhs.bits())));
- return expr::mkIf(val.sle(val2), a, b);
+ (not_undef && newe == expr::IntSMin(lhs.bits())) ||
+ (not_undef2 && newe2 == expr::IntSMax(rhs.bits())));
+ return expr::mkIf(newe.sle(newe2), a, b);
}
}
if (c.isULE(lhs, rhs)) {
// (ite (bvule val (ite (= #b0 isundef_%var) %var undef)) #b1 #b0)
- if (is_if_undef(rhs, val, not_undef) && !has_undef(lhs)) {
- addUB(not_undef || lhs == 0);
+ // (ite (bvule val (bvadd c (ite (= #b0 isundef_%var) %var undef)))
+ // #b1 #b0)
+ if (is_if_undef_or_add(rhs, val, not_undef, newe) && !has_undef(lhs)) {
+ expr cond = lhs == 0;
+ addUB(not_undef || cond);
+ if (cond.isFalse())
mark_notundef(val);
- return expr::mkIf(lhs.ule(val), a, b);
+ // lhs <=u %var
+ // lhs <=u (bvadd c %var)
+ return expr::mkIf(lhs.ule(newe), a, b);
}
// (ite (bvule (ite (= #b0 isundef_%var) %var undef) val) #b1 #b0)
- if (is_if_undef(lhs, val, not_undef) && !has_undef(rhs)) {
- addUB(not_undef || rhs == expr::mkInt(-1, rhs));
+ // (ite (bvule (bvadd c (ite (= #b0 isundef_%var) %var undef)) %val)
+ // #b1 #b0)
+ if (is_if_undef_or_add(lhs, val, not_undef, newe) && !has_undef(rhs)) {
+ expr cond = rhs == expr::mkInt(-1, rhs);
+ addUB(not_undef || cond);
+ if (cond.isFalse())
mark_notundef(val);
- return expr::mkIf(val.ule(rhs), a, b);
+ return expr::mkIf(newe.ule(rhs), a, b);
}
// undef <= undef
- if (is_if_undef(lhs, val, not_undef) &&
- is_if_undef(rhs, val2, not_undef2)) {
+ if (is_if_undef_or_add(lhs, val, not_undef, newe) &&
+ is_if_undef_or_add(rhs, val2, not_undef2, newe2)) {
addUB((not_undef && not_undef2) ||
- (not_undef && val == 0) ||
- (not_undef2 && val2 == expr::mkInt(-1, rhs)));
- return expr::mkIf(val.ule(val2), a, b);
+ (not_undef && newe == 0) ||
+ (not_undef2 && newe2 == expr::mkInt(-1, rhs)));
+ return expr::mkIf(newe.ule(newe2), a, b);
}
}
}

ADD
tests/alive-tv/undef/strip-add-eq.srctgt.ll
+; TEST-ARGS: -se-verbose
+define i32 @src(i32 %x) {
+ %v = add i32 %x, 1
+ %c = icmp eq i32 %x, 5
+ br i1 %c, label %A, label %B
+A:
+ ret i32 %x
+B:
+ ret i32 %x
+}
+
+define i32 @tgt(i32 %x) {
+ %v = add i32 %x, 1
+ %c = icmp eq i32 %x, 5
+ br i1 %c, label %A, label %B
+A:
+ ret i32 %x
+B:
+ ret i32 %x
+}
+
+; CHECK: return = %x / true

ADD
tests/alive-tv/undef/strip-add-ule.srctgt.ll
+define i32 @src(i32 %x) {
+ %c = icmp ule i32 0, %x
+ br i1 %c, label %A, label %B
+A:
+ %x.fr = freeze i32 %x
+ ret i32 %x.fr
+B:
+ ret i32 0
+}
+
+define i32 @tgt(i32 %x) {
+ %c = icmp ule i32 0, %x
+ br i1 %c, label %A, label %B
+A:
+ ret i32 %x
+B:
+ ret i32 0
+}
+
+; ERROR: Target's return value is more undefined

recognize add pattern in strip_undef_and_add_ub (#523)