remove rhs poison expr from div/rem np result expr
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -632,12 +632,12 @@ 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 { move(v), ap && bp && np };
+ return { move(v), ap && (isDivOrRem() ? expr(true) : bp) && np };
};
}
auto &a = s[*lhs];
- auto &b = isDivOrRem(op) ? s.getAndAddPoisonUB(*rhs) : s[*rhs];
+ auto &b = isDivOrRem() ? s.getAndAddPoisonUB(*rhs) : s[*rhs];
if (lhs->getType().isVectorType()) {
auto retty = getType().getAsAggregateType();
@@ -746,7 +746,7 @@ unique_ptr<Instr> BinOp::dup(const string &suffix) const {
fmath);
}
-bool BinOp::isDivOrRem(const Op op) {
+bool BinOp::isDivOrRem() const {
switch (op) {
case Op::SDiv:
case Op::SRem:

MODIFY
ir/instr.h
ir/instr.h
@@ -55,6 +55,7 @@ private:
Op op;
unsigned flags;
FastMathFlags fmath;
+ bool isDivOrRem() const;
public:
BinOp(Type &type, std::string &&name, Value &lhs, Value &rhs, Op op,
@@ -66,8 +67,6 @@ public:
StateValue toSMT(State &s) const override;
smt::expr getTypeConstraints(const Function &f) const override;
std::unique_ptr<Instr> dup(const std::string &suffix) const override;
-
- static bool isDivOrRem(const Op op);
};

remove rhs poison expr from div/rem np result expr