funnel shift: Address review notes.
ADD
.clang-format
+---
+Language: Cpp
+BasedOnStyle: LLVM
+AllowShortFunctionsOnASingleLine: Empty
+...

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -309,34 +309,6 @@ void TernaryOp::print(ostream &os) const {
os << getName() << " = " << str << A << ", " << B << ", " << C;
}
-expr TernaryOp::funnelShiftNotPoison(const expr &a, const expr &ap,
- const expr &b, const expr &bp,
- const expr &c, const expr &cp) const {
- assert((op == FShl || op == FShr) && "Only for funnel shift operations.");
-
- expr input_not_poison;
- if (a.eq(b)) {
- assert(ap.eq(bp) && "structurally equivalent expressions have structurally "
- "inequivalent poisonness statuses");
- // If both of the values-to-be-funnel-shifted are identical, then regardless
- // of the shift amt, we'll only propagate the poison status of said value.
- input_not_poison = ap;
- } else {
- // Else, if the values participating in the funnel shift aren't identical,
- // then we need to pay attention to the shift amount.
- auto nbits = c.bits();
- expr c_mod_width = c.urem(expr::mkUInt(nbits, nbits));
- // If the shift amount is zero, then we will only use one of the values,
- // (If it's shift-left, then only 'a', else if shift-right then only 'b')
- // But if shift amount is *not* zero, then we will use both of the values.
- input_not_poison =
- expr::mkIf(c_mod_width == 0u, (op == FShl ? ap : bp), ap && bp);
- }
-
- // But the shift amount must not be poison regardless.
- return input_not_poison && cp;
-}
-
StateValue TernaryOp::toSMT(State &s) const {
auto &[a, ap] = s[A];
auto &[b, bp] = s[B];
@@ -346,9 +318,12 @@ StateValue TernaryOp::toSMT(State &s) const {
switch (op) {
case FShl:
+ newval = expr::fshl(a, b, c);
+ not_poison = ap && bp && cp;
+ break;
case FShr:
- newval = expr::funnelShift(a, b, c, /*is_left_shift=*/op == FShl);
- not_poison = funnelShiftNotPoison(a, ap, b, bp, c, cp);
+ newval = expr::fshr(a, b, c);
+ not_poison = ap && bp && cp;
break;
}

MODIFY
ir/instr.h
ir/instr.h
@@ -67,10 +67,6 @@ private:
Value &A, &B, &C;
Op op;
- smt::expr funnelShiftNotPoison(const smt::expr &a, const smt::expr &ap,
- const smt::expr &b, const smt::expr &bp,
- const smt::expr &c, const smt::expr &cp) const;
-
public:
TernaryOp(Type &type, std::string &&name, Value &A, Value &B, Value &C, Op op)
: Instr(type, std::move(name)), A(A), B(B), C(C), op(op) {}

MODIFY
ir/type.cpp
ir/type.cpp
@@ -77,7 +77,9 @@ expr Type::enforceIntType() const {
return false;
}
-expr Type::enforceIntOrVectorType() const { return false; }
+expr Type::enforceIntOrVectorType() const {
+ return false;
+}
expr Type::enforceIntOrPtrOrVectorType() const {
return false;
@@ -140,7 +142,9 @@ expr IntType::enforceIntType() const {
return true;
}
-expr IntType::enforceIntOrVectorType() const { return true; }
+expr IntType::enforceIntOrVectorType() const {
+ return true;
+}
expr IntType::enforceIntOrPtrOrVectorType() const {
return true;
@@ -185,7 +189,9 @@ void PtrType::fixup(const Model &m) {
// TODO
}
-expr PtrType::enforceIntOrVectorType() const { return false; }
+expr PtrType::enforceIntOrVectorType() const {
+ return false;
+}
expr PtrType::enforceIntOrPtrOrVectorType() const {
return true;
@@ -229,7 +235,9 @@ void VectorType::fixup(const Model &m) {
// TODO
}
-expr VectorType::enforceIntOrVectorType() const { return true; }
+expr VectorType::enforceIntOrVectorType() const {
+ return true;
+}
expr VectorType::enforceIntOrPtrOrVectorType() const {
return true;

MODIFY
smt/expr.cpp
smt/expr.cpp
#include "smt/expr.h"
#include "smt/ctx.h"
#include <cassert>
-#include <limits>
#include <memory>
#include <z3.h>
@@ -512,55 +511,44 @@ expr expr::lshr(const expr &rhs) const {
return Z3_mk_bvlshr(ctx(), ast(), rhs());
}
-expr expr::rotate(const expr &rhs, bool shift_left) const {
- C(rhs);
- if (isZero() || isAllOnes() || rhs.isZero())
- return *this;
+expr expr::fshl(const expr &a, const expr &b, const expr &c) {
+ C2(a, b, c);
- auto nbits = bits();
- expr rhs_mod_width = rhs.urem(mkUInt(nbits, nbits));
- if (rhs_mod_width.isZero())
- return *this;
+ if (c.isZero())
+ return a;
- // FIXME: could do constant-folding, but *only* for i8/i16/i32/i64.
+ auto nbits = a.bits();
+ expr c_mod_width = c.urem(mkUInt(nbits, nbits));
+ if (c_mod_width.isZero())
+ return a;
+
+ // FIXME: could do constant-folding
- uint64_t rhs_mod_width_const;
- if (rhs_mod_width.isUInt(rhs_mod_width_const))
- return shift_left ? Z3_mk_rotate_left(ctx(), rhs_mod_width_const, ast())
- : Z3_mk_rotate_right(ctx(), rhs_mod_width_const, ast());
+ expr res = a.concat(b);
+ expr c_mod_width_zext = c_mod_width.zext(nbits);
+ res = res << c_mod_width_zext;
+ res = res.extract(2 * nbits - 1, nbits); // upper half (MSB)
- return shift_left ? Z3_mk_ext_rotate_left(ctx(), ast(), rhs_mod_width.ast())
- : Z3_mk_ext_rotate_right(ctx(), ast(), rhs_mod_width.ast());
+ return res;
}
-expr expr::funnelShift(const expr &a, const expr &b, const expr &c,
- bool is_left_shift) {
+expr expr::fshr(const expr &a, const expr &b, const expr &c) {
C2(a, b, c);
if (c.isZero())
- return is_left_shift ? a : b;
+ return b;
auto nbits = a.bits();
expr c_mod_width = c.urem(mkUInt(nbits, nbits));
if (c_mod_width.isZero())
- return is_left_shift ? a : b;
+ return b;
- if (a.eq(b))
- return a.rotate(c_mod_width, is_left_shift);
-
- // FIXME: could do constant-folding, but *only* for i8/i16/i32/i64.
+ // FIXME: could do constant-folding
expr res = a.concat(b);
- expr c_mod_width_zext = c_mod_width.zext(res.bits() - c_mod_width.bits());
- res = is_left_shift ? res << c_mod_width_zext : res.lshr(c_mod_width_zext);
-
- unsigned high = nbits - 1;
- unsigned low = 0;
- if (is_left_shift) {
- high += nbits;
- low += nbits;
- }
- res = res.extract(high, low); // FIXME: would be nicer to pass {offset, len}
+ expr c_mod_width_zext = c_mod_width.zext(nbits);
+ res = res.lshr(c_mod_width_zext);
+ res = res.extract(nbits - 1, 0); // lower half (LSB)
return res;
}

MODIFY
smt/expr.h
smt/expr.h
@@ -125,10 +125,8 @@ public:
expr ashr(const expr &rhs) const;
expr lshr(const expr &rhs) const;
- expr rotate(const expr &rhs, bool shift_left) const;
-
- static expr funnelShift(const expr &a, const expr &b, const expr &c,
- bool is_left_shift);
+ static expr fshl(const expr &a, const expr &b, const expr &c);
+ static expr fshr(const expr &a, const expr &b, const expr &c);
expr shl_no_soverflow(const expr &rhs) const;
expr shl_no_uoverflow(const expr &rhs) const;

MODIFY
tests/unit/fshl/poison-6.opt
tests/unit/fshl/poison-6.opt
%b = poison
%t = poison
%r = select i8 %c_is_zero, i8 poison, i8 %z
-
-; ERROR: Target is more poisonous than source for i8 %t

MODIFY
tests/unit/fshl/poison-7.opt
tests/unit/fshl/poison-7.opt
%b = poison
%t = poison
%r = select i8 %c_is_seven, i8 %t, i8 %z
-
-; ERROR: Target is more poisonous than source for i8 %t
-
-; FIXME: XFAIL. this is a false-negative.
-; We used both %b (which is poison) and %a, so the result should be poison.
-; poison-7-v2.opt agrees.

MODIFY
tests/unit/fshl/poison-8.opt
tests/unit/fshl/poison-8.opt
%b = poison
%t = poison
%r = select i8 %c_is_eight, i8 poison, i8 %z
-
-; ERROR: Target is more poisonous than source for i8 %t

MODIFY
tests/unit/fshr/poison-3.opt
tests/unit/fshr/poison-3.opt
%a = poison
%t = poison
%r = select i8 %c_is_zero, i8 poison, i8 %z
-
-; ERROR: Target is more poisonous than source for i8 %t

MODIFY
tests/unit/fshr/poison-4.opt
tests/unit/fshr/poison-4.opt
%a = poison
%t = poison
%r = select i8 %c_is_seven, i8 poison, i8 %z
-
-; ERROR: Target is more poisonous than source for i8 %t
-
-; FIXME: XFAIL. this is a false-negative.
-; We used both %b (which is poison) and %a, so the result should be poison.
-; poison-4-v2.opt agrees.

MODIFY
tests/unit/fshr/poison-5.opt
tests/unit/fshr/poison-5.opt
%a = poison
%t = poison
%r = select i8 %c_is_eight, i8 poison, i8 %z
-
-; ERROR: Target is more poisonous than source for i8 %t

funnel shift: Address review notes.