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.
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.
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.
- 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.
- Lower SIL at any SILStage to
- 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.
swift::cloneModule()
(PR).- Run Swift's build system's dependency resolver (PR).
- Remove the unsued
loc
parameter inSILFunction::init()
(in-progress). - Resolve a null pointer dereference that is triggered when
SILFunction.front()
is called on aSILFunction
that contains zeroSILBasicBlock
s (in-progress).
- 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
.- Linking errors with ProtocolConformance.cpp (example)
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.