[−][src]Module cranelift_codegen::verifier

A verifier for ensuring that functions are well formed. It verifies:

EBB integrity

  • All instructions reached from the ebb_insts iterator must belong to the EBB as reported by inst_ebb().
  • Every EBB must end in a terminator instruction, and no other instruction can be a terminator.
  • Every value in the ebb_params iterator belongs to the EBB as reported by value_ebb.

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, EBBs, 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 EBB, or be an argument of an existing EBB.
  • 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 EBB.
  • All branches to an EBB 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 EBBs that match the expected types exactly. The number of arguments must match.
  • All EBBs 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.