fix add support for llvm.canonicalize
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -784,11 +784,15 @@ static StateValue round_value_(const function<StateValue(FpRoundingMode)> &fn,
static StateValue round_value(const function<StateValue(FpRoundingMode)> &fn,
State &s, const Type &ty, FpRoundingMode rm,
- bool enable_subnormal_flush = true) {
+ bool enable_subnormal_flush = true,
+ optional<FPDenormalAttrs::Type>
+ denormal_type = {}) {
auto [v, np] = round_value_(fn, s, rm);
if (enable_subnormal_flush)
- v = handle_subnormal(s.getFn().getFnAttrs().getFPDenormal(ty).output,
+ v = handle_subnormal(
+ denormal_type.value_or(s.getFn().getFnAttrs().getFPDenormal(ty).output),
std::move(v));
+
if (ty.isFloatType())
v = ty.getAsFloatType()->fromFloat(s, v);
return { std::move(v), std::move(np) };
@@ -1056,6 +1060,7 @@ void FpUnaryOp::print(ostream &os) const {
switch (op) {
case FAbs: str = "fabs "; break;
case FNeg: str = "fneg "; break;
+ case Canonicalize: str = "canonicalize "; break;
case Ceil: str = "ceil "; break;
case Floor: str = "floor "; break;
case RInt: str = "rint "; break;
@@ -1074,17 +1079,24 @@ void FpUnaryOp::print(ostream &os) const {
StateValue FpUnaryOp::toSMT(State &s) const {
expr (*fn)(const expr&, FpRoundingMode);
- bool flush_denormal = true;
+ bool flush_denormal_in = true;
+ bool flush_denormal_out = true;
+ optional<FPDenormalAttrs::Type> denormal_type;
switch (op) {
case FAbs:
- flush_denormal = false;
+ flush_denormal_in = flush_denormal_out = false;
fn = [](const expr &v, FpRoundingMode rm) { return v.fabs(); };
break;
case FNeg:
- flush_denormal = false;
+ flush_denormal_in = flush_denormal_out = false;
fn = [](const expr &v, FpRoundingMode rm) { return v.fneg(); };
break;
+ case Canonicalize:
+ flush_denormal_in = false;
+ fn = [](const expr &v, FpRoundingMode rm) { return v; };
+ denormal_type = FPDenormalAttrs::PreserveSign;
+ break;
case Ceil:
fn = [](const expr &v, FpRoundingMode rm) { return v.ceil(); };
break;
@@ -1115,8 +1127,8 @@ StateValue FpUnaryOp::toSMT(State &s) const {
round_value([&](auto rm) {
return fm_poison(s, v.value, v.non_poison,
[&](auto &v){ return fn(v, rm); }, ty, fmath,
- !flush_denormal, flush_denormal, false);
- }, s, ty, rm, flush_denormal);
+ !flush_denormal_in, flush_denormal_in, false);
+ }, s, ty, rm, flush_denormal_out, denormal_type);
};
auto &v = s[*val];

MODIFY
ir/instr.h
ir/instr.h
@@ -116,7 +116,8 @@ public:
class FpUnaryOp final : public Instr {
public:
enum Op {
- FAbs, FNeg, Ceil, Floor, RInt, NearbyInt, Round, RoundEven, Trunc, Sqrt
+ FAbs, FNeg, Canonicalize, Ceil, Floor, RInt, NearbyInt, Round, RoundEven,
+ Trunc, Sqrt
};
private:

MODIFY
ir/type.cpp
ir/type.cpp
@@ -438,7 +438,7 @@ expr FloatType::fromFloat(State &s, const expr &fp) const {
unsigned var_bits = fraction_bits + 1;
// NaN has a non-deterministic non-zero fraction bit pattern
- expr var = expr::mkFreshVar("NaN", expr::mkUInt(0, var_bits));
+ expr var = expr::mkVar("#NaN", var_bits);
expr fraction = var.extract(fraction_bits - 1, 0);
// sign bit, exponent (-1), fraction (non-zero)
@@ -446,7 +446,6 @@ expr FloatType::fromFloat(State &s, const expr &fp) const {
.concat(expr::mkInt(-1, exp_bits))
.concat(fraction);
s.addPre(fraction != 0);
- s.addQuantVar(var);
return expr::mkIf(isnan, nan, val);
}
@@ -487,10 +486,10 @@ bool FloatType::isNaNInt(const expr &e) const {
expr nan, nan2;
unsigned h, l;
- bool ok = sign.isExtract(nan, h, l) && fraction.isExtract(nan2, h, l) &&
- nan.eq(nan2);
- auto nan_name = nan.fn_name();
- ok &= nan_name.starts_with("NaN!");
+ bool ok = sign.isExtract(nan, h, l) &&
+ fraction.isExtract(nan2, h, l) &&
+ nan.eq(nan2) &&
+ nan.fn_name() == "#NaN";
return ok && exponent.isAllOnes();
}

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -970,6 +970,7 @@ public:
make_unique<FpBinOp>(*ty, value_name(i), *a, *b, op, parse_fmath(i),
parse_rounding(i), parse_exceptions(i)));
}
+ case llvm::Intrinsic::canonicalize:
case llvm::Intrinsic::fabs:
case llvm::Intrinsic::ceil:
case llvm::Intrinsic::experimental_constrained_ceil:
@@ -991,6 +992,7 @@ public:
PARSE_UNOP();
FpUnaryOp::Op op;
switch (i.getIntrinsicID()) {
+ case llvm::Intrinsic::canonicalize: op = FpUnaryOp::Canonicalize; break;
case llvm::Intrinsic::fabs: op = FpUnaryOp::FAbs; break;
case llvm::Intrinsic::ceil:
case llvm::Intrinsic::experimental_constrained_ceil: op = FpUnaryOp::Ceil; break;

ADD
tests/alive-tv/fp/canonicalize.srctgt.ll
+define i1 @src() {
+ %a = bitcast i32 2139095042 to float
+ %b = bitcast i32 2139095044 to float
+ %a2 = call float @llvm.canonicalize.f32(float %a)
+ %b2 = call float @llvm.canonicalize.f32(float %b)
+ %x = bitcast float %a2 to i32
+ %y = bitcast float %b2 to i32
+ %cmp = icmp eq i32 %x, %y
+ ret i1 %cmp
+}
+
+define i1 @tgt() {
+ ret i1 true
+}
+
+declare float @llvm.canonicalize.f32(float)

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -381,10 +381,6 @@ static expr encode_undef_refinement(const Type &type, const State::ValTy &a,
for (auto &v : val.undef_vars) {
repls.emplace_back(v, expr::some(v));
}
- for (auto &v : val.val.value.vars()) {
- if (v.fn_name().starts_with("NaN!"))
- repls.emplace_back(v, expr::some(v));
- }
return val.val.value.subst(repls);
};

fix #856: add support for llvm.canonicalize