Assert.qll

import cpp
import codingstandards.cpp.ast.Conditions
import codingstandards.cpp.ast.Search

/**
 * The assert macro.
 */
class AssertMacro extends Macro {
  AssertMacro() { this.getName() = "assert" }
}

/**
 * An assertion via the `assert` macro.
 */
class AssertInvocation extends MacroInvocation {
  AssertInvocation() { this.getMacro() instanceof AssertMacro }

  /**
   * Get the expression that is being asserted, for example, `x > 0` in `assert(x > 0);`.
   *
   * Since the assert macro may expand to various forms of conditional statements, this method
   * uses a combination of AST inspection and control flow analysis to determine the actual
   * condition being asserted.
   *
   * For example, `assert(x)` may expand to `{ if (!__unlikely(x)) abort(); }`. In this case:
   * - We first identify the "outermost conditonal" generated by the macro, which is the `if`
   *   statement, with the raw condition `!__unlikely(x)`.
   * - We then analyze the control flow to see if the abort occurs when this raw condition is true
   *   or false. In this case, it aborts when the raw condition `!__unlikely(x)` is true.
   * - To unwrap the user provided condition `x` from the raw condition, we remove the compiler
   *   intrinsics such as `__unlikely`.
   * - Lastly, we also account for the negation. Since the program aborts on `!x`, we know we are
   *   asserting `!x` is false, which is equivalent to asserting `x` is true.
   *
   * Note that the last two bullets are handled in either order, to support `!__unlikely(x)` or
   * `__unlikely(!x)`.
   */
  Expr getAssertCondition() {
    exists(Conditional conditional, Expr condition, Boolean isTrue |
      // Get the outermost conditional in the assert body (if, &&, ||, ?:, etc).
      conditional = OutermostSearch<Conditional>::find(this.getGeneratedBody()) and
      condition = conditional.getCondition() and
      // An assertion of form `assert(x)` may expand to a negated form, e.g. `if (!x) abort()`, or
      // it may expand to a non-negated form e.g. `x || abort()`. We check whether the condition
      // appears to abort when `condition` is true or false to distinguish these cases.
      Asserts::appearsToAssert(conditional, isTrue) and
      // If we seem to be asserting the condition is both true and false, give no result.
      not Asserts::appearsToAssert(conditional, isTrue.booleanNot()) and
      // Unwrap compiler inserted calls around the actual asserted condition such as `__unlikely`,
      // and unwrap conditions such as `!x` if we found `appearsToAssert(conditional, false)`.
      result = Asserts::unwrapAssertRawCondition(condition, isTrue.booleanNot())
    )
  }

  /**
   * Helper method to get the body whether it is a statement or an expression.
   */
  Element getGeneratedBody() { result = this.getStmt() or result = this.getExpr() }

  /**
   * Holds if this is an assertion of the form `assert(false)` or `assert(false && "message")`.
   */
  predicate isAssertFalse() {
    exists(Expr assertCondition |
      assertCondition = this.getAssertCondition() and
      (
        // plain `assert(false)`
        assertCondition.(Literal).getValue() = "0"
        or
        // with literal, e.g. `assert(false && "message")`
        exists(LogicalAndExpr lAnd |
          lAnd = assertCondition and
          lAnd.getLeftOperand().(Literal).getValue() = "0" and
          lAnd.getRightOperand() instanceof StringLiteral
        )
      )
    )
  }
}

private module Asserts {
  /**
   * The outermost condition of an assert macro may not be the actual condition passed to assert, as
   * the compiler may insert special calls like `__unlikely` or `__builtin_expect` around it. This
   * function unwraps those calls to get to the actual condition.
   *
   * `negated` indicates whether negations were unwrapped. For example, `assert(x)` may expand
   * to `if (!x) abort();`, so this predicate would hold for `(x, true)` and `(!x, false)`.
   */
  Expr unwrapAssertRawCondition(Expr e, Boolean negated) {
    exists(Boolean inner_negated |
      result = unwrapAssertRawCondition(e.(NotExpr).getOperand(), inner_negated) and
      negated = inner_negated.booleanNot()
    )
    or
    if e.(FunctionCall).getTarget().getName().matches("__%")
    then result = unwrapAssertRawCondition(e.(FunctionCall).getArgument(0), negated)
    else (
      result = e and negated = false
    )
  }

  /**
   * Holds if the given conditional appears to assert its condition to be `isTrue`.
   *
   * For example, `x || abort();` appears to assert `x` is true, while `if (!x) abort();`
   * appears to assert `x` is false.
   */
  predicate appearsToAssert(Conditional conditional, Boolean isTrue) {
    // Check if an aborting side is reachable via the given boolean value of the condition.
    sideAborts(conditional, _, isTrue.booleanNot())
    or
    // If the condition is a constant value, then we may not be able to reach the side that aborts
    // via control flow. Detect such cases here.
    not sideAborts(conditional, _, _) and
    (
      // If the false side is unreachable, we presume the false side aborts when reachable
      not exists(conditional.getCondition().getAFalseSuccessor()) and
      // Therefore this asserts the condition is true
      isTrue = true
      or
      // If the true side is unreachable, we presume the true side aborts when reachable
      not exists(conditional.getCondition().getATrueSuccessor()) and
      // Therefore this asserts the condition is false
      isTrue = false
    )
  }

  /**
   * Holds if a control flow node contained by the `conditional` ast node appears to abort the
   * program when the condition evaluates to `isTrue`.
   */
  predicate sideAborts(Conditional conditional, Expr abort, Boolean isTrue) {
    abort.getEnclosingElement*() = conditional and
    appearsToAbort(abort) and
    exists(ControlFlowNode branch |
      branch.getASuccessor*() = abort and
      (
        isTrue = true and
        branch = conditional.getCondition().(ControlFlowNode).getATrueSuccessor()
        or
        isTrue = false and
        branch = conditional.getCondition().(ControlFlowNode).getAFalseSuccessor()
      )
    )
  }

  /**
   * Holds if a control flow node appears to abort the program.
   *
   * We currently detect:
   * - Calls to functions with "fail" or "abort" in their name.
   * - Calls to functions beginning with "__" and containing "assert" in their name.
   * - Nodes with no successors (e.g. a call to `std::terminate` or a throw statement).
   */
  predicate appearsToAbort(ControlFlowNode node) {
    node.(FunctionCall).getTarget().getName().matches(["%fail%", "%abort%", "__%assert"])
    or
    not exists(node.getASuccessor()) and not node instanceof Conversion
  }
}

import Asserts