Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

can we use this work as a C++ x86 emulation library? #12

Open
aa755 opened this issue Feb 5, 2021 · 3 comments
Open

can we use this work as a C++ x86 emulation library? #12

aa755 opened this issue Feb 5, 2021 · 3 comments

Comments

@aa755
Copy link

aa755 commented Feb 5, 2021

We are looking for a trustworthy C++ library to emulate x86 instructions. Is it possible to use this work? Can the semantics in K be compiled to C/C++? if not, is there a fast C++ K interpreter?

@ehildenb
Copy link
Member

ehildenb commented Feb 5, 2021

It should be possible, yes. @dwightguth or @theo25 would know more about the details.

What I'm not sure about is whether this semantics has been updated to use the LLVM backend. Currently it likely supports the OCaml backend. That means the K definition in compiled into OCaml code which implements an x86 interpreter.

If you update it to the LLVM backend (which may or may not be a lot of work), then you will have a much faster x86 interpreter.

@dwightguth
Copy link
Member

Pretty sure this never actually made it off the java backend. So there's a lot of maintenance to do here before you could reasonably use it with modern K. It's probably not worth pursuing if you want an out of the box solution.

@amelieled
Copy link

Are you sure @dwightguth ? One can read the following lines in the README:

cd X86-semantics/semantics
../scripts/kompile.pl --backend java

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

4 participants