From 5cd03b4c8a33f44cb81af30990666f06ecf7b0b6 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 22 Jul 2025 15:30:06 +0200 Subject: [PATCH 01/10] Guards: Remove CustomGuard nesting in Guards instantiation. --- .../semmle/code/java/controlflow/Guards.qll | 121 +++++++++--------- .../controlflow/codeql/controlflow/Guards.qll | 89 +++++++------ 2 files changed, 110 insertions(+), 100 deletions(-) diff --git a/java/ql/lib/semmle/code/java/controlflow/Guards.qll b/java/ql/lib/semmle/code/java/controlflow/Guards.qll index 8cead5b666bb..d13c54e35ad7 100644 --- a/java/ql/lib/semmle/code/java/controlflow/Guards.qll +++ b/java/ql/lib/semmle/code/java/controlflow/Guards.qll @@ -322,6 +322,58 @@ private module GuardsInput implements SharedGuards::InputSig { Expr getElse() { result = super.getFalseExpr() } } + + class Parameter = J::Parameter; + + 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`. */ + overlay[caller?] + 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() + } + + Parameter getParameter(ParameterPosition ppos) { + super.getParameter(ppos) = result and + not result.isVarargs() + } + + 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) } + } } private module GuardsImpl = SharedGuards::Make; @@ -364,6 +416,10 @@ private module LogicInput_v1 implements GuardsImpl::LogicInputSig { } } + predicate parameterDefinition(Parameter p, SsaDefinition def) { + def.(BaseSsaImplicitInit).isParameterDefinition(p) + } + predicate additionalNullCheck = LogicInputCommon::additionalNullCheck/4; predicate additionalImpliesStep( @@ -400,14 +456,16 @@ private module LogicInput_v2 implements GuardsImpl::LogicInputSig { } } + predicate parameterDefinition(Parameter p, SsaDefinition def) { + def.(SSA::SsaImplicitInit).isParameterDefinition(p) + } + 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) } } @@ -424,67 +482,8 @@ private module LogicInput_v3 implements GuardsImpl::LogicInputSig { 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`. */ - overlay[caller?] - 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; diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index d78d6ec8e8a1..8de0907ee920 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -207,6 +207,46 @@ signature module InputSig { /** Gets the false branch of this expression. */ Expr getElse(); } + + class Parameter { + /** Gets a textual representation of this parameter. */ + string toString(); + + /** Gets the location of this parameter. */ + Location getLocation(); + } + + 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 { + Parameter getParameter(ParameterPosition ppos); + + /** Gets an expression being returned by this method. */ + Expr getAReturnExpr(); + } + + class BooleanMethodCall extends Expr { + BooleanMethod getMethod(); + + Expr getArgument(ArgumentPosition apos); + } } /** Provides guards-related predicates and classes. */ @@ -503,6 +543,8 @@ module Make Input> { predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb); } + predicate parameterDefinition(Parameter p, SsaDefinition def); + /** * Holds if `guard` evaluating to `val` ensures that: * `e <= k` when `upper = true` @@ -525,8 +567,6 @@ module Make Input> { * 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() @@ -859,6 +899,11 @@ module Make Input> { impliesStepSsaGuard(def0, v0, guard, v) ) or + exists(Guard g0, GuardValue v0 | + guardControls(g0, v0, tgtGuard, tgtVal) and + CustomGuard::additionalImpliesStep(g0, v0, guard, v) + ) + or exists(Guard g0, GuardValue v0 | guardControls(g0, v0, tgtGuard, tgtVal) and additionalImpliesStep(g0, v0, guard, v) @@ -902,6 +947,7 @@ module Make Input> { */ predicate nullGuard(Guard guard, GuardValue v, Expr e, boolean isNull) { impliesStep2(guard, v, e, any(GuardValue gv | gv.isNullness(isNull))) or + CustomGuard::additionalImpliesStep(guard, v, e, any(GuardValue gv | gv.isNullness(isNull))) or additionalImpliesStep(guard, v, e, any(GuardValue gv | gv.isNullness(isNull))) } @@ -944,47 +990,12 @@ module Make Input> { ) } - 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 module CustomGuard { final private class FinalExpr = Expr; private class ReturnExpr extends FinalExpr { @@ -1010,7 +1021,7 @@ module Make Input> { ) { exists(BooleanMethod m, SsaDefinition param | m.getAReturnExpr() = ret and - m.getParameter(ppos) = param + parameterDefinition(m.getParameter(ppos), param) | exists(Guard g0, GuardValue v0 | g0.directlyValueControls(ret.getBasicBlock(), v0) and From 439872b8a0ab51eb900fbb99f2ae3e467be063e1 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 22 Jul 2025 15:32:41 +0200 Subject: [PATCH 02/10] Java: Simplify Guards instantiation a bit. --- .../semmle/code/java/controlflow/Guards.qll | 30 +++++++++---------- 1 file changed, 14 insertions(+), 16 deletions(-) diff --git a/java/ql/lib/semmle/code/java/controlflow/Guards.qll b/java/ql/lib/semmle/code/java/controlflow/Guards.qll index d13c54e35ad7..697273d59d74 100644 --- a/java/ql/lib/semmle/code/java/controlflow/Guards.qll +++ b/java/ql/lib/semmle/code/java/controlflow/Guards.qll @@ -392,6 +392,17 @@ private module LogicInputCommon { NullGuards::nullCheckMethod(call.getMethod(), val.asBooleanValue(), isNull) ) } + + 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_v1 implements GuardsImpl::LogicInputSig { @@ -422,16 +433,7 @@ private module LogicInput_v1 implements GuardsImpl::LogicInputSig { 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) - ) - } + predicate additionalImpliesStep = LogicInputCommon::additionalImpliesStep/4; } private module LogicInput_v2 implements GuardsImpl::LogicInputSig { @@ -462,11 +464,7 @@ private module LogicInput_v2 implements GuardsImpl::LogicInputSig { predicate additionalNullCheck = LogicInputCommon::additionalNullCheck/4; - predicate additionalImpliesStep( - GuardsImpl::PreGuard g1, GuardValue v1, GuardsImpl::PreGuard g2, GuardValue v2 - ) { - LogicInput_v1::additionalImpliesStep(g1, v1, g2, v2) - } + predicate additionalImpliesStep = LogicInputCommon::additionalImpliesStep/4; } private module LogicInput_v3 implements GuardsImpl::LogicInputSig { @@ -479,7 +477,7 @@ private module LogicInput_v3 implements GuardsImpl::LogicInputSig { predicate additionalNullCheck = LogicInputCommon::additionalNullCheck/4; - predicate additionalImpliesStep = LogicInput_v2::additionalImpliesStep/4; + predicate additionalImpliesStep = LogicInputCommon::additionalImpliesStep/4; } class GuardValue = GuardsImpl::GuardValue; From a8ad67e3929d40dd7d9cdbd4ec1fdbb7671ff5b2 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 22 Jul 2025 15:33:52 +0200 Subject: [PATCH 03/10] Guards: Rename module. --- shared/controlflow/codeql/controlflow/Guards.qll | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index 8de0907ee920..27cbde2e72a1 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -901,7 +901,7 @@ module Make Input> { or exists(Guard g0, GuardValue v0 | guardControls(g0, v0, tgtGuard, tgtVal) and - CustomGuard::additionalImpliesStep(g0, v0, guard, v) + WrapperGuard::additionalImpliesStep(g0, v0, guard, v) ) or exists(Guard g0, GuardValue v0 | @@ -947,7 +947,7 @@ module Make Input> { */ predicate nullGuard(Guard guard, GuardValue v, Expr e, boolean isNull) { impliesStep2(guard, v, e, any(GuardValue gv | gv.isNullness(isNull))) or - CustomGuard::additionalImpliesStep(guard, v, e, any(GuardValue gv | gv.isNullness(isNull))) or + WrapperGuard::additionalImpliesStep(guard, v, e, any(GuardValue gv | gv.isNullness(isNull))) or additionalImpliesStep(guard, v, e, any(GuardValue gv | gv.isNullness(isNull))) } @@ -992,10 +992,9 @@ module Make Input> { /** * Provides an implementation of guard implication logic for custom - * wrappers. This can be used to instantiate the `additionalImpliesStep` - * predicate. + * wrappers. */ - private module CustomGuard { + private module WrapperGuard { final private class FinalExpr = Expr; private class ReturnExpr extends FinalExpr { From 9353c4a3e0cc309448a53f3961f1194229359c99 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 23 Jul 2025 12:59:59 +0200 Subject: [PATCH 04/10] Guards: Generalise wrapper guards. --- .../semmle/code/java/controlflow/Guards.qll | 15 ++--- java/ql/test/library-tests/guards/Guards.java | 59 ++++++++++++++++++ .../guards/GuardsInline.expected | 23 +++++++ .../controlflow/codeql/controlflow/Guards.qll | 60 ++++++++++++------- 4 files changed, 128 insertions(+), 29 deletions(-) diff --git a/java/ql/lib/semmle/code/java/controlflow/Guards.qll b/java/ql/lib/semmle/code/java/controlflow/Guards.qll index 697273d59d74..19bcf66fe331 100644 --- a/java/ql/lib/semmle/code/java/controlflow/Guards.qll +++ b/java/ql/lib/semmle/code/java/controlflow/Guards.qll @@ -344,11 +344,8 @@ private module GuardsInput implements SharedGuards::InputSig { final private class FinalMethod = Method; - class BooleanMethod extends FinalMethod { - BooleanMethod() { - super.getReturnType().(PrimitiveType).hasName("boolean") and - not super.isOverridable() - } + class NonOverridableMethod extends FinalMethod { + NonOverridableMethod() { not super.isOverridable() } Parameter getParameter(ParameterPosition ppos) { super.getParameter(ppos) = result and @@ -363,14 +360,14 @@ private module GuardsInput implements SharedGuards::InputSig { } } - private predicate booleanMethodCall(MethodCall call, BooleanMethod m) { + private predicate nonOverridableMethodCall(MethodCall call, NonOverridableMethod m) { call.getMethod().getSourceDeclaration() = m } - class BooleanMethodCall extends GuardsInput::Expr instanceof MethodCall { - BooleanMethodCall() { booleanMethodCall(this, _) } + class NonOverridableMethodCall extends GuardsInput::Expr instanceof MethodCall { + NonOverridableMethodCall() { nonOverridableMethodCall(this, _) } - BooleanMethod getMethod() { booleanMethodCall(this, result) } + NonOverridableMethod getMethod() { nonOverridableMethodCall(this, result) } GuardsInput::Expr getArgument(ArgumentPosition apos) { result = super.getArgument(apos) } } diff --git a/java/ql/test/library-tests/guards/Guards.java b/java/ql/test/library-tests/guards/Guards.java index b75e549d1669..270f8d5266c1 100644 --- a/java/ql/test/library-tests/guards/Guards.java +++ b/java/ql/test/library-tests/guards/Guards.java @@ -143,4 +143,63 @@ void t7(int[] a) { chk(); // $ guarded=found:true guarded='i < a.length:false' } } + + public static boolean testNotNull1(String input) { + return input != null && input.length() > 0; + } + + public static boolean testNotNull2(String input) { + if (input == null) return false; + return input.length() > 0; + } + + public static int getNumOrDefault(Integer number) { + return number == null ? 0 : number; + } + + public static String concatNonNull(String s1, String s2) { + if (s1 == null || s2 == null) return null; + return s1 + s2; + } + + public static Status testEnumWrapper(boolean flag) { + return flag ? Status.SUCCESS : Status.FAILURE; + } + + enum Status { SUCCESS, FAILURE } + + void testWrappers(String s, Integer i) { + if (testNotNull1(s)) { + chk(); // $ guarded='s:not null' guarded=testNotNull1(...):true + } else { + chk(); // $ guarded=testNotNull1(...):false + } + + if (testNotNull2(s)) { + chk(); // $ guarded='s:not null' guarded=testNotNull2(...):true + } else { + chk(); // $ guarded=testNotNull2(...):false + } + + if (0 == getNumOrDefault(i)) { + chk(); // $ guarded='0 == getNumOrDefault(...):true' guarded='getNumOrDefault(...):0' + } else { + chk(); // $ guarded='0 == getNumOrDefault(...):false' guarded='getNumOrDefault(...):not 0' guarded='i:not 0' guarded='i:not null' + } + + if (null == concatNonNull(s, "suffix")) { + chk(); // $ guarded='concatNonNull(...):null' guarded='null == concatNonNull(...):true' + } else { + chk(); // $ guarded='concatNonNull(...):not null' guarded='null == concatNonNull(...):false' guarded='s:not null' + } + + switch (testEnumWrapper(g(1))) { + case SUCCESS: + chk(); // $ guarded='testEnumWrapper(...):SUCCESS' guarded='testEnumWrapper(...):match SUCCESS' guarded=g(1):true + break; + case FAILURE: + chk(); // $ guarded='testEnumWrapper(...):FAILURE' guarded='testEnumWrapper(...):match FAILURE' guarded=g(1):false + break; + } + } } diff --git a/java/ql/test/library-tests/guards/GuardsInline.expected b/java/ql/test/library-tests/guards/GuardsInline.expected index c45d536b7e9a..0ace810c9ec3 100644 --- a/java/ql/test/library-tests/guards/GuardsInline.expected +++ b/java/ql/test/library-tests/guards/GuardsInline.expected @@ -89,3 +89,26 @@ | 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 | +| Guards.java:173:7:173:11 | chk(...) | 's:not null' | +| Guards.java:173:7:173:11 | chk(...) | testNotNull1(...):true | +| Guards.java:175:7:175:11 | chk(...) | testNotNull1(...):false | +| Guards.java:179:7:179:11 | chk(...) | 's:not null' | +| Guards.java:179:7:179:11 | chk(...) | testNotNull2(...):true | +| Guards.java:181:7:181:11 | chk(...) | testNotNull2(...):false | +| Guards.java:185:7:185:11 | chk(...) | '0 == getNumOrDefault(...):true' | +| Guards.java:185:7:185:11 | chk(...) | 'getNumOrDefault(...):0' | +| Guards.java:187:7:187:11 | chk(...) | '0 == getNumOrDefault(...):false' | +| Guards.java:187:7:187:11 | chk(...) | 'getNumOrDefault(...):not 0' | +| Guards.java:187:7:187:11 | chk(...) | 'i:not 0' | +| Guards.java:187:7:187:11 | chk(...) | 'i:not null' | +| Guards.java:191:7:191:11 | chk(...) | 'concatNonNull(...):null' | +| Guards.java:191:7:191:11 | chk(...) | 'null == concatNonNull(...):true' | +| Guards.java:193:7:193:11 | chk(...) | 'concatNonNull(...):not null' | +| Guards.java:193:7:193:11 | chk(...) | 'null == concatNonNull(...):false' | +| Guards.java:193:7:193:11 | chk(...) | 's:not null' | +| Guards.java:198:9:198:13 | chk(...) | 'testEnumWrapper(...):SUCCESS' | +| Guards.java:198:9:198:13 | chk(...) | 'testEnumWrapper(...):match SUCCESS' | +| Guards.java:198:9:198:13 | chk(...) | g(1):true | +| Guards.java:201:9:201:13 | chk(...) | 'testEnumWrapper(...):FAILURE' | +| Guards.java:201:9:201:13 | chk(...) | 'testEnumWrapper(...):match FAILURE' | +| Guards.java:201:9:201:13 | chk(...) | g(1):false | diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index 27cbde2e72a1..cd6e7126f546 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -234,16 +234,16 @@ signature module InputSig { */ predicate parameterMatch(ParameterPosition ppos, ArgumentPosition apos); - /** A non-overridable method with a boolean return value. */ - class BooleanMethod { + /** A non-overridable method. */ + class NonOverridableMethod { Parameter getParameter(ParameterPosition ppos); /** Gets an expression being returned by this method. */ Expr getAReturnExpr(); } - class BooleanMethodCall extends Expr { - BooleanMethod getMethod(); + class NonOverridableMethodCall extends Expr { + NonOverridableMethod getMethod(); Expr getArgument(ArgumentPosition apos); } @@ -998,17 +998,32 @@ module Make Input> { final private class FinalExpr = Expr; private class ReturnExpr extends FinalExpr { - ReturnExpr() { any(BooleanMethod m).getAReturnExpr() = this } + ReturnExpr() { any(NonOverridableMethod m).getAReturnExpr() = this } + + NonOverridableMethod getMethod() { result.getAReturnExpr() = this } pragma[nomagic] BasicBlock getBasicBlock() { result = super.getBasicBlock() } } - private predicate booleanReturnGuard(Guard guard, GuardValue val) { - guard instanceof ReturnExpr and exists(val.asBooleanValue()) + private predicate relevantCallValue(NonOverridableMethodCall call, GuardValue val) { + BranchImplies::guardControls(call, val, _, _) or + ReturnImplies::guardControls(call, val, _, _) + } + + private predicate relevantReturnValue(NonOverridableMethod m, GuardValue val) { + exists(NonOverridableMethodCall call | + relevantCallValue(call, val) and + call.getMethod() = m and + not val instanceof TException + ) + } + + private predicate returnGuard(Guard guard, GuardValue val) { + relevantReturnValue(guard.(ReturnExpr).getMethod(), val) } - private module ReturnImplies = ImpliesTC; + private module ReturnImplies = ImpliesTC; /** * Holds if `ret` is a return expression in a non-overridable method that @@ -1016,32 +1031,36 @@ module Make Input> { * parameter has the value `val`. */ private predicate validReturnInCustomGuard( - ReturnExpr ret, ParameterPosition ppos, boolean retval, GuardValue val + ReturnExpr ret, ParameterPosition ppos, GuardValue retval, GuardValue val ) { - exists(BooleanMethod m, SsaDefinition param | + exists(NonOverridableMethod m, SsaDefinition param | m.getAReturnExpr() = ret and parameterDefinition(m.getParameter(ppos), param) | exists(Guard g0, GuardValue v0 | g0.directlyValueControls(ret.getBasicBlock(), v0) and BranchImplies::ssaControls(param, val, g0, v0) and - retval = [true, false] + relevantReturnValue(m, retval) ) or - ReturnImplies::ssaControls(param, val, ret, - any(GuardValue r | r.asBooleanValue() = retval)) + ReturnImplies::ssaControls(param, val, ret, 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 + * Gets a non-overridable method 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) { + private NonOverridableMethod customGuard( + ParameterPosition ppos, GuardValue retval, GuardValue val + ) { forex(ReturnExpr ret | result.getAReturnExpr() = ret and - not ret.(ConstantExpr).asBooleanValue() = retval.booleanNot() + not exists(GuardValue notRetval | + exprHasValue(ret, notRetval) and + disjointValues(notRetval, retval) + ) | validReturnInCustomGuard(ret, ppos, retval, val) ) @@ -1056,11 +1075,12 @@ module Make Input> { * custom guard wrappers. */ predicate additionalImpliesStep(PreGuard g1, GuardValue v1, PreGuard g2, GuardValue v2) { - exists(BooleanMethodCall call, ParameterPosition ppos, ArgumentPosition apos | + exists(NonOverridableMethodCall call, ParameterPosition ppos, ArgumentPosition apos | g1 = call and - call.getMethod() = customGuard(ppos, v1.asBooleanValue(), v2) and + call.getMethod() = customGuard(ppos, v1, v2) and call.getArgument(apos) = g2 and - parameterMatch(pragma[only_bind_out](ppos), pragma[only_bind_out](apos)) + parameterMatch(pragma[only_bind_out](ppos), pragma[only_bind_out](apos)) and + not exprHasValue(g2, v2) // disregard trivial guard ) } } From e7bdfe1d433774a593adae8af9b3c338576af1ba Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 23 Jul 2025 13:03:01 +0200 Subject: [PATCH 05/10] Guards: Rename predicate. --- shared/controlflow/codeql/controlflow/Guards.qll | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index cd6e7126f546..d7ec0a0f4125 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -901,7 +901,7 @@ module Make Input> { or exists(Guard g0, GuardValue v0 | guardControls(g0, v0, tgtGuard, tgtVal) and - WrapperGuard::additionalImpliesStep(g0, v0, guard, v) + WrapperGuard::wrapperImpliesStep(g0, v0, guard, v) ) or exists(Guard g0, GuardValue v0 | @@ -947,7 +947,7 @@ module Make Input> { */ predicate nullGuard(Guard guard, GuardValue v, Expr e, boolean isNull) { impliesStep2(guard, v, e, any(GuardValue gv | gv.isNullness(isNull))) or - WrapperGuard::additionalImpliesStep(guard, v, e, any(GuardValue gv | gv.isNullness(isNull))) or + WrapperGuard::wrapperImpliesStep(guard, v, e, any(GuardValue gv | gv.isNullness(isNull))) or additionalImpliesStep(guard, v, e, any(GuardValue gv | gv.isNullness(isNull))) } @@ -1074,7 +1074,7 @@ module Make Input> { * This predicate covers the implication steps that arise from calls to * custom guard wrappers. */ - predicate additionalImpliesStep(PreGuard g1, GuardValue v1, PreGuard g2, GuardValue v2) { + predicate wrapperImpliesStep(PreGuard g1, GuardValue v1, PreGuard g2, GuardValue v2) { exists(NonOverridableMethodCall call, ParameterPosition ppos, ArgumentPosition apos | g1 = call and call.getMethod() = customGuard(ppos, v1, v2) and From 8b58c2c32fc1aee4a73ed6e98b363abf48bcb432 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 23 Jul 2025 15:31:34 +0200 Subject: [PATCH 06/10] Guards: Add support for wrappers that may throw exceptions. --- .../semmle/code/java/controlflow/Guards.qll | 2 ++ java/ql/test/library-tests/guards/Guards.java | 10 ++++++++++ .../guards/GuardsInline.expected | 2 ++ .../controlflow/codeql/controlflow/Guards.qll | 19 +++++++++++++++++++ 4 files changed, 33 insertions(+) diff --git a/java/ql/lib/semmle/code/java/controlflow/Guards.qll b/java/ql/lib/semmle/code/java/controlflow/Guards.qll index 19bcf66fe331..c33658cb67b6 100644 --- a/java/ql/lib/semmle/code/java/controlflow/Guards.qll +++ b/java/ql/lib/semmle/code/java/controlflow/Guards.qll @@ -146,6 +146,8 @@ private module GuardsInput implements SharedGuards::InputSig { class ControlFlowNode = J::ControlFlowNode; + class NormalExitNode = ControlFlow::NormalExitNode; + class BasicBlock = J::BasicBlock; predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2) { J::dominatingEdge(bb1, bb2) } diff --git a/java/ql/test/library-tests/guards/Guards.java b/java/ql/test/library-tests/guards/Guards.java index 270f8d5266c1..aca64d6f64da 100644 --- a/java/ql/test/library-tests/guards/Guards.java +++ b/java/ql/test/library-tests/guards/Guards.java @@ -202,4 +202,14 @@ void testWrappers(String s, Integer i) { break; } } + + static void ensureNotNull(Object o) throws Exception { + if (o == null) throw new Exception(); + } + + void testExceptionWrapper(String s) throws Exception { + chk(); // nothing guards here + ensureNotNull(s); + chk(); // $ guarded='ensureNotNull(...):no exception' guarded='s:not null' + } } diff --git a/java/ql/test/library-tests/guards/GuardsInline.expected b/java/ql/test/library-tests/guards/GuardsInline.expected index 0ace810c9ec3..a76e2629cde0 100644 --- a/java/ql/test/library-tests/guards/GuardsInline.expected +++ b/java/ql/test/library-tests/guards/GuardsInline.expected @@ -112,3 +112,5 @@ | Guards.java:201:9:201:13 | chk(...) | 'testEnumWrapper(...):FAILURE' | | Guards.java:201:9:201:13 | chk(...) | 'testEnumWrapper(...):match FAILURE' | | Guards.java:201:9:201:13 | chk(...) | g(1):false | +| Guards.java:213:5:213:9 | chk(...) | 'ensureNotNull(...):no exception' | +| Guards.java:213:5:213:9 | chk(...) | 's:not null' | diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index d7ec0a0f4125..ccfb1a983802 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -79,6 +79,9 @@ signature module InputSig { Location getLocation(); } + /** A control flow node indicating normal termination of a callable. */ + class NormalExitNode extends ControlFlowNode; + /** * A basic block, that is, a maximal straight-line sequence of control flow nodes * without branches or joins. @@ -520,6 +523,8 @@ module Make Input> { ) } + private predicate normalExitBlock(BasicBlock bb) { bb.getNode(_) instanceof NormalExitNode } + signature module LogicInputSig { class SsaDefinition { /** Gets the basic block to which this SSA definition belongs. */ @@ -1047,6 +1052,13 @@ module Make Input> { ) } + private predicate guardDirectlyControlsExit(Guard guard, GuardValue val) { + exists(BasicBlock bb | + guard.directlyValueControls(bb, val) and + normalExitBlock(bb) + ) + } + /** * Gets a non-overridable method that performs a check on the `ppos`th * parameter. A return value equal to `retval` allows us to conclude @@ -1064,6 +1076,13 @@ module Make Input> { | validReturnInCustomGuard(ret, ppos, retval, val) ) + or + exists(SsaDefinition param, Guard g0, GuardValue v0 | + parameterDefinition(result.getParameter(ppos), param) and + guardDirectlyControlsExit(g0, v0) and + retval = TException(false) and + BranchImplies::ssaControls(param, val, g0, v0) + ) } /** From 7127cca8c188c1d1892108beb476efd1d0a883e2 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 24 Jul 2025 13:02:51 +0200 Subject: [PATCH 07/10] Guards: Add support for extending BarrierGuards with wrapped invocations. --- .../controlflow/codeql/controlflow/Guards.qll | 104 +++++++++++++++++- 1 file changed, 101 insertions(+), 3 deletions(-) diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index ccfb1a983802..3f7ebc9a9552 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -52,6 +52,7 @@ module; private import codeql.util.Boolean private import codeql.util.Location +private import codeql.util.Unit signature module InputSig { class SuccessorType { @@ -1002,7 +1003,7 @@ module Make Input> { private module WrapperGuard { final private class FinalExpr = Expr; - private class ReturnExpr extends FinalExpr { + class ReturnExpr extends FinalExpr { ReturnExpr() { any(NonOverridableMethod m).getAReturnExpr() = this } NonOverridableMethod getMethod() { result.getAReturnExpr() = this } @@ -1016,7 +1017,7 @@ module Make Input> { ReturnImplies::guardControls(call, val, _, _) } - private predicate relevantReturnValue(NonOverridableMethod m, GuardValue val) { + predicate relevantReturnValue(NonOverridableMethod m, GuardValue val) { exists(NonOverridableMethodCall call | relevantCallValue(call, val) and call.getMethod() = m and @@ -1028,7 +1029,7 @@ module Make Input> { relevantReturnValue(guard.(ReturnExpr).getMethod(), val) } - private module ReturnImplies = ImpliesTC; + module ReturnImplies = ImpliesTC; /** * Holds if `ret` is a return expression in a non-overridable method that @@ -1104,6 +1105,103 @@ module Make Input> { } } + signature predicate guardChecksSig(Guard g, Expr e, boolean branch); + + bindingset[this] + signature class StateSig; + + private module WithState { + signature predicate guardChecksSig(Guard g, Expr e, boolean branch, State state); + } + + /** + * Extends a `BarrierGuard` input predicate with wrapped invocations. + */ + module ValidationWrapper { + private predicate guardChecksWithState(Guard g, Expr e, boolean branch, Unit state) { + guardChecks0(g, e, branch) and exists(state) + } + + private module StatefulWrapper = ValidationWrapperWithState; + + /** + * Holds if the guard `g` validates the expression `e` upon evaluating to `val`. + */ + predicate guardChecks(Guard g, Expr e, GuardValue val) { + StatefulWrapper::guardChecks(g, e, val, _) + } + } + + /** + * Extends a `BarrierGuard` input predicate with wrapped invocations. + */ + module ValidationWrapperWithState< + StateSig State, WithState::guardChecksSig/4 guardChecks0> + { + private import WrapperGuard + + /** + * 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 been validated by the given guard. + */ + private predicate validReturnInValidationWrapper( + ReturnExpr ret, ParameterPosition ppos, GuardValue retval, State state + ) { + exists(NonOverridableMethod m, SsaDefinition param, Guard guard, GuardValue val | + m.getAReturnExpr() = ret and + parameterDefinition(m.getParameter(ppos), param) and + guardChecks(guard, param.getARead(), val, state) + | + guard.valueControls(ret.getBasicBlock(), val) and + relevantReturnValue(m, retval) + or + ReturnImplies::guardControls(guard, val, ret, retval) + ) + } + + /** + * Gets a non-overridable method that performs a check on the `ppos`th + * parameter. A return value equal to `retval` allows us to conclude + * that the argument has been validated by the given guard. + */ + private NonOverridableMethod validationWrapper( + ParameterPosition ppos, GuardValue retval, State state + ) { + forex(ReturnExpr ret | + result.getAReturnExpr() = ret and + not exists(GuardValue notRetval | + exprHasValue(ret, notRetval) and + disjointValues(notRetval, retval) + ) + | + validReturnInValidationWrapper(ret, ppos, retval, state) + ) + or + exists(SsaDefinition param, BasicBlock bb, Guard guard, GuardValue val | + parameterDefinition(result.getParameter(ppos), param) and + guardChecks(guard, param.getARead(), val, state) and + guard.valueControls(bb, val) and + normalExitBlock(bb) and + retval = TException(false) + ) + } + + /** + * Holds if the guard `g` validates the expression `e` upon evaluating to `val`. + */ + predicate guardChecks(Guard g, Expr e, GuardValue val, State state) { + guardChecks0(g, e, val.asBooleanValue(), state) + or + exists(NonOverridableMethodCall call, ParameterPosition ppos, ArgumentPosition apos | + g = call and + call.getMethod() = validationWrapper(ppos, val, state) and + call.getArgument(apos) = e and + parameterMatch(pragma[only_bind_out](ppos), pragma[only_bind_out](apos)) + ) + } + } + /** * 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 From 961558298a0fdcee571c29d4007525c320ffe3fb Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 24 Jul 2025 15:26:38 +0200 Subject: [PATCH 08/10] Guards: Slight join-order improvement. --- shared/controlflow/codeql/controlflow/Guards.qll | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index 3f7ebc9a9552..ed2691fbf0e9 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -1031,6 +1031,11 @@ module Make Input> { module ReturnImplies = ImpliesTC; + pragma[nomagic] + private predicate directlyControlsReturn(Guard guard, GuardValue val, ReturnExpr ret) { + guard.directlyValueControls(ret.getBasicBlock(), val) + } + /** * 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 @@ -1044,7 +1049,7 @@ module Make Input> { parameterDefinition(m.getParameter(ppos), param) | exists(Guard g0, GuardValue v0 | - g0.directlyValueControls(ret.getBasicBlock(), v0) and + directlyControlsReturn(g0, v0, ret) and BranchImplies::ssaControls(param, val, g0, v0) and relevantReturnValue(m, retval) ) From 8d747e95837ea5e3bc928fcfbb33971d187fae83 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 24 Jul 2025 15:33:28 +0200 Subject: [PATCH 09/10] Java: Accept qltest change. --- java/ql/test/query-tests/Nullness/C.java | 2 +- java/ql/test/query-tests/Nullness/NullMaybe.expected | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/java/ql/test/query-tests/Nullness/C.java b/java/ql/test/query-tests/Nullness/C.java index d195eea6acb3..9424cbe71f22 100644 --- a/java/ql/test/query-tests/Nullness/C.java +++ b/java/ql/test/query-tests/Nullness/C.java @@ -204,7 +204,7 @@ public void ex14(int[] a) { obj = new Object(); } else if (a[i] == 2) { verifyNotNull(obj); - obj.hashCode(); // NPE - false positive + obj.hashCode(); // OK } } } diff --git a/java/ql/test/query-tests/Nullness/NullMaybe.expected b/java/ql/test/query-tests/Nullness/NullMaybe.expected index a19fae57e74e..9f2920293b07 100644 --- a/java/ql/test/query-tests/Nullness/NullMaybe.expected +++ b/java/ql/test/query-tests/Nullness/NullMaybe.expected @@ -29,7 +29,6 @@ | 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 | | C.java:144:15:144:15 | a | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:141:20:141:26 | a | a | C.java:142:13:142:21 | ... == ... | this | | C.java:188:9:188:11 | obj | Variable $@ may be null at this access because of $@ assignment. | C.java:181:5:181:22 | Object obj | obj | C.java:181:12:181:21 | obj | this | -| 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 | | 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 | From 8b5ee4923008a591568ebea533076ecf82262fb0 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 28 Jul 2025 13:45:04 +0200 Subject: [PATCH 10/10] Java: Add change note. --- java/ql/lib/change-notes/2025-07-28-guardwrappers.md | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 java/ql/lib/change-notes/2025-07-28-guardwrappers.md diff --git a/java/ql/lib/change-notes/2025-07-28-guardwrappers.md b/java/ql/lib/change-notes/2025-07-28-guardwrappers.md new file mode 100644 index 000000000000..cf976fe77896 --- /dev/null +++ b/java/ql/lib/change-notes/2025-07-28-guardwrappers.md @@ -0,0 +1,4 @@ +--- +category: minorAnalysis +--- +* Guard implication logic involving wrapper methods has been improved. In particular, this means fewer false positives for `java/dereferenced-value-may-be-null`.