/**
 * Simple range analysis library. Range analysis is usually done as an
 * abstract interpretation over the lattice of range values. (A range is a
 * pair, containing a lower and upper bound for the value.) The problem
 * with this approach is that the lattice is very tall, which means it can
 * take an extremely large number of iterations to find the least fixed
 * point. This example illustrates the problem:
 *
 *    int count = 0;
 *    for (; p; p = p->next) {
 *      count = count+1;
 *    }
 *
 * The range of 'count' is initially (0,0), then (0,1) on the second
 * iteration, (0,2) on the third iteration, and so on until we eventually
 * reach maxInt.
 *
 * This library uses a crude solution to the problem described above: if
 * the upper (or lower) bound of an expression might depend recursively on
 * itself then we round it up (down for lower bounds) to one of a fixed set
 * of values, such as 0, 1, 2, 256, and +Inf. This limits the height of the
 * lattice which ensures that the analysis will terminate in a reasonable
 * amount of time. This solution is similar to the abstract interpretation
 * technique known as 'widening', but it is less precise because we are
 * unable to inspect the bounds from the previous iteration of the fixed
 * point computation. For example, widening might be able to deduce that
 * the lower bound is -11 but we would approximate it to -16.
 *
 * QL does not allow us to compute an aggregate over a recursive
 * sub-expression, so we cannot compute the minimum lower bound and maximum
 * upper bound during the recursive phase of the query. Instead, the
 * recursive phase computes a set of lower bounds and a set of upper bounds
 * for each expression. We compute the minimum lower bound and maximum
 * upper bound after the recursion is finished. This is another reason why
 * we need to limit the number of bounds per expression, because they will
 * all be stored until the recursive phase is finished.
 *
 * The ranges are represented using a pair of floating point numbers. This
 * is simpler than using integers because floating point numbers cannot
 * overflow and wrap. It is also convenient because we can detect overflow
 * and negative overflow by looking for bounds that are outside the range
 * of the type.
 */
import cpp
private import RangeAnalysisUtils
import RangeSSA
import SimpleRangeAnalysisCached

/**
 * This fixed set of lower bounds is used when the lower bounds of an
 * expression are recursively defined. The inferred lower bound is rounded
 * down to the nearest lower bound in the fixed set. This restricts the
 * height of the lattice, which prevents the analysis from exploding.
 *
 * Note: these bounds were chosen fairly arbitrarily. Feel free to add more
 * bounds to the set if it helps on specific examples and does not make
 * performance dramatically worse on large codebases, such as libreoffice.
 */
private
float wideningLowerBounds(ArithmeticType t) {
  result = 2.0 or
  result = 1.0 or
  result = 0.0 or
  result = -1.0 or
  result = -2.0 or
  result = -8.0 or
  result = -16.0 or
  result = -128.0 or
  result = -256.0 or
  result = -32768.0 or
  result = -65536.0 or
  result = typeLowerBound(t) or
  result = -(1.0/0.0)  // -Inf
}

/** See comment for `wideningLowerBounds`, above. */
private
float wideningUpperBounds(ArithmeticType t) {
  result = -2.0 or
  result = -1.0 or
  result = 0.0 or
  result = 1.0 or
  result = 2.0 or
  result = 7.0 or
  result = 15.0 or
  result = 127.0 or
  result = 255.0 or
  result = 32767.0 or
  result = 65535.0 or
  result = typeUpperBound(t) or
  result = 1.0/0.0  // +Inf
}

/** Set of expressions which we know how to analyze. */
private
predicate analyzableExpr(Expr e) {
  // The type of the expression must be arithmetic. We reuse the logic in
  // `exprMinVal` to check this.
  exists (exprMinVal(e)) and
  ((exists (e.getValue().toFloat())) or
   (e instanceof UnaryPlusExpr) or
   (e instanceof UnaryMinusExpr) or
   (e instanceof MinExpr) or
   (e instanceof MaxExpr) or
   (e instanceof ConditionalExpr) or
   (e instanceof AddExpr) or
   (e instanceof SubExpr) or
   (e instanceof CrementOperation) or
   (e instanceof RemExpr) or
   (e instanceof CommaExpr) or
   (e instanceof StmtExpr) or

   // A conversion is analyzable, provided that its child has an arithmetic
   // type. (Sometimes the child is a reference type, and so does not get
   // any bounds.) Rather than checking whether the type of the child is
   // arithmetic, we reuse the logic that is already encoded in
   // `exprMinVal`.
   exists(exprMinVal(e.(Conversion).getExpr())) or

   // Also allow variable accesses, provided that they have SSA
   // information.
   exists (RangeSsaDefinition def, LocalScopeVariable v | e = def.getAUse(v)))
}

/**
 * Set of definitions that this definition depends on. The transitive
 * closure of this relation is used to detect definitions which are
 * recursively defined, so that we can prevent the analysis from exploding.
 *
 * The structure of `defDependsOnDef` and its helper predicates matches the
 * structure of `getDefLowerBoundsImpl` and
 * `getDefUpperBoundsImpl`. Therefore, if changes are made to the structure
 * of the main analysis algorithm then matching changes need to be made
 * here.
 */
private
predicate defDependsOnDef(
  RangeSsaDefinition def, LocalScopeVariable v,
  RangeSsaDefinition srcDef, LocalScopeVariable srcVar
) {
  // Definitions with a defining value.
  exists (Expr expr
  | assignmentDef(def, v, expr)
  | exprDependsOnDef(expr, srcDef, srcVar))
  or
  exists (
    AssignAddExpr assignAdd, RangeSsaDefinition nextDef
  | def = assignAdd and
    assignAdd.getLValue() = nextDef.getAUse(v)
  | defDependsOnDef(nextDef, v, srcDef, srcVar) or
    exprDependsOnDef(assignAdd.getRValue(), srcDef, srcVar))
  or
  exists (
    AssignSubExpr assignSub, RangeSsaDefinition nextDef
  | def = assignSub and
    assignSub.getLValue() = nextDef.getAUse(v)
  | defDependsOnDef(nextDef, v, srcDef, srcVar) or
    exprDependsOnDef(assignSub.getRValue(), srcDef, srcVar))
  or
  exists (CrementOperation crem
  | def = crem and
    crem.getOperand() = v.getAnAccess() and
    exprDependsOnDef(crem.getOperand(), srcDef, srcVar))
  or
  // Phi nodes.
  phiDependsOnDef(def, v, srcDef, srcVar)
}

/**
 * Helper predicate for `defDependsOnDef`. This predicate matches
 * the structure of `getLowerBoundsImpl` and `getUpperBoundsImpl`.
 */
private
predicate exprDependsOnDef(
  Expr e, RangeSsaDefinition srcDef, LocalScopeVariable srcVar
) {
  exists (UnaryMinusExpr negateExpr
  | e = negateExpr
  | exprDependsOnDef(negateExpr.getOperand(), srcDef, srcVar))
  or
  exists (UnaryPlusExpr plusExpr
  | e = plusExpr
  | exprDependsOnDef(plusExpr.getOperand(), srcDef, srcVar))
  or
  exists (MinExpr minExpr
  | e = minExpr
  | exprDependsOnDef(minExpr.getAnOperand(), srcDef, srcVar))
  or
  exists (MaxExpr maxExpr
  | e = maxExpr
  | exprDependsOnDef(maxExpr.getAnOperand(), srcDef, srcVar))
  or
  exists (ConditionalExpr condExpr
  | e = condExpr
  | exprDependsOnDef(condExpr.getAnOperand(), srcDef, srcVar))
  or
  exists (AddExpr addExpr
  | e = addExpr
  | exprDependsOnDef(addExpr.getAnOperand(), srcDef, srcVar))
  or
  exists (SubExpr subExpr
  | e = subExpr
  | exprDependsOnDef(subExpr.getAnOperand(), srcDef, srcVar))
  or
  exists (CrementOperation crementExpr
  | e = crementExpr
  | exprDependsOnDef(crementExpr.getOperand(), srcDef, srcVar))
  or
  exists (RemExpr remExpr
  | e = remExpr
  | exprDependsOnDef(remExpr.getAnOperand(), srcDef, srcVar))
  or
  exists (CommaExpr commaExpr
  | e = commaExpr
  | exprDependsOnDef(commaExpr.getRightOperand(), srcDef, srcVar))
  or
  exists (StmtExpr stmtExpr
  | e = stmtExpr
  | exprDependsOnDef(stmtExpr.getResultExpr(), srcDef, srcVar))
  or
  exists (Conversion convExpr
  | e = convExpr
  | exprDependsOnDef(convExpr.getExpr(), srcDef, srcVar))
  or
  e = srcDef.getAUse(srcVar)
}

/**
 * Helper predicate for `defDependsOnDef`. This predicate matches
 * the structure of `getPhiLowerBounds` and `getPhiUpperBounds`.
 */
private
predicate phiDependsOnDef(
  RangeSsaDefinition phi, LocalScopeVariable v,
  RangeSsaDefinition srcDef, LocalScopeVariable srcVar
) {
  exists (VariableAccess access, ComparisonOperation guard
  | access = v.getAnAccess() and
    phi.isGuardPhi(access, guard, _)
  | exprDependsOnDef(guard.getAnOperand(), srcDef, srcVar) or
    exprDependsOnDef(access, srcDef, srcVar))
  or
  (srcDef = phi.getAPhiInput(v) and srcVar = v)
}

/** The transitive closure of `defDependsOnDef`. */
private
predicate defDependsOnDefTransitively(
  RangeSsaDefinition def, LocalScopeVariable v,
  RangeSsaDefinition srcDef, LocalScopeVariable srcVar
) {
  defDependsOnDef(def, v, srcDef, srcVar) or
  exists (RangeSsaDefinition midDef, LocalScopeVariable midVar
  | defDependsOnDef(def, v, midDef, midVar)
  | defDependsOnDefTransitively(midDef, midVar, srcDef, srcVar))
}

/** The set of definitions that depend recursively on themselves. */
private
predicate isRecursiveDef(RangeSsaDefinition def, LocalScopeVariable v) {
  defDependsOnDefTransitively(def, v, def, v)
}

/**
 * We distinguish 3 kinds of RangeSsaDefinition:
 *
 * 1. Definitions with a defining value.
 *    For example: x = y+3 is a definition of x with defining value y+3.
 *
 * 2. Phi nodes: x3 = phi(x0,x1,x2)
 *
 * 3. Unanalyzable definitions.
 *    For example: a parameter is unanalyzable because we know nothing
 *    about its value.
 *
 * This predicate finds all the definitions in the first set.
 */
private
predicate assignmentDef(RangeSsaDefinition def, LocalScopeVariable v, Expr expr) {
  v.getType().getUnspecifiedType() instanceof ArithmeticType
  and
  ((def = v.getInitializer().getExpr() and def = expr)
   or
   exists(AssignExpr assign
   | def = assign and
     assign.getLValue() = v.getAnAccess() and
     expr = assign.getRValue()))
}

/** See comment above sourceDef. */
private
predicate analyzableDef(RangeSsaDefinition def, LocalScopeVariable v) {
  assignmentDef(def, v, _) or defDependsOnDef(def, v, _, _)
}

/**
 * Computes a normal form of `x` where -0.0 has changed to +0.0. This can be
 * needed on the lesser side of a floating-point comparison or on both sides of
 * a floating point equality because QL does not follow IEEE in floating-point
 * comparisons but instead defines -0.0 to be less than and distinct from 0.0.
 */
bindingset[x]
private float normalizeFloatUp(float x) {
  result = x + 0.0
}

/**
 * Computes `x + y`, rounded towards +Inf. This is the general case where both
 * `x` and `y` may be large numbers.
 */
bindingset[x, y]
private float addRoundingUp(float x, float y) {
  if normalizeFloatUp((x + y) - x) < y or normalizeFloatUp((x + y) - y) < x
  then result = (x + y).nextUp()
  else result = (x + y)
}

/**
 * Computes `x + y`, rounded towards -Inf. This is the general case where both
 * `x` and `y` may be large numbers.
 */
bindingset[x, y]
private float addRoundingDown(float x, float y) {
  if (x + y) - x > normalizeFloatUp(y) or (x + y) - y > normalizeFloatUp(x)
  then result = (x + y).nextDown()
  else result = (x + y)
}

/**
 * Computes `x + small`, rounded towards +Inf, where `small` is a small
 * constant.
 */
bindingset[x, small]
private float addRoundingUpSmall(float x, float small) {
  if (x + small) - x < small
  then result = (x + small).nextUp()
  else result = (x + small)
}

/**
 * Computes `x + small`, rounded towards -Inf, where `small` is a small
 * constant.
 */
bindingset[x, small]
private float addRoundingDownSmall(float x, float small) {
  if (x + small) - x > small
  then result = (x + small).nextDown()
  else result = (x + small)
}

/**
 * Gets the truncated lower bounds of the fully converted expression.
 */
private
float getFullyConvertedLowerBounds(Expr expr) {
  result = getTruncatedLowerBounds(expr.getFullyConverted())
}

/**
 * Gets the lower bounds of the expression.
 *
 * Most of the work of computing the lower bounds is done by
 * `getLowerBoundsImpl`. However, the lower bounds computed by
 * `getLowerBoundsImpl` may not be representable by the result type of the
 * expression. For example, if `x` and `y` are of type `int32` and each
 * have lower bound -2147483648, then getLowerBoundsImpl` will compute a
 * lower bound -4294967296 for the expression `x+y`, even though
 * -4294967296 cannot be represented as an `int32`. Such unrepresentable
 * bounds are replaced with `exprMinVal(expr)`. This predicate also adds
 * `exprMinVal(expr)` as a lower bound if the expression might overflow
 * positively, or if it is unanalyzable.
 *
 * Note: most callers should use `getFullyConvertedLowerBounds` rather than
 * this predicate.
 */
private
float getTruncatedLowerBounds(Expr expr) {
  if analyzableExpr(expr)
     then // If the expression evaluates to a constant, then there is no
          // need to call getLowerBoundsImpl.
          if exists(expr.getValue().toFloat())
             then result = expr.getValue().toFloat()
             else (// Some of the bounds computed by getLowerBoundsImpl might
                   // overflow, so we replace invalid bounds with exprMinVal.
                   exists (float newLB
                   | newLB = getLowerBoundsImpl(expr)
                   | if exprMinVal(expr) <= newLB and newLB <= exprMaxVal(expr)
                        then result = newLB
                        else result = exprMinVal(expr))
                   or
                   // The expression might overflow and wrap. If so, the
                   // lower bound is exprMinVal.
                   (exprMightOverflowPositively(expr) and
                    result = exprMinVal(expr)))
     else // The expression is not analyzable, so its lower bound is
          // unknown. Note that the call to exprMinVal restricts the
          // expressions to just those with arithmetic types. There is no
          // need to return results for non-arithmetic expressions.
          result = exprMinVal(expr)
}

/**
 * Gets the truncated upper bounds of the fully converted expression.
 */
private
float getFullyConvertedUpperBounds(Expr expr) {
  result = getTruncatedUpperBounds(expr.getFullyConverted())
}

/**
 * Gets the upper bounds of the expression.
 *
 * Most of the work of computing the upper bounds is done by
 * `getUpperBoundsImpl`. However, the upper bounds computed by
 * `getUpperBoundsImpl` may not be representable by the result type of the
 * expression. For example, if `x` and `y` are of type `int32` and each
 * have upper bound 2147483647, then getUpperBoundsImpl` will compute an
 * upper bound 4294967294 for the expression `x+y`, even though 4294967294
 * cannot be represented as an `int32`. Such unrepresentable bounds are
 * replaced with `exprMaxVal(expr)`.  This predicate also adds
 * `exprMaxVal(expr)` as an upper bound if the expression might overflow
 * negatively, or if it is unanalyzable.
 *
 * Note: most callers should use `getFullyConvertedUpperBounds` rather than
 * this predicate.
 */
private
float getTruncatedUpperBounds(Expr expr) {
  if analyzableExpr(expr)
     then // If the expression evaluates to a constant, then there is no
          // need to call getUpperBoundsImpl.
          if exists(expr.getValue().toFloat())
             then result = expr.getValue().toFloat()
             else (// Some of the bounds computed by `getUpperBoundsImpl`
                   // might overflow, so we replace invalid bounds with
                   // `exprMaxVal`.
                   exists (float newUB
                   | newUB = getUpperBoundsImpl(expr)
                   | if exprMinVal(expr) <= newUB and newUB <= exprMaxVal(expr)
                        then result = newUB
                        else result = exprMaxVal(expr))
                   or
                   // The expression might overflow negatively and wrap. If so,
                   // the upper bound is `exprMaxVal`.
                   (exprMightOverflowNegatively(expr) and
                    result = exprMaxVal(expr)))
     else // The expression is not analyzable, so its upper bound is
          // unknown. Note that the call to exprMaxVal restricts the
          // expressions to just those with arithmetic types. There is no
          // need to return results for non-arithmetic expressions.
          result = exprMaxVal(expr)
}

/**
 * Holds if the expression might overflow negatively. This predicate
 * does not consider the possibility that the expression might overflow
 * due to a conversion.
 *
 * DEPRECATED: use `exprMightOverflowNegatively` instead.
 */
deprecated predicate negative_overflow(Expr expr) {
  exprMightOverflowNegatively(expr)
}


/**
 * Holds if the expression might overflow positively. This predicate
 * does not consider the possibility that the expression might overflow
 * due to a conversion.
 *
 * DEPRECATED: use `exprMightOverflowPositively` instead.
 */
deprecated predicate positive_overflow(Expr expr) {
  exprMightOverflowPositively(expr)
}

/** Only to be called by `getTruncatedLowerBounds`. */
private
float getLowerBoundsImpl(Expr expr) {
  exists (UnaryPlusExpr plusExpr
  | expr = plusExpr and
    result = getFullyConvertedLowerBounds(plusExpr.getOperand()) )
  or
  exists (UnaryMinusExpr negateExpr, float xHigh
  | expr = negateExpr and
    xHigh = getFullyConvertedUpperBounds(negateExpr.getOperand()) and
    result = -xHigh)
  or
  exists (MinExpr minExpr
  | expr = minExpr and
    // Return the union of the lower bounds from both children.
    result = getFullyConvertedLowerBounds(minExpr.getAnOperand()))
  or
  exists (MaxExpr maxExpr
  | expr = maxExpr and
    // Compute the cross product of the bounds from both children.  We are
    // using this mathematical property:
    //
    //    max (minimum{X}, minimum{Y})
    //  = minimum { max(x,y) | x in X, y in Y }
    exists (float x, float y
    | x = getFullyConvertedLowerBounds(maxExpr.getLeftOperand()) and
      y = getFullyConvertedLowerBounds(maxExpr.getRightOperand()) and
      if x >= y
        then result = x
        else result = y))
  or
  // ConditionalExpr (true branch)
  exists (ConditionalExpr condExpr
  | expr = condExpr and
    // Use `boolConversionUpperBound` to determine whether the condition
    // might evaluate to `true`.
    boolConversionUpperBound(condExpr.getCondition().getFullyConverted()) = 1 and
    result = getFullyConvertedLowerBounds(condExpr.getThen()))
  or
  // ConditionalExpr (false branch)
  exists (ConditionalExpr condExpr
  | expr = condExpr and
    // Use `boolConversionLowerBound` to determine whether the condition
    // might evaluate to `false`.
    boolConversionLowerBound(condExpr.getCondition().getFullyConverted()) = 0 and
    result = getFullyConvertedLowerBounds(condExpr.getElse()))
  or
  exists (AddExpr addExpr, float xLow, float yLow
  | expr = addExpr and
    xLow = getFullyConvertedLowerBounds(addExpr.getLeftOperand()) and
    yLow = getFullyConvertedLowerBounds(addExpr.getRightOperand()) and
    result = addRoundingDown(xLow, yLow))
  or
  exists (SubExpr subExpr, float xLow, float yHigh
  | expr = subExpr and
    xLow = getFullyConvertedLowerBounds(subExpr.getLeftOperand()) and
    yHigh = getFullyConvertedUpperBounds(subExpr.getRightOperand()) and
    result = addRoundingDown(xLow, -yHigh))
  or
  exists (PrefixIncrExpr incrExpr, float xLow
  | expr = incrExpr and
    xLow = getFullyConvertedLowerBounds(incrExpr.getOperand()) and
    result = xLow+1)
  or
  exists (PrefixDecrExpr decrExpr, float xLow
  | expr = decrExpr and
    xLow = getFullyConvertedLowerBounds(decrExpr.getOperand()) and
    result = addRoundingDownSmall(xLow, -1))
  or
  // `PostfixIncrExpr` and `PostfixDecrExpr` return the value of their
  // operand. The incrementing/decrementing behavior is handled in
  // `getDefLowerBoundsImpl`.
  exists (PostfixIncrExpr incrExpr
  | expr = incrExpr and
    result = getFullyConvertedLowerBounds(incrExpr.getOperand()))
  or
  exists (PostfixDecrExpr decrExpr
  | expr = decrExpr and
    result = getFullyConvertedLowerBounds(decrExpr.getOperand()))
  or
  exists (RemExpr remExpr
  | expr = remExpr
  | // If both inputs are positive then the lower bound is zero.
    result = 0
    or
    // If either input could be negative then the output could be
    // negative. If so, the lower bound of `x%y` is `-abs(y)`, which is
    // equal to `min(-y,y)`.
    exists(float childLB
    | childLB = getFullyConvertedLowerBounds(remExpr.getAnOperand()) and
      not (childLB >= 0)
    | result = getFullyConvertedLowerBounds(remExpr.getRightOperand())
      or
      exists(float rhsUB
      | rhsUB = getFullyConvertedUpperBounds(remExpr.getRightOperand())
      | result = -rhsUB)))
  or
  exists (CommaExpr commaExpr
  | expr = commaExpr and
    result = getFullyConvertedLowerBounds(commaExpr.getRightOperand()))
  or
  exists (StmtExpr stmtExpr
  | expr = stmtExpr and
    result = getFullyConvertedLowerBounds(stmtExpr.getResultExpr()))
  or
  // If the conversion is to an arithmetic type then we just return the
  // lower bound of the child. We do not need to handle truncation and
  // overflow here, because that is done in `getTruncatedLowerBounds`.
  // Conversions to `bool` need to be handled specially because they test
  // whether the value of the expression is equal to 0.
  exists (Conversion convExpr
  | expr = convExpr
  | if convExpr.getType().getUnspecifiedType() instanceof BoolType
      then result = boolConversionLowerBound(convExpr.getExpr())
      else result = getTruncatedLowerBounds(convExpr.getExpr()))
  or
  // Use SSA to get the lower bounds for a variable use.
  exists (RangeSsaDefinition def, LocalScopeVariable v
  | expr = def.getAUse(v)
  | result = getDefLowerBounds(def, v))
}

/** Only to be called by `getTruncatedUpperBounds`. */
private
float getUpperBoundsImpl(Expr expr) {
  exists (UnaryPlusExpr plusExpr
  | expr = plusExpr and
    result = getFullyConvertedUpperBounds(plusExpr.getOperand()))
  or
  exists (UnaryMinusExpr negateExpr, float xLow
  | expr = negateExpr and
    xLow = getFullyConvertedLowerBounds(negateExpr.getOperand()) and
    result = -xLow)
  or
  exists (MaxExpr maxExpr
  | expr = maxExpr and
    // Return the union of the upper bounds from both children.
    result = getFullyConvertedUpperBounds(maxExpr.getAnOperand()))
  or
  exists (MinExpr minExpr
  | expr = minExpr and
    // Compute the cross product of the bounds from both children.  We are
    // using this mathematical property:
    //
    //    min (maximum{X}, maximum{Y})
    //  = maximum { min(x,y) | x in X, y in Y }
    exists (float x, float y
    | x = getFullyConvertedUpperBounds(minExpr.getLeftOperand()) and
      y = getFullyConvertedUpperBounds(minExpr.getRightOperand()) and
      if x <= y
        then result = x
        else result = y))
  or
  // ConditionalExpr (true branch)
  exists (ConditionalExpr condExpr
  | expr = condExpr and
    // Use `boolConversionUpperBound` to determine whether the condition
    // might evaluate to `true`.
    boolConversionUpperBound(condExpr.getCondition().getFullyConverted()) = 1 and
    result = getFullyConvertedUpperBounds(condExpr.getThen()))
  or
  // ConditionalExpr (false branch)
  exists (ConditionalExpr condExpr
  | expr = condExpr and
    // Use `boolConversionLowerBound` to determine whether the condition
    // might evaluate to `false`.
    boolConversionLowerBound(condExpr.getCondition().getFullyConverted()) = 0 and
    result = getFullyConvertedUpperBounds(condExpr.getElse()))
  or
  exists (AddExpr addExpr, float xHigh, float yHigh
  | expr = addExpr and
    xHigh = getFullyConvertedUpperBounds(addExpr.getLeftOperand()) and
    yHigh = getFullyConvertedUpperBounds(addExpr.getRightOperand()) and
    result = addRoundingUp(xHigh, yHigh))
  or
  exists (SubExpr subExpr, float xHigh, float yLow
  | expr = subExpr and
    xHigh = getFullyConvertedUpperBounds(subExpr.getLeftOperand()) and
    yLow = getFullyConvertedLowerBounds(subExpr.getRightOperand()) and
    result = addRoundingUp(xHigh, -yLow))
  or
  exists (PrefixIncrExpr incrExpr, float xHigh
  | expr = incrExpr and
    xHigh = getFullyConvertedUpperBounds(incrExpr.getOperand()) and
    result = addRoundingUpSmall(xHigh, 1))
  or
  exists (PrefixDecrExpr decrExpr, float xHigh
  | expr = decrExpr and
    xHigh = getFullyConvertedUpperBounds(decrExpr.getOperand()) and
    result = xHigh-1)
  or
  // `PostfixIncrExpr` and `PostfixDecrExpr` return the value of their operand.
  // The incrementing/decrementing behavior is handled in
  // `getDefUpperBoundsImpl`.
  exists (PostfixIncrExpr incrExpr
  | expr = incrExpr and
    result = getFullyConvertedUpperBounds(incrExpr.getOperand()))
  or
  exists (PostfixDecrExpr decrExpr
  | expr = decrExpr and
    result = getFullyConvertedUpperBounds(decrExpr.getOperand()))
  or
  exists (RemExpr remExpr, float rhsUB
  | expr = remExpr and
    rhsUB = getFullyConvertedUpperBounds(remExpr.getRightOperand())
  | result = rhsUB
    or
    // If the right hand side could be negative then we need to take its
    // absolute value. Since `abs(x) = max(-x,x)` this is equivalent to
    // adding `-rhsLB` to the set of upper bounds.
    exists(float rhsLB
    | rhsLB = getFullyConvertedLowerBounds(remExpr.getAnOperand()) and
      not (rhsLB >= 0)
    | result = -rhsLB))
  or
  exists (CommaExpr commaExpr
  | expr = commaExpr and
    result = getFullyConvertedUpperBounds(commaExpr.getRightOperand()))
  or
  exists (StmtExpr stmtExpr
  | expr = stmtExpr and
    result = getFullyConvertedUpperBounds(stmtExpr.getResultExpr()))
  or
  // If the conversion is to an arithmetic type then we just return the
  // upper bound of the child. We do not need to handle truncation and
  // overflow here, because that is done in `getTruncatedUpperBounds`.
  // Conversions to `bool` need to be handled specially because they test
  // whether the value of the expression is equal to 0.
  exists (Conversion convExpr
  | expr = convExpr
  | if convExpr.getType().getUnspecifiedType() instanceof BoolType
      then result = boolConversionUpperBound(convExpr.getExpr())
      else result = getTruncatedUpperBounds(convExpr.getExpr()))
  or
  // Use SSA to get the upper bounds for a variable use.
  exists (RangeSsaDefinition def, LocalScopeVariable v
  | expr = def.getAUse(v)
  | result = getDefUpperBounds(def, v))
}

/**
 * Holds if `expr` is converted to `bool` or if it is the child of a
 * logical operation.
 *
 * The purpose of this predicate is to optimize `boolConversionLowerBound`
 * and `boolConversionUpperBound` by preventing them from computing
 * unnecessary results. In other words, `exprIsUsedAsBool(expr)` holds if
 * `expr` is an expression that might be passed as an argument to
 * `boolConversionLowerBound` or `boolConversionUpperBound`.
 */
private predicate exprIsUsedAsBool(Expr expr) {
  expr = any(BinaryLogicalOperation op).getAnOperand().getFullyConverted() or
  expr = any(UnaryLogicalOperation op).getOperand().getFullyConverted() or
  expr = any(ConditionalExpr c).getCondition().getFullyConverted() or
  exists (Conversion cast
  | cast.getType().getUnspecifiedType() instanceof BoolType
  | expr = cast.getExpr())
}

/**
 * Gets the lower bound of the conversion `(bool)expr`. If we can prove that
 * the value of `expr` is never 0 then `lb = 1`. Otherwise `lb = 0`.
 */
private float boolConversionLowerBound(Expr expr) {
  // Case 1: if the range for `expr` includes the value 0,
  // then `result = 0`.
  (exprIsUsedAsBool(expr) and
   exists (float lb | lb = getTruncatedLowerBounds(expr) and not (lb > 0)) and
   exists (float ub | ub = getTruncatedUpperBounds(expr) and not (ub < 0)) and
   result = 0)
  or
  // Case 2a: if the range for `expr` does not include the value 0,
  // then `result = 1`.
  (exprIsUsedAsBool(expr) and getTruncatedLowerBounds(expr) > 0 and result = 1)
  or
  // Case 2b: if the range for `expr` does not include the value 0,
  // then `result = 1`.
  (exprIsUsedAsBool(expr) and getTruncatedUpperBounds(expr) < 0 and result = 1)
  or
  // Case 3: the type of `expr` is not arithmetic. For example, it might
  // be a pointer.
  (exprIsUsedAsBool(expr) and not exists(exprMinVal(expr)) and result = 0)
}

/**
 * Gets the upper bound of the conversion `(bool)expr`. If we can prove that
 * the value of `expr` is always 0 then `ub = 0`. Otherwise `ub = 1`.
 */
private float boolConversionUpperBound(Expr expr) {
  // Case 1a: if the upper bound of the operand is <= 0, then the upper
  // bound might be 0.
  (exprIsUsedAsBool(expr) and getTruncatedUpperBounds(expr) <= 0 and result = 0)
  or
  // Case 1b: if the upper bound of the operand is not <= 0, then the upper
  // bound is 1.
  (exprIsUsedAsBool(expr) and
   exists (float ub | ub = getTruncatedUpperBounds(expr) and not (ub <= 0)) and
   result = 1)
  or
  // Case 2a: if the lower bound of the operand is >= 0, then the upper
  // bound might be 0.
  (exprIsUsedAsBool(expr) and getTruncatedLowerBounds(expr) >= 0 and result = 0)
  or
  // Case 2b: if the lower bound of the operand is not >= 0, then the upper
  // bound is 1.
  (exprIsUsedAsBool(expr) and
   exists (float lb | lb = getTruncatedLowerBounds(expr) and not (lb >= 0)) and
   result = 1)
  or
  // Case 3: the type of `expr` is not arithmetic. For example, it might
  // be a pointer.
  (exprIsUsedAsBool(expr) and not exists(exprMaxVal(expr)) and result = 1)
}

/**
 * This predicate computes the lower bounds of a phi definition. If the
 * phi definition corresponds to a guard, then the guard is used to
 * deduce a better lower bound.
 * For example:
 *
 *     def:      x = y % 10;
 *     guard:    if (x >= 2) {
 *     block:      f(x)
 *               }
 *
 * In this example, the lower bound of x is 0, but we can
 * use the guard to deduce that the lower bound is 2 inside the block.
 */
private
float getPhiLowerBounds(LocalScopeVariable v, RangeSsaDefinition phi) {
  exists (
    VariableAccess access, ComparisonOperation guard, boolean branch,
    float defLB, float guardLB
  | access = v.getAnAccess() and
    phi.isGuardPhi(access, guard, branch) and
    lowerBoundFromGuard(guard, access, guardLB, branch) and
    defLB = getFullyConvertedLowerBounds(access)
  | // Compute the maximum of `guardLB` and `defLB`.
    if guardLB > defLB
       then result = guardLB
       else result = defLB)
  or
  result = getDefLowerBounds(phi.getAPhiInput(v), v)
}

/** See comment for `getPhiLowerBounds`, above. */
private
float getPhiUpperBounds(LocalScopeVariable v, RangeSsaDefinition phi) {
  exists (
    VariableAccess access, ComparisonOperation guard, boolean branch,
    float defUB, float guardUB
  | access = v.getAnAccess() and
    phi.isGuardPhi(access, guard, branch) and
    upperBoundFromGuard(guard, access, guardUB, branch) and
    defUB = getFullyConvertedUpperBounds(access)
  | // Compute the minimum of `guardUB` and `defUB`.
    if guardUB < defUB
       then result = guardUB
       else result = defUB)
  or
  result = getDefUpperBounds(phi.getAPhiInput(v), v)
}

/** Only to be called by `getDefLowerBounds`. */
private
float getDefLowerBoundsImpl(RangeSsaDefinition def, LocalScopeVariable v) {
  // Definitions with a defining value.
  exists (Expr expr
  | assignmentDef(def, v, expr)
  | result = getFullyConvertedLowerBounds(expr))
  or
  exists (
    AssignAddExpr assignAdd, RangeSsaDefinition nextDef, float lhsLB, float rhsLB
  | def = assignAdd and
    assignAdd.getLValue() = nextDef.getAUse(v) and
    lhsLB = getDefLowerBounds(nextDef, v) and
    rhsLB = getFullyConvertedLowerBounds(assignAdd.getRValue()) and
    result = addRoundingDown(lhsLB, rhsLB))
  or
  exists (
    AssignSubExpr assignSub, RangeSsaDefinition nextDef, float lhsLB, float rhsUB
  | def = assignSub and
    assignSub.getLValue() = nextDef.getAUse(v) and
    lhsLB = getDefLowerBounds(nextDef, v) and
    rhsUB = getFullyConvertedUpperBounds(assignSub.getRValue()) and
    result = addRoundingDown(lhsLB, -rhsUB))
  or
  exists (IncrementOperation incr, float newLB
  | def = incr and
    incr.getOperand() = v.getAnAccess() and
    newLB = getFullyConvertedLowerBounds(incr.getOperand()) and
    result = newLB+1)
  or
  exists (DecrementOperation decr, float newLB
  | def = decr and
    decr.getOperand() = v.getAnAccess() and
    newLB = getFullyConvertedLowerBounds(decr.getOperand()) and
    result = addRoundingDownSmall(newLB, -1))
  or
  // Phi nodes.
  result = getPhiLowerBounds(v, def)
  or
  // Unanalyzable definitions.
  unanalyzableDefBounds(def, v, result, _)
}

/** Only to be called by `getDefUpperBounds`. */
private
float getDefUpperBoundsImpl(RangeSsaDefinition def, LocalScopeVariable v) {
  // Definitions with a defining value.
  exists (Expr expr
  | assignmentDef(def, v, expr)
  | result = getFullyConvertedUpperBounds(expr))
  or
  exists (
    AssignAddExpr assignAdd, RangeSsaDefinition nextDef, float lhsUB, float rhsUB
  | def = assignAdd and
    assignAdd.getLValue() = nextDef.getAUse(v) and
    lhsUB = getDefUpperBounds(nextDef, v) and
    rhsUB = getFullyConvertedUpperBounds(assignAdd.getRValue()) and
    result = addRoundingUp(lhsUB, rhsUB))
  or
  exists (
    AssignSubExpr assignSub, RangeSsaDefinition nextDef, float lhsUB, float rhsLB
  | def = assignSub and
    assignSub.getLValue() = nextDef.getAUse(v) and
    lhsUB = getDefUpperBounds(nextDef, v) and
    rhsLB = getFullyConvertedLowerBounds(assignSub.getRValue()) and
    result = addRoundingUp(lhsUB, -rhsLB))
  or
  exists (IncrementOperation incr, float newUB
  | def = incr and
    incr.getOperand() = v.getAnAccess() and
    newUB = getFullyConvertedUpperBounds(incr.getOperand()) and
    result = addRoundingUpSmall(newUB, 1))
  or
  exists (DecrementOperation decr, float newUB
  | def = decr and
    decr.getOperand() = v.getAnAccess() and
    newUB = getFullyConvertedUpperBounds(decr.getOperand()) and
    result = newUB-1)
  or
  // Phi nodes.
  result = getPhiUpperBounds(v, def)
  or
  // Unanalyzable definitions.
  unanalyzableDefBounds(def, v, _, result)
}

/**
 * Get the lower bounds for a `RangeSsaDefinition`. Most of the work is
 * done by `getDefLowerBoundsImpl`, but this is where widening is applied
 * to prevent the analysis from exploding due to a recursive definition.
 */
private
float getDefLowerBounds(RangeSsaDefinition def, LocalScopeVariable v) {
  exists (float newLB, float truncatedLB
  | newLB = getDefLowerBoundsImpl(def, v) and
    if varMinVal(v) <= newLB and newLB <= varMaxVal(v)
      then truncatedLB = newLB
      else truncatedLB = varMinVal(v)
  | // Widening: check whether the new lower bound is from a source which
    // depends recursively on the current definition.
    if isRecursiveDef(def, v)
      then // The new lower bound is from a recursive source, so we round
           // down to one of a limited set of values to prevent the
           // recursion from exploding.
           result =
             max (float widenLB
             | widenLB = wideningLowerBounds(v.getType().getUnspecifiedType()) and
               not (widenLB > truncatedLB)
             | widenLB)
      else result = truncatedLB)
  or
  // The definition might overflow positively and wrap. If so, the lower
  // bound is `typeLowerBound`.
  (defMightOverflowPositively(def, v) and result = varMinVal(v))
}

/** See comment for `getDefLowerBounds`, above. */
private
float getDefUpperBounds(RangeSsaDefinition def, LocalScopeVariable v) {
  exists (float newUB, float truncatedUB
  | newUB = getDefUpperBoundsImpl(def, v) and
    if varMinVal(v) <= newUB and newUB <= varMaxVal(v)
      then truncatedUB = newUB
      else truncatedUB = varMaxVal(v)
  | // Widening: check whether the new upper bound is from a source which
    // depends recursively on the current definition.
    if isRecursiveDef(def, v)
      then // The new upper bound is from a recursive source, so we round
           // up to one of a fixed set of values to prevent the recursion
           // from exploding.
           result =
             min (float widenUB
             | widenUB = wideningUpperBounds(v.getType().getUnspecifiedType()) and
               not (widenUB < truncatedUB)
             | widenUB)
      else result = truncatedUB)
  or
  // The definition might overflow negatively and wrap. If so, the upper
  // bound is `typeUpperBound`.
  (defMightOverflowNegatively(def, v) and result = varMaxVal(v))
}

/**
 * Helper for `getDefLowerBounds` and `getDefUpperBounds`. Find the set of
 * unanalyzable definitions (such as function parameters) and make their
 * bounds unknown.
 */
private
predicate unanalyzableDefBounds(
  RangeSsaDefinition def, LocalScopeVariable v, float lb, float ub) {
  v = def.getAVariable() and
  not analyzableDef(def, v) and
  lb = varMinVal(v) and
  ub = varMaxVal(v)
}

/**
 * If the guard is a comparison of the form `p*v + q <CMP> r`, then this
 * predicate uses the bounds information for `r` to compute a lower bound
 * for `v`.
 */
private
predicate lowerBoundFromGuard(
  ComparisonOperation guard, VariableAccess v, float lb, boolean branch
) {
  exists (float childLB, RelationStrictness strictness
  | boundFromGuard(guard, v, childLB, true, strictness, branch)
  | if (strictness = Nonstrict() or
        not (v.getType().getUnspecifiedType() instanceof IntegralType))
      then lb = childLB
      else lb = childLB+1)
}

/**
 * If the guard is a comparison of the form `p*v + q <CMP> r`, then this
 * predicate uses the bounds information for `r` to compute a upper bound
 * for `v`.
 */
private
predicate upperBoundFromGuard(
  ComparisonOperation guard, VariableAccess v, float ub, boolean branch
) {
  exists (float childUB, RelationStrictness strictness
  | boundFromGuard(guard, v, childUB, false, strictness, branch)
  | if (strictness = Nonstrict() or
        not (v.getType().getUnspecifiedType() instanceof IntegralType))
      then ub = childUB
      else ub = childUB-1)
}

/**
 * This predicate simplifies the results returned by
 * `linearBoundFromGuard`.
 */
private
predicate boundFromGuard(
  ComparisonOperation guard, VariableAccess v,
  float boundValue,
  boolean isLowerBound, RelationStrictness strictness, boolean branch
) {
  exists (
    float p, float q, float r, boolean isLB
  | linearBoundFromGuard(
      guard, v, p, q, r, isLB, strictness, branch) and
    boundValue = (r - q)/p
  | // If the multiplier is negative then the direction of the comparison
    // needs to be flipped.
    (p > 0 and isLowerBound = isLB) or
    (p < 0 and isLowerBound = isLB.booleanNot()))
}

/**
 * This predicate finds guards of the form `p*v + q < r or p*v + q == r`
 * and decomposes them into a tuple of values which can be used to deduce a
 * lower or upper bound for `v`.
 */
private
predicate linearBoundFromGuard(
  ComparisonOperation guard, VariableAccess v,
  float p, float q, float boundValue,
  boolean isLowerBound,  // Is this a lower or an upper bound?
  RelationStrictness strictness,
  boolean branch         // Which control-flow branch is this bound valid on?
) {
  // For the comparison x < RHS, we create two bounds:
  //
  //   1. x < upperbound(RHS)
  //   2. x >= typeLowerBound(RHS.getType().getUnspecifiedType())
  //
  exists (Expr lhs, Expr rhs, RelationDirection dir, RelationStrictness st
  | linearAccess(lhs, v, p, q) and
    relOpWithSwapAndNegate(guard, lhs, rhs, dir, st, branch)
  | (isLowerBound = directionIsGreater(dir) and
     strictness = st and
     getBounds(rhs, boundValue, isLowerBound))
    or
    (isLowerBound = directionIsLesser(dir) and
     strictness = Nonstrict() and
     exprTypeBounds(rhs, boundValue, isLowerBound)))

  // For x == RHS, we create the following bounds:
  //
  //   1. x <= upperbound(RHS)
  //   2. x >= lowerbound(RHS)
  //
  // For x != RHS, we create trivial bounds:
  //
  //   1. x <= typeUpperBound(RHS.getType().getUnspecifiedType())
  //   2. x >= typeLowerBound(RHS.getType().getUnspecifiedType())
  //
  or
  exists (Expr lhs, Expr rhs, boolean isEQ
  | linearAccess(lhs, v, p, q) and
    eqOpWithSwapAndNegate(guard, lhs, rhs, isEQ, branch) and
    strictness = Nonstrict()
  | // True branch
    (isEQ = true and getBounds(rhs, boundValue, isLowerBound))
    or
    // False branch: set the bounds to the min/max for the type.
    (isEQ = false and exprTypeBounds(rhs, boundValue, isLowerBound)))
}

/** Utility for `linearBoundFromGuard`. */
private
predicate getBounds(Expr expr, float boundValue, boolean isLowerBound) {
  (isLowerBound = true and boundValue = getFullyConvertedLowerBounds(expr)) or
  (isLowerBound = false and boundValue = getFullyConvertedUpperBounds(expr))
}

/** Utility for `linearBoundFromGuard`. */
private
predicate exprTypeBounds(Expr expr, float boundValue, boolean isLowerBound) {
  (isLowerBound = true and boundValue = exprMinVal(expr.getFullyConverted())) or
  (isLowerBound = false and boundValue = exprMaxVal(expr.getFullyConverted()))
}

private cached module SimpleRangeAnalysisCached {
    /**
   * Gets the lower bound of the expression.
   *
   * Note: expressions in C/C++ are often implicitly or explicitly cast to a
   * different result type. Such casts can cause the value of the expression
   * to overflow or to be truncated. This predicate computes the lower bound
   * of the expression without including the effect of the casts. To compute
   * the lower bound of the expression after all the casts have been applied,
   * call `lowerBound` like this:
   *
   *    `lowerBound(expr.getFullyConverted())`
   */
  cached
  float lowerBound(Expr expr) {
    // Combine the lower bounds returned by getTruncatedLowerBounds into a
    // single minimum value.
    result = min(float lb | lb = getTruncatedLowerBounds(expr) | lb)
  }
  
  /**
   * Gets the upper bound of the expression.
   *
   * Note: expressions in C/C++ are often implicitly or explicitly cast to a
   * different result type. Such casts can cause the value of the expression
   * to overflow or to be truncated. This predicate computes the upper bound
   * of the expression without including the effect of the casts. To compute
   * the upper bound of the expression after all the casts have been applied,
   * call `upperBound` like this:
   *
   *    `upperBound(expr.getFullyConverted())`
   */
  cached
  float upperBound(Expr expr) {
    // Combine the upper bounds returned by getTruncatedUpperBounds into a
    // single maximum value.
    result = max(float ub | ub = getTruncatedUpperBounds(expr) | ub)
  }
  
  /**
   * Holds if `expr` has a provably empty range. For example:
   *
   *   10 < expr and expr < 5
   *
   * The range of an expression can only be empty if it can never be
   * executed. For example:
   *
   *   if (10 < x) {
   *     if (x < 5) {
   *       // Unreachable code
   *       return x; // x has an empty range: 10 < x && x < 5
   *     }
   *   }
   */
  cached
  predicate exprWithEmptyRange(Expr expr) {
    analyzableExpr(expr) and
    (not exists(lowerBound(expr)) or
     not exists(upperBound(expr)) or
     lowerBound(expr) > upperBound(expr))
  }

  /** Holds if the definition might overflow negatively. */
  cached
  predicate defMightOverflowNegatively(RangeSsaDefinition def, LocalScopeVariable v) {
    getDefLowerBoundsImpl(def, v) < varMinVal(v)
  }
  
  /** Holds if the definition might overflow positively. */
  cached
  predicate defMightOverflowPositively(RangeSsaDefinition def, LocalScopeVariable v) {
    getDefUpperBoundsImpl(def, v) > varMaxVal(v)
  }
  
  /**
   * Holds if the definition might overflow (either positively or
   * negatively).
   */
  cached
  predicate defMightOverflow(RangeSsaDefinition def, LocalScopeVariable v) {
    defMightOverflowNegatively(def, v) or
    defMightOverflowPositively(def, v)
  }
  
  /**
   * Holds if the expression might overflow negatively. This predicate
   * does not consider the possibility that the expression might overflow
   * due to a conversion.
   */
  cached
  predicate exprMightOverflowNegatively(Expr expr) {
    getLowerBoundsImpl(expr) < exprMinVal(expr)
  }
  
  /**
   * Holds if the expression might overflow negatively. Conversions
   * are also taken into account. For example the expression
   * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
   * due to the addition.
   */
  cached
  predicate convertedExprMightOverflowNegatively(Expr expr) {
    exprMightOverflowNegatively(expr) or
    convertedExprMightOverflowNegatively(expr.getConversion())
  }
  
    /**
   * Holds if the expression might overflow positively. This predicate
   * does not consider the possibility that the expression might overflow
   * due to a conversion.
   */
  cached
  predicate exprMightOverflowPositively(Expr expr) {
    getUpperBoundsImpl(expr) > exprMaxVal(expr)
  }
  
  /**
   * Holds if the expression might overflow positively. Conversions
   * are also taken into account. For example the expression
   * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
   * due to the addition.
   */
  cached
  predicate convertedExprMightOverflowPositively(Expr expr) {
    exprMightOverflowPositively(expr) or
    convertedExprMightOverflowPositively(expr.getConversion())
  }
  
  /**
   * Holds if the expression might overflow (either positively or
   * negatively). The possibility that the expression might overflow
   * due to an implicit or explicit cast is also considered.
   */
  cached
  predicate convertedExprMightOverflow(Expr expr) {
    convertedExprMightOverflowNegatively(expr) or
    convertedExprMightOverflowPositively(expr)
  }
}
