xquad vm check

Run the bytecode verifier over a program without executing it, and report the first violation found.

Usage

xquad vm check [OPTIONS] <FILE>

Arguments

Options

xquad vm check runs the same default pipeline documented in Verifier: structural checks, jump-target checks, loop-nesting balance, register type-state, must-init analysis, and stack depth, in that order, stopping at the first phase that fails. This page covers only the command’s own behaviour; for what each phase checks and what each error means, see that page. For a task-oriented walkthrough of fixing a rejected program, see Verification.

A passing program

xquad vm check add.xqb

ok: add.xqb (4 instructions)

The instruction count includes the whole decoded stream: labelled positions as well as visible mnemonics. check writes this line to stdout and exits 0. With --text, the same message names the .xqasm source path rather than a .xqb file, since the source is assembled in memory first and never written to disk.

A failing program

uninit.xqasm reads register r0 before anything ever writes it:

LOAD r0
HALT

xquad vm check --text uninit.xqasm

Error: check failed: ReadUnsetRegister: register r0 read at byte 0x0000 before being written

check exits 1 on the first violation any phase finds. A program with two independent defects reports only this one; fixing it and re-running may surface the next.

Passing verification is not a runtime guarantee

Verification is a set of static checks over types, control flow and stack depth. It does not look at values. An allocator size, a grid extent, a loop bound and every arithmetic operand are runtime quantities, so a program that allocates a negative model, resizes past its own variable count, overflows an i64 or exhausts its step or allocation budget verifies cleanly and faults when run. See Verifier for the precise scope of what a pass proves, and Limits and Errors for the faults that have no static counterpart.