fabs/fneg/copysign are bitwise (again..)
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -625,7 +625,7 @@ static expr any_fp_zero(State &s, const expr &v) {
}
expr var = expr::mkFreshVar("anyzero", true);
- s.addQuantVar(var);
+ s.addNondetVar(var);
return expr::mkIf(var && is_zero, v.fneg(), v);
}
@@ -784,7 +784,7 @@ static StateValue fm_poison(State &s, expr a, const expr &ap, expr b,
expr::mkIf(fp_b.isNaN() && var == 1, b,
expr::mkIf(fp_c.isNaN() && var == 2, c, canonical_nan))));
}
- s.addQuantVar(var);
+ s.addNondetVar(var);
}
#endif
}
@@ -816,35 +816,36 @@ static StateValue fm_poison(State &s, expr a, const expr &ap,
}
StateValue FpBinOp::toSMT(State &s) const {
- function<expr(const expr&, const expr&, FpRoundingMode)> fn;
+ function<expr(const expr&, const expr&, const Type&, FpRoundingMode)> fn;
+ bool bitwise = false;
switch (op) {
case FAdd:
- fn = [](const expr &a, const expr &b, FpRoundingMode rm) {
+ fn = [](const expr &a, const expr &b, const Type &ty, FpRoundingMode rm) {
return a.fadd(b, rm.toSMT());
};
break;
case FSub:
- fn = [](const expr &a, const expr &b, FpRoundingMode rm) {
+ fn = [](const expr &a, const expr &b, const Type &ty, FpRoundingMode rm) {
return a.fsub(b, rm.toSMT());
};
break;
case FMul:
- fn = [](const expr &a, const expr &b, FpRoundingMode rm) {
+ fn = [](const expr &a, const expr &b, const Type &ty, FpRoundingMode rm) {
return a.fmul(b, rm.toSMT());
};
break;
case FDiv:
- fn = [](const expr &a, const expr &b, FpRoundingMode rm) {
+ fn = [](const expr &a, const expr &b, const Type &ty, FpRoundingMode rm) {
return a.fdiv(b, rm.toSMT());
};
break;
case FRem:
- fn = [&](const expr &a, const expr &b, FpRoundingMode rm) {
+ fn = [&](const expr &a, const expr &b, const Type &ty, FpRoundingMode rm) {
// TODO; Z3 has no support for LLVM's frem which is actually an fmod
auto val = expr::mkUF("fmod", {a, b}, a);
s.doesApproximation("frem", val);
@@ -854,9 +855,9 @@ StateValue FpBinOp::toSMT(State &s) const {
case FMin:
case FMax:
- fn = [&](const expr &a, const expr &b, FpRoundingMode rm) {
+ fn = [&](const expr &a, const expr &b, const Type &ty, FpRoundingMode rm) {
expr ndet = expr::mkFreshVar("maxminnondet", true);
- s.addQuantVar(ndet);
+ s.addNondetVar(ndet);
auto ndz = expr::mkIf(ndet, expr::mkNumber("0", a),
expr::mkNumber("-0", a));
@@ -871,7 +872,7 @@ StateValue FpBinOp::toSMT(State &s) const {
case FMinimum:
case FMaximum:
- fn = [&](const expr &a, const expr &b, FpRoundingMode rm) {
+ fn = [&](const expr &a, const expr &b, const Type &ty, FpRoundingMode rm) {
expr zpos = expr::mkNumber("0", a), zneg = expr::mkNumber("-0", a);
expr cmp = (op == FMinimum) ? a.fole(b) : a.foge(b);
expr neg_cond = op == FMinimum ? (a.isFPNegative() || b.isFPNegative())
@@ -885,14 +886,17 @@ StateValue FpBinOp::toSMT(State &s) const {
break;
case CopySign:
- fn = [&](const expr &a, const expr &b, FpRoundingMode rm) {
- auto isnan = b.isNaN();
+ bitwise = true;
+ fn = [&](const expr &a, const expr &b, const Type &ty, FpRoundingMode rm) {
+ auto fpty = ty.getAsFloatType();
+ expr fp_b = fpty->getFloat(b);
+ auto isnan = fp_b.isNaN();
auto samesign = a.isFPNegative() == b.isFPNegative();
if (isnan.isFalse())
return expr::mkIf(samesign, a, a.fneg());
expr var = expr::mkFreshVar("#flipsign", false);
- s.addQuantVar(var);
+ s.addNondetVar(var);
return expr::mkIf(expr::mkIf(isnan, var, samesign), a, a.fneg());
};
break;
@@ -900,8 +904,8 @@ StateValue FpBinOp::toSMT(State &s) const {
auto scalar = [&](const auto &a, const auto &b, const Type &ty) {
return fm_poison(s, a.value, a.non_poison, b.value, b.non_poison,
- [&](auto &a, auto &b, auto rm){ return fn(a, b, rm); },
- ty, fmath, rm, false);
+ [&](auto &a, auto &b, auto rm){ return fn(a, b, ty, rm); },
+ ty, fmath, rm, bitwise);
};
auto &a = s[*lhs];
@@ -992,7 +996,7 @@ StateValue UnaryOp::toSMT(State &s) const {
// may or may not be a constant
expr var = expr::mkFreshVar("is.const", one);
- s.addQuantVar(var);
+ s.addNondetVar(var);
return { std::move(var), true };
}
case FFS:
@@ -1105,12 +1109,12 @@ StateValue FpUnaryOp::toSMT(State &s) const {
switch (op) {
case FAbs:
- //TODO: enable in some strict FP mode: bitwise = true;
+ bitwise = true;
normalize = false;
fn = [](const expr &v, FpRoundingMode rm) { return v.fabs(); };
break;
case FNeg:
- // TODO: enable in some strict FP mode: bitwise = true;
+ bitwise = true;
normalize = false;
fn = [](const expr &v, FpRoundingMode rm) { return v.fneg(); };
break;
@@ -1398,7 +1402,7 @@ StateValue FpTernaryOp::toSMT(State &s) const {
fn = [&](const expr &a, const expr &b, const expr &c, FpRoundingMode rm0) {
auto rm = rm0.toSMT();
expr var = expr::mkFreshVar("nondet", expr(false));
- s.addQuantVar(var);
+ s.addNondetVar(var);
return expr::mkIf(var, expr::fma(a, b, c, rm), a.fmul(b, rm).fadd(c, rm));
};
break;
@@ -2332,7 +2336,7 @@ StateValue FnCall::toSMT(State &s) const {
sv2 = s.getAndAddPoisonUB(*arg, false);
} else {
sv = s[*arg];
- sv2 = s[*arg];
+ sv2 = s.eval(*arg, true);
}
unpack_inputs(s, *arg, arg->getType(), flags, std::move(sv), std::move(sv2),
@@ -2691,7 +2695,7 @@ static StateValue freeze_elems(State &s, const Type &ty, const StateValue &v) {
StateValue ret_type = ty.getDummyValue(true);
expr nondet = expr::mkFreshVar("nondet", ret_type.value);
- s.addFreezeVar(nondet);
+ s.addQuantVar(nondet);
return { expr::mkIf(v.non_poison, v.value, nondet),
std::move(ret_type.non_poison) };
}
@@ -3846,16 +3850,16 @@ StateValue Memcmp::toSMT(State &s) const {
if (is_bcmp) {
result_var = expr::mkFreshVar("bcmp_nonzero", zero);
s.addPre(result_var != zero);
- s.addQuantVar(result_var);
+ s.addNondetVar(result_var);
} else {
auto z31 = expr::mkUInt(0, 31);
result_var = expr::mkFreshVar("memcmp_nonzero", z31);
s.addPre(result_var != z31);
- s.addQuantVar(result_var);
+ s.addNondetVar(result_var);
result_var = expr::mkUInt(0, 1).concat(result_var);
result_var_neg = expr::mkFreshVar("memcmp", z31);
- s.addQuantVar(result_var_neg);
+ s.addNondetVar(result_var_neg);
result_var_neg = expr::mkUInt(1, 1).concat(result_var_neg);
}

MODIFY
ir/state.cpp
ir/state.cpp
@@ -437,7 +437,7 @@ void State::check_enough_tmp_slots() {
throw AliveException("Too many temporaries", false);
}
-const StateValue& State::operator[](const Value &val) {
+const StateValue& State::eval(const Value &val, bool quantify_nondet) {
auto &[var, val_uvars] = values[values_map.at(&val)];
auto &[sval, _retdom, _ub, uvars] = val_uvars;
@@ -467,7 +467,7 @@ const StateValue& State::operator[](const Value &val) {
if (is_non_undef) {
// We don't need to add uvar to undef_vars
- freeze_vars.insert(uvars.begin(), uvars.end());
+ quantified_vars.insert(uvars.begin(), uvars.end());
return simplify(sval, true);
}
@@ -488,14 +488,30 @@ const StateValue& State::operator[](const Value &val) {
if (hit_half_memory_limit())
throw_oom_exception();
+ unsigned undef_repls = repls.size();
+ assert(undef_repls > 0);
+
+ if (quantify_nondet) {
+ for (auto &var : sval.vars()) {
+ if (nondet_vars.count(var)) {
+ auto qvar = expr::mkFreshVar("nondetvar", var);
+ addNondetVar(qvar);
+ repls.emplace_back(var, std::move(qvar));
+ }
+ }
+ }
+
auto sval_new = sval.subst(repls);
if (sval_new.eq(sval)) {
uvars.clear();
return simplify(sval, true);
}
+ unsigned i = 0;
for (auto &p : repls) {
undef_vars.emplace(std::move(p.second));
+ if (++i == undef_repls)
+ break;
}
check_enough_tmp_slots();
@@ -1022,8 +1038,8 @@ void State::addQuantVar(const expr &var) {
quantified_vars.emplace(var);
}
-void State::addFreezeVar(const expr &var) {
- freeze_vars.emplace(var);
+void State::addNondetVar(const expr &var) {
+ nondet_vars.emplace(var);
}
void State::addFnQuantVar(const expr &var) {
@@ -1035,7 +1051,7 @@ void State::addUndefVar(expr &&var) {
}
void State::resetUndefVars() {
- freeze_vars.insert(undef_vars.begin(), undef_vars.end());
+ quantified_vars.insert(undef_vars.begin(), undef_vars.end());
undef_vars.clear();
}

MODIFY
ir/state.h
ir/state.h
@@ -112,7 +112,7 @@ private:
std::set<std::pair<std::string,std::optional<smt::expr>>> used_approximations;
std::set<smt::expr> quantified_vars;
- std::set<smt::expr> freeze_vars;
+ std::set<smt::expr> nondet_vars;
// var -> ((value, not_poison), ub, undef_vars)
std::unordered_map<const Value*, unsigned> values_map;
@@ -198,7 +198,8 @@ public:
/*--- Get values or update registers ---*/
const ValTy& exec(const Value &v);
- const StateValue& operator[](const Value &val);
+ const StateValue& eval(const Value &val, bool quantify_nondet);
+ const StateValue& operator[](const Value &val) { return eval(val, false); }
const StateValue& getAndAddUndefs(const Value &val);
// If undef_ub is true, UB is also added when val was undef
const StateValue& getAndAddPoisonUB(const Value &val, bool undef_ub = false,
@@ -240,7 +241,7 @@ public:
auto& getApproximations() const { return used_approximations; }
void addQuantVar(const smt::expr &var);
- void addFreezeVar(const smt::expr &var);
+ void addNondetVar(const smt::expr &var);
void addFnQuantVar(const smt::expr &var);
void addUndefVar(smt::expr &&var);
auto& getUndefVars() const { return undef_vars; }
@@ -263,7 +264,7 @@ public:
auto& getFnPre() const { return fn_call_pre; }
const auto& getValues() const { return values; }
const auto& getQuantVars() const { return quantified_vars; }
- const auto& getFreezeVars() const { return freeze_vars; }
+ const auto& getNondetVars() const { return nondet_vars; }
const auto& getFnQuantVars() const { return fn_call_qvars; }
void saveReturnedInput();

MODIFY
ir/type.cpp
ir/type.cpp
@@ -440,7 +440,7 @@ expr FloatType::mkNaN(State &s, bool canonical) const {
s.addPre(fraction != 0);
// TODO s.addPre(expr::mkUF("isQNaN", { fraction }, false));
if (!canonical)
- s.addQuantVar(var);
+ s.addNondetVar(var);
// sign bit, exponent (-1), fraction (non-zero)
return var.extract(fraction_bits, fraction_bits)

MODIFY
tests/alive-tv/fp/fabs.srctgt.ll
tests/alive-tv/fp/fabs.srctgt.ll
@@ -26,11 +26,11 @@ define void @tgt() {
%zero = fdiv float 0.0, 1.0
%inf = fdiv float 1.0, 0.0
%nan = fdiv float 0.0, 0.0
+ %posnan = call float @llvm.fabs.f32(float %nan)
- call void @f(float %one, float %one, float %zero, float %zero, float %inf, float %inf, float %nan, float %nan)
+ call void @f(float %one, float %one, float %zero, float %zero, float %inf, float %inf, float %posnan, float %posnan)
ret void
}
-
declare void @f(float, float, float, float, float, float, float, float)
declare float @llvm.fabs.f32(float)

MODIFY
tests/alive-tv/fp/fneg.srctgt.ll
tests/alive-tv/fp/fneg.srctgt.ll
-define half @src(half %x) {
+define void @src(half %x, half %y) {
%s = fsub half -0.0, %x
- ret half %s
+ call void @fn(half %s)
+ ret void
}
-define half @tgt(half %x) {
+define void @tgt(half %x, half %y) {
%s = fneg half %x
- ret half %s
+ call void @fn(half %s)
+ ret void
}
+
+declare void @fn(half)

MODIFY
tests/unit/fabs/fabs.opt
tests/unit/fabs/fabs.opt
@@ -8,12 +8,6 @@ Name: constant2
=>
%r = 2.0
-Name: nnan
-%negnan = fdiv float 0.0, -0.0
-%r = fabs float %negnan
- =>
-%r = %negnan
-
Name: fabs-twice
%k = fabs float %x
%r = fabs float %k

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -392,7 +392,7 @@ static expr encode_undef_refinement(const State &src_state,
// expressions. Since we are now rewriting those expressions, those
// variables *may* need to be refreshed.
if (!repls.empty()) {
- for (auto &v : state.getQuantVars()) {
+ for (auto &v : state.getNondetVars()) {
repls.emplace_back(v, expr::some(v));
}
}
@@ -419,8 +419,8 @@ check_refinement(Errors &errs, const Transform &t, State &src_state,
auto &uvars = ap.undef_vars;
auto qvars = src_state.getQuantVars();
qvars.insert(ap.undef_vars.begin(), ap.undef_vars.end());
- auto &src_freeze_vars = src_state.getFreezeVars();
- qvars.insert(src_freeze_vars.begin(), src_freeze_vars.end());
+ auto &src_nondet_vars = src_state.getNondetVars();
+ qvars.insert(src_nondet_vars.begin(), src_nondet_vars.end());
auto &fn_qvars = tgt_state.getFnQuantVars();
qvars.insert(fn_qvars.begin(), fn_qvars.end());

fabs/fneg/copysign are bitwise (again..)