fix bug in range metadata with poison values
introduce a flag in assume instr to state that it only holds if input is non poison
fixes bug
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -568,12 +568,15 @@ expr Return::getTypeConstraints(const Function &f) const {
void Assume::print(ostream &os) const {
- os << "assume " << cond;
+ os << (if_non_poison ? "assume_non_poison " : "assume ") << cond;
}
StateValue Assume::toSMT(State &s) const {
- auto &[v, p] = s[cond];
- s.addUB(v != 0 && p);
+ auto &[v, np] = s[cond];
+ if (if_non_poison)
+ s.addUB(np.implies(v != 0));
+ else
+ s.addUB(np && v != 0);
return {};
}

MODIFY
ir/instr.h
ir/instr.h
@@ -180,8 +180,10 @@ public:
class Assume final : public Instr {
Value &cond;
+ bool if_non_poison; /// cond only needs to hold if non-poison
public:
- Assume(Value &cond) : Instr(Type::voidTy, ""), cond(cond) {}
+ Assume(Value &cond, bool if_non_poison)
+ : Instr(Type::voidTy, ""), cond(cond), if_non_poison(if_non_poison) {}
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;

MODIFY
tv/tv.cpp
tv/tv.cpp
@@ -387,7 +387,7 @@ public:
}
if (range)
- BB.addInstr(make_unique<Assume>(*range));
+ BB.addInstr(make_unique<Assume>(*range, true));
break;
}
default:

fix bug in range metadata with poison values
introduce a flag in assume instr to state that it only holds if input is non poison
fixes bug #35