[][src]Module cranelift_codegen::verifier

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 by inst_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 by value_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 an 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 an block must be present in the CFG.
  • A recomputed dominator tree is identical to the existing one.

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.

TODO: Ad hoc checking

  • Stack slot loads and stores must be in-bounds.
  • Immediate constraints for certain opcodes, like udiv_imm v3, 0.
  • Insertlane and extractlane 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.



A verifier error.


List of verifier errors.



Verify func after checking the integrity of associated context data structures cfg and domtree.


Verify conventional SSA form for func.


Verify func.


Verify liveness information for func.


Verify value locations for func.

Type Definitions


Result of a verification operation.


Result of a step in the verification process.