// http://llvm.org/docs/LangRef.html#indirectbr-instr
// keywords: terminator; instr

.type IndirectBrInstruction <: symbol
.decl indirectbr_instr(instr:IndirectBrInstruction)

instr(v) :- indirectbr_instr(v).
terminator_instr(v) :- indirectbr_instr(v).


// The ‘address‘ argument is the address of the label to jump to.
.decl indirectbr_instr_address(instr:Instruction, address:Operand)


// The rest of the arguments indicate the full set
// of possible destinations that the address may point to.
// This destination list is required so that dataflow analysis
// has an accurate understanding of the CFG.

.decl indirectbr_instr_label(instr:Instruction, index:number, label:Variable)
.decl indirectbr_instr_nlabels(instr:Instruction, total:number)


//------------------------------------------------------------------------------
// [Constraints]
//
//  (1) Address must be derived from a blockaddress constant.
//
//  (2) The ‘blockaddress‘ constant computes the address of the
//      specified basic block in the specified func, and always
//      has an i8* type.
//------------------------------------------------------------------------------

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   indirectbr_instr(Instr),
   !indirectbr_instr_address(Instr, _).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   indirectbr_instr(Instr),
   !indirectbr_instr_nlabels(Instr, _).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   indirectbr_instr(Instr),
   indirectbr_instr_label(Instr, _, Label),
   !variable_is_label(Label).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   indirectbr_instr(Instr),
   indirectbr_instr_label(Instr, Index, _),
   Index < 0.

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   indirectbr_instr(Instr),
   indirectbr_instr_label(Instr, Index, _),
   indirectbr_instr_nlabels(Instr, Total),
   Index >= Total.

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   indirectbr_instr(Instr),
   indirectbr_instr_address(Instr, Address),
   operand_has_type(Address, Type),
   !int8_type(Type).
