K-buitin Floats do not provide any hooks to convert a specific bit pattern into a single precision or double precision floating point value.

[sdasgup3]

Requirement

We need the ability to do the conversion as shown in examples:

    Example 1:

    bit-vector: 32' 01000001 01000110 00000000 00000000 === MInt(32, 1095106560)
        convert to or from
    Float(single precision): 12.375f.

    Example 2:
    bit-vector: 64' 0b0100000000101000110000000000000000000000000000000000000000000000 === MInt(64, 4623156123728347136)
        convert to or from
    Float(single precision): 12.375d.

Commit:

Provides two following two hooks:

1. float2mint(Float F, Int W): Converts a float point value F(single or double precision)  to a BitVector or MInt of bitwidth W.
2. mint2float(MInt MI, Int Precision, Int Exponent): Converts a Bitvector or MInt to an single or double precision float point value.

The hooks are tested extensively using corner cases.

Note

• The available hooks like float2Int or int2Float converts between the float and its integer equivalent and hence not suitable. From example 2, int2Float(4623156123728347136) gives 4.623156123728347136 e+18

• Some peculiarities of exiting mpfr library support:

  1. While creating the BigFloat using BigFLoat constrcutor, we need to pass the unbiased exponent (mint(e1...e8) - 127) as the callee expects that. This is more evident from https://github.com/kframework/mpfr-java/blob/a24d33c7589e285e840eaaba74368581dc15ebb3/src/main/java/org/kframework/mpfr/BigFloat.java#L357 where exponent is compared with mc.minExponent(-126) and mc.MaxExponent(+127).

  2. For zero, BigFloat constructor expects -127 as opposed to -126 (a special exponent used for +/- zero). Inside the constructor, its converted back to 126. This is used to easily distinguish =/- zero and sub normals value from others. https://github.com/kframework/mpfr-java/blob/a24d33c7589e285e840eaaba74368581dc15ebb3/src/main/java/org/kframework/mpfr/BigFloat.java#L364

Please accept the request if it seems suitable to the k-developers.

[kframework-bot]

Can one of the admins verify this patch?

[daejunpark]

Jenkins: ok to test