Verified Intermediate Representation

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.

Building and testing

Common tasks are wrapped in the Makefile: make build to build and make tests to run the tests. Run make to list every target.

With Nix, nix develop enters a development shell containing Lean's toolchain manager and all native and Python dependencies needed by those Make targets. Executable targets like veir-opt and veir-interpret can be run with nix run .#veir-opt, nix run .#veir-interpret, etc. For convenience, makefile targets are also exposed as flake apps with nix run .#build and nix run .#tests; nix run . displays the Makefile help.

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).

From C to VeIR

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.c
unsigned 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.c

Optimize it a little:

opt -passes=sroa demorgan.ll -S -o demorgan-opt.ll

Translate to MLIR:

mlir-translate --import-llvm demorgan-opt.ll | mlir-opt --mlir-print-op-generic --mlir-print-local-scope > demorgan-opt.mlir

Optimize using VeIR's InstCombine and DCE (dead code elimination) passes:

lake exec veir-opt -p=instcombine,dce demorgan-opt.mlir

Alternatively, 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