For some context, Alive2 is a tool that validates that an LLVM IR optimization pass(es) doesn't add any undefined behavior that isn't already present in the input to the optimization pass (Note: this property is called refinement.). The heart of Alive2 is the Z3 SMT solver. (Here are some helpful resources for understanding Z3.) Z3 allows Alive2 to understand the semantics of LLVM IR and reason deeply about its properties.
In this project, we'll extend Alive2 to understand SIL. An important note: because Z3 and Alive can reason deeply about the properties of the code it can go beyond the verification capabilities of SILVerifyer.
Soon we'll begin extending Alive2. As we plan our path forward, it'd be helpful to know:
- What instruction(s) should we extend Alive2 to understand first? In other words, where will we get the most bang for our buck? For example, would it best to start working with the reference counting instructions, ownership SSA, or ...?
- In addition to refinement, what properties should we try to verify? For example, would it be helpful to verify that an optimization pass does not add an unnecessary copy?
- What are some bugs that you've found in SIL optimization passes? What semantics would we need to capture in order to catch that bug in our tool?
- When working on an existing SIL optimization pass what would want this tool to check for you? For example, when working on SIL opaque values.
Key aspects of these questions are:
- What instruction(s) struggle to be verified by SILVerifyer?
- What properties does SILVerifyer struggle to understand?