Verifier

[stoklund]

Cretonne needs an IR verifier.

The verifier can be run before and after different passes. It checks those IR invariants that are not enforced by the type system.

Instruction integrity:

• The instruction format must match the opcode.
• All result values must be created for multi-valued instructions.
• Instructions with no results must have a VOID first_type().
• All referenced entities must exist. (Values, EBBs, stack slots, ...)

EBB integrity:

• All instructions reached from the ebb_insts iterator must belong to the EBB as reported by inst_ebb().
• Should we detect loops in the ebb_insts iterator? The current linked list representation could theoretically do it.
• Every EBB must end in a terminator instruction, and no other instruction can be a terminator.
• Every value in the ebb_args iterator belongs to the EBB as reported by value_ebb.

SSA form. All values used by an instruction must:

• Be defined by an instruction that exists and that is inserted in an EBB, or be an argument of an existing EBB.
• Dominate the instruction. This check should probably be skipped for EBBs that can't be reached from the entry.

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:

• Verify all 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 excatly. 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.

Ad hoc checking:

• Stack slot loads and stores must be in-bounds.
• Immediate constraints for certain opcodes, like udiv_imm v3, 0.
• Extend / truncate instructions have more type constraints: Source type can't be larger / smaller than result type.

[stoklund]

More ad-hoc checks:

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

The direction I'm currently heading WRT overall structure and testing. The testing will need to be refactored to isolate some repeated code. https://github.com/mrrrgn/cretonne/commit/17303baa8195d4fd68d31c0e6ad682d3d5130d3f

[stoklund]

This is looking good! A few comments:

The entity references like Inst and Ebb implement Display, so they print nicer with {} than {:?}, IMHO.

In the verifier.rs module, you could add a public function:

pub fn verify(func: &Function) -> Result<(), String> {
    Verifier::new(func).run()
}

This is easier to use than the two-step create a Verifier, call run. You could then even make the Verifier struct private to the module.

I'd prefer to use the term terminator everywhere, so rename is_terminating to is_terminator.

Being a terminator instruction should be a property of the opcode, not of the instruction format. The instruction format is simply computed from the kind of operands the instruction takes, so it can't really be used to infer anything other than how an instruction is represented in memory.

Eventually, I want Opcode::is_terminator() to be generated automatically from the meta instruction definitions. I even added some is_terminator=True to meta/cretonne/base.py, but they are not used for anything yet.

In the meantime, just implement Opcode::is_terminator() manually.

[stoklund]

Opened #12 to track the opcode flags like is_terminator.

Whoops, I just saw the above suggestions, will fix them asap. In the meantime, I'm adding more checks. I'm curious about how to handle InstructionData::Call results in instruction_integrity as I've started on it here: https://github.com/mrrrgn/cretonne/commit/dff05c900116474780831c0ed11af66b6ab83067

[stoklund]

I'm curious about how to handle InstructionData::Call results in instruction_integrity as I've started on it here: mrrrgn@dff05c9

Yeah, that makes sense. The IR data structure is missing some stuff you'll need for verifying function calls. This is what I have in mind:

There will be two kinds of call instructions, direct calls and indirect calls. A direct call will have an external function entity reference as its callee. These external functions must be declared in the preamble as described in the language reference. An indirect call will reference a signature entity.

I imagine we'll add something like this to ir::Function:

pub ext_funcs: EntityMap<ExtFunc, ExtFuncData>,
pub signatures: EntityMap<Signature, SignatureData>,

In either case, you should be able to get your hands on a signature that you can use to verify both argument and return types.

[DemiMarie]

I think that there should be an (optional) component that does safety checks: a safe module cannot corrupt memory.

[stoklund]

Safety in Cretonne is expressed by using a reduced instruction set. Specifically, the heap_load and heap_store instructions are bounds-checked, while load and store can access all memory. We don't have a way of tagging safe instructions at the moment, but when we do, it would make sense to have the verifier check that only the permitted instruction sets are in use.

[bnjbvr]

@leurfete, are you still working on this? If not, would you mind that I take this over, basing my work upon your commits?

[angusholder]

For "Values must be defined by an instruction that exists", I'm currently just looping through all values in dfg.extended_values, is this the right idea? As far as I know, the only other values possible are the primary result values of instructions, and they only exist when an instruction exists right?

[stoklund]

I think there can be dead values in dfg.extended_values, and that's OK. You should only check values that are actually used as operands on an instruction. So basically your verify_value() function.

You can use dfg.value_def(value) to see where the value is defined. Then you can verify that the EBB or defining instructions are valid references and that they are inserted in the layout. See layout.is_ebb_inserted() and layout.inst_ebb().

[angusholder]

Great, thanks, I've managed to do all that now.

For some of these checks I need a ControlFlowGraph and a DominatorTree, what should I do for that? Make a separate verify_context that takes a &Context?

[stoklund]

I think you should always compute a dominator tree from scratch if you need it. We can't trust that the one in Context is correct. You can use the Verifier struct as your context and store it there.

After you compute your own dominator tree, it would be nice to also compare it to the existing one in Context. A verify_context() function would be good for that.

[stoklund]

Same thing for the ControlFlowGraph. You can't trust the one in Context, so you should compute your own.