The way Alive2 is built, it parses LLVM-IR then implements a lowering phase to Alive2's IR, which is finally lowered to constraints and submitted to Z3. Those authors are correct: We need only identify a lowering from SIL to Alive2's IR. There will be some interesting challenges doing so, since SIL is a much, much higher-level IR than LLVM. But you may also find certain operations much easier to implement as a result.
I think there is a reasonable "core" cadre of SIL instructions that one could focus on. For example, a candidate could choose to ignore (as in, treat as no-ops/fresh defs from Alive's perspective) ownership instructions, access enforcement instructions, and a lot of the builtins entirely. Some of the more exotic instructions we need like the ones for indexing various kinds of buffers could also be ignored. A very reasonable version of this tool could start by tracking the provenance of SIL undef and try to focus on how different kinds of optimizer transforms propagate it with respect to different combinations of other instructions. You would probably start by modeling the lowering of undef, copy_value, instructions for generating constants (the *_literal instructions). Then, I recommend searching SIL.rst for the places it mentions undefined behavior by name and modelling the lowering of those instructions one by one. As for challenges, I don't have a clear idea for how to lower the constraints for ownership to Alive2, but exploring that will certainly be an exciting challenge.
It doesn't exist! However, I have tried this by hand a few different ways, and it really depends on which way you're most comfortable with expressing this kind of infrastructure. For example, you could choose to build the tool in C++, so you could link the SIL parser directly. You could choose to build the tool in Swift, so you'd have to go a custom route. There, you could rewrite the SIL parser (it's not all that difficult, just a bit tedious) with respect to whatever subset of instructions you can lower and verify. Or you could explore various kinds of parser-generators. @harlanhaskins built a tool we used for a language project of ours that lowers a pure Swift description of an AST into libSyntax nodes. You could wind up producing "libSILSyntax" in the process! Finally, LLVM also has a bunch of macros you can use to build a C API on top of C++, so you could potentially do this by wrapping libSIL and the SIL Parser in a C interface that could possibly get lifted into Swift if necessary.
Whatever path you choose, bear in mind it will have an impact on the way you interact with Alive2 and Z3. There are bindings to Z3 in Swift you can find on Github, though they are incomplete with respect to Alive2's lowering. There are no bindings to Alive, so those would have to be generated as well if this were done in Swift.
I think this is a big open-ended project that can be taken as far as the candidate is comfortable taking it. If all that happens at the end of the day is we learn how to parse a subset of SIL in Swift, that's still quite the accomplishment. If we can lower a subset of SIL to Alive2, all the better. I would say it's best to pick an area of verifications you're interested in building and try to figure out where your comfort level with the different implementation options you have here lies. That will direct you towards a solid implementation strategy.
