+
+
+If a condition always evaluates to true or always evaluates to false, this often indicates
+incomplete code or a latent bug, and it should be examined carefully.
+
+
+
+
+
+
+Examine the surrounding code to determine why the condition is redundant. If it is no
+longer needed, remove it.
+
+
+
+If the check is needed to guard against NaN values, insert a comment explaning the possibility of NaN.
+
+
+
+
+
+
+The following example finds the index of an element in a given slice of the array:
+
+
+
+
+
+The condition i < end at the end is always false, however. The code can be clarified if the
+redundant condition is removed:
+
+
+
+
+
+
+
+
+Mozilla Developer Network: Truthy,
+Falsy.
+
+
+
diff --git a/javascript/ql/src/Statements/UselessComparisonTest.ql b/javascript/ql/src/Statements/UselessComparisonTest.ql
new file mode 100644
index 000000000000..419f02a000c3
--- /dev/null
+++ b/javascript/ql/src/Statements/UselessComparisonTest.ql
@@ -0,0 +1,60 @@
+/**
+ * @name Useless comparison test
+ * @description A comparison that always evaluates to true or always evaluates to false may
+ * indicate faulty logic and dead code.
+ * @kind problem
+ * @problem.severity warning
+ * @id js/useless-comparison-test
+ * @tags correctness
+ * @precision high
+ */
+
+import javascript
+
+/**
+ * Holds if there are any contradictory guard nodes in `container`.
+ *
+ * We use this to restrict reachability analysis to a small set of containers.
+ */
+predicate hasContradictoryGuardNodes(StmtContainer container) {
+ exists (ConditionGuardNode guard |
+ RangeAnalysis::isContradictoryGuardNode(guard) and
+ container = guard.getContainer())
+}
+
+/**
+ * Holds if `block` is reachable and is in a container with contradictory guard nodes.
+ */
+predicate isReachable(BasicBlock block) {
+ exists (StmtContainer container |
+ hasContradictoryGuardNodes(container) and
+ block = container.getEntryBB())
+ or
+ isReachable(block.getAPredecessor()) and
+ not RangeAnalysis::isContradictoryGuardNode(block.getANode())
+}
+
+/**
+ * Holds if `block` is unreachable, but could be reached if `guard` was not contradictory.
+ */
+predicate isBlockedByContradictoryGuardNodes(BasicBlock block, ConditionGuardNode guard) {
+ RangeAnalysis::isContradictoryGuardNode(guard) and
+ isReachable(block.getAPredecessor()) and // the guard itself is reachable
+ block = guard.getBasicBlock()
+ or
+ isBlockedByContradictoryGuardNodes(block.getAPredecessor(), guard) and
+ not isReachable(block)
+}
+
+/**
+ * Holds if the given guard node is contradictory and causes an expression or statement to be unreachable.
+ */
+predicate isGuardNodeWithDeadCode(ConditionGuardNode guard) {
+ exists (BasicBlock block |
+ isBlockedByContradictoryGuardNodes(block, guard) and
+ block.getANode() instanceof ExprOrStmt)
+}
+
+from ConditionGuardNode guard
+where isGuardNodeWithDeadCode(guard)
+select guard.getTest(), "The condition '" + guard.getTest() + "' is always " + guard.getOutcome().booleanNot() + "."
diff --git a/javascript/ql/src/Statements/examples/UselessComparisonTest.js b/javascript/ql/src/Statements/examples/UselessComparisonTest.js
new file mode 100644
index 000000000000..53496ce2e4ef
--- /dev/null
+++ b/javascript/ql/src/Statements/examples/UselessComparisonTest.js
@@ -0,0 +1,12 @@
+function findValue(values, x, start, end) {
+ let i;
+ for (i = start; i < end; ++i) {
+ if (values[i] === x) {
+ return i;
+ }
+ }
+ if (i < end) {
+ return i;
+ }
+ return -1;
+}
diff --git a/javascript/ql/src/Statements/examples/UselessComparisonTestGood.js b/javascript/ql/src/Statements/examples/UselessComparisonTestGood.js
new file mode 100644
index 000000000000..6f86622c99b6
--- /dev/null
+++ b/javascript/ql/src/Statements/examples/UselessComparisonTestGood.js
@@ -0,0 +1,8 @@
+function findValue(values, x, start, end) {
+ for (let i = start; i < end; ++i) {
+ if (values[i] === x) {
+ return i;
+ }
+ }
+ return -1;
+}
diff --git a/javascript/ql/src/javascript.qll b/javascript/ql/src/javascript.qll
index 030bc3ce33d3..4202d86ce1ea 100644
--- a/javascript/ql/src/javascript.qll
+++ b/javascript/ql/src/javascript.qll
@@ -36,6 +36,7 @@ import semmle.javascript.NPM
import semmle.javascript.Paths
import semmle.javascript.Promises
import semmle.javascript.CanonicalNames
+import semmle.javascript.RangeAnalysis
import semmle.javascript.Regexp
import semmle.javascript.SSA
import semmle.javascript.StandardLibrary
diff --git a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll
new file mode 100644
index 000000000000..28ccbf2d0caa
--- /dev/null
+++ b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll
@@ -0,0 +1,631 @@
+import javascript
+
+/*
+ * The range analysis is based on Difference Bound constraints, that is, inequalities of form:
+ *
+ * a - b <= c
+ *
+ * or equivalently,
+ *
+ * a <= b + c
+ *
+ * where a and b are variables in the constraint system, and c is an integer constant.
+ *
+ * Such constraints obey a transitive law. Given two constraints,
+ *
+ * a - x <= c1
+ * x - b <= c2
+ *
+ * adding the two inequalities yields the obvious transitive conclusion:
+ *
+ * a - b <= c1 + c2
+ *
+ * We view the system of constraints as a weighted graph, where `a - b <= c`
+ * corresponds to the edge `a -> b` with weight `c`.
+ *
+ * Paths in this graph corresponds to the additional inequalities we can derive from the constraint set.
+ * A negative-weight cycle represents a contradiction, such as `a <= a - 1`.
+ *
+ *
+ * CONTROL FLOW:
+ *
+ * Each constraint is associated with a CFG node where that constraint is known to be valid.
+ * The constraint is only valid within the dominator subtree of that node.
+ *
+ * The transitive rule additionally requires that, in order to compose two edges, one of
+ * their CFG nodes must dominate the other, and the resulting edge becomes associated with the
+ * dominated CFG node (i.e. the most restrictive scope). This ensures constraints
+ * cannot be taken out of context.
+ *
+ * If a negative-weight cycle can be constructed from the edges "in scope" at a given CFG node
+ * (i.e. associated with a dominator of the node), that node is unreachable.
+ *
+ *
+ * DUAL CONSTRAINTS:
+ *
+ * For every data flow node `a` we have two constraint variables, `+a` and `-a` (or just `a` and `-a`)
+ * representing the numerical value of `a` and its negation. Negations let us reason about the sum of
+ * two variables. For example:
+ *
+ * a + b <= 10 becomes a - (-b) <= 10
+ *
+ * It also lets us reason about the upper and lower bounds of a single variable:
+ *
+ * a <= 10 becomes a + a <= 20 becomes a - (-a) <= 20
+ * a >= 10 becomes -a <= -10 becomes (-a) - a <= -20
+ *
+ * For the graph analogy to include the relationship between `a` and `-a`, all constraints
+ * imply their dual constraint:
+ *
+ * a - b <= c implies (-b) - (-a) <= c
+ *
+ * That is, for every edge from a -> b, there is an edge with the same weight from (-b) -> (-a).
+ *
+ *
+ * PATH FINDING:
+ *
+ * See `extendedEdge` predicate for details about how we find negative-weight paths in the graph.
+ *
+ *
+ * CAVEATS:
+ *
+ * - We assume !(x <= y) means x > y, ignoring NaN, unless a nearby comment or identifier mentions NaN.
+ *
+ * - We assume integer arithmetic is exact, ignoring values above 2^53.
+ *
+ */
+
+/**
+ * Contains predicates for reasoning about the relative numeric value of expressions.
+ */
+module RangeAnalysis {
+ /**
+ * Holds if the given node is relevant for range analysis.
+ */
+ private predicate isRelevant(DataFlow::Node node) {
+ node = any(Comparison cmp).getAnOperand().flow()
+ or
+ node = any(ConditionGuardNode guard).getTest().flow()
+ or
+ exists (DataFlow::Node succ | isRelevant(succ) |
+ succ = node.getASuccessor()
+ or
+ linearDefinitionStep(succ, node, _, _)
+ or
+ exists (BinaryExpr bin | bin instanceof AddExpr or bin instanceof SubExpr |
+ succ.asExpr() = bin and
+ bin.getAnOperand().flow() = node))
+ }
+
+ /**
+ * Holds if the given node has a unique data flow predecessor.
+ */
+ pragma[noinline]
+ private predicate hasUniquePredecessor(DataFlow::Node node) {
+ isRelevant(node) and
+ strictcount(node.getAPredecessor()) = 1
+ }
+
+ /**
+ * Gets the definition of `node`, without unfolding phi nodes.
+ */
+ DataFlow::Node getDefinition(DataFlow::Node node) {
+ if hasUniquePredecessor(node) then
+ result = getDefinition(node.getAPredecessor())
+ else
+ result = node
+ }
+
+ /**
+ * Gets a data flow node holding the result of the add/subtract operation in
+ * the given increment/decrement expression.
+ */
+ private DataFlow::Node updateExprResult(UpdateExpr expr) {
+ exists (SsaExplicitDefinition def | def.getDef() = expr |
+ result = DataFlow::ssaDefinitionNode(def))
+ or
+ expr.isPrefix() and
+ result = expr.flow()
+ }
+
+ /**
+ * Gets a data flow node holding the result of the given componund assignment.
+ */
+ private DataFlow::Node compoundAssignResult(CompoundAssignExpr expr) {
+ exists (SsaExplicitDefinition def | def.getDef() = expr |
+ result = DataFlow::ssaDefinitionNode(def))
+ or
+ result = expr.flow()
+ }
+
+ /**
+ * A 30-bit integer.
+ *
+ * Adding two such integers is guaranteed not to overflow. We simply omit constraints
+ * whose parameters would exceed this range.
+ */
+ private class Bias extends int {
+ bindingset[this]
+ Bias() {
+ -536870912 < this and this < 536870912
+ }
+ }
+
+ /**
+ * Holds if `r` can be modelled as `r = root * sign + bias`.
+ *
+ * Only looks "one step", that is, does not follow data flow and does not recursively
+ * unfold nested arithmetic expressions.
+ */
+ private predicate linearDefinitionStep(DataFlow::Node r, DataFlow::Node root, int sign, Bias bias) {
+ not exists(r.asExpr().getIntValue()) and
+ (
+ exists (AddExpr expr | r.asExpr() = expr |
+ // r = root + k
+ root = expr.getLeftOperand().flow() and
+ bias = expr.getRightOperand().getIntValue() and
+ sign = 1
+ or
+ // r = k + root
+ bias = expr.getLeftOperand().getIntValue() and
+ root = expr.getRightOperand().flow() and
+ sign = 1)
+ or
+ exists (SubExpr expr | r.asExpr() = expr |
+ // r = root - k
+ root = expr.getLeftOperand().flow() and
+ bias = -expr.getRightOperand().getIntValue() and
+ sign = 1
+ or
+ // r = k - root
+ bias = expr.getLeftOperand().getIntValue() and
+ root = expr.getRightOperand().flow() and
+ sign = -1)
+ or
+ exists (NegExpr expr | r.asExpr() = expr |
+ // r = -root
+ root = expr.getOperand().flow() and
+ bias = 0 and
+ sign = -1)
+ or
+ exists (UpdateExpr update | r = updateExprResult(update) |
+ // r = ++root
+ root = update.getOperand().flow() and
+ sign = 1 and
+ if update instanceof IncExpr then
+ bias = 1
+ else
+ bias = -1)
+ or
+ exists (UpdateExpr update | r.asExpr() = update | // Return value of x++ is just x (coerced to an int)
+ // r = root++
+ root = update.getOperand().flow() and
+ not update.isPrefix() and
+ sign = 1 and
+ bias = 0)
+ or
+ exists (CompoundAssignExpr assign | r = compoundAssignResult(assign) |
+ root = assign.getLhs().flow() and
+ sign = 1 and
+ (
+ // r = root += k
+ assign instanceof AssignAddExpr and
+ bias = assign.getRhs().getIntValue()
+ or
+ // r = root -= k
+ assign instanceof AssignSubExpr and
+ bias = -assign.getRhs().getIntValue()
+ ))
+ )
+ }
+
+ /**
+ * Holds if `r` can be modelled as `r = root * sign + bias`.
+ */
+ predicate linearDefinition(DataFlow::Node r, DataFlow::Node root, int sign, Bias bias) {
+ if hasUniquePredecessor(r) then
+ linearDefinition(r.getAPredecessor(), root, sign, bias)
+ else if linearDefinitionStep(r, _, _, _) then
+ exists (DataFlow::Node pred, int sign1, int bias1, int sign2, int bias2 |
+ // r = pred * sign1 + bias1
+ linearDefinitionStep(r, pred, sign1, bias1) and
+ // pred = root * sign2 + bias2
+ linearDefinition(pred, root, sign2, bias2) and
+ // r = (root * sign2 + bias2) * sign1 + bias1
+ sign = sign1 * sign2 and
+ bias = bias1 + sign1 * bias2)
+ else (
+ isRelevant(r) and
+ root = r and
+ sign = 1 and
+ bias = 0
+ )
+ }
+
+ /**
+ * Holds if `r` can be modelled as `r = xroot * xsign + yroot * ysign + bias`.
+ */
+ predicate linearDefinitionSum(DataFlow::Node r, DataFlow::Node xroot, int xsign, DataFlow::Node yroot, int ysign, Bias bias) {
+ if hasUniquePredecessor(r) then
+ linearDefinitionSum(r.getAPredecessor(), xroot, xsign, yroot, ysign, bias)
+ else if exists(r.asExpr().getIntValue()) then
+ none() // do not model constants as sums
+ else (
+ exists (AddExpr add, int bias1, int bias2 | r.asExpr() = add |
+ // r = r1 + r2
+ linearDefinition(add.getLeftOperand().flow(), xroot, xsign, bias1) and
+ linearDefinition(add.getRightOperand().flow(), yroot, ysign, bias2) and
+ bias = bias1 + bias2)
+ or
+ exists (SubExpr sub, int bias1, int bias2 | r.asExpr() = sub |
+ // r = r1 - r2
+ linearDefinition(sub.getLeftOperand().flow(), xroot, xsign, bias1) and
+ linearDefinition(sub.getRightOperand().flow(), yroot, -ysign, -bias2) and // Negate right-hand operand
+ bias = bias1 + bias2)
+ or
+ linearDefinitionSum(r.asExpr().(NegExpr).getOperand().flow(), xroot, -xsign, yroot, -ysign, -bias)
+ )
+ }
+
+ /**
+ * Holds if the given comparison can be modelled as `A