//------------------------------------------------------------------------------
// [Atexit Function - Itanium C++ ABI]
//
// Signature:
// int __cxa_atexit(void (*func) (void *), void * arg, void * dso_handle);
//
// Registers a destructor func to be called by exit() or when a
// shared library is unloaded.
//
// Its arguments are:
//   * A pointer to the destructor func
//   * The receiver object of the call
//   * A handle to the shared library
//
// This routine never returns.
//------------------------------------------------------------------------------

.decl cxx_atexit_func(?func: FunctionDecl)

cxx_atexit_func(?func) :-
   func_name(?func, "@__cxa_atexit"),
   func_ty(?func, ?fType),
   func_type_param(?fType, 0, ?type1),
   func_type_param(?fType, 1, ?type2),
   func_type_param(?fType, 2, ?type3),
   pointer_type_has_component(?type1, ?compType1),
   func_type(?compType1),
   integer_pointer_type(?type2),
   integer_pointer_type(?type3),
   func_type_nparams(?fType, 3).


// Model effects of `__cxa_atexit`

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

  .decl alloc_aliases(?alloc1: Allocation, ?alloc2: Allocation) inline
  .decl callgraph_edge(?calleeCtx: Context, ?callee: FunctionDecl, ?callerCtx: Context, ?callerInstr: CallBase) inline
  .decl operand_points_to(?aCtx: Context, ?alloc: Allocation, ?ctx: Context, ?operand: Operand) inline
  .decl reachable_context(?ctx: Context, ?func: FunctionDecl) 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 _registers_dtor_atexit(?callCtx: Context, ?dtorOperand: Operand, ?recvOperand: Operand)
  _registers_dtor_atexit(?callCtx, ?dtorOperand, ?recvOperand) :-
    cxx_atexit_func(?atExit),
    callgraph_edge(_, ?atExit, ?callCtx, ?callInstr),
    call_instr_arg(?callInstr, 0, ?dtorOperand),
    call_instr_arg(?callInstr, 1, ?recvOperand).

  // The following rule augments the logic about identifying funcs
  // registered to run at program exit, so that it also works with
  // func pointers.

  .decl _registers_atexit(?callerCtx: Context, ?funcOp: Operand)

  _registers_atexit(?callerCtx, ?funcOp) :-
    func_name(?atExit, "@atexit"),
    callgraph_edge(_, ?atExit, ?callerCtx, ?callerInstr),
    actual_arg(?callerInstr, 0, ?funcOp).

  // Functions registered to @atexit are also reachable if the @atexit
  // call is reachable.
  .decl called_at_exit(func:FunctionDecl)

  called_at_exit(?callback) :-
    _registers_atexit(?ctx, ?funcOp),
    operand_points_to(_, ?alloc, ?ctx, ?funcOp),
    func_by_location(?alloc, ?callback).

  called_at_exit(Callback) :-
    func_name(AtExit, "@atexit"),
    callgraph_edge(_, AtExit, _, CallerInstr),
    call_instr_arg(CallerInstr, 0, Constant),
    // the following is a simplified version of logic that can only
    // work with direct func calls
    constant_references_func(Constant, Callback).

  .decl _dtor_accepts_recv(?aCtx: Context, ?recvObj: GlobalAllocation , ?dtor: FunctionDecl)

  _dtor_accepts_recv(?aCtx, ?recvObj, ?dtor) :-
    _registers_dtor_atexit(?ctx, ?dtorOperand, ?recvOperand),
    operand_points_to(_, ?dtorObj, ?ctx, ?dtorOperand),
    operand_points_to(?aCtx, ?someObj, ?ctx, ?recvOperand),
    alloc_aliases(?recvObj, ?someObj),
    global_allocation(?recvObj),
    static_allocation_type(?recvObj, ?recvType),
    func_by_location(?dtorObj, ?dtor),
    func_ty(?dtor, ?dtorType),
    func_type_param(?dtorType, 0, ?ptrType),
    pointer_type_has_component(?ptrType, ?recvType).

  called_at_exit(?dtor) :- _dtor_accepts_recv(_, _, ?dtor).

  .decl at_exit_var_points_to(?aCtx: Context, ?alloc: Allocation, ?ctx: Context, ?var: Variable)
  at_exit_var_points_to(?aCtx, ?recvObj, ?exitCtx, ?this) :-
    exit_context(?exitCtx),
    _dtor_accepts_recv(?aCtx, ?recvObj, ?dtor),
    reachable_context(?exitCtx, ?dtor),
    func_param(?dtor, 0, ?this).
}
