Expand description
A verifier for ensuring that functions are well formed. It verifies:
block integrity
- All instructions reached from the
block_insts
iterator must belong to the block as reported byinst_block()
. - Every block must end in a terminator instruction, and no other instruction can be a terminator.
- Every value in the
block_params
iterator belongs to the block as reported byvalue_block
.
Instruction integrity
- The instruction format must match the opcode.
- All result values must be created for multi-valued instructions.
- All referenced entities must exist. (Values, blocks, stack slots, …)
- Instructions must not reference (eg. branch to) the entry block.
SSA form
- Values must be defined by an instruction that exists and that is inserted in a block, or be an argument of an existing block.
- Values used by an instruction must dominate the instruction.
Control flow graph and dominator tree integrity:
- All predecessors in the CFG must be branches to the block.
- All branches to a block must be present in the CFG.
- A recomputed dominator tree is identical to the existing one.
- The entry block must not be a cold block.
Type checking
- Compare input and output values against the opcode’s type constraints. For polymorphic opcodes, determine the controlling type variable first.
- Branches and jumps must pass arguments to destination blocks that match the expected types exactly. The number of arguments must match.
- All blocks in a jump table must take no arguments.
- Function calls are type checked against their signature.
- The entry block must take arguments that match the signature of the current function.
- All return instructions must have return value operands matching the current function signature.
Global values
- Detect cycles in global values.
- Detect use of ‘vmctx’ global value when no corresponding parameter is defined.
Memory types
- Ensure that struct fields are in offset order.
- Ensure that struct fields are completely within the overall struct size, and do not overlap.
TODO: Ad hoc checking
- Stack slot loads and stores must be in-bounds.
- Immediate constraints for certain opcodes, like
udiv_imm v3, 0
. Insertlane
andextractlane
instructions have immediate lane numbers that must be in range for their polymorphic type.- Swizzle and shuffle instructions take a variable number of lane arguments. The number of arguments must match the destination type, and the lane indexes must be in range.
Structs§
- A verifier error.
- List of verifier errors.
Functions§
- Verify
func
after checking the integrity of associated context data structurescfg
anddomtree
. - Verify
func
.
Type Aliases§
- Result of a verification operation.
- Result of a step in the verification process.