//------------------------------------
// Instruction (EDB) Entities
//------------------------------------

.type Instruction
  = AShrInstruction
  | AddInstruction
  | AllocaInstruction
  | AndInstruction
  | AtomicRMWInstruction
  | BitcastInstruction
  | BrCondInstruction
  | BrUncondInstruction
  | CallInstruction
  | CmpXchgInstruction
  | ExtractElementInstruction
  | ExtractValueInstruction
  | FAddInstruction
  | FCmpInstruction
  | FDivInstruction
  | FMulInstruction
  | FNegInstruction
  | FPExtInstruction
  | FPToSIInstruction
  | FPToUIInstruction
  | FPTruncInstruction
  | FRemInstruction
  | FSubInstruction
  | FenceInstruction
  | FreezeInstruction
  | GetElementPtrInstruction
  | ICmpInstruction
  | IndirectBrInstruction
  | InsertElementInstruction
  | InsertValueInstruction
  | IntToPtrInstruction
  | InvokeInstruction
  | LShrInstruction
  | LandingPadInstruction
  | LoadInstruction
  | MulInstruction
  | OrInstruction
  | PhiInstruction
  | PtrToIntInstruction
  | ResumeInstruction
  | RetInstruction
  | SDivInstruction
  | SExtInstruction
  | SIToFPInstruction
  | SRemInstruction
  | SelectInstruction
  | ShlInstruction
  | ShuffleVectorInstruction
  | StoreInstruction
  | SubInstruction
  | SwitchInstruction
  | TruncInstruction
  | UDivInstruction
  | UIToFPInstruction
  | URemInstruction
  | UnreachableInstruction
  | VaArgInstruction
  | XorInstruction
  | ZExtInstruction

// Like llvm::CallBase
.type CallBase
  = CallInstruction
  | InvokeInstruction

.decl instr(instr:Instruction)

// For constraints
.decl schema_invalid_instr(instr:Instruction, file:File, line:Line)


// Apart from the instrs with 'void' type,
// every instr assigns its result to a variable.
.decl instr_assigns_to(instr:Instruction, var:Variable)

// Auxiliary predicate that stores the instr's return type
.decl instr_returns_type(instr:Instruction, type:Type)

instr_returns_type(Instr, Type) :-
   instr_assigns_to(Instr, Var),
   variable_has_type(Var, Type).

// Terminator Instruction Subset
.decl terminator_instr(instr:Instruction)


// Instruction Flags
.type Flag <: symbol
.decl flag(flag:Flag)
.decl instr_flag(instr:Instruction, flag:Flag)

flag(Flag) :- instr_flag(_, Flag).


// helpful in avoiding non-termination warnings
.decl instr_successor_index(instr:Instruction, index:number, next_index:number)

// Position of instr on source code (if debug info is available)
.decl instr_pos(instr:Instruction, line:LineNumber, column:ColumnNumber)


//------------------------------------
// Sequence of instrs
//------------------------------------

// The next instr in the source file.
.decl instr_successor(instr:Instruction, next:Instruction)

// The func that contains the instr
.decl instr_func(instr:Instruction, func:Function)

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   instr(Instr),
   !instr_func(Instr, _).
