Merge pull request #20121 from aschackmull/guards/wrapperguard

Guards: Improve support for wrapped guards
2025-12-16 16:53:25 +01:00 · 2025-08-07 15:41:04 +02:00
parent dfe4401f13 2909def9b6
commit 3674966946
7 changed files with 385 additions and 140 deletions
--- a/java/ql/lib/change-notes/2025-07-28-guardwrappers.md
+++ 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`.
--- 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<Location> {

  class ControlFlowNode = J::ControlFlowNode;

+  class NormalExitNode = ControlFlow::NormalExitNode;
+
  class BasicBlock = J::BasicBlock;

  predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2) { J::dominatingEdge(bb1, bb2) }
@@ -322,6 +324,55 @@ private module GuardsInput implements SharedGuards::InputSig<Location> {

    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 NonOverridableMethod extends FinalMethod {
+    NonOverridableMethod() { 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 nonOverridableMethodCall(MethodCall call, NonOverridableMethod m) {
+    call.getMethod().getSourceDeclaration() = m
+  }
+
+  class NonOverridableMethodCall extends GuardsInput::Expr instanceof MethodCall {
+    NonOverridableMethodCall() { nonOverridableMethodCall(this, _) }
+
+    NonOverridableMethod getMethod() { nonOverridableMethodCall(this, result) }
+
+    GuardsInput::Expr getArgument(ArgumentPosition apos) { result = super.getArgument(apos) }
+  }
 }

 private module GuardsImpl = SharedGuards::Make<Location, GuardsInput>;
@@ -340,6 +391,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 {
@@ -364,18 +426,13 @@ private module LogicInput_v1 implements GuardsImpl::LogicInputSig {
    }
  }

+  predicate parameterDefinition(Parameter p, SsaDefinition def) {
+    def.(BaseSsaImplicitInit).isParameterDefinition(p)
+  }
+
  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 {
@@ -400,15 +457,13 @@ 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)
-  }
+  predicate additionalImpliesStep = LogicInputCommon::additionalImpliesStep/4;
 }

 private module LogicInput_v3 implements GuardsImpl::LogicInputSig {
@@ -421,70 +476,11 @@ private module LogicInput_v3 implements GuardsImpl::LogicInputSig {

  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`. */
-  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) }
-  }
+  predicate additionalImpliesStep = LogicInputCommon::additionalImpliesStep/4;
 }

 class GuardValue = GuardsImpl::GuardValue;

-private module CustomGuard = Guards_v2::CustomGuard<CustomGuardInput>;
-
 /** INTERNAL: Don't use. */
 module Guards_v1 = GuardsImpl::Logic<LogicInput_v1>;

--- a/java/ql/test/library-tests/guards/Guards.java
+++ b/java/ql/test/library-tests/guards/Guards.java
@@ -143,4 +143,73 @@ public class Guards {
      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;
+    }
+  }
+
+  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'
+  }
 }
--- a/java/ql/test/library-tests/guards/GuardsInline.expected
+++ b/java/ql/test/library-tests/guards/GuardsInline.expected
@@ -89,3 +89,28 @@
 | 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 |
+| Guards.java:213:5:213:9 | chk(...) | 'ensureNotNull(...):no exception' |
+| Guards.java:213:5:213:9 | chk(...) | 's:not null' |
--- a/java/ql/test/query-tests/Nullness/C.java
+++ b/java/ql/test/query-tests/Nullness/C.java
@@ -204,7 +204,7 @@ public class C {
        obj = new Object();
      } else if (a[i] == 2) {
        verifyNotNull(obj);
-        obj.hashCode(); // NPE - false positive
+        obj.hashCode(); // OK
      }
    }
  }
--- 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 |
--- 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<LocationSig Location> {
  class SuccessorType {
@@ -79,6 +80,9 @@ signature module InputSig<LocationSig Location> {
    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.
@@ -207,6 +211,46 @@ signature module InputSig<LocationSig Location> {
    /** 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. */
+  class NonOverridableMethod {
+    Parameter getParameter(ParameterPosition ppos);
+
+    /** Gets an expression being returned by this method. */
+    Expr getAReturnExpr();
+  }
+
+  class NonOverridableMethodCall extends Expr {
+    NonOverridableMethod getMethod();
+
+    Expr getArgument(ArgumentPosition apos);
+  }
 }

 /** Provides guards-related predicates and classes. */
@@ -480,6 +524,8 @@ module Make<LocationSig Location, InputSig<Location> 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. */
@@ -503,6 +549,8 @@ module Make<LocationSig Location, InputSig<Location> 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 +573,6 @@ module Make<LocationSig Location, InputSig<Location> 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 +905,11 @@ module Make<LocationSig Location, InputSig<Location> Input> {
          impliesStepSsaGuard(def0, v0, guard, v)
        )
        or
+        exists(Guard g0, GuardValue v0 |
+          guardControls(g0, v0, tgtGuard, tgtVal) and
+          WrapperGuard::wrapperImpliesStep(g0, v0, guard, v)
+        )
+        or
        exists(Guard g0, GuardValue v0 |
          guardControls(g0, v0, tgtGuard, tgtVal) and
          additionalImpliesStep(g0, v0, guard, v)
@@ -902,6 +953,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
     */
    predicate nullGuard(Guard guard, GuardValue v, Expr e, boolean isNull) {
      impliesStep2(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)))
    }

@@ -944,61 +996,45 @@ module Make<LocationSig Location, InputSig<Location> 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.
+     * Provides an implementation of guard implication logic for guard
+     * wrappers.
     */
-    module CustomGuard<CustomGuardInputSig CustomGuardInput> {
-      private import CustomGuardInput
-
+    private module WrapperGuard {
      final private class FinalExpr = Expr;

-      private class ReturnExpr extends FinalExpr {
-        ReturnExpr() { any(BooleanMethod m).getAReturnExpr() = this }
+      class ReturnExpr extends FinalExpr {
+        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 module ReturnImplies = ImpliesTC<booleanReturnGuard/2>;
+      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)
+      }
+
+      module ReturnImplies = ImpliesTC<returnGuard/2>;
+
+      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
@@ -1006,35 +1042,53 @@ module Make<LocationSig Location, InputSig<Location> 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
-          m.getParameter(ppos) = param
+          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
-            retval = [true, false]
+            relevantReturnValue(m, retval)
          )
          or
-          ReturnImplies::ssaControls(param, val, ret,
-            any(GuardValue r | r.asBooleanValue() = retval))
+          ReturnImplies::ssaControls(param, val, ret, retval)
+        )
+      }
+
+      private predicate guardDirectlyControlsExit(Guard guard, GuardValue val) {
+        exists(BasicBlock bb |
+          guard.directlyValueControls(bb, val) and
+          normalExitBlock(bb)
        )
      }

      /**
-       * 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 wrapperGuard(
+        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)
        )
+        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)
+        )
      }

      /**
@@ -1043,13 +1097,111 @@ module Make<LocationSig Location, InputSig<Location> Input> {
       * dominates the evaluation of `g1` to `v1`.
       *
       * This predicate covers the implication steps that arise from calls to
-       * custom guard wrappers.
+       * guard wrappers.
       */
-      predicate additionalImpliesStep(PreGuard g1, GuardValue v1, PreGuard g2, GuardValue v2) {
-        exists(BooleanMethodCall call, ParameterPosition ppos, ArgumentPosition apos |
+      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.asBooleanValue(), v2) and
+          call.getMethod() = wrapperGuard(ppos, v1, v2) and
          call.getArgument(apos) = g2 and
+          parameterMatch(pragma[only_bind_out](ppos), pragma[only_bind_out](apos)) and
+          not exprHasValue(g2, v2) // disregard trivial guard
+        )
+      }
+    }
+
+    signature predicate guardChecksSig(Guard g, Expr e, boolean branch);
+
+    bindingset[this]
+    signature class StateSig;
+
+    private module WithState<StateSig State> {
+      signature predicate guardChecksSig(Guard g, Expr e, boolean branch, State state);
+    }
+
+    /**
+     * Extends a `BarrierGuard` input predicate with wrapped invocations.
+     */
+    module ValidationWrapper<guardChecksSig/3 guardChecks0> {
+      private predicate guardChecksWithState(Guard g, Expr e, boolean branch, Unit state) {
+        guardChecks0(g, e, branch) and exists(state)
+      }
+
+      private module StatefulWrapper = ValidationWrapperWithState<Unit, guardChecksWithState/4>;
+
+      /**
+       * 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<State>::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))
        )
      }