Alive2 for SIL - GSoC Final Report.md

Alive2 for SIL - GSoC Final Report

The Alive2 for SIL project aims to do translation validation of the Swift compiler's optimization passes using Alive2. For more details about the project checkout it's abstract and proposal.

Final Product

Running sil-opt with the --translation-validation flag at the beginning and end of the list of optimization passes will invoke translation validation engine on said optimization passes.

Where's the Code?

The modifications to the Swift compiler are in the sil-alive branch of my fork of the Swift compiler and the modificaitons to Alive2 are in my fork of Alive2. Use this link to view the changes made to the Swift compiler and this link to view the changes made to Alive2.

What Work Got Done?

• Added the SILAlive library to the Swift compiler. It can:
  • Lower SIL at any SILStage to SILStage::Lowered.
  • Lower SILStage::Lowered SIL to LLVM IR.
  • Lower the functions of an LLVM IR module to Alive2 IR function.
  • Invoke the Alive2's translation validation engine on a pair of Alive2 IR functions.
• Added the ability to clone a SILModule with swift::cloneModule().
• Added Alive2 and Z3 to the Swift compiler's dependency manager and build system.
• Downgraded Alive2 from C++ 20 to C++ 14. Robert Widmann did most of the work on this. It helped Alive2 to better integrate into the Swift compiler since the Swift compiler uses C++ 14.
  • This work ended up containing bugs, so it is not used in the current iteration of the tool.
• Added the TranslationValidation optimization pass to invoke our tool via sil-opt.
• Extended LLVM's Integrated Tester (lit) and sil-opt here and here respectivly to invoke our tool when running the Swift compiler's test suite.

What Pull Requests did you Submit?

• swift::cloneModule() (PR).
• Run Swift's build system's dependency resolver (PR).
• Remove the unsued loc parameter in SILFunction::init() (in-progress).
• Resolve a null pointer dereference that is triggered when SILFunction.front() is called on a SILFunction that contains zero SILBasicBlocks (in-progress).

What's Left To Do?

• The Alive2 and Z3 support within the build system is dependent on my computer as seen here and here. This should be changed to work seamlessly on any system supported by the Swift compiler.
• Fix an use after free of a reference counted Z3_ast in Alive2.
• Fix an use after free of the Z3_context that necessitated this band-aid commit.
• Fix common bugs that are exposed when using lit.
  1. Linking errors with ProtocolConformance.cpp (example)
  2. swift::cloneModule() triggers an assertion in the linear lifetime checker (example)
• Fix bugs in the sil-alive tool to do translation validation on a pair of SIL files.
• Lower SIL -> Alive2 IR instead of SIL -> LLVM IR -> Alive2 IR.