shufflevector: change sema to match LangRef's mask undef detection
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2089,14 +2089,31 @@ StateValue ShuffleVector::toSMT(State &s) const {
auto mty = mask->getType().getAsAggregateType();
vector<StateValue> vals;
+ auto &vect1 = s[*v1];
+ auto &vect2 = s[*v2];
+ auto &mask_vector = static_cast<AggregateConst*>(mask)->getVals();
+
for (unsigned i = 0, e = mty->numElementsConst(); i != e; ++i) {
- auto [iv, ip] = mty->extract(s[*mask], i);
- auto [lv, lp] = vty->extract(s[*v1], iv);
- auto [rv, rp] = vty->extract(s[*v2], iv - sz);
- expr v = expr::mkIf(iv.uge(sz), rv, lv);
- expr np = expr::mkIf(iv.uge(sz), rp, lp);
+ auto mask = mask_vector[i];
+ // mask must be either a constant or undef
+ // special case undef to yield undef
+ if (dynamic_cast<UndefValue*>(mask)) {
+ vals.emplace_back(UndefValue(vty->getChild(0)).toSMT(s));
+ continue;
+ }
+
+ auto &[iv, ip] = s[*mask];
+ assert(ip.isTrue());
+ auto [lv, lp] = vty->extract(vect1, iv);
+ auto [rv, rp] = vty->extract(vect2, iv - sz);
+
+ expr val = expr::mkIf(iv.uge(sz), rv, lv);
expr inbounds = iv.ult(sz + sz);
- vals.emplace_back(move(v), ip && inbounds && np);
+ if (!inbounds.isTrue())
+ val = expr::mkIf(inbounds, val,
+ UndefValue(vty->getChild(0)).toSMT(s).value);
+
+ vals.emplace_back(move(val), !inbounds || expr::mkIf(iv.uge(sz), rp, lp));
}
return getType().getAsAggregateType()->aggregateVals(vals);

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -398,6 +398,7 @@ expr expr::binop_commutative(const expr &rhs,
expr expr::binop_commutative(const expr &rhs,
Z3_ast(*op)(Z3_context, Z3_ast, Z3_ast)) const {
+ assert(!isValid() || !rhs.isValid() || sort() == rhs.sort());
auto cmp = *this < rhs;
return (cmp ? *this : rhs).binop_fold(cmp ? rhs : *this, op);
}

MODIFY
tests/unit/vector/shufflevector1.opt
tests/unit/vector/shufflevector1.opt
@@ -46,12 +46,12 @@ Name: constant-folding-8
Name: constant-folding-9
-%r = shufflevector <2 x i4> <i4 3, i4 5>, <2 x i4> <i4 4, i4 6>, <3 x i32> <i32 poison, i32 1, i32 4>
+%r = shufflevector <2 x i4> <i4 3, i4 5>, <2 x i4> <i4 4, i4 6>, <3 x i32> <i32 undef, i32 1, i32 4>
=>
-%r = <3 x i4> <i4 poison, i4 5, i4 poison>
+%r = <3 x i4> <i4 undef, i4 5, i4 undef>
Name: constant-folding-10
-%r = shufflevector <2 x float> <float 3.0, float 5.0>, <2 x float> <float 4.0, float 6.0>, <3 x i32> <i32 poison, i32 1, i32 4>
+%r = shufflevector <2 x float> <float 3.0, float 5.0>, <2 x float> <float 4.0, float 6.0>, <3 x i32> <i32 undef, i32 1, i32 4>
=>
-%r = <3 x float> <float poison, float 5.0, float poison>
+%r = <3 x float> <float undef, float 5.0, float undef>

shufflevector: change sema to match LangRef's mask undef detection