veir-tests

Differential testing for veir — a verified MLIR implementation in Lean 4. Tests run the same MLIR programs through both lli (LLVM's interpreter) and veir-interpret, comparing results to catch semantic divergences.

How it works

Test files in tests/ are standard MLIR using the LLVM dialect (the same format used in the LLVM project). The test pipeline converts each file and runs it through two interpreters:

tests/*.mlir (standard MLIR with llvm.func)
    │
    ├─ convert.py ──► veir-compatible MLIR ──► veir-interpret ──► result
    │                        │
    │                        └─ re-wrap in llvm.func ──► mlir-translate ──► .ll ──► lli ──► result
    │
    └─ compare ──► PASS / FAIL

The conversion from standard MLIR to veir format involves:

• Replacing llvm.func with a flat builtin.module (veir doesn't support llvm.func)
• Substituting function arguments with llvm.constant values
• Replacing llvm.return with func.return
• Converting property encodings (overflowFlags = 1 : i32 → nsw, isExact → exact, etc.)

Prerequisites

You need three tools from an LLVM build and a checkout of veir:

Tool	Purpose
lli	LLVM bitcode interpreter (reference)
mlir-translate	Converts MLIR to LLVM IR
mlir-opt	Converts pretty-printed MLIR to generic format
veir	The veir project (built with lake build)

Set them via environment variables or add to your PATH:

export LLI=/path/to/llvm-project/build/bin/lli
export MLIR_TRANSLATE=/path/to/llvm-project/build/bin/mlir-translate
export MLIR_OPT=/path/to/llvm-project/build/bin/mlir-opt
export VEIR_DIR=/path/to/veir

Running tests

# Run all tests
./scripts/run-test.sh

# Run a specific test
./scripts/run-test.sh exact

Example output:

[PASS] disjoint: lli=7, veir=7
[PASS] exact: lli=3, veir=3
[PASS] nsw_nuw: lli=3, veir=3

All tests passed.

Adding tests

Test files are standard MLIR from the LLVM project. To add a new test, copy an MLIR file into tests/:

cp /path/to/llvm-project/mlir/test/Target/LLVMIR/some_test.mlir tests/

Since veir replaces function arguments with constant values, you can specify what values to use with an // ARGS: comment at the top of the file:

// ARGS: 24,3
// RUN: mlir-translate -mlir-to-llvmir %s | FileCheck %s
llvm.func @my_func(%arg0: i64, %arg1: i64) {
  ...
}

If no // ARGS: comment is present, default values 7, 3, 5, 11, ... are used. Choose values that satisfy operation constraints (e.g., exact division requires the dividend to be evenly divisible).

You can also preview the veir conversion without running tests:

python3 scripts/convert.py tests/some_test.mlir

Current limitations

veir's interpreter supports a subset of LLVM operations:

• Arithmetic: add, sub, mul, sdiv, udiv, srem, urem
• Bitwise: and, or, xor, shl, lshr, ashr
• Comparison: icmp, select
• Casts: trunc, sext, zext
• Integer types only — no floats, vectors, or pointers
• Single basic block — no branches, loops, or function calls
• No memory operations — no alloca, load, store

Development setup

Install pre-commit hooks for formatting (Python via ruff, shell via shfmt):

pip install pre-commit
pre-commit install

This runs formatting checks automatically on every commit. To run manually:

pre-commit run --all-files

Repository structure

veir-tests/
├── scripts/
│   ├── convert.py       # Standard MLIR → veir-compatible MLIR converter
│   └── run-test.sh      # Test runner: runs both lli and veir-interpret, compares results
├── tests/               # Standard MLIR test files (LLVM dialect)
├── .pre-commit-config.yaml
└── README.md