fix optimization for guaranteed non-poison values was broken for vectors
and making all vectors poison after they were proved to be non-poison
so any operation after e.g. a division would be marked as poison
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -193,6 +193,7 @@ void BinOp::print(ostream &os) const {
static void div_ub(State &s, const expr &a, const expr &b, const expr &ap,
const expr &bp, bool sign) {
// addUB(bp) is not needed because it is registered by getAndAddPoisonUB.
+ assert(!bp.isValid() || bp.isTrue());
s.addUB(b != 0);
if (sign)
s.addUB((ap && a != expr::IntSMin(b.bits())) || b != expr::mkInt(-1, b));
@@ -456,7 +457,7 @@ StateValue BinOp::toSMT(State &s) const {
} else {
scalar_op = [&](auto &a, auto &ap, auto &b, auto &bp) -> StateValue {
auto [v, np] = fn(a, ap, b, bp);
- return { std::move(v), ap && (isDivOrRem() ? expr(true) : bp) && np };
+ return { std::move(v), ap && bp && np };
};
}

MODIFY
ir/state.cpp
ir/state.cpp
@@ -409,7 +409,7 @@ const StateValue& State::operator[](const Value &val) {
}
if (is_non_poison) {
const expr &np = sv_new.non_poison;
- sv_new.non_poison = np.isBool() ? true : expr::mkUInt(0, np);
+ sv_new.non_poison = np.isBool() ? true : expr::mkInt(-1, np);
}
return sv_new;
};

MODIFY
ir/value.cpp
ir/value.cpp
@@ -160,7 +160,7 @@ void AggregateValue::print(std::ostream &os) const {
static string attr_str(const ParamAttrs &attr) {
stringstream ss;
ss << attr;
- return ss.str();
+ return std::move(ss).str();
}
Input::Input(Type &type, string &&name, ParamAttrs &&attributes)

ADD
tests/alive-tv/vector/rem.srctgt.ll
+define <2 x i8> @src(<2 x i8> %x) {
+ %rem.i = srem <2 x i8> %x, <i8 2, i8 2>
+ %cmp.i = icmp slt <2 x i8> %rem.i, zeroinitializer
+ %add.i = select <2 x i1> %cmp.i, <2 x i8> <i8 2, i8 2>, <2 x i8> zeroinitializer
+ ret <2 x i8> %add.i
+}
+
+define <2 x i8> @tgt(<2 x i8> %x) {
+ %rem.i = srem <2 x i8> %x, <i8 2, i8 2>
+ %tmp1 = and <2 x i8> %rem.i, <i8 2, i8 2>
+ ret <2 x i8> %tmp1
+}

fix #784: optimization for guaranteed non-poison values was broken for vectors
and making all vectors poison after they were proved to be non-poison
so any operation after e.g. a division would be marked as poison