[GSoC 2021] Alive2 for SIL

Hello all, I'm Justin, a third-year computer science student at the University of Rochester interested in programming languages, formal verification, and the "Alive2 for SIL" GSoC project proposal mentored by @codafi !

After looking into the proposal for a bit, I have some questions :slight_smile:

  1. The proposal indicates that the project will involve re-implementing Alive2 for SIL instead of LLVM-IR. However, during this talk the authors of Alive2 indicate that this could be done by simply mapping SIL to Alive2's IR. What're the community's thoughts on this? Is this the case, is it better to start from scratch, or is this something that would be investigated during the project?

  2. The proposal says that "the tool does not need to be complete". I'm assuming that this means the candidate will identify a subset of SIL to attempt to verify. Are there ideas about which subset of SIL should be used to start with or which parts of SIL that may be difficult to verify? Also, I've found these two pieces of documentation for SIL (one two). If y'all have recommendations for other things to check out, please post a link!

  3. The project proposal says that the project could either be implemented as "a pure Swift tool or a C++ tool that integrates directly with the Swift compiler libraries". I've found the C++ SIL parser in the compiler, but I haven't been able to find Swift bindings to it. Does anyone know if one exists / where it is? (Is it correct to assume that writing a parser for SIL wouldn't be a part of the project?)

  4. @codafi do you have other ideas or thoughts about the project that you want to share that you didn't include in the project proposal or have had since submitting the proposal?

2 Likes

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.

1 Like

Thanks for the responses @codafi! After doing some more research, I have some more follow-ups and questions.


What are the different areas of verification? Is one area tracking the provenance of `undef`` and another tracking the undefined behavior introduced by different SIL memory operations (e.g. operations of raw pointers)?


I think I'm more interested in verifying SIL optimizations than in building a SIL parser for Swift. Would it make sense for the project to use the existing C++ SIL parser (and thus build the tool entirely in C++) to avoid spending time building a SIL parser for Swift and FFI bindings to Alive2?


Do you think that this would be a good deliverable for the entire GSOC project or more of a milestone along the way? If it's the latter, then what do you think a good deliverable would look like? Could it just be the list of SIL optimizations that we are able to verify or SIL instructions that we can encode in Z3?

I'm trying to gauge how much I will be able to do so that I can set realistic deliverable and timeline goals for the project.


After spending time looking through Alive2's IR, I'm having trouble seeing the benefits of using it as opposed to working directly with Z3. Alive2's IR seems to be closely related to LLVM IR. The instructions Alive2's IR supports are very similar to LLVM IR instructions. By using Alive2's IR would you lose the ability to verify something by lowering to it instead of lowering directly to Z3? Would SIL fit well into Alive2's IR or would Alive2's IR need to be adjusted to because it was designed with LLVM IR specifically in mind?

Is this something that I would spend time looking into as a part of the project?


When I finish my project proposal would you be open to reviewing it?

@codafi, just wanted to ping you again in case the previous notification slipped by.

Hey, sorry for letting this sit idle for so long. I'm going to make a more conscious effort to follow along with the discussions on evolution during this busy season.

Undef analyses were something I suggested because it's a large part of the early verification powers of Alive and Alive2. Today, they are incredibly powerful tools that help LLVM optimization pass authors reason about undef and poison, which have lots of subtleties. The point being it's well-trodden ground that can help bring a tool up quickly since we'd have something to compare it to, but there are other areas worth pursuing here.

Absolutely. If you're comfortable with C++, let's build this in C++!

It would be a stellar deliverable. If we can stand up this tool and run it across a well-defined subset of SIL, no matter how small, that's a win in my book.

I think you would lose the ability to do higher-level kinds of analyses in the future by not lowering SIL directly to Alive IR. For example, ownership constraints are lowered away by IRGen, but lots of SIL passes still have to deal with those instructions. Since we have the ownership verifier built it's unlikely a pass would introduce undefined behavior by messing up the instruction stream, but it would be interesting to submit constraints that roughly equate to "this pass doesn't unnecessarily introduce refcounting traffic".

As for the second question, Alive2's IR is pretty well tied to LLVM, but then again SIL has a battle-tested lowering to LLVM IR already written. It seems to me we could exploit that and get things up and running quicker. But it's just one way of doing things.

Sure!

1 Like

@codafi, here's my proposal! I have also submitted it through the GSoC portal. Anyone should feel welcome to check it out and comment on it :slightly_smiling_face:


To do this, are you anticipating needing to modify/extend Alive2 so that it understands ownership?


Based on this, what do you think about building the system by: (This is different than what I currently have in my project proposal.)

  1. Writing a program that takes SIL as input, passes that SIL into a SIL optimization pass to get the target SIL, uses the Swift compiler to lower the source and target SIL to LLVM IR, and invokes Alive2 with that source and target LLVM IR.
  2. Extend that program to lower the source and target SIL directly to Alive2's IR, instead of using the Swift compiler to lower the SIL to LLVM IR.

Number 1 could be an alternative to the second deliverable that I described in my project proposal.

Terms of Service

Privacy Policy

Cookie Policy