add support for icmp
MODIFY
ir/instr.cpp
ir/instr.cpp
#include "ir/instr.h"
#include "smt/expr.h"
+#include "smt/solver.h"
#include "util/compiler.h"
using namespace smt;
@@ -279,6 +280,66 @@ expr Select::getTypeConstraints() const {
}
+ICmp::ICmp(std::string &&name, Cond cond, Value &a, Value &b) :
+ Instr(make_unique<IntType>(1), move(name)), a(a), b(b), cond(cond) {
+ a.getWType().enforceIntOrPtrOrVectorType();
+ b.getWType().enforceIntOrPtrOrVectorType();
+
+ auto str = getName() + "_cond";
+ cond_var = expr::mkVar(str.c_str(), 4);
+}
+
+void ICmp::print(ostream &os) const {
+ const char *condtxt = nullptr;
+ switch (cond) {
+ case EQ: condtxt = "eq "; break;
+ case NE: condtxt = "ne "; break;
+ case SLE: condtxt = "sle "; break;
+ case SLT: condtxt = "slt "; break;
+ case SGE: condtxt = "sge "; break;
+ case SGT: condtxt = "sgt "; break;
+ case ULE: condtxt = "ule "; break;
+ case ULT: condtxt = "ult "; break;
+ case UGE: condtxt = "uge "; break;
+ case UGT: condtxt = "ugt "; break;
+ case Any: condtxt = " "; break;
+ }
+ os << getName() << " = icmp " << condtxt << a << ", " << b.getName();
+}
+
+StateValue ICmp::toSMT(State &s) const {
+ auto &[av, ap] = s[a];
+ auto &[bv, bp] = s[b];
+ expr val;
+ switch (cond) {
+ case EQ: val = av == bv; break;
+ case NE: val = av != bv; break;
+ case SLE: val = av.sle(bv); break;
+ case SLT: val = av.slt(bv); break;
+ case SGE: val = av.sge(bv); break;
+ case SGT: val = av.sgt(bv); break;
+ case ULE: val = av.ule(bv); break;
+ case ULT: val = av.ult(bv); break;
+ case UGE: val = av.uge(bv); break;
+ case UGT: val = av.ugt(bv); break;
+ case Any:
+ UNREACHABLE();
+ }
+ return { expr::mkIf(val, expr::mkUInt(1,1), expr::mkUInt(0,1)), ap && bp };
+}
+
+expr ICmp::getTypeConstraints() const {
+ return a.getTypeConstraints() &&
+ a.getType() == b.getType() &&
+ (cond == Any ? cond_var.ule(expr::mkUInt(9, 4))
+ : cond_var == expr::mkUInt(cond, 4));
+}
+
+void ICmp::fixupTypes(const Model &m) {
+ cond = (Cond)m.getUInt(cond_var);
+}
+
+
void Return::print(ostream &os) const {
os << "ret " << val;
}

MODIFY
ir/instr.h
ir/instr.h
@@ -64,6 +64,24 @@ public:
};
+class ICmp final : public Instr {
+public:
+ enum Cond { EQ, NE, SLE, SLT, SGE, SGT, ULE, ULT, UGE, UGT, Any };
+
+private:
+ Value &a, &b;
+ smt::expr cond_var;
+ Cond cond;
+
+public:
+ ICmp(std::string &&name, Cond cond, Value &a, Value &b);
+ void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
+ smt::expr getTypeConstraints() const override;
+ void fixupTypes(const smt::Model &m) override;
+};
+
+
class Return final : public Instr {
Value &val;
public:

MODIFY
ir/value.h
ir/value.h
@@ -31,7 +31,7 @@ public:
virtual void print(std::ostream &os) const = 0;
virtual StateValue toSMT(State &s) const = 0;
virtual smt::expr getTypeConstraints() const = 0;
- void fixupTypes(const smt::Model &m);
+ virtual void fixupTypes(const smt::Model &m);
virtual ~Value();
friend std::ostream& operator<<(std::ostream &os, const Value &val);

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -126,6 +126,14 @@ Z3_app expr::isApp() const {
return nullptr;
}
+Z3_app expr::isAppOf(int app_type) const {
+ auto app = isApp();
+ if (!app)
+ return nullptr;
+ auto decl = Z3_get_app_decl(ctx(), app);
+ return Z3_get_decl_kind(ctx(), decl) == app_type ? app : nullptr;
+}
+
Z3_ast expr::mkTrue() {
return Z3_mk_true(ctx());
}
@@ -245,17 +253,12 @@ bool expr::isInt(int64_t &n) const {
bool expr::isNot(expr &neg) const {
C();
- auto app = isApp();
- if (!app)
- return false;
-
- auto decl = Z3_get_app_decl(ctx(), app);
- if (Z3_get_decl_kind(ctx(), decl) != Z3_OP_NOT)
- return false;
-
+ if (auto app = isAppOf(Z3_OP_NOT)) {
neg = Z3_get_app_arg(ctx(), app, 0);
return true;
}
+ return false;
+}
expr expr::binop_commutative(const expr &rhs,
uint64_t (*native)(uint64_t, uint64_t),
@@ -522,6 +525,28 @@ expr expr::operator==(const expr &rhs) const {
return true;
if (isConst() && rhs.isConst())
return false;
+
+ if (auto app = isAppOf(Z3_OP_ITE)) {
+ expr c = Z3_get_app_arg(ctx(), app, 0);
+ expr t = Z3_get_app_arg(ctx(), app, 1);
+ expr e = Z3_get_app_arg(ctx(), app, 2);
+
+#if 0
+ // TODO: benchmark
+ // (= (ite c t e) (ite c x y)) -> (ite c (= t x) (= e y))
+ if (auto rhs_app = rhs.isAppOf(Z3_OP_ITE)) {
+ expr c2 = Z3_get_app_arg(ctx(), rhs_app, 0);
+ if (c.eq(c2))
+ return mkIf(c,
+ t == Z3_get_app_arg(ctx(), rhs_app, 1),
+ e == Z3_get_app_arg(ctx(), rhs_app, 2));
+ }
+#endif
+
+ // (= (ite c t e) x) -> (ite c (= t x) (= e x))
+ if (rhs.isConst() || (t.isConst() && e.isConst()))
+ return mkIf(c, t == rhs, e == rhs);
+ }
return binop_commutative(rhs, Z3_mk_eq);
}
@@ -674,6 +699,11 @@ expr expr::mkIf(const expr &cond, const expr &then, const expr &els) {
if (cond.isFalse())
return els;
+ if (then.isTrue() && els.isFalse())
+ return cond;
+ if (then.isFalse() && els.isTrue())
+ return !cond;
+
expr notcond;
Z3_ast c, t = then(), e = els();
if (cond.isNot(notcond)) {

MODIFY
smt/expr.h
smt/expr.h
@@ -27,6 +27,7 @@ class expr {
Z3_sort sort() const;
Z3_app isApp() const;
+ Z3_app isAppOf(int app) const;
expr binop_commutative(const expr &rhs,
uint64_t(*native)(uint64_t, uint64_t),

MODIFY
tools/alive_lexer.re
tools/alive_lexer.re
@@ -147,6 +147,17 @@ re2c:yyfill:check = 0;
"trunc" { return TRUNC; }
"to" { return TO; }
"select" { return SELECT; }
+"icmp" { return ICMP; }
+"eq" { return EQ; }
+"ne" { return NE; }
+"sle" { return SLE; }
+"slt" { return SLT; }
+"sge" { return SGE; }
+"sgt" { return SGT; }
+"ule" { return ULE; }
+"ult" { return ULT; }
+"uge" { return UGE; }
+"ugt" { return UGT; }
"ret" { return RETURN; }
"unreachable" { return UNREACH; }

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -260,6 +260,34 @@ static unique_ptr<Instr> parse_select(string_view name) {
return make_unique<Select>(move(aty), string(name), cond, a, b);
}
+static ICmp::Cond parse_icmp_cond() {
+ switch (auto t = *tokenizer) {
+ case EQ: return ICmp::EQ;
+ case NE: return ICmp::NE;
+ case SLE: return ICmp::SLE;
+ case SLT: return ICmp::SLT;
+ case SGE: return ICmp::SGE;
+ case SGT: return ICmp::SGT;
+ case ULE: return ICmp::ULE;
+ case ULT: return ICmp::ULT;
+ case UGE: return ICmp::UGE;
+ case UGT: return ICmp::UGT;
+ default:
+ tokenizer.unget(t);
+ return ICmp::Any;
+ }
+}
+
+static unique_ptr<Instr> parse_icmp(string_view name) {
+ // icmp cond ty %a, &b
+ auto cond = parse_icmp_cond();
+ auto ty = parse_type();
+ auto &a = parse_operand(ty.get());
+ parse_comma();
+ auto &b = parse_operand(ty.get());
+ return make_unique<ICmp>(string(name), cond, a, b);
+}
+
static unique_ptr<Instr> parse_instr(string_view name) {
// %name = instr arg1, arg2, ...
tokenizer.ensure(EQUALS);
@@ -284,6 +312,8 @@ static unique_ptr<Instr> parse_instr(string_view name) {
return parse_conversionop(name, t);
case SELECT:
return parse_select(name);
+ case ICMP:
+ return parse_icmp(name);
default:
error(string("Expected instruction name; got: ") + token_name[t]);
}

MODIFY
tools/tokens.h
tools/tokens.h
@@ -7,15 +7,18 @@ TOKEN(AND)
TOKEN(ARROW)
TOKEN(ASHR)
TOKEN(COMMA)
+TOKEN(EQ)
TOKEN(EQUALS)
TOKEN(EXACT)
TOKEN(FALSE)
+TOKEN(ICMP)
TOKEN(IDENTIFIER)
TOKEN(INT_TYPE)
TOKEN(LABEL)
TOKEN(LSHR)
TOKEN(MUL)
TOKEN(NAME)
+TOKEN(NE)
TOKEN(NSW)
TOKEN(NUM)
TOKEN(NUW)
@@ -25,13 +28,21 @@ TOKEN(RETURN)
TOKEN(SDIV)
TOKEN(SELECT)
TOKEN(SEXT)
+TOKEN(SGE)
+TOKEN(SGT)
TOKEN(SHL)
+TOKEN(SLE)
+TOKEN(SLT)
TOKEN(SREM)
TOKEN(SUB)
TOKEN(TO)
TOKEN(TRUE)
TOKEN(TRUNC)
TOKEN(UDIV)
+TOKEN(UGE)
+TOKEN(UGT)
+TOKEN(ULE)
+TOKEN(ULT)
TOKEN(UNREACH)
TOKEN(UREM)
TOKEN(XOR)

add support for icmp