Add Machine Float support to K framework

[sdasgup3]

Problem

For supporting AVX/SSE2 instructions, I should have the support for 128 xmm registers, where the 128 bits can be interpreted as any one of he following:

2 64 bit doubles or
4 32-bit floats or
1 128 bit int or
2 64 bit ints or
4 32 bit ints or
8 16 bit ints or
16 8-bit ints or

The plan is to use mi(128,I) for those registers and whenever I need to interpret it as floats (or double), I will extract each 32 (or 64) bit chunks and get the corresponding float (or double).

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

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.

[sdasgup3]

Added the pull request to K repository
runtimeverification/k#2383

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