change semantics of nsz to allow more undef propagation
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -279,10 +279,7 @@ static expr any_fp_zero(State &s, const expr &v) {
expr var = expr::mkFreshVar("anyzero", true);
s.addQuantVar(var);
- return expr::mkIf(is_zero,
- expr::mkIf(var, expr::mkNumber("0", v),
- expr::mkNumber("-0", v)),
- v);
+ return expr::mkIf(var && is_zero, v.fneg(), v);
}
static StateValue fm_poison(State &s, const expr &a, const expr &ap,

MODIFY
scripts/opt-alive.sh.in
scripts/opt-alive.sh.in
@@ -72,7 +72,7 @@ TV_SMT_TO=""
TV_SMT_STATS=""
if [[ @FOR_ALIVE2_TEST@ == 0 ]]; then
TV_REPORT_DIR=-tv-report-dir=@CMAKE_BINARY_DIR@/logs
- TIMEOUT="timeout 1000"
+ TIMEOUT="timeout 1500"
TV_SMT_TO=-tv-smt-to=10000
TV_SMT_STATS=-tv-smt-stats
fi

ADD
tests/alive-tv/fp/select-nsz.srctgt.ll
+define float @src(float %x, float %y, i1 %b) {
+ %ny = fneg float %y
+ %s = select nsz i1 %b, float %x, float %ny
+ %r = fneg float %s
+ ret float %r
+}
+
+define float @tgt(float %x, float %y, i1 %b) {
+ %x.neg = fneg nsz float %x
+ %a = select nsz i1 %b, float %x.neg, float %y
+ ret float %a
+}

change semantics of nsz to allow more undef propagation