More instruction support with Remill

[pgoodman]

Remill has a large (and growing) set of well-tested x86 and x86-64-bit instruction semantics support, implemented as C++ functions, and compiled to LLVM bitcode. It supports large portions of the X87, MMX, SSE, and AVX(2) instruction sets, and has been coded to eventually support AVX512.

It is advertised as a static binary translator, though I use it for DBT is some cases.

As the creator and lead developer of Remill, I would be very interested in helping the STOKE team support more instructions using Remill.

[bchurchill]

You might take a brief look at src/validator/README.md although it's a bit old and there's not a lot of detail. The key thing to do is to add another 'handler' in the /src/validator/handlers folder that implements the circuits you want to support. You'll need to implement some kind of conversion between Remill semantics and our interface there.

[stefanheule]

It seems the main question is whether there is a formal (SMT) semantics for LLVM bitcode that one could use. If so, this should mostly be a matter of matching up different CPU state/instruction encodings.