codeql/python/ql/lib/semmle/python/dataflow/old/StateTracking.qll

/**
 * Provides classes and predicates for tracking global state across the control flow and call graphs.
 *
 * NOTE: State tracking tracks both whether a state may apply to a given node in a given context *and*
 * whether it may not apply.
 * That `state.appliesTo(f, ctx)` holds implies nothing about whether `state.mayNotApplyTo(f, ctx)` holds.
 * Neither may hold which merely means that `f` with context `ctx` is not reached during the analysis.
 * Conversely, both may hold, which means that `state` may or may not apply depending on how `f` was reached.
 */

import python
private import LegacyPointsTo

/** A state that should be tracked. */
abstract class TrackableState extends string {
  bindingset[this]
  TrackableState() { this = this }

  /** Holds if this state may apply to the control flow node `f`, regardless of the context. */
  final predicate appliesTo(ControlFlowNode f) { this.appliesTo(f, _) }

  /** Holds if this state may not apply to the control flow node `f`, given the context `ctx`. */
  final predicate appliesTo(ControlFlowNode f, Context ctx) {
    StateTracking::appliesToNode(this, f, ctx, true)
  }

  /** Holds if this state may apply to the control flow node `f`, given the context `ctx`. */
  final predicate mayNotApplyTo(ControlFlowNode f, Context ctx) {
    StateTracking::appliesToNode(this, f, ctx, false)
  }

  /** Holds if this state may apply to the control flow node `f`, regardless of the context. */
  final predicate mayNotApplyTo(ControlFlowNode f) { this.mayNotApplyTo(f, _) }

  /** Holds if `test` shows value to be untainted with `taint`, given the context `ctx`. */
  predicate testsFor(PyEdgeRefinement test, Context ctx, boolean sense) {
    ctx.appliesToScope(test.getScope()) and this.testsFor(test, sense)
  }

  /** Holds if `test` shows value to be untainted with `taint` */
  predicate testsFor(PyEdgeRefinement test, boolean sense) { none() }

  /**
   * Holds if state starts at `f`.
   * Either this predicate or `startsAt(ControlFlowNode f, Context ctx)`
   * should be overridden by sub-classes.
   */
  predicate startsAt(ControlFlowNode f) { none() }

  /**
   * Holds if state starts at `f` given context `ctx`.
   * Either this predicate or `startsAt(ControlFlowNode f)`
   * should be overridden by sub-classes.
   */
  pragma[noinline]
  predicate startsAt(ControlFlowNode f, Context ctx) { ctx.appliesTo(f) and this.startsAt(f) }

  /**
   * Holds if state ends at `f`.
   * Either this predicate or `endsAt(ControlFlowNode f, Context ctx)`
   * may be overridden by sub-classes.
   */
  predicate endsAt(ControlFlowNode f) { none() }

  /**
   * Holds if state ends at `f` given context `ctx`.
   * Either this predicate or `endsAt(ControlFlowNode f)`
   * may be overridden by sub-classes.
   */
  pragma[noinline]
  predicate endsAt(ControlFlowNode f, Context ctx) { ctx.appliesTo(f) and this.endsAt(f) }
}

module StateTracking {
  private predicate not_allowed(TrackableState state, ControlFlowNode f, Context ctx, boolean sense) {
    state.endsAt(f, ctx) and sense = true
    or
    state.startsAt(f, ctx) and sense = false
  }

  /**
   * Holds if `state` may apply (with `sense` = true) or may not apply (with `sense` = false) to
   * control flow node `f` given the context `ctx`.
   */
  predicate appliesToNode(TrackableState state, ControlFlowNode f, Context ctx, boolean sense) {
    state.endsAt(f, ctx) and sense = false
    or
    state.startsAt(f, ctx) and sense = true
    or
    not not_allowed(state, f, ctx, sense) and
    (
      exists(BasicBlock b |
        /* First node in a block */
        f = b.getNode(0) and appliesAtBlockStart(state, b, ctx, sense)
        or
        /* Other nodes in block, except trackable calls */
        exists(int n |
          f = b.getNode(n) and
          appliesToNode(state, b.getNode(n - 1), ctx, sense) and
          not exists(Context callee | callee.fromCall(f, _, ctx))
        )
      )
      or
      /* Function entry via call */
      exists(PythonFunctionObjectInternal func, CallNode call, Context caller |
        ctx.fromCall(call, func, caller) and
        func.getScope().getEntryNode() = f and
        appliesToNode(state, call.getAPredecessor(), caller, sense)
      )
      or
      /* Function return */
      exists(PythonFunctionObjectInternal func, Context callee |
        callee.fromCall(f, func, ctx) and
        appliesToNode(state, func.getScope().getANormalExit(), callee, sense)
      )
      or
      /* Other scope entries */
      exists(Scope s |
        s.getEntryNode() = f and
        ctx.appliesToScope(s)
      |
        not exists(Scope pred | pred.precedes(s)) and
        (ctx.isImport() or ctx.isRuntime()) and
        sense = false
        or
        exists(Scope pred, Context pred_ctx |
          appliesToNode(state, pred.getANormalExit(), pred_ctx, sense) and
          pred.precedes(s) and
          ctx.isRuntime()
        |
          pred_ctx.isRuntime() or pred_ctx.isImport()
        )
      )
    )
  }

  /**
   * Holds  if `state` may apply (with `sense` = true) or may not apply (with `sense` = false) at the
   * start of basic block `block` given the context `ctx`.
   */
  private predicate appliesAtBlockStart(
    TrackableState state, BasicBlock block, Context ctx, boolean sense
  ) {
    exists(PyEdgeRefinement test |
      test.getSuccessor() = block and
      state.testsFor(test, ctx, sense)
    )
    or
    exists(BasicBlock pred |
      pred.getASuccessor() = block and
      appliesAtBlockEnd(state, pred, ctx, sense) and
      not exists(PyEdgeRefinement test |
        test.getPredecessor() = pred and
        test.getSuccessor() = block and
        state.testsFor(test, sense.booleanNot())
      )
    )
  }

  /**
   * Holds  if `state` may apply (with `sense` = true) or may not apply (with `sense` = false) at the
   * end of basic block `block` given the context `ctx`.
   */
  private predicate appliesAtBlockEnd(
    TrackableState state, BasicBlock block, Context ctx, boolean sense
  ) {
    appliesToNode(state, block.getLastNode(), ctx, sense)
  }
}