// http://llvm.org/docs/LangRef.html#load-instr
// keywords: memory; instr

.type LoadInstruction <: symbol
.decl load_instr(instr:LoadInstruction)

instr(v) :- load_instr(v).

.decl load_instr_alignment(instr:LoadInstruction, alignment:number)
.decl load_instr_ordering(instr:LoadInstruction, ordering:Ordering)

// If the load is marked as volatile, then the optimizer is not allowed
// to modify the number or order of execution of this load with other
// volatile operations.

.decl load_instr_is_volatile(instr:LoadInstruction)


// If the load is marked as atomic, it takes an extra ordering
// and optional singlethread argument.

.decl load_instr_is_atomic(instr:LoadInstruction)

load_instr_is_atomic(Instr) :-
   load_instr_ordering(Instr, _).


// The argument to the load instr specifies the memory address
// from which to load.

.decl load_instr_address(instr:LoadInstruction, pointer:Operand)


// Helper predicates

.decl load_instr_address_ptr_type(instr:LoadInstruction, type:Type) 

load_instr_address_ptr_type(Instr, PtrType) :-
   load_instr_address(Instr, PtrAddress),
   operand_has_type(PtrAddress, PtrType).


//------------------------------------------------------------------------------
// [Constraints]
//
//  (i)  The pointer must point to a first class type.
//
//  (ii) The release and acq_rel orderings are not valid on load instrs.
//------------------------------------------------------------------------------

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   load_instr(Instr),
   !load_instr_address(Instr, _).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   load_instr(Instr),
   load_instr_address_ptr_type(Instr, PtrType),
   !pointer_type_to_firstclass(PtrType).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   load_instr(Instr),
   load_instr_address_ptr_type(Instr, PtrType),
   pointer_type_has_component(PtrType, CompType),
   !instr_returns_type(Instr, CompType).

schema_invalid_instr(Instr, __FILE__, __LINE__) :-
   schema_sanity(),
   load_instr(Instr),
   load_instr_ordering(Instr, Ord),
   ( release_ordering(Ord)
   ; acq_rel_ordering(Ord) ).
