From a374540c55d90bbbbb34ff694b63b2a7f5d2b0a5 Mon Sep 17 00:00:00 2001 From: Asger F Date: Wed, 12 Sep 2018 18:37:21 +0100 Subject: [PATCH 01/27] JS: Range analysis library --- javascript/ql/src/javascript.qll | 1 + .../src/semmle/javascript/RangeAnalysis.qll | 366 ++++++++++++++++++ .../RangeAnalysis/DeadBranch.expected | 0 .../library-tests/RangeAnalysis/DeadBranch.ql | 35 ++ .../test/library-tests/RangeAnalysis/plus.js | 28 ++ .../test/library-tests/RangeAnalysis/tst.js | 52 +++ 6 files changed, 482 insertions(+) create mode 100644 javascript/ql/src/semmle/javascript/RangeAnalysis.qll create mode 100644 javascript/ql/test/library-tests/RangeAnalysis/DeadBranch.expected create mode 100644 javascript/ql/test/library-tests/RangeAnalysis/DeadBranch.ql create mode 100644 javascript/ql/test/library-tests/RangeAnalysis/plus.js create mode 100644 javascript/ql/test/library-tests/RangeAnalysis/tst.js 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..c4c8a287bc5a --- /dev/null +++ b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll @@ -0,0 +1,366 @@ +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. + * + * - We assume x < y means x <= y + 1, ignoring floats. + * + * - 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 has a unique data flow predecessor. + */ + pragma[noinline] + private predicate hasUniquePredecessor(DataFlow::Node node) { + 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 + } + + /** + * Holds if `r` can be modelled as `r = root * sign + bias`. + * + * Does not follow data flow edges and is not recursive (that is, `root` may itself be defined linearly). + */ + private predicate linearDefinitionStep(DataFlow::Node r, DataFlow::Node root, int sign, int bias) { + not exists(r.asExpr().getIntValue()) and + ( + exists (AddExpr expr | r.asExpr() = expr | + root = expr.getLeftOperand().flow() and + bias = expr.getRightOperand().getIntValue() and + sign = 1) + or + exists (AddExpr expr | r.asExpr() = expr | + bias = expr.getLeftOperand().getIntValue() and + root = expr.getRightOperand().flow() and + sign = 1) + or + exists (SubExpr expr | r.asExpr() = expr | + root = expr.getLeftOperand().flow() and + bias = -expr.getRightOperand().getIntValue() and + sign = 1) + or + exists (SubExpr expr | r.asExpr() = expr | + bias = expr.getLeftOperand().getIntValue() and + root = expr.getRightOperand().flow() and + sign = -1) + or + exists (NegExpr expr | r.asExpr() = expr | + root = expr.getOperand().flow() and + bias = 0 and + sign = -1) + ) + } + + /** + * Holds if `r` can be modelled as `r = root * sign + bias`. + */ + predicate linearDefinition(DataFlow::Node r, DataFlow::Node root, int sign, int 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 | + linearDefinitionStep(r, pred, sign1, bias1) and + linearDefinition(pred, root, sign2, bias2) and + sign = sign1 * sign2 and + bias = bias1 + sign1 * bias2) + else ( + 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, int 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 | + 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 | + 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 B + bias` where `` is the comparison operator. + */ + predicate linearComparison(Comparison comparison, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int bias) { + exists(Expr left, Expr right, int bias1, int bias2 | left = comparison.getLeftOperand() and right = comparison.getRightOperand() | + // A <= B + c + linearDefinition(left.flow(), a, asign, bias1) and + linearDefinition(right.flow(), b, bsign, bias2) and + bias = bias2 - bias1 + or + // A - B + c1 <= c2 becomes A <= B + (c2 - c1) + linearDefinitionSum(left.flow(), a, asign, b, -bsign, bias1) and + right.getIntValue() = bias2 and + bias = bias2 - bias1 + or + // c1 <= -A + B + c2 becomes A <= B + (c2 - c1) + left.getIntValue() = bias1 and + linearDefinitionSum(right.flow(), a, -asign, b, bsign, bias2) and + bias = bias2 - bias1 + ) + } + + /** + * Holds if `guard` asserts that the outcome of `A B + bias` is true, where `` is a comparison operator. + */ + predicate linearComparisonGuard(ConditionGuardNode guard, DataFlow::Node a, int asign, string operator, DataFlow::Node b, int bsign, int bias) { + exists (Comparison compare | compare = getDefinition(guard.getTest().flow()).asExpr() | + linearComparison(compare, a, asign, b, bsign, bias) and + ( + guard.getOutcome() = true and operator = compare.getOperator() + or + guard.getOutcome() = false and operator = negateOperator(compare.getOperator()) + ) + ) + } + + /** + * Gets the binary operator whose return value is the opposite of `operator` (excluding NaN comparisons). + */ + private string negateOperator(string operator) { + operator = "==" and result = "!=" or + operator = "!=" and result = "==" or + operator = "===" and result = "!==" or + operator = "!==" and result = "===" or + operator = "<" and result = ">=" or + operator = "<=" and result = ">" or + operator = ">" and result = "<=" or + operator = ">=" and result = "<" + } + + /** + * Holds if immediately after `cfg` it becomes known that `A <= B + c`. + * + * These are the initial inputs to the difference bound constraint system. + * + * The dual constraint `-B <= -A + c` is not included in this predicate. + */ + predicate comparisonEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int bias) { + // A <= B + c + linearComparisonGuard(cfg, a, asign, "<=", b, bsign, bias) + or + // A <= B + c iff A < B + c + 1 (assuming A,B are integers) + linearComparisonGuard(cfg, a, asign, "<", b, bsign, bias + 1) + or + // A <= B + c iff B >= A - c + linearComparisonGuard(cfg, b, bsign, ">=", a, asign, -bias) + or + // A <= B + c iff B > A - c - 1 (assuming A,B are integers) + linearComparisonGuard(cfg, b, bsign, ">", a, asign, -bias - 1) + or + exists (string operator | operator = "==" or operator = "===" | + // A == B + c iff A <= B + c and B <= A - c + linearComparisonGuard(cfg, a, asign, operator, b, bsign, bias) + or + linearComparisonGuard(cfg, b, bsign, operator, a, asign, -bias) + ) + } + + /** + * The set of initial edges including those from dual constraints. + */ + private predicate seedEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int c) { + // A <= B + c + comparisonEdge(cfg, a, asign, b, bsign, c) + or + // -B <= -A + c (dual constraint) + comparisonEdge(cfg, b, -bsign, a, -asign, c) + } + + /** + * Applies a restricted transitive rule to the edge set. + * + * In particular, we apply the transitive rule only where a negative edge followed by a non-negative edge. + * For example: + * + * A --(-1)--> B --(+3)--> C + * + * yields: + * + * A --(+2)--> C + * + * In practice, the restriction to edges of different sign prevent the + * quadratic blow-up you would normally get from a transitive closure. + * + * It also prevents the relation from becoming infinite in case + * there are negative-weight cycles, where the transitive weights would + * otherwise diverge towards minus infinity. + * + * Moreover, the rule is enough to guarantee the following property: + * + * A negative-weight path from X to Y exists iff a path of negative-weight edges exists from X to Y. + * + * This means negative-weight cycles (contradictions) can be detected using simple cycle detection. + */ + private predicate extendedEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int c) { + seedEdge(cfg, a, asign, b, bsign, c) + or + exists (DataFlow::Node mid, int midx, ControlFlowNode cfg1, int c1, ControlFlowNode cfg2, int c2 | + extendedEdge(cfg1, a, asign, mid, midx, c1) and + extendedEdge(cfg2, mid, midx, b, bsign, c2) and + c1 < 0 and + c2 >= 0 and + c = c1 + c2 and + // One of the two CFG nodes must dominate the other, and `cfg` must be bound to the dominated one. + ( + // They are in the same basic block + exists (BasicBlock bb, int i, int j | + bb.getNode(i) = cfg1 and + bb.getNode(j) = cfg2 and + if i < j then + cfg = cfg2 + else + cfg = cfg1) + or + // They are in different basic blocks + cfg1.getBasicBlock().(ReachableBasicBlock).strictlyDominates(cfg2.getBasicBlock()) and + cfg = cfg2 + or + cfg2.getBasicBlock().(ReachableBasicBlock).strictlyDominates(cfg1.getBasicBlock()) and + cfg = cfg1 + ) + ) + } + + /** + * Holds if there is a negative-weight edge from src to dst. + */ + private predicate negativeEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign) { + exists (int weight | extendedEdge(cfg, a, asign, b, bsign, weight) | + weight < 0) + } + + /** + * Holds if `src` can reach `dst` using only negative-weight edges. + * + * The initial outgoing edge from `src` must be derived at `cfg`. + */ + pragma[noopt] + private predicate reachableByNegativeEdges(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign) { + negativeEdge(cfg, a, asign, b, bsign) + or + exists(DataFlow::Node mid, int midx, ControlFlowNode midcfg | + reachableByNegativeEdges(cfg, a, asign, mid, midx) and + negativeEdge(midcfg, mid, midx, b, bsign) and + exists (BasicBlock bb, int i, int j | + bb.getNode(i) = midcfg and + bb.getNode(j) = cfg and + i <= j)) + or + // Same as above, but where CFG nodes are in different basic blocks + exists(DataFlow::Node mid, int midx, ControlFlowNode midcfg, BasicBlock midBB, ReachableBasicBlock midRBB, BasicBlock cfgBB | + reachableByNegativeEdges(cfg, a, asign, mid, midx) and + negativeEdge(midcfg, mid, midx, b, bsign) and + midBB = midcfg.getBasicBlock() and + midRBB = midBB.(ReachableBasicBlock) and + cfgBB = cfg.getBasicBlock() and + midRBB.strictlyDominates(cfgBB) + ) + } + + /** + * Holds if the condition asserted at `guard` is contradictory, that is, its condition always has the + * opposite of the expected outcome. + */ + predicate isContradictoryGuardNode(ConditionGuardNode guard) { + exists (DataFlow::Node a, int asign | reachableByNegativeEdges(guard, a, asign, a, asign)) + } +} diff --git a/javascript/ql/test/library-tests/RangeAnalysis/DeadBranch.expected b/javascript/ql/test/library-tests/RangeAnalysis/DeadBranch.expected new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/javascript/ql/test/library-tests/RangeAnalysis/DeadBranch.ql b/javascript/ql/test/library-tests/RangeAnalysis/DeadBranch.ql new file mode 100644 index 000000000000..838e45c77e47 --- /dev/null +++ b/javascript/ql/test/library-tests/RangeAnalysis/DeadBranch.ql @@ -0,0 +1,35 @@ +import javascript + +class AssertionComment extends LineComment { + boolean isOK; + + AssertionComment() { + isOK = true and getText().trim().regexpMatch("OK.*") + or + isOK = false and getText().trim().regexpMatch("NOT OK.*") + } + + ConditionGuardNode getAGuardNode() { + result.getLocation().getStartLine() = this.getLocation().getStartLine() and + result.getFile() = this.getFile() + } + + Expr getTestExpr() { result = getAGuardNode().getTest() } + + string getMessage() { + not exists(getAGuardNode()) and result = "Error: no guard node on this line" + or + isOK = true and + exists (ConditionGuardNode guard | guard = getAGuardNode() | + RangeAnalysis::isContradictoryGuardNode(guard) and + result = "Error: analysis claims " + getTestExpr() + " is always " + guard.getOutcome().booleanNot() + ) + or + isOK = false and + not RangeAnalysis::isContradictoryGuardNode(getAGuardNode()) and + result = "Error: " + getTestExpr() + " is always true or always false" + } +} + +from AssertionComment assertion +select assertion, assertion.getMessage() diff --git a/javascript/ql/test/library-tests/RangeAnalysis/plus.js b/javascript/ql/test/library-tests/RangeAnalysis/plus.js new file mode 100644 index 000000000000..ac430bcba4cd --- /dev/null +++ b/javascript/ql/test/library-tests/RangeAnalysis/plus.js @@ -0,0 +1,28 @@ +function f(x,y) { + if (x + 1 < y) { + if (x < y) {} // NOT OK - always true + if (x + 1 < y) {} // NOT OK - always true + if (x + 1 <= y) {} // NOT OK - always true + if (x > y) {} // NOT OK - always false + if (x >= y) {} // NOT OK - always false + if (x + 1 >= y) {} // NOT OK - always false + if (x + 2 < y) {} // OK + if (x < y - 1) {} // NOT OK - always true + } + if (x < y + 1) { + if (x < y) {} // OK + if (x + 1 < y) {} // OK + if (x - 1 < y) {} // NOT OK - always true + } +} + +function g(x) { + let z = x + 1; + z += 1; + ++z; + z++; + if (z < x + 4) {} // NOT OK - always false + if (z > x + 4) {} // NOT OK - always false + if (z < x + 5) {} // NOT OK - always true + if (z > x + 5) {} // NOT OK - always false +} diff --git a/javascript/ql/test/library-tests/RangeAnalysis/tst.js b/javascript/ql/test/library-tests/RangeAnalysis/tst.js new file mode 100644 index 000000000000..f89086711f6b --- /dev/null +++ b/javascript/ql/test/library-tests/RangeAnalysis/tst.js @@ -0,0 +1,52 @@ +function f(x,y) { + if (x < y) { + if (x < y) {} // NOT OK - always true + if (x <= y) {} // NOT OK - always true + if (x > y) {} // NOT OK - always false + if (x >= y) {} // NOT OK - always false + if (x === y) {} // NOT OK - always false + } else { + if (x < y) {} // NOT OK - always false + if (x <= y) {} // OK - could be equal + if (x > y) {} // OK + if (x >= y) {} // NOT OK - always true + if (x === y) {} // OK + } +} + +function g(x,y) { + if (x <= y) { + if (x < y) {} // OK + if (x <= y) {} // NOT OK - always true + if (x > y) {} // NOT OK - always false + if (x >= y) {} // OK - could be equal + if (x === y) {} // OK + } else { + if (x < y) {} // NOT OK - always false + if (x <= y) {} // NOT OK - always false + if (x > y) {} // NOT OK - always true + if (x >= y) {} // NOT OK - always true + if (x === y) {} // NOT OK - always false + } +} + +function loop(start, end) { + var i; + for (i = start; i < end; i++) { + if (i < end) {} // NOT OK - always true + if (i >= end) {} // NOT OK - always false + } + if (i >= end) {} // NOT OK - always true + if (i < end) {} // NOT OK - always false +} + +function h(x, y) { + if (x - y < 0) { + if (x < y) {} // NOT OK - always true + if (x >= y) {} // NOT OK - always false + } + if (0 < x - y) { // y < x + if (x <= y) {} // NOT OK - always false + if (x > y) {} // NOT OK - always true + } +} From 73cbdee691d895a9949b0f2949bf4e7fe11ac96c Mon Sep 17 00:00:00 2001 From: Asger F Date: Wed, 19 Sep 2018 18:28:18 +0100 Subject: [PATCH 02/27] JS: Compound assignments and update exprs in range analysis --- .../src/semmle/javascript/RangeAnalysis.qll | 44 ++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) diff --git a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll index c4c8a287bc5a..9e1cb9b76623 100644 --- a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll +++ b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll @@ -99,10 +99,33 @@ module RangeAnalysis { 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() + } + /** * Holds if `r` can be modelled as `r = root * sign + bias`. * - * Does not follow data flow edges and is not recursive (that is, `root` may itself be defined linearly). + * 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, int bias) { not exists(r.asExpr().getIntValue()) and @@ -131,6 +154,25 @@ module RangeAnalysis { root = expr.getOperand().flow() and bias = 0 and sign = -1) + or + exists (UpdateExpr update | r = updateExprResult(update) | + root = update.getOperand().flow() and + sign = 1 and + if update instanceof IncExpr then + bias = 1 + else + bias = -1) + or + exists (CompoundAssignExpr assign | r = compoundAssignResult(assign) | + root = assign.getLhs().flow() and + sign = 1 and + ( + assign instanceof AssignAddExpr and + bias = assign.getRhs().getIntValue() + or + assign instanceof AssignSubExpr and + bias = -assign.getRhs().getIntValue() + )) ) } From 09ca6652fb0397289ebe168212d149fcc4c91606 Mon Sep 17 00:00:00 2001 From: Asger F Date: Wed, 19 Sep 2018 18:45:55 +0100 Subject: [PATCH 03/27] JS: Support return value of x++ --- javascript/ql/src/semmle/javascript/RangeAnalysis.qll | 6 ++++++ javascript/ql/test/library-tests/RangeAnalysis/plus.js | 5 +++++ 2 files changed, 11 insertions(+) diff --git a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll index 9e1cb9b76623..1eafe1215a9f 100644 --- a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll +++ b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll @@ -163,6 +163,12 @@ module RangeAnalysis { else bias = -1) or + exists (UpdateExpr update | r.asExpr() = update | // Return value of x++ is just x (coerced to an int) + 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 diff --git a/javascript/ql/test/library-tests/RangeAnalysis/plus.js b/javascript/ql/test/library-tests/RangeAnalysis/plus.js index ac430bcba4cd..3b997a49371f 100644 --- a/javascript/ql/test/library-tests/RangeAnalysis/plus.js +++ b/javascript/ql/test/library-tests/RangeAnalysis/plus.js @@ -26,3 +26,8 @@ function g(x) { if (z < x + 5) {} // NOT OK - always true if (z > x + 5) {} // NOT OK - always false } + +function h(x) { + let y = x++; + if (x > y) {} // NOT OK - always true +} From 064b1099ebf3b6468caa9e59bee54d4077c8979f Mon Sep 17 00:00:00 2001 From: Asger F Date: Thu, 20 Sep 2018 16:47:57 +0100 Subject: [PATCH 04/27] JS: range analysis through phi nodes --- .../src/semmle/javascript/RangeAnalysis.qll | 76 ++++++++++++++++++- .../test/library-tests/RangeAnalysis/loop.js | 40 ++++++++++ 2 files changed, 114 insertions(+), 2 deletions(-) create mode 100644 javascript/ql/test/library-tests/RangeAnalysis/loop.js diff --git a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll index 1eafe1215a9f..c91d2ad0e5aa 100644 --- a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll +++ b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll @@ -302,6 +302,71 @@ module RangeAnalysis { ) } + /** + * Holds if `node` is a phi node with `left` and `right` has the only two inputs. + * + * Note that this predicate is symmetric: when it holds for (left, right) it also holds for (right, left). + */ + predicate binaryPhiNode(DataFlow::Node node, DataFlow::Node left, DataFlow::Node right) { + exists (SsaPhiNode phi | node = DataFlow::ssaDefinitionNode(phi) | + strictcount(phi.getAnInput()) = 2 and + left = DataFlow::ssaDefinitionNode(phi.getAnInput()) and + right = DataFlow::ssaDefinitionNode(phi.getAnInput()) and + left != right) + } + + /** + * Holds if `A <= B + c` can be determined based on a phi node. + */ + predicate phiEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int c) { + exists (DataFlow::Node phi, DataFlow::Node left, DataFlow::Node right | + binaryPhiNode(phi, left, right) and + cfg = phi.getBasicBlock() + | + // Both inputs are defined in terms of the same root: + // phi = PHI(root + bias1, root + bias2) + exists (DataFlow::Node root, int sign, int bias1, int bias2 | + linearDefinition(left, root, sign, bias1) and + linearDefinition(right, root, sign, bias2) and + bias1 < bias2 and + // root + bias1 <= phi <= root + bias2 + ( + // root <= phi - bias1 + a = root and asign = 1 and + b = phi and bsign = 1 and + c = -bias1 + or + // phi <= root + bias2 + a = phi and asign = 1 and + b = root and bsign = 1 and + c = bias2 + ) + ) + or + // One input is defined in terms of the phi node itself: + // phi = PHI(phi + increment, x) + exists (int increment, DataFlow::Node root, int sign, int bias | + linearDefinition(left, phi, 1, increment) and + linearDefinition(right, root, sign, bias) and + ( + // If increment is positive (or zero): + // phi >= right' + bias + increment >= 0 and + a = root and asign = sign and + b = phi and bsign = 1 and + c = -bias + or + // If increment is negative (or zero): + // phi <= right' + bias + increment <= 0 and + a = phi and asign = 1 and + b = root and bsign = sign and + c = bias + ) + ) + ) + } + /** * The set of initial edges including those from dual constraints. */ @@ -309,8 +374,15 @@ module RangeAnalysis { // A <= B + c comparisonEdge(cfg, a, asign, b, bsign, c) or + phiEdge(cfg, a, asign, b, bsign, c) + } + + private predicate seedEdgeWithDual(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int c) { + // A <= B + c + seedEdge(cfg, a, asign, b, bsign, c) + or // -B <= -A + c (dual constraint) - comparisonEdge(cfg, b, -bsign, a, -asign, c) + seedEdge(cfg, b, -bsign, a, -asign, c) } /** @@ -339,7 +411,7 @@ module RangeAnalysis { * This means negative-weight cycles (contradictions) can be detected using simple cycle detection. */ private predicate extendedEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int c) { - seedEdge(cfg, a, asign, b, bsign, c) + seedEdgeWithDual(cfg, a, asign, b, bsign, c) or exists (DataFlow::Node mid, int midx, ControlFlowNode cfg1, int c1, ControlFlowNode cfg2, int c2 | extendedEdge(cfg1, a, asign, mid, midx, c1) and diff --git a/javascript/ql/test/library-tests/RangeAnalysis/loop.js b/javascript/ql/test/library-tests/RangeAnalysis/loop.js new file mode 100644 index 000000000000..57bbe2a0262b --- /dev/null +++ b/javascript/ql/test/library-tests/RangeAnalysis/loop.js @@ -0,0 +1,40 @@ +function increasing(start, end) { + for (var i = start; i < end; ++i) { + if (i >= start) {} // NOT OK - always true + if (i < start) {} // NOT OK - always false + + if (i < end) {} // NOT OK - always true + if (i >= end) {} // NOT OK - always false + + if (i + 1 > start) {} // NOT OK - always true + if (i - 1 < start) {} // OK + } +} + +function decreasing(start, end) { + for (var i = start; i > end; --i) { + if (i <= start) {} // NOT OK - always true + if (i > start) {} // NOT OK - always false + + if (i + 1 > start) {} // OK + if (i - 1 < start) {} // NOT OK - always true + } +} + +function middleIncrement(start, end) { + for (var i = start; i < end;) { + if (i >= start) {} // OK - always true but we don't catch it + if (i < start) {} // OK - always false but we don't catch it + + if (i < end) {} // NOT OK - always true + if (i >= end) {} // NOT OK - always false + + if (something()) { + i += 2; + } + if (i >= start) {} // OK - always true but we don't catch it + if (i < start) {} // OK - always false but we don't catch it + if (i < end) {} // OK + if (i >= end) {} // OK + } +} From 6c53ad80c746b4f4940af5cc124d154c8718a20e Mon Sep 17 00:00:00 2001 From: Asger F Date: Thu, 20 Sep 2018 17:24:13 +0100 Subject: [PATCH 05/27] JS: add constant constraints in range analysis --- .../src/semmle/javascript/RangeAnalysis.qll | 19 +++++++++++++++++++ .../library-tests/RangeAnalysis/constants.js | 8 ++++++++ 2 files changed, 27 insertions(+) create mode 100644 javascript/ql/test/library-tests/RangeAnalysis/constants.js diff --git a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll index c91d2ad0e5aa..6451c62a0cf2 100644 --- a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll +++ b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll @@ -367,6 +367,23 @@ module RangeAnalysis { ) } + /** + * Holds constraints derived from `A = const`. + * + * `A = c` is written to `A + A = 2c` which is then converted to `<=` and `>=`. + * + * A + A <= 2c becomes A <= -A + 2c + * A + A >= 2c becomes -A <= A - 2c + */ + predicate constantEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int c) { + exists (NumberLiteral literal | cfg = literal | + a = literal.flow() and + b = a and + (asign = 1 or asign = -1) and + bsign = -asign and + c = literal.getIntValue() * 2 * asign) + } + /** * The set of initial edges including those from dual constraints. */ @@ -375,6 +392,8 @@ module RangeAnalysis { comparisonEdge(cfg, a, asign, b, bsign, c) or phiEdge(cfg, a, asign, b, bsign, c) + or + constantEdge(cfg, a, asign, b, bsign, c) } private predicate seedEdgeWithDual(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int c) { diff --git a/javascript/ql/test/library-tests/RangeAnalysis/constants.js b/javascript/ql/test/library-tests/RangeAnalysis/constants.js new file mode 100644 index 000000000000..9e1a3b914e3c --- /dev/null +++ b/javascript/ql/test/library-tests/RangeAnalysis/constants.js @@ -0,0 +1,8 @@ +function f() { + if (1 > 0) {} // NOT OK - always true + if (1 - 1 >= 0) {} // NOT OK - always true + let one = 1; + let two = 2; + if (two > one) {} // NOT OK - always true + if (two <= one) {} // NOT OK - always false +} From 9d8d953292b6d93bacd890a649374ad0571db80e Mon Sep 17 00:00:00 2001 From: Asger F Date: Tue, 25 Sep 2018 16:50:29 +0100 Subject: [PATCH 06/27] JS: perform widening when adding operands of very different magnitude --- .../src/semmle/javascript/RangeAnalysis.qll | 24 ++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) diff --git a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll index 6451c62a0cf2..5669dad514ae 100644 --- a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll +++ b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll @@ -404,6 +404,26 @@ module RangeAnalysis { seedEdge(cfg, b, -bsign, a, -asign, c) } + /** + * Adds a negative and positive integer, but only if they are within in the same + * order of magnitude. + */ + bindingset[x, y] + private int wideningAddition(int x, int y) { + x < 0 and + y >= 0 and + ( + x = 0 + or + y = 0 + or + // If non-zero, check that the values are within a factor 16 of each other + x.abs().bitShiftRight(4) < y.abs() and + y.abs().bitShiftRight(4) < x.abs() + ) and + result = x + y + } + /** * Applies a restricted transitive rule to the edge set. * @@ -435,9 +455,7 @@ module RangeAnalysis { exists (DataFlow::Node mid, int midx, ControlFlowNode cfg1, int c1, ControlFlowNode cfg2, int c2 | extendedEdge(cfg1, a, asign, mid, midx, c1) and extendedEdge(cfg2, mid, midx, b, bsign, c2) and - c1 < 0 and - c2 >= 0 and - c = c1 + c2 and + c = wideningAddition(c1, c2) and // One of the two CFG nodes must dominate the other, and `cfg` must be bound to the dominated one. ( // They are in the same basic block From 20aa4e1f6dc434acaf84a81fda043993e7186e72 Mon Sep 17 00:00:00 2001 From: Asger F Date: Fri, 28 Sep 2018 18:20:13 +0100 Subject: [PATCH 07/27] JS: handle sharp inequalities directly --- .../src/semmle/javascript/RangeAnalysis.qll | 60 ++++++++++--------- 1 file changed, 33 insertions(+), 27 deletions(-) diff --git a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll index 5669dad514ae..f8ccfa441593 100644 --- a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll +++ b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll @@ -71,8 +71,6 @@ import javascript * * - We assume !(x <= y) means x > y, ignoring NaN. * - * - We assume x < y means x <= y + 1, ignoring floats. - * * - We assume integer arithmetic is exact, ignoring values above 2^53. * */ @@ -281,19 +279,24 @@ module RangeAnalysis { * * The dual constraint `-B <= -A + c` is not included in this predicate. */ - predicate comparisonEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int bias) { + predicate comparisonEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int bias, boolean sharp) { // A <= B + c - linearComparisonGuard(cfg, a, asign, "<=", b, bsign, bias) + linearComparisonGuard(cfg, a, asign, "<=", b, bsign, bias) and + sharp = false or - // A <= B + c iff A < B + c + 1 (assuming A,B are integers) - linearComparisonGuard(cfg, a, asign, "<", b, bsign, bias + 1) + // A < B + c + linearComparisonGuard(cfg, a, asign, "<", b, bsign, bias) and + sharp = true or // A <= B + c iff B >= A - c - linearComparisonGuard(cfg, b, bsign, ">=", a, asign, -bias) + linearComparisonGuard(cfg, b, bsign, ">=", a, asign, -bias) and + sharp = false or - // A <= B + c iff B > A - c - 1 (assuming A,B are integers) - linearComparisonGuard(cfg, b, bsign, ">", a, asign, -bias - 1) + // A < B + c iff B > A - c + linearComparisonGuard(cfg, b, bsign, ">", a, asign, -bias) and + sharp = true or + sharp = false and exists (string operator | operator = "==" or operator = "===" | // A == B + c iff A <= B + c and B <= A - c linearComparisonGuard(cfg, a, asign, operator, b, bsign, bias) @@ -387,31 +390,31 @@ module RangeAnalysis { /** * The set of initial edges including those from dual constraints. */ - private predicate seedEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int c) { + private predicate seedEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int c, boolean sharp) { // A <= B + c - comparisonEdge(cfg, a, asign, b, bsign, c) + comparisonEdge(cfg, a, asign, b, bsign, c, sharp) or - phiEdge(cfg, a, asign, b, bsign, c) + phiEdge(cfg, a, asign, b, bsign, c) and sharp = false or - constantEdge(cfg, a, asign, b, bsign, c) + constantEdge(cfg, a, asign, b, bsign, c) and sharp = false } - private predicate seedEdgeWithDual(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int c) { + private predicate seedEdgeWithDual(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int c, boolean sharp) { // A <= B + c - seedEdge(cfg, a, asign, b, bsign, c) + seedEdge(cfg, a, asign, b, bsign, c, sharp) or // -B <= -A + c (dual constraint) - seedEdge(cfg, b, -bsign, a, -asign, c) + seedEdge(cfg, b, -bsign, a, -asign, c, sharp) } /** * Adds a negative and positive integer, but only if they are within in the same * order of magnitude. */ - bindingset[x, y] - private int wideningAddition(int x, int y) { - x < 0 and - y >= 0 and + bindingset[x, sharpx, y, sharpy] + private int wideningAddition(int x, boolean sharpx, int y, boolean sharpy) { + (x < 0 or x = 0 and sharpx = true) and + (y > 0 or y = 0 and sharpy = false) and ( x = 0 or @@ -449,13 +452,14 @@ module RangeAnalysis { * * This means negative-weight cycles (contradictions) can be detected using simple cycle detection. */ - private predicate extendedEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int c) { - seedEdgeWithDual(cfg, a, asign, b, bsign, c) + private predicate extendedEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int c, boolean sharp) { + seedEdgeWithDual(cfg, a, asign, b, bsign, c, sharp) or - exists (DataFlow::Node mid, int midx, ControlFlowNode cfg1, int c1, ControlFlowNode cfg2, int c2 | - extendedEdge(cfg1, a, asign, mid, midx, c1) and - extendedEdge(cfg2, mid, midx, b, bsign, c2) and - c = wideningAddition(c1, c2) and + exists (DataFlow::Node mid, int midx, ControlFlowNode cfg1, int c1, ControlFlowNode cfg2, int c2, boolean sharp1, boolean sharp2 | + extendedEdge(cfg1, a, asign, mid, midx, c1, sharp1) and + extendedEdge(cfg2, mid, midx, b, bsign, c2, sharp2) and + sharp = sharp1.booleanOr(sharp2) and + c = wideningAddition(c1, sharp1, c2, sharp2) and // One of the two CFG nodes must dominate the other, and `cfg` must be bound to the dominated one. ( // They are in the same basic block @@ -481,7 +485,9 @@ module RangeAnalysis { * Holds if there is a negative-weight edge from src to dst. */ private predicate negativeEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign) { - exists (int weight | extendedEdge(cfg, a, asign, b, bsign, weight) | + exists (int weight, boolean sharp | extendedEdge(cfg, a, asign, b, bsign, weight, sharp) | + weight = 0 and sharp = true // a strict "< 0" edge counts as negative + or weight < 0) } From feb8a8c4fd11fad881f1ec3072806a8c84bd21d2 Mon Sep 17 00:00:00 2001 From: Asger F Date: Thu, 4 Oct 2018 11:47:11 +0100 Subject: [PATCH 08/27] JS: restrict bias to 30-bit range to avoid overflow --- .../src/semmle/javascript/RangeAnalysis.qll | 42 ++++++++++++------- 1 file changed, 28 insertions(+), 14 deletions(-) diff --git a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll index f8ccfa441593..2010823d5f39 100644 --- a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll +++ b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll @@ -119,13 +119,26 @@ module RangeAnalysis { 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, int bias) { + 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 | @@ -183,7 +196,7 @@ module RangeAnalysis { /** * Holds if `r` can be modelled as `r = root * sign + bias`. */ - predicate linearDefinition(DataFlow::Node r, DataFlow::Node root, int sign, int 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 @@ -202,7 +215,7 @@ module RangeAnalysis { /** * 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, int 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 @@ -225,7 +238,7 @@ module RangeAnalysis { /** * Holds if the given comparison can be modelled as `A B + bias` where `` is the comparison operator. */ - predicate linearComparison(Comparison comparison, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int bias) { + predicate linearComparison(Comparison comparison, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, Bias bias) { exists(Expr left, Expr right, int bias1, int bias2 | left = comparison.getLeftOperand() and right = comparison.getRightOperand() | // A <= B + c linearDefinition(left.flow(), a, asign, bias1) and @@ -247,7 +260,7 @@ module RangeAnalysis { /** * Holds if `guard` asserts that the outcome of `A B + bias` is true, where `` is a comparison operator. */ - predicate linearComparisonGuard(ConditionGuardNode guard, DataFlow::Node a, int asign, string operator, DataFlow::Node b, int bsign, int bias) { + predicate linearComparisonGuard(ConditionGuardNode guard, DataFlow::Node a, int asign, string operator, DataFlow::Node b, int bsign, Bias bias) { exists (Comparison compare | compare = getDefinition(guard.getTest().flow()).asExpr() | linearComparison(compare, a, asign, b, bsign, bias) and ( @@ -279,7 +292,7 @@ module RangeAnalysis { * * The dual constraint `-B <= -A + c` is not included in this predicate. */ - predicate comparisonEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int bias, boolean sharp) { + predicate comparisonEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, Bias bias, boolean sharp) { // A <= B + c linearComparisonGuard(cfg, a, asign, "<=", b, bsign, bias) and sharp = false @@ -321,14 +334,14 @@ module RangeAnalysis { /** * Holds if `A <= B + c` can be determined based on a phi node. */ - predicate phiEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int c) { + predicate phiEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, Bias c) { exists (DataFlow::Node phi, DataFlow::Node left, DataFlow::Node right | binaryPhiNode(phi, left, right) and cfg = phi.getBasicBlock() | // Both inputs are defined in terms of the same root: // phi = PHI(root + bias1, root + bias2) - exists (DataFlow::Node root, int sign, int bias1, int bias2 | + exists (DataFlow::Node root, int sign, Bias bias1, Bias bias2 | linearDefinition(left, root, sign, bias1) and linearDefinition(right, root, sign, bias2) and bias1 < bias2 and @@ -348,7 +361,7 @@ module RangeAnalysis { or // One input is defined in terms of the phi node itself: // phi = PHI(phi + increment, x) - exists (int increment, DataFlow::Node root, int sign, int bias | + exists (int increment, DataFlow::Node root, int sign, Bias bias | linearDefinition(left, phi, 1, increment) and linearDefinition(right, root, sign, bias) and ( @@ -378,8 +391,9 @@ module RangeAnalysis { * A + A <= 2c becomes A <= -A + 2c * A + A >= 2c becomes -A <= A - 2c */ - predicate constantEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int c) { + predicate constantEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, Bias c) { exists (NumberLiteral literal | cfg = literal | + literal.getIntValue() instanceof Bias and // avoid overflow a = literal.flow() and b = a and (asign = 1 or asign = -1) and @@ -390,7 +404,7 @@ module RangeAnalysis { /** * The set of initial edges including those from dual constraints. */ - private predicate seedEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int c, boolean sharp) { + predicate seedEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, Bias c, boolean sharp) { // A <= B + c comparisonEdge(cfg, a, asign, b, bsign, c, sharp) or @@ -399,7 +413,7 @@ module RangeAnalysis { constantEdge(cfg, a, asign, b, bsign, c) and sharp = false } - private predicate seedEdgeWithDual(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int c, boolean sharp) { + private predicate seedEdgeWithDual(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, Bias c, boolean sharp) { // A <= B + c seedEdge(cfg, a, asign, b, bsign, c, sharp) or @@ -452,10 +466,10 @@ module RangeAnalysis { * * This means negative-weight cycles (contradictions) can be detected using simple cycle detection. */ - private predicate extendedEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, int c, boolean sharp) { + private predicate extendedEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, Bias c, boolean sharp) { seedEdgeWithDual(cfg, a, asign, b, bsign, c, sharp) or - exists (DataFlow::Node mid, int midx, ControlFlowNode cfg1, int c1, ControlFlowNode cfg2, int c2, boolean sharp1, boolean sharp2 | + exists (DataFlow::Node mid, int midx, ControlFlowNode cfg1, Bias c1, ControlFlowNode cfg2, Bias c2, boolean sharp1, boolean sharp2 | extendedEdge(cfg1, a, asign, mid, midx, c1, sharp1) and extendedEdge(cfg2, mid, midx, b, bsign, c2, sharp2) and sharp = sharp1.booleanOr(sharp2) and From 43df9538bf7d9f676be2aee09b3db0a86dc5d557 Mon Sep 17 00:00:00 2001 From: Asger F Date: Tue, 23 Oct 2018 15:36:41 +0100 Subject: [PATCH 09/27] JS: be conservative in presence of NaN comments --- .../src/semmle/javascript/RangeAnalysis.qll | 21 ++++++++++++++++++- .../test/library-tests/RangeAnalysis/tst.js | 12 +++++++++++ 2 files changed, 32 insertions(+), 1 deletion(-) diff --git a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll index 2010823d5f39..e944b82494e9 100644 --- a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll +++ b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll @@ -69,7 +69,7 @@ import javascript * * CAVEATS: * - * - We assume !(x <= y) means x > y, ignoring NaN. + * - 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. * @@ -257,6 +257,24 @@ module RangeAnalysis { ) } + /** + * Holds if the given container has a comment or identifier mentioning `NaN`. + */ + predicate hasNaNIndicator(StmtContainer container) { + exists (Comment comment | + comment.getText().regexpMatch("(?s).*N[aA]N.*") and + comment.getFile() = container.getFile() and + ( + comment.getLocation().getStartLine() >= container.getLocation().getStartLine() and + comment.getLocation().getEndLine() <= container.getLocation().getEndLine() + or + comment.getNextToken() = container.getFirstToken() + )) + or + exists (Identifier id | id.getName() = "NaN" or id.getName() = "isNaN" | + id.getContainer() = container) + } + /** * Holds if `guard` asserts that the outcome of `A B + bias` is true, where `` is a comparison operator. */ @@ -266,6 +284,7 @@ module RangeAnalysis { ( guard.getOutcome() = true and operator = compare.getOperator() or + not hasNaNIndicator(guard.getContainer()) and guard.getOutcome() = false and operator = negateOperator(compare.getOperator()) ) ) diff --git a/javascript/ql/test/library-tests/RangeAnalysis/tst.js b/javascript/ql/test/library-tests/RangeAnalysis/tst.js index f89086711f6b..6dcdd8420457 100644 --- a/javascript/ql/test/library-tests/RangeAnalysis/tst.js +++ b/javascript/ql/test/library-tests/RangeAnalysis/tst.js @@ -50,3 +50,15 @@ function h(x, y) { if (x > y) {} // NOT OK - always true } } + +function nan(x) { + // This is a NaN comment. + if (x - 1 < x) {} // OK +} + +/** + * This is a NAN comment. + */ +function nan2(x) { + if (x - 1 < x) {} // OK +} From d813635f3e5af74df2783822de270ea83dad6389 Mon Sep 17 00:00:00 2001 From: Asger F Date: Thu, 25 Oct 2018 16:05:23 +0100 Subject: [PATCH 10/27] JS: Restrict constraint generation to relevant nodes --- .../src/semmle/javascript/RangeAnalysis.qll | 22 +++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll index e944b82494e9..befc244b8acd 100644 --- a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll +++ b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll @@ -79,11 +79,30 @@ import javascript * 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 } @@ -206,6 +225,7 @@ module RangeAnalysis { sign = sign1 * sign2 and bias = bias1 + sign1 * bias2) else ( + isRelevant(r) and root = r and sign = 1 and bias = 0 @@ -344,6 +364,7 @@ module RangeAnalysis { */ predicate binaryPhiNode(DataFlow::Node node, DataFlow::Node left, DataFlow::Node right) { exists (SsaPhiNode phi | node = DataFlow::ssaDefinitionNode(phi) | + isRelevant(node) and strictcount(phi.getAnInput()) = 2 and left = DataFlow::ssaDefinitionNode(phi.getAnInput()) and right = DataFlow::ssaDefinitionNode(phi.getAnInput()) and @@ -412,6 +433,7 @@ module RangeAnalysis { */ predicate constantEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, Bias c) { exists (NumberLiteral literal | cfg = literal | + isRelevant(literal.flow()) and literal.getIntValue() instanceof Bias and // avoid overflow a = literal.flow() and b = a and From 344bec38656f4e220cbd12bb4ccce5cf94b8f2ca Mon Sep 17 00:00:00 2001 From: Asger F Date: Fri, 21 Sep 2018 12:24:25 +0100 Subject: [PATCH 11/27] JS: Add UselessRangeCheck.ql --- .../ql/src/Statements/UselessRangeCheck.qhelp | 47 +++++++++++++++++++ .../ql/src/Statements/UselessRangeCheck.ql | 28 +++++++++++ .../Statements/examples/UselessRangeCheck.js | 12 +++++ .../examples/UselessRangeCheckGood.js | 8 ++++ .../UselessRangeCheck.expected | 1 + .../UselessRangeCheck/UselessRangeCheck.qlref | 1 + .../Statements/UselessRangeCheck/example.js | 12 +++++ .../UselessRangeCheck/exampleGood.js | 8 ++++ 8 files changed, 117 insertions(+) create mode 100644 javascript/ql/src/Statements/UselessRangeCheck.qhelp create mode 100644 javascript/ql/src/Statements/UselessRangeCheck.ql create mode 100644 javascript/ql/src/Statements/examples/UselessRangeCheck.js create mode 100644 javascript/ql/src/Statements/examples/UselessRangeCheckGood.js create mode 100644 javascript/ql/test/query-tests/Statements/UselessRangeCheck/UselessRangeCheck.expected create mode 100644 javascript/ql/test/query-tests/Statements/UselessRangeCheck/UselessRangeCheck.qlref create mode 100644 javascript/ql/test/query-tests/Statements/UselessRangeCheck/example.js create mode 100644 javascript/ql/test/query-tests/Statements/UselessRangeCheck/exampleGood.js diff --git a/javascript/ql/src/Statements/UselessRangeCheck.qhelp b/javascript/ql/src/Statements/UselessRangeCheck.qhelp new file mode 100644 index 000000000000..74a6168dd722 --- /dev/null +++ b/javascript/ql/src/Statements/UselessRangeCheck.qhelp @@ -0,0 +1,47 @@ + + + +

+If a condition always evaluates to true or always evaluates to false, this often indicates +incomplete code or a latent bug and should be examined carefully. +

+ + + + +

+Examine the surrounding code to determine why the condition is useless. 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/UselessRangeCheck.ql b/javascript/ql/src/Statements/UselessRangeCheck.ql new file mode 100644 index 000000000000..f737110442f5 --- /dev/null +++ b/javascript/ql/src/Statements/UselessRangeCheck.ql @@ -0,0 +1,28 @@ +/** + * @name Useless range check + * @description If a range check always fails or always succeeds it is indicative of a bug. + * @kind problem + * @problem.severity warning + * @id js/useless-range-check + * @tags correctness + * @precision high + */ + +import javascript + +/** + * Gets the guard node with the opposite outcome of `guard`. + */ +ConditionGuardNode getOppositeGuard(ConditionGuardNode guard) { + result.getTest() = guard.getTest() and + result.getOutcome() = guard.getOutcome().booleanNot() +} + +from ConditionGuardNode guard +where RangeAnalysis::isContradictoryGuardNode(guard) + + // Do not report conditions that themselves are unreachable because of + // a prior contradiction. + and not RangeAnalysis::isContradictoryGuardNode(getOppositeGuard(guard)) + +select guard.getTest(), "The condition '" + guard.getTest() + "' is always " + guard.getOutcome().booleanNot() diff --git a/javascript/ql/src/Statements/examples/UselessRangeCheck.js b/javascript/ql/src/Statements/examples/UselessRangeCheck.js new file mode 100644 index 000000000000..53496ce2e4ef --- /dev/null +++ b/javascript/ql/src/Statements/examples/UselessRangeCheck.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/UselessRangeCheckGood.js b/javascript/ql/src/Statements/examples/UselessRangeCheckGood.js new file mode 100644 index 000000000000..6f86622c99b6 --- /dev/null +++ b/javascript/ql/src/Statements/examples/UselessRangeCheckGood.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/test/query-tests/Statements/UselessRangeCheck/UselessRangeCheck.expected b/javascript/ql/test/query-tests/Statements/UselessRangeCheck/UselessRangeCheck.expected new file mode 100644 index 000000000000..bdf5055e767c --- /dev/null +++ b/javascript/ql/test/query-tests/Statements/UselessRangeCheck/UselessRangeCheck.expected @@ -0,0 +1 @@ +| example.js:8:7:8:13 | i < end | The condition 'i < end' is always false | diff --git a/javascript/ql/test/query-tests/Statements/UselessRangeCheck/UselessRangeCheck.qlref b/javascript/ql/test/query-tests/Statements/UselessRangeCheck/UselessRangeCheck.qlref new file mode 100644 index 000000000000..f5d7a1ee7a40 --- /dev/null +++ b/javascript/ql/test/query-tests/Statements/UselessRangeCheck/UselessRangeCheck.qlref @@ -0,0 +1 @@ +Statements/UselessRangeCheck.ql diff --git a/javascript/ql/test/query-tests/Statements/UselessRangeCheck/example.js b/javascript/ql/test/query-tests/Statements/UselessRangeCheck/example.js new file mode 100644 index 000000000000..53496ce2e4ef --- /dev/null +++ b/javascript/ql/test/query-tests/Statements/UselessRangeCheck/example.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/test/query-tests/Statements/UselessRangeCheck/exampleGood.js b/javascript/ql/test/query-tests/Statements/UselessRangeCheck/exampleGood.js new file mode 100644 index 000000000000..6f86622c99b6 --- /dev/null +++ b/javascript/ql/test/query-tests/Statements/UselessRangeCheck/exampleGood.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; +} From 84ea4cf1d1db0223855809e42a6166b70d4c7afc Mon Sep 17 00:00:00 2001 From: Asger F Date: Thu, 1 Nov 2018 12:11:02 +0000 Subject: [PATCH 12/27] JS: manually reorder extendedEdge and negativeEdge --- .../src/semmle/javascript/RangeAnalysis.qll | 24 +++++++++---------- 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll index befc244b8acd..0079bd842f3c 100644 --- a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll +++ b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll @@ -507,12 +507,12 @@ module RangeAnalysis { * * This means negative-weight cycles (contradictions) can be detected using simple cycle detection. */ - private predicate extendedEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, Bias c, boolean sharp) { + private predicate extendedEdge(DataFlow::Node a, int asign, DataFlow::Node b, int bsign, Bias c, boolean sharp, ControlFlowNode cfg) { seedEdgeWithDual(cfg, a, asign, b, bsign, c, sharp) or exists (DataFlow::Node mid, int midx, ControlFlowNode cfg1, Bias c1, ControlFlowNode cfg2, Bias c2, boolean sharp1, boolean sharp2 | - extendedEdge(cfg1, a, asign, mid, midx, c1, sharp1) and - extendedEdge(cfg2, mid, midx, b, bsign, c2, sharp2) and + extendedEdge(a, asign, mid, midx, c1, sharp1, cfg1) and + extendedEdge(mid, midx, b, bsign, c2, sharp2, cfg2) and sharp = sharp1.booleanOr(sharp2) and c = wideningAddition(c1, sharp1, c2, sharp2) and // One of the two CFG nodes must dominate the other, and `cfg` must be bound to the dominated one. @@ -539,8 +539,8 @@ module RangeAnalysis { /** * Holds if there is a negative-weight edge from src to dst. */ - private predicate negativeEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign) { - exists (int weight, boolean sharp | extendedEdge(cfg, a, asign, b, bsign, weight, sharp) | + private predicate negativeEdge(DataFlow::Node a, int asign, DataFlow::Node b, int bsign, ControlFlowNode cfg) { + exists (int weight, boolean sharp | extendedEdge(a, asign, b, bsign, weight, sharp, cfg) | weight = 0 and sharp = true // a strict "< 0" edge counts as negative or weight < 0) @@ -552,12 +552,12 @@ module RangeAnalysis { * The initial outgoing edge from `src` must be derived at `cfg`. */ pragma[noopt] - private predicate reachableByNegativeEdges(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign) { - negativeEdge(cfg, a, asign, b, bsign) + private predicate reachableByNegativeEdges(DataFlow::Node a, int asign, DataFlow::Node b, int bsign, ControlFlowNode cfg) { + negativeEdge(a, asign, b, bsign, cfg) or exists(DataFlow::Node mid, int midx, ControlFlowNode midcfg | - reachableByNegativeEdges(cfg, a, asign, mid, midx) and - negativeEdge(midcfg, mid, midx, b, bsign) and + reachableByNegativeEdges(a, asign, mid, midx, cfg) and + negativeEdge(mid, midx, b, bsign, midcfg) and exists (BasicBlock bb, int i, int j | bb.getNode(i) = midcfg and bb.getNode(j) = cfg and @@ -565,8 +565,8 @@ module RangeAnalysis { or // Same as above, but where CFG nodes are in different basic blocks exists(DataFlow::Node mid, int midx, ControlFlowNode midcfg, BasicBlock midBB, ReachableBasicBlock midRBB, BasicBlock cfgBB | - reachableByNegativeEdges(cfg, a, asign, mid, midx) and - negativeEdge(midcfg, mid, midx, b, bsign) and + reachableByNegativeEdges(a, asign, mid, midx, cfg) and + negativeEdge(mid, midx, b, bsign, midcfg) and midBB = midcfg.getBasicBlock() and midRBB = midBB.(ReachableBasicBlock) and cfgBB = cfg.getBasicBlock() and @@ -579,6 +579,6 @@ module RangeAnalysis { * opposite of the expected outcome. */ predicate isContradictoryGuardNode(ConditionGuardNode guard) { - exists (DataFlow::Node a, int asign | reachableByNegativeEdges(guard, a, asign, a, asign)) + exists (DataFlow::Node a, int asign | reachableByNegativeEdges(a, asign, a, asign, guard)) } } From 2d6bf0aff36cc6b1134484aad22dac117959863b Mon Sep 17 00:00:00 2001 From: Asger F Date: Thu, 1 Nov 2018 13:36:03 +0000 Subject: [PATCH 13/27] JS: improve join ordering in extendedEdge --- .../src/semmle/javascript/RangeAnalysis.qll | 61 ++++++++++++------- 1 file changed, 40 insertions(+), 21 deletions(-) diff --git a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll index 0079bd842f3c..da6ef36dcb0a 100644 --- a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll +++ b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll @@ -507,33 +507,52 @@ module RangeAnalysis { * * This means negative-weight cycles (contradictions) can be detected using simple cycle detection. */ + pragma[noopt] private predicate extendedEdge(DataFlow::Node a, int asign, DataFlow::Node b, int bsign, Bias c, boolean sharp, ControlFlowNode cfg) { seedEdgeWithDual(cfg, a, asign, b, bsign, c, sharp) or - exists (DataFlow::Node mid, int midx, ControlFlowNode cfg1, Bias c1, ControlFlowNode cfg2, Bias c2, boolean sharp1, boolean sharp2 | + // One of the two CFG nodes must dominate the other, and `cfg` must be bound to the dominated one. + exists (ControlFlowNode cfg1, ControlFlowNode cfg2 | + // They are in the same basic block + extendedEdgeCandidate(a, asign, b, bsign, c, sharp, cfg1, cfg2) and + exists (BasicBlock bb, int i, int j | + bb.getNode(i) = cfg1 and + bb.getNode(j) = cfg2 and + if i < j then + cfg = cfg2 + else + cfg = cfg1) + or + // They are in different basic blocks + extendedEdgeCandidate(a, asign, b, bsign, c, sharp, cfg1, cfg2) and + exists (BasicBlock cfg1BB, ReachableBasicBlock cfg1RBB, BasicBlock cfg2BB, ReachableBasicBlock cfg2RBB | + cfg1BB = cfg1.getBasicBlock() and + cfg1RBB = cfg1BB.(ReachableBasicBlock) and + cfg2BB = cfg2.getBasicBlock() and + cfg2RBB = cfg2BB.(ReachableBasicBlock) and + ( + cfg1RBB.strictlyDominates(cfg2BB) and + cfg = cfg2 + or + cfg2RBB.strictlyDominates(cfg1RBB) and + cfg = cfg1 + )) + ) and + cfg instanceof ControlFlowNode + } + + /** + * Holds if an extended edge from `A` to `B` can potentially be generates from two edges, from `cfg1` and `cfg2`, respectively. + * + * This does not check for dominance between `cfg1` and `cfg2`. + */ + pragma[nomagic] + private predicate extendedEdgeCandidate(DataFlow::Node a, int asign, DataFlow::Node b, int bsign, Bias c, boolean sharp, ControlFlowNode cfg1, ControlFlowNode cfg2) { + exists (DataFlow::Node mid, int midx, Bias c1, Bias c2, boolean sharp1, boolean sharp2 | extendedEdge(a, asign, mid, midx, c1, sharp1, cfg1) and extendedEdge(mid, midx, b, bsign, c2, sharp2, cfg2) and sharp = sharp1.booleanOr(sharp2) and - c = wideningAddition(c1, sharp1, c2, sharp2) and - // One of the two CFG nodes must dominate the other, and `cfg` must be bound to the dominated one. - ( - // They are in the same basic block - exists (BasicBlock bb, int i, int j | - bb.getNode(i) = cfg1 and - bb.getNode(j) = cfg2 and - if i < j then - cfg = cfg2 - else - cfg = cfg1) - or - // They are in different basic blocks - cfg1.getBasicBlock().(ReachableBasicBlock).strictlyDominates(cfg2.getBasicBlock()) and - cfg = cfg2 - or - cfg2.getBasicBlock().(ReachableBasicBlock).strictlyDominates(cfg1.getBasicBlock()) and - cfg = cfg1 - ) - ) + c = wideningAddition(c1, sharp1, c2, sharp2)) } /** From 5283c6cd48af0d30edd6df224c147458f64505ad Mon Sep 17 00:00:00 2001 From: Asger F Date: Tue, 6 Nov 2018 11:47:18 +0000 Subject: [PATCH 14/27] JS: only warn about dead code --- .../ql/src/Statements/UselessRangeCheck.ql | 49 +++++++++++++++---- 1 file changed, 40 insertions(+), 9 deletions(-) diff --git a/javascript/ql/src/Statements/UselessRangeCheck.ql b/javascript/ql/src/Statements/UselessRangeCheck.ql index f737110442f5..c52a24c6341e 100644 --- a/javascript/ql/src/Statements/UselessRangeCheck.ql +++ b/javascript/ql/src/Statements/UselessRangeCheck.ql @@ -11,18 +11,49 @@ import javascript /** - * Gets the guard node with the opposite outcome of `guard`. + * Holds if there are any contradictory guard nodes in `container`. + * + * We use this to restrict reachability analysis to a small set of containers. */ -ConditionGuardNode getOppositeGuard(ConditionGuardNode guard) { - result.getTest() = guard.getTest() and - result.getOutcome() = guard.getOutcome().booleanNot() +predicate hasContradictoryGuardNodes(StmtContainer container) { + exists (ConditionGuardNode guard | + RangeAnalysis::isContradictoryGuardNode(guard) and + container = guard.getContainer()) } -from ConditionGuardNode guard -where RangeAnalysis::isContradictoryGuardNode(guard) +/** + * 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) +} - // Do not report conditions that themselves are unreachable because of - // a prior contradiction. - and not RangeAnalysis::isContradictoryGuardNode(getOppositeGuard(guard)) +/** + * 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() From 4a367d3fdb371d80c0cb69b64bc3b0f5f2ef2a67 Mon Sep 17 00:00:00 2001 From: Asger F Date: Fri, 9 Nov 2018 13:16:06 +0000 Subject: [PATCH 15/27] JS: more efficient encoding of unary constraints --- .../src/semmle/javascript/RangeAnalysis.qll | 48 ++++++++++++------- 1 file changed, 32 insertions(+), 16 deletions(-) diff --git a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll index da6ef36dcb0a..bc2e8cbf39d5 100644 --- a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll +++ b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll @@ -424,34 +424,50 @@ module RangeAnalysis { } /** - * Holds constraints derived from `A = const`. + * Holds if a comparison implies that `A <= B + c`. * - * `A = c` is written to `A + A = 2c` which is then converted to `<=` and `>=`. - * - * A + A <= 2c becomes A <= -A + 2c - * A + A >= 2c becomes -A <= A - 2c + * Comparisons where one operand is really a constant are converted into a unary constraint. */ - predicate constantEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, Bias c) { - exists (NumberLiteral literal | cfg = literal | - isRelevant(literal.flow()) and - literal.getIntValue() instanceof Bias and // avoid overflow - a = literal.flow() and + predicate foldedComparisonEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, Bias c, boolean sharp) { + // A <= B + c (where A and B are not constants) + comparisonEdge(cfg, a, asign, b, bsign, c, sharp) and + not exists(a.asExpr().getIntValue()) and + not exists(b.asExpr().getIntValue()) + or + // A - k <= c becomes A - (-A) <= 2*(k + c) + exists (DataFlow::Node k, int ksign, Bias kbias, Bias value | + comparisonEdge(cfg, a, asign, k, ksign, kbias, sharp) and + value = k.asExpr().getIntValue() and b = a and - (asign = 1 or asign = -1) and bsign = -asign and - c = literal.getIntValue() * 2 * asign) + c = 2 * (value * ksign + kbias)) + or + // k - A <= c becomes -A - A <= 2(-k + c) + exists (DataFlow::Node k, int ksign, Bias kbias, Bias value | + comparisonEdge(cfg, k, ksign, b, bsign, kbias, sharp) and + value = k.asExpr().getIntValue() and + a = b and + asign = -bsign and + c = 2 * (-value * ksign + kbias)) + or + // For completeness, generate a contradictory constraint for trivially false conditions. + exists (DataFlow::Node k, int ksign, Bias bias, int avalue, int kvalue | + comparisonEdge(cfg, a, asign, k, ksign, bias, sharp) and + avalue = a.asExpr().getIntValue() * asign and + kvalue = b.asExpr().getIntValue() * bsign and + (avalue < kvalue + bias or sharp = true and avalue = kvalue + bias) and + a = b and + asign = bsign and + c = -1) } /** * The set of initial edges including those from dual constraints. */ predicate seedEdge(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, Bias c, boolean sharp) { - // A <= B + c - comparisonEdge(cfg, a, asign, b, bsign, c, sharp) + foldedComparisonEdge(cfg, a, asign, b, bsign, c, sharp) or phiEdge(cfg, a, asign, b, bsign, c) and sharp = false - or - constantEdge(cfg, a, asign, b, bsign, c) and sharp = false } private predicate seedEdgeWithDual(ControlFlowNode cfg, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, Bias c, boolean sharp) { From f3020f776e5b17356e31fd874c9524c42e691441 Mon Sep 17 00:00:00 2001 From: Asger F Date: Mon, 12 Nov 2018 12:26:06 +0000 Subject: [PATCH 16/27] JS: avoid extending self-edges --- javascript/ql/src/semmle/javascript/RangeAnalysis.qll | 2 ++ 1 file changed, 2 insertions(+) diff --git a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll index bc2e8cbf39d5..e16731a6132e 100644 --- a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll +++ b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll @@ -567,6 +567,8 @@ module RangeAnalysis { exists (DataFlow::Node mid, int midx, Bias c1, Bias c2, boolean sharp1, boolean sharp2 | extendedEdge(a, asign, mid, midx, c1, sharp1, cfg1) and extendedEdge(mid, midx, b, bsign, c2, sharp2, cfg2) and + (a != mid or asign != midx) and + (b != mid or bsign != midx) and sharp = sharp1.booleanOr(sharp2) and c = wideningAddition(c1, sharp1, c2, sharp2)) } From 76a69f4ff2a4bd8ad1ed34466270deaeaebafd12 Mon Sep 17 00:00:00 2001 From: Asger F Date: Tue, 13 Nov 2018 12:44:29 +0000 Subject: [PATCH 17/27] JS: address review comments --- .../ql/src/Statements/UselessRangeCheck.qhelp | 4 +-- .../src/semmle/javascript/RangeAnalysis.qll | 32 ++++++++++++------- 2 files changed, 23 insertions(+), 13 deletions(-) diff --git a/javascript/ql/src/Statements/UselessRangeCheck.qhelp b/javascript/ql/src/Statements/UselessRangeCheck.qhelp index 74a6168dd722..c9f933ef7872 100644 --- a/javascript/ql/src/Statements/UselessRangeCheck.qhelp +++ b/javascript/ql/src/Statements/UselessRangeCheck.qhelp @@ -17,7 +17,7 @@ longer needed, remove it.

    -If the check is needed to guard against NaN values, insert a comment explaning the possibility of NaN. +If the check is needed to guard against NaN values, insert a comment explaning the possibility of NaN.

    @@ -30,7 +30,7 @@ The following example finds the index of an element in a given slice of the arra

    -The condition i < end at the end is always false, however. The code can be clarified if the +The condition i < end at the end is always false, however. The code can be clarified if the redundant condition is removed:

    diff --git a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll index e16731a6132e..229d3bc97e4a 100644 --- a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll +++ b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll @@ -161,31 +161,35 @@ module RangeAnalysis { 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 - exists (AddExpr expr | r.asExpr() = expr | + 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 - exists (SubExpr expr | r.asExpr() = expr | + 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 @@ -194,6 +198,7 @@ module RangeAnalysis { 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 @@ -203,9 +208,11 @@ module RangeAnalysis { 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() )) @@ -220,8 +227,11 @@ module RangeAnalysis { 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 ( @@ -242,11 +252,13 @@ module RangeAnalysis { 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) @@ -256,7 +268,8 @@ module RangeAnalysis { } /** - * Holds if the given comparison can be modelled as `A B + bias` where `` is the comparison operator. + * Holds if the given comparison can be modelled as `A B + bias` where `` is the comparison operator, + * and `A` is `a * asign` and likewise `B` is `b * bsign`. */ predicate linearComparison(Comparison comparison, DataFlow::Node a, int asign, DataFlow::Node b, int bsign, Bias bias) { exists(Expr left, Expr right, int bias1, int bias2 | left = comparison.getLeftOperand() and right = comparison.getRightOperand() | @@ -315,13 +328,10 @@ module RangeAnalysis { */ private string negateOperator(string operator) { operator = "==" and result = "!=" or - operator = "!=" and result = "==" or operator = "===" and result = "!==" or - operator = "!==" and result = "===" or operator = "<" and result = ">=" or - operator = "<=" and result = ">" or operator = ">" and result = "<=" or - operator = ">=" and result = "<" + operator = negateOperator(result) } /** From 287020929919710df5702bfda292f6a48bdad7f1 Mon Sep 17 00:00:00 2001 From: Asger F Date: Thu, 15 Nov 2018 16:49:48 +0000 Subject: [PATCH 18/27] JS: fix links in qhelp file --- javascript/ql/src/Statements/UselessRangeCheck.qhelp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/javascript/ql/src/Statements/UselessRangeCheck.qhelp b/javascript/ql/src/Statements/UselessRangeCheck.qhelp index c9f933ef7872..6c35fdd2848d 100644 --- a/javascript/ql/src/Statements/UselessRangeCheck.qhelp +++ b/javascript/ql/src/Statements/UselessRangeCheck.qhelp @@ -27,14 +27,14 @@ If the check is needed to guard against NaN values, insert a commen 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:

    - + From 2e65f6b66022b20d708d5b328f15bb2329f121ce Mon Sep 17 00:00:00 2001 From: Asger F Date: Thu, 15 Nov 2018 16:53:34 +0000 Subject: [PATCH 19/27] JS: address some style comments --- javascript/ql/src/Statements/UselessRangeCheck.qhelp | 4 ++-- javascript/ql/src/Statements/UselessRangeCheck.ql | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/javascript/ql/src/Statements/UselessRangeCheck.qhelp b/javascript/ql/src/Statements/UselessRangeCheck.qhelp index 6c35fdd2848d..8bac3f99818f 100644 --- a/javascript/ql/src/Statements/UselessRangeCheck.qhelp +++ b/javascript/ql/src/Statements/UselessRangeCheck.qhelp @@ -5,14 +5,14 @@

    If a condition always evaluates to true or always evaluates to false, this often indicates -incomplete code or a latent bug and should be examined carefully. +incomplete code or a latent bug, and it should be examined carefully.

    -Examine the surrounding code to determine why the condition is useless. If it is no +Examine the surrounding code to determine why the condition is redundant. If it is no longer needed, remove it.

    diff --git a/javascript/ql/src/Statements/UselessRangeCheck.ql b/javascript/ql/src/Statements/UselessRangeCheck.ql index c52a24c6341e..c124b5e3a9ad 100644 --- a/javascript/ql/src/Statements/UselessRangeCheck.ql +++ b/javascript/ql/src/Statements/UselessRangeCheck.ql @@ -1,6 +1,6 @@ /** * @name Useless range check - * @description If a range check always fails or always succeeds it is indicative of a bug. + * @description If a range check always fails or always succeeds, it is indicative of a bug. * @kind problem * @problem.severity warning * @id js/useless-range-check From 477be260f35b64d37fb73aa1b5262d2f23b6c9d7 Mon Sep 17 00:00:00 2001 From: Asger F Date: Thu, 15 Nov 2018 17:08:34 +0000 Subject: [PATCH 20/27] JS: rename UselessRangeCheck -> UselessComparisonTest --- .../{UselessRangeCheck.qhelp => UselessComparisonTest.qhelp} | 4 ++-- .../{UselessRangeCheck.ql => UselessComparisonTest.ql} | 5 +++-- .../{UselessRangeCheck.js => UselessComparisonTest.js} | 0 ...UselessRangeCheckGood.js => UselessComparisonTestGood.js} | 0 .../UselessComparisonTest.expected} | 0 .../UselessComparisonTest/UselessComparisonTest.qlref | 1 + .../{UselessRangeCheck => UselessComparisonTest}/example.js | 0 .../exampleGood.js | 0 .../Statements/UselessRangeCheck/UselessRangeCheck.qlref | 1 - 9 files changed, 6 insertions(+), 5 deletions(-) rename javascript/ql/src/Statements/{UselessRangeCheck.qhelp => UselessComparisonTest.qhelp} (90%) rename javascript/ql/src/Statements/{UselessRangeCheck.ql => UselessComparisonTest.ql} (91%) rename javascript/ql/src/Statements/examples/{UselessRangeCheck.js => UselessComparisonTest.js} (100%) rename javascript/ql/src/Statements/examples/{UselessRangeCheckGood.js => UselessComparisonTestGood.js} (100%) rename javascript/ql/test/query-tests/Statements/{UselessRangeCheck/UselessRangeCheck.expected => UselessComparisonTest/UselessComparisonTest.expected} (100%) create mode 100644 javascript/ql/test/query-tests/Statements/UselessComparisonTest/UselessComparisonTest.qlref rename javascript/ql/test/query-tests/Statements/{UselessRangeCheck => UselessComparisonTest}/example.js (100%) rename javascript/ql/test/query-tests/Statements/{UselessRangeCheck => UselessComparisonTest}/exampleGood.js (100%) delete mode 100644 javascript/ql/test/query-tests/Statements/UselessRangeCheck/UselessRangeCheck.qlref diff --git a/javascript/ql/src/Statements/UselessRangeCheck.qhelp b/javascript/ql/src/Statements/UselessComparisonTest.qhelp similarity index 90% rename from javascript/ql/src/Statements/UselessRangeCheck.qhelp rename to javascript/ql/src/Statements/UselessComparisonTest.qhelp index 8bac3f99818f..27483f5516a0 100644 --- a/javascript/ql/src/Statements/UselessRangeCheck.qhelp +++ b/javascript/ql/src/Statements/UselessComparisonTest.qhelp @@ -27,14 +27,14 @@ If the check is needed to guard against NaN values, insert a commen 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:

    - + diff --git a/javascript/ql/src/Statements/UselessRangeCheck.ql b/javascript/ql/src/Statements/UselessComparisonTest.ql similarity index 91% rename from javascript/ql/src/Statements/UselessRangeCheck.ql rename to javascript/ql/src/Statements/UselessComparisonTest.ql index c124b5e3a9ad..6a4eef8c631e 100644 --- a/javascript/ql/src/Statements/UselessRangeCheck.ql +++ b/javascript/ql/src/Statements/UselessComparisonTest.ql @@ -1,6 +1,7 @@ /** - * @name Useless range check - * @description If a range check always fails or always succeeds, it is indicative of a bug. + * @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-range-check diff --git a/javascript/ql/src/Statements/examples/UselessRangeCheck.js b/javascript/ql/src/Statements/examples/UselessComparisonTest.js similarity index 100% rename from javascript/ql/src/Statements/examples/UselessRangeCheck.js rename to javascript/ql/src/Statements/examples/UselessComparisonTest.js diff --git a/javascript/ql/src/Statements/examples/UselessRangeCheckGood.js b/javascript/ql/src/Statements/examples/UselessComparisonTestGood.js similarity index 100% rename from javascript/ql/src/Statements/examples/UselessRangeCheckGood.js rename to javascript/ql/src/Statements/examples/UselessComparisonTestGood.js diff --git a/javascript/ql/test/query-tests/Statements/UselessRangeCheck/UselessRangeCheck.expected b/javascript/ql/test/query-tests/Statements/UselessComparisonTest/UselessComparisonTest.expected similarity index 100% rename from javascript/ql/test/query-tests/Statements/UselessRangeCheck/UselessRangeCheck.expected rename to javascript/ql/test/query-tests/Statements/UselessComparisonTest/UselessComparisonTest.expected diff --git a/javascript/ql/test/query-tests/Statements/UselessComparisonTest/UselessComparisonTest.qlref b/javascript/ql/test/query-tests/Statements/UselessComparisonTest/UselessComparisonTest.qlref new file mode 100644 index 000000000000..ade7e7d0607e --- /dev/null +++ b/javascript/ql/test/query-tests/Statements/UselessComparisonTest/UselessComparisonTest.qlref @@ -0,0 +1 @@ +Statements/UselessComparisonTest.ql diff --git a/javascript/ql/test/query-tests/Statements/UselessRangeCheck/example.js b/javascript/ql/test/query-tests/Statements/UselessComparisonTest/example.js similarity index 100% rename from javascript/ql/test/query-tests/Statements/UselessRangeCheck/example.js rename to javascript/ql/test/query-tests/Statements/UselessComparisonTest/example.js diff --git a/javascript/ql/test/query-tests/Statements/UselessRangeCheck/exampleGood.js b/javascript/ql/test/query-tests/Statements/UselessComparisonTest/exampleGood.js similarity index 100% rename from javascript/ql/test/query-tests/Statements/UselessRangeCheck/exampleGood.js rename to javascript/ql/test/query-tests/Statements/UselessComparisonTest/exampleGood.js diff --git a/javascript/ql/test/query-tests/Statements/UselessRangeCheck/UselessRangeCheck.qlref b/javascript/ql/test/query-tests/Statements/UselessRangeCheck/UselessRangeCheck.qlref deleted file mode 100644 index f5d7a1ee7a40..000000000000 --- a/javascript/ql/test/query-tests/Statements/UselessRangeCheck/UselessRangeCheck.qlref +++ /dev/null @@ -1 +0,0 @@ -Statements/UselessRangeCheck.ql From 6d7ac885ec43092df6f561dfde253b568c6be3f0 Mon Sep 17 00:00:00 2001 From: Asger F Date: Tue, 20 Nov 2018 11:47:17 +0000 Subject: [PATCH 21/27] JS: add to correctness-more suite --- javascript/config/suites/javascript/correctness-more | 1 + 1 file changed, 1 insertion(+) diff --git a/javascript/config/suites/javascript/correctness-more b/javascript/config/suites/javascript/correctness-more index 10aa1dcf7967..2e57bcd7327b 100644 --- a/javascript/config/suites/javascript/correctness-more +++ b/javascript/config/suites/javascript/correctness-more @@ -15,3 +15,4 @@ + semmlecode-javascript-queries/Statements/ReturnOutsideFunction.ql: /Correctness/Statements + semmlecode-javascript-queries/Statements/SuspiciousUnusedLoopIterationVariable.ql: /Correctness/Statements + semmlecode-javascript-queries/Statements/UselessConditional.ql: /Correctness/Statements ++ semmlecode-javascript-queries/Statements/UselessComparisonTest.ql: /Correctness/Statements From 2c51f86f1ba6b671e43a76c8315b56adf2ae041a Mon Sep 17 00:00:00 2001 From: Asger F Date: Wed, 21 Nov 2018 16:42:37 +0000 Subject: [PATCH 22/27] JS: avoid joining on =0 --- javascript/ql/src/semmle/javascript/RangeAnalysis.qll | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll index 229d3bc97e4a..ec848209ac05 100644 --- a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll +++ b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll @@ -497,9 +497,9 @@ module RangeAnalysis { (x < 0 or x = 0 and sharpx = true) and (y > 0 or y = 0 and sharpy = false) and ( - x = 0 + x <= 0 and x >= 0 or - y = 0 + y <= 0 and y >= 0 or // If non-zero, check that the values are within a factor 16 of each other x.abs().bitShiftRight(4) < y.abs() and From 8fd3a417c253e96de1a89dce3e75f2f91bb89513 Mon Sep 17 00:00:00 2001 From: Asger F Date: Wed, 28 Nov 2018 09:47:50 +0000 Subject: [PATCH 23/27] JS: address comments --- javascript/ql/src/Statements/UselessComparisonTest.ql | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/javascript/ql/src/Statements/UselessComparisonTest.ql b/javascript/ql/src/Statements/UselessComparisonTest.ql index 6a4eef8c631e..419f02a000c3 100644 --- a/javascript/ql/src/Statements/UselessComparisonTest.ql +++ b/javascript/ql/src/Statements/UselessComparisonTest.ql @@ -4,7 +4,7 @@ * indicate faulty logic and dead code. * @kind problem * @problem.severity warning - * @id js/useless-range-check + * @id js/useless-comparison-test * @tags correctness * @precision high */ @@ -57,4 +57,4 @@ predicate isGuardNodeWithDeadCode(ConditionGuardNode guard) { from ConditionGuardNode guard where isGuardNodeWithDeadCode(guard) -select guard.getTest(), "The condition '" + guard.getTest() + "' is always " + guard.getOutcome().booleanNot() +select guard.getTest(), "The condition '" + guard.getTest() + "' is always " + guard.getOutcome().booleanNot() + "." From d69e584cc2b98a25ed9069f16566c43d4b043945 Mon Sep 17 00:00:00 2001 From: Asger F Date: Wed, 28 Nov 2018 10:21:43 +0000 Subject: [PATCH 24/27] JS: fix bug in foldedComparisonEdge --- javascript/ql/src/semmle/javascript/RangeAnalysis.qll | 4 ++-- javascript/ql/test/library-tests/RangeAnalysis/length.js | 3 +++ .../UselessComparisonTest/UselessComparisonTest.expected | 4 +++- .../query-tests/Statements/UselessComparisonTest/constant.js | 4 ++++ 4 files changed, 12 insertions(+), 3 deletions(-) create mode 100644 javascript/ql/test/library-tests/RangeAnalysis/length.js create mode 100644 javascript/ql/test/query-tests/Statements/UselessComparisonTest/constant.js diff --git a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll index ec848209ac05..28ccbf2d0caa 100644 --- a/javascript/ql/src/semmle/javascript/RangeAnalysis.qll +++ b/javascript/ql/src/semmle/javascript/RangeAnalysis.qll @@ -464,8 +464,8 @@ module RangeAnalysis { exists (DataFlow::Node k, int ksign, Bias bias, int avalue, int kvalue | comparisonEdge(cfg, a, asign, k, ksign, bias, sharp) and avalue = a.asExpr().getIntValue() * asign and - kvalue = b.asExpr().getIntValue() * bsign and - (avalue < kvalue + bias or sharp = true and avalue = kvalue + bias) and + kvalue = k.asExpr().getIntValue() * ksign and + (avalue > kvalue + bias or sharp = true and avalue = kvalue + bias) and a = b and asign = bsign and c = -1) diff --git a/javascript/ql/test/library-tests/RangeAnalysis/length.js b/javascript/ql/test/library-tests/RangeAnalysis/length.js new file mode 100644 index 000000000000..41835c245b17 --- /dev/null +++ b/javascript/ql/test/library-tests/RangeAnalysis/length.js @@ -0,0 +1,3 @@ +function f(arr) { + if (arr.length > 2) {} // OK +} \ No newline at end of file diff --git a/javascript/ql/test/query-tests/Statements/UselessComparisonTest/UselessComparisonTest.expected b/javascript/ql/test/query-tests/Statements/UselessComparisonTest/UselessComparisonTest.expected index bdf5055e767c..edb4ea205bc6 100644 --- a/javascript/ql/test/query-tests/Statements/UselessComparisonTest/UselessComparisonTest.expected +++ b/javascript/ql/test/query-tests/Statements/UselessComparisonTest/UselessComparisonTest.expected @@ -1 +1,3 @@ -| example.js:8:7:8:13 | i < end | The condition 'i < end' is always false | +| constant.js:2:7:2:11 | 1 > 2 | The condition '1 > 2' is always false. | +| constant.js:3:7:3:11 | 1 > 0 | The condition '1 > 0' is always true. | +| example.js:8:7:8:13 | i < end | The condition 'i < end' is always false. | diff --git a/javascript/ql/test/query-tests/Statements/UselessComparisonTest/constant.js b/javascript/ql/test/query-tests/Statements/UselessComparisonTest/constant.js new file mode 100644 index 000000000000..aa5ee0e1fb5b --- /dev/null +++ b/javascript/ql/test/query-tests/Statements/UselessComparisonTest/constant.js @@ -0,0 +1,4 @@ +function f() { + if (1 > 2) {} else {} // NOT OK - always false + if (1 > 0) {} else {} // NOT OK - always true +} From 959776b77537260cefd1d98b598a38cb95970cdc Mon Sep 17 00:00:00 2001 From: Asger F Date: Tue, 27 Nov 2018 16:36:09 +0000 Subject: [PATCH 25/27] JS: add test case --- .../ql/test/library-tests/RangeAnalysis/expressions.js | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 javascript/ql/test/library-tests/RangeAnalysis/expressions.js diff --git a/javascript/ql/test/library-tests/RangeAnalysis/expressions.js b/javascript/ql/test/library-tests/RangeAnalysis/expressions.js new file mode 100644 index 000000000000..ec25286b1153 --- /dev/null +++ b/javascript/ql/test/library-tests/RangeAnalysis/expressions.js @@ -0,0 +1,9 @@ +function f(arr) { + if (arr.length > 2) {} // OK + + let x = arr.length || 0; + if (x > 2) {} // OK + + let y = arr.length && 3; + if (y > 2) {} // OK +} From b2a82ae598b2f6f5f65bcb21db885eaf13baa450 Mon Sep 17 00:00:00 2001 From: Asger F Date: Thu, 15 Nov 2018 17:08:58 +0000 Subject: [PATCH 26/27] JS: add 1.20 change note --- change-notes/1.20/analysis-javascript.md | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 change-notes/1.20/analysis-javascript.md diff --git a/change-notes/1.20/analysis-javascript.md b/change-notes/1.20/analysis-javascript.md new file mode 100644 index 000000000000..3d8a0022f122 --- /dev/null +++ b/change-notes/1.20/analysis-javascript.md @@ -0,0 +1,24 @@ +# Improvements to JavaScript analysis + +## General improvements + +* TODO + +## New queries + +| **Query** | **Tags** | **Purpose** | +|-----------------------------------------------|------------------------------------------------------|-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------| +| Useless comparison test | correctness | Highlight code that is unreachable due to a numeric comparison that is always true or alway false. | + + +## Changes to existing queries + +| **Query** | **Expected impact** | **Change** | +|--------------------------------|----------------------------|----------------------------------------------| +| todo | | | + + +## Changes to QL libraries + +* TODO + From d4023fe95a0038c150c6c24fbff9cd2361546662 Mon Sep 17 00:00:00 2001 From: Asger F Date: Thu, 29 Nov 2018 11:37:38 +0000 Subject: [PATCH 27/27] JS: address review --- change-notes/1.20/analysis-javascript.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/change-notes/1.20/analysis-javascript.md b/change-notes/1.20/analysis-javascript.md index 3d8a0022f122..a4687323110f 100644 --- a/change-notes/1.20/analysis-javascript.md +++ b/change-notes/1.20/analysis-javascript.md @@ -8,7 +8,7 @@ | **Query** | **Tags** | **Purpose** | |-----------------------------------------------|------------------------------------------------------|-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------| -| Useless comparison test | correctness | Highlight code that is unreachable due to a numeric comparison that is always true or alway false. | +| Useless comparison test | correctness | Highlights code that is unreachable due to a numeric comparison that is always true or always false. | ## Changes to existing queries