VeIR is a compiler infrastructure written in Lean that offers both an MLIR-style imperative design and (optional) ITP-level verification. VeIR connects with MLIR via the MLIR textual format, making it easy to combine MLIR and VeIR tools.
| VeIR Features | Complete | Verified |
|---|---|---|
| MLIR core data structures (block, operation, region) | ✅ | 🔒 |
| define dialects | ✅ (basic) | |
| pass infrastructure | ✅ | |
| peephole rewriter | ✅ | |
| peephole rewriter (declarative) | ||
| interpreter framework | ✅ |
Common tasks are wrapped in the Makefile: make build to build and
make tests to run the tests. Run make to list every target.
Our testing framework is split into two parts: unit tests written in Lean and
FileCheck tests for the
command line tool veir-opt. The FileCheck tests require
uv to be installed.
Run a single benchmark with lake exe run-benchmarks <name> (see
Veir/Benchmarks.lean for the available names).
This section gives an example showing how to run code through a VeIR pass, starting from C code.
Prerequisite: An up-to-date MLIR bin directory in your PATH.
Start with a C function:
cat <<_end_ > demorgan.cunsigned d1(unsigned p, unsigned q) { return ~(~p & ~q);}unsigned short d2(unsigned short p, unsigned short q) { return ~(~p | ~q);}_end_Compile to LLVM IR:
clang -cc1 -O0 -disable-O0-optnone -emit-llvm demorgan.cOptimize it a little:
opt -passes=sroa demorgan.ll -S -o demorgan-opt.llTranslate to MLIR:
mlir-translate --import-llvm demorgan-opt.ll | mlir-opt --mlir-print-op-generic --mlir-print-local-scope > demorgan-opt.mlirOptimize using VeIR's InstCombine and DCE (dead code elimination) passes:
lake exec veir-opt -p=instcombine,dce demorgan-opt.mlirAlternatively, you can batch up these commands using the provided compiler driver and emit the optimized MLIR to stdout:
Tools/vcc demorgan.c --emit-mlir -O -o -Without an explicit emit mode, vcc translates VeIR's output back to
LLVM IR and asks clang to produce an executable:
cat <<_end_ > hello.c#include <stdio.h>int main(void) { printf("hello, world\n");}_end_
Tools/vcc hello.c -o hello