Add support for fcmp
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -854,6 +854,65 @@ unique_ptr<Instr> ICmp::dup(const string &suffix) const {
return make_unique<ICmp>(getType(), getName() + suffix, cond, a, b);
}
+FCmp::FCmp(Type &type, string &&name, Cond cond, Value &a, Value &b)
+ : Instr(type, move(name)), a(a), b(b), cond(cond) {}
+
+void FCmp::print(ostream &os) const {
+ const char *condtxt = nullptr;
+ switch (cond) {
+ case OEQ: condtxt = "oeq "; break;
+ case OGT: condtxt = "ogt "; break;
+ case OGE: condtxt = "oge "; break;
+ case OLT: condtxt = "olt "; break;
+ case OLE: condtxt = "ole "; break;
+ case ONE: condtxt = "one "; break;
+ case ORD: condtxt = "ord "; break;
+ case UEQ: condtxt = "ueq "; break;
+ case UGT: condtxt = "ugt "; break;
+ case UGE: condtxt = "uge "; break;
+ case ULT: condtxt = "ult "; break;
+ case ULE: condtxt = "ule "; break;
+ case UNE: condtxt = "une "; break;
+ case UNO: condtxt = "uno "; break;
+ }
+ os << getName() << " = fcmp " << condtxt << a << ", " << b.getName();
+}
+
+StateValue FCmp::toSMT(State &s) const {
+ auto &[av, ap] = s[a];
+ auto &[bv, bp] = s[b];
+ expr val;
+ switch (cond) {
+ case OEQ: val = av.foeq(bv); break;
+ case OGT: val = av.fogt(bv); break;
+ case OGE: val = av.foge(bv); break;
+ case OLT: val = av.folt(bv); break;
+ case OLE: val = av.fole(bv); break;
+ case ONE: val = av.fone(bv); break;
+ case ORD: val = av.ford(bv); break;
+ case UEQ: val = av.fueq(bv); break;
+ case UGT: val = av.fugt(bv); break;
+ case UGE: val = av.fuge(bv); break;
+ case ULT: val = av.fult(bv); break;
+ case ULE: val = av.fule(bv); break;
+ case UNE: val = av.fune(bv); break;
+ case UNO: val = av.funo(bv); break;
+ }
+ return { val.toBVBool(), ap && bp };
+}
+
+expr FCmp::getTypeConstraints(const Function &f) const {
+ return Value::getTypeConstraints() &&
+ getType().enforceIntType() &&
+ getType().sizeVar() == 1u &&
+ a.getType().enforceFloatType() &&
+ a.getType() == b.getType();
+}
+
+unique_ptr<Instr> FCmp::dup(const string &suffix) const {
+ return make_unique<FCmp>(getType(), getName() + suffix, cond, a, b);
+}
+
void Freeze::print(ostream &os) const {
os << getName() << " = freeze " << val;

MODIFY
ir/instr.h
ir/instr.h
@@ -168,6 +168,23 @@ public:
std::unique_ptr<Instr> dup(const std::string &suffix) const override;
};
+class FCmp final : public Instr {
+public:
+ enum Cond { OEQ, OGT, OGE, OLT, OLE, ONE, ORD,
+ UEQ, UGT, UGE, ULT, ULE, UNE, UNO };
+
+private:
+ Value &a, &b;
+ Cond cond;
+
+public:
+ FCmp(Type &type, 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 Function &f) const override;
+ std::unique_ptr<Instr> dup(const std::string &suffix) const override;
+};
+
class Freeze final : public Instr {
Value &val;

MODIFY
llvm_util/utils.cpp
llvm_util/utils.cpp
@@ -329,6 +329,42 @@ public:
cond, *a, *b));
}
+ RetTy visitFCmpInst(llvm::FCmpInst &i) {
+ PARSE_BINOP();
+ FCmp::Cond cond;
+ switch (i.getPredicate()) {
+ case llvm::CmpInst::FCMP_OEQ: cond = FCmp::OEQ; break;
+ case llvm::CmpInst::FCMP_OGT: cond = FCmp::OGT; break;
+ case llvm::CmpInst::FCMP_OGE: cond = FCmp::UGE; break;
+ case llvm::CmpInst::FCMP_OLT: cond = FCmp::OLT; break;
+ case llvm::CmpInst::FCMP_OLE: cond = FCmp::OLE; break;
+ case llvm::CmpInst::FCMP_ONE: cond = FCmp::ONE; break;
+ case llvm::CmpInst::FCMP_ORD: cond = FCmp::ORD; break;
+ case llvm::CmpInst::FCMP_UEQ: cond = FCmp::UEQ; break;
+ case llvm::CmpInst::FCMP_UGT: cond = FCmp::UGT; break;
+ case llvm::CmpInst::FCMP_UGE: cond = FCmp::UGE; break;
+ case llvm::CmpInst::FCMP_ULT: cond = FCmp::ULT; break;
+ case llvm::CmpInst::FCMP_ULE: cond = FCmp::ULE; break;
+ case llvm::CmpInst::FCMP_UNE: cond = FCmp::UNE; break;
+ case llvm::CmpInst::FCMP_UNO: cond = FCmp::UNO; break;
+ case llvm::CmpInst::FCMP_TRUE: {
+ auto tru = get_operand(llvm::ConstantInt::getTrue(i.getContext()));
+ RETURN_IDENTIFIER(make_unique<UnaryOp>(*int_types[1].get(),
+ value_name(i), *tru, UnaryOp::Copy));
+ }
+ case llvm::CmpInst::FCMP_FALSE: {
+ auto fals = get_operand(llvm::ConstantInt::getFalse(i.getContext()));
+ RETURN_IDENTIFIER(make_unique<UnaryOp>(*int_types[1].get(),
+ value_name(i), *fals, UnaryOp::Copy));
+ }
+ default:
+ UNREACHABLE();
+ }
+ RETURN_IDENTIFIER(make_unique<FCmp>(*int_types[1].get(), value_name(i),
+ cond, *a, *b));
+ }
+
+
RetTy visitSelectInst(llvm::SelectInst &i) {
PARSE_TRIOP();
RETURN_IDENTIFIER(make_unique<Select>(*ty, value_name(i), *a, *b, *c));

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -706,6 +706,11 @@ expr expr::ctpop() const {
return res;
}
+expr expr::isNaN() const {
+ C();
+ return Z3_mk_fpa_is_nan(ctx(), ast());
+}
+
// TODO: make rounding mode customizable
expr expr::fadd(const expr &rhs) const {
C(rhs);
@@ -731,6 +736,74 @@ expr expr::fdiv(const expr &rhs) const {
return Z3_mk_fpa_div(ctx(), rm, ast(), rhs());
}
+expr expr::foeq(const expr &rhs) const {
+ C(rhs);
+ return ford(rhs) && Z3_mk_fpa_eq(ctx(), ast(), rhs());
+}
+
+expr expr::fogt(const expr &rhs) const {
+ C(rhs);
+ return ford(rhs) && Z3_mk_fpa_gt(ctx(), ast(), rhs());
+}
+
+expr expr::foge(const expr &rhs) const {
+ C(rhs);
+ return ford(rhs) && Z3_mk_fpa_geq(ctx(), ast(), rhs());
+}
+
+expr expr::folt(const expr &rhs) const {
+ C(rhs);
+ return ford(rhs) && Z3_mk_fpa_lt(ctx(), ast(), rhs());
+}
+
+expr expr::fole(const expr &rhs) const {
+ C(rhs);
+ return ford(rhs) && Z3_mk_fpa_leq(ctx(), ast(), rhs());
+}
+
+expr expr::fone(const expr &rhs) const {
+ C(rhs);
+ return ford(rhs) && !expr(Z3_mk_fpa_eq(ctx(), ast(), rhs()));
+}
+
+expr expr::ford(const expr &rhs) const {
+ return !isNaN() && !rhs.isNaN();
+}
+
+expr expr::fueq(const expr &rhs) const {
+ C(rhs);
+ return funo(rhs) || Z3_mk_fpa_eq(ctx(), ast(), rhs());
+}
+
+expr expr::fugt(const expr &rhs) const {
+ C(rhs);
+ return funo(rhs) || Z3_mk_fpa_gt(ctx(), ast(), rhs());
+}
+
+expr expr::fuge(const expr &rhs) const {
+ C(rhs);
+ return funo(rhs) || Z3_mk_fpa_geq(ctx(), ast(), rhs());
+}
+
+expr expr::fult(const expr &rhs) const {
+ C(rhs);
+ return funo(rhs) || Z3_mk_fpa_lt(ctx(), ast(), rhs());
+}
+
+expr expr::fule(const expr &rhs) const {
+ C(rhs);
+ return funo(rhs) || Z3_mk_fpa_leq(ctx(), ast(), rhs());
+}
+
+expr expr::fune(const expr &rhs) const {
+ C(rhs);
+ return funo(rhs) || !expr(Z3_mk_fpa_eq(ctx(), ast(), rhs()));
+}
+
+expr expr::funo(const expr &rhs) const {
+ return !ford(rhs());
+}
+
expr expr::operator&(const expr &rhs) const {
if (eq(rhs))
return *this;

MODIFY
smt/expr.h
smt/expr.h
@@ -154,11 +154,28 @@ public:
expr ctlz() const;
expr ctpop() const;
+ expr isNaN() const;
expr fadd(const expr &rhs) const;
expr fsub(const expr &rhs) const;
expr fmul(const expr &rhs) const;
expr fdiv(const expr &rhs) const;
+ expr foeq(const expr &rhs) const;
+ expr fogt(const expr &rhs) const;
+ expr foge(const expr &rhs) const;
+ expr folt(const expr &rhs) const;
+ expr fole(const expr &rhs) const;
+ expr fone(const expr &rhs) const;
+ expr ford(const expr &rhs) const;
+ expr fueq(const expr &rhs) const;
+ expr fugt(const expr &rhs) const;
+ expr fuge(const expr &rhs) const;
+ expr fult(const expr &rhs) const;
+ expr fule(const expr &rhs) const;
+ expr fune(const expr &rhs) const;
+ expr funo(const expr &rhs) const;
+
+
expr operator&(const expr &rhs) const;
expr operator|(const expr &rhs) const;
expr operator^(const expr &rhs) const;

ADD
tests/unit/fp/fcmp.opt
+Name: T1
+%t = fcmp oeq float 4.0, 5.0
+ =>
+%t = false
+
+Name: T2
+%t = fcmp one float 4.0, 5.0
+ =>
+%t = true
+
+Name: T3
+%t = fcmp olt float 4.0, 5.0
+ =>
+%t = true
+
+Name: T4
+%t = fcmp ueq float 1.0, 2.0
+ =>
+%t = false
+
+Name: T5
+%t = fcmp true float 1.0, 2.0
+ =>
+%t = true
+
+Name: T6
+%t = fcmp false float 4.0, 5.0
+ =>
+%t = false
+
+Name: T7
+%t = true
+ =>
+%t = fcmp true float 1.0, 2.0
+
+Name: T8
+%t = false
+ =>
+%t = fcmp false float 4.0, 5.0

MODIFY
tools/alive_lexer.re
tools/alive_lexer.re
@@ -225,6 +225,17 @@ re2c:yyfill:check = 0;
"fmul" { return FMUL; }
"fdiv" { return FDIV; }
"frem" { return FREM; }
+"fcmp" { return FCMP; }
+"oeq" { return OEQ; }
+"ogt" { return OGT; }
+"oge" { return OGE; }
+"olt" { return OLT; }
+"ole" { return OLE; }
+"one" { return ONE; }
+"ord" { return ORD; }
+"ueq" { return UEQ; }
+"une" { return UNE; }
+"uno" { return UNO; }
"half" { return HALF;}
"float" { return FLOAT;}
"double" { return DOUBLE;}

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -614,6 +614,51 @@ static unique_ptr<Instr> parse_icmp(string_view name) {
return make_unique<ICmp>(*int_types[1].get(), string(name), cond, a, b);
}
+static unique_ptr<Instr> parse_fcmp(string_view name) {
+ // fcmp cond ty %a, &b
+ FCmp::Cond cond;
+ auto cond_t = *tokenizer;
+ switch (cond_t) {
+ case OEQ: cond = FCmp::OEQ; break;
+ case OGT: cond = FCmp::OGT; break;
+ case OGE: cond = FCmp::OGE; break;
+ case OLT: cond = FCmp::OLT; break;
+ case OLE: cond = FCmp::OLE; break;
+ case ONE: cond = FCmp::ONE; break;
+ case ORD: cond = FCmp::ORD; break;
+ case UEQ: cond = FCmp::UEQ; break;
+ case UGT: cond = FCmp::UGT; break;
+ case UGE: cond = FCmp::UGE; break;
+ case ULT: cond = FCmp::ULT; break;
+ case ULE: cond = FCmp::ULE; break;
+ case UNE: cond = FCmp::UNE; break;
+ case UNO: cond = FCmp::UNO; break;
+ case TRUE: break;
+ case FALSE: break;
+ default:
+ error("Expected fcmp cond", cond_t);
+ }
+
+ auto &ty = parse_type();
+ auto &a = parse_operand(ty);
+ parse_comma();
+ auto &b = parse_operand(ty);
+
+ switch (cond_t) {
+ case TRUE:
+ return make_unique<UnaryOp>(*int_types[1].get(), string(name),
+ get_constant(1, *int_types[1].get()),
+ UnaryOp::Copy);
+ case FALSE:
+ return make_unique<UnaryOp>(*int_types[1].get(), string(name),
+ get_constant(0, *int_types[1].get()),
+ UnaryOp::Copy);
+ default:
+ return make_unique<FCmp>(*int_types[1].get(), string(name), cond, a, b);
+ }
+ UNREACHABLE();
+}
+
static unique_ptr<Instr> parse_freeze(string_view name) {
// freeze ty %op
auto &ty = parse_type();
@@ -697,6 +742,8 @@ static unique_ptr<Instr> parse_instr(string_view name) {
return parse_extractvalue(name);
case ICMP:
return parse_icmp(name);
+ case FCMP:
+ return parse_fcmp(name);
case FREEZE:
return parse_freeze(name);
case CALL:

MODIFY
tools/tokens.h
tools/tokens.h
@@ -29,6 +29,7 @@ TOKEN(EXACT)
TOKEN(EXTRACTVALUE)
TOKEN(FADD)
TOKEN(FALSE)
+TOKEN(FCMP)
TOKEN(FDIV)
TOKEN(FLOAT)
TOKEN(FMUL)
@@ -53,7 +54,14 @@ TOKEN(NSW)
TOKEN(NUM)
TOKEN(NUM_STR)
TOKEN(NUW)
+TOKEN(OEQ)
+TOKEN(OGE)
+TOKEN(OGT)
+TOKEN(OLE)
+TOKEN(OLT)
+TOKEN(ONE)
TOKEN(OR)
+TOKEN(ORD)
TOKEN(PLUS)
TOKEN(POISON)
TOKEN(PRE)
@@ -82,12 +90,15 @@ TOKEN(TRUNC)
TOKEN(UADD_OVERFLOW)
TOKEN(UADD_SAT)
TOKEN(UDIV)
+TOKEN(UEQ)
TOKEN(UGE)
TOKEN(UGT)
TOKEN(ULE)
TOKEN(ULT)
TOKEN(UMUL_OVERFLOW)
TOKEN(UNDEF)
+TOKEN(UNE)
+TOKEN(UNO)
TOKEN(UNREACH)
TOKEN(UREM)
TOKEN(USUB_OVERFLOW)

Add support for fcmp