/**
 * Provides classes and predicates for defining flow summaries.
 */

private import cpp as Cpp
private import codeql.dataflow.internal.FlowSummaryImpl
private import codeql.dataflow.internal.AccessPathSyntax as AccessPath
private import semmle.code.cpp.ir.dataflow.internal.DataFlowPrivate
private import semmle.code.cpp.ir.dataflow.internal.DataFlowUtil
private import semmle.code.cpp.ir.dataflow.internal.DataFlowImplSpecific as DataFlowImplSpecific
private import semmle.code.cpp.dataflow.ExternalFlow
private import semmle.code.cpp.ir.IR

module Input implements InputSig<DataFlowImplSpecific::CppDataFlow> {
  class SummarizedCallableBase = Function;

  ArgumentPosition callbackSelfParameterPosition() { result = TDirectPosition(-1) }

  ReturnKind getStandardReturnValueKind() { result.(NormalReturnKind).getIndirectionIndex() = 0 }

  string encodeParameterPosition(ParameterPosition pos) { result = pos.toString() }

  string encodeArgumentPosition(ArgumentPosition pos) { result = pos.toString() }

  string encodeReturn(ReturnKind rk, string arg) {
    rk != getStandardReturnValueKind() and
    result = "ReturnValue" and
    arg = rk.toString()
  }

  string encodeContent(ContentSet cs, string arg) {
    exists(FieldContent c |
      cs.isSingleton(c) and
      result = "Field" and
      arg = c.getField().getName()
    )
    // TODO: indirection support here?
  }

  string encodeWithoutContent(ContentSet c, string arg) {
    result = "WithoutContent" + c and arg = ""
  }

  string encodeWithContent(ContentSet c, string arg) { result = "WithContent" + c and arg = "" }

  bindingset[token]
  ParameterPosition decodeUnknownParameterPosition(AccessPath::AccessPathTokenBase token) {
    // needed to support `Argument[x..y]` ranges and `Argument[-1]`
    token.getName() = "Argument" and
    exists(int pos | pos = AccessPath::parseInt(token.getAnArgument()) |
      result = TDirectPosition(pos)
    )
  }

  bindingset[token]
  ArgumentPosition decodeUnknownArgumentPosition(AccessPath::AccessPathTokenBase token) {
    // needed to support `Parameter[x..y]` ranges and `Parameter[-1]`
    token.getName() = "Parameter" and
    exists(int pos | pos = AccessPath::parseInt(token.getAnArgument()) |
      result = TDirectPosition(pos)
    )
  }
}

private import Make<DataFlowImplSpecific::CppDataFlow, Input> as Impl

private module StepsInput implements Impl::Private::StepsInputSig {
  DataFlowCall getACall(Public::SummarizedCallable sc) {
    result.getStaticCallTarget().getUnderlyingCallable() = sc
  }
}

module SourceSinkInterpretationInput implements
  Impl::Private::External::SourceSinkInterpretationInputSig<Location>
{
  class Element = Cpp::Element;

  class SourceOrSinkElement = Element;

  /**
   * Holds if an external source specification exists for `e` with output specification
   * `output`, kind `kind`, and provenance `provenance`.
   */
  predicate sourceElement(SourceOrSinkElement e, string output, string kind) {
    exists(
      string namespace, string type, boolean subtypes, string name, string signature, string ext
    |
      sourceModel(namespace, type, subtypes, name, signature, ext, output, kind, _) and
      e = interpretElement(namespace, type, subtypes, name, signature, ext)
    )
  }

  /**
   * Holds if an external sink specification exists for `e` with input specification
   * `input`, kind `kind` and provenance `provenance`.
   */
  predicate sinkElement(SourceOrSinkElement e, string input, string kind) {
    exists(
      string package, string type, boolean subtypes, string name, string signature, string ext
    |
      sinkModel(package, type, subtypes, name, signature, ext, input, kind, _) and
      e = interpretElement(package, type, subtypes, name, signature, ext)
    )
  }

  private newtype TInterpretNode =
    TElement_(Element n) or
    TNode_(Node n)

  /** An entity used to interpret a source/sink specification. */
  class InterpretNode extends TInterpretNode {
    /** Gets the element that this node corresponds to, if any. */
    SourceOrSinkElement asElement() { this = TElement_(result) }

    /** Gets the data-flow node that this node corresponds to, if any. */
    Node asNode() { this = TNode_(result) }

    /** Gets the call that this node corresponds to, if any. */
    DataFlowCall asCall() {
      this.asElement() = result.asCallInstruction().getUnconvertedResultExpression()
      // TODO: or summary call?
    }

    /** Gets the callable that this node corresponds to, if any. */
    DataFlowCallable asCallable() { result.getUnderlyingCallable() = this.asElement() }

    /** Gets the target of this call, if any. */
    Element getCallTarget() { result = this.asCall().getStaticCallTarget().getUnderlyingCallable() }

    /** Gets a textual representation of this node. */
    string toString() {
      result = this.asElement().toString()
      or
      result = this.asNode().toString()
      or
      result = this.asCall().toString()
    }

    /** Gets the location of this node. */
    Location getLocation() {
      result = this.asElement().getLocation()
      or
      result = this.asNode().getLocation()
      or
      result = this.asCall().getLocation()
    }
  }

  /** Provides additional sink specification logic. */
  bindingset[c]
  predicate interpretOutput(string c, InterpretNode mid, InterpretNode node) {
    // Allow fields to be picked as output nodes.
    exists(Node n, Element ast |
      n = node.asNode() and
      ast = mid.asElement()
    |
      c = "" and
      n.asExpr().(VariableAccess).getTarget() = ast
    )
  }

  /** Provides additional source specification logic. */
  bindingset[c]
  predicate interpretInput(string c, InterpretNode mid, InterpretNode node) {
    exists(Node n, Element ast, VariableAccess e |
      n = node.asNode() and
      ast = mid.asElement() and
      e.getTarget() = ast
    |
      // Allow fields to be picked as input nodes.
      c = "" and
      e.getQualifier() = n.asExpr()
      or
      // Allow variables to be picked as input nodes.
      // We could simply do this as `e = n.asExpr()`, but that would not allow
      // us to pick `x` as a sink in an example such as `x = source()` (but
      // only subsequent uses of `x`) since the variable access on `x` doesn't
      // actually load the value of `x`. So instead, we pick the instruction
      // node corresponding to the generated `StoreInstruction` and use the
      // expression associated with the destination instruction. This means
      // that the `x` in `x = source()` can be marked as an input.
      c = "" and
      exists(StoreInstruction store |
        store.getDestinationAddress().getUnconvertedResultExpression() = e and
        n.asInstruction() = store
      )
      or
      // Allow post update nodes to be picked as input nodes when the `input` column
      // of the row is `PostUpdate`.
      c = "PostUpdate" and
      e.getQualifier() = n.(PostUpdateNode).getPreUpdateNode().asExpr()
    )
  }
}

module Private {
  import Impl::Private

  module Steps = Impl::Private::Steps<StepsInput>;

  module External {
    import Impl::Private::External
    import Impl::Private::External::SourceSinkInterpretation<Location, SourceSinkInterpretationInput>
  }

  /**
   * Provides predicates for constructing summary components.
   */
  module SummaryComponent {
    private import Impl::Private::SummaryComponent as SC

    predicate parameter = SC::parameter/1;

    predicate argument = SC::argument/1;

    predicate content = SC::content/1;

    predicate withoutContent = SC::withoutContent/1;

    predicate withContent = SC::withContent/1;
  }

  /**
   * Provides predicates for constructing stacks of summary components.
   */
  module SummaryComponentStack {
    private import Impl::Private::SummaryComponentStack as SCS

    predicate singleton = SCS::singleton/1;

    predicate push = SCS::push/2;

    predicate argument = SCS::argument/1;
  }
}

module Public = Impl::Public;