add support for denormal function attribute (fixes
MODIFY
ir/attrs.cpp
ir/attrs.cpp
@@ -39,6 +39,22 @@ ostream& operator<<(ostream &os, const ParamAttrs &attr) {
}
+static ostream& operator<<(ostream &os, FPDenormalAttrs::Type t) {
+ const char *str = nullptr;
+ switch (t) {
+ case FPDenormalAttrs::IEEE: str = "ieee"; break;
+ case FPDenormalAttrs::PreserveSign: str = "preserve-sign"; break;
+ case FPDenormalAttrs::PositiveZero: str = "positive-zero"; break;
+ }
+ return os << str;
+}
+
+void FPDenormalAttrs::print(ostream &os, bool is_fp32) const {
+ os << " denormal-fp-math" << (is_fp32 ? "-f32=" : "=")
+ << output << ',' << input;
+}
+
+
ostream& operator<<(ostream &os, const FnAttrs &attr) {
if (attr.has(FnAttrs::NoRead))
os << " noread";
@@ -72,6 +88,10 @@ ostream& operator<<(ostream &os, const FnAttrs &attr) {
os << " inaccessiblememonly";
if (attr.has(FnAttrs::NullPointerIsValid))
os << " null_pointer_is_valid";
+
+ attr.fp_denormal.print(os);
+ if (attr.fp_denormal32)
+ attr.fp_denormal32->print(os, true);
return os;
}
@@ -170,6 +190,21 @@ bool FnAttrs::undefImpliesUB() const {
return ub;
}
+void FnAttrs::setFPDenormal(FPDenormalAttrs attr, unsigned bits) {
+ switch (bits) {
+ case 0: fp_denormal = attr; break;
+ case 32: fp_denormal32 = attr; break;
+ default: UNREACHABLE();
+ }
+}
+
+FPDenormalAttrs FnAttrs::getFPDenormal(const Type &ty) const {
+ switch (ty.bits()) {
+ case 32: return fp_denormal32.value_or(fp_denormal);
+ default: return fp_denormal;
+ }
+}
+
pair<AndExpr, expr>
FnAttrs::encode(const State &s, const StateValue &val, const Type &ty) const {
AndExpr UB;

MODIFY
ir/attrs.h
ir/attrs.h
// Distributed under the MIT license that can be found in the LICENSE file.
#include "smt/exprs.h"
+#include <optional>
#include <ostream>
namespace IR {
@@ -47,8 +48,17 @@ public:
encode(const State &s, const StateValue &val, const Type &ty) const;
};
+struct FPDenormalAttrs {
+ enum Type { IEEE, PreserveSign, PositiveZero };
+ Type input = IEEE;
+ Type output = IEEE;
+
+ void print(std::ostream &os, bool is_fp32 = false) const;
+};
class FnAttrs final {
+ FPDenormalAttrs fp_denormal;
+ std::optional<FPDenormalAttrs> fp_denormal32;
unsigned bits;
public:
@@ -76,11 +86,14 @@ public:
// Returns true if returning (partially) undef is UB
bool undefImpliesUB() const;
- friend std::ostream& operator<<(std::ostream &os, const FnAttrs &attr);
+ void setFPDenormal(FPDenormalAttrs attr, unsigned bits = 0);
+ FPDenormalAttrs getFPDenormal(const Type &ty) const;
// Encodes the semantics of attributes using UB and poison.
std::pair<smt::AndExpr, smt::expr>
encode(const State &s, const StateValue &val, const Type &ty) const;
+
+ friend std::ostream& operator<<(std::ostream &os, const FnAttrs &attr);
};

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -629,12 +629,30 @@ static expr any_fp_zero(State &s, const expr &v) {
return expr::mkIf(var && is_zero, v.fneg(), v);
}
+static expr handle_subnormal(FPDenormalAttrs::Type attr, expr &&v) {
+ switch (attr) {
+ case FPDenormalAttrs::IEEE:
+ break;
+ case FPDenormalAttrs::PositiveZero:
+ v = expr::mkIf(v.isFPSubNormal(), expr::mkNumber("0", v), v);
+ break;
+ case FPDenormalAttrs::PreserveSign:
+ v = expr::mkIf(v.isFPSubNormal(),
+ expr::mkIf(v.isFPNegative(),
+ expr::mkNumber("-0", v),
+ expr::mkNumber("0", v)),
+ v);
+ break;
+ }
+ return std::move(v);
+}
+
static StateValue fm_poison(State &s, const expr &a, const expr &ap,
const expr &b, const expr &bp, const expr &c,
const expr &cp,
function<expr(expr&,expr&,expr&)> fn,
- FastMathFlags fmath, bool only_input,
- int nary = 3) {
+ const Type &ty, FastMathFlags fmath,
+ bool only_input = false, int nary = 3) {
expr new_a, new_b, new_c;
if (fmath.flags & FastMathFlags::NSZ) {
new_a = any_fp_zero(s, a);
@@ -649,6 +667,15 @@ static StateValue fm_poison(State &s, const expr &a, const expr &ap,
new_c = c;
}
+ auto fpdenormal = s.getFn().getFnAttrs().getFPDenormal(ty).input;
+ if (!only_input) {
+ new_a = handle_subnormal(fpdenormal, std::move(new_a));
+ if (nary >= 2)
+ new_b = handle_subnormal(fpdenormal, std::move(new_b));
+ if (nary >= 3)
+ new_c = handle_subnormal(fpdenormal, std::move(new_c));
+ }
+
expr val = fn(new_a, new_b, new_c);
AndExpr non_poison;
non_poison.add(ap);
@@ -702,21 +729,22 @@ static StateValue fm_poison(State &s, const expr &a, const expr &ap,
static StateValue fm_poison(State &s, const expr &a, const expr &ap,
const expr &b, const expr &bp,
function<expr(expr&,expr&)> fn,
- FastMathFlags fmath, bool only_input) {
- return fm_poison(s, std::move(a), ap, std::move(b), bp, expr(), expr(),
+ const Type &ty, FastMathFlags fmath,
+ bool only_input = false) {
+ return fm_poison(s, a, ap, std::move(b), bp, expr(), expr(),
[&](expr &a, expr &b, expr &c) { return fn(a, b); },
- fmath, only_input, 2);
+ ty, fmath, only_input, 2);
}
static StateValue fm_poison(State &s, const expr &a, const expr &ap,
- function<expr(expr&)> fn,
- FastMathFlags fmath, bool only_input) {
- return fm_poison(s, std::move(a), ap, expr(), expr(), expr(), expr(),
+ function<expr(expr&)> fn, const Type &ty,
+ FastMathFlags fmath, bool only_input = false) {
+ return fm_poison(s, a, ap, expr(), expr(), expr(), expr(),
[&](expr &a, expr &b, expr &c) { return fn(a); },
- fmath, only_input, 1);
+ ty, fmath, only_input, 1);
}
-static StateValue round_value(const function<StateValue(FpRoundingMode)> &fn,
+static StateValue round_value_(const function<StateValue(FpRoundingMode)> &fn,
const State &s, FpRoundingMode rm) {
if (rm.isDefault())
return fn(FpRoundingMode::RNE);
@@ -734,45 +762,59 @@ static StateValue round_value(const function<StateValue(FpRoundingMode)> &fn,
fn(FpRoundingMode::RTZ)))));
}
+static StateValue round_value(const function<StateValue(FpRoundingMode)> &fn,
+ const State &s, const Type &ty,
+ FpRoundingMode rm) {
+ auto [v, np] = round_value_(fn, s, rm);
+ return { handle_subnormal(s.getFn().getFnAttrs().getFPDenormal(ty).output,
+ std::move(v)),
+ std::move(np) };
+}
+
StateValue FpBinOp::toSMT(State &s) const {
function<StateValue(const expr&, const expr&, const expr&, const expr&,
- FpRoundingMode)> fn;
+ const Type&, FpRoundingMode)> fn;
switch (op) {
case FAdd:
- fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto rm) -> StateValue {
+ fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto &ty,
+ auto rm) -> StateValue {
return fm_poison(s, a, ap, b, bp,
[&](expr &a, expr &b) { return a.fadd(b, rm.toSMT()); },
- fmath, false);
+ ty, fmath);
};
break;
case FSub:
- fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto rm) -> StateValue {
+ fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto &ty,
+ auto rm) -> StateValue {
return fm_poison(s, a, ap, b, bp,
[&](expr &a, expr &b) { return a.fsub(b, rm.toSMT()); },
- fmath, false);
+ ty, fmath);
};
break;
case FMul:
- fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto rm) -> StateValue {
+ fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto &ty,
+ auto rm) -> StateValue {
return fm_poison(s, a, ap, b, bp,
[&](expr &a, expr &b) { return a.fmul(b, rm.toSMT()); },
- fmath, false);
+ ty, fmath);
};
break;
case FDiv:
- fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto rm) -> StateValue {
+ fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto &ty,
+ auto rm) -> StateValue {
return fm_poison(s, a, ap, b, bp,
[&](expr &a, expr &b) { return a.fdiv(b, rm.toSMT()); },
- fmath, false);
+ ty, fmath);
};
break;
case FRem:
- fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto rm) -> StateValue {
+ fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto &ty,
+ auto rm) -> StateValue {
// TODO; Z3 has no support for LLVM's frem which is actually an fmod
return fm_poison(s, a, ap, b, bp,
[&](expr &a, expr &b) {
@@ -780,13 +822,14 @@ StateValue FpBinOp::toSMT(State &s) const {
s.doesApproximation("frem", val);
return val;
},
- fmath, false);
+ ty, fmath);
};
break;
case FMin:
case FMax:
- fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto rm) -> StateValue {
+ fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto &ty,
+ auto rm) -> StateValue {
expr ndet = expr::mkFreshVar("maxminnondet", true);
s.addQuantVar(ndet);
auto ndz = expr::mkIf(ndet, expr::mkNumber("0", a),
@@ -800,13 +843,14 @@ StateValue FpBinOp::toSMT(State &s) const {
expr::mkIf(z, ndz,
expr::mkIf(cmp, a, b))));
};
- return fm_poison(s, a, ap, b, bp, v, fmath, false);
+ return fm_poison(s, a, ap, b, bp, v, ty, fmath);
};
break;
case FMinimum:
case FMaximum:
- fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto rm) -> StateValue {
+ fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto &ty,
+ auto rm) -> StateValue {
auto v = [&](expr &a, expr &b) {
expr zpos = expr::mkNumber("0", a), zneg = expr::mkNumber("-0", a);
expr cmp = (op == FMinimum) ? a.fole(b) : a.foge(b);
@@ -818,24 +862,25 @@ StateValue FpBinOp::toSMT(State &s) const {
return expr::mkIf(a.isNaN(), a, expr::mkIf(b.isNaN(), b, e));
};
- return fm_poison(s, a, ap, b, bp, v, fmath, false);
+ return fm_poison(s, a, ap, b, bp, v, ty, fmath);
};
break;
case CopySign:
- fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto rm) -> StateValue {
+ fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto &ty,
+ auto rm) -> StateValue {
return fm_poison(s, a, ap, b, bp,
[](expr &a, expr &b) {
return expr::mkIf(a.isFPNegative() == b.isFPNegative(),
a, a.fneg()); },
- fmath, false);
+ ty, fmath);
};
break;
}
- auto scalar = [&](const auto &a, const auto &b) {
+ auto scalar = [&](const auto &a, const auto &b, const Type &ty) {
return round_value([&](auto rm) {
- return fn(a.value, a.non_poison, b.value, b.non_poison, rm);
- }, s, rm);
+ return fn(a.value, a.non_poison, b.value, b.non_poison, ty, rm);
+ }, s, ty, rm);
};
auto &a = s[*lhs];
@@ -845,11 +890,12 @@ StateValue FpBinOp::toSMT(State &s) const {
auto retty = getType().getAsAggregateType();
vector<StateValue> vals;
for (unsigned i = 0, e = retty->numElementsConst(); i != e; ++i) {
- vals.emplace_back(scalar(retty->extract(a, i), retty->extract(b, i)));
+ vals.emplace_back(scalar(retty->extract(a, i), retty->extract(b, i),
+ retty->getChild(i)));
}
return retty->aggregateVals(vals);
}
- return scalar(a, b);
+ return scalar(a, b, getType());
}
expr FpBinOp::getTypeConstraints(const Function &f) const {
@@ -1030,67 +1076,68 @@ void FpUnaryOp::print(ostream &os) const {
}
StateValue FpUnaryOp::toSMT(State &s) const {
- function<StateValue(const expr&, const expr&, FpRoundingMode)> fn;
+ function<StateValue(const expr&, const expr&, const Type&,
+ FpRoundingMode)> fn;
switch (op) {
case FAbs:
- fn = [&](auto &v, auto &np, auto rm) -> StateValue {
- return fm_poison(s, v, np, [](expr &v) { return v.fabs(); }, fmath, true);
+ fn = [&](auto &v, auto &np, auto &ty, auto rm) -> StateValue {
+ return fm_poison(s, v, np, [](expr &v) { return v.fabs();}, ty, fmath);
};
break;
case FNeg:
- fn = [&](auto &v, auto &np, auto rm) -> StateValue {
- return fm_poison(s, v, np, [](expr &v){ return v.fneg(); }, fmath, false);
+ fn = [&](auto &v, auto &np, auto &ty, auto rm) -> StateValue {
+ return fm_poison(s, v, np, [](expr &v){ return v.fneg(); }, ty, fmath);
};
break;
case Ceil:
- fn = [&](auto &v, auto &np, auto rm) -> StateValue {
- return fm_poison(s, v, np, [](expr &v) { return v.ceil(); }, fmath, true);
+ fn = [&](auto &v, auto &np, auto &ty, auto rm) -> StateValue {
+ return fm_poison(s, v, np, [](expr &v) { return v.ceil();}, ty, fmath);
};
break;
case Floor:
- fn = [&](auto &v, auto &np, auto rm) -> StateValue {
- return fm_poison(s, v, np, [](expr &v) { return v.floor(); }, fmath,
- true);
+ fn = [&](auto &v, auto &np, auto &ty, auto rm) -> StateValue {
+ return fm_poison(s, v, np, [](expr &v) { return v.floor(); }, ty, fmath);
};
break;
case RInt:
case NearbyInt:
// TODO: they differ in exception behavior
- fn = [&](auto &v, auto &np, auto rm) -> StateValue {
+ fn = [&](auto &v, auto &np, auto &ty, auto rm) -> StateValue {
return fm_poison(s, v, np, [&](expr &v) { return v.round(rm.toSMT()); },
- fmath, true);
+ ty, fmath);
};
break;
case Round:
- fn = [&](auto &v, auto &np, auto rm) -> StateValue {
+ fn = [&](auto &v, auto &np, auto &ty, auto rm) -> StateValue {
return fm_poison(s, v, np, [](expr &v) { return v.round(expr::rna()); },
- fmath, true);
+ ty, fmath);
};
break;
case RoundEven:
- fn = [&](auto &v, auto &np, auto rm) -> StateValue {
+ fn = [&](auto &v, auto &np, auto &ty, auto rm) -> StateValue {
return fm_poison(s, v, np, [](expr &v) { return v.round(expr::rne()); },
- fmath, true);
+ ty, fmath);
};
break;
case Trunc:
- fn = [&](auto &v, auto &np, auto rm) -> StateValue {
+ fn = [&](auto &v, auto &np, auto &ty, auto rm) -> StateValue {
return fm_poison(s, v, np, [](expr &v) { return v.round(expr::rtz()); },
- fmath, true);
+ ty, fmath);
};
break;
case Sqrt:
- fn = [&](auto &v, auto &np, auto rm) -> StateValue {
+ fn = [&](auto &v, auto &np, auto &ty, auto rm) -> StateValue {
return fm_poison(s, v, np, [&](expr &v){ return v.sqrt(rm.toSMT()); },
- fmath, false);
+ ty, fmath);
};
break;
}
- auto scalar = [&](const StateValue &v) {
- return round_value([&](auto rm) { return fn(v.value, v.non_poison, rm); },
- s, rm);
+ auto scalar = [&](const StateValue &v, const Type &ty) {
+ return
+ round_value([&](auto rm) { return fn(v.value, v.non_poison, ty, rm); },
+ s, ty, rm);
};
auto &v = s[*val];
@@ -1099,11 +1146,11 @@ StateValue FpUnaryOp::toSMT(State &s) const {
vector<StateValue> vals;
auto ty = val->getType().getAsAggregateType();
for (unsigned i = 0, e = ty->numElementsConst(); i != e; ++i) {
- vals.emplace_back(scalar(ty->extract(v, i)));
+ vals.emplace_back(scalar(ty->extract(v, i), ty->getChild(i)));
}
return getType().getAsAggregateType()->aggregateVals(vals);
}
- return scalar(v);
+ return scalar(v, getType());
}
expr FpUnaryOp::getTypeConstraints(const Function &f) const {
@@ -1335,19 +1382,19 @@ StateValue FpTernaryOp::toSMT(State &s) const {
auto &bv = s[*b];
auto &cv = s[*c];
function<StateValue(const StateValue&, const StateValue&, const StateValue&,
- FpRoundingMode)> fn;
+ const Type&, FpRoundingMode)> fn;
switch (op) {
case FMA:
- fn = [&](auto &a, auto &b, auto &c, auto rm) -> StateValue {
+ fn = [&](auto &a, auto &b, auto &c, auto &ty, auto rm) -> StateValue {
return fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, c.value,
c.non_poison, [&](expr &a, expr &b, expr &c) {
return expr::fma(a, b, c, rm.toSMT());
- }, fmath, false);
+ }, ty, fmath);
};
break;
case MulAdd:
- fn = [&](auto &a, auto &b, auto &c, auto rm0) -> StateValue {
+ fn = [&](auto &a, auto &b, auto &c, auto &ty, auto rm0) -> StateValue {
auto rm = rm0.toSMT();
expr var = expr::mkFreshVar("nondet", expr(false));
s.addQuantVar(var);
@@ -1355,14 +1402,14 @@ StateValue FpTernaryOp::toSMT(State &s) const {
c.non_poison, [&](expr &a, expr &b, expr &c) {
return expr::mkIf(var, expr::fma(a, b, c, rm),
a.fmul(b, rm).fadd(c, rm));
- }, fmath, false);
+ }, ty, fmath);
};
break;
}
auto scalar = [&](const StateValue &a, const StateValue &b,
- const StateValue &c) {
- return round_value([&](auto rm) { return fn(a, b, c, rm); }, s, rm);
+ const StateValue &c, const Type &ty) {
+ return round_value([&](auto rm) { return fn(a, b, c, ty, rm); }, s, ty, rm);
};
if (getType().isVectorType()) {
@@ -1371,11 +1418,11 @@ StateValue FpTernaryOp::toSMT(State &s) const {
for (unsigned i = 0, e = ty->numElementsConst(); i != e; ++i) {
vals.emplace_back(scalar(ty->extract(av, i), ty->extract(bv, i),
- ty->extract(cv, i)));
+ ty->extract(cv, i), ty->getChild(i)));
}
return ty->aggregateVals(vals);
}
- return scalar(av, bv, cv);
+ return scalar(av, bv, cv, getType());
}
expr FpTernaryOp::getTypeConstraints(const Function &f) const {
@@ -1717,7 +1764,8 @@ StateValue FpConversionOp::toSMT(State &s) const {
auto scalar = [&](const StateValue &sv, const Type &to_type) -> StateValue {
auto [v, np]
- = round_value([&](auto rm) { return fn(sv.value, to_type, rm); }, s, rm);
+ = round_value([&](auto rm) { return fn(sv.value, to_type, rm); }, s,
+ to_type, rm);
return { std::move(v), sv.non_poison && np };
};
@@ -1791,8 +1839,10 @@ StateValue Select::toSMT(State &s) const {
auto scalar = [&](const auto &a, const auto &b, const auto &c) -> StateValue {
auto cond = c.value == 1;
auto identity = [](const expr &x) { return x; };
- StateValue sva = fm_poison(s, a.value, a.non_poison, identity, fmath, true);
- StateValue svb = fm_poison(s, b.value, b.non_poison, identity, fmath, true);
+ StateValue sva
+ = fm_poison(s, a.value, a.non_poison, identity, getType(), fmath, true);
+ StateValue svb
+ = fm_poison(s, b.value, b.non_poison, identity, getType(), fmath, true);
return { expr::mkIf(cond, sva.value, svb.value),
c.non_poison && expr::mkIf(cond, sva.non_poison, svb.non_poison) };
};
@@ -2469,7 +2519,7 @@ StateValue FCmp::toSMT(State &s) const {
}
};
auto [val, np] = fm_poison(s, a.value, a.non_poison, b.value, b.non_poison,
- cmp, fmath, true);
+ cmp, getType(), fmath, true);
return { val.toBVBool(), std::move(np) };
};
@@ -2629,7 +2679,8 @@ StateValue Phi::toSMT(State &s) const {
StateValue sv = *ret();
auto identity = [](const expr &x) { return x; };
- return fm_poison(s, sv.value, sv.non_poison, identity, fmath, true);
+ return
+ fm_poison(s, sv.value, sv.non_poison, identity, getType(), fmath, true);
}
expr Phi::getTypeConstraints(const Function &f) const {

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -1348,8 +1348,37 @@ public:
}
}
+ static FPDenormalAttrs::Type parse_fp_denormal_str(string_view str) {
+ if (str == "ieee") return FPDenormalAttrs::IEEE;
+ if (str == "preserve-sign") return FPDenormalAttrs::PreserveSign;
+ if (str == "positive-zero") return FPDenormalAttrs::PositiveZero;
+ UNREACHABLE();
+ }
+
+ static FPDenormalAttrs parse_fp_denormal(string_view str) {
+ FPDenormalAttrs attr;
+ auto comma = str.find(',');
+ if (comma == string_view::npos) {
+ attr.input = attr.output = parse_fp_denormal_str(str);
+ } else {
+ attr.output = parse_fp_denormal_str(string_view(str.data(), comma));
+ attr.input = parse_fp_denormal_str(str.data() + comma + 1);
+ }
+ return attr;
+ }
+
void handleFnAttrs(const llvm::AttributeSet &aset, FnAttrs &attrs) {
for (const llvm::Attribute &llvmattr : aset) {
+ if (llvmattr.isStringAttribute()) {
+ auto str = llvmattr.getKindAsString();
+ auto val = llvmattr.getValueAsString();
+ if (str == "denormal-fp-math") {
+ attrs.setFPDenormal(parse_fp_denormal(val));
+ } else if (str == "denormal-fp-math-f32") {
+ attrs.setFPDenormal(parse_fp_denormal(val), 32);
+ }
+ }
+
if (!llvmattr.isEnumAttribute() && !llvmattr.isIntAttribute() &&
!llvmattr.isTypeAttribute())
continue;

add support for denormal function attribute (fixes #808)