[SMT-LIB] Idea: fp.to_ieee_bv as extension to FloatingPoint theory

[Levent Erkok]

I think this would be a nice addition, making high-level translators much
easier to work with. I can definitely use this function in my own work.

Regarding partiality: We already have that issue with respect to other
floating-point conversion functions: fp.to_sbv, fp.to_ubv, and fp.to_real
are all unspecified for NaN and infinity input values. I'm actually quite
fond of that: There's really no good reason to fix the result of these
functions for NaN and Infinity. Likewise, I'd suggest that to_ieee_bv would
remain unspecified for NaN as well, since the payload will not be unique.
(Note that the exponent *will* be unique, but not the mantissa; so that
should be the case in the translation.)

-Levent.

On Fri, Apr 7, 2017 at 4:55 AM, Delcypher <delcypher at gmail.com> wrote:

> Hi,
>
> This follows on from a discussion on the smt-comp mailing list [1].
> This is a proposal to add a function `fp.to_ieee_bv` to the
> FloatingPoint theory [2].
>
> # TL;DR
>
> `fp.to_ieee_bv` is a total function (based on Z3's `fp.to_ieee_bv`)
> that takes a floating point sort and as output gives the binary
> IEEE-754 encoding of that floating point sort as bitvector.
>
> # Why do I want this?
>
> The reason for wanting this function is in my tool I have to handle
> bitcasts in C programs. In these programs bitcasts between integers
> (i.e. BitVector sort) and floating point variables may occur. An
> example is the `signbit()` function that examines the sign bit of the
> floating point variable.
>
> The FloatingPoint theory standard currently suggests to handle this by
> introducing a fresh bitvector variable and an additional assertion
> that the fresh bitvector converted to a floating point sort is equal
> to the expression that I wish to convert to Bitvector sort.
>
> I find this rather cumbersome. It makes queries harder to read and write.
>
> # fp.to_ieee_bv
>
> The function `fp.to_ieee_bv` converts a floating point sort to a
> bitvector sort using the IEEE-754 binary encoding. To be a total
> function if the argument to the function is a NaN it picks the
> encoding of a quiet NaN (from IEEE-754 2008) with the following
> additional constraints
>
> - The sign bit is 0
> - In the trailing significand field only the most significant bit is
> set 1, the rest are set to zero.
>
> This choice is arbitrary and I'd happy for it to be something else
> provided there are good reasons.
>
> Although we could make `fp.to_ieee_bv` a partial function (i.e. have
> it undefined for NaN inputs) I worry we'd hit issues like we have with
> `bvudiv` (i.e. division by zero).
>
> This function provides a convenient way to do conversion that works
> well provided the user is willing to accept only a single encoding for
> NaN is considered. If the user wants multiple encodings to be
> considered they would need to use the fresh variable approach
> suggested in [2].
>
> # Final thoughts
>
> I don't feel that strongly about this idea so I won't fight for it but
> I think it would be good to discuss it.
>
>
> [1] http://cs.nyu.edu/pipermail/smt-comp/2017/000436.html
> [2] http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml
>
> Thanks,
> Dan
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>