Segmentation fault in floating point theory

[martin-neuhaeusser]

Attached is a log that produces a segmentation fault (with Z3 commit id 62a54cf1) The example stems from a test case of verifying floating point programs that involve comparison with NaN.

float_bug.zip

[wintersteiger]

That was indeed a bug, thanks for the report!

Note that fp.to_ieee_bv is a non-standard, Z3-only function which was used as a hack before the FP standard was finalized, so its use is discouraged. The SMT FP theory definition has this to say on this topic:

:note "There is no function for converting from ( FloatingPoint eb sb) to the corresponding IEEE 754-2008 binary format, as a bit vector ( BitVec m) with m = eb + sb, because ( NaN eb sb) has multiple, well-defined representations. Instead, an encoding of the kind below is recommended, where f is a term of sort ( FloatingPoint eb sb):

(declare-fun b () ( BitVec m)) (assert (= (( to_fp eb sb) b) f)) "

[martin-neuhaeusser]

Hi Christoph, thanks for the bug fix and the hint to the SMTLIB standard!

Perhaps I am missing some important point here, but I find the encoding proposed in the standard very cumbersome from a practical point of view. Having to use an assertion each time that one intends to map a floating point term to a bit-vector complicates the construction of terms very much. In fact, it breaks our entire architecture. Am I correct that one cannot build a term that involves such a conversion alone and that one has to interact with the solver to introduce "helper variables" such as b accompanied by an additional assertion for each conversion from FP to BV?

The only alternative that I see is to axiomatize the to_ieee_bv operation using an uninterpreted function symbol. But this obviously can't be the solution for a "simple" conversion between theories either (actually, Z3 reports unknown already when checking the example below).

(declare-fun convert_to_ieee_bv ((_ FloatingPoint 8 24)) (_ BitVec 32))
(assert (forall ((x (_ FloatingPoint 8 24))) (= x ((_ to_fp 8 24) (convert_to_ieee_bv x)))))

Therefore I am very much in favor of having an operator such as to_ieee_bv for converting from floating-point numbers to bit vectors. For the case of a conversion of NaN into a bit vector, would it be possible to leave the significand bits and the sign bit unspecified but to enforce a 1-bit vector for the exponent? Doesn't this encode the equivalence class for NaN correctly?

Currently, the operator fp.to_ieee_bv as implemented in Z3 yields the bit-vector term 0 if applied to NaN. Is this intended? The code snippet below reproduces the behavior in Z3:

let () =
  let ctx = Z3.mk_context [] in
  let float_nan = Z3.FloatingPoint.mk_nan ctx (Z3.FloatingPoint.mk_sort_32 ctx) in
  let ieee_bv = Z3.FloatingPoint.mk_to_ieee_bv ctx float_nan in
  Printf.printf "mk_to_ieee_bv(%s) = %s; after simplify: %s\n"
    (Z3.Expr.to_string float_nan)
    (Z3.Expr.to_string ieee_bv)
    (Z3.Expr.to_string (Z3.Expr.simplify ieee_bv None))

I am aware that the SMTLIB standard states that fp.to* are unspecified for NaN; but I cannot see the reason for that and simplifying to a zero bit vector as Z3 currently does, seems to be wrong anyways.

As a side node: The MathSAT5 API offers an operator similar to Z3's to_ieee_bv (see the function msat_make_fp_to_bv here http://mathsat.fbk.eu/apireference.html#a26a0d2d2ead14bb1f538ccd4f24517f4).

[wintersteiger]

Hi Martin,

Yes, the SMTLIB-proposed encoding is a bit cumbersome, but ultimately not that hard to do. During all other encoding is going on, I usually keep a vector of expressions for "side conditions" where all such additional things go, and in the end when everything is done, I add all those additional things to the solver/goal/etc. You do have to introduce variables (like b), but they are not much more expensive than asking the solver to introduce variables and then hide their names (e.g., after FPA to BV conversion, the result is virtually identical).

Using quantifiers to axiomatize these functions is definitely a bad idea, way too expensive and fragile (Z3 can solve your formula, but will not do it with the default options (mbqi instantiation limit too small) and it's not fast).

I really wouldn't want to add another special instruction or to modify the existing semantics of to_ieee_bv. In fact, I'd much rather remove to_ieee_bv and then add whatever the SMTLIB people decide to use; FPA is complicated enough. Also, do not assume that SMT solvers use the encoding into bit-vectors that is proposed in the IEEE standard - one of the objectives of the SMT standard was not to prescribe any encoding, such that solvers are free to use whatever thechniques they think make sense. Z3 happens to use a similar encoding (but not identical), so for me adding to_ieee_bv was easy, but for others it may be much harder to add, than it is to ask you to use additional variables and assertions :)

Also, note that in SMT-FP there is always exactly one NaN, and it has no predefined bit-vector equivalent (since there is no SMT-compliant function to translate it). Also, the IEEE standard only proposes encodings for particular float types (half, single, double, quadruple, etc), but SMT FP allows any number of significand/exponent bits, and I'm sure Z3 still contains bugs that are only triggered by weird combinations for which the "generalized" IEEE encoding is a disadvantage.

The implementation of to_ieeebv is almost surely buggy somewhere as it has undergone very little testing. The fact that it returns 0 for NaN is full expected though. Z3 supports two ways of treating undefined results for all fp.to* functions: Either keep an uninterpreted function, or just return 0 (similar to the "hardware interpretation" of bit-vector operations). At this point, just returning 0 is the default operation, but I may change that now that I have at least 1 example of a person who uses it. The magic option is rewriter.hi_fp_unspecified which is true by default. Of course, if you disable this option, Z3 will not be able to use a pure SAT solver anymore and it will have to fall back to a solver that supports uninterpreted functions (we do have a roughly "practical" solution for unspecified bit-vectors by eager ackermannization, but that's not available for FPA yet).

[wintersteiger]

(And yes, there is a bug in to_ieee_bv when rewriter.hi_fp_unspecified=false; working on it :) )

[martin-neuhaeusser]

Hi Christoph,

If it was only the encoding of a query to the solver, I'd be fine with it. But doesn't an encoding with side conditions as it is proposed by the SMTLIB standard break many common operations on terms? Looking only at the resulting term after the encoding, the free variable b is completely unrelated to the floating-point term f. Therefore, the encoding renders syntactic term transformations such as weakest preconditions, strongest postconditions, term simplifications, etc. invalid. This is a pitty, as we are heavily relying on many such operations and interleave them with term simplifications of the underlying SMT solver.

A solution that might work for us is to introduce an interpreted conversion operator in our own term representation (which we have, anyways) and encode it in the way proposed by the SMTLIB standard whenever such a term becomes asserted into the SMT solver (i.e. directly before the check_sat). In this way, our predicate transformers would remain correct. However, we would still loose the ability to sporadically ask the SMT solver to simplify the intermediate results during, e.g. a wp computation (we map our terms to Z3 terms, let Z3 simplify the term, and map the result back into our representation).

Do you know a solution or an approach to tackle this? Are there other cases in the SMTLIB standard that require such an encoding using "side conditions"?

Of course, this question is rather about the SMTLIB standard than about Z3. Sorry for that!

[delcypher]

@martin-neuhaeusser @wintersteiger I've been reading this discussion with interest.

I have not needed to use Z3's mk_to_ieee_bv yet but I suspect I will soon and this issue with NaNs looks a little worrying.

I understand that because there are multiple bit representations of NaN there cannot be a SMT-LIB function mk_to_ieee_bv as a function cannot map one value (i.e. NaN) to multiple different values.

I have a suggestion for handling this in Z3 and in SMT-LIB. A function fp.to_ieee_bv could be added that takes an additional argument which is the value that should be returned if the floating point argument is a NaN.

e.g.

(declare-fun x() Float32)
(assert (fp.isNaN x))
(assert (= (fp.to_ieee_bv x #x7fc00000) #x7fc00000))
(check-sat)
sat

(declare-fun x() Float32)
(assert (fp.isNaN x))
(assert (distinct (= (fp.to_ieee_bv x #x7fc00000) #x7fc00000)))
(check-sat)
unsat

and another way of representing NaN

(declare-fun x() Float32)
(assert (fp.isNaN x))
(assert (= (fp.to_ieee_bv x #x7f800001) #x7f800001))
(check-sat)
sat

To me this seems like the right solution as it gives the user control of what to return if the input is a NaN rather than forcing the implementer of an SMT solver to make an arbitrary choice on which bit pattern should be returned when given a NaN.

[wintersteiger]

@martin-neuhaeusser, @delcypher: Both your arguments make sense, but they are an SMT issue, not a Z3 issue. There is a Google group for this kind of discussion called "smt-fp".

@martin-neuhaeusser: Yes, there are other cases of the same problem: For instance, bit-vector divison (and remainder) by 0 is unspecified in SMT, but in many cases that "hardware interpretation" (a fixed number) is fine, regardless of which number is divided by 0. Just recently we added an eager ackermannization tactic to our default tactic for QF_BV which is often able to get rid of those uninterpreted functions, so that we can then use a pure (and fast) SAT solver instead of the (old, slow) SMT solver that supports uninterpreted functions. The same will also work for many cases of FP, but it's not hooked up yet.
And yes, I totally agree, this complicates many things and makes seemingly trivial operations expensive and there was much discussion about this topic (and related ones) before the FP standard was finalized.

For the obvious reasons I have kept to_ieee_bv and a global flag that determines whether all FP conversions are unspecified for NaN (and related) or a fixed numeral (usually 0) (the option rewriter.hi_fp_unspecified switches between the two). An additional function and/or flag is thus not necessary.

@delcypher: No, SMT-FP numbers have exactly one NaN, not multiple, and that single NaN does not have any bit-vector representation (there is no to_ieeebv in the standard, and the value reported in models is `( NaN 8 24), not#x7f800001`). The idea at the time was that FP-solver implementors are not forced to use a bit-vector representation of FP numbers internally (Z3 does currently uses bit-vectors, but not always biased-exponent bit-vectors; MathSAT has both, a bit-(vector)-blaster and the ACDCL solver that, as far as I understand at least, doesn't use bit-vectors).

I'm currently fixing to_ieee_bv for NaN inputs. Apparently I skipped that one back then when I added the unspecified operations, so it didn't actually have "unspecified" behaviour. Since @martin-neuhaeusser was the first one to ask for it, I'll now implement exactly what he suggested, i.e., for single precision floats, `#x7f800001 when rewriter.hi_fp_unspecified=true and #b*11111111*...*1 otherwise.

[delcypher]

@wintersteiger

@delcypher: No, SMT-FP numbers have exactly one NaN, not multiple, and that single NaN does not have any bit-vector representation

That's not what I said. I know there is only one representation of NaN for SMT-FP numbers. What I was (trying) to say was that there are multiple bitvector patterns that IEEE-754 considers to be NaN and this is why SMT-LIB does not have a function to convert a SMT-FP to an IEEE-754 bit-vector. What I was suggesting is that a way around this problem is to have the conversion function take an extra argument which is the value that should be returned by the conversion function if the SMT-FP number being converted is a NaN. You are right though this probably ought to be discussed on the smtlib mailing list.

[delcypher]

@wintersteiger Hmm I can't join the smt-fp mailing list. It's public but there's no "join" button like other google groups. Is this list closed to new members?

[wintersteiger]

@delcypher: Yes, definitely one for the SMT list/group. I'll implement whatever the standard says, so far it just said nothing, and since we need unspecified for other operations (fp.to_* but also fp.min/fp.max) it doesn't make much of a difference.

Aside, the additional flag is not really needed at all. Guarding the expression explicitly is easy to do and it forces the user to chose whatever interpretation he prefers. Thus,

to_ieee_bv(x, flag)

becomes

ite(fp.isNaN(x), whatever-you-prefer, to_ieee_bv(x))

[wintersteiger]

@delcypher: It says "shared publically" when I go to the groups webpage, but I'm not absolutely positive that means everybody can join. They might have closed it when the standard was finalized expecting that users will use the usual SMT mailing list.

[martin-neuhaeusser]

@delcypher: We also tried to guard the to_ieee_bv function by an ITE construct similar to the proposal of Christoph. We simply choose one IEEE encoding for NaN. I will have to look more deeply into this, but I guess that for our specific use-case, this is more or less fine: Our memory model requires us to "store" a floating point term as a bit vector; but whenever it is "read", it is converted back into the floating point theory and hence, into its unique NaN representation.

In general, however, I wonder about this choice in the standard. @wintersteiger: Please keep the to_ieee_bv function in Z3. It is very precious ;-)

[wintersteiger]

@martin-neuhaeusser: No worries, I'll keep it at least until a good replacement for it is added to the SMT standard :)

[wintersteiger]

There were a few other things to fix arsound this one, but it should now work as intended.

rewriter.hi_fp_unspecified will remain on for now, but I will soon switch this off by default, so that we get the unspecified semantics by default.