add Assume instruction
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -495,6 +495,21 @@ expr Return::getTypeConstraints(const Function &f) const {
}
+void Assume::print(ostream &os) const {
+ os << "assume " << cond;
+}
+
+StateValue Assume::toSMT(State &s) const {
+ auto &[v, p] = s[cond];
+ s.addUB(v != 0 && p);
+ return {};
+}
+
+expr Assume::getTypeConstraints(const Function &f) const {
+ return cond.getType().enforceIntType();
+}
+
+
void Unreachable::print(ostream &os) const {
os << "unreachable";
}

MODIFY
ir/instr.h
ir/instr.h
@@ -161,6 +161,17 @@ public:
};
+class Assume final : public Instr {
+ Value &cond;
+public:
+ Assume(Value &cond) : Instr(Type::voidTy, ""), cond(cond) {}
+
+ void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
+ smt::expr getTypeConstraints(const Function &f) const override;
+};
+
+
class Unreachable final : public Instr {
public:
Unreachable() : Instr(Type::voidTy, "") {}

MODIFY
smt/expr.h
smt/expr.h
@@ -162,6 +162,7 @@ public:
expr uge(uint64_t rhs) const { return uge(mkUInt(rhs, bits())); }
expr ugt(uint64_t rhs) const { return ugt(mkUInt(rhs, bits())); }
expr operator==(uint64_t rhs) const { return *this == mkUInt(rhs, bits()); }
+ expr operator!=(uint64_t rhs) const { return *this != mkUInt(rhs, bits()); }
expr sext(unsigned amount) const;
expr zext(unsigned amount) const;

add Assume instruction