[Draft] Update SMT-based ISLE verifier

[avanhatt]

Update the core ISLE verifier for formal, SMT-based checking of instruction lowering rules. This brings the implementation up-to-date with our work described at OOPSLA 2025, rather than the prior ASPLOS 2024 implementation.

The core improvements are:

1. Automatic rule chaining. Rather than requiring specifications on every ISLE term, terms can be marked veri chain to be automatically composed/inlined. This reduces the specification burden substantially. See the paper for details.
2. For the aarch64 backend, most machine inst Minst specifications are automatically derived from the authoritative ARM ASL reference, with our work building on the ASLp project to derive more targeted specifications for this domain.
3. Our state modeling now handles traps and other side effects more explicitly, see the paper for details.
4. The specification language is more expressive, including structs and macros. See the language reference updates for details.

[bjorn3]

Accidental commit?

[avanhatt]

Ah yes, thanks for spotting!

[cfallin]

This largely looks good! I skimmed over any spec/model/attr forms in the diffs of ISLE, and the cranelift/isle/veri tree in general; reviewed more carefully the bits that were touched in Cranelift and the ISLE compiler proper. Some logistical comments but nothing really substantial. Thanks for all the work in getting this in shape for upstreaming!

[cfallin]

Spurious code-motion in diff?

[avanhatt]

This was actually intentional, but for a niche reason.

The verifier was previously failing to type check the use of the get_exception_handler_address ISLE term. It turned out that this was the only term with both a raw block and an immediate, and that the order that gen_isle added the block, then the immediate, did not match the order of the declaration:

Builder::new("ExceptionHandlerAddress")
                .raw_block()
                .imm(&imm.imm64)
                .build(),

Because the veri code does not expand external extractors and used the generated ISLE decl for this type directly (shown below), this mismatch made the rule appear to have incorrect argument order. Whereas in standard ISLE codegen, the inlined extractor had the same swapped order, essentially cancelling out the mismatch.

Before, generated code on main:

(decl get_exception_handler_address (Type Block Imm64) Inst) ;; cranelift/codegen/meta/src/gen_isle.rs:243
(extractor ;; cranelift/codegen/meta/src/gen_isle.rs:262
    (get_exception_handler_address ty block index) ;; cranelift/codegen/meta/src/gen_isle.rs:264
    (inst_data_value ty (InstructionData.ExceptionHandlerAddress (Opcode.GetExceptionHandlerAddress) index block))
)

Note the first line has block, then immediate, but the last line has immediate, then block.

It's a bit annoying because making the orders match required me to also change the arg order of the get_exception_handler_address rule in all backends, but it feels like the right move because before, all the rules used an argument order different from the generated decl.

The new generated code:

(decl get_exception_handler_address (Type Block Imm64) Inst) ;; cranelift/codegen/meta/src/gen_isle.rs:243
(extractor ;; cranelift/codegen/meta/src/gen_isle.rs:262
    (get_exception_handler_address ty block index) ;; cranelift/codegen/meta/src/gen_isle.rs:264
    (inst_data_value ty (InstructionData.ExceptionHandlerAddress (Opcode.GetExceptionHandlerAddress) block index))
)

Let me know if you prefer a different fix, though, or for me to land this change separately?

[cfallin]

Unnecessary/trivial doc comments here and below? (shift_ones being described as "Shift ones" doesn't add anything; but then we don't need doc-comments here, perhaps we can just drop)

[avanhatt]

Ah, we added uses of cranelift_codegen::isa::aarch64::inst::... within cranelift/isle/veri, which made all of these fail deny(missing_docs).

Would we prefer I add an #![allow(missing_docs)] with a comment that we use these within cranelift/isle/veri? Or something else?

[cfallin]

likewise here as above -- no need for doc-comments that just reproduce function names

[cfallin]

Is this a codegen change? It's not totally clear to me (I haven't traced through the emit code) but this is at least adding some new logic where we passed size through to MInst.MovToFpu directly before.

[avanhatt]

My intention was to break the recursion (the new size_for_mov_to_fpu actually should not have the rec tag, fixing) to allow chaining, but match the logic/not change codegen.

Reasoning:

• If size is ScalarSize.Size16 and (use_fp16) is false, the higher-priority rule below will match and size_for_mov_to_fpu will pass (ScalarSize.Size32).
• In all other cases, the default size_for_mov_to_fpu rule just passes the size back.

That is, we didn't pass size through directly to MInst.MovToFpu directly before in exactly the same case, due to the recursive rule below this one:

(rule 1 (mov_to_fpu x (ScalarSize.Size16))
        (if-let false (use_fp16))
        (mov_to_fpu x (ScalarSize.Size32)))

[cfallin]

For this and related prelude ISLE for the spec (e.g. fpconst.isle, inst_tags.isle, inst_spec.isle, ...) could we put it in a subdirectory, e.g. spec/?

[cfallin]

Let's use workspace deps here; and I'll need to push vets before this merges to make cargo-vet happy

[cfallin]

Likewise here (and elsewhere in this diff) -- workspace deps only, to centralize our deps management and version upgrades.