.type ContextItem = CallBase | symbol

//---------------------------------------------------------
// The Context datatype
//---------------------------------------------------------

// TODO(lb): Put notes here on Souffle record performance.
//
// NOTE(lb): AFAIK, Souffle can't index fields of records. Therefore, when
// matching on a destructuring of a record, it has to scan the whole table.

.type Context = [
    head : ContextItem,
    tail : Context
]

// Well-formed, reachable contexts
.decl context(ctx: Context)

.decl max_context_depth(n: number)

.decl insensitive()
insensitive() :- user_options("context_sensitivity", "insensitive").

max_context_depth(n) :-
  !insensitive(),
  user_options("context_sensitivity", Config),
  ns = substr(Config, 0, 1),
  n = to_number(ns).

//---------------------------------------------------------
// Merge
//---------------------------------------------------------

.decl context_depth(n: number, ctx: Context)

context_depth(0, nil).
context_depth(1 + tailLen, [head, tail]) :-
  context([head, tail]),
  context_depth(tailLen, tail).

.decl drop_last(out: Context, in: Context)

drop_last(nil, ?in)
  :-
  context_depth(1, ?in).

drop_last(?out, ?in),
  context(?out)
  :-  // base case
  context(?in),
  // Variable ?tailHead is unused, but required for Souffle to consider this
  // record grounded.
  ?in = [?head, [?tailHead, nil]],
  ?out = [?head, nil].

drop_last(?out, ?in),
  context(?out)
  :-  // recursive case
  context(?in),
  ?in = [?head, [?tailHead, ?tailTail]],
  drop_last(?droppedTailTail, ?tailTail),
  ?out = [?head, [?tailHead, ?droppedTailTail]].

// This component is parameterized over callgraph information
.comp Merge {

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

  .decl reachable_context(?ctx: Context, ?func: FunctionDecl) inline

  //----------------------------------------------------------------------------
  // "Output"/defined rules
  //
  // By convention, rules that begin with an underscore are internal
  // implementation details, and should not be accessed outside the component.
  //----------------------------------------------------------------------------

  .decl _reachable_call(?ctx: Context, ?instr: CallBase)
  _reachable_call(?ctx, ?instr) :-
    (call_instr(?instr); invoke_instr(?instr)),
    instr_func(?instr, ?func),
    reachable_context(?ctx, ?func).

  // Merge is the constructor for new calling contexts.
  // The arguments are:
  //
  // 0. The new context
  // 1. The call site
  // 2. The current calling context
  .decl merge(?newCtx: Context,
              ?callerInstr: CallBase,
              ?callerCtx: Context)

  // The case of a "dropped" context item, see drop.dl
  merge(?oldCtx,
        ?callerInstr,
        ?oldCtx)
   :-
    ! insensitive(),
    _reachable_call(?oldCtx, ?callerInstr),
    drop_context_item_by_invoc(?callerInstr),
    ! drop_context_by_invoc(?callerInstr).

  // The case of a whole "dropped" context, see drop.dl
  merge(nil,
        ?callerInstr,
        ?oldCtx)
   :-
    ! insensitive(),
    _reachable_call(?oldCtx, ?callerInstr),
    drop_context_by_invoc(?callerInstr).

  // The case of insensitive analysis
  merge(?oldCtx,
        ?callerInstr,
        ?oldCtx)
   :-
    _reachable_call(?oldCtx, ?callerInstr),
    insensitive().

  // The case where the previous context has depth < k
  merge(?newCtx,
        ?callerInstr,
        ?callerCtx),
   context(?newCtx)
   :-
    ! insensitive(),
    _reachable_call(?callerCtx, ?callerInstr),
    context_depth(?callerCtxDepth, ?callerCtx),
    max_context_depth(?maxDepth),
    ?callerCtxDepth < ?maxDepth,
    context_item_by_invoc(?callerInstr, ?newItem),
    ?newCtx = [?newItem, ?callerCtx].

  // The case where the previous context has depth = k
  merge(?newCtx,
        ?callerInstr,
        ?callerCtx),
   context(?newCtx)
   :-
    ! insensitive(),
    _reachable_call(?callerCtx, ?callerInstr),
    context_depth(?callerCtxDepth, ?callerCtx),
    max_context_depth(?maxDepth),
    ?callerCtxDepth = ?maxDepth,
    drop_last(?droppedCallerCtx, ?callerCtx),
    context_item_by_invoc(?callerInstr, ?newItem),
    ?newCtx = [?newItem, ?droppedCallerCtx].

  //---------------------------------------------------------
  // Assertions
  //---------------------------------------------------------

  .decl count_context_items(?instr: CallBase, ?nContextItems: number)
  count_context_items(?instr, ?nContextItems) :-
    (call_instr(?instr); invoke_instr(?instr)),
    !drop_context_by_invoc(?instr),
    !drop_context_item_by_invoc(?instr),
    ?nContextItems = count : context_item_by_invoc(?instr, _).

  .decl count_contexts(?instr: CallBase, ?nContexts: number)
  count_contexts(?instr, ?nContexts) :-
    (call_instr(?instr); invoke_instr(?instr)),
    !drop_context_by_invoc(?instr),
    !drop_context_item_by_invoc(?instr),
    // Have to access internal relation due to inlining
    ?nContexts = count : merge(_, ?instr, _).

  .decl assert_reachable_calls_have_context_items(?instr: CallBase)
  assert_reachable_calls_have_context_items(?instr) :-
    user_options("context_sensitivity", _),
    _reachable_call(_, ?instr),
    count_context_items(?instr, 0).

  .decl assert_reachable_calls_have_contexts(?instr: CallBase)
  assert_reachable_calls_have_contexts(?instr) :-
    user_options("context_sensitivity", _),
    _reachable_call(_, ?instr),
    count_contexts(?instr, 0).
}

//---------------------------------------------------------
// Allocation contexts and record
//---------------------------------------------------------

.decl alloc_context(?ctx : Context)

// Record is the constructor for new allocation contexts.
// The inputs are:
// 1. The current calling context at the allocation site
.decl record(?out: Context, alloc: symbol, ?in: Context) inline

record(?ctx, ?alloc, ?ctx), alloc_context(?ctx) :- context(?ctx).

//---------------------------------------------------------
// Initial contexts
//---------------------------------------------------------

.decl empty_alloc_context(?ctx: Context)
alloc_context(nil).
empty_alloc_context(nil).

.decl empty_context(?ctx: Context)
.decl main_context(?ctx: Context)
.decl startup_context(?ctx: Context)
.decl exit_context(?ctx: Context)

context(nil).
empty_context(nil).

context(?ctx),
  main_context(?ctx)
  :-
  ?ctx = ["<<main-context>>", nil].

context(?ctx),
  startup_context(?ctx)
  :-
  ?ctx = ["<<startup-context>>", nil].

context(?ctx),
  exit_context(?ctx)
  :-
  ?ctx = ["<<exit_context>>", nil].

//---------------------------------------------------------
// Context sensitivity
//---------------------------------------------------------

.decl context_item_by_invoc(?invoc : CallBase, ?ctxItem : ContextItem)
.decl context_item_by_invoc_interim(?invoc : CallBase, ?ctxItem : ContextItem)

context_item_by_invoc(?invoc, ?ctxItem) :-
  context_item_by_invoc_interim(?invoc, ?ctxItem),
  !drop_context_by_invoc(?invoc),
  !drop_context_item_by_invoc(?invoc).

context_item_by_invoc_interim(?invoc, ?ctxItem) :-
  user_options("context_sensitivity", Config),
  ( Config = "insensitive"
  ; Config = "1-callsite"
  ; Config = "2-callsite"
  ; Config = "3-callsite"
  ; Config = "4-callsite"
  ; Config = "5-callsite"
  ; Config = "6-callsite"
  ; Config = "7-callsite"
  ; Config = "8-callsite"
  ; Config = "9-callsite"
  ),
  (call_instr(?invoc);
   invoke_instr(?invoc)),
  ?ctxItem = ?invoc.

context_item_by_invoc_interim(?invoc, ?ctxItem) :-
  user_options("context_sensitivity", Config),
  ( Config = "1-caller"
  ; Config = "2-caller"
  ; Config = "3-caller"
  ; Config = "4-caller"
  ; Config = "5-caller"
  ; Config = "6-caller"
  ; Config = "7-caller"
  ; Config = "8-caller"
  ; Config = "9-caller"
  ),
  (call_instr(?invoc); invoke_instr(?invoc)),
  instr_func(?invoc, ?func),
  func_name(?func, ?name),
  ?ctxItem = ?name.

//---------------------------------------------------------
// Serialization
//---------------------------------------------------------

.decl context_to_string(ctx: Context, str: symbol)
context_to_string(nil, "nil").
context_to_string(ctx, str) :-
  context(ctx),
  ctx = [item, tail],
  context_to_string(tail, tailStr),
  str = cat(item, "#", tailStr).
