Stream: cranelift

Topic: Control flow specs in Arrival

Stephan Stanisic (May 21 2026 at 08:33):

Hi! I am trying to use Arrival to reason about chains of instructions that contain control flow, like jumps and conditional branches. I was looking through the generated ISA specs in the Arrival repo, but instructions like CondBr, Jump and Call seem to lack accompanying specifications.

I noticed in the paper for both Crocus and Arrival control flow is specifically omitted from the current work, as I assume its hard to reason about in arbitrary programs. However, the code I am verifying isn't arbitrary, and we can possibly give information about the CFG to Arrival for example.

Does anyone have any suggestions on how to proceed? An example snippet of code I'm trying to reason about is the following:

_instr_I32Const:
    # read 1 byte from source program
    movzx rdx, byte ptr [rax]
    add rax, 1
    # jump to the call decode path if the sign bit is set (decoding needed)
    test dl, dl
    js label_else
    # jump over the sign if no decoding is needed
    jmp label_end

label_else:
    call _decode_leb128

label_end:
    # push the decoded value onto the value stack
    add rsi, -4
    mov DWORD PTR [rsi], edx

This has been generated (through isle/arrival) from a much higher level DSL:

vec![
    Deref(Scratch2, InstructionPointer),
    IfThenElse(
        Sign,
        Scratch2,
        vec![Call(GlobalAddressLabels::DecodeLeb128)],
        vec![],
    ),
    Push(I32, Scratch2),
],

I could provide a small isle file with some more context if that would be helpful.

Last updated: Jun 01 2026 at 09:49 UTC