Name Date Size #Lines LOC

..15-May-2026-

docs/H15-May-2026-1,6071,273

fuzz/H15-May-2026-7355

isle/H15-May-2026-10,4588,081

islec/H15-May-2026-6350

veri/H15-May-2026-20,01417,807

.gitignoreH A D15-May-202618 43

LICENSEH A D15-May-202612 KiB221182

README.mdH A D15-May-202618.2 KiB526430

TODOH A D15-May-2026918 2316

README.md

1# ISLE: Instruction Selection/Lowering Expressions DSL
2
3See also: [Language Reference](./docs/language-reference.md)
4
5## Table of Contents
6
7* [Introduction](#introduction)
8* [Example Usage](#example-usage)
9* [Tutorial](#tutorial)
10* [Implementation](#implementation)
11
12## Introduction
13
14ISLE is a DSL that allows one to write instruction-lowering rules for a
15compiler backend. It is based on a "term-rewriting" paradigm in which the input
16-- some sort of compiler IR -- is, conceptually, a tree of terms, and we have a
17set of rewrite rules that turn this into another tree of terms.
18
19This repository contains a prototype meta-compiler that compiles ISLE rules
20down to an instruction selector implementation in generated Rust code. The
21generated code operates efficiently in a single pass over the input, and merges
22all rules into a decision tree, sharing work where possible, while respecting
23user-configurable priorities on each rule.
24
25The ISLE language is designed so that the rules can both be compiled into an
26efficient compiler backend and can be used in formal reasoning about the
27compiler. The compiler in this repository implements the former. The latter
28use-case is future work and outside the scope of this prototype, but at a high
29level, the rules can be seen as simple equivalences between values in two
30languages, and so should be translatable to formal constraints or other logical
31specification languages.
32
33Some more details and motivation are in [BA RFC #15](https://github.com/bytecodealliance/rfcs/pull/15).
34Reference documentation can be found [here](docs/language-reference.md).
35Details on ISLE's integration into Cranelift can be found
36[here](../docs/isle-integration.md).
37
38## Example Usage
39
40Build `islec`, the ISLE compiler:
41
42```console
43cargo build --release
44```
45
46Compile a `.isle` source file into Rust code:
47
48```console
49target/release/islec -i isle_examples/test.isle -o isle_examples/test.rs
50```
51
52Include that Rust code in your crate and compile it:
53
54```console
55rustc isle_examples/test_main.rs
56```
57
58## Tutorial
59
60This tutorial walks through defining an instruction selection and lowering pass
61for a simple, RISC-y, high-level IR down to low-level, CISC-y machine
62instructions. It is intentionally somewhat similar to CLIF to MachInst lowering,
63although it restricts the input and output languages to only adds, loads, and
64constants so that we can focus on ISLE itself.
65
66> The full ISLE source code for this tutorial is available at
67> `isle_examples/tutorial.isle`.
68
69The ISLE language is based around rules for translating a term (i.e. expression)
70into another term. Terms are typed, so before we can write rules for translating
71some type of term into another type of term, we have to define those types:
72
73```lisp
74;; Declare that we are using the `i32` primitive type from Rust.
75(type i32 (primitive i32))
76
77;; Our high-level, RISC-y input IR.
78(type HighLevelInst
79  (enum (Add (a Value) (b Value))
80        (Load (addr Value))
81        (Const (c i32))))
82
83;; A value in our high-level IR is a Rust `Copy` type. Values are either defined
84;; by an instruction, or are a basic block argument.
85(type Value (primitive Value))
86
87;; Our low-level, CISC-y machine instructions.
88(type LowLevelInst
89  (enum (Add (mode AddrMode))
90        (Load (offset i32) (addr Reg))
91        (Const (c i32))))
92
93;; Different kinds of addressing modes for operands to our low-level machine
94;; instructions.
95(type AddrMode
96  (enum
97    ;; Both operands in registers.
98    (RegReg (a Reg) (b Reg))
99    ;; The destination/first operand is a register; the second operand is in
100    ;; memory at `[b + offset]`.
101    (RegMem (a Reg) (b Reg) (offset i32))
102    ;; The destination/first operand is a register, second operand is an
103    ;; immediate.
104    (RegImm (a Reg) (imm i32))))
105
106;; The register type is a Rust `Copy` type.
107(type Reg (primitive Reg))
108```
109
110Now we can start writing some basic lowering rules! We declare the top-level
111lowering function (a "constructor term" in ISLE terminology) and attach rules to
112it. The simplest case is matching a high-level `Const` instruction and lowering
113that to a low-level `Const` instruction, since there isn't any translation we
114really have to do.
115
116```lisp
117;; Declare our top-level lowering function. We will attach rules to this
118;; declaration for lowering various patterns of `HighLevelInst` inputs.
119(decl lower (HighLevelInst) LowLevelInst)
120
121;; Simple rule for lowering constants.
122(rule (lower (HighLevelInst.Const c))
123      (LowLevelInst.Const c))
124```
125
126Each rule has the form `(rule <left-hand side> <right-hand-side>)`. The
127left-hand side (LHS) is a *pattern* and the right-hand side (RHS) is an
128*expression*. When the LHS pattern matches the input, then we evaluate the RHS
129expression. The LHS pattern can bind variables from the input that are then
130available in the right-hand side. For example, in our `Const`-lowering rule, the
131variable `c` is bound from the LHS and then reused in the RHS.
132
133Now we can compile this code by running
134
135```console
136islec isle_examples/tutorial.isle
137```
138
139and we'll get the following output <sup>(ignoring any minor code generation
140changes in the future)</sup>:
141
142```rust
143// GENERATED BY ISLE. DO NOT EDIT!
144//
145// Generated automatically from the instruction-selection DSL code in:
146// - isle_examples/tutorial.isle
147
148// [Type and `Context` definitions removed for brevity...]
149
150// Generated as internal constructor for term lower.
151pub fn constructor_lower<C: Context>(ctx: &mut C, arg0: &HighLevelInst) -> Option<LowLevelInst> {
152    let pattern0_0 = arg0;
153    if let &HighLevelInst::Const { c: pattern1_0 } = pattern0_0 {
154        // Rule at isle_examples/tutorial.isle line 45.
155        let expr0_0 = LowLevelInst::Const {
156            c: pattern1_0,
157        };
158        return Some(expr0_0);
159    }
160    return None;
161}
162```
163
164There are a few things to notice about this generated Rust code:
165
166* The `lower` constructor term becomes the `constructor_lower` function in the
167  generated code.
168
169* The function returns a value of type `Option<LowLevelInst>` and returns `None`
170  when it doesn't know how to lower an input `HighLevelInst`. This is useful for
171  incrementally porting hand-written lowering code to ISLE.
172
173* There is a helpful comment documenting where in the ISLE source code a rule
174  was defined. The goal is to make ISLE more transparent and less magical.
175
176* The code is parameterized by a type that implements a `Context`
177  trait. Implementing this trait is how you glue the generated code into your
178  compiler. Right now this is an empty trait; more on `Context` later.
179
180* Lastly, and most importantly, this generated Rust code is basically what we
181  would have written by hand to do the same thing, other than things like
182  variable names. It checks if the input is a `Const`, and if so, translates it
183  into a `LowLevelInst::Const`.
184
185Okay, one rule isn't very impressive, but in order to start writing more rules
186we need to be able to put the result of a lowered instruction into a `Reg`. This
187might internally have to do arbitrary things like update use counts or anything
188else that Cranelift's existing `LowerCtx::put_input_in_reg` does for different
189target architectures. To allow for plugging in this kind of arbitrary logic,
190ISLE supports *external constructors*. These end up as methods of the `Context`
191trait in the generated Rust code, and you can implement them however you want
192with custom Rust code.
193
194Here is how we declare an external helper to put a value into a register:
195
196```lisp
197;; Declare an external constructor that puts a high-level `Value` into a
198;; low-level `Reg`.
199(decl put_in_reg (Value) Reg)
200(extern constructor put_in_reg put_in_reg)
201```
202
203If we rerun `islec` on our ISLE source, instead of an empty `Context` trait, now
204we will get this trait definition:
205
206```rust
207pub trait Context {
208    fn put_in_reg(&mut self, arg0: Value) -> (Reg,);
209}
210```
211
212With the `put_in_reg` helper available, we can define rules for lowering loads
213and adds:
214
215```lisp
216;; Simple rule for lowering adds.
217(rule (lower (HighLevelInst.Add a b))
218      (LowLevelInst.Add
219        (AddrMode.RegReg (put_in_reg a) (put_in_reg b))))
220
221;; Simple rule for lowering loads.
222(rule (lower (HighLevelInst.Load addr))
223      (LowLevelInst.Load 0 (put_in_reg addr)))
224```
225
226If we compile our ISLE source into Rust code once again, the generated code for
227`lower` now looks like this:
228
229```rust
230// Generated as internal constructor for term lower.
231pub fn constructor_lower<C: Context>(ctx: &mut C, arg0: &HighLevelInst) -> Option<LowLevelInst> {
232    let pattern0_0 = arg0;
233    match pattern0_0 {
234        &HighLevelInst::Const { c: pattern1_0 } => {
235            // Rule at isle_examples/tutorial.isle line 45.
236            let expr0_0 = LowLevelInst::Const {
237                c: pattern1_0,
238            };
239            return Some(expr0_0);
240        }
241        &HighLevelInst::Load { addr: pattern1_0 } => {
242            // Rule at isle_examples/tutorial.isle line 59.
243            let expr0_0: i32 = 0;
244            let expr1_0 = C::put_in_reg(ctx, pattern1_0);
245            let expr2_0 = LowLevelInst::Load {
246                offset: expr0_0,
247                addr: expr1_0,
248            };
249            return Some(expr2_0);
250        }
251        &HighLevelInst::Add { a: pattern1_0, b: pattern1_1 } => {
252            // Rule at isle_examples/tutorial.isle line 54.
253            let expr0_0 = C::put_in_reg(ctx, pattern1_0);
254            let expr1_0 = C::put_in_reg(ctx, pattern1_1);
255            let expr2_0 = AddrMode::RegReg {
256                a: expr0_0,
257                b: expr1_0,
258            };
259            let expr3_0 = LowLevelInst::Add {
260                mode: expr2_0,
261            };
262            return Some(expr3_0);
263        }
264        _ => {}
265    }
266    return None;
267}
268```
269
270As you can see, each of our rules was collapsed into a single, efficient `match`
271expression. Just like we would have otherwise written by hand. And wherever we
272need to get a high-level operand as a low-level register, there is a call to the
273`Context::put_in_reg` trait method, allowing us to hook whatever arbitrary logic
274we need to when putting a value into a register when we implement the `Context`
275trait.
276
277Things start to get more interesting when we want to do things like sink a load
278into the add's addressing mode. This is only desirable when our add is the only
279use of the loaded value. Furthermore, it is only valid to do when there isn't
280any store that might write to the same address we are loading from in between
281the load and the add. Otherwise, moving the load across the store could result
282in a miscompilation where we load the wrong value to add:
283
284```text
285x = load addr
286store 42 -> addr
287y = add x, 1
288
289==/==>
290
291store 42 -> addr
292x = load addr
293y = add x, 1
294```
295
296We can encode these kinds of preconditions in an *external extractor*. An
297extractor is like our regular constructor functions, but it is used inside LHS
298patterns, rather than RHS expressions, and its arguments and results flipped
299around: instead of taking arguments and producing results, it takes a result and
300(fallibly) produces the arguments. This allows us to write custom preconditions
301for matching code.
302
303Let's make this more clear with a concrete example. Here is the declaration of
304an external extractor to match on the high-level instruction that defined a
305given operand `Value`, along with a new rule to sink loads into adds:
306
307```lisp
308;; Declare an external extractor for extracting the instruction that defined a
309;; given operand value.
310(decl inst_result (HighLevelInst) Value)
311(extern extractor inst_result inst_result)
312
313;; Rule to sink loads into adds.
314(rule (lower (HighLevelInst.Add a (inst_result (HighLevelInst.Load addr))))
315      (LowLevelInst.Add
316        (AddrMode.RegMem (put_in_reg a)
317                         (put_in_reg addr)
318                         0)))
319```
320
321Note that the operand `Value` passed into this extractor might be a basic block
322parameter, in which case there is no such instruction. Or there might be a store
323or function call instruction in between the current instruction and the
324instruction that defines the given operand value, in which case we want to
325"hide" the instruction so that we don't illegally sink loads into adds they
326shouldn't be sunk into. So this extractor might fail to return an instruction
327for a given operand `Value`.
328
329If we recompile our ISLE source into Rust code once again, we see a new
330`inst_result` method defined on our `Context` trait, we notice that its
331arguments and returns are flipped around from the `decl` in the ISLE source
332because it is an extractor, and finally that it returns an `Option` because it
333isn't guaranteed that we can extract a defining instruction for the given
334operand `Value`:
335
336```rust
337pub trait Context {
338    fn put_in_reg(&mut self, arg0: Value) -> (Reg,);
339    fn inst_result(&mut self, arg0: Value) -> Option<(HighLevelInst,)>;
340}
341```
342
343And if we look at the generated code for our `lower` function, there is a new,
344nested case for sinking loads into adds that uses the `Context::inst_result`
345trait method to see if our new rule can be applied:
346
347```rust
348// Generated as internal constructor for term lower.
349pub fn constructor_lower<C: Context>(ctx: &mut C, arg0: &HighLevelInst) -> Option<LowLevelInst> {
350    let pattern0_0 = arg0;
351    match pattern0_0 {
352        &HighLevelInst::Const { c: pattern1_0 } => {
353            // [...]
354        }
355        &HighLevelInst::Load { addr: pattern1_0 } => {
356            // [...]
357        }
358        &HighLevelInst::Add { a: pattern1_0, b: pattern1_1 } => {
359            if let Some((pattern2_0,)) = C::inst_result(ctx, pattern1_1) {
360                if let &HighLevelInst::Load { addr: pattern3_0 } = &pattern2_0 {
361                    // Rule at isle_examples/tutorial.isle line 68.
362                    let expr0_0 = C::put_in_reg(ctx, pattern1_0);
363                    let expr1_0 = C::put_in_reg(ctx, pattern3_0);
364                    let expr2_0: i32 = 0;
365                    let expr3_0 = AddrMode::RegMem {
366                        a: expr0_0,
367                        b: expr1_0,
368                        offset: expr2_0,
369                    };
370                    let expr4_0 = LowLevelInst::Add {
371                        mode: expr3_0,
372                    };
373                    return Some(expr4_0);
374                }
375            }
376            // Rule at isle_examples/tutorial.isle line 54.
377            let expr0_0 = C::put_in_reg(ctx, pattern1_0);
378            let expr1_0 = C::put_in_reg(ctx, pattern1_1);
379            let expr2_0 = AddrMode::RegReg {
380                a: expr0_0,
381                b: expr1_0,
382            };
383            let expr3_0 = LowLevelInst::Add {
384                mode: expr2_0,
385            };
386            return Some(expr3_0);
387        }
388        _ => {}
389    }
390    return None;
391}
392```
393
394Once again, this is pretty much the code you would have otherwise written by
395hand to sink the load into the add.
396
397At this point we can start defining a whole bunch of even-more-complicated
398lowering rules that do things like take advantage of folding static offsets into
399loads into adds:
400
401```lisp
402;; Rule to sink a load of a base address with a static offset into a single add.
403(rule (lower (HighLevelInst.Add
404               a
405               (inst_result (HighLevelInst.Load
406                              (inst_result (HighLevelInst.Add
407                                             base
408                                             (inst_result (HighLevelInst.Const offset))))))))
409      (LowLevelInst.Add
410        (AddrMode.RegMem (put_in_reg a)
411                         (put_in_reg base)
412                         offset)))
413
414;; Rule for sinking an immediate into an add.
415(rule (lower (HighLevelInst.Add a (inst_result (HighLevelInst.Const c))))
416      (LowLevelInst.Add
417        (AddrMode.RegImm (put_in_reg a) c)))
418
419;; Rule for lowering loads of a base address with a static offset.
420(rule (lower (HighLevelInst.Load
421               (inst_result (HighLevelInst.Add
422                              base
423                              (inst_result (HighLevelInst.Const offset))))))
424      (LowLevelInst.Load offset (put_in_reg base)))
425```
426
427I'm not going to show the generated Rust code for these new rules here because
428it is starting to get a bit too big. But you can compile
429`isle_examples/tutorial.isle` and verify yourself that it generates the code you
430expect it to.
431
432In conclusion, adding new lowering rules is easy with ISLE. And you still get
433that efficient, compact tree of `match` expressions in the generated Rust code
434that you would otherwise write by hand.
435
436## Implementation
437
438This is an overview of `islec`'s passes and data structures:
439
440```text
441    +------------------+
442    | ISLE Source Text |
443    +------------------+
444             |
445             | Lex
446             V
447         +--------+
448         | Tokens |
449         +--------+
450             |
451             | Parse
452             V
453   +----------------------+
454   | Abstract Syntax Tree |
455   +----------------------+
456             |
457             | Semantic Analysis
458             V
459+----------------------------+
460| Term and Type Environments |
461+----------------------------+
462             |
463             | Trie Construction
464             V
465       +-----------+
466       | Term Trie |
467       +-----------+
468             |
469             | Code Generation
470             V
471    +------------------+
472    | Rust Source Code |
473    +------------------+
474```
475
476### Lexing
477
478Lexing breaks up the input ISLE source text into a stream of tokens. Our lexer
479is pull-based, meaning that we don't eagerly construct the full stream of
480tokens. Instead, we wait until the next token is requested, at which point we
481lazily lex it.
482
483Relevant source files:
484
485* `isle/src/lexer.rs`
486
487### Parsing
488
489Parsing translates the stream of tokens into an abstract syntax tree (AST). Our
490parser is a simple, hand-written, recursive-descent parser.
491
492Relevant source files:
493
494* `isle/src/ast.rs`
495* `isle/src/parser.rs`
496
497### Semantic Analysis
498
499Semantic analysis performs type checking, figures out which rules apply to which
500terms, etc. It creates a type environment and a term environment that we can use
501to get information about our terms throughout the rest of the pipeline.
502
503Relevant source files:
504
505* `isle/src/sema.rs`
506
507### Trie Construction
508
509The trie construction phase linearizes each rule's LHS pattern and inserts them
510into a trie that maps LHS patterns to RHS expressions. This trie is the skeleton
511of the decision tree that will be emitted during code generation.
512
513Relevant source files:
514
515* `isle/src/ir.rs`
516* `isle/src/trie.rs`
517
518### Code Generation
519
520Code generation takes in the term trie and emits Rust source code that
521implements it.
522
523Relevant source files:
524
525* `isle/src/codegen.rs`
526