From a0c849139c1d8ec29b4d5f67c03da44c6cdda554 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 1 May 2025 13:51:13 +0200 Subject: [PATCH 01/22] Java: Add guards-logic qltest with inline expectation. --- java/ql/test/library-tests/guards/Guards.java | 130 ++++++++++++++++++ .../guards/GuardsInline.expected | 56 ++++++++ .../test/library-tests/guards/GuardsInline.ql | 42 ++++++ .../library-tests/guards/GuardsInline.qlref | 2 + 4 files changed, 230 insertions(+) create mode 100644 java/ql/test/library-tests/guards/Guards.java create mode 100644 java/ql/test/library-tests/guards/GuardsInline.expected create mode 100644 java/ql/test/library-tests/guards/GuardsInline.ql create mode 100644 java/ql/test/library-tests/guards/GuardsInline.qlref diff --git a/java/ql/test/library-tests/guards/Guards.java b/java/ql/test/library-tests/guards/Guards.java new file mode 100644 index 000000000000..a524c237f130 --- /dev/null +++ b/java/ql/test/library-tests/guards/Guards.java @@ -0,0 +1,130 @@ +public class Guards { + static void chk() { } + + static boolean g(Object lbl) { return lbl.hashCode() > 10; } + + static void checkTrue(boolean b, String msg) { + if (!b) throw new Error(msg); + } + + static void checkFalse(boolean b, String msg) { + checkTrue(!b, msg); + } + + void t1(int[] a, String s) { + if (g("A")) { + chk(); // $ guarded=g(A):true + } else { + chk(); // $ guarded=g(A):false + } + + boolean b = g(1) ? g(2) : true; + if (b != false) { + chk(); // $ guarded=...?...:...:true guarded='b != false:true' guarded=b:true + } else { + chk(); // $ guarded=...?...:...:false guarded='b != false:false' guarded=b:false guarded=g(1):true guarded=g(2):false + } + int sz = a != null ? a.length : 0; + for (int i = 0; i < sz; i++) { + chk(); // $ guarded='a != null:true' guarded='i < sz:true' + int e = a[i]; + if (e > 2) break; + } + chk(); // nothing guards here + + if (g(3)) + s = "bar"; + switch (s) { + case "bar": + chk(); // $ guarded='s:match "bar"' + break; + case "foo": + chk(); // $ guarded='s:match "foo"' guarded=g(3):false + break; + default: + chk(); // $ guarded='s:non-match "bar"' guarded='s:non-match "foo"' guarded='s:match default' guarded=g(3):false + break; + } + + Object o = g(4) ? null : s; + if (o instanceof String) { + chk(); // $ guarded=...instanceof...:true guarded=g(4):false + } + } + + void t2() { + checkTrue(g(1), "A"); + checkFalse(g(2), "B"); + chk(); // $ guarded=checkTrue(A):true guarded=g(1):true guarded=checkFalse(B):false guarded=g(2):false + } + + void t3() { + boolean b = g(1) && (g(2) || g(3)); + if (b) { + chk(); // $ guarded=b:true guarded='g(...) && ... \|\| ...:true' guarded=g(1):true guarded='g(...) \|\| g(...):true' + } else { + chk(); // $ guarded=b:false guarded='g(...) && ... \|\| ...:false' + } + b = g(4) || !g(5); + if (b) { + chk(); // $ guarded=b:true guarded='g(...) \|\| !...:true' + } else { + chk(); // $ guarded=b:false guarded='g(...) \|\| !...:false' guarded=g(4):false guarded=!...:false guarded=g(5):true + } + } + + enum Val { + E1, + E2, + E3 + } + + void t4() { + Val x = null; // unique value + if (g(1)) x = Val.E1; // unique value + if (g(2)) x = Val.E2; + if (g("Alt2")) x = Val.E2; + if (g(3)) x = Val.E3; // unique value + if (x == null) + chk(); // $ guarded='x == null:true' guarded=g(3):false + switch (x) { + case E1: + chk(); // $ guarded='x:match E1' guarded=g(1):true guarded=g(3):false + break; + case E2: + chk(); // $ guarded='x:match E2' guarded=g(3):false + break; + case E3: + chk(); // $ guarded='x:match E3' guarded=g(3):true + break; + } + Object o = g(4) ? new Object() : null; + if (o == null) { + chk(); // $ guarded='o == null:true' guarded=g(4):false + } else { + chk(); // $ guarded='o == null:false' guarded=g(4):true + } + } + + void t5(String foo) { + String base = foo; + if (base == null) { + base = "/user"; + } + if (base.equals("/")) + chk(); // $ guarded=equals(/):true guarded='base == null:false' + } + + void t6() { + Object o = null; + if (g(1)) { + o = new Object(); + if (g(2)) { } + } + if (o != null) { + chk(); // $ guarded='o != null:true' + } else { + chk(); // $ guarded='o != null:false' guarded=g(1):false + } + } +} diff --git a/java/ql/test/library-tests/guards/GuardsInline.expected b/java/ql/test/library-tests/guards/GuardsInline.expected new file mode 100644 index 000000000000..665424c2f5b6 --- /dev/null +++ b/java/ql/test/library-tests/guards/GuardsInline.expected @@ -0,0 +1,56 @@ +| Guards.java:16:7:16:11 | chk(...) | g(A):true | +| Guards.java:18:7:18:11 | chk(...) | g(A):false | +| Guards.java:23:7:23:11 | chk(...) | 'b != false:true' | +| Guards.java:23:7:23:11 | chk(...) | ...?...:...:true | +| Guards.java:23:7:23:11 | chk(...) | b:true | +| Guards.java:25:7:25:11 | chk(...) | 'b != false:false' | +| Guards.java:25:7:25:11 | chk(...) | ...?...:...:false | +| Guards.java:25:7:25:11 | chk(...) | b:false | +| Guards.java:25:7:25:11 | chk(...) | g(1):true | +| Guards.java:25:7:25:11 | chk(...) | g(2):false | +| Guards.java:29:7:29:11 | chk(...) | 'a != null:true' | +| Guards.java:29:7:29:11 | chk(...) | 'i < sz:true' | +| Guards.java:39:9:39:13 | chk(...) | 's:match "bar"' | +| Guards.java:42:9:42:13 | chk(...) | 's:match "foo"' | +| Guards.java:42:9:42:13 | chk(...) | g(3):false | +| Guards.java:45:9:45:13 | chk(...) | 's:match default' | +| Guards.java:45:9:45:13 | chk(...) | 's:non-match "bar"' | +| Guards.java:45:9:45:13 | chk(...) | 's:non-match "foo"' | +| Guards.java:45:9:45:13 | chk(...) | g(3):false | +| Guards.java:51:7:51:11 | chk(...) | ...instanceof...:true | +| Guards.java:51:7:51:11 | chk(...) | g(4):false | +| Guards.java:58:5:58:9 | chk(...) | checkFalse(B):false | +| Guards.java:58:5:58:9 | chk(...) | checkTrue(A):true | +| Guards.java:58:5:58:9 | chk(...) | g(1):true | +| Guards.java:58:5:58:9 | chk(...) | g(2):false | +| Guards.java:64:7:64:11 | chk(...) | 'g(...) && ... \|\| ...:true' | +| Guards.java:64:7:64:11 | chk(...) | 'g(...) \|\| g(...):true' | +| Guards.java:64:7:64:11 | chk(...) | b:true | +| Guards.java:64:7:64:11 | chk(...) | g(1):true | +| Guards.java:66:7:66:11 | chk(...) | 'g(...) && ... \|\| ...:false' | +| Guards.java:66:7:66:11 | chk(...) | b:false | +| Guards.java:70:7:70:11 | chk(...) | 'g(...) \|\| !...:true' | +| Guards.java:70:7:70:11 | chk(...) | b:true | +| Guards.java:72:7:72:11 | chk(...) | !...:false | +| Guards.java:72:7:72:11 | chk(...) | 'g(...) \|\| !...:false' | +| Guards.java:72:7:72:11 | chk(...) | b:false | +| Guards.java:72:7:72:11 | chk(...) | g(4):false | +| Guards.java:72:7:72:11 | chk(...) | g(5):true | +| Guards.java:89:7:89:11 | chk(...) | 'x == null:true' | +| Guards.java:89:7:89:11 | chk(...) | g(3):false | +| Guards.java:92:9:92:13 | chk(...) | 'x:match E1' | +| Guards.java:92:9:92:13 | chk(...) | g(1):true | +| Guards.java:92:9:92:13 | chk(...) | g(3):false | +| Guards.java:95:9:95:13 | chk(...) | 'x:match E2' | +| Guards.java:95:9:95:13 | chk(...) | g(3):false | +| Guards.java:98:9:98:13 | chk(...) | 'x:match E3' | +| Guards.java:98:9:98:13 | chk(...) | g(3):true | +| Guards.java:103:7:103:11 | chk(...) | 'o == null:true' | +| Guards.java:103:7:103:11 | chk(...) | g(4):false | +| Guards.java:105:7:105:11 | chk(...) | 'o == null:false' | +| Guards.java:105:7:105:11 | chk(...) | g(4):true | +| Guards.java:115:7:115:11 | chk(...) | 'base == null:false' | +| Guards.java:115:7:115:11 | chk(...) | equals(/):true | +| Guards.java:125:7:125:11 | chk(...) | 'o != null:true' | +| Guards.java:127:7:127:11 | chk(...) | 'o != null:false' | +| Guards.java:127:7:127:11 | chk(...) | g(1):false | diff --git a/java/ql/test/library-tests/guards/GuardsInline.ql b/java/ql/test/library-tests/guards/GuardsInline.ql new file mode 100644 index 000000000000..54386f9777a9 --- /dev/null +++ b/java/ql/test/library-tests/guards/GuardsInline.ql @@ -0,0 +1,42 @@ +import java +import semmle.code.java.controlflow.Guards +import codeql.util.Boolean + +string ppGuard(Guard g, Boolean branch) { + exists(MethodCall mc, Literal s | + mc = g and + mc.getAnArgument() = s and + result = mc.getMethod().getName() + "(" + s.getValue() + ")" + ":" + branch + ) + or + exists(BinaryExpr bin | + bin = g and + result = "'" + bin.getLeftOperand() + bin.getOp() + bin.getRightOperand() + ":" + branch + "'" + ) + or + exists(SwitchCase cc, Expr s, string match, string value | + cc = g and + cc.getSelectorExpr() = s and + ( + cc.(ConstCase).getValue().toString() = value + or + cc instanceof DefaultCase and value = "default" + ) and + if branch = true then match = ":match " else match = ":non-match " + | + result = "'" + s.toString() + match + value + "'" + ) +} + +query predicate guarded(MethodCall mc, string guard) { + mc.getMethod().hasName("chk") and + exists(Guard g, BasicBlock bb, boolean branch | + g.controls(bb, branch) and + mc.getBasicBlock() = bb + | + guard = ppGuard(g, branch) + or + not exists(ppGuard(g, branch)) and + guard = g.toString() + ":" + branch + ) +} diff --git a/java/ql/test/library-tests/guards/GuardsInline.qlref b/java/ql/test/library-tests/guards/GuardsInline.qlref new file mode 100644 index 000000000000..a9492ac8f238 --- /dev/null +++ b/java/ql/test/library-tests/guards/GuardsInline.qlref @@ -0,0 +1,2 @@ +query: GuardsInline.ql +postprocess: utils/test/InlineExpectationsTestQuery.ql From 994c1f6427c0d65f2fc7fce5c8d70016e33647b1 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Fri, 2 May 2025 12:42:21 +0200 Subject: [PATCH 02/22] Java: Add hasInputFromBlock predicate in BaseSSA. --- java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll b/java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll index 874aca871832..ec56822d5852 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll @@ -372,5 +372,10 @@ class BaseSsaImplicitInit extends BaseSsaVariable instanceof Impl::WriteDefiniti /** An SSA phi node. */ class BaseSsaPhiNode extends BaseSsaVariable instanceof Impl::PhiNode { /** Gets an input to the phi node defining the SSA variable. */ - BaseSsaVariable getAPhiInput() { phiHasInputFromBlock(this, result, _) } + BaseSsaVariable getAPhiInput() { this.hasInputFromBlock(result, _) } + + /** Holds if `inp` is an input to the phi node along the edge originating in `bb`. */ + predicate hasInputFromBlock(BaseSsaVariable inp, BasicBlock bb) { + phiHasInputFromBlock(this, inp, bb) + } } From 1d75008eba73914b6f7cf3344fcc02fa7d9134aa Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Fri, 2 May 2025 14:44:28 +0200 Subject: [PATCH 03/22] Shared: Add a shared Guards library inspired by the Java and C# versions. --- .../controlflow/codeql/controlflow/Guards.qll | 792 ++++++++++++++++++ 1 file changed, 792 insertions(+) create mode 100644 shared/controlflow/codeql/controlflow/Guards.qll diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll new file mode 100644 index 000000000000..db5727fd7afb --- /dev/null +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -0,0 +1,792 @@ +/** + * Provides classes and predicates for determining "guard-controls" + * relationships. + * + * In their most general form, these relate a guard expression, a value, and a + * basic block, and state that execution of the basic block implies that + * control flow must have passed through the guard in order to reach the basic + * block, and when it did, the guard evaluated to the given value. + * + * For example, in `if (x == 0) { A }`, the guard `x == 0` evaluating to `true` + * controls the basic block `A`, in this case because the true branch dominates + * `A`, but more elaborate controls-relationships may also hold. + * For example, in + * ``` + * int sz = a != null ? a.length : 0; + * if (sz != 0) { + * // this block is controlled by: + * // sz != 0 evaluating to true + * // sz evaluating to not 0 + * // a.length evaluating to not 0 + * // a != null evaluating to true + * // a evaluating to not null + * } + * ``` + * + * The implementation is nested in two parameterized modules intended to + * facilitate multiple instantiations of the nested module with different + * precision levels + */ + +private import codeql.util.Boolean +private import codeql.util.Location + +signature module InputSig { + class SuccessorType { + /** Gets a textual representation of this successor type. */ + string toString(); + } + + class ConditionalSuccessor extends SuccessorType { + /** Gets the Boolean value of this successor. */ + boolean getValue(); + } + + class BooleanSuccessor extends ConditionalSuccessor; + + class NullnessSuccessor extends ConditionalSuccessor; + + /** A control flow node. */ + class ControlFlowNode { + /** Gets a textual representation of this control flow node. */ + string toString(); + + /** Gets the location of this control flow node. */ + Location getLocation(); + } + + /** + * A basic block, that is, a maximal straight-line sequence of control flow nodes + * without branches or joins. + */ + class BasicBlock { + /** Gets a textual representation of this basic block. */ + string toString(); + + /** Gets the `i`th node in this basic block. */ + ControlFlowNode getNode(int i); + + /** Gets the last control flow node in this basic block. */ + ControlFlowNode getLastNode(); + + /** Gets the length of this basic block. */ + int length(); + + /** Gets the location of this basic block. */ + Location getLocation(); + + BasicBlock getASuccessor(SuccessorType t); + + predicate dominates(BasicBlock bb); + + predicate strictlyDominates(BasicBlock bb); + } + + predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2); + + class Expr { + /** Gets a textual representation of this expression. */ + string toString(); + + /** Gets the location of this expression. */ + Location getLocation(); + + /** Gets the associated control flow node. */ + ControlFlowNode getControlFlowNode(); + + /** Gets the basic block containing this expression. */ + BasicBlock getBasicBlock(); + } + + class ConstantValue { + /** Gets a textual representation of this constant value. */ + string toString(); + } + + class ConstantExpr extends Expr { + predicate isNull(); + + boolean asBooleanValue(); + + int asIntegerValue(); + + ConstantValue asConstantValue(); + } + + class NonNullExpr extends Expr; + + class Case { + /** Gets a textual representation of this switch case. */ + string toString(); + + Location getLocation(); + + Expr getSwitchExpr(); + + predicate isDefaultCase(); + + ConstantExpr asConstantCase(); + + predicate matchEdge(BasicBlock bb1, BasicBlock bb2); + + predicate nonMatchEdge(BasicBlock bb1, BasicBlock bb2); + } + + class AndExpr extends Expr { + /** Gets an operand of this expression. */ + Expr getAnOperand(); + } + + class OrExpr extends Expr { + /** Gets an operand of this expression. */ + Expr getAnOperand(); + } + + class NotExpr extends Expr { + /** Gets the operand of this expression. */ + Expr getOperand(); + } + + /** + * An expression that has the same value as a specific sub-expression. + * + * For example, in Java, the assignment `x = rhs` has the same value as `rhs`. + */ + class IdExpr extends Expr { + Expr getEqualChildExpr(); + } + + class EqualityTest extends Expr { + /** Gets an operand of this expression. */ + Expr getAnOperand(); + + /** Gets a boolean indicating whether this test is equality (true) or inequality (false). */ + boolean polarity(); + } + + class ConditionalExpr extends Expr { + /** Gets the condition of this expression. */ + Expr getCondition(); + + /** Gets the true branch of this expression. */ + Expr getThen(); + + /** Gets the false branch of this expression. */ + Expr getElse(); + } +} + +module Make Input> { + private import Input + + private newtype TAbstractSingleValue = + TValueNull() or + TValueTrue() or + TValueInt(int i) { exists(ConstantExpr c | c.asIntegerValue() = i) or i = 0 } or + TValueConstant(ConstantValue c) { exists(ConstantExpr ce | ce.asConstantValue() = c) } + + private newtype TGuardValue = + TValue(TAbstractSingleValue val, Boolean isVal) or + TCaseMatch(Case c, Boolean match) + + private class AbstractSingleValue extends TAbstractSingleValue { + /** Gets a textual representation of this value. */ + string toString() { + result = "null" and this instanceof TValueNull + or + result = "true" and this instanceof TValueTrue + or + exists(int i | result = i.toString() and this = TValueInt(i)) + or + exists(ConstantValue c | result = c.toString() and this = TValueConstant(c)) + } + } + + /** An abstract value that a `Guard` may evaluate to. */ + class GuardValue extends TGuardValue { + /** + * Gets the dual value. Examples of dual values include: + * - null vs. not null + * - true vs. false + * - evaluating to a specific value vs. evaluating to any other value + * - matching a specific case vs. not matching that case + */ + GuardValue getDualValue() { + exists(AbstractSingleValue val, boolean isVal | + this = TValue(val, isVal) and + result = TValue(val, isVal.booleanNot()) + ) + or + exists(Case c, boolean match | + this = TCaseMatch(c, match) and + result = TCaseMatch(c, match.booleanNot()) + ) + } + + /** Holds if this value represents `null`. */ + predicate isNullValue() { this = TValue(TValueNull(), true) } + + /** Gets the integer that this value represents, if any. */ + int asIntValue() { this = TValue(TValueInt(result), true) } + + /** Gets the boolean that this value represents, if any. */ + boolean asBooleanValue() { this = TValue(TValueTrue(), result) } + + /** Gets the constant that this value represents, if any. */ + ConstantValue asConstantValue() { this = TValue(TValueConstant(result), true) } + + /** Gets a textual representation of this value. */ + string toString() { + result = this.asBooleanValue().toString() + or + exists(AbstractSingleValue val | not val instanceof TValueTrue | + this = TValue(val, true) and result = val.toString() + or + this = TValue(val, false) and result = "not " + val.toString() + ) + or + exists(Case c, boolean match, string s | this = TCaseMatch(c, match) | + ( + exists(ConstantExpr ce | c.asConstantCase() = ce and s = ce.toString()) + or + not exists(c.asConstantCase()) and s = c.toString() + ) and + ( + match = true and result = "match " + s + or + match = false and result = "non-match " + s + ) + ) + } + } + + bindingset[a, b] + pragma[inline_late] + private predicate disjointValues(GuardValue a, GuardValue b) { + a = b.getDualValue() + or + exists(AbstractSingleValue a1, AbstractSingleValue b1 | + a = TValue(a1, true) and + b = TValue(b1, true) and + a1 != b1 + ) + } + + private predicate constantHasValue(ConstantExpr c, GuardValue v) { + c.isNull() and v = TValue(TValueNull(), true) + or + v = TValue(TValueTrue(), c.asBooleanValue()) + or + v = TValue(TValueInt(c.asIntegerValue()), true) + or + v = TValue(TValueConstant(c.asConstantValue()), true) + } + + private predicate exprHasValue(Expr e, GuardValue v) { + constantHasValue(e, v) + or + e instanceof NonNullExpr and v = TValue(TValueNull(), false) + } + + private predicate branchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue v) { + exists(ConditionalSuccessor s | + bb1.getASuccessor(s) = bb2 and + exists(AbstractSingleValue val | + s instanceof NullnessSuccessor and val = TValueNull() + or + s instanceof BooleanSuccessor and val = TValueTrue() + | + v = TValue(val, s.getValue()) + ) + ) + or + exists(Case c | + v = TCaseMatch(c, true) and + c.matchEdge(bb1, bb2) + or + v = TCaseMatch(c, false) and + c.nonMatchEdge(bb1, bb2) + ) + } + + pragma[nomagic] + private predicate eqtestHasOperands(EqualityTest eqtest, Expr e1, Expr e2, boolean polarity) { + eqtest.getAnOperand() = e1 and + eqtest.getAnOperand() = e2 and + e1 != e2 and + eqtest.polarity() = polarity + } + + private predicate caseGuard(PreGuard g, Case c, Expr switchExpr) { + g.hasValueBranchEdge(_, _, TCaseMatch(c, _)) and + switchExpr = c.getSwitchExpr() + } + + private predicate constcaseEquality(PreGuard g, Expr e1, ConstantExpr e2, GuardValue eqval) { + exists(Case c | + caseGuard(g, c, e1) and + c.asConstantCase() = e2 and + eqval = TCaseMatch(c, true) + ) + } + + final private class ExprFinal = Expr; + + /** + * A guard. This may be any expression whose value determines subsequent + * control flow. + */ + final class PreGuard extends ExprFinal { + /** + * Holds if this guard is the last node in `bb1` and that its successor is + * `bb2` exactly when evaluating to `v`. + */ + predicate hasValueBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue v) { + bb1.getLastNode() = this.getControlFlowNode() and + branchEdge(bb1, bb2, v) + } + + /** + * Holds if this guard evaluating to `v` directly controls the basic block `bb`. + * + * That is, `bb` is dominated by the `v`-successor edge of this guard. + */ + predicate directlyValueControls(BasicBlock bb, GuardValue v) { + exists(BasicBlock guard, BasicBlock succ | + this.hasValueBranchEdge(guard, succ, v) and + dominatingEdge(guard, succ) and + succ.dominates(bb) + ) + } + + /** + * Holds if this guard is the last node in `bb1` and that its successor is + * `bb2` exactly when evaluating to `branch`. + */ + predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { + this.hasValueBranchEdge(bb1, bb2, TValue(TValueTrue(), branch)) + } + + /** + * Holds if this guard evaluating to `branch` directly controls the basic + * block `bb`. + * + * That is, `bb` is dominated by the `branch`-successor edge of this guard. + */ + predicate directlyControls(BasicBlock bb, boolean branch) { + this.directlyValueControls(bb, TValue(TValueTrue(), branch)) + } + + /** + * Holds if this guard tests equality between `e1` and `e2` upon evaluating + * to `eqval`. + */ + predicate isEquality(Expr e1, Expr e2, GuardValue eqval) { + eqtestHasOperands(this, e1, e2, eqval.asBooleanValue()) + or + constcaseEquality(this, e1, e2, eqval) + or + constcaseEquality(this, e2, e1, eqval) + } + } + + private Expr getBranchExpr(ConditionalExpr cond, boolean branch) { + branch = true and result = cond.getThen() + or + branch = false and result = cond.getElse() + } + + bindingset[g1, v1] + pragma[inline_late] + private predicate unboundBaseImpliesStep(PreGuard g1, GuardValue v1, PreGuard g2, GuardValue v2) { + g1.(IdExpr).getEqualChildExpr() = g2 and v1 = v2 + or + exists(ConditionalExpr cond, boolean branch, Expr e, GuardValue ev | + cond = g1 and + e = getBranchExpr(cond, branch) and + exprHasValue(e, ev) and + disjointValues(v1, ev) + | + // g1 === g2 ? e : ...; + // g1 === g2 ? ... : e; + g2 = cond.getCondition() and + v2 = TValue(TValueTrue(), branch.booleanNot()) + or + // g1 === ... ? g2 : e + // g1 === ... ? e : g2 + g2 = getBranchExpr(cond, branch.booleanNot()) and + v2 = v1 and + not exprHasValue(g2, v2) // disregard trivial guard + ) + } + + private predicate baseImpliesStep(PreGuard g1, GuardValue v1, PreGuard g2, GuardValue v2) { + g1.(AndExpr).getAnOperand() = g2 and v1 = TValue(TValueTrue(), true) and v2 = v1 + or + g1.(OrExpr).getAnOperand() = g2 and v1 = TValue(TValueTrue(), false) and v2 = v1 + or + g1.(NotExpr).getOperand() = g2 and v1.asBooleanValue().booleanNot() = v2.asBooleanValue() + or + exists(GuardValue eqval, ConstantExpr constant, GuardValue cv | + g1.isEquality(g2, constant, eqval) and + constantHasValue(constant, cv) + | + v1 = eqval and v2 = cv + or + v1 = eqval.getDualValue() and v2 = cv.getDualValue() + ) + or + exists(NonNullExpr nonnull | + eqtestHasOperands(g1, g2, nonnull, v1.asBooleanValue()) and + v2 = TValue(TValueNull(), false) + ) + or + exists(Case c1, Case c2, Expr switchExpr | + caseGuard(g1, c1, switchExpr) and + v1 = TCaseMatch(c1, true) and + c1.isDefaultCase() and + caseGuard(g2, c2, switchExpr) and + v2 = TCaseMatch(c2, false) and + c1 != c2 + ) + } + + signature module LogicInputSig { + class SsaDefinition { + /** Gets the basic block to which this SSA definition belongs. */ + BasicBlock getBasicBlock(); + + Expr getARead(); + } + + class SsaWriteDefinition extends SsaDefinition { + Expr getDefinition(); + } + + class SsaPhiNode extends SsaDefinition { + /** Holds if `inp` is an input to the phi node along the edge originating in `bb`. */ + predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb); + } + + /** + * Holds if `guard` evaluating to `val` ensures that: + * `e <= k` when `upper = true` + * `e >= k` when `upper = false` + */ + default predicate rangeGuard(PreGuard guard, GuardValue val, Expr e, int k, boolean upper) { + none() + } + + /** + * Holds if `guard` evaluating to `val` ensures that: + * `e == null` when `isNull = true` + * `e != null` when `isNull = false` + */ + default predicate additionalNullCheck(PreGuard guard, GuardValue val, Expr e, boolean isNull) { + none() + } + } + + module Logic { + private import LogicInput + + private predicate guardControlsPhiBranch( + Guard guard, GuardValue v, SsaPhiNode phi, Expr input, BasicBlock bbInput, BasicBlock bbPhi + ) { + exists(SsaWriteDefinition inp | + phi.hasInputFromBlock(inp, bbInput) and + phi.getBasicBlock() = bbPhi and + inp.getDefinition() = input and + guard.directlyValueControls(bbInput, v) and + guard.getBasicBlock().strictlyDominates(bbPhi) and + not guard.directlyValueControls(bbPhi, _) + ) + } + + /** + * Holds if `phi` takes `input` exactly when `guard` is `v`. That is, + * `guard == v` directly controls `input` and `guard == v.getDualValue()` + * directly controls all other inputs to `phi`. + * + * This makes `phi` similar to the conditional `phi = guard==v ? input : ...`. + */ + private predicate guardDeterminesPhiInput(Guard guard, GuardValue v, SsaPhiNode phi, Expr input) { + exists(GuardValue dv, BasicBlock bbInput, BasicBlock bbPhi | + guardControlsPhiBranch(guard, v, phi, input, bbInput, bbPhi) and + dv = v.getDualValue() and + forall(BasicBlock other | phi.hasInputFromBlock(_, other) and other != bbInput | + guard.directlyValueControls(other, dv) + or + guard.hasValueBranchEdge(other, bbPhi, dv) + ) + ) + } + + pragma[nomagic] + private predicate guardChecksEqualVars( + Guard guard, SsaDefinition v1, SsaDefinition v2, boolean branch + ) { + eqtestHasOperands(guard, v1.getARead(), v2.getARead(), branch) + } + + private predicate guardReadsSsaVar(Guard guard, SsaDefinition def) { + def.getARead() = guard + or + exists(Guard eqtest, SsaDefinition other, boolean branch | + guardChecksEqualVars(eqtest, def, other, branch) and + other.getARead() = guard and + eqtest.directlyControls(guard.getBasicBlock(), branch) + ) + } + + private predicate valueStep(Expr e1, Expr e2) { + e2.(ConditionalExpr).getThen() = e1 or + e2.(ConditionalExpr).getElse() = e1 or + e2.(IdExpr).getEqualChildExpr() = e1 + } + + /** + * Gets a sub-expression of `e` whose value can flow to `e` through + * `valueStep`s + */ + private Expr possibleValue(Expr e) { + result = possibleValue(any(Expr e1 | valueStep(e1, e))) + or + result = e and not valueStep(_, e) + } + + /** + * Gets an ultimate definition of `v` that is not itself a phi node. The + * boolean `fromBackEdge` indicates whether the flow from `result` to `v` goes + * through a back edge. + */ + private SsaDefinition getADefinition(SsaDefinition v, boolean fromBackEdge) { + result = v and not v instanceof SsaPhiNode and fromBackEdge = false + or + exists(SsaDefinition inp, BasicBlock bb, boolean fbe | + v.(SsaPhiNode).hasInputFromBlock(inp, bb) and + result = getADefinition(inp, fbe) and + (if v.getBasicBlock().dominates(bb) then fromBackEdge = true else fromBackEdge = fbe) + ) + } + + /** + * Holds if `v` can have a value that is not representable as an `GuardValue`. + */ + private predicate hasPossibleUnknownValue(SsaDefinition v) { + exists(SsaDefinition def | def = getADefinition(v, _) | + not exists(def.(SsaWriteDefinition).getDefinition()) + or + exists(Expr e | e = possibleValue(def.(SsaWriteDefinition).getDefinition()) | + not constantHasValue(e, _) + ) + ) + } + + /** + * Holds if `e` equals `k` and may be assigned to `v`. The boolean + * `fromBackEdge` indicates whether the flow from `e` to `v` goes through a + * back edge. + */ + private predicate possibleValue(SsaDefinition v, boolean fromBackEdge, Expr e, GuardValue k) { + not hasPossibleUnknownValue(v) and + exists(SsaWriteDefinition def | + def = getADefinition(v, fromBackEdge) and + e = possibleValue(def.getDefinition()) and + constantHasValue(e, k) + ) + } + + /** + * Holds if `e` equals `k` and may be assigned to `v` without going through + * back edges, and all other possible ultimate definitions of `v` are different + * from `k`. The trivial case where `v` is an `SsaWriteDefinition` with `e` as + * the only possible value is excluded. + */ + private predicate uniqueValue(SsaDefinition v, Expr e, GuardValue k) { + possibleValue(v, false, e, k) and + forex(Expr other, GuardValue otherval | possibleValue(v, _, other, otherval) and other != e | + disjointValues(otherval, k) + ) + } + + /** + * Holds if `phi` has exactly two inputs, `def1` and `e2`, and that `def1` + * does not come from a back-edge into `phi`. + */ + private predicate phiWithTwoInputs(SsaPhiNode phi, SsaDefinition def1, Expr e2) { + exists(SsaWriteDefinition def2, BasicBlock bb1 | + 2 = strictcount(SsaDefinition inp, BasicBlock bb | phi.hasInputFromBlock(inp, bb)) and + phi.hasInputFromBlock(def1, bb1) and + phi.hasInputFromBlock(def2, _) and + def1 != def2 and + not phi.getBasicBlock().dominates(bb1) and + def2.getDefinition() = e2 + ) + } + + /** Holds if `e` may take the value `k` */ + private predicate relevantInt(Expr e, int k) { + e.(ConstantExpr).asIntegerValue() = k + or + relevantInt(any(Expr e1 | valueStep(e1, e)), k) + or + exists(SsaDefinition def | + guardReadsSsaVar(e, def) and + relevantInt(getADefinition(def, _).(SsaWriteDefinition).getDefinition(), k) + ) + } + + private predicate impliesStep(Guard g1, GuardValue v1, Guard g2, GuardValue v2) { + baseImpliesStep(g1, v1, g2, v2) + or + exists(SsaDefinition def, Expr e | + // If `def = g2 ? v1 : ...` and all other assignments to `def` are different from + // `v1` then a guard proving `def == v1` ensures that `g2` evaluates to `v2`. + uniqueValue(def, e, v1) and + guardReadsSsaVar(g1, def) and + g2.directlyValueControls(e.getBasicBlock(), v2) and + not g2.directlyValueControls(g1.getBasicBlock(), v2) + ) + or + exists(int k1, int k2, boolean upper | + rangeGuard(g1, v1, g2, k1, upper) and + relevantInt(g2, k2) and + v2 = TValue(TValueInt(k2), false) + | + upper = true and k1 < k2 // g2 <= k1 < k2 ==> g2 != k2 + or + upper = false and k1 > k2 // g2 >= k1 > k2 ==> g2 != k2 + ) + or + exists(boolean isNull | + additionalNullCheck(g1, v1, g2, isNull) and + v2 = TValue(TValueNull(), isNull) + ) + } + + bindingset[g1, v1] + pragma[inline_late] + private predicate unboundImpliesStep(Guard g1, GuardValue v1, Guard g2, GuardValue v2) { + unboundBaseImpliesStep(g1, v1, g2, v2) + } + + bindingset[def1, v1] + pragma[inline_late] + private predicate impliesStepSsaGuard(SsaDefinition def1, GuardValue v1, Guard g2, GuardValue v2) { + def1.(SsaWriteDefinition).getDefinition() = g2 and + v1 = v2 and + not exprHasValue(g2, v2) // disregard trivial guard + or + exists(Expr e, GuardValue ev | + guardDeterminesPhiInput(g2, v2.getDualValue(), def1, e) and + exprHasValue(e, ev) and + disjointValues(v1, ev) + ) + } + + bindingset[def1, v] + pragma[inline_late] + private predicate impliesStepSsa(SsaDefinition def1, GuardValue v, SsaDefinition def2) { + exists(Expr e, GuardValue ev | + phiWithTwoInputs(def1, def2, e) and + exprHasValue(e, ev) and + disjointValues(v, ev) + ) + } + + pragma[nomagic] + private predicate guardControlsBranchEdge( + Guard guard, BasicBlock bb1, BasicBlock bb2, GuardValue v + ) { + guard.hasValueBranchEdge(bb1, bb2, v) + or + exists(Guard g0, GuardValue v0 | + guardControlsBranchEdge(g0, bb1, bb2, v0) and + impliesStep(g0, v0, guard, v) + ) + or + exists(Guard g0, GuardValue v0 | + guardControlsBranchEdge(g0, bb1, bb2, v0) and + unboundImpliesStep(g0, v0, guard, v) + ) + or + exists(SsaDefinition def0, GuardValue v0 | + ssaControlsBranchEdge(def0, bb1, bb2, v0) and + impliesStepSsaGuard(def0, v0, guard, v) + ) + } + + pragma[nomagic] + private predicate ssaControlsBranchEdge( + SsaDefinition def, BasicBlock bb1, BasicBlock bb2, GuardValue v + ) { + exists(Guard g0 | + guardControlsBranchEdge(g0, bb1, bb2, v) and + guardReadsSsaVar(g0, def) + ) + or + exists(SsaDefinition def0 | + ssaControlsBranchEdge(def0, bb1, bb2, v) and + impliesStepSsa(def0, v, def) + ) + } + + /** + * A guard. This may be any expression whose value determines subsequent + * control flow. + */ + final class Guard extends PreGuard { + /** + * Holds if this guard evaluating to `v` controls the control-flow branch + * edge from `bb1` to `bb2`. That is, following the edge from `bb1` to + * `bb2` implies that this guard evaluated to `v`. + * + * Note that this goes beyond mere control-flow graph dominance, as it + * also considers additional logical reasoning. + */ + predicate valueControlsBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue v) { + guardControlsBranchEdge(this, bb1, bb2, v) + } + + /** + * Holds if this guard evaluating to `v` controls the basic block `bb`. + * That is, execution of `bb` implies that this guard evaluated to `v`. + * + * Note that this goes beyond mere control-flow graph dominance, as it + * also considers additional logical reasoning. + */ + predicate valueControls(BasicBlock bb, GuardValue v) { + exists(BasicBlock guard, BasicBlock succ | + this.valueControlsBranchEdge(guard, succ, v) and + dominatingEdge(guard, succ) and + succ.dominates(bb) + ) + } + + /** + * Holds if this guard evaluating to `branch` controls the control-flow + * branch edge from `bb1` to `bb2`. That is, following the edge from + * `bb1` to `bb2` implies that this guard evaluated to `branch`. + * + * Note that this goes beyond mere control-flow graph dominance, as it + * also considers additional logical reasoning. + */ + predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { + this.valueControlsBranchEdge(bb1, bb2, TValue(TValueTrue(), branch)) + } + + /** + * Holds if this guard evaluating to `branch` controls the basic block + * `bb`. That is, execution of `bb` implies that this guard evaluated to + * `branch`. + * + * Note that this goes beyond mere control-flow graph dominance, as it + * also considers additional logical reasoning. + */ + predicate controls(BasicBlock bb, boolean branch) { + this.valueControls(bb, TValue(TValueTrue(), branch)) + } + } + } +} From 14b87f97b96e83a9005c7b4d6d88c7e20227f54a Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 13 May 2025 15:57:39 +0200 Subject: [PATCH 04/22] Shared: Extend the shared Guards library with support for custom wrappers. --- .../controlflow/codeql/controlflow/Guards.qll | 203 +++++++++++++++--- 1 file changed, 175 insertions(+), 28 deletions(-) diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index db5727fd7afb..7d9b9fe283fa 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -485,6 +485,17 @@ module Make Input> { default predicate additionalNullCheck(PreGuard guard, GuardValue val, Expr e, boolean isNull) { none() } + + /** + * Holds if the assumption that `g1` has been evaluated to `v1` implies that + * `g2` has been evaluated to `v2`, that is, the evaluation of `g2` to `v2` + * dominates the evaluation of `g1` to `v1`. + * + * This predicate can be instantiated with `CustomGuard<..>::additionalImpliesStep`. + */ + default predicate additionalImpliesStep(PreGuard g1, GuardValue v1, PreGuard g2, GuardValue v2) { + none() + } } module Logic { @@ -695,41 +706,177 @@ module Make Input> { ) } - pragma[nomagic] + private signature predicate baseGuardValueSig(Guard guard, GuardValue v); + + /** + * Calculates the transitive closure of all the guard implication steps + * starting from a given set of base cases. + */ + private module ImpliesTC { + pragma[nomagic] + predicate guardControls(Guard guard, GuardValue v, Guard tgtGuard, GuardValue tgtVal) { + baseGuardValue(tgtGuard, tgtVal) and + guard = tgtGuard and + v = tgtVal + or + exists(Guard g0, GuardValue v0 | + guardControls(g0, v0, tgtGuard, tgtVal) and + impliesStep(g0, v0, guard, v) + ) + or + exists(Guard g0, GuardValue v0 | + guardControls(g0, v0, tgtGuard, tgtVal) and + unboundImpliesStep(g0, v0, guard, v) + ) + or + exists(SsaDefinition def0, GuardValue v0 | + ssaControls(def0, v0, tgtGuard, tgtVal) and + impliesStepSsaGuard(def0, v0, guard, v) + ) + or + exists(Guard g0, GuardValue v0 | + guardControls(g0, v0, tgtGuard, tgtVal) and + additionalImpliesStep(g0, v0, guard, v) + ) + } + + pragma[nomagic] + predicate ssaControls(SsaDefinition def, GuardValue v, Guard tgtGuard, GuardValue tgtVal) { + exists(Guard g0 | + guardControls(g0, v, tgtGuard, tgtVal) and + guardReadsSsaVar(g0, def) + ) + or + exists(SsaDefinition def0 | + ssaControls(def0, v, tgtGuard, tgtVal) and + impliesStepSsa(def0, v, def) + ) + } + } + + private predicate hasAValueBranchEdge(Guard guard, GuardValue v) { + guard.hasValueBranchEdge(_, _, v) + } + + private module BranchImplies = ImpliesTC; + private predicate guardControlsBranchEdge( Guard guard, BasicBlock bb1, BasicBlock bb2, GuardValue v ) { - guard.hasValueBranchEdge(bb1, bb2, v) - or exists(Guard g0, GuardValue v0 | - guardControlsBranchEdge(g0, bb1, bb2, v0) and - impliesStep(g0, v0, guard, v) - ) - or - exists(Guard g0, GuardValue v0 | - guardControlsBranchEdge(g0, bb1, bb2, v0) and - unboundImpliesStep(g0, v0, guard, v) - ) - or - exists(SsaDefinition def0, GuardValue v0 | - ssaControlsBranchEdge(def0, bb1, bb2, v0) and - impliesStepSsaGuard(def0, v0, guard, v) + g0.hasValueBranchEdge(bb1, bb2, v0) and + BranchImplies::guardControls(guard, v, g0, v0) ) } - pragma[nomagic] - private predicate ssaControlsBranchEdge( - SsaDefinition def, BasicBlock bb1, BasicBlock bb2, GuardValue v - ) { - exists(Guard g0 | - guardControlsBranchEdge(g0, bb1, bb2, v) and - guardReadsSsaVar(g0, def) - ) - or - exists(SsaDefinition def0 | - ssaControlsBranchEdge(def0, bb1, bb2, v) and - impliesStepSsa(def0, v, def) - ) + signature module CustomGuardInputSig { + class ParameterPosition { + /** Gets a textual representation of this element. */ + bindingset[this] + string toString(); + } + + class ArgumentPosition { + /** Gets a textual representation of this element. */ + bindingset[this] + string toString(); + } + + /** + * Holds if the parameter position `ppos` matches the argument position + * `apos`. + */ + predicate parameterMatch(ParameterPosition ppos, ArgumentPosition apos); + + /** A non-overridable method with a boolean return value. */ + class BooleanMethod { + SsaDefinition getParameter(ParameterPosition ppos); + + Expr getAReturnExpr(); + } + + class BooleanMethodCall extends Expr { + BooleanMethod getMethod(); + + Expr getArgument(ArgumentPosition apos); + } + } + + /** + * Provides an implementation of guard implication logic for custom + * wrappers. This can be used to instantiate the `additionalImpliesStep` + * predicate. + */ + module CustomGuard { + private import CustomGuardInput + + private class ReturnExpr extends ExprFinal { + ReturnExpr() { any(BooleanMethod m).getAReturnExpr() = this } + + pragma[nomagic] + BasicBlock getBasicBlock() { result = super.getBasicBlock() } + } + + private predicate booleanReturnGuard(Guard guard, GuardValue val) { + guard instanceof ReturnExpr and exists(val.asBooleanValue()) + } + + private module ReturnImplies = ImpliesTC; + + /** + * Holds if `ret` is a return expression in a non-overridable method that + * on a return value of `retval` allows the conclusion that the `ppos`th + * parameter has the value `val`. + */ + private predicate validReturnInCustomGuard( + ReturnExpr ret, ParameterPosition ppos, boolean retval, GuardValue val + ) { + exists(BooleanMethod m, SsaDefinition param | + m.getAReturnExpr() = ret and + m.getParameter(ppos) = param and + not val instanceof TCaseMatch + | + exists(Guard g0, GuardValue v0 | + g0.directlyValueControls(ret.getBasicBlock(), v0) and + BranchImplies::ssaControls(param, val, g0, v0) and + retval = [true, false] + ) + or + ReturnImplies::ssaControls(param, val, ret, + any(GuardValue r | r.asBooleanValue() = retval)) + ) + } + + /** + * Gets a non-overridable method with a boolean return value that performs a check + * on the `ppos`th parameter. A return value equal to `retval` allows us to conclude + * that the argument has the value `val`. + */ + private BooleanMethod customGuard(ParameterPosition ppos, boolean retval, GuardValue val) { + forex(ReturnExpr ret | + result.getAReturnExpr() = ret and + not ret.(ConstantExpr).asBooleanValue() = retval.booleanNot() + | + validReturnInCustomGuard(ret, ppos, retval, val) + ) + } + + /** + * Holds if the assumption that `g1` has been evaluated to `v1` implies that + * `g2` has been evaluated to `v2`, that is, the evaluation of `g2` to `v2` + * dominates the evaluation of `g1` to `v1`. + * + * This predicate covers the implication steps that arise from calls to + * custom guard wrappers. + */ + predicate additionalImpliesStep(PreGuard g1, GuardValue v1, PreGuard g2, GuardValue v2) { + exists(BooleanMethodCall call, ParameterPosition ppos, ArgumentPosition apos | + g1 = call and + call.getMethod() = customGuard(ppos, v1.asBooleanValue(), v2) and + call.getArgument(apos) = g2 and + parameterMatch(pragma[only_bind_out](ppos), pragma[only_bind_out](apos)) + ) + } } /** From 16c5b57953fef53fe94e3d1585c62648f55df5c2 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 15 May 2025 16:07:47 +0200 Subject: [PATCH 05/22] Shared: Extend the shared Guards library with support for exception branch points. --- .../controlflow/codeql/controlflow/Guards.qll | 34 +++++++++++++++++-- 1 file changed, 32 insertions(+), 2 deletions(-) diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index 7d9b9fe283fa..62308a6a105f 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -37,6 +37,8 @@ signature module InputSig { string toString(); } + class ExceptionSuccessor extends SuccessorType; + class ConditionalSuccessor extends SuccessorType { /** Gets the Boolean value of this successor. */ boolean getValue(); @@ -187,7 +189,8 @@ module Make Input> { private newtype TGuardValue = TValue(TAbstractSingleValue val, Boolean isVal) or - TCaseMatch(Case c, Boolean match) + TCaseMatch(Case c, Boolean match) or + TException(Boolean throws) private class AbstractSingleValue extends TAbstractSingleValue { /** Gets a textual representation of this value. */ @@ -221,6 +224,11 @@ module Make Input> { this = TCaseMatch(c, match) and result = TCaseMatch(c, match.booleanNot()) ) + or + exists(boolean throws | + this = TException(throws) and + result = TException(throws.booleanNot()) + ) } /** Holds if this value represents `null`. */ @@ -235,6 +243,9 @@ module Make Input> { /** Gets the constant that this value represents, if any. */ ConstantValue asConstantValue() { this = TValue(TValueConstant(result), true) } + /** Holds if this value represents throwing an exception. */ + predicate isThrowsException() { this = TException(true) } + /** Gets a textual representation of this value. */ string toString() { result = this.asBooleanValue().toString() @@ -257,6 +268,12 @@ module Make Input> { match = false and result = "non-match " + s ) ) + or + exists(boolean throws | this = TException(throws) | + throws = true and result = "exception" + or + throws = false and result = "no exception" + ) } } @@ -288,6 +305,15 @@ module Make Input> { e instanceof NonNullExpr and v = TValue(TValueNull(), false) } + private predicate exceptionBranchPoint(BasicBlock bb1, BasicBlock normalSucc, BasicBlock excSucc) { + exists(SuccessorType norm, ExceptionSuccessor exc | + bb1.getASuccessor(norm) = normalSucc and + bb1.getASuccessor(exc) = excSucc and + normalSucc != excSucc and + not norm instanceof ExceptionSuccessor + ) + } + private predicate branchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue v) { exists(ConditionalSuccessor s | bb1.getASuccessor(s) = bb2 and @@ -307,6 +333,10 @@ module Make Input> { v = TCaseMatch(c, false) and c.nonMatchEdge(bb1, bb2) ) + or + exceptionBranchPoint(bb1, bb2, _) and v = TException(false) + or + exceptionBranchPoint(bb1, _, bb2) and v = TException(true) } pragma[nomagic] @@ -399,7 +429,7 @@ module Make Input> { bindingset[g1, v1] pragma[inline_late] private predicate unboundBaseImpliesStep(PreGuard g1, GuardValue v1, PreGuard g2, GuardValue v2) { - g1.(IdExpr).getEqualChildExpr() = g2 and v1 = v2 + g1.(IdExpr).getEqualChildExpr() = g2 and v1 = v2 and not v1 instanceof TException or exists(ConditionalExpr cond, boolean branch, Expr e, GuardValue ev | cond = g1 and From c212d0ac8fbc15a0ca898b1cf6b2be5cb110b452 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 20 May 2025 14:00:10 +0200 Subject: [PATCH 06/22] Shared: Improve shared guards lib. --- .../controlflow/codeql/controlflow/Guards.qll | 122 +++++++++++------- 1 file changed, 77 insertions(+), 45 deletions(-) diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index 62308a6a105f..e30f87341ce1 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -299,12 +299,6 @@ module Make Input> { v = TValue(TValueConstant(c.asConstantValue()), true) } - private predicate exprHasValue(Expr e, GuardValue v) { - constantHasValue(e, v) - or - e instanceof NonNullExpr and v = TValue(TValueNull(), false) - } - private predicate exceptionBranchPoint(BasicBlock bb1, BasicBlock normalSucc, BasicBlock excSucc) { exists(SuccessorType norm, ExceptionSuccessor exc | bb1.getASuccessor(norm) = normalSucc and @@ -426,30 +420,6 @@ module Make Input> { branch = false and result = cond.getElse() } - bindingset[g1, v1] - pragma[inline_late] - private predicate unboundBaseImpliesStep(PreGuard g1, GuardValue v1, PreGuard g2, GuardValue v2) { - g1.(IdExpr).getEqualChildExpr() = g2 and v1 = v2 and not v1 instanceof TException - or - exists(ConditionalExpr cond, boolean branch, Expr e, GuardValue ev | - cond = g1 and - e = getBranchExpr(cond, branch) and - exprHasValue(e, ev) and - disjointValues(v1, ev) - | - // g1 === g2 ? e : ...; - // g1 === g2 ? ... : e; - g2 = cond.getCondition() and - v2 = TValue(TValueTrue(), branch.booleanNot()) - or - // g1 === ... ? g2 : e - // g1 === ... ? e : g2 - g2 = getBranchExpr(cond, branch.booleanNot()) and - v2 = v1 and - not exprHasValue(g2, v2) // disregard trivial guard - ) - } - private predicate baseImpliesStep(PreGuard g1, GuardValue v1, PreGuard g2, GuardValue v2) { g1.(AndExpr).getAnOperand() = g2 and v1 = TValue(TValueTrue(), true) and v2 = v1 or @@ -532,15 +502,17 @@ module Make Input> { private import LogicInput private predicate guardControlsPhiBranch( - Guard guard, GuardValue v, SsaPhiNode phi, Expr input, BasicBlock bbInput, BasicBlock bbPhi + Guard guard, GuardValue v, SsaPhiNode phi, SsaDefinition inp ) { - exists(SsaWriteDefinition inp | - phi.hasInputFromBlock(inp, bbInput) and + exists(BasicBlock bbPhi | + phi.hasInputFromBlock(inp, _) and phi.getBasicBlock() = bbPhi and - inp.getDefinition() = input and - guard.directlyValueControls(bbInput, v) and guard.getBasicBlock().strictlyDominates(bbPhi) and - not guard.directlyValueControls(bbPhi, _) + not guard.directlyValueControls(bbPhi, _) and + forex(BasicBlock bbInput | phi.hasInputFromBlock(inp, bbInput) | + guard.directlyValueControls(bbInput, v) or + guard.hasValueBranchEdge(bbInput, bbPhi, v) + ) ) } @@ -552,13 +524,12 @@ module Make Input> { * This makes `phi` similar to the conditional `phi = guard==v ? input : ...`. */ private predicate guardDeterminesPhiInput(Guard guard, GuardValue v, SsaPhiNode phi, Expr input) { - exists(GuardValue dv, BasicBlock bbInput, BasicBlock bbPhi | - guardControlsPhiBranch(guard, v, phi, input, bbInput, bbPhi) and + exists(GuardValue dv, SsaWriteDefinition inp | + guardControlsPhiBranch(guard, v, phi, inp) and + inp.getDefinition() = input and dv = v.getDualValue() and - forall(BasicBlock other | phi.hasInputFromBlock(_, other) and other != bbInput | - guard.directlyValueControls(other, dv) - or - guard.hasValueBranchEdge(other, bbPhi, dv) + forall(SsaDefinition other | phi.hasInputFromBlock(other, _) and other != inp | + guardControlsPhiBranch(guard, dv, phi, other) ) ) } @@ -702,14 +673,67 @@ module Make Input> { or exists(boolean isNull | additionalNullCheck(g1, v1, g2, isNull) and - v2 = TValue(TValueNull(), isNull) + v2 = TValue(TValueNull(), isNull) and + not (g2 instanceof NonNullExpr and isNull = false) // disregard trivial guard + ) + } + + /** + * Holds if `g` evaluating to `v` implies that `def` evaluates to `ssaVal`. + * The included set of implications is somewhat restricted to avoid a + * recursive dependency on `exprHasValue`. + */ + private predicate baseSsaValueCheck(SsaDefinition def, GuardValue ssaVal, Guard g, GuardValue v) { + exists(Guard g0, GuardValue v0 | + guardReadsSsaVar(g0, def) and v0 = ssaVal + or + baseSsaValueCheck(def, ssaVal, g0, v0) + | + impliesStep(g, v, g0, v0) + ) + } + + private predicate exprHasValue(Expr e, GuardValue v) { + constantHasValue(e, v) + or + e instanceof NonNullExpr and v = TValue(TValueNull(), false) + or + exprHasValue(e.(IdExpr).getEqualChildExpr(), v) + or + exists(SsaDefinition def, Guard g, GuardValue gv | + e = def.getARead() and + g.directlyValueControls(e.getBasicBlock(), gv) and + baseSsaValueCheck(def, v, g, gv) + ) + or + exists(SsaWriteDefinition def | + exprHasValue(def.getDefinition(), v) and + e = def.getARead() ) } bindingset[g1, v1] pragma[inline_late] private predicate unboundImpliesStep(Guard g1, GuardValue v1, Guard g2, GuardValue v2) { - unboundBaseImpliesStep(g1, v1, g2, v2) + g1.(IdExpr).getEqualChildExpr() = g2 and v1 = v2 and not v1 instanceof TException + or + exists(ConditionalExpr cond, boolean branch, Expr e, GuardValue ev | + cond = g1 and + e = getBranchExpr(cond, branch) and + exprHasValue(e, ev) and + disjointValues(v1, ev) + | + // g1 === g2 ? e : ...; + // g1 === g2 ? ... : e; + g2 = cond.getCondition() and + v2 = TValue(TValueTrue(), branch.booleanNot()) + or + // g1 === ... ? g2 : e + // g1 === ... ? e : g2 + g2 = getBranchExpr(cond, branch.booleanNot()) and + v2 = v1 and + not exprHasValue(g2, v2) // disregard trivial guard + ) } bindingset[def1, v1] @@ -742,7 +766,11 @@ module Make Input> { * Calculates the transitive closure of all the guard implication steps * starting from a given set of base cases. */ - private module ImpliesTC { + module ImpliesTC { + /** + * Holds if `tgtGuard` evaluating to `tgtVal` implies that `guard` + * evaluates to `v`. + */ pragma[nomagic] predicate guardControls(Guard guard, GuardValue v, Guard tgtGuard, GuardValue tgtVal) { baseGuardValue(tgtGuard, tgtVal) and @@ -770,6 +798,10 @@ module Make Input> { ) } + /** + * Holds if `tgtGuard` evaluating to `tgtVal` implies that `def` + * evaluates to `v`. + */ pragma[nomagic] predicate ssaControls(SsaDefinition def, GuardValue v, Guard tgtGuard, GuardValue tgtVal) { exists(Guard g0 | From 73ae613b7af5fb4a6aeee274fb678000192119ac Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Fri, 23 May 2025 08:46:42 +0200 Subject: [PATCH 07/22] Shared: Many tweaks to Guards. --- .../controlflow/codeql/controlflow/Guards.qll | 93 +++++++++++++++++-- 1 file changed, 83 insertions(+), 10 deletions(-) diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index e30f87341ce1..54ee848bd87b 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -234,6 +234,9 @@ module Make Input> { /** Holds if this value represents `null`. */ predicate isNullValue() { this = TValue(TValueNull(), true) } + /** Holds if this value represents `null` or non-`null` as indicated by `isNull`. */ + predicate isNullness(boolean isNull) { this = TValue(TValueNull(), isNull) } + /** Gets the integer that this value represents, if any. */ int asIntValue() { this = TValue(TValueInt(result), true) } @@ -320,17 +323,19 @@ module Make Input> { ) ) or - exists(Case c | + exceptionBranchPoint(bb1, bb2, _) and v = TException(false) + or + exceptionBranchPoint(bb1, _, bb2) and v = TException(true) + } + + private predicate caseBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue v, Expr switchExpr) { + exists(Case c | switchExpr = c.getSwitchExpr() | v = TCaseMatch(c, true) and c.matchEdge(bb1, bb2) or v = TCaseMatch(c, false) and c.nonMatchEdge(bb1, bb2) ) - or - exceptionBranchPoint(bb1, bb2, _) and v = TException(false) - or - exceptionBranchPoint(bb1, _, bb2) and v = TException(true) } pragma[nomagic] @@ -362,12 +367,16 @@ module Make Input> { */ final class PreGuard extends ExprFinal { /** - * Holds if this guard is the last node in `bb1` and that its successor is - * `bb2` exactly when evaluating to `v`. + * Holds if this guard evaluating to `v` corresponds to taking the edge + * from `bb1` to `bb2`. For ordinary conditional branching this guard is + * the last node in `bb1`, but for switch case matching it is the switch + * expression, which may either be in `bb1` or an earlier basic block. */ predicate hasValueBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue v) { bb1.getLastNode() = this.getControlFlowNode() and branchEdge(bb1, bb2, v) + or + caseBranchEdge(bb1, bb2, v, this) } /** @@ -457,6 +466,12 @@ module Make Input> { BasicBlock getBasicBlock(); Expr getARead(); + + /** Gets a textual representation of this SSA definition. */ + string toString(); + + /** Gets the location of this SSA definition. */ + Location getLocation(); } class SsaWriteDefinition extends SsaDefinition { @@ -549,6 +564,9 @@ module Make Input> { other.getARead() = guard and eqtest.directlyControls(guard.getBasicBlock(), branch) ) + or + // An expression `x = ...` can be considered as a read of `x`. + guard.(IdExpr).getEqualChildExpr() = def.(SsaWriteDefinition).getDefinition() } private predicate valueStep(Expr e1, Expr e2) { @@ -649,7 +667,7 @@ module Make Input> { ) } - private predicate impliesStep(Guard g1, GuardValue v1, Guard g2, GuardValue v2) { + private predicate impliesStep1(Guard g1, GuardValue v1, Guard g2, GuardValue v2) { baseImpliesStep(g1, v1, g2, v2) or exists(SsaDefinition def, Expr e | @@ -689,7 +707,7 @@ module Make Input> { or baseSsaValueCheck(def, ssaVal, g0, v0) | - impliesStep(g, v, g0, v0) + impliesStep1(g, v, g0, v0) ) } @@ -712,6 +730,16 @@ module Make Input> { ) } + private predicate impliesStep2(Guard g1, GuardValue v1, Guard g2, GuardValue v2) { + impliesStep1(g1, v1, g2, v2) + or + exists(Expr nonnull | + exprHasValue(nonnull, v2) and + eqtestHasOperands(g1, g2, nonnull, v1.asBooleanValue()) and + v2 = TValue(TValueNull(), false) + ) + } + bindingset[g1, v1] pragma[inline_late] private predicate unboundImpliesStep(Guard g1, GuardValue v1, Guard g2, GuardValue v2) { @@ -779,7 +807,7 @@ module Make Input> { or exists(Guard g0, GuardValue v0 | guardControls(g0, v0, tgtGuard, tgtVal) and - impliesStep(g0, v0, guard, v) + impliesStep2(g0, v0, guard, v) ) or exists(Guard g0, GuardValue v0 | @@ -816,6 +844,27 @@ module Make Input> { } } + private predicate booleanGuard(Guard guard, GuardValue val) { + exists(guard) and exists(val.asBooleanValue()) + } + + private module BooleanImplies = ImpliesTC; + + /** INTERNAL: Don't use. */ + predicate boolImplies(Guard g1, GuardValue v1, Guard g2, GuardValue v2) { + BooleanImplies::guardControls(g2, v2, g1, v1) and + g2 != g1 + } + + /** + * Holds if `guard` evaluating to `v` implies that `e` is guaranteed to be + * null if `isNull` is true, and non-null if `isNull` is false. + */ + predicate nullGuard(Guard guard, GuardValue v, Expr e, boolean isNull) { + impliesStep2(guard, v, e, TValue(TValueNull(), isNull)) or + additionalImpliesStep(guard, v, e, TValue(TValueNull(), isNull)) + } + private predicate hasAValueBranchEdge(Guard guard, GuardValue v) { guard.hasValueBranchEdge(_, _, v) } @@ -831,6 +880,30 @@ module Make Input> { ) } + /** + * Holds if `def` evaluating to `v` controls the control-flow branch + * edge from `bb1` to `bb2`. That is, following the edge from `bb1` to + * `bb2` implies that `def` evaluated to `v`. + */ + predicate ssaControlsBranchEdge(SsaDefinition def, BasicBlock bb1, BasicBlock bb2, GuardValue v) { + exists(Guard g0, GuardValue v0 | + g0.hasValueBranchEdge(bb1, bb2, v0) and + BranchImplies::ssaControls(def, v, g0, v0) + ) + } + + /** + * Holds if `def` evaluating to `v` controls the basic block `bb`. + * That is, execution of `bb` implies that `def` evaluated to `v`. + */ + predicate ssaControls(SsaDefinition def, BasicBlock bb, GuardValue v) { + exists(BasicBlock guard, BasicBlock succ | + ssaControlsBranchEdge(def, guard, succ, v) and + dominatingEdge(guard, succ) and + succ.dominates(bb) + ) + } + signature module CustomGuardInputSig { class ParameterPosition { /** Gets a textual representation of this element. */ From f772493f4ccf83a04fd698c8f6a6c9ae6a52bc38 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Fri, 23 May 2025 15:21:01 +0200 Subject: [PATCH 08/22] Shared: Elaborate qldoc. --- .../controlflow/codeql/controlflow/Guards.qll | 30 +++++++++++++++++-- 1 file changed, 28 insertions(+), 2 deletions(-) diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index 54ee848bd87b..ff616147fc05 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -23,9 +23,29 @@ * } * ``` * + * The provided predicates are separated into general "controls" predicates and + * "directly controls" predicates. The former use all possible implication + * logic as described above, whereas the latter only use control flow dominance + * of the corresponding conditional successor edges. + * + * In some cases, a guard may have a successor edge that can be relevant for + * controlling the input to an SSA phi node, but does not dominate the + * preceding block. To support this, the `hasBranchEdge` and + * `controlsBranchEdge` predicates are provided, where the former only uses the + * control flow graph similar to the `directlyControls` predicate, and the + * latter uses the full implication logic. + * + * All of these predicates are also available in the more general form that refers + * to `GuardValue`s instead of `boolean`s. + * * The implementation is nested in two parameterized modules intended to * facilitate multiple instantiations of the nested module with different - * precision levels + * precision levels. For example, more implications are available if the result + * of Range Analysis is available, but Range Analysis depends on Guards. This + * allows an initial instantiation of the `Logic` module without Range Analysis + * that can be used as input to Range Analysis, and a second instantiation + * using the result of Range Analysis to provide a final and more complete + * controls relation. */ private import codeql.util.Boolean @@ -178,6 +198,7 @@ signature module InputSig { } } +/** Provides guards-related predicates and classes. */ module Make Input> { private import Input @@ -513,6 +534,10 @@ module Make Input> { } } + /** + * Provides the `Guard` class with suitable 'controls' predicates augmented + * with logical implications based on SSA. + */ module Logic { private import LogicInput @@ -1016,7 +1041,8 @@ module Make Input> { /** * A guard. This may be any expression whose value determines subsequent - * control flow. + * control flow. It may also be a switch case, which as a guard is considered + * to evaluate to either true or false depending on whether the case matches. */ final class Guard extends PreGuard { /** From b19bff9a4e80d4bf825cc3d460ba7916a311ec42 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 26 May 2025 16:02:37 +0200 Subject: [PATCH 09/22] Shared: Switch case guards to be the case statements. --- .../controlflow/codeql/controlflow/Guards.qll | 113 ++++++++---------- 1 file changed, 49 insertions(+), 64 deletions(-) diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index ff616147fc05..c991d44f2e8c 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -106,13 +106,15 @@ signature module InputSig { predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2); - class Expr { - /** Gets a textual representation of this expression. */ + class AstNode { + /** Gets a textual representation of this AST node. */ string toString(); - /** Gets the location of this expression. */ + /** Gets the location of this AST node. */ Location getLocation(); + } + class Expr extends AstNode { /** Gets the associated control flow node. */ ControlFlowNode getControlFlowNode(); @@ -137,12 +139,7 @@ signature module InputSig { class NonNullExpr extends Expr; - class Case { - /** Gets a textual representation of this switch case. */ - string toString(); - - Location getLocation(); - + class Case extends AstNode { Expr getSwitchExpr(); predicate isDefaultCase(); @@ -210,7 +207,6 @@ module Make Input> { private newtype TGuardValue = TValue(TAbstractSingleValue val, Boolean isVal) or - TCaseMatch(Case c, Boolean match) or TException(Boolean throws) private class AbstractSingleValue extends TAbstractSingleValue { @@ -233,7 +229,7 @@ module Make Input> { * - null vs. not null * - true vs. false * - evaluating to a specific value vs. evaluating to any other value - * - matching a specific case vs. not matching that case + * - throwing an exception vs. not throwing an exception */ GuardValue getDualValue() { exists(AbstractSingleValue val, boolean isVal | @@ -241,11 +237,6 @@ module Make Input> { result = TValue(val, isVal.booleanNot()) ) or - exists(Case c, boolean match | - this = TCaseMatch(c, match) and - result = TCaseMatch(c, match.booleanNot()) - ) - or exists(boolean throws | this = TException(throws) and result = TException(throws.booleanNot()) @@ -280,19 +271,6 @@ module Make Input> { this = TValue(val, false) and result = "not " + val.toString() ) or - exists(Case c, boolean match, string s | this = TCaseMatch(c, match) | - ( - exists(ConstantExpr ce | c.asConstantCase() = ce and s = ce.toString()) - or - not exists(c.asConstantCase()) and s = c.toString() - ) and - ( - match = true and result = "match " + s - or - match = false and result = "non-match " + s - ) - ) - or exists(boolean throws | this = TException(throws) | throws = true and result = "exception" or @@ -349,14 +327,12 @@ module Make Input> { exceptionBranchPoint(bb1, _, bb2) and v = TException(true) } - private predicate caseBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue v, Expr switchExpr) { - exists(Case c | switchExpr = c.getSwitchExpr() | - v = TCaseMatch(c, true) and - c.matchEdge(bb1, bb2) - or - v = TCaseMatch(c, false) and - c.nonMatchEdge(bb1, bb2) - ) + private predicate caseBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue v, Case c) { + v = TValue(TValueTrue(), true) and + c.matchEdge(bb1, bb2) + or + v = TValue(TValueTrue(), false) and + c.nonMatchEdge(bb1, bb2) } pragma[nomagic] @@ -367,26 +343,22 @@ module Make Input> { eqtest.polarity() = polarity } - private predicate caseGuard(PreGuard g, Case c, Expr switchExpr) { - g.hasValueBranchEdge(_, _, TCaseMatch(c, _)) and - switchExpr = c.getSwitchExpr() - } - - private predicate constcaseEquality(PreGuard g, Expr e1, ConstantExpr e2, GuardValue eqval) { + private predicate constcaseEquality(PreGuard g, Expr e1, ConstantExpr e2) { exists(Case c | - caseGuard(g, c, e1) and - c.asConstantCase() = e2 and - eqval = TCaseMatch(c, true) + g = c and + e1 = c.getSwitchExpr() and + e2 = c.asConstantCase() ) } - final private class ExprFinal = Expr; + final private class FinalAstNode = AstNode; /** * A guard. This may be any expression whose value determines subsequent - * control flow. + * control flow. It may also be a switch case, which as a guard is considered + * to evaluate to either true or false depending on whether the case matches. */ - final class PreGuard extends ExprFinal { + final class PreGuard extends FinalAstNode { /** * Holds if this guard evaluating to `v` corresponds to taking the edge * from `bb1` to `bb2`. For ordinary conditional branching this guard is @@ -394,7 +366,7 @@ module Make Input> { * expression, which may either be in `bb1` or an earlier basic block. */ predicate hasValueBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue v) { - bb1.getLastNode() = this.getControlFlowNode() and + bb1.getLastNode() = this.(Expr).getControlFlowNode() and branchEdge(bb1, bb2, v) or caseBranchEdge(bb1, bb2, v, this) @@ -435,12 +407,23 @@ module Make Input> { * Holds if this guard tests equality between `e1` and `e2` upon evaluating * to `eqval`. */ - predicate isEquality(Expr e1, Expr e2, GuardValue eqval) { - eqtestHasOperands(this, e1, e2, eqval.asBooleanValue()) + predicate isEquality(Expr e1, Expr e2, boolean eqval) { + eqtestHasOperands(this, e1, e2, eqval) or - constcaseEquality(this, e1, e2, eqval) + constcaseEquality(this, e1, e2) and eqval = true or - constcaseEquality(this, e2, e1, eqval) + constcaseEquality(this, e2, e1) and eqval = true + } + + /** + * Gets the basic block of this guard. For expressions, this is the basic + * block of the expression itself, and for switch cases, this is the basic + * block of the expression being compared against the cases. + */ + BasicBlock getBasicBlock() { + result = this.(Expr).getBasicBlock() + or + result = this.(Case).getSwitchExpr().getBasicBlock() } } @@ -458,7 +441,7 @@ module Make Input> { g1.(NotExpr).getOperand() = g2 and v1.asBooleanValue().booleanNot() = v2.asBooleanValue() or exists(GuardValue eqval, ConstantExpr constant, GuardValue cv | - g1.isEquality(g2, constant, eqval) and + g1.isEquality(g2, constant, eqval.asBooleanValue()) and constantHasValue(constant, cv) | v1 = eqval and v2 = cv @@ -471,13 +454,14 @@ module Make Input> { v2 = TValue(TValueNull(), false) ) or - exists(Case c1, Case c2, Expr switchExpr | - caseGuard(g1, c1, switchExpr) and - v1 = TCaseMatch(c1, true) and + exists(Case c1, Expr switchExpr | + g1 = c1 and c1.isDefaultCase() and - caseGuard(g2, c2, switchExpr) and - v2 = TCaseMatch(c2, false) and - c1 != c2 + c1.getSwitchExpr() = switchExpr and + v1.asBooleanValue() = true and + g2.(Case).getSwitchExpr() = switchExpr and + v2.asBooleanValue() = false and + g1 != g2 ) } @@ -970,7 +954,9 @@ module Make Input> { module CustomGuard { private import CustomGuardInput - private class ReturnExpr extends ExprFinal { + final private class FinalExpr = Expr; + + private class ReturnExpr extends FinalExpr { ReturnExpr() { any(BooleanMethod m).getAReturnExpr() = this } pragma[nomagic] @@ -993,8 +979,7 @@ module Make Input> { ) { exists(BooleanMethod m, SsaDefinition param | m.getAReturnExpr() = ret and - m.getParameter(ppos) = param and - not val instanceof TCaseMatch + m.getParameter(ppos) = param | exists(Guard g0, GuardValue v0 | g0.directlyValueControls(ret.getBasicBlock(), v0) and From 378209a6ad0699efe40aecf4d1afcd3e09f97fe6 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 27 May 2025 14:19:01 +0200 Subject: [PATCH 10/22] Shared: Simplify and improve joins. --- .../controlflow/codeql/controlflow/Guards.qll | 43 ++++++++++--------- 1 file changed, 23 insertions(+), 20 deletions(-) diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index c991d44f2e8c..bbaea7b87ad0 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -244,7 +244,10 @@ module Make Input> { } /** Holds if this value represents `null`. */ - predicate isNullValue() { this = TValue(TValueNull(), true) } + predicate isNullValue() { this.isNullness(true) } + + /** Holds if this value represents non-`null`. */ + predicate isNonNullValue() { this.isNullness(false) } /** Holds if this value represents `null` or non-`null` as indicated by `isNull`. */ predicate isNullness(boolean isNull) { this = TValue(TValueNull(), isNull) } @@ -292,13 +295,13 @@ module Make Input> { } private predicate constantHasValue(ConstantExpr c, GuardValue v) { - c.isNull() and v = TValue(TValueNull(), true) + c.isNull() and v.isNullValue() or - v = TValue(TValueTrue(), c.asBooleanValue()) + v.asBooleanValue() = c.asBooleanValue() or - v = TValue(TValueInt(c.asIntegerValue()), true) + v.asIntValue() = c.asIntegerValue() or - v = TValue(TValueConstant(c.asConstantValue()), true) + v.asConstantValue() = c.asConstantValue() } private predicate exceptionBranchPoint(BasicBlock bb1, BasicBlock normalSucc, BasicBlock excSucc) { @@ -328,10 +331,10 @@ module Make Input> { } private predicate caseBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue v, Case c) { - v = TValue(TValueTrue(), true) and + v.asBooleanValue() = true and c.matchEdge(bb1, bb2) or - v = TValue(TValueTrue(), false) and + v.asBooleanValue() = false and c.nonMatchEdge(bb1, bb2) } @@ -390,7 +393,7 @@ module Make Input> { * `bb2` exactly when evaluating to `branch`. */ predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { - this.hasValueBranchEdge(bb1, bb2, TValue(TValueTrue(), branch)) + this.hasValueBranchEdge(bb1, bb2, any(GuardValue gv | gv.asBooleanValue() = branch)) } /** @@ -400,7 +403,7 @@ module Make Input> { * That is, `bb` is dominated by the `branch`-successor edge of this guard. */ predicate directlyControls(BasicBlock bb, boolean branch) { - this.directlyValueControls(bb, TValue(TValueTrue(), branch)) + this.directlyValueControls(bb, any(GuardValue gv | gv.asBooleanValue() = branch)) } /** @@ -434,9 +437,9 @@ module Make Input> { } private predicate baseImpliesStep(PreGuard g1, GuardValue v1, PreGuard g2, GuardValue v2) { - g1.(AndExpr).getAnOperand() = g2 and v1 = TValue(TValueTrue(), true) and v2 = v1 + g1.(AndExpr).getAnOperand() = g2 and v1.asBooleanValue() = true and v2 = v1 or - g1.(OrExpr).getAnOperand() = g2 and v1 = TValue(TValueTrue(), false) and v2 = v1 + g1.(OrExpr).getAnOperand() = g2 and v1.asBooleanValue() = false and v2 = v1 or g1.(NotExpr).getOperand() = g2 and v1.asBooleanValue().booleanNot() = v2.asBooleanValue() or @@ -451,7 +454,7 @@ module Make Input> { or exists(NonNullExpr nonnull | eqtestHasOperands(g1, g2, nonnull, v1.asBooleanValue()) and - v2 = TValue(TValueNull(), false) + v2.isNonNullValue() ) or exists(Case c1, Expr switchExpr | @@ -700,7 +703,7 @@ module Make Input> { or exists(boolean isNull | additionalNullCheck(g1, v1, g2, isNull) and - v2 = TValue(TValueNull(), isNull) and + v2.isNullness(isNull) and not (g2 instanceof NonNullExpr and isNull = false) // disregard trivial guard ) } @@ -723,7 +726,7 @@ module Make Input> { private predicate exprHasValue(Expr e, GuardValue v) { constantHasValue(e, v) or - e instanceof NonNullExpr and v = TValue(TValueNull(), false) + e instanceof NonNullExpr and v.isNonNullValue() or exprHasValue(e.(IdExpr).getEqualChildExpr(), v) or @@ -745,7 +748,7 @@ module Make Input> { exists(Expr nonnull | exprHasValue(nonnull, v2) and eqtestHasOperands(g1, g2, nonnull, v1.asBooleanValue()) and - v2 = TValue(TValueNull(), false) + v2.isNonNullValue() ) } @@ -763,7 +766,7 @@ module Make Input> { // g1 === g2 ? e : ...; // g1 === g2 ? ... : e; g2 = cond.getCondition() and - v2 = TValue(TValueTrue(), branch.booleanNot()) + v2.asBooleanValue() = branch.booleanNot() or // g1 === ... ? g2 : e // g1 === ... ? e : g2 @@ -870,8 +873,8 @@ module Make Input> { * null if `isNull` is true, and non-null if `isNull` is false. */ predicate nullGuard(Guard guard, GuardValue v, Expr e, boolean isNull) { - impliesStep2(guard, v, e, TValue(TValueNull(), isNull)) or - additionalImpliesStep(guard, v, e, TValue(TValueNull(), isNull)) + impliesStep2(guard, v, e, any(GuardValue gv | gv.isNullness(isNull))) or + additionalImpliesStep(guard, v, e, any(GuardValue gv | gv.isNullness(isNull))) } private predicate hasAValueBranchEdge(Guard guard, GuardValue v) { @@ -1066,7 +1069,7 @@ module Make Input> { * also considers additional logical reasoning. */ predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { - this.valueControlsBranchEdge(bb1, bb2, TValue(TValueTrue(), branch)) + this.valueControlsBranchEdge(bb1, bb2, any(GuardValue gv | gv.asBooleanValue() = branch)) } /** @@ -1078,7 +1081,7 @@ module Make Input> { * also considers additional logical reasoning. */ predicate controls(BasicBlock bb, boolean branch) { - this.valueControls(bb, TValue(TValueTrue(), branch)) + this.valueControls(bb, any(GuardValue gv | gv.asBooleanValue() = branch)) } } } From 22d5dc999a385acc3bea0301b3279876fea087f9 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 16 Jun 2025 13:05:04 +0200 Subject: [PATCH 11/22] Shared: Bugfix for unique value implication. --- java/ql/test/library-tests/guards/Guards.java | 16 ++++++++++++++++ .../library-tests/guards/GuardsInline.expected | 4 ++++ shared/controlflow/codeql/controlflow/Guards.qll | 1 + 3 files changed, 21 insertions(+) diff --git a/java/ql/test/library-tests/guards/Guards.java b/java/ql/test/library-tests/guards/Guards.java index a524c237f130..877c1827166b 100644 --- a/java/ql/test/library-tests/guards/Guards.java +++ b/java/ql/test/library-tests/guards/Guards.java @@ -127,4 +127,20 @@ void t6() { chk(); // $ guarded='o != null:false' guarded=g(1):false } } + + void t7(int[] a) { + boolean found = false; + for (int i = 0; i < a.length; i++) { + boolean answer = a[i] == 42; + if (answer) { + found = true; + } + if (found) { + chk(); // $ guarded=found:true guarded='i < a.length:true' + } + } + if (found) { + chk(); // $ guarded=found:true guarded='i < a.length:false' + } + } } diff --git a/java/ql/test/library-tests/guards/GuardsInline.expected b/java/ql/test/library-tests/guards/GuardsInline.expected index 665424c2f5b6..1aaf791acabd 100644 --- a/java/ql/test/library-tests/guards/GuardsInline.expected +++ b/java/ql/test/library-tests/guards/GuardsInline.expected @@ -54,3 +54,7 @@ | Guards.java:125:7:125:11 | chk(...) | 'o != null:true' | | Guards.java:127:7:127:11 | chk(...) | 'o != null:false' | | Guards.java:127:7:127:11 | chk(...) | g(1):false | +| Guards.java:139:9:139:13 | chk(...) | 'i < a.length:true' | +| Guards.java:139:9:139:13 | chk(...) | found:true | +| Guards.java:143:7:143:11 | chk(...) | 'i < a.length:false' | +| Guards.java:143:7:143:11 | chk(...) | found:true | diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index bbaea7b87ad0..9733114613b3 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -647,6 +647,7 @@ module Make Input> { */ private predicate uniqueValue(SsaDefinition v, Expr e, GuardValue k) { possibleValue(v, false, e, k) and + not possibleValue(v, true, e, k) and forex(Expr other, GuardValue otherval | possibleValue(v, _, other, otherval) and other != e | disjointValues(otherval, k) ) From a2778eee75d9640a4c8c98e56f4bbc7e93406ac7 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 14 May 2025 11:22:58 +0200 Subject: [PATCH 12/22] Java: Refactor clearlyNotNullExpr into a base case that does not rely on SSA. --- .../semmle/code/java/dataflow/NullGuards.qll | 50 +++++++++++-------- 1 file changed, 30 insertions(+), 20 deletions(-) diff --git a/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll b/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll index 2dd72d78a2ea..971fc3cf0728 100644 --- a/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll +++ b/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll @@ -40,34 +40,44 @@ EqualityTest varEqualityTestExpr(SsaVariable v1, SsaVariable v2, boolean isEqual isEqualExpr = result.polarity() } -/** Gets an expression that is provably not `null`. */ -Expr clearlyNotNullExpr(Expr reason) { - result instanceof ClassInstanceExpr and reason = result +Expr baseNotNullExpr() { + result instanceof ClassInstanceExpr or - result instanceof ArrayCreationExpr and reason = result + result instanceof ArrayCreationExpr or - result instanceof TypeLiteral and reason = result + result instanceof TypeLiteral or - result instanceof ThisAccess and reason = result + result instanceof ThisAccess or - result instanceof StringLiteral and reason = result + result instanceof StringLiteral or - result instanceof AddExpr and result.getType() instanceof TypeString and reason = result + result instanceof AddExpr and result.getType() instanceof TypeString or exists(Field f | result = f.getAnAccess() and (f.hasName("TRUE") or f.hasName("FALSE")) and - f.getDeclaringType().hasQualifiedName("java.lang", "Boolean") and - reason = result + f.getDeclaringType().hasQualifiedName("java.lang", "Boolean") ) or - result.(CastExpr).getExpr() = clearlyNotNullExpr(reason) + result = any(EnumConstant c).getAnAccess() or - result.(ImplicitCastExpr).getExpr() = clearlyNotNullExpr(reason) + result instanceof ImplicitNotNullExpr or - result instanceof ImplicitNotNullExpr and reason = result + result instanceof ImplicitCoercionToUnitExpr or - result instanceof ImplicitCoercionToUnitExpr and reason = result + result + .(MethodCall) + .getMethod() + .hasQualifiedName("com.google.common.base", "Strings", "nullToEmpty") +} + +/** Gets an expression that is provably not `null`. */ +Expr clearlyNotNullExpr(Expr reason) { + result = baseNotNullExpr() and reason = result + or + result.(CastExpr).getExpr() = clearlyNotNullExpr(reason) + or + result.(ImplicitCastExpr).getExpr() = clearlyNotNullExpr(reason) or result.(AssignExpr).getSource() = clearlyNotNullExpr(reason) or @@ -83,14 +93,14 @@ Expr clearlyNotNullExpr(Expr reason) { guard.controls(rval.getBasicBlock(), branch) and reason = guard and rval = v.getAUse() and - result = rval + result = rval and + not result = baseNotNullExpr() ) or - exists(SsaVariable v | clearlyNotNull(v, reason) and result = v.getAUse()) - or - exists(Method m | m = result.(MethodCall).getMethod() and reason = result | - m.getDeclaringType().hasQualifiedName("com.google.common.base", "Strings") and - m.hasName("nullToEmpty") + exists(SsaVariable v | + clearlyNotNull(v, reason) and + result = v.getAUse() and + not result = baseNotNullExpr() ) } From 0607fefc57bc35d6eb89067c837cde044f2b6559 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 19 May 2025 14:31:22 +0200 Subject: [PATCH 13/22] Java: Refactor integerGuard. --- .../code/java/dataflow/IntegerGuards.qll | 121 ++++++++---------- 1 file changed, 56 insertions(+), 65 deletions(-) diff --git a/java/ql/lib/semmle/code/java/dataflow/IntegerGuards.qll b/java/ql/lib/semmle/code/java/dataflow/IntegerGuards.qll index 58d77b649788..a91dbced456a 100644 --- a/java/ql/lib/semmle/code/java/dataflow/IntegerGuards.qll +++ b/java/ql/lib/semmle/code/java/dataflow/IntegerGuards.qll @@ -32,6 +32,58 @@ class IntComparableExpr extends Expr { } } +/** + * Holds if `comp` evaluating to `branch` ensures that `e1` is less than `e2`. + * When `strict` is true, `e1` is strictly less than `e2`, otherwise it is less + * than or equal to `e2`. + */ +private predicate comparison(ComparisonExpr comp, boolean branch, Expr e1, Expr e2, boolean strict) { + branch = true and + e1 = comp.getLesserOperand() and + e2 = comp.getGreaterOperand() and + (if comp.isStrict() then strict = true else strict = false) + or + branch = false and + e1 = comp.getGreaterOperand() and + e2 = comp.getLesserOperand() and + (if comp.isStrict() then strict = false else strict = true) +} + +/** + * Holds if `guard` evaluating to `branch` ensures that: + * `e <= k` when `upper = true` + * `e >= k` when `upper = false` + */ +pragma[nomagic] +predicate rangeGuard(Expr guard, boolean branch, Expr e, int k, boolean upper) { + exists(EqualityTest eqtest, Expr c | + eqtest = guard and + eqtest.hasOperands(e, c) and + bounded(c, any(ZeroBound zb), k, upper, _) and + branch = eqtest.polarity() + ) + or + exists(Expr c, int val, boolean strict, int d | + bounded(c, any(ZeroBound zb), val, upper, _) and + ( + upper = true and + comparison(guard, branch, e, c, strict) and + d = -1 + or + upper = false and + comparison(guard, branch, c, e, strict) and + d = 1 + ) and + ( + strict = false and k = val + or + // e < c <= val ==> e <= c - 1 <= val - 1 + // e > c >= val ==> e >= c + 1 >= val + 1 + strict = true and k = val + d + ) + ) +} + /** * An expression that directly tests whether a given expression is equal to `k` or not. * The set of `k`s is restricted to those that are relevant for the expression or @@ -53,75 +105,14 @@ Expr integerGuard(IntComparableExpr e, boolean branch, int k, boolean is_k) { ) ) or - exists(EqualityTest eqtest, int val, Expr c, boolean upper | - k = e.relevantInt() and - eqtest = result and - eqtest.hasOperands(e, c) and - bounded(c, any(ZeroBound zb), val, upper, _) and - is_k = false and - ( - upper = true and val < k - or - upper = false and val > k - ) and - branch = eqtest.polarity() - ) - or - exists(ComparisonExpr comp, Expr c, int val, boolean upper | + exists(int val, boolean upper | + rangeGuard(result, branch, e, val, upper) and k = e.relevantInt() and - comp = result and - comp.hasOperands(e, c) and - bounded(c, any(ZeroBound zb), val, upper, _) and is_k = false | - // k <= val <= c < e, so e != k - comp.getLesserOperand() = c and - comp.isStrict() and - branch = true and - val >= k and - upper = false - or - comp.getLesserOperand() = c and - comp.isStrict() and - branch = false and - val < k and - upper = true - or - comp.getLesserOperand() = c and - not comp.isStrict() and - branch = true and - val > k and - upper = false + upper = true and val < k // e <= val < k ==> e != k or - comp.getLesserOperand() = c and - not comp.isStrict() and - branch = false and - val <= k and - upper = true - or - comp.getGreaterOperand() = c and - comp.isStrict() and - branch = true and - val <= k and - upper = true - or - comp.getGreaterOperand() = c and - comp.isStrict() and - branch = false and - val > k and - upper = false - or - comp.getGreaterOperand() = c and - not comp.isStrict() and - branch = true and - val < k and - upper = true - or - comp.getGreaterOperand() = c and - not comp.isStrict() and - branch = false and - val >= k and - upper = false + upper = false and val > k // e >= val > k ==> e != k ) } From cc13193cb6a909513294da7312f031381de38293 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 21 May 2025 14:16:11 +0200 Subject: [PATCH 14/22] Java: Replace some references to basicNullGuard. --- .../semmle/code/java/dataflow/NullGuards.qll | 19 +++++++++++++++---- .../ql/src/Language Abuse/UselessNullCheck.ql | 2 +- 2 files changed, 16 insertions(+), 5 deletions(-) diff --git a/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll b/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll index 971fc3cf0728..5fde238a4b65 100644 --- a/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll +++ b/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll @@ -306,10 +306,21 @@ private Method customNullGuard(int index, boolean retval, boolean isnull) { } /** - * `guard` is a guard expression that suggests that `v` might be null. - * - * This is equivalent to `guard = basicNullGuard(sameValue(v, _), _, true)`. + * Holds if `guard` is a guard expression that suggests that `e` might be null. + */ +predicate guardSuggestsExprMaybeNull(Expr guard, Expr e) { + guard.(EqualityTest).hasOperands(e, any(NullLiteral n)) + or + exists(MethodCall call | + call = guard and + call.getAnArgument() = e and + nullCheckMethod(call.getMethod(), _, true) + ) +} + +/** + * Holds if `guard` is a guard expression that suggests that `v` might be null. */ predicate guardSuggestsVarMaybeNull(Expr guard, SsaVariable v) { - guard = basicNullGuard(sameValue(v, _), _, true) + guardSuggestsExprMaybeNull(guard, sameValue(v, _)) } diff --git a/java/ql/src/Language Abuse/UselessNullCheck.ql b/java/ql/src/Language Abuse/UselessNullCheck.ql index 1ad1c4c8e1e2..d95b528c4c46 100644 --- a/java/ql/src/Language Abuse/UselessNullCheck.ql +++ b/java/ql/src/Language Abuse/UselessNullCheck.ql @@ -18,7 +18,7 @@ import semmle.code.java.controlflow.Guards from Expr guard, Expr e, Expr reason, string msg where - guard = basicNullGuard(e, _, true) and + guardSuggestsExprMaybeNull(guard, e) and e = clearlyNotNullExpr(reason) and ( if reason instanceof Guard From 5c0dcd980d2eb474863e49d4d9f17749ff7995f9 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 15 May 2025 16:23:21 +0200 Subject: [PATCH 15/22] Java: Switch to the shared Guards library. --- .../code/java/controlflow/BasicBlocks.qll | 11 + .../semmle/code/java/controlflow/Guards.qll | 619 +++++++++++------- .../java/controlflow/internal/GuardsLogic.qll | 396 ----------- .../semmle/code/java/dataflow/NullGuards.qll | 110 +--- .../semmle/code/java/dataflow/Nullness.qll | 27 +- .../code/java/dataflow/RangeAnalysis.qll | 5 +- .../semmle/code/java/dataflow/RangeUtils.qll | 2 +- .../java/dataflow/internal/DataFlowNodes.qll | 2 - .../rangeanalysis/ModulusAnalysisSpecific.qll | 2 +- .../rangeanalysis/SignAnalysisSpecific.qll | 2 +- .../code/java/security/ArithmeticCommon.qll | 1 - .../ql/src/Language Abuse/UselessNullCheck.ql | 2 +- java/ql/test/library-tests/guards/Guards.java | 30 +- .../guards/GuardsInline.expected | 35 +- .../test/library-tests/guards/GuardsInline.ql | 9 + .../library-tests/guards12/guard.expected | 8 - java/ql/test/library-tests/guards12/guard.ql | 4 +- java/ql/test/query-tests/Nullness/C.java | 2 +- .../query-tests/Nullness/NullMaybe.expected | 1 - 19 files changed, 484 insertions(+), 784 deletions(-) delete mode 100644 java/ql/lib/semmle/code/java/controlflow/internal/GuardsLogic.qll diff --git a/java/ql/lib/semmle/code/java/controlflow/BasicBlocks.qll b/java/ql/lib/semmle/code/java/controlflow/BasicBlocks.qll index 284ee1dad0ce..7c9e58b20ce1 100644 --- a/java/ql/lib/semmle/code/java/controlflow/BasicBlocks.qll +++ b/java/ql/lib/semmle/code/java/controlflow/BasicBlocks.qll @@ -85,6 +85,17 @@ class BasicBlock extends BbImpl::BasicBlock { */ predicate dominates(BasicBlock bb) { super.dominates(bb) } + /** + * Holds if this basic block strictly dominates basic block `bb`. + * + * That is, all paths reaching `bb` from the entry point basic block must + * go through this basic block and this basic block is different from `bb`. + */ + predicate strictlyDominates(BasicBlock bb) { super.strictlyDominates(bb) } + + /** Gets an immediate successor of this basic block of a given type, if any. */ + BasicBlock getASuccessor(Input::SuccessorType t) { result = super.getASuccessor(t) } + /** * DEPRECATED: Use `getASuccessor` instead. * diff --git a/java/ql/lib/semmle/code/java/controlflow/Guards.qll b/java/ql/lib/semmle/code/java/controlflow/Guards.qll index 4042e7b29624..be023939b8c0 100644 --- a/java/ql/lib/semmle/code/java/controlflow/Guards.qll +++ b/java/ql/lib/semmle/code/java/controlflow/Guards.qll @@ -5,9 +5,9 @@ import java private import semmle.code.java.controlflow.Dominance -private import semmle.code.java.controlflow.internal.GuardsLogic private import semmle.code.java.controlflow.internal.Preconditions private import semmle.code.java.controlflow.internal.SwitchCases +private import codeql.controlflow.Guards as SharedGuards /** * A basic block that terminates in a condition, splitting the subsequent control flow. @@ -137,67 +137,381 @@ private predicate isNonFallThroughPredecessor(SwitchCase sc, ControlFlowNode pre ) } -/** - * A condition that can be evaluated to either true or false. This can either - * be an `Expr` of boolean type that isn't a boolean literal, or a case of a - * switch statement, or a method access that acts as a precondition check. - * - * Evaluating a switch case to true corresponds to taking that switch case, and - * evaluating it to false corresponds to taking some other branch. - */ -final class Guard extends ExprParent { - Guard() { - this.(Expr).getType() instanceof BooleanType and not this instanceof BooleanLiteral - or - this instanceof SwitchCase - or - conditionCheckArgument(this, _, _) +private module GuardsInput implements SharedGuards::InputSig { + private import java as J + private import semmle.code.java.dataflow.NullGuards as NullGuards + import SuccessorType + + class ControlFlowNode = J::ControlFlowNode; + + class BasicBlock = J::BasicBlock; + + predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2) { J::dominatingEdge(bb1, bb2) } + + class AstNode = ExprParent; + + class Expr = J::Expr; + + private newtype TConstantValue = + TCharValue(string c) { any(CharacterLiteral lit).getValue() = c } or + TStringValue(string value) { any(CompileTimeConstantExpr c).getStringValue() = value } or + TEnumValue(EnumConstant c) + + class ConstantValue extends TConstantValue { + string toString() { + this = TCharValue(result) + or + this = TStringValue(result) + or + exists(EnumConstant c | this = TEnumValue(c) and result = c.toString()) + } } - /** Gets the immediately enclosing callable whose body contains this guard. */ - Callable getEnclosingCallable() { - result = this.(Expr).getEnclosingCallable() or - result = this.(SwitchCase).getEnclosingCallable() + abstract class ConstantExpr extends Expr { + predicate isNull() { none() } + + boolean asBooleanValue() { none() } + + int asIntegerValue() { none() } + + ConstantValue asConstantValue() { none() } } - /** Gets the statement containing this guard. */ - Stmt getEnclosingStmt() { - result = this.(Expr).getEnclosingStmt() or - result = this.(SwitchCase).getSwitch() or - result = this.(SwitchCase).getSwitchExpr().getEnclosingStmt() + private class NullConstant extends ConstantExpr instanceof J::NullLiteral { + override predicate isNull() { any() } } - /** - * Gets the basic block containing this guard or the basic block that tests the - * applicability of this switch case -- for a pattern case this is the case statement - * itself; for a non-pattern case this is the most recent pattern case or the top of - * the switch block if there is none. - */ - BasicBlock getBasicBlock() { - // Not a switch case - result = this.(Expr).getBasicBlock() - or - // Return the closest pattern case statement before this one, including this one. - result = getClosestPrecedingPatternCase(this).getBasicBlock() - or - // Not a pattern case and no preceding pattern case -- return the top of the switch block. - not exists(getClosestPrecedingPatternCase(this)) and - result = this.(SwitchCase).getSelectorExpr().getBasicBlock() + private class BooleanConstant extends ConstantExpr instanceof J::BooleanLiteral { + override boolean asBooleanValue() { result = super.getBooleanValue() } } - /** - * Holds if this guard is an equality test between `e1` and `e2`. The test - * can be either `==`, `!=`, `.equals`, or a switch case. If the test is - * negated, that is `!=`, then `polarity` is false, otherwise `polarity` is - * true. - */ - predicate isEquality(Expr e1, Expr e2, boolean polarity) { - exists(Expr exp1, Expr exp2 | equalityGuard(this, exp1, exp2, polarity) | - e1 = exp1 and e2 = exp2 + private class IntegerConstant extends ConstantExpr instanceof J::CompileTimeConstantExpr { + override int asIntegerValue() { result = super.getIntValue() } + } + + private class CharConstant extends ConstantExpr instanceof J::CharacterLiteral { + override ConstantValue asConstantValue() { result = TCharValue(super.getValue()) } + } + + private class StringConstant extends ConstantExpr instanceof J::CompileTimeConstantExpr { + override ConstantValue asConstantValue() { result = TStringValue(super.getStringValue()) } + } + + private class EnumConstantExpr extends ConstantExpr instanceof J::VarAccess { + override ConstantValue asConstantValue() { + exists(EnumConstant c | this = c.getAnAccess() and result = TEnumValue(c)) + } + } + + class NonNullExpr extends Expr { + NonNullExpr() { + this = NullGuards::baseNotNullExpr() + or + exists(Field f | + this = f.getAnAccess() and + f.isFinal() and + f.getInitializer() = NullGuards::baseNotNullExpr() + ) + } + } + + class Case extends ExprParent instanceof J::SwitchCase { + Expr getSwitchExpr() { result = super.getSelectorExpr() } + + predicate isDefaultCase() { this instanceof DefaultCase } + + ConstantExpr asConstantCase() { + exists(ConstCase cc | this = cc | + cc.getValue() = result and + strictcount(cc.getValue(_)) = 1 + ) + } + + private predicate hasPatternCaseMatchEdge(BasicBlock bb1, BasicBlock bb2, boolean isMatch) { + exists(ConditionNode patterncase | + this instanceof PatternCase and + patterncase = super.getControlFlowNode() and + bb1.getLastNode() = patterncase and + bb2.getFirstNode() = patterncase.getABranchSuccessor(isMatch) + ) + } + + predicate matchEdge(BasicBlock bb1, BasicBlock bb2) { + exists(ControlFlowNode pred | + // Pattern cases are handled as ConditionBlocks. + not this instanceof PatternCase and + bb2.getFirstNode() = super.getControlFlowNode() and + isNonFallThroughPredecessor(this, pred) and + bb1 = pred.getBasicBlock() + ) + or + this.hasPatternCaseMatchEdge(bb1, bb2, true) + } + + predicate nonMatchEdge(BasicBlock bb1, BasicBlock bb2) { + this.hasPatternCaseMatchEdge(bb1, bb2, false) + } + } + + abstract private class BinExpr extends Expr { + Expr getAnOperand() { + result = this.(BinaryExpr).getAnOperand() or result = this.(AssignOp).getSource() + } + } + + class AndExpr extends BinExpr { + AndExpr() { + this instanceof AndBitwiseExpr or + this instanceof AndLogicalExpr or + this instanceof AssignAndExpr + } + } + + class OrExpr extends BinExpr { + OrExpr() { + this instanceof OrBitwiseExpr or + this instanceof OrLogicalExpr or + this instanceof AssignOrExpr + } + } + + class NotExpr extends Expr instanceof J::LogNotExpr { + Expr getOperand() { result = this.(J::LogNotExpr).getExpr() } + } + + class IdExpr extends Expr { + IdExpr() { this instanceof AssignExpr or this instanceof CastExpr } + + Expr getEqualChildExpr() { + result = this.(AssignExpr).getSource() + or + result = this.(CastExpr).getExpr() + } + } + + private predicate objectsEquals(Method equals) { + equals.hasQualifiedName("java.util", "Objects", "equals") and + equals.getNumberOfParameters() = 2 + } + + class EqualityTest extends Expr { + EqualityTest() { + this instanceof J::EqualityTest or + this.(MethodCall).getMethod() instanceof EqualsMethod or + objectsEquals(this.(MethodCall).getMethod()) + } + + Expr getAnOperand() { + result = this.(J::EqualityTest).getAnOperand() + or + result = this.(MethodCall).getAnArgument() + or + this.(MethodCall).getMethod() instanceof EqualsMethod and + result = this.(MethodCall).getQualifier() + } + + boolean polarity() { + result = this.(J::EqualityTest).polarity() or - e2 = exp1 and e1 = exp2 + result = true and not this instanceof J::EqualityTest + } + } + + class ConditionalExpr extends Expr instanceof J::ConditionalExpr { + Expr getCondition() { result = super.getCondition() } + + Expr getThen() { result = super.getTrueExpr() } + + Expr getElse() { result = super.getFalseExpr() } + } +} + +private module GuardsImpl = SharedGuards::Make; + +private module LogicInputCommon { + private import semmle.code.java.dataflow.NullGuards as NullGuards + + predicate additionalNullCheck( + GuardsImpl::PreGuard guard, GuardValue val, GuardsInput::Expr e, boolean isNull + ) { + guard.(InstanceOfExpr).getExpr() = e and val.asBooleanValue() = true and isNull = false + or + exists(MethodCall call | + call = guard and + call.getAnArgument() = e and + NullGuards::nullCheckMethod(call.getMethod(), val.asBooleanValue(), isNull) + ) + } +} + +private module LogicInput_v1 implements GuardsImpl::LogicInputSig { + private import semmle.code.java.dataflow.internal.BaseSSA + + final private class FinalBaseSsaVariable = BaseSsaVariable; + + class SsaDefinition extends FinalBaseSsaVariable { + GuardsInput::Expr getARead() { result = this.getAUse() } + } + + class SsaWriteDefinition extends SsaDefinition instanceof BaseSsaUpdate { + GuardsInput::Expr getDefinition() { + super.getDefiningExpr().(VariableAssign).getSource() = result or + super.getDefiningExpr().(AssignOp) = result + } + } + + class SsaPhiNode extends SsaDefinition instanceof BaseSsaPhiNode { + predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb) { + super.hasInputFromBlock(inp, bb) + } + } + + predicate additionalNullCheck = LogicInputCommon::additionalNullCheck/4; + + predicate additionalImpliesStep( + GuardsImpl::PreGuard g1, GuardValue v1, GuardsImpl::PreGuard g2, GuardValue v2 + ) { + exists(MethodCall check, int argIndex | + g1 = check and + v1.getDualValue().isThrowsException() and + conditionCheckArgument(check, argIndex, v2.asBooleanValue()) and + g2 = check.getArgument(argIndex) ) } +} + +private module LogicInput_v2 implements GuardsImpl::LogicInputSig { + private import semmle.code.java.dataflow.SSA as SSA + + final private class FinalSsaVariable = SSA::SsaVariable; + + class SsaDefinition extends FinalSsaVariable { + GuardsInput::Expr getARead() { result = this.getAUse() } + } + + class SsaWriteDefinition extends SsaDefinition instanceof SSA::SsaExplicitUpdate { + GuardsInput::Expr getDefinition() { + super.getDefiningExpr().(VariableAssign).getSource() = result or + super.getDefiningExpr().(AssignOp) = result + } + } + + class SsaPhiNode extends SsaDefinition instanceof SSA::SsaPhiNode { + predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb) { + super.hasInputFromBlock(inp, bb) + } + } + + predicate additionalNullCheck = LogicInputCommon::additionalNullCheck/4; + + predicate additionalImpliesStep( + GuardsImpl::PreGuard g1, GuardValue v1, GuardsImpl::PreGuard g2, GuardValue v2 + ) { + LogicInput_v1::additionalImpliesStep(g1, v1, g2, v2) + or + CustomGuard::additionalImpliesStep(g1, v1, g2, v2) + } +} + +private module LogicInput_v3 implements GuardsImpl::LogicInputSig { + private import semmle.code.java.dataflow.IntegerGuards as IntegerGuards + import LogicInput_v2 + + predicate rangeGuard(GuardsImpl::PreGuard guard, GuardValue val, Expr e, int k, boolean upper) { + IntegerGuards::rangeGuard(guard, val.asBooleanValue(), e, k, upper) + } + + predicate additionalNullCheck = LogicInputCommon::additionalNullCheck/4; + + predicate additionalImpliesStep = LogicInput_v2::additionalImpliesStep/4; +} + +private module CustomGuardInput implements Guards_v2::CustomGuardInputSig { + private import semmle.code.java.dataflow.SSA + + private int parameterPosition() { result in [-1, any(Parameter p).getPosition()] } + + /** A parameter position represented by an integer. */ + class ParameterPosition extends int { + ParameterPosition() { this = parameterPosition() } + } + + /** An argument position represented by an integer. */ + class ArgumentPosition extends int { + ArgumentPosition() { this = parameterPosition() } + } + + /** Holds if arguments at position `apos` match parameters at position `ppos`. */ + pragma[inline] + predicate parameterMatch(ParameterPosition ppos, ArgumentPosition apos) { ppos = apos } + + final private class FinalMethod = Method; + + class BooleanMethod extends FinalMethod { + BooleanMethod() { + super.getReturnType().(PrimitiveType).hasName("boolean") and + not super.isOverridable() + } + + LogicInput_v2::SsaDefinition getParameter(ParameterPosition ppos) { + exists(Parameter p | + super.getParameter(ppos) = p and + not p.isVarargs() and + result.(SsaImplicitInit).isParameterDefinition(p) + ) + } + + GuardsInput::Expr getAReturnExpr() { + exists(ReturnStmt ret | + this = ret.getEnclosingCallable() and + ret.getResult() = result + ) + } + } + + private predicate booleanMethodCall(MethodCall call, BooleanMethod m) { + call.getMethod().getSourceDeclaration() = m + } + + class BooleanMethodCall extends GuardsInput::Expr instanceof MethodCall { + BooleanMethodCall() { booleanMethodCall(this, _) } + + BooleanMethod getMethod() { booleanMethodCall(this, result) } + + GuardsInput::Expr getArgument(ArgumentPosition apos) { result = super.getArgument(apos) } + } +} + +class GuardValue = GuardsImpl::GuardValue; + +private module CustomGuard = Guards_v2::CustomGuard; + +/** INTERNAL: Don't use. */ +module Guards_v1 = GuardsImpl::Logic; + +/** INTERNAL: Don't use. */ +module Guards_v2 = GuardsImpl::Logic; + +/** INTERNAL: Don't use. */ +module Guards_v3 = GuardsImpl::Logic; + +/** INTERNAL: Don't use. */ +predicate implies_v3(Guard g1, boolean b1, Guard g2, boolean b2) { + Guards_v3::boolImplies(g1, any(GuardValue v | v.asBooleanValue() = b1), g2, + any(GuardValue v | v.asBooleanValue() = b2)) +} + +/** + * A guard. This may be any expression whose value determines subsequent + * control flow. It may also be a switch case, which as a guard is considered + * to evaluate to either true or false depending on whether the case matches. + */ +final class Guard extends Guards_v3::Guard { + /** Gets the immediately enclosing callable whose body contains this guard. */ + Callable getEnclosingCallable() { + result = this.(Expr).getEnclosingCallable() or + result = this.(SwitchCase).getEnclosingCallable() + } /** * Holds if this guard tests whether `testedExpr` has type `testedType`. @@ -231,211 +545,14 @@ final class Guard extends ExprParent { else restricted = false ) } - - /** - * Holds if the evaluation of this guard to `branch` corresponds to the edge - * from `bb1` to `bb2`. - */ - predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { - exists(ConditionBlock cb | - cb = bb1 and - cb.getCondition() = this and - bb2 = cb.getTestSuccessor(branch) - ) - or - exists(SwitchCase sc, ControlFlowNode pred | - sc = this and - // Pattern cases are handled as ConditionBlocks above. - not sc instanceof PatternCase and - branch = true and - bb2.getFirstNode() = sc.getControlFlowNode() and - isNonFallThroughPredecessor(sc, pred) and - bb1 = pred.getBasicBlock() - ) - or - preconditionBranchEdge(this, bb1, bb2, branch) - } - - /** - * Holds if this guard evaluating to `branch` directly controls the block - * `controlled`. That is, the `true`- or `false`-successor of this guard (as - * given by `branch`) dominates `controlled`. - */ - predicate directlyControls(BasicBlock controlled, boolean branch) { - exists(ConditionBlock cb | - cb.getCondition() = this and - cb.controls(controlled, branch) - ) - or - switchCaseControls(this, controlled) and branch = true - or - preconditionControls(this, controlled, branch) - } - - /** - * Holds if this guard evaluating to `branch` controls the control-flow - * branch edge from `bb1` to `bb2`. That is, following the edge from - * `bb1` to `bb2` implies that this guard evaluated to `branch`. - */ - predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { - guardControlsBranchEdge_v3(this, bb1, bb2, branch) - } - - /** - * Holds if this guard evaluating to `branch` directly or indirectly controls - * the block `controlled`. That is, the evaluation of `controlled` is - * dominated by this guard evaluating to `branch`. - */ - predicate controls(BasicBlock controlled, boolean branch) { - guardControls_v3(this, controlled, branch) - } -} - -private predicate switchCaseControls(SwitchCase sc, BasicBlock bb) { - exists(BasicBlock caseblock | - // Pattern cases are handled as condition blocks - not sc instanceof PatternCase and - caseblock.getFirstNode() = sc.getControlFlowNode() and - caseblock.dominates(bb) and - // Check we can't fall through from a previous block: - forall(ControlFlowNode pred | pred = sc.getControlFlowNode().getAPredecessor() | - isNonFallThroughPredecessor(sc, pred) - ) - ) -} - -private predicate preconditionBranchEdge( - MethodCall ma, BasicBlock bb1, BasicBlock bb2, boolean branch -) { - conditionCheckArgument(ma, _, branch) and - bb1.getLastNode() = ma.getControlFlowNode() and - bb2.getFirstNode() = bb1.getLastNode().getANormalSuccessor() -} - -private predicate preconditionControls(MethodCall ma, BasicBlock controlled, boolean branch) { - exists(BasicBlock check, BasicBlock succ | - preconditionBranchEdge(ma, check, succ, branch) and - dominatingEdge(check, succ) and - succ.dominates(controlled) - ) } /** - * INTERNAL: Use `Guards.controls` instead. + * INTERNAL: Use `Guard.controls` instead. * * Holds if `guard.controls(controlled, branch)`, except this only relies on * BaseSSA-based reasoning. */ -predicate guardControls_v1(Guard guard, BasicBlock controlled, boolean branch) { - guard.directlyControls(controlled, branch) - or - exists(Guard g, boolean b | - guardControls_v1(g, controlled, b) and - implies_v1(g, b, guard, branch) - ) -} - -/** - * INTERNAL: Use `Guards.controls` instead. - * - * Holds if `guard.controls(controlled, branch)`, except this doesn't rely on - * RangeAnalysis. - */ -predicate guardControls_v2(Guard guard, BasicBlock controlled, boolean branch) { - guard.directlyControls(controlled, branch) - or - exists(Guard g, boolean b | - guardControls_v2(g, controlled, b) and - implies_v2(g, b, guard, branch) - ) -} - -pragma[nomagic] -private predicate guardControls_v3(Guard guard, BasicBlock controlled, boolean branch) { - guard.directlyControls(controlled, branch) - or - exists(Guard g, boolean b | - guardControls_v3(g, controlled, b) and - implies_v3(g, b, guard, branch) - ) -} - -pragma[nomagic] -private predicate guardControlsBranchEdge_v2( - Guard guard, BasicBlock bb1, BasicBlock bb2, boolean branch -) { - guard.hasBranchEdge(bb1, bb2, branch) - or - exists(Guard g, boolean b | - guardControlsBranchEdge_v2(g, bb1, bb2, b) and - implies_v2(g, b, guard, branch) - ) -} - -pragma[nomagic] -private predicate guardControlsBranchEdge_v3( - Guard guard, BasicBlock bb1, BasicBlock bb2, boolean branch -) { - guard.hasBranchEdge(bb1, bb2, branch) - or - exists(Guard g, boolean b | - guardControlsBranchEdge_v3(g, bb1, bb2, b) and - implies_v3(g, b, guard, branch) - ) -} - -/** INTERNAL: Use `Guard` instead. */ -final class Guard_v2 extends Guard { - /** - * Holds if this guard evaluating to `branch` controls the control-flow - * branch edge from `bb1` to `bb2`. That is, following the edge from - * `bb1` to `bb2` implies that this guard evaluated to `branch`. - */ - predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { - guardControlsBranchEdge_v2(this, bb1, bb2, branch) - } - - /** - * Holds if this guard evaluating to `branch` directly or indirectly controls - * the block `controlled`. That is, the evaluation of `controlled` is - * dominated by this guard evaluating to `branch`. - */ - predicate controls(BasicBlock controlled, boolean branch) { - guardControls_v2(this, controlled, branch) - } -} - -private predicate equalityGuard(Guard g, Expr e1, Expr e2, boolean polarity) { - exists(EqualityTest eqtest | - eqtest = g and - polarity = eqtest.polarity() and - eqtest.hasOperands(e1, e2) - ) - or - exists(MethodCall ma | - ma = g and - ma.getMethod() instanceof EqualsMethod and - polarity = true and - ma.getAnArgument() = e1 and - ma.getQualifier() = e2 - ) - or - exists(MethodCall ma, Method equals | - ma = g and - ma.getMethod() = equals and - polarity = true and - equals.hasName("equals") and - equals.getNumberOfParameters() = 2 and - equals.getDeclaringType().hasQualifiedName("java.util", "Objects") and - ma.getArgument(0) = e1 and - ma.getArgument(1) = e2 - ) - or - exists(ConstCase cc | - cc = g and - polarity = true and - cc.getSelectorExpr() = e1 and - cc.getValue() = e2 and - strictcount(cc.getValue(_)) = 1 - ) +predicate guardControls_v1(Guards_v1::Guard guard, BasicBlock controlled, boolean branch) { + guard.controls(controlled, branch) } diff --git a/java/ql/lib/semmle/code/java/controlflow/internal/GuardsLogic.qll b/java/ql/lib/semmle/code/java/controlflow/internal/GuardsLogic.qll deleted file mode 100644 index 4cb3bc74f97f..000000000000 --- a/java/ql/lib/semmle/code/java/controlflow/internal/GuardsLogic.qll +++ /dev/null @@ -1,396 +0,0 @@ -/** - * Provides predicates for working with the internal logic of the `Guards` - * library. - */ - -import java -import semmle.code.java.controlflow.Guards -private import Preconditions -private import semmle.code.java.dataflow.SSA -private import semmle.code.java.dataflow.internal.BaseSSA -private import semmle.code.java.dataflow.NullGuards -private import semmle.code.java.dataflow.IntegerGuards - -/** - * Holds if the assumption that `g1` has been evaluated to `b1` implies that - * `g2` has been evaluated to `b2`, that is, the evaluation of `g2` to `b2` - * dominates the evaluation of `g1` to `b1`. - * - * Restricted to BaseSSA-based reasoning. - */ -predicate implies_v1(Guard g1, boolean b1, Guard g2, boolean b2) { - g1.(AndBitwiseExpr).getAnOperand() = g2 and b1 = true and b2 = true - or - g1.(OrBitwiseExpr).getAnOperand() = g2 and b1 = false and b2 = false - or - g1.(AssignAndExpr).getSource() = g2 and b1 = true and b2 = true - or - g1.(AssignOrExpr).getSource() = g2 and b1 = false and b2 = false - or - g1.(AndLogicalExpr).getAnOperand() = g2 and b1 = true and b2 = true - or - g1.(OrLogicalExpr).getAnOperand() = g2 and b1 = false and b2 = false - or - g1.(LogNotExpr).getExpr() = g2 and - b1 = b2.booleanNot() and - b1 = [true, false] - or - exists(EqualityTest eqtest, boolean polarity, BooleanLiteral boollit | - eqtest = g1 and - eqtest.hasOperands(g2, boollit) and - eqtest.polarity() = polarity and - b1 = [true, false] and - b2 = b1.booleanXor(polarity).booleanXor(boollit.getBooleanValue()) - ) - or - exists(ConditionalExpr cond, boolean branch, BooleanLiteral boollit, boolean boolval | - cond.getBranchExpr(branch) = boollit and - cond = g1 and - boolval = boollit.getBooleanValue() and - b1 = boolval.booleanNot() and - ( - g2 = cond.getCondition() and b2 = branch.booleanNot() - or - g2 = cond.getABranchExpr() and b2 = b1 - ) - ) - or - g1.(DefaultCase).getSwitch().getAConstCase() = g2 and b1 = true and b2 = false - or - g1.(DefaultCase).getSwitchExpr().getAConstCase() = g2 and b1 = true and b2 = false - or - exists(MethodCall check, int argIndex | check = g1 | - conditionCheckArgument(check, argIndex, _) and - g2 = check.getArgument(argIndex) and - b1 = [true, false] and - b2 = b1 - ) - or - exists(BaseSsaUpdate vbool | - vbool.getDefiningExpr().(VariableAssign).getSource() = g2 or - vbool.getDefiningExpr().(AssignOp) = g2 - | - vbool.getAUse() = g1 and - b1 = [true, false] and - b2 = b1 - ) - or - g1.(AssignExpr).getSource() = g2 and b2 = b1 and b1 = [true, false] -} - -/** - * Holds if the assumption that `g1` has been evaluated to `b1` implies that - * `g2` has been evaluated to `b2`, that is, the evaluation of `g2` to `b2` - * dominates the evaluation of `g1` to `b1`. - * - * Allows full use of SSA but is restricted to pre-RangeAnalysis reasoning. - */ -predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) { - implies_v1(g1, b1, g2, b2) - or - exists(SsaExplicitUpdate vbool | - vbool.getDefiningExpr().(VariableAssign).getSource() = g2 or - vbool.getDefiningExpr().(AssignOp) = g2 - | - vbool.getAUse() = g1 and - b1 = [true, false] and - b2 = b1 - ) - or - exists(SsaVariable v, AbstractValue k | - // If `v = g2 ? k : ...` or `v = g2 ? ... : k` then a guard - // proving `v != k` ensures that `g2` evaluates to `b2`. - conditionalAssignVal(v, g2, b2.booleanNot(), k) and - guardImpliesNotEqual1(g1, b1, v, k) - ) - or - exists(SsaVariable v, Expr e, AbstractValue k | - // If `v = g2 ? k : ...` and all other assignments to `v` are different from - // `k` then a guard proving `v == k` ensures that `g2` evaluates to `b2`. - uniqueValue(v, e, k) and - guardImpliesEqual(g1, b1, v, k) and - g2.directlyControls(e.getBasicBlock(), b2) and - not g2.directlyControls(g1.getBasicBlock(), b2) - ) -} - -/** - * Holds if the assumption that `g1` has been evaluated to `b1` implies that - * `g2` has been evaluated to `b2`, that is, the evaluation of `g2` to `b2` - * dominates the evaluation of `g1` to `b1`. - */ -cached -predicate implies_v3(Guard g1, boolean b1, Guard g2, boolean b2) { - implies_v2(g1, b1, g2, b2) - or - exists(SsaVariable v, AbstractValue k | - // If `v = g2 ? k : ...` or `v = g2 ? ... : k` then a guard - // proving `v != k` ensures that `g2` evaluates to `b2`. - conditionalAssignVal(v, g2, b2.booleanNot(), k) and - guardImpliesNotEqual2(g1, b1, v, k) - ) - or - exists(SsaVariable v | - conditionalAssign(v, g2, b2.booleanNot(), clearlyNotNullExpr()) and - guardImpliesEqual(g1, b1, v, TAbsValNull()) - ) -} - -private newtype TAbstractValue = - TAbsValNull() or - TAbsValInt(int i) { exists(CompileTimeConstantExpr c | c.getIntValue() = i) } or - TAbsValChar(string c) { exists(CharacterLiteral lit | lit.getValue() = c) } or - TAbsValString(string s) { exists(StringLiteral lit | lit.getValue() = s) } or - TAbsValEnum(EnumConstant c) - -/** The value of a constant expression. */ -abstract private class AbstractValue extends TAbstractValue { - abstract string toString(); - - /** Gets an expression whose value is this abstract value. */ - abstract Expr getExpr(); -} - -private class AbsValNull extends AbstractValue, TAbsValNull { - override string toString() { result = "null" } - - override Expr getExpr() { result = alwaysNullExpr() } -} - -private class AbsValInt extends AbstractValue, TAbsValInt { - int i; - - AbsValInt() { this = TAbsValInt(i) } - - override string toString() { result = i.toString() } - - override Expr getExpr() { result.(CompileTimeConstantExpr).getIntValue() = i } -} - -private class AbsValChar extends AbstractValue, TAbsValChar { - string c; - - AbsValChar() { this = TAbsValChar(c) } - - override string toString() { result = c } - - override Expr getExpr() { result.(CharacterLiteral).getValue() = c } -} - -private class AbsValString extends AbstractValue, TAbsValString { - string s; - - AbsValString() { this = TAbsValString(s) } - - override string toString() { result = s } - - override Expr getExpr() { result.(CompileTimeConstantExpr).getStringValue() = s } -} - -private class AbsValEnum extends AbstractValue, TAbsValEnum { - EnumConstant c; - - AbsValEnum() { this = TAbsValEnum(c) } - - override string toString() { result = c.toString() } - - override Expr getExpr() { result = c.getAnAccess() } -} - -/** - * Holds if `v` can have a value that is not representable as an `AbstractValue`. - */ -private predicate hasPossibleUnknownValue(SsaVariable v) { - exists(SsaVariable def | v.getAnUltimateDefinition() = def | - def instanceof SsaImplicitUpdate - or - def instanceof SsaImplicitInit - or - exists(VariableUpdate upd | upd = def.(SsaExplicitUpdate).getDefiningExpr() | - not exists(upd.(VariableAssign).getSource()) - ) - or - exists(VariableAssign a, Expr e | - a = def.(SsaExplicitUpdate).getDefiningExpr() and - e = possibleValue(a.getSource()) and - not exists(AbstractValue val | val.getExpr() = e) - ) - ) -} - -/** - * Gets a sub-expression of `e` whose value can flow to `e` through - * `ConditionalExpr`s. - */ -private Expr possibleValue(Expr e) { - result = possibleValue(e.(ConditionalExpr).getABranchExpr()) - or - result = e and not e instanceof ConditionalExpr -} - -/** - * Gets an ultimate definition of `v` that is not itself a phi node. The - * boolean `fromBackEdge` indicates whether the flow from `result` to `v` goes - * through a back edge. - */ -SsaVariable getADefinition(SsaVariable v, boolean fromBackEdge) { - result = v and not v instanceof SsaPhiNode and fromBackEdge = false - or - exists(SsaVariable inp, BasicBlock bb, boolean fbe | - v.(SsaPhiNode).hasInputFromBlock(inp, bb) and - result = getADefinition(inp, fbe) and - (if v.getBasicBlock().dominates(bb) then fromBackEdge = true else fromBackEdge = fbe) - ) -} - -/** - * Holds if `e` equals `k` and may be assigned to `v`. The boolean - * `fromBackEdge` indicates whether the flow from `e` to `v` goes through a - * back edge. - */ -private predicate possibleValue(SsaVariable v, boolean fromBackEdge, Expr e, AbstractValue k) { - not hasPossibleUnknownValue(v) and - exists(SsaExplicitUpdate def | - def = getADefinition(v, fromBackEdge) and - e = possibleValue(def.getDefiningExpr().(VariableAssign).getSource()) and - k.getExpr() = e - ) -} - -/** - * Holds if `e` equals `k` and may be assigned to `v` without going through - * back edges, and all other possible ultimate definitions of `v` are different - * from `k`. The trivial case where `v` is an `SsaExplicitUpdate` with `e` as - * the only possible value is excluded. - */ -private predicate uniqueValue(SsaVariable v, Expr e, AbstractValue k) { - possibleValue(v, false, e, k) and - forex(Expr other, AbstractValue otherval | possibleValue(v, _, other, otherval) and other != e | - otherval != k - ) -} - -/** - * Holds if `v1` and `v2` have the same value in `bb`. - */ -private predicate equalVarsInBlock(BasicBlock bb, SsaVariable v1, SsaVariable v2) { - exists(Guard guard, boolean branch | - guard.isEquality(v1.getAUse(), v2.getAUse(), branch) and - guardControls_v1(guard, bb, branch) - ) -} - -/** - * Holds if `guard` evaluating to `branch` implies that `v` equals `k`. - */ -private predicate guardImpliesEqual(Guard guard, boolean branch, SsaVariable v, AbstractValue k) { - exists(SsaVariable v0 | - guard.isEquality(v0.getAUse(), k.getExpr(), branch) and - (v = v0 or equalVarsInBlock(guard.getBasicBlock(), v0, v)) - ) -} - -private BasicBlock getAGuardBranchSuccessor(Guard g, boolean branch) { - result.getFirstNode() = g.(Expr).getControlFlowNode().(ConditionNode).getABranchSuccessor(branch) - or - result.getFirstNode() = g.(SwitchCase).getControlFlowNode() and branch = true -} - -/** - * Holds if `guard` dominates `phi` and `guard` evaluating to `branch` controls the definition - * `upd = e` where `upd` is a possible input to `phi`. - */ -private predicate guardControlsPhiBranch( - SsaExplicitUpdate upd, SsaPhiNode phi, Guard guard, boolean branch, Expr e -) { - guard.directlyControls(upd.getBasicBlock(), branch) and - upd.getDefiningExpr().(VariableAssign).getSource() = e and - upd = phi.getAPhiInput() and - guard.getBasicBlock().strictlyDominates(phi.getBasicBlock()) -} - -/** - * Holds if `v` is conditionally assigned `e` under the condition that `guard` evaluates to `branch`. - * - * The evaluation of `guard` dominates the definition of `v` and `guard` evaluating to `branch` - * implies that `e` is assigned to `v`. In particular, this allows us to conclude that if `v` has - * a value different from `e` then `guard` must have evaluated to `branch.booleanNot()`. - */ -private predicate conditionalAssign(SsaVariable v, Guard guard, boolean branch, Expr e) { - exists(ConditionalExpr c | - v.(SsaExplicitUpdate).getDefiningExpr().(VariableAssign).getSource() = c and - guard = c.getCondition() - | - e = c.getBranchExpr(branch) - ) - or - exists(SsaExplicitUpdate upd, SsaPhiNode phi | - phi = v and - guardControlsPhiBranch(upd, phi, guard, branch, e) and - not guard.directlyControls(phi.getBasicBlock(), branch) and - forall(SsaVariable other | other != upd and other = phi.getAPhiInput() | - guard.directlyControls(other.getBasicBlock(), branch.booleanNot()) - or - other.getBasicBlock().dominates(guard.getBasicBlock()) and - not other.isLiveAtEndOfBlock(getAGuardBranchSuccessor(guard, branch)) - ) - ) -} - -/** - * Holds if `v` is conditionally assigned `val` under the condition that `guard` evaluates to `branch`. - */ -private predicate conditionalAssignVal(SsaVariable v, Guard guard, boolean branch, AbstractValue val) { - conditionalAssign(v, guard, branch, val.getExpr()) -} - -private predicate relevantEq(SsaVariable v, AbstractValue val) { - conditionalAssignVal(v, _, _, val) - or - exists(SsaVariable v0 | - conditionalAssignVal(v0, _, _, val) and - equalVarsInBlock(_, v0, v) - ) -} - -/** - * Holds if the evaluation of `guard` to `branch` implies that `v` does not have the value `val`. - */ -private predicate guardImpliesNotEqual1( - Guard guard, boolean branch, SsaVariable v, AbstractValue val -) { - exists(SsaVariable v0 | - relevantEq(v0, val) and - ( - guard.isEquality(v0.getAUse(), val.getExpr(), branch.booleanNot()) - or - exists(AbstractValue val2 | - guard.isEquality(v0.getAUse(), val2.getExpr(), branch) and - val != val2 - ) - or - guard.(InstanceOfExpr).getExpr() = sameValue(v0, _) and branch = true and val = TAbsValNull() - ) and - (v = v0 or equalVarsInBlock(guard.getBasicBlock(), v0, v)) - ) -} - -/** - * Holds if the evaluation of `guard` to `branch` implies that `v` does not have the value `val`. - */ -private predicate guardImpliesNotEqual2( - Guard guard, boolean branch, SsaVariable v, AbstractValue val -) { - exists(SsaVariable v0 | - relevantEq(v0, val) and - ( - guard = directNullGuard(v0, branch, false) and val = TAbsValNull() - or - exists(int k | - guard = integerGuard(v0.getAUse(), branch, k, false) and - val = TAbsValInt(k) - ) - ) and - (v = v0 or equalVarsInBlock(guard.getBasicBlock(), v0, v)) - ) -} diff --git a/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll b/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll index 5fde238a4b65..d28a2e0e30cb 100644 --- a/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll +++ b/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll @@ -4,7 +4,7 @@ import java import SSA -private import semmle.code.java.controlflow.internal.GuardsLogic +private import semmle.code.java.controlflow.Guards private import semmle.code.java.frameworks.apache.Collections private import IntegerGuards @@ -40,6 +40,7 @@ EqualityTest varEqualityTestExpr(SsaVariable v1, SsaVariable v2, boolean isEqual isEqualExpr = result.polarity() } +/** Gets an expression that is provably not `null`. */ Expr baseNotNullExpr() { result instanceof ClassInstanceExpr or @@ -183,50 +184,19 @@ predicate nullCheckMethod(Method m, boolean branch, boolean isnull) { * is true, and non-null if `isnull` is false. */ Expr basicNullGuard(Expr e, boolean branch, boolean isnull) { - exists(EqualityTest eqtest, boolean polarity | - eqtest = result and - eqtest.hasOperands(e, any(NullLiteral n)) and - polarity = eqtest.polarity() and - ( - branch = true and isnull = polarity - or - branch = false and isnull = polarity.booleanNot() - ) - ) - or - result.(InstanceOfExpr).getExpr() = e and branch = true and isnull = false - or - exists(MethodCall call | - call = result and - call.getAnArgument() = e and - nullCheckMethod(call.getMethod(), branch, isnull) - ) - or - exists(EqualityTest eqtest | - eqtest = result and - eqtest.hasOperands(e, clearlyNotNullExpr()) and - isnull = false and - branch = eqtest.polarity() - ) - or - result = enumConstEquality(e, branch, _) and isnull = false + Guards_v3::nullGuard(result, any(GuardValue v | v.asBooleanValue() = branch), e, isnull) } /** + * DEPRECATED: Use `basicNullGuard` instead. + * * Gets an expression that directly tests whether a given expression, `e`, is null or not. * * If `result` evaluates to `branch`, then `e` is guaranteed to be null if `isnull` * is true, and non-null if `isnull` is false. */ -Expr basicOrCustomNullGuard(Expr e, boolean branch, boolean isnull) { +deprecated Expr basicOrCustomNullGuard(Expr e, boolean branch, boolean isnull) { result = basicNullGuard(e, branch, isnull) - or - exists(MethodCall call, Method m, int ix | - call = result and - call.getArgument(ix) = e and - call.getMethod().getSourceDeclaration() = m and - m = customNullGuard(ix, branch, isnull) - ) } /** @@ -236,72 +206,42 @@ Expr basicOrCustomNullGuard(Expr e, boolean branch, boolean isnull) { * is true, and non-null if `isnull` is false. */ Expr directNullGuard(SsaVariable v, boolean branch, boolean isnull) { - result = basicOrCustomNullGuard(sameValue(v, _), branch, isnull) + result = basicNullGuard(sameValue(v, _), branch, isnull) } /** + * DEPRECATED: Use `nullGuardControls`/`nullGuardControlsBranchEdge` instead. + * * Gets a `Guard` that tests (possibly indirectly) whether a given SSA variable is null or not. * * If `result` evaluates to `branch`, then `v` is guaranteed to be null if `isnull` * is true, and non-null if `isnull` is false. */ -Guard nullGuard(SsaVariable v, boolean branch, boolean isnull) { - result = directNullGuard(v, branch, isnull) or - exists(boolean branch0 | implies_v3(result, branch, nullGuard(v, branch0, isnull), branch0)) +deprecated Guard nullGuard(SsaVariable v, boolean branch, boolean isnull) { + result = directNullGuard(v, branch, isnull) } /** - * A return statement in a non-overridable method that on a return value of - * `retval` allows the conclusion that the parameter `p` either is null or - * non-null as specified by `isnull`. + * Holds if there exists a null check on `v`, such that taking the branch edge + * from `bb1` to `bb2` implies that `v` is guaranteed to be null if `isnull` is + * true, and non-null if `isnull` is false. */ -private predicate validReturnInCustomNullGuard( - ReturnStmt ret, Parameter p, boolean retval, boolean isnull -) { - exists(Method m | - ret.getEnclosingCallable() = m and - p.getCallable() = m and - m.getReturnType().(PrimitiveType).hasName("boolean") and - not p.isVarargs() and - p.getType() instanceof RefType and - not m.isOverridable() - ) and - exists(SsaImplicitInit ssa | ssa.isParameterDefinition(p) | - nullGuardedReturn(ret, ssa, isnull) and - (retval = true or retval = false) - or - exists(Expr res | res = ret.getResult() | res = nullGuard(ssa, retval, isnull)) - ) -} - -private predicate nullGuardedReturn(ReturnStmt ret, SsaImplicitInit ssa, boolean isnull) { - exists(boolean branch | - nullGuard(ssa, branch, isnull).directlyControls(ret.getBasicBlock(), branch) +predicate nullGuardControlsBranchEdge(SsaVariable v, boolean isnull, BasicBlock bb1, BasicBlock bb2) { + exists(GuardValue gv | + Guards_v3::ssaControlsBranchEdge(v, bb1, bb2, gv) and + gv.isNullness(isnull) ) } -pragma[nomagic] -private Method returnStmtGetEnclosingCallable(ReturnStmt ret) { - ret.getEnclosingCallable() = result -} - /** - * Gets a non-overridable method with a boolean return value that performs a null-check - * on the `index`th parameter. A return value equal to `retval` allows us to conclude - * that the argument either is null or non-null as specified by `isnull`. + * Holds if there exists a null check on `v` that controls `bb`, such that in + * `bb` `v` is guaranteed to be null if `isnull` is true, and non-null if + * `isnull` is false. */ -private Method customNullGuard(int index, boolean retval, boolean isnull) { - exists(Parameter p | - p.getCallable() = result and - p.getPosition() = index and - forex(ReturnStmt ret | - returnStmtGetEnclosingCallable(ret) = result and - exists(Expr res | res = ret.getResult() | - not res.(BooleanLiteral).getBooleanValue() = retval.booleanNot() - ) - | - validReturnInCustomNullGuard(ret, p, retval, isnull) - ) +predicate nullGuardControls(SsaVariable v, boolean isnull, BasicBlock bb) { + exists(GuardValue gv | + Guards_v3::ssaControls(v, bb, gv) and + gv.isNullness(isnull) ) } diff --git a/java/ql/lib/semmle/code/java/dataflow/Nullness.qll b/java/ql/lib/semmle/code/java/dataflow/Nullness.qll index 36ad96c497f0..a4b007e1b13e 100644 --- a/java/ql/lib/semmle/code/java/dataflow/Nullness.qll +++ b/java/ql/lib/semmle/code/java/dataflow/Nullness.qll @@ -141,9 +141,9 @@ private ControlFlowNode varDereference(SsaVariable v, VarAccess va) { private ControlFlowNode ensureNotNull(SsaVariable v) { result = varDereference(v, _) or - exists(AssertTrueMethod m | result.asCall() = m.getACheck(nullGuard(v, true, false))) + exists(AssertTrueMethod m | result.asCall() = m.getACheck(directNullGuard(v, true, false))) or - exists(AssertFalseMethod m | result.asCall() = m.getACheck(nullGuard(v, false, false))) + exists(AssertFalseMethod m | result.asCall() = m.getACheck(directNullGuard(v, false, false))) or exists(AssertNotNullMethod m | result.asCall() = m.getACheck(v.getAUse())) or @@ -339,7 +339,7 @@ private predicate nullVarStep( not assertFail(mid, _) and bb = mid.getASuccessor() and not impossibleEdge(mid, bb) and - not exists(boolean branch | nullGuard(midssa, branch, false).hasBranchEdge(mid, bb, branch)) and + not nullGuardControlsBranchEdge(midssa, false, mid, bb) and not (leavingFinally(mid, bb, true) and midstoredcompletion = true) and if bb.getFirstNode().asStmt() = any(TryStmt try | | try.getFinally()) then @@ -476,6 +476,11 @@ private ConditionBlock ssaEnumConstEquality(SsaVariable v, boolean polarity, Enu result.getCondition() = enumConstEquality(v.getAUse(), polarity, c) } +private predicate conditionChecksNull(ConditionBlock cond, SsaVariable v, boolean branchIsNull) { + nullGuardControlsBranchEdge(v, true, cond, cond.getTestSuccessor(branchIsNull)) and + nullGuardControlsBranchEdge(v, false, cond, cond.getTestSuccessor(branchIsNull.booleanNot())) +} + /** A pair of correlated conditions for a given NPE candidate. */ private predicate correlatedConditions( SsaSourceVariable npecand, ConditionBlock cond1, ConditionBlock cond2, boolean inverted @@ -491,10 +496,8 @@ private predicate correlatedConditions( ) or exists(SsaVariable v, boolean branch1, boolean branch2 | - cond1.getCondition() = nullGuard(v, branch1, true) and - cond1.getCondition() = nullGuard(v, branch1.booleanNot(), false) and - cond2.getCondition() = nullGuard(v, branch2, true) and - cond2.getCondition() = nullGuard(v, branch2.booleanNot(), false) and + conditionChecksNull(cond1, v, branch1) and + conditionChecksNull(cond2, v, branch2) and inverted = branch1.booleanXor(branch2) ) or @@ -620,7 +623,7 @@ private Expr trackingVarGuard( SsaVariable trackssa, SsaSourceVariable trackvar, TrackVarKind kind, boolean branch, boolean isA ) { exists(Expr init | trackingVar(_, trackssa, trackvar, kind, init) | - result = basicOrCustomNullGuard(trackvar.getAnAccess(), branch, isA) and + result = basicNullGuard(trackvar.getAnAccess(), branch, isA) and kind = TrackVarKindNull() or result = trackvar.getAnAccess() and @@ -831,15 +834,13 @@ predicate alwaysNullDeref(SsaSourceVariable v, VarAccess va) { def.(SsaExplicitUpdate).getDefiningExpr().(VariableAssign).getSource() = alwaysNullExpr() ) or - exists(boolean branch | - nullGuard(ssa, branch, true).directlyControls(bb, branch) and - not clearlyNotNull(ssa) - ) + nullGuardControls(ssa, true, bb) and + not clearlyNotNull(ssa) | // Exclude fields as they might not have an accurate ssa representation. not v.getVariable() instanceof Field and firstVarDereferenceInBlock(bb, ssa, va) and ssa.getSourceVariable() = v and - not exists(boolean branch | nullGuard(ssa, branch, false).directlyControls(bb, branch)) + not nullGuardControls(ssa, false, bb) ) } diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll index 64f68b9c075a..4bbac387c896 100644 --- a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll +++ b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll @@ -66,7 +66,6 @@ import java private import SSA private import RangeUtils -private import semmle.code.java.controlflow.internal.GuardsLogic private import semmle.code.java.security.RandomDataSource private import SignAnalysis private import semmle.code.java.Reflection @@ -79,7 +78,7 @@ module Sem implements Semantic { private import java as J private import SSA as SSA private import RangeUtils as RU - private import semmle.code.java.controlflow.internal.GuardsLogic as GL + private import semmle.code.java.controlflow.Guards as G class Expr = J::Expr; @@ -219,7 +218,7 @@ module Sem implements Semantic { int getBlockId1(BasicBlock bb) { idOf(bb, result) } - class Guard extends GL::Guard_v2 { + class Guard extends G::Guards_v2::Guard { Expr asExpr() { result = this } } diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll b/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll index 444fec8f8659..a9b8abf90b63 100644 --- a/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll +++ b/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll @@ -4,7 +4,7 @@ import java private import SSA -private import semmle.code.java.controlflow.internal.GuardsLogic +private import semmle.code.java.controlflow.Guards private import semmle.code.java.Constants private import semmle.code.java.dataflow.RangeAnalysis private import codeql.rangeanalysis.internal.RangeUtils diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll index 7778f6ebc353..0a4e6c8d062a 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll @@ -60,8 +60,6 @@ module SsaFlow { cached private module Cached { - private import semmle.code.java.controlflow.internal.GuardsLogic as GuardsLogic - cached newtype TNode = TExprNode(Expr e) { diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll index b639947793b5..8aebfc672861 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll @@ -14,7 +14,7 @@ module Private { class Expr = J::Expr; - class Guard = G::Guard_v2; + class Guard = G::Guards_v2::Guard; class ConstantIntegerExpr = RU::ConstantIntegerExpr; diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll index 04e896b26011..72dd345d69e2 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll @@ -12,7 +12,7 @@ module Private { class ConstantIntegerExpr = RU::ConstantIntegerExpr; - class Guard = G::Guard_v2; + class Guard = G::Guards_v2::Guard; class SsaVariable = Ssa::SsaVariable; diff --git a/java/ql/lib/semmle/code/java/security/ArithmeticCommon.qll b/java/ql/lib/semmle/code/java/security/ArithmeticCommon.qll index 785dce3da7ed..2628ae7ba4d0 100644 --- a/java/ql/lib/semmle/code/java/security/ArithmeticCommon.qll +++ b/java/ql/lib/semmle/code/java/security/ArithmeticCommon.qll @@ -7,7 +7,6 @@ private import semmle.code.java.dataflow.DataFlow private import semmle.code.java.dataflow.RangeAnalysis private import semmle.code.java.dataflow.RangeUtils private import semmle.code.java.dataflow.SignAnalysis -private import semmle.code.java.controlflow.internal.GuardsLogic /** * Holds if the type of `exp` is narrower than or equal to `numType`, diff --git a/java/ql/src/Language Abuse/UselessNullCheck.ql b/java/ql/src/Language Abuse/UselessNullCheck.ql index d95b528c4c46..92041ca9e4a2 100644 --- a/java/ql/src/Language Abuse/UselessNullCheck.ql +++ b/java/ql/src/Language Abuse/UselessNullCheck.ql @@ -21,7 +21,7 @@ where guardSuggestsExprMaybeNull(guard, e) and e = clearlyNotNullExpr(reason) and ( - if reason instanceof Guard + if reason = directNullGuard(_, _, _) then msg = "This check is useless. $@ cannot be null at this check, since it is guarded by $@." else if reason != e diff --git a/java/ql/test/library-tests/guards/Guards.java b/java/ql/test/library-tests/guards/Guards.java index 877c1827166b..b75e549d1669 100644 --- a/java/ql/test/library-tests/guards/Guards.java +++ b/java/ql/test/library-tests/guards/Guards.java @@ -26,7 +26,7 @@ void t1(int[] a, String s) { } int sz = a != null ? a.length : 0; for (int i = 0; i < sz; i++) { - chk(); // $ guarded='a != null:true' guarded='i < sz:true' + chk(); // $ guarded='a != null:true' guarded='i < sz:true' guarded='sz:not 0' guarded='...?...:...:not 0' guarded='a.length:not 0' guarded='a:not null' int e = a[i]; if (e > 2) break; } @@ -36,26 +36,26 @@ void t1(int[] a, String s) { s = "bar"; switch (s) { case "bar": - chk(); // $ guarded='s:match "bar"' + chk(); // $ guarded='s:match "bar"' guarded='s:bar' break; case "foo": - chk(); // $ guarded='s:match "foo"' guarded=g(3):false + chk(); // $ guarded='s:match "foo"' guarded='s:foo' guarded=g(3):false break; default: - chk(); // $ guarded='s:non-match "bar"' guarded='s:non-match "foo"' guarded='s:match default' guarded=g(3):false + chk(); // $ guarded='s:non-match "bar"' guarded='s:non-match "foo"' guarded='s:not bar' guarded='s:not foo' guarded='s:match default' guarded=g(3):false break; } Object o = g(4) ? null : s; if (o instanceof String) { - chk(); // $ guarded=...instanceof...:true guarded=g(4):false + chk(); // $ guarded=...instanceof...:true guarded='o:not null' guarded='...?...:...:not null' guarded=g(4):false guarded='s:not null' } } void t2() { checkTrue(g(1), "A"); checkFalse(g(2), "B"); - chk(); // $ guarded=checkTrue(A):true guarded=g(1):true guarded=checkFalse(B):false guarded=g(2):false + chk(); // $ guarded='checkTrue(...):no exception' guarded=g(1):true guarded='checkFalse(...):no exception' guarded=g(2):false } void t3() { @@ -86,23 +86,23 @@ void t4() { if (g("Alt2")) x = Val.E2; if (g(3)) x = Val.E3; // unique value if (x == null) - chk(); // $ guarded='x == null:true' guarded=g(3):false + chk(); // $ guarded='x == null:true' guarded='x:null' guarded=g(1):false guarded=g(2):false guarded=g(Alt2):false guarded=g(3):false switch (x) { case E1: - chk(); // $ guarded='x:match E1' guarded=g(1):true guarded=g(3):false + chk(); // $ guarded='x:match E1' guarded='x:E1' guarded=g(1):true guarded=g(2):false guarded=g(Alt2):false guarded=g(3):false break; case E2: - chk(); // $ guarded='x:match E2' guarded=g(3):false + chk(); // $ guarded='x:match E2' guarded='x:E2' guarded=g(3):false break; case E3: - chk(); // $ guarded='x:match E3' guarded=g(3):true + chk(); // $ guarded='x:match E3' guarded='x:E3' guarded=g(3):true break; } Object o = g(4) ? new Object() : null; if (o == null) { - chk(); // $ guarded='o == null:true' guarded=g(4):false + chk(); // $ guarded='o == null:true' guarded='o:null' guarded='...?...:...:null' guarded=g(4):false } else { - chk(); // $ guarded='o == null:false' guarded=g(4):true + chk(); // $ guarded='o == null:false' guarded='o:not null' guarded='...?...:...:not null' guarded=g(4):true } } @@ -112,7 +112,7 @@ void t5(String foo) { base = "/user"; } if (base.equals("/")) - chk(); // $ guarded=equals(/):true guarded='base == null:false' + chk(); // $ guarded=equals(/):true guarded='base:/' guarded='base:not null' guarded='base == null:false' guarded='foo:/' guarded='foo:not null' } void t6() { @@ -122,9 +122,9 @@ void t6() { if (g(2)) { } } if (o != null) { - chk(); // $ guarded='o != null:true' + chk(); // $ guarded='o != null:true' guarded='o:not null' guarded=g(1):true } else { - chk(); // $ guarded='o != null:false' guarded=g(1):false + chk(); // $ guarded='o != null:false' guarded='o:null' guarded=g(1):false } } diff --git a/java/ql/test/library-tests/guards/GuardsInline.expected b/java/ql/test/library-tests/guards/GuardsInline.expected index 1aaf791acabd..c45d536b7e9a 100644 --- a/java/ql/test/library-tests/guards/GuardsInline.expected +++ b/java/ql/test/library-tests/guards/GuardsInline.expected @@ -8,19 +8,30 @@ | Guards.java:25:7:25:11 | chk(...) | b:false | | Guards.java:25:7:25:11 | chk(...) | g(1):true | | Guards.java:25:7:25:11 | chk(...) | g(2):false | +| Guards.java:29:7:29:11 | chk(...) | '...?...:...:not 0' | | Guards.java:29:7:29:11 | chk(...) | 'a != null:true' | +| Guards.java:29:7:29:11 | chk(...) | 'a.length:not 0' | +| Guards.java:29:7:29:11 | chk(...) | 'a:not null' | | Guards.java:29:7:29:11 | chk(...) | 'i < sz:true' | +| Guards.java:29:7:29:11 | chk(...) | 'sz:not 0' | +| Guards.java:39:9:39:13 | chk(...) | 's:bar' | | Guards.java:39:9:39:13 | chk(...) | 's:match "bar"' | +| Guards.java:42:9:42:13 | chk(...) | 's:foo' | | Guards.java:42:9:42:13 | chk(...) | 's:match "foo"' | | Guards.java:42:9:42:13 | chk(...) | g(3):false | | Guards.java:45:9:45:13 | chk(...) | 's:match default' | | Guards.java:45:9:45:13 | chk(...) | 's:non-match "bar"' | | Guards.java:45:9:45:13 | chk(...) | 's:non-match "foo"' | +| Guards.java:45:9:45:13 | chk(...) | 's:not bar' | +| Guards.java:45:9:45:13 | chk(...) | 's:not foo' | | Guards.java:45:9:45:13 | chk(...) | g(3):false | +| Guards.java:51:7:51:11 | chk(...) | '...?...:...:not null' | +| Guards.java:51:7:51:11 | chk(...) | 'o:not null' | +| Guards.java:51:7:51:11 | chk(...) | 's:not null' | | Guards.java:51:7:51:11 | chk(...) | ...instanceof...:true | | Guards.java:51:7:51:11 | chk(...) | g(4):false | -| Guards.java:58:5:58:9 | chk(...) | checkFalse(B):false | -| Guards.java:58:5:58:9 | chk(...) | checkTrue(A):true | +| Guards.java:58:5:58:9 | chk(...) | 'checkFalse(...):no exception' | +| Guards.java:58:5:58:9 | chk(...) | 'checkTrue(...):no exception' | | Guards.java:58:5:58:9 | chk(...) | g(1):true | | Guards.java:58:5:58:9 | chk(...) | g(2):false | | Guards.java:64:7:64:11 | chk(...) | 'g(...) && ... \|\| ...:true' | @@ -37,22 +48,42 @@ | Guards.java:72:7:72:11 | chk(...) | g(4):false | | Guards.java:72:7:72:11 | chk(...) | g(5):true | | Guards.java:89:7:89:11 | chk(...) | 'x == null:true' | +| Guards.java:89:7:89:11 | chk(...) | 'x:null' | +| Guards.java:89:7:89:11 | chk(...) | g(1):false | +| Guards.java:89:7:89:11 | chk(...) | g(2):false | | Guards.java:89:7:89:11 | chk(...) | g(3):false | +| Guards.java:89:7:89:11 | chk(...) | g(Alt2):false | +| Guards.java:92:9:92:13 | chk(...) | 'x:E1' | | Guards.java:92:9:92:13 | chk(...) | 'x:match E1' | | Guards.java:92:9:92:13 | chk(...) | g(1):true | +| Guards.java:92:9:92:13 | chk(...) | g(2):false | | Guards.java:92:9:92:13 | chk(...) | g(3):false | +| Guards.java:92:9:92:13 | chk(...) | g(Alt2):false | +| Guards.java:95:9:95:13 | chk(...) | 'x:E2' | | Guards.java:95:9:95:13 | chk(...) | 'x:match E2' | | Guards.java:95:9:95:13 | chk(...) | g(3):false | +| Guards.java:98:9:98:13 | chk(...) | 'x:E3' | | Guards.java:98:9:98:13 | chk(...) | 'x:match E3' | | Guards.java:98:9:98:13 | chk(...) | g(3):true | +| Guards.java:103:7:103:11 | chk(...) | '...?...:...:null' | | Guards.java:103:7:103:11 | chk(...) | 'o == null:true' | +| Guards.java:103:7:103:11 | chk(...) | 'o:null' | | Guards.java:103:7:103:11 | chk(...) | g(4):false | +| Guards.java:105:7:105:11 | chk(...) | '...?...:...:not null' | | Guards.java:105:7:105:11 | chk(...) | 'o == null:false' | +| Guards.java:105:7:105:11 | chk(...) | 'o:not null' | | Guards.java:105:7:105:11 | chk(...) | g(4):true | | Guards.java:115:7:115:11 | chk(...) | 'base == null:false' | +| Guards.java:115:7:115:11 | chk(...) | 'base:/' | +| Guards.java:115:7:115:11 | chk(...) | 'base:not null' | +| Guards.java:115:7:115:11 | chk(...) | 'foo:/' | +| Guards.java:115:7:115:11 | chk(...) | 'foo:not null' | | Guards.java:115:7:115:11 | chk(...) | equals(/):true | | Guards.java:125:7:125:11 | chk(...) | 'o != null:true' | +| Guards.java:125:7:125:11 | chk(...) | 'o:not null' | +| Guards.java:125:7:125:11 | chk(...) | g(1):true | | Guards.java:127:7:127:11 | chk(...) | 'o != null:false' | +| Guards.java:127:7:127:11 | chk(...) | 'o:null' | | Guards.java:127:7:127:11 | chk(...) | g(1):false | | Guards.java:139:9:139:13 | chk(...) | 'i < a.length:true' | | Guards.java:139:9:139:13 | chk(...) | found:true | diff --git a/java/ql/test/library-tests/guards/GuardsInline.ql b/java/ql/test/library-tests/guards/GuardsInline.ql index 54386f9777a9..1b854659d87b 100644 --- a/java/ql/test/library-tests/guards/GuardsInline.ql +++ b/java/ql/test/library-tests/guards/GuardsInline.ql @@ -39,4 +39,13 @@ query predicate guarded(MethodCall mc, string guard) { not exists(ppGuard(g, branch)) and guard = g.toString() + ":" + branch ) + or + mc.getMethod().hasName("chk") and + exists(Guard g, BasicBlock bb, GuardValue val | + g.valueControls(bb, val) and + not exists(val.asBooleanValue()) and + mc.getBasicBlock() = bb + | + guard = "'" + g.toString() + ":" + val + "'" + ) } diff --git a/java/ql/test/library-tests/guards12/guard.expected b/java/ql/test/library-tests/guards12/guard.expected index 0980e891d84a..fade9fd4e8fc 100644 --- a/java/ql/test/library-tests/guards12/guard.expected +++ b/java/ql/test/library-tests/guards12/guard.expected @@ -51,13 +51,5 @@ hasBranchEdge | Test.java:12:7:12:17 | case ... | Test.java:9:13:9:13 | s | Test.java:12:12:12:14 | "d" | true | false | Test.java:13:7:13:16 | default | | Test.java:12:7:12:17 | case ... | Test.java:9:13:9:13 | s | Test.java:12:12:12:14 | "d" | true | true | Test.java:12:7:12:17 | case ... | | Test.java:17:26:17:33 | ... == ... | Test.java:17:26:17:28 | len | Test.java:17:33:17:33 | 4 | true | true | Test.java:17:38:17:40 | { ... } | -| Test.java:18:7:18:17 | case ... | Test.java:16:13:16:13 | s | Test.java:18:12:18:14 | "e" | true | false | Test.java:19:7:19:16 | default | -| Test.java:18:7:18:17 | case ... | Test.java:16:13:16:13 | s | Test.java:18:12:18:14 | "e" | true | true | Test.java:18:7:18:17 | case ... | -| Test.java:22:7:22:17 | case ... | Test.java:21:13:21:41 | ...?...:... | Test.java:22:12:22:14 | "f" | true | false | Test.java:25:7:25:16 | default | -| Test.java:22:7:22:17 | case ... | Test.java:21:13:21:41 | ...?...:... | Test.java:22:12:22:14 | "f" | true | true | Test.java:22:7:22:17 | case ... | | Test.java:23:27:23:34 | ... == ... | Test.java:23:27:23:29 | len | Test.java:23:34:23:34 | 4 | true | true | Test.java:23:39:23:41 | { ... } | -| Test.java:24:7:24:17 | case ... | Test.java:21:13:21:41 | ...?...:... | Test.java:24:12:24:14 | "g" | true | false | Test.java:25:7:25:16 | default | -| Test.java:24:7:24:17 | case ... | Test.java:21:13:21:41 | ...?...:... | Test.java:24:12:24:14 | "g" | true | true | Test.java:24:7:24:17 | case ... | -| Test.java:28:7:28:15 | case ... | Test.java:27:13:27:13 | s | Test.java:28:12:28:14 | "h" | true | false | Test.java:33:7:33:14 | default | | Test.java:28:7:28:15 | case ... | Test.java:27:13:27:13 | s | Test.java:28:12:28:14 | "h" | true | true | Test.java:28:7:28:15 | case ... | -| Test.java:30:7:30:15 | case ... | Test.java:27:13:27:13 | s | Test.java:30:12:30:14 | "i" | true | false | Test.java:33:7:33:14 | default | diff --git a/java/ql/test/library-tests/guards12/guard.ql b/java/ql/test/library-tests/guards12/guard.ql index cff2845ad9f8..d53dfdbc7135 100644 --- a/java/ql/test/library-tests/guards12/guard.ql +++ b/java/ql/test/library-tests/guards12/guard.ql @@ -1,8 +1,8 @@ import java import semmle.code.java.controlflow.Guards -query predicate hasBranchEdge(Guard g, BasicBlock bb1, BasicBlock bb2, boolean branch) { - g.hasBranchEdge(bb1, bb2, branch) +query predicate hasBranchEdge(Guard g, BasicBlock bb1, BasicBlock bb2, GuardValue branch) { + g.hasValueBranchEdge(bb1, bb2, branch) } from Guard g, BasicBlock bb, boolean branch, Expr e1, Expr e2, boolean pol diff --git a/java/ql/test/query-tests/Nullness/C.java b/java/ql/test/query-tests/Nullness/C.java index ac6a5f291da2..317569e64c1d 100644 --- a/java/ql/test/query-tests/Nullness/C.java +++ b/java/ql/test/query-tests/Nullness/C.java @@ -60,7 +60,7 @@ public void ex5(boolean hasArr, int[] arr) { arrLen = arr == null ? 0 : arr.length; } if (arrLen > 0) { - arr[0] = 0; // NPE - false positive + arr[0] = 0; // OK } } diff --git a/java/ql/test/query-tests/Nullness/NullMaybe.expected b/java/ql/test/query-tests/Nullness/NullMaybe.expected index 80cf8f00f8d5..a19fae57e74e 100644 --- a/java/ql/test/query-tests/Nullness/NullMaybe.expected +++ b/java/ql/test/query-tests/Nullness/NullMaybe.expected @@ -24,7 +24,6 @@ | C.java:10:17:10:18 | a3 | Variable $@ may be null at this access because of $@ assignment. | C.java:8:5:8:21 | long[] a3 | a3 | C.java:8:12:8:20 | a3 | this | | C.java:21:7:21:8 | s1 | Variable $@ may be null at this access because of $@ assignment. | C.java:14:5:14:30 | String s1 | s1 | C.java:17:7:17:24 | ...=... | this | | C.java:51:7:51:11 | slice | Variable $@ may be null at this access because of $@ assignment. | C.java:43:5:43:30 | List slice | slice | C.java:43:18:43:29 | slice | this | -| C.java:63:7:63:9 | arr | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:57:35:57:43 | arr | arr | C.java:60:16:60:26 | ... == ... | this | | C.java:100:7:100:10 | arr2 | Variable $@ may be null at this access because of $@ assignment. | C.java:95:5:95:22 | int[] arr2 | arr2 | C.java:95:11:95:21 | arr2 | this | | C.java:110:25:110:27 | obj | Variable $@ may be null at this access because of $@ assignment. | C.java:106:5:106:30 | Object obj | obj | C.java:118:13:118:22 | ...=... | this | | C.java:137:7:137:10 | obj2 | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:131:5:131:23 | Object obj2 | obj2 | C.java:132:9:132:20 | ... != ... | this | From 42b1b12aa10374e5eac2d2629d39f189183030b8 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 27 May 2025 10:43:35 +0200 Subject: [PATCH 16/22] Java: Fix qltests --- .../library-tests/guards/guardslogic.expected | 28 ++++++------- .../test/library-tests/guards/guardslogic.ql | 9 +++-- .../guards/guardspreconditions.expected | 40 +++++++++---------- .../guards/guardspreconditions.ql | 9 +++-- 4 files changed, 44 insertions(+), 42 deletions(-) diff --git a/java/ql/test/library-tests/guards/guardslogic.expected b/java/ql/test/library-tests/guards/guardslogic.expected index 6536ad3b69fa..29c11ccd153d 100644 --- a/java/ql/test/library-tests/guards/guardslogic.expected +++ b/java/ql/test/library-tests/guards/guardslogic.expected @@ -30,33 +30,33 @@ | Logic.java:29:16:29:19 | g(...) | false | Logic.java:30:30:31:5 | { ... } | | Logic.java:29:16:29:19 | g(...) | true | Logic.java:29:23:29:26 | null | | Logic.java:30:9:30:27 | ...instanceof... | true | Logic.java:30:30:31:5 | { ... } | -| Logic.java:35:5:35:29 | checkTrue(...) | true | Logic.java:36:5:36:28 | ; | -| Logic.java:35:5:35:29 | checkTrue(...) | true | Logic.java:37:5:37:15 | if (...) | -| Logic.java:35:5:35:29 | checkTrue(...) | true | Logic.java:37:17:39:5 | { ... } | -| Logic.java:35:5:35:29 | checkTrue(...) | true | Logic.java:40:5:40:18 | var ...; | +| Logic.java:35:5:35:29 | checkTrue(...) | no exception | Logic.java:36:5:36:28 | ; | +| Logic.java:35:5:35:29 | checkTrue(...) | no exception | Logic.java:37:5:37:15 | if (...) | +| Logic.java:35:5:35:29 | checkTrue(...) | no exception | Logic.java:37:17:39:5 | { ... } | +| Logic.java:35:5:35:29 | checkTrue(...) | no exception | Logic.java:40:5:40:18 | var ...; | | Logic.java:35:15:35:19 | ... > ... | true | Logic.java:36:5:36:28 | ; | | Logic.java:35:15:35:19 | ... > ... | true | Logic.java:37:5:37:15 | if (...) | | Logic.java:35:15:35:19 | ... > ... | true | Logic.java:37:17:39:5 | { ... } | | Logic.java:35:15:35:19 | ... > ... | true | Logic.java:40:5:40:18 | var ...; | -| Logic.java:36:5:36:27 | checkFalse(...) | false | Logic.java:37:5:37:15 | if (...) | -| Logic.java:36:5:36:27 | checkFalse(...) | false | Logic.java:37:17:39:5 | { ... } | -| Logic.java:36:5:36:27 | checkFalse(...) | false | Logic.java:40:5:40:18 | var ...; | +| Logic.java:36:5:36:27 | checkFalse(...) | no exception | Logic.java:37:5:37:15 | if (...) | +| Logic.java:36:5:36:27 | checkFalse(...) | no exception | Logic.java:37:17:39:5 | { ... } | +| Logic.java:36:5:36:27 | checkFalse(...) | no exception | Logic.java:40:5:40:18 | var ...; | | Logic.java:36:16:36:21 | g(...) | false | Logic.java:37:5:37:15 | if (...) | | Logic.java:36:16:36:21 | g(...) | false | Logic.java:37:17:39:5 | { ... } | | Logic.java:36:16:36:21 | g(...) | false | Logic.java:40:5:40:18 | var ...; | | Logic.java:37:9:37:14 | ... > ... | true | Logic.java:37:17:39:5 | { ... } | | Logic.java:44:10:44:10 | b | false | Logic.java:44:33:44:35 | msg | -| Logic.java:52:5:52:29 | checkTrue(...) | true | Logic.java:53:5:53:28 | ; | -| Logic.java:52:5:52:29 | checkTrue(...) | true | Logic.java:54:5:54:15 | if (...) | -| Logic.java:52:5:52:29 | checkTrue(...) | true | Logic.java:54:17:56:5 | { ... } | -| Logic.java:52:5:52:29 | checkTrue(...) | true | Logic.java:57:5:57:18 | var ...; | +| Logic.java:52:5:52:29 | checkTrue(...) | no exception | Logic.java:53:5:53:28 | ; | +| Logic.java:52:5:52:29 | checkTrue(...) | no exception | Logic.java:54:5:54:15 | if (...) | +| Logic.java:52:5:52:29 | checkTrue(...) | no exception | Logic.java:54:17:56:5 | { ... } | +| Logic.java:52:5:52:29 | checkTrue(...) | no exception | Logic.java:57:5:57:18 | var ...; | | Logic.java:52:24:52:28 | ... > ... | true | Logic.java:53:5:53:28 | ; | | Logic.java:52:24:52:28 | ... > ... | true | Logic.java:54:5:54:15 | if (...) | | Logic.java:52:24:52:28 | ... > ... | true | Logic.java:54:17:56:5 | { ... } | | Logic.java:52:24:52:28 | ... > ... | true | Logic.java:57:5:57:18 | var ...; | -| Logic.java:53:5:53:27 | checkFalse(...) | false | Logic.java:54:5:54:15 | if (...) | -| Logic.java:53:5:53:27 | checkFalse(...) | false | Logic.java:54:17:56:5 | { ... } | -| Logic.java:53:5:53:27 | checkFalse(...) | false | Logic.java:57:5:57:18 | var ...; | +| Logic.java:53:5:53:27 | checkFalse(...) | no exception | Logic.java:54:5:54:15 | if (...) | +| Logic.java:53:5:53:27 | checkFalse(...) | no exception | Logic.java:54:17:56:5 | { ... } | +| Logic.java:53:5:53:27 | checkFalse(...) | no exception | Logic.java:57:5:57:18 | var ...; | | Logic.java:53:21:53:26 | g(...) | false | Logic.java:54:5:54:15 | if (...) | | Logic.java:53:21:53:26 | g(...) | false | Logic.java:54:17:56:5 | { ... } | | Logic.java:53:21:53:26 | g(...) | false | Logic.java:57:5:57:18 | var ...; | diff --git a/java/ql/test/library-tests/guards/guardslogic.ql b/java/ql/test/library-tests/guards/guardslogic.ql index afbb313d6645..f2ce9fdaa365 100644 --- a/java/ql/test/library-tests/guards/guardslogic.ql +++ b/java/ql/test/library-tests/guards/guardslogic.ql @@ -1,8 +1,9 @@ import java import semmle.code.java.controlflow.Guards -from Guard g, BasicBlock bb, boolean branch +from Guard g, BasicBlock bb, GuardValue gv where - g.controls(bb, branch) and - g.getEnclosingCallable().getDeclaringType().hasName("Logic") -select g, branch, bb + g.valueControls(bb, gv) and + g.getEnclosingCallable().getDeclaringType().hasName("Logic") and + (exists(gv.asBooleanValue()) or gv.isThrowsException() or gv.getDualValue().isThrowsException()) +select g, gv, bb diff --git a/java/ql/test/library-tests/guards/guardspreconditions.expected b/java/ql/test/library-tests/guards/guardspreconditions.expected index 9c0136c8e6e9..41080a5dab6e 100644 --- a/java/ql/test/library-tests/guards/guardspreconditions.expected +++ b/java/ql/test/library-tests/guards/guardspreconditions.expected @@ -1,20 +1,20 @@ -| Preconditions.java:8:9:8:31 | assertTrue(...) | true | Preconditions.java:9:9:9:18 | ; | -| Preconditions.java:13:9:13:32 | assertTrue(...) | true | Preconditions.java:14:9:14:18 | ; | -| Preconditions.java:18:9:18:33 | assertFalse(...) | false | Preconditions.java:19:9:19:18 | ; | -| Preconditions.java:23:9:23:32 | assertFalse(...) | false | Preconditions.java:24:9:24:18 | ; | -| Preconditions.java:28:9:28:41 | assertTrue(...) | true | Preconditions.java:29:9:29:18 | ; | -| Preconditions.java:33:9:33:42 | assertTrue(...) | true | Preconditions.java:34:9:34:18 | ; | -| Preconditions.java:38:9:38:43 | assertFalse(...) | false | Preconditions.java:39:9:39:18 | ; | -| Preconditions.java:43:9:43:42 | assertFalse(...) | false | Preconditions.java:44:9:44:18 | ; | -| Preconditions.java:48:9:48:35 | assertTrue(...) | true | Preconditions.java:49:9:49:18 | ; | -| Preconditions.java:53:9:53:36 | assertTrue(...) | true | Preconditions.java:54:9:54:18 | ; | -| Preconditions.java:58:9:58:37 | assertFalse(...) | false | Preconditions.java:59:9:59:18 | ; | -| Preconditions.java:63:9:63:36 | assertFalse(...) | false | Preconditions.java:64:9:64:18 | ; | -| Preconditions.java:68:9:68:45 | assertTrue(...) | true | Preconditions.java:69:9:69:18 | ; | -| Preconditions.java:73:9:73:46 | assertTrue(...) | true | Preconditions.java:74:9:74:18 | ; | -| Preconditions.java:78:9:78:47 | assertFalse(...) | false | Preconditions.java:79:9:79:18 | ; | -| Preconditions.java:83:9:83:46 | assertFalse(...) | false | Preconditions.java:84:9:84:18 | ; | -| Preconditions.java:88:9:88:15 | t(...) | true | Preconditions.java:89:9:89:18 | ; | -| Preconditions.java:93:9:93:16 | t(...) | true | Preconditions.java:94:9:94:18 | ; | -| Preconditions.java:98:9:98:16 | f(...) | false | Preconditions.java:99:9:99:18 | ; | -| Preconditions.java:103:9:103:15 | f(...) | false | Preconditions.java:104:9:104:18 | ; | +| Preconditions.java:8:9:8:31 | assertTrue(...) | no exception | Preconditions.java:9:9:9:18 | ; | +| Preconditions.java:13:9:13:32 | assertTrue(...) | no exception | Preconditions.java:14:9:14:18 | ; | +| Preconditions.java:18:9:18:33 | assertFalse(...) | no exception | Preconditions.java:19:9:19:18 | ; | +| Preconditions.java:23:9:23:32 | assertFalse(...) | no exception | Preconditions.java:24:9:24:18 | ; | +| Preconditions.java:28:9:28:41 | assertTrue(...) | no exception | Preconditions.java:29:9:29:18 | ; | +| Preconditions.java:33:9:33:42 | assertTrue(...) | no exception | Preconditions.java:34:9:34:18 | ; | +| Preconditions.java:38:9:38:43 | assertFalse(...) | no exception | Preconditions.java:39:9:39:18 | ; | +| Preconditions.java:43:9:43:42 | assertFalse(...) | no exception | Preconditions.java:44:9:44:18 | ; | +| Preconditions.java:48:9:48:35 | assertTrue(...) | no exception | Preconditions.java:49:9:49:18 | ; | +| Preconditions.java:53:9:53:36 | assertTrue(...) | no exception | Preconditions.java:54:9:54:18 | ; | +| Preconditions.java:58:9:58:37 | assertFalse(...) | no exception | Preconditions.java:59:9:59:18 | ; | +| Preconditions.java:63:9:63:36 | assertFalse(...) | no exception | Preconditions.java:64:9:64:18 | ; | +| Preconditions.java:68:9:68:45 | assertTrue(...) | no exception | Preconditions.java:69:9:69:18 | ; | +| Preconditions.java:73:9:73:46 | assertTrue(...) | no exception | Preconditions.java:74:9:74:18 | ; | +| Preconditions.java:78:9:78:47 | assertFalse(...) | no exception | Preconditions.java:79:9:79:18 | ; | +| Preconditions.java:83:9:83:46 | assertFalse(...) | no exception | Preconditions.java:84:9:84:18 | ; | +| Preconditions.java:88:9:88:15 | t(...) | no exception | Preconditions.java:89:9:89:18 | ; | +| Preconditions.java:93:9:93:16 | t(...) | no exception | Preconditions.java:94:9:94:18 | ; | +| Preconditions.java:98:9:98:16 | f(...) | no exception | Preconditions.java:99:9:99:18 | ; | +| Preconditions.java:103:9:103:15 | f(...) | no exception | Preconditions.java:104:9:104:18 | ; | diff --git a/java/ql/test/library-tests/guards/guardspreconditions.ql b/java/ql/test/library-tests/guards/guardspreconditions.ql index 12c823e9638c..77e4a4e48c08 100644 --- a/java/ql/test/library-tests/guards/guardspreconditions.ql +++ b/java/ql/test/library-tests/guards/guardspreconditions.ql @@ -1,8 +1,9 @@ import java import semmle.code.java.controlflow.Guards -from Guard g, BasicBlock bb, boolean branch +from Guard g, BasicBlock bb, GuardValue gv where - g.controls(bb, branch) and - g.getEnclosingCallable().getDeclaringType().hasName("Preconditions") -select g, branch, bb + g.valueControls(bb, gv) and + g.getEnclosingCallable().getDeclaringType().hasName("Preconditions") and + (gv.isThrowsException() or gv.getDualValue().isThrowsException()) +select g, gv, bb From d4c897f8e2afdb364f5f57a5cf2c95baa0d55ae4 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 27 May 2025 14:40:54 +0200 Subject: [PATCH 17/22] Java: Fix perf issue. --- java/ql/lib/semmle/code/java/dataflow/FlowSteps.qll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/java/ql/lib/semmle/code/java/dataflow/FlowSteps.qll b/java/ql/lib/semmle/code/java/dataflow/FlowSteps.qll index d081a6289ecd..fb491e91e097 100644 --- a/java/ql/lib/semmle/code/java/dataflow/FlowSteps.qll +++ b/java/ql/lib/semmle/code/java/dataflow/FlowSteps.qll @@ -160,7 +160,7 @@ private class NumberTaintPreservingCallable extends TaintPreservingCallable { int argument; NumberTaintPreservingCallable() { - this.getDeclaringType().getAnAncestor().hasQualifiedName("java.lang", "Number") and + this.getDeclaringType().getASourceSupertype*().hasQualifiedName("java.lang", "Number") and ( this instanceof Constructor and argument = 0 From 5a34a1a51b1efb36bdfba48d1bcdf6d4318d7a00 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 16 Jun 2025 11:19:20 +0200 Subject: [PATCH 18/22] Shared: Try caching. --- shared/controlflow/codeql/controlflow/Guards.qll | 3 +++ 1 file changed, 3 insertions(+) diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index 9733114613b3..275a3ee644b9 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -807,12 +807,14 @@ module Make Input> { * Calculates the transitive closure of all the guard implication steps * starting from a given set of base cases. */ + cached module ImpliesTC { /** * Holds if `tgtGuard` evaluating to `tgtVal` implies that `guard` * evaluates to `v`. */ pragma[nomagic] + cached predicate guardControls(Guard guard, GuardValue v, Guard tgtGuard, GuardValue tgtVal) { baseGuardValue(tgtGuard, tgtVal) and guard = tgtGuard and @@ -844,6 +846,7 @@ module Make Input> { * evaluates to `v`. */ pragma[nomagic] + cached predicate ssaControls(SsaDefinition def, GuardValue v, Guard tgtGuard, GuardValue tgtVal) { exists(Guard g0 | guardControls(g0, v, tgtGuard, tgtVal) and From 73810a6d859b0d7ff4873fb4e72ba6e048be58b9 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 17 Jun 2025 10:08:28 +0200 Subject: [PATCH 19/22] Java: Fix perf issue. --- .../ql/lib/semmle/code/java/frameworks/struts/StrutsActions.qll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/java/ql/lib/semmle/code/java/frameworks/struts/StrutsActions.qll b/java/ql/lib/semmle/code/java/frameworks/struts/StrutsActions.qll index 4200e83d4db2..818296ba4b80 100644 --- a/java/ql/lib/semmle/code/java/frameworks/struts/StrutsActions.qll +++ b/java/ql/lib/semmle/code/java/frameworks/struts/StrutsActions.qll @@ -130,7 +130,7 @@ class Struts2PrepareMethod extends Method { */ class Struts2ActionSupportClass extends Class { Struts2ActionSupportClass() { - this.getAStrictAncestor().hasQualifiedName("com.opensymphony.xwork2", "ActionSupport") + this.getASourceSupertype+().hasQualifiedName("com.opensymphony.xwork2", "ActionSupport") } /** From 4645856f09801909c95a0cd3466586c2ce07906f Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 17 Jun 2025 13:37:04 +0200 Subject: [PATCH 20/22] Java: document FP --- java/ql/test/query-tests/Nullness/C.java | 10 ++++++++++ java/ql/test/query-tests/Nullness/NullMaybe.expected | 3 +++ 2 files changed, 13 insertions(+) diff --git a/java/ql/test/query-tests/Nullness/C.java b/java/ql/test/query-tests/Nullness/C.java index 317569e64c1d..eccf6382c156 100644 --- a/java/ql/test/query-tests/Nullness/C.java +++ b/java/ql/test/query-tests/Nullness/C.java @@ -244,4 +244,14 @@ public void ex17() { } xs[0]++; // OK } + + public void ex18(boolean b, int[] xs, Object related) { + assert (!b && xs == null && related == null) || + (b && xs != null && related != null) || + (b && xs == null && related == null); + if (b) { + if (related == null) { return; } + xs[0] = 42; // FP - correlated conditions fails to recognize assert edges + } + } } diff --git a/java/ql/test/query-tests/Nullness/NullMaybe.expected b/java/ql/test/query-tests/Nullness/NullMaybe.expected index a19fae57e74e..a65d1f643c11 100644 --- a/java/ql/test/query-tests/Nullness/NullMaybe.expected +++ b/java/ql/test/query-tests/Nullness/NullMaybe.expected @@ -32,6 +32,9 @@ | C.java:207:9:207:11 | obj | Variable $@ may be null at this access because of $@ assignment. | C.java:201:5:201:22 | Object obj | obj | C.java:201:12:201:21 | obj | this | | C.java:219:9:219:10 | o1 | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:212:20:212:28 | o1 | o1 | C.java:213:9:213:18 | ... == ... | this | | C.java:233:7:233:8 | xs | Variable $@ may be null at this access because of $@ assignment. | C.java:231:5:231:56 | int[] xs | xs | C.java:231:11:231:55 | xs | this | +| C.java:254:7:254:8 | xs | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:248:31:248:38 | xs | xs | C.java:249:19:249:28 | ... == ... | this | +| C.java:254:7:254:8 | xs | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:248:31:248:38 | xs | xs | C.java:250:18:250:27 | ... != ... | this | +| C.java:254:7:254:8 | xs | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:248:31:248:38 | xs | xs | C.java:251:18:251:27 | ... == ... | this | | F.java:11:5:11:7 | obj | Variable $@ may be null at this access as suggested by $@ null guard. | F.java:8:18:8:27 | obj | obj | F.java:9:9:9:19 | ... == ... | this | | F.java:17:5:17:7 | obj | Variable $@ may be null at this access as suggested by $@ null guard. | F.java:14:18:14:27 | obj | obj | F.java:15:9:15:19 | ... == ... | this | | G.java:20:12:20:12 | s | Variable $@ may be null at this access as suggested by $@ null guard. | G.java:3:27:3:34 | s | s | G.java:5:9:5:17 | ... == ... | this | From 5ddddaecdcda0e0e0024ca1841a4dfcdef33878e Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 17 Jun 2025 14:01:23 +0200 Subject: [PATCH 21/22] Java: Add change note. --- java/ql/src/change-notes/2025-06-17-improved-guards.md | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 java/ql/src/change-notes/2025-06-17-improved-guards.md diff --git a/java/ql/src/change-notes/2025-06-17-improved-guards.md b/java/ql/src/change-notes/2025-06-17-improved-guards.md new file mode 100644 index 000000000000..b49710460f1f --- /dev/null +++ b/java/ql/src/change-notes/2025-06-17-improved-guards.md @@ -0,0 +1,4 @@ +--- +category: minorAnalysis +--- +* Java analysis of guards has been switched to use the new and improved shared guards library. This improves precision of a number of queries, in particular `java/dereferenced-value-may-be-null`, which now has fewer false positives, and `java/useless-null-check` and `java/constant-comparison`, which gain additional true positives. From 6f4adb889229d6bdff7468bfd78bdcc92546b73a Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 25 Jun 2025 14:43:04 +0200 Subject: [PATCH 22/22] Shared: address review comments. --- .../controlflow/codeql/controlflow/Guards.qll | 41 +++++++++++++++---- 1 file changed, 33 insertions(+), 8 deletions(-) diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index 275a3ee644b9..627e0e1694fe 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -11,7 +11,7 @@ * controls the basic block `A`, in this case because the true branch dominates * `A`, but more elaborate controls-relationships may also hold. * For example, in - * ``` + * ```java * int sz = a != null ? a.length : 0; * if (sz != 0) { * // this block is controlled by: @@ -104,6 +104,19 @@ signature module InputSig { predicate strictlyDominates(BasicBlock bb); } + /** + * Holds if `bb1` has `bb2` as a direct successor and the edge between `bb1` + * and `bb2` is a dominating edge. + * + * An edge `(bb1, bb2)` is dominating if there exists a basic block that can + * only be reached from the entry block by going through `(bb1, bb2)`. This + * implies that `(bb1, bb2)` dominates its endpoint `bb2`. I.e., `bb2` can + * only be reached from the entry block by going via `(bb1, bb2)`. + * + * This is a necessary and sufficient condition for an edge to dominate some + * block, and therefore `dominatingEdge(bb1, bb2) and bb2.dominates(bb3)` + * means that the edge `(bb1, bb2)` dominates `bb3`. + */ predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2); class AstNode { @@ -528,6 +541,17 @@ module Make Input> { module Logic { private import LogicInput + /** + * Holds if `guard` evaluating to `v` directly controls `phi` taking the value + * `inp`. This means that `guard` evaluating to `v` must control all the input + * edges to `phi` that read `inp`. + * + * We also require that `guard` dominates `phi` in order to allow logical inferences + * from the value of `phi` to the value of `guard`. + * + * Trivial cases where `guard` controls `phi` itself are excluded, since that makes + * logical inferences from `phi` to `guard` trivial and irrelevant. + */ private predicate guardControlsPhiBranch( Guard guard, GuardValue v, SsaPhiNode phi, SsaDefinition inp ) { @@ -571,6 +595,7 @@ module Make Input> { private predicate guardReadsSsaVar(Guard guard, SsaDefinition def) { def.getARead() = guard or + // A read of `y` can be considered as a read of `x` if guarded by `x == y`. exists(Guard eqtest, SsaDefinition other, boolean branch | guardChecksEqualVars(eqtest, def, other, branch) and other.getARead() = guard and @@ -602,21 +627,21 @@ module Make Input> { * boolean `fromBackEdge` indicates whether the flow from `result` to `v` goes * through a back edge. */ - private SsaDefinition getADefinition(SsaDefinition v, boolean fromBackEdge) { + private SsaDefinition getAnUltimateDefinition(SsaDefinition v, boolean fromBackEdge) { result = v and not v instanceof SsaPhiNode and fromBackEdge = false or exists(SsaDefinition inp, BasicBlock bb, boolean fbe | v.(SsaPhiNode).hasInputFromBlock(inp, bb) and - result = getADefinition(inp, fbe) and + result = getAnUltimateDefinition(inp, fbe) and (if v.getBasicBlock().dominates(bb) then fromBackEdge = true else fromBackEdge = fbe) ) } /** - * Holds if `v` can have a value that is not representable as an `GuardValue`. + * Holds if `v` can have a value that is not representable as a `GuardValue`. */ private predicate hasPossibleUnknownValue(SsaDefinition v) { - exists(SsaDefinition def | def = getADefinition(v, _) | + exists(SsaDefinition def | def = getAnUltimateDefinition(v, _) | not exists(def.(SsaWriteDefinition).getDefinition()) or exists(Expr e | e = possibleValue(def.(SsaWriteDefinition).getDefinition()) | @@ -633,7 +658,7 @@ module Make Input> { private predicate possibleValue(SsaDefinition v, boolean fromBackEdge, Expr e, GuardValue k) { not hasPossibleUnknownValue(v) and exists(SsaWriteDefinition def | - def = getADefinition(v, fromBackEdge) and + def = getAnUltimateDefinition(v, fromBackEdge) and e = possibleValue(def.getDefinition()) and constantHasValue(e, k) ) @@ -676,7 +701,7 @@ module Make Input> { or exists(SsaDefinition def | guardReadsSsaVar(e, def) and - relevantInt(getADefinition(def, _).(SsaWriteDefinition).getDefinition(), k) + relevantInt(getAnUltimateDefinition(def, _).(SsaWriteDefinition).getDefinition(), k) ) } @@ -808,7 +833,7 @@ module Make Input> { * starting from a given set of base cases. */ cached - module ImpliesTC { + private module ImpliesTC { /** * Holds if `tgtGuard` evaluating to `tgtVal` implies that `guard` * evaluates to `v`.