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 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.

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.

Structs

VerifierError	A verifier error.
VerifierErrors	List of verifier errors.

Functions

verify_context	Verify func after checking the integrity of associated context data structures cfg and domtree.
verify_cssa	Verify conventional SSA form for func.
verify_function	Verify func.
verify_liveness	Verify liveness information for func.
verify_locations	Verify value locations for func.

Type Definitions

VerifierResult	Result of a verification operation.
VerifierStepResult	Result of a step in the verification process.