K-user mailing list

[Sandeep Dasgupta <sdasgup3 AT illinois.edu>]

Hello Daejun,
Thanks for the reply.

A. I have implemented 2 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.

B. Both are heavily tested. Soon sending the pull request.




Thanks again,
Sandeep

On 12/07/2017 01:38 PM, Park, Daejun wrote:

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