search

kframework / X86-64-semantics

Semantics of x86-64 in K
Other
137 stars 11 forks source link

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

Open aa755 opened 3 years ago

aa755 commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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 commented 1 year ago

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

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