K-user mailing list

["Park, Daejun" <dpark69 AT illinois.edu>]

You can implement a new hook using `mpfr-java` library, specifically the following `BigFloat` constructor:

https://github.com/kframework/mpfr-java/blob/a24d33c7589e285e840eaaba74368581dc15ebb3/src/main/java/org/kframework/mpfr/BigFloat.java#L356

where (for single-precision case):

@param `sign`: true/false depending on the sign bit

@param `exponent`: `uint(e1...e8) - 127` where `e1...e8` are the exponent bits.

@param `significand`: `uint(1 s1...s23)` where `s1...s23` are the significant bits (note that the prepended bit `1`).

or `unit(0 s1...s23)` if `uint(e1...e8) == 0`.

(for double-precision, replace 8 by 11, and 23 by 52 in the above)

Best,

Daejun

On Dec 7, 2017, at 10:22 AM, Sandeep Dasgupta <sdasgup3 AT illinois.edu> wrote:

Hello k Team,

I am upto defining x86-64 semantics in K.
I need some help with the following requirement.

For supporting AVX/SSE2 instructions, I should have the support for 128 xmm registers, where the 128 bits can be interpreted as
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

My 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).

In the domain.k we have FLOAT but it does not seem suitable for for the purpose. Also the int2float gives the float equivalent of an int like Int2Float(5, 53, 11) gives 5.0.

Can you please give me some suggestion or pointers to address this ? 

Thanks
Sandeep