K-user mailing list

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

Hi Sandeep,

The builtin INT module has the bitwise operators:

https://github.com/kframework/k/blob/master/k-distribution/include/builtin/domains.k#L312-L319

Also, we have MINT module that presents machine integers of arbitrary bit width represented in 2's complement:

https://github.com/kframework/k/blob/master/k-distribution/include/builtin/domains.k#L810-L1002

To use MINT module, you may need to import it in your semantics module, like:

imports MINT

INT module is automatically imported by default.

Please let us know if you need more help.

Best,

Daejun

On Nov 17, 2017, at 2:14 PM, Sandeep Dasgupta <sdasgup3 AT illinois.edu> wrote:

Hello All,

I am new to K and trying to define the semantics of x86-64 and I wil appreciate some help on the following issues:

Issue:

The semantic rules for assembly language need various representations of integers and various bitwise operation between those.
For example: addb $1, %al; adds 1 to lower 8 bits of hardware register %rax in 64 bit machine and does not affect the any higher bits.
I  would like have built-in operators like +Int8 and "ability to mask out the relevant bits"  which implements the semantics of above instruction. For that I might need the bitwise operators which I failed to find.
    
Can somebody please point me to some relevant examples or places where can I get some hint on that?

Thanks
Sandeep