Skip to content

Commit 9ff4ac3

Browse files
nunoplopesnunoplopes
committed
Make fabs & copysign ignore denormal flushing
1 parent b32e40c commit 9ff4ac3

File tree

1 file changed

+71
-121
lines changed

1 file changed

+71
-121
lines changed

‎ir/instr.cpp‎

Lines changed: 71 additions & 121 deletions
Original file line numberDiff line numberDiff line change
@@ -778,115 +778,88 @@ static StateValue round_value(const function<StateValue(FpRoundingMode)> &fn,
778778
}
779779

780780
StateValue FpBinOp::toSMT(State &s) const {
781-
function<StateValue(const expr&, const expr&, const expr&, const expr&,
782-
const Type&, FpRoundingMode)> fn;
781+
function<expr(const expr&, const expr&, FpRoundingMode)> fn;
782+
bool flush_denormal = true;
783783

784784
switch (op) {
785785
case FAdd:
786-
fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto &ty,
787-
auto rm) -> StateValue {
788-
return fm_poison(s, a, ap, b, bp,
789-
[&](expr &a, expr &b) { return a.fadd(b, rm.toSMT()); },
790-
ty, fmath);
786+
fn = [](const expr &a, const expr &b, FpRoundingMode rm) {
787+
return a.fadd(b, rm.toSMT());
791788
};
792789
break;
793790

794791
case FSub:
795-
fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto &ty,
796-
auto rm) -> StateValue {
797-
return fm_poison(s, a, ap, b, bp,
798-
[&](expr &a, expr &b) { return a.fsub(b, rm.toSMT()); },
799-
ty, fmath);
792+
fn = [](const expr &a, const expr &b, FpRoundingMode rm) {
793+
return a.fsub(b, rm.toSMT());
800794
};
801795
break;
802796

803797
case FMul:
804-
fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto &ty,
805-
auto rm) -> StateValue {
806-
return fm_poison(s, a, ap, b, bp,
807-
[&](expr &a, expr &b) { return a.fmul(b, rm.toSMT()); },
808-
ty, fmath);
798+
fn = [](const expr &a, const expr &b, FpRoundingMode rm) {
799+
return a.fmul(b, rm.toSMT());
809800
};
810801
break;
811802

812803
case FDiv:
813-
fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto &ty,
814-
auto rm) -> StateValue {
815-
return fm_poison(s, a, ap, b, bp,
816-
[&](expr &a, expr &b) { return a.fdiv(b, rm.toSMT()); },
817-
ty, fmath);
804+
fn = [](const expr &a, const expr &b, FpRoundingMode rm) {
805+
return a.fdiv(b, rm.toSMT());
818806
};
819807
break;
820808

821809
case FRem:
822-
fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto &ty,
823-
auto rm) -> StateValue {
810+
fn = [&](const expr &a, const expr &b, FpRoundingMode rm) {
824811
// TODO; Z3 has no support for LLVM's frem which is actually an fmod
825-
return fm_poison(s, a, ap, b, bp,
826-
[&](expr &a, expr &b) {
827-
auto val = expr::mkUF("fmod", {a, b}, a);
828-
s.doesApproximation("frem", val);
829-
return val;
830-
},
831-
ty, fmath);
812+
auto val = expr::mkUF("fmod", {a, b}, a);
813+
s.doesApproximation("frem", val);
814+
return val;
832815
};
833816
break;
834817

835818
case FMin:
836819
case FMax:
837-
fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto &ty,
838-
auto rm) -> StateValue {
820+
fn = [&](const expr &a, const expr &b, FpRoundingMode rm) {
839821
expr ndet = expr::mkFreshVar("maxminnondet", true);
840822
s.addQuantVar(ndet);
841823
auto ndz = expr::mkIf(ndet, expr::mkNumber("0", a),
842824
expr::mkNumber("-0", a));
843825

844-
auto v = [&](expr &a, expr &b) {
845-
expr z = a.isFPZero() && b.isFPZero();
846-
expr cmp = op == FMin ? a.fole(b) : a.foge(b);
847-
return expr::mkIf(a.isNaN(), b,
848-
expr::mkIf(b.isNaN(), a,
849-
expr::mkIf(z, ndz,
850-
expr::mkIf(cmp, a, b))));
851-
};
852-
return fm_poison(s, a, ap, b, bp, v, ty, fmath);
826+
expr z = a.isFPZero() && b.isFPZero();
827+
expr cmp = op == FMin ? a.fole(b) : a.foge(b);
828+
return expr::mkIf(a.isNaN(), b,
829+
expr::mkIf(b.isNaN(), a,
830+
expr::mkIf(z, ndz,
831+
expr::mkIf(cmp, a, b))));
853832
};
854833
break;
855834

856835
case FMinimum:
857836
case FMaximum:
858-
fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto &ty,
859-
auto rm) -> StateValue {
860-
auto v = [&](expr &a, expr &b) {
861-
expr zpos = expr::mkNumber("0", a), zneg = expr::mkNumber("-0", a);
862-
expr cmp = (op == FMinimum) ? a.fole(b) : a.foge(b);
863-
expr neg_cond = op == FMinimum ? (a.isFPNegative() || b.isFPNegative())
864-
: (a.isFPNegative() && b.isFPNegative());
865-
expr e = expr::mkIf(a.isFPZero() && b.isFPZero(),
866-
expr::mkIf(neg_cond, zneg, zpos),
867-
expr::mkIf(cmp, a, b));
868-
869-
return expr::mkIf(a.isNaN(), a, expr::mkIf(b.isNaN(), b, e));
870-
};
871-
return fm_poison(s, a, ap, b, bp, v, ty, fmath);
837+
fn = [&](const expr &a, const expr &b, FpRoundingMode rm) {
838+
expr zpos = expr::mkNumber("0", a), zneg = expr::mkNumber("-0", a);
839+
expr cmp = (op == FMinimum) ? a.fole(b) : a.foge(b);
840+
expr neg_cond = op == FMinimum ? (a.isFPNegative() || b.isFPNegative())
841+
: (a.isFPNegative() && b.isFPNegative());
842+
expr e = expr::mkIf(a.isFPZero() && b.isFPZero(),
843+
expr::mkIf(neg_cond, zneg, zpos),
844+
expr::mkIf(cmp, a, b));
845+
846+
return expr::mkIf(a.isNaN(), a, expr::mkIf(b.isNaN(), b, e));
872847
};
873848
break;
874849
case CopySign:
875-
fn = [&](auto &a, auto &ap, auto &b, auto &bp, auto &ty,
876-
auto rm) -> StateValue {
877-
return fm_poison(s, a, ap, b, bp,
878-
[](expr &a, expr &b) {
879-
return expr::mkIf(a.isFPNegative() == b.isFPNegative(),
880-
a, a.fneg()); },
881-
ty, fmath);
850+
flush_denormal = false;
851+
fn = [](const expr &a, const expr &b, FpRoundingMode rm) {
852+
return expr::mkIf(a.isFPNegative() == b.isFPNegative(), a, a.fneg());
882853
};
883854
break;
884855
}
885856

886857
auto scalar = [&](const auto &a, const auto &b, const Type &ty) {
887858
return round_value([&](auto rm) {
888-
return fn(a.value, a.non_poison, b.value, b.non_poison, ty, rm);
889-
}, s, ty, rm);
859+
return fm_poison(s, a.value, a.non_poison, b.value, b.non_poison,
860+
[&](expr &a, expr &b){ return fn(a, b, rm); }, ty,
861+
fmath, !flush_denormal, flush_denormal);
862+
}, s, ty, rm, flush_denormal);
890863
};
891864

892865
auto &a = s[*lhs];
@@ -1083,71 +1056,50 @@ void FpUnaryOp::print(ostream &os) const {
10831056
}
10841057

10851058
StateValue FpUnaryOp::toSMT(State &s) const {
1086-
function<StateValue(const expr&, const expr&, const Type&,
1087-
FpRoundingMode)> fn;
1059+
expr (*fn)(const expr&, FpRoundingMode);
1060+
bool flush_denormal = true;
10881061

10891062
switch (op) {
10901063
case FAbs:
1091-
fn = [&](auto &v, auto &np, auto &ty, auto rm) -> StateValue {
1092-
return fm_poison(s, v, np, [](expr &v) { return v.fabs();}, ty, fmath);
1093-
};
1064+
flush_denormal = false;
1065+
fn = [](const expr &v, FpRoundingMode rm) { return v.fabs(); };
10941066
break;
10951067
case FNeg:
1096-
fn = [&](auto &v, auto &np, auto &ty, auto rm) -> StateValue {
1097-
return
1098-
fm_poison(s, v, np, [](expr &v){ return v.fneg(); }, ty, fmath, true,
1099-
/*flush_denormal=*/false);
1100-
};
1068+
flush_denormal = false;
1069+
fn = [](const expr &v, FpRoundingMode rm){ return v.fneg(); };
11011070
break;
11021071
case Ceil:
1103-
fn = [&](auto &v, auto &np, auto &ty, auto rm) -> StateValue {
1104-
return fm_poison(s, v, np, [](expr &v) { return v.ceil();}, ty, fmath);
1105-
};
1072+
fn = [](const expr &v, FpRoundingMode rm) { return v.ceil(); };
11061073
break;
11071074
case Floor:
1108-
fn = [&](auto &v, auto &np, auto &ty, auto rm) -> StateValue {
1109-
return fm_poison(s, v, np, [](expr &v) { return v.floor(); }, ty, fmath);
1110-
};
1075+
fn = [](const expr &v, FpRoundingMode rm) { return v.floor(); };
11111076
break;
11121077
case RInt:
11131078
case NearbyInt:
11141079
// TODO: they differ in exception behavior
1115-
fn = [&](auto &v, auto &np, auto &ty, auto rm) -> StateValue {
1116-
return fm_poison(s, v, np, [&](expr &v) { return v.round(rm.toSMT()); },
1117-
ty, fmath);
1118-
};
1080+
fn = [](const expr &v, FpRoundingMode rm) { return v.round(rm.toSMT()); };
11191081
break;
11201082
case Round:
1121-
fn = [&](auto &v, auto &np, auto &ty, auto rm) -> StateValue {
1122-
return fm_poison(s, v, np, [](expr &v) { return v.round(expr::rna()); },
1123-
ty, fmath);
1124-
};
1083+
fn = [](const expr &v, FpRoundingMode rm) { return v.round(expr::rna()); };
11251084
break;
11261085
case RoundEven:
1127-
fn = [&](auto &v, auto &np, auto &ty, auto rm) -> StateValue {
1128-
return fm_poison(s, v, np, [](expr &v) { return v.round(expr::rne()); },
1129-
ty, fmath);
1130-
};
1086+
fn = [](const expr &v, FpRoundingMode rm) { return v.round(expr::rne()); };
11311087
break;
11321088
case Trunc:
1133-
fn = [&](auto &v, auto &np, auto &ty, auto rm) -> StateValue {
1134-
return fm_poison(s, v, np, [](expr &v) { return v.round(expr::rtz()); },
1135-
ty, fmath);
1136-
};
1089+
fn = [](const expr &v, FpRoundingMode rm) { return v.round(expr::rtz()); };
11371090
break;
11381091
case Sqrt:
1139-
fn = [&](auto &v, auto &np, auto &ty, auto rm) -> StateValue {
1140-
return fm_poison(s, v, np, [&](expr &v){ return v.sqrt(rm.toSMT()); },
1141-
ty, fmath);
1142-
};
1092+
fn = [](const expr &v, FpRoundingMode rm) { return v.sqrt(rm.toSMT()); };
11431093
break;
11441094
}
11451095

11461096
auto scalar = [&](const StateValue &v, const Type &ty) {
1147-
// NOTE: fneg doesn't flush to zero on denormal numbers
11481097
return
1149-
round_value([&](auto rm) { return fn(v.value, v.non_poison, ty, rm); },
1150-
s, ty, rm, op != FNeg);
1098+
round_value([&](auto rm) {
1099+
return fm_poison(s, v.value, v.non_poison,
1100+
[&](expr &v){ return fn(v, rm); }, ty, fmath,
1101+
!flush_denormal, flush_denormal);
1102+
}, s, ty, rm, flush_denormal);
11511103
};
11521104

11531105
auto &v = s[*val];
@@ -1388,40 +1340,38 @@ void FpTernaryOp::print(ostream &os) const {
13881340
}
13891341

13901342
StateValue FpTernaryOp::toSMT(State &s) const {
1391-
auto &av = s[*a];
1392-
auto &bv = s[*b];
1393-
auto &cv = s[*c];
1394-
function<StateValue(const StateValue&, const StateValue&, const StateValue&,
1395-
const Type&, FpRoundingMode)> fn;
1343+
function<expr(const expr&, const expr&, const expr&, FpRoundingMode)> fn;
13961344

13971345
switch (op) {
13981346
case FMA:
1399-
fn = [&](auto &a, auto &b, auto &c, auto &ty, auto rm) -> StateValue {
1400-
return fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, c.value,
1401-
c.non_poison, [&](expr &a, expr &b, expr &c) {
1402-
return expr::fma(a, b, c, rm.toSMT());
1403-
}, ty, fmath);
1347+
fn = [](const expr &a, const expr &b, const expr &c, FpRoundingMode rm) {
1348+
return expr::fma(a, b, c, rm.toSMT());
14041349
};
14051350
break;
14061351
case MulAdd:
1407-
fn = [&](auto &a, auto &b, auto &c, auto &ty, auto rm0) -> StateValue {
1352+
fn = [&](const expr &a, const expr &b, const expr &c, FpRoundingMode rm0) {
14081353
auto rm = rm0.toSMT();
14091354
expr var = expr::mkFreshVar("nondet", expr(false));
14101355
s.addQuantVar(var);
1411-
return fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, c.value,
1412-
c.non_poison, [&](expr &a, expr &b, expr &c) {
1413-
return expr::mkIf(var, expr::fma(a, b, c, rm),
1414-
a.fmul(b, rm).fadd(c, rm));
1415-
}, ty, fmath);
1356+
return expr::mkIf(var, expr::fma(a, b, c, rm), a.fmul(b, rm).fadd(c, rm));
14161357
};
14171358
break;
14181359
}
14191360

14201361
auto scalar = [&](const StateValue &a, const StateValue &b,
14211362
const StateValue &c, const Type &ty) {
1422-
return round_value([&](auto rm) { return fn(a, b, c, ty, rm); }, s, ty, rm);
1363+
return round_value([&](auto rm) {
1364+
return fm_poison(s, a.value, a.non_poison, b.value, b.non_poison,
1365+
c.value, c.non_poison,
1366+
[&](expr &a, expr &b, expr &c){ return fn(a, b, c, rm);},
1367+
ty, fmath);
1368+
}, s, ty, rm);
14231369
};
14241370

1371+
auto &av = s[*a];
1372+
auto &bv = s[*b];
1373+
auto &cv = s[*c];
1374+
14251375
if (getType().isVectorType()) {
14261376
vector<StateValue> vals;
14271377
auto ty = getType().getAsAggregateType();

0 commit comments

Comments
 (0)