Verifying SIL Optimization Passes

Hi all :slight_smile:

I'm working on the Alive2 for SIL GSoC project with @codafi. The project's purpose is to build a tool that will find bugs in SIL optimization passes.

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:

  1. 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 ...?
  2. 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?
  3. 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?
  4. 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:

  1. What instruction(s) struggle to be verified by SILVerifyer?
  2. What properties does SILVerifyer struggle to understand?
6 Likes

Thanks for taking this on. Here's my inital take without giving any thought to how feasible this would be...

Any optimization that removes runtime checks is a good candidate for formal verification. There would be a lot of value in being able to verify consistent semantics of runtime checks before and after optimization passes.

This would be especially great for exclusivity enforcement. To do this well, we should preserve all access markers in optimization passes. That's still work-in-progress but could probably be done in parallel.

Other important runtime checks:

  • uniquely referenced object checks
  • type checks
  • bounds checks
  • etc.

I agree that modeling copies could also have a lot of value and might be an easier task.

3 Likes
Terms of Service

Privacy Policy

Cookie Policy