Floating point: Inspecting NaN payloads

[LeventErkok]

@wintersteiger

I do realize that SMT-Lib floating point types have only one NaN value; but I'm pretty sure z3 must be keeping track of the payload for internal purposes. I've a few use cases (admittedly curiosity at this point), where I'd like z3 to show me the payload of a NaN. Would it be possible (via some pretty-printer option perhaps), to see the NaN payloads in models?

I came up with the following "work-around:"

(set-logic QF_FPBV)
(declare-fun x () (_ FloatingPoint  8 24))

; Track the bits of x:
(declare-fun bitsOfX () (_ BitVec 32))
(assert (= x ((_ to_fp 8 24) bitsOfX)))

; make it a NaN and put an interesting payload:
(assert (not (fp.eq x x)))
(assert (= ((_ extract 22 22) bitsOfX) #b1))

(check-sat)

; Get the payload:
(get-value (bitsOfX))

; But can we get it directly from x as well, without the need for bitsOfX tracking?
(get-value (x))

Right now this prints:

sat
((bitsOfX #x7fc00000))
((x (_ NaN 8 24)))

But it comes at the cost of creating an extra variable for each float (bitsOfX above), regardless whether it may end up being NaN or not and all the extra management the upper layers have to do with the extra assert etc. The general use case I'm thinking of are functions that I'm working on that set and conserve NaN payloads as in x86 semantics; which allows for tracking the "source" of anomalies in certain numerical analysis scenarios.

I'm wondering if it would be possible to add a pretty-printer option so NaN's can be displayed with payload. I'm imagining something like:

(set-option :pp.fp_show_nan_payloads true)
(get-value (x))

and z3 would respond

((x ((_ to_fp 8 24) #x7fc00000)))

I found that you already support pp.fp_real_literals, which does print things like:

((x ((_ to_fp 8 24) RTZ 0.5 -126)))

But it doesn't seem to work on NaN values. Perhaps it can be repurposed to do this for NaN values too, with a more intuitive bit-pattern input (as conversion wouldn't make sense); but I'm perfectly happy with a separate pp setting as well.

[NikolajBjorner]

You would have to change mpf.cpp line 622 and ast_smt2_pp.cpp line 240 to take use_fp_real_literals to change the output.

[LeventErkok]

@NikolajBjorner

I've played around with this a bit, but without success. Line 622 of mpf.cpp you pointed out seems to be in the floating-point multiplier; and there are many other mk_nan calls around. Do you mean each one of these calls need to change to account for the payload? Looking at the definition of mk_nan also reveals it simply has no notion of a payload in there. I suspect it has to be explicitly kept track of; not as simple as I originally thought perhaps. I wish @wintersteiger opined, though he seems busy with other stuff.

[NikolajBjorner]

The relevant place would be code that converts an mpf to a string. It currently handles the NaN, +oo, zero cases differently from others. This code gets used in ast_smt2_pp, which would have to be updated.

std::string mpf_manager::to_string(mpf const & x) { std::string res; if (is_nan(x)) res = "NaN"; else { if (is_inf(x)) res = sgn(x) ? "-oo" : "+oo"; else if (is_zero(x)) res = sgn(x) ? "-zero" : "+zero"; else { res = sgn(x) ? "-" : ""; scoped_mpz num(m_mpq_manager), denom(m_mpq_manager); num = 0; denom = 1;

[LeventErkok]

I think the code is actually here:

https://github.com/Z3Prover/z3/blob/master/src/ast/ast_smt2_pp.cpp#L233-L292

I did take a shot at implementing a new pretty-print option, called fp_show_nan_payloads, and it does indeed work "correctly," in that it prints the payloads just fine:

https://github.com/LeventErkok/z3/commit/57d2101f660cb9cfd9eac6e52af79b58f5d32ad7

But it's not correct in the sense that the payloads all seem get squashed; i.e., my original thought that z3 actually keeps track of NaN payloads explicitly and only discards them during printing doesn't seem to be correct. (There's no reason why that should be correct, but it was a hopeful guess.) In particular, each time an FP operation is performed with a NaN, it'd have to propagate the correct NaN payload through the operation. My reading of the code is that this is not what's happening. Whenever it deduces a NaN, it simply creates a generic value, instead of propagating the payload. And SMTLib semantics is completely OK with that; it's just not what x86 does.

So, it seems properly doing this would require way more than just tweaking the printer. It's really impossible for me to tell what the actual cost of doing this would be, and admittedly the ROI seems very small.

[NikolajBjorner]

Whenever it deduces a NaN, it simply creates a generic value, instead of propagating the payload

Right, I started suspecting that. Generally, I have the impression now that assuming something about payloads breaks abstraction barriers so it would not be a good design choice.

[LeventErkok]

Agreed; this is very little ROI. If the FP solver was to be reconstructed from scratch, it might be a good idea to track NaN payloads to enable more precise x86 behavior analysis; but adding it on top of the existing code base seems too risky for little return. Thanks for looking into it though!

[wintersteiger]

Sorry, this one passed right by me and I just found it accidentally. I don't understand what exactly you mean by "payload". NaN values in models are provided exactly as you'd expect. The SMT standard/theory does not prescribe a bit-wise representation though, so none such is provided by the theory. However, we do have the Z3-only unsound-imprecise extension fp.to_ieee_bv, which, for NaNs should give you the IEEE754 representation (and for other values, but I make no claims regarding correctness to avoid having to fix it :-))

[LeventErkok]

Thanks Christoph.

The motivation was modeling signaling/quiet NaN's and NaN propagation through various FP operations. SMTLib FP logic has only one NaN as you pointed out, but IEEE754 (at least as implemented by x86), has both quiet and signaling NaNs, and FP operations propagate the actual bit patterns according to the following rules:

My motivation was to see if I can model this behavior. The easiest thing to do would be, of course, if z3 already did this internally and perhaps I can somehow reach in and get the payload out of the NaNs. But looking at the code convinced me that you actually do not implement this. (Nor you are required to of course, per the SMTLib FP logic.) That's what I wanted to confirm.

[wintersteiger]

That's right, we do not implement that, we implement the SMT FP theory. I think it would be a major effort to add support for that internally, but it's not impossible. Did you find a solution to do that without modifying the theory solver/bitvector translation?

[LeventErkok]

I thought about creating a layer of functions, where I would represent a float with a pair of FP and 32-bit vector (and a double by an FP and a 64-bit vector), explicitly tracking bit-patterns in each case. But there are so many functions, and the pair-wise encoding gets out of hand fairly quickly; so I'm concerned about scalability and code maintenance. I think it's doable outside the solver this way, but too much work for little benefit really. Something to try on a rainy afternoon!