// See doc/signatures.rst for documentation on signature_*
.decl signature_return_alloc(?func : FunctionName)
.decl signature_return_alloc_once(?func : FunctionName)
.decl signature_return_aliases_arg(?func : FunctionName, ?index : ArgumentIndex)
.decl signature_return_aliases_arg_reachable(?func : FunctionName, ?index : ArgumentIndex)
.decl signature_return_points_to_global(?func : FunctionName, ?global : GlobalVarName)
.decl signature_return_aliases_global(?func : FunctionName, ?global : GlobalVarName)
.decl signature_return_aliases_global_reachable(?func : FunctionName, ?global : GlobalVarName)
.decl signature_arg_alloc(?func : FunctionName, ?index : ArgumentIndex)
.decl signature_arg_alloc_once(?func : FunctionName, ?index : ArgumentIndex)
.decl signature_arg_memcpy_arg(?func : FunctionName, ?index1 : ArgumentIndex, ?index2 : ArgumentIndex)
.decl signature_arg_memcpy_arg_reachable(?func : FunctionName, ?index1 : ArgumentIndex, ?index2 : ArgumentIndex)
.decl signature_arg_points_to_global(?func : FunctionName, ?index : ArgumentIndex, ?global : GlobalVarName)
.decl signature_arg_memcpy_global(?func : FunctionName, ?index : ArgumentIndex, ?global : GlobalVarName)
.decl signature_arg_memcpy_global_reachable(?func : FunctionName, ?index : ArgumentIndex, ?global : GlobalVarName)
.decl signature_global_memcpy_arg(?func : FunctionName, ?global : GlobalVarName, ?index : ArgumentIndex)
.decl signature_global_memcpy_arg_reachable(?func : FunctionName, ?global : GlobalVarName, ?index : ArgumentIndex)
.decl signature_none(?func : FunctionName)

.decl func_needs_signature(?func : FunctionDecl)
.decl func_pts_signature(?func : FunctionDecl)
.decl func_missing_signature(?func : FunctionDecl)

.decl type_has_subelement(?type : Type, ?elem : Type)

type_has_subelement(?type, ?elem) :-
  type_has_subelement(?type, ?mid),
  array_type_has_component(?mid, ?elem).

type_has_subelement(?type, ?elem) :-
  type_has_subelement(?type, ?mid),
  struct_type_field(?mid, _, ?elem).

type_has_subelement(?type, ?elem) :-
  type_has_subelement(?type, ?mid),
  vector_type_has_component(?mid, ?elem).

type_has_subelement(?type, ?type) :-
  type(?type).

func_needs_signature(?func) :-
  func_decl(?func),
  func_name(?func, ?name),
  !(func_decl_to_defn(?func,_);
    heap_alloc_func(?func);
    "@memcpy"=substr(?name,0,7);
    "@llvm.memcpy"=substr(?name,0,12)),
  func_ty(?func, ?type),
  func_type_return(?type, ?rtype),
  pointer_type(?rtype).

func_needs_signature(?func) :-
  func_decl(?func),
  func_name(?func, ?name),
  !(func_decl_to_defn(?func,_);
    heap_alloc_func(?func);
    "@memcpy"=substr(?name,0,7);
    "@llvm.memcpy"=substr(?name,0,12)),
  func_ty(?func, ?type),
  func_type_param(?type, _, ?ptype),
  pointer_type_has_component(?ptype, ?comp),
  type_has_subelement(?comp, ?elem),
  pointer_type(?elem).

func_pts_signature(?func) :-
  func_name(?func, ?name),
  (signature_none(?name);
   signature_return_alloc(?name);
   signature_return_alloc_once(?name);
   signature_return_aliases_arg(?name, _);
   signature_return_aliases_arg_reachable(?name, _);
   signature_return_points_to_global(?name, _);
   signature_return_aliases_global(?name, _);
   signature_return_aliases_global_reachable(?name, _);
   signature_arg_alloc(?name, _);
   signature_arg_alloc_once(?name, _);
   signature_arg_memcpy_arg(?name, _, _);
   signature_arg_memcpy_arg_reachable(?name, _, _);
   signature_arg_points_to_global(?name, _, _);
   signature_arg_memcpy_global(?name, _, _);
   signature_arg_memcpy_global_reachable(?name, _, _);
   signature_global_memcpy_arg(?name, _, _);
   signature_global_memcpy_arg_reachable(?name, _, _)).

func_missing_signature(?func) :-
  func_needs_signature(?func),
  !func_pts_signature(?func).

//------------------------------------------------------------------------------
//  Allocation funcs
//------------------------------------------------------------------------------

.decl build_signature_allocation(sigAlloc: SignatureAllocation, func: Function, caller: Function, type: Type, var: Variable, pos: symbol) inline
build_signature_allocation(sigAlloc, func, caller, type, var, pos) :-
  func_name(func, funcName),
  func_name(caller, callerName),
  variable_has_name(var, varName),
  sigAlloc = cat("*sig_alloc", funcName, "|", callerName, "[", type, " ", varName, "(", pos, ")", "]").

.decl build_signature_allocation_once(sigAlloc: SignatureAllocation, func: Function, type: Type, pos: symbol) inline
build_signature_allocation_once(sigAlloc, func, type, pos) :-
  func_name(func, funcName),
  sigAlloc = cat("*sig_alloc", funcName, "[", type, "(", pos, ")]").

.comp Signatures {

  //----------------------------------------------------------------------------
  // "Input"/declared rules
  //
  // https://souffle-lang.github.io/components#input-rules
  //----------------------------------------------------------------------------

  .decl allocation_type(?alloc:Allocation, ?type:Type) inline
  .decl alloc_may_alias(?alloc1: Allocation, ?alloc2: Allocation) inline
  .decl alloc_with_ctx(?aCtx: Context, ?alloc: Allocation) inline
  .decl callgraph_edge(?calleeCtx: Context, ?callee: FunctionDecl, ?callerCtx: Context, ?callerInstr: CallBase) inline
  .decl reachable_context(?ctx: Context, ?func: FunctionDecl) inline
  .decl operand_points_to(?aCtx: Context, ?alloc: Allocation, ?ctx: Context, ?operand: Operand) inline
  .decl ptr_points_to(?aCtx: Context, ?alloc: Allocation, ?ctx: Context, ?ptr: Allocation) inline
  .decl var_points_to(?aCtx: Context, ?alloc: Allocation, ?ctx: Context, ?var: Variable) inline

  //----------------------------------------------------------------------------
  // "Output"/defined rules
  //
  // NOTE! This component can compute new points-to facts, and these need to be
  // propagated back into the points-to component.
  //----------------------------------------------------------------------------

  .decl sig_allocation_type(?alloc:Allocation, ?type:Type) inline

  .decl sig_ptr_points_to(?aCtx: Context, ?alloc: Allocation, ?ptrACtx: Context, ?ptrAlloc: Allocation)
  .decl sig_var_points_to(?aCtx: Context, ?alloc: Allocation, ?ctx: Context, ?var: Variable) inline

  .decl _sig_var_alloc(?aCtx: Context, ?sigAlloc: SignatureAllocation, ?ctx: Context, ?var: Variable, ?type: Type)
  .decl _sig_ptr_alloc(?aCtx: Context, ?sigAlloc: SignatureAllocation, ?ctx: Context, ?ptr: Allocation, ?type: Type)

  .decl _sig_alloc(?aCtx: Context, ?sigAlloc: SignatureAllocation, ?ctx: Context, ?type: Type) inline

  _sig_alloc(?aCtx, ?sigAlloc, ?ctx, ?type) :-
    _sig_var_alloc(?aCtx, ?sigAlloc, ?ctx, _, ?type).

  _sig_alloc(?aCtx, ?sigAlloc, ?ctx, ?type) :-
    _sig_ptr_alloc(?aCtx, ?sigAlloc, ?ctx, _, ?type).

  alloc_with_ctx(?aCtx, ?sigAlloc) :-
    _sig_alloc(?aCtx, ?sigAlloc, _, _).

  signature_allocation(?sigAlloc) :-
    _sig_alloc(_, ?sigAlloc, _, _).

  sig_allocation_type(?sigAlloc, ?type) :-
    _sig_alloc(_, ?sigAlloc, _, ?type).

  sig_var_points_to(?newCtx, ?sigAlloc, ?ctx, ?var) :-
    _sig_var_alloc(?newCtx, ?sigAlloc, ?ctx, ?var, _).

  sig_ptr_points_to(?newCtx, ?sigAlloc, ?ctx, ?ptr) :-
    _sig_ptr_alloc(?newCtx, ?sigAlloc, ?ctx, ?ptr, _).

  _sig_var_alloc(?newCtx, ?sigAlloc, ?ctx, ?var, ?type) :-
     func_name(?func, ?sname),
     signature_return_alloc(?sname),
     ( call_instr_fn_target(?instr, ?func)
     ; invoke_instr_fn_target(?instr, ?func)),
     instr_assigns_to(?instr, ?var),
     instr_func(?instr,  ?instrFunc),

     variable_has_type(?var,?ptrType),
     pointer_type_has_component(?ptrType, ?type),

     reachable_context(?ctx, ?instrFunc),
     build_signature_allocation(?sigAlloc, ?func, ?instrFunc, ?ptrType, ?var, "return"),
     record(?newCtx, ?sigAlloc, ?ctx).

  _sig_var_alloc(?newCtx, ?sigAlloc, ?ctx, ?var, ?type) :-
     func_name(?func, ?sname),
     signature_return_alloc_once(?sname),
     ( call_instr_fn_target(?instr, ?func)
     ; invoke_instr_fn_target(?instr, ?func)),
     instr_assigns_to(?instr, ?var),
     instr_func(?instr,  ?instrFunc),

     variable_has_type(?var,?ptrType),
     pointer_type_has_component(?ptrType, ?type),

     reachable_context(?ctx, ?instrFunc),
     build_signature_allocation_once(?sigAlloc, ?func, ?ptrType, "return"),
     empty_alloc_context(?newCtx).

  _sig_ptr_alloc(?newCtx, ?sigAlloc, ?ptrCtx, ?ptr, ?type) :-
     func_name(?func, ?sname),
     signature_arg_alloc(?sname, ?index),
     ( call_instr_fn_target(?instr, ?func)
     ; invoke_instr_fn_target(?instr, ?func)),
     instr_func(?instr,  ?instrFunc),
     actual_arg(?instr, ?index, ?var),

     reachable_context(?ctx, ?instrFunc),
     var_points_to(?ptrCtx, ?ptr, ?ctx, ?var),

     allocation_type(?ptr, ?ptrType),
     pointer_type_has_component(?ptrType, ?type),

     ?indexStr = to_string(?index),
     build_signature_allocation(?sigAlloc, ?func, ?instrFunc, ?ptrType, ?var, ?indexStr),
     record(?newCtx, ?sigAlloc, ?ctx).

  _sig_ptr_alloc(?newCtx, ?sigAlloc, ?ptrCtx, ?ptr, ?type) :-
     func_name(?func, ?sname),
     signature_arg_alloc_once(?sname, ?index),
     ( call_instr_fn_target(?instr, ?func)
     ; invoke_instr_fn_target(?instr, ?func)),
     instr_func(?instr,  ?instrFunc),
     actual_arg(?instr, ?index, ?var),

     reachable_context(?ctx, ?instrFunc),
     var_points_to(?ptrCtx, ?ptr, ?ctx, ?var),

     allocation_type(?ptr, ?ptrType),
     pointer_type_has_component(?ptrType, ?type),

     ?indexStr = to_string(?index),
     build_signature_allocation_once(?sigAlloc, ?func, ?ptrType, ?indexStr),
     user_options("context_sensitivity", _),
     empty_alloc_context(?newCtx).

  dynamically_sized_alloc(?sigAlloc) :-
    signature_allocation(?sigAlloc).

  //------------------------------------------------------------------------------
  //  Aliasing
  //------------------------------------------------------------------------------

  .decl signature_var_points_to_base(?aCtx: Context, ?alloc: Allocation, ?ctx: Context, ?var: Variable)
  .decl signature_ptr_points_to_base(?aCtx: Context, ?alloc: Allocation, ?ptrACtx : Context, ?ptrAlloc : Allocation)

  .decl memcpy_sig(?toCtx: Context, ?to: Allocation, ?fromCtx: Context , ?from: Allocation)

  .decl _ptr_reaches_to_request(?ptrACtx: Context, ?ptrAlloc: Allocation)
  .decl _ptr_reaches_to(?aCtx: Context, ?alloc: Allocation, ?ptrACtx: Context, ?ptrAlloc: Allocation)

  _ptr_reaches_to(?ptrACtx, ?ptrAllocAlias, ?ptrACtx, ?ptrAlloc) :-
     _ptr_reaches_to_request(?ptrACtx, ?ptrAlloc),
     alloc_may_alias(?ptrAlloc, ?ptrAllocAlias).

  _ptr_reaches_to(?aCtx, ?allocAlias, ?ptrACtx, ?ptrAlloc) :-
     _ptr_reaches_to(?ptrMidACtx, ?ptrMid, ?ptrACtx, ?ptrAlloc),
     ptr_points_to(?aCtx, ?alloc, ?ptrMidACtx, ?ptrMid),
     alloc_may_alias(?alloc, ?allocAlias).

  signature_var_points_to_base(?aCtx, ?alloc, ?callerCtx, ?toVar) :-
     callgraph_edge(_, ?callee, ?callerCtx, ?callerInstr),
     func_name(?callee, ?name),
     signature_return_aliases_arg(?name, ?index),
     instr_assigns_to(?callerInstr, ?toVar),
     actual_arg(?callerInstr, ?index, ?fromValue),
     operand_points_to(?aCtx, ?alloc, ?callerCtx, ?fromValue).

  _ptr_reaches_to_request(?ptrACtx, ?ptrAlloc) :-
     callgraph_edge(_, ?callee, ?callerCtx, ?callerInstr),
     func_name(?callee, ?name),
     signature_return_aliases_arg_reachable(?name, ?index),
     actual_arg(?callerInstr, ?index, ?fromValue),
     operand_points_to(?ptrACtx, ?ptrAlloc, ?callerCtx, ?fromValue).

  signature_var_points_to_base(?aCtx, ?alloc, ?callerCtx, ?toVar) :-
     callgraph_edge(_, ?callee, ?callerCtx, ?callerInstr),
     func_name(?callee, ?name),
     signature_return_aliases_arg_reachable(?name, ?index),
     instr_assigns_to(?callerInstr, ?toVar),
     actual_arg(?callerInstr, ?index, ?fromValue),
     operand_points_to(?ptrACtx, ?ptrAlloc, ?callerCtx, ?fromValue),
     _ptr_reaches_to(?aCtx, ?alloc, ?ptrACtx, ?ptrAlloc).

  signature_var_points_to_base(?aCtx, ?alloc, ?callerCtx, ?toVar) :-
     callgraph_edge(_, ?callee, ?callerCtx, ?callerInstr),
     func_name(?callee, ?name),
     signature_return_points_to_global(?name, ?globalName),
     global_allocation_by_name(?globalName, ?alloc),
     empty_context(?aCtx),
     instr_assigns_to(?callerInstr, ?toVar).

  signature_var_points_to_base(?aCtx, ?alloc, ?callerCtx, ?toVar) :-
     callgraph_edge(_, ?callee, ?callerCtx, ?callerInstr),
     func_name(?callee, ?name),
     signature_return_aliases_global(?name, ?globalName),
     global_allocation_by_name(?globalName, ?globalAlloc),
     empty_context(?globalCtx),
     instr_assigns_to(?callerInstr, ?toVar),
     ptr_points_to(?aCtx, ?alloc, ?globalCtx, ?globalAlloc).

  _ptr_reaches_to_request(?globalCtx, ?globalAlloc) :-
     callgraph_edge(_, ?callee, _, ?callerInstr),
     func_name(?callee, ?name),
     signature_return_aliases_global_reachable(?name, ?globalName),
     global_allocation_by_name(?globalName, ?globalAlloc),
     empty_context(?globalCtx),
     instr_assigns_to(?callerInstr, _).

  signature_var_points_to_base(?aCtx, ?alloc, ?callerCtx, ?toVar) :-
     callgraph_edge(_, ?callee, ?callerCtx, ?callerInstr),
     func_name(?callee, ?name),
     signature_return_aliases_global_reachable(?name, ?globalName),
     global_allocation_by_name(?globalName, ?globalAlloc),
     empty_context(?globalCtx),
     instr_assigns_to(?callerInstr, ?toVar),
     _ptr_reaches_to(?aCtx, ?alloc, ?globalCtx, ?globalAlloc).

  memcpy_sig(?toACtx, ?toAlloc, ?fromACtx, ?fromAlloc) :-
     callgraph_edge(_, ?callee, ?callerCtx, ?callerInstr),
     func_name(?callee, ?name),
     signature_arg_memcpy_arg(?name, ?toIndex, ?fromIndex),
     actual_arg(?callerInstr, ?toIndex, ?toValue),
     actual_arg(?callerInstr, ?fromIndex, ?fromValue),
     operand_points_to(?toACtx, ?toAlloc, ?callerCtx, ?toValue),
     operand_points_to(?fromACtx, ?fromAlloc, ?callerCtx, ?fromValue).

  _ptr_reaches_to_request(?fromPtrACtx, ?fromPtrAlloc) :-
     callgraph_edge(_, ?callee, ?callerCtx, ?callerInstr),
     func_name(?callee, ?name),
     signature_arg_memcpy_arg_reachable(?name, ?toIndex, ?fromIndex),
     actual_arg(?callerInstr, ?toIndex, ?toValue),
     actual_arg(?callerInstr, ?fromIndex, ?fromValue),
     operand_points_to(_, _, ?callerCtx, ?toValue),
     operand_points_to(?fromPtrACtx, ?fromPtrAlloc, ?callerCtx, ?fromValue).

  memcpy_sig(?toACtx, ?toAlloc, ?fromACtx, ?fromAlloc) :-
     callgraph_edge(_, ?callee, ?callerCtx, ?callerInstr),
     func_name(?callee, ?name),
     signature_arg_memcpy_arg_reachable(?name, ?toIndex, ?fromIndex),
     actual_arg(?callerInstr, ?toIndex, ?toValue),
     actual_arg(?callerInstr, ?fromIndex, ?fromValue),
     operand_points_to(?toACtx, ?toAlloc, ?callerCtx, ?toValue),
     operand_points_to(?fromPtrACtx, ?fromPtrAlloc, ?callerCtx, ?fromValue),
     _ptr_reaches_to(?fromACtx, ?fromAlloc, ?fromPtrACtx, ?fromPtrAlloc).

  signature_ptr_points_to_base(?gACtx, ?gAlloc, ?ptrACtx, ?ptrAlloc) :-
     callgraph_edge(_, ?callee, ?callerCtx, ?callerInstr),
     func_name(?callee, ?name),
     signature_arg_points_to_global(?name, ?index, ?globalName),
     actual_arg(?callerInstr, ?index, ?toValue),
     operand_points_to(?ptrACtx, ?ptrAlloc, ?callerCtx, ?toValue),
     global_allocation_by_name(?globalName, ?gAlloc),
     empty_context(?gACtx).

  memcpy_sig(?toACtx, ?toAlloc, ?fromACtx, ?fromAlloc) :-
     callgraph_edge(_, ?callee, ?callerCtx, ?callerInstr),
     func_name(?callee, ?name),
     signature_arg_memcpy_global(?name, ?index, ?globalName),
     actual_arg(?callerInstr, ?index, ?toValue),
     operand_points_to(?toACtx, ?toAlloc, ?callerCtx, ?toValue),
     global_allocation_by_name(?globalName, ?fromAlloc),
     empty_context(?fromACtx).

  _ptr_reaches_to_request(?gACtx, ?gAlloc) :-
     callgraph_edge(_, ?callee, ?callerCtx, ?callerInstr),
     func_name(?callee, ?name),
     signature_arg_memcpy_global_reachable(?name, ?index, ?globalName),
     actual_arg(?callerInstr, ?index, ?toValue),
     operand_points_to(_, _, ?callerCtx, ?toValue),
     global_allocation_by_name(?globalName, ?gAlloc),
     empty_context(?gACtx).

  memcpy_sig(?toACtx, ?toAlloc, ?fromACtx, ?fromAlloc) :-
     callgraph_edge(_, ?callee, ?callerCtx, ?callerInstr),
     func_name(?callee, ?name),
     signature_arg_memcpy_global_reachable(?name, ?index, ?globalName),
     actual_arg(?callerInstr, ?index, ?toValue),
     operand_points_to(?toACtx, ?toAlloc, ?callerCtx, ?toValue),
     global_allocation_by_name(?globalName, ?gAlloc),
     empty_context(?gACtx),
     _ptr_reaches_to(?fromACtx, ?fromAlloc, ?gACtx, ?gAlloc).

  memcpy_sig(?toACtx, ?toAlloc, ?fromACtx, ?fromAlloc) :-
     callgraph_edge(_, ?callee, ?callerCtx, ?callerInstr),
     func_name(?callee, ?name),
     signature_global_memcpy_arg(?name, ?globalName, ?index),
     actual_arg(?callerInstr, ?index, ?toValue),
     operand_points_to(?fromACtx, ?fromAlloc, ?callerCtx, ?toValue),
     global_allocation_by_name(?globalName, ?toAlloc),
     empty_context(?toACtx).

  _ptr_reaches_to_request(?ptrACtx, ?ptrAlloc) :-
     callgraph_edge(_, ?callee, ?callerCtx, ?callerInstr),
     func_name(?callee, ?name),
     signature_global_memcpy_arg_reachable(?name, _, ?index),
     actual_arg(?callerInstr, ?index, ?toValue),
     operand_points_to(?ptrACtx, ?ptrAlloc, ?callerCtx, ?toValue).

  memcpy_sig(?toACtx, ?toAlloc, ?fromACtx, ?fromAlloc) :-
     callgraph_edge(_, ?callee, ?callerCtx, ?callerInstr),
     func_name(?callee, ?name),
     signature_global_memcpy_arg_reachable(?name, ?globalName, ?index),
     actual_arg(?callerInstr, ?index, ?toValue),
     operand_points_to(?ptrACtx, ?ptrAlloc, ?callerCtx, ?toValue),
     global_allocation_by_name(?globalName, ?toAlloc),
     empty_context(?toACtx),
     _ptr_reaches_to(?fromACtx, ?fromAlloc, ?ptrACtx, ?ptrAlloc).

  //------------------------------------------------------------------------------
  //  Points-to updates
  //------------------------------------------------------------------------------

  sig_var_points_to(?baseACtx, ?baseAlloc, ?callerCtx, ?toVar) :-
     signature_var_points_to_base(?baseACtx, ?baseAlloc, ?callerCtx, ?toVar),
     variable_has_type(?toVar, ?toPtrType),
     pointer_type_has_component(?toPtrType, ?toType),
     allocation_type(?baseAlloc, ?allocType),
     type_compatible(?allocType, ?toType).

  //var_points_to(?baseACtx, ?alloc, ?callerCtx, ?toVar) :-
  //   signature_var_points_to_base(?baseACtx, ?baseAlloc, ?callerCtx, ?toVar),
  //   alloc_subregion_base(?alloc, ?baseAlloc),
  //   variable_has_type(?toVar, ?toPtrType),
  //   pointer_type_has_component(?toPtrType, ?toType),
  //   allocation_type(?alloc, ?allocType),
  //   type_compatible(?allocType, ?toType).

  sig_ptr_points_to(?baseACtx, ?baseAlloc, ?ptrACtx, ?ptrAlloc) :-
     signature_ptr_points_to_base(?baseACtx, ?baseAlloc, ?ptrACtx, ?ptrAlloc),
     allocation_type(?baseAlloc, ?allocType),
     allocation_type(?ptrAlloc, ?ptrType),
     pointer_type_has_component(?ptrType, ?toType),
     type_compatible(?allocType, ?toType).

  //ptr_points_to(?baseACtx, ?baseSubAlloc, ?ptrACtx, ?ptrAlloc) :-
  //   signature_ptr_points_to_base(?baseACtx, ?baseAlloc, ?ptrACtx, ?ptrAlloc),
  //   alloc_subregion_base(?baseSubAlloc, ?baseAlloc),
  //   allocation_type(?baseSubAlloc, ?allocType),
  //   allocation_type(?ptrAlloc, ?ptrType),
  //   pointer_type_has_component(?ptrType, ?toType),
  //   type_compatible(?allocType, ?toType).

  //ptr_points_to(?baseACtx, ?baseAlloc, ?ptrACtx, ?ptrSubAlloc) :-
  //   signature_ptr_points_to_base(?baseACtx, ?baseAlloc, ?ptrACtx, ?ptrAlloc),
  //   alloc_subregion_base(?ptrSubAlloc, ?ptrAlloc),
  //   allocation_type(?baseAlloc, ?allocType),
  //   allocation_type(?ptrSubAlloc, ?ptrType),
  //   pointer_type_has_component(?ptrType, ?toType),
  //   type_compatible(?allocType, ?toType).

  //ptr_points_to(?baseACtx, ?baseSubAlloc, ?ptrACtx, ?ptrSubAlloc) :-
  //   signature_ptr_points_to_base(?baseACtx, ?baseAlloc, ?ptrACtx, ?ptrAlloc),
  //   alloc_subregion_base(?baseSubAlloc, ?baseAlloc),
  //   alloc_subregion_base(?ptrSubAlloc, ?ptrAlloc),
  //   allocation_type(?baseSubAlloc, ?allocType),
  //   allocation_type(?ptrSubAlloc, ?ptrType),
  //   pointer_type_has_component(?ptrType, ?toType),
  //   type_compatible(?allocType, ?toType).

}
