Merge branch 'main' into jcogs33/java/insecure-spring-actuator-config-promotion

java/ql/lib/semmle/code/java/ControlFlowGraph.qll

@@ -347,12 +347,28 @@ private module ControlFlowGraphImpl {
     )
   }
 
+  private predicate methodMayThrow(Method m, ThrowableType t) {
+    exists(AstNode n |
+      t = n.(ThrowStmt).getThrownExceptionType() and
+      not n.(ThrowStmt).getParent() = any(Method m0).getBody()
+      or
+      uncheckedExceptionFromMethod(n, t)
+    |
+      n.getEnclosingStmt().getEnclosingCallable() = m and
+      not exists(TryStmt try |
+        exists(try.getACatchClause()) and try.getBlock() = n.getEnclosingStmt().getEnclosingStmt*()
+      )
+    )
+  }
+
   /**
-   * Bind `t` to an unchecked exception that may occur in a precondition check.
+   * Bind `t` to an unchecked exception that may occur in a precondition check or guard wrapper.
    */
   private predicate uncheckedExceptionFromMethod(MethodCall ma, ThrowableType t) {
     conditionCheckArgument(ma, _, _) and
     (t instanceof TypeError or t instanceof TypeRuntimeException)
+    or
+    methodMayThrow(ma.getMethod(), t)
   }
 
   /**
@@ -1621,7 +1637,8 @@ private module ControlFlowGraphImpl {
         result.(AssertThrowNode).getAstNode() = assertstmt
       )
       or
-      last(assertstmt.getMessage(), n, NormalCompletion()) and
+      last(assertstmt.getMessage(), n, completion) and
+      completion = NormalCompletion() and
       result.(AssertThrowNode).getAstNode() = assertstmt
     )
     or

java/ql/lib/semmle/code/java/Diagnostics.qll

@@ -61,3 +61,9 @@ class Diagnostic extends @diagnostic {
   /** Gets a textual representation of this diagnostic. */
   string toString() { result = this.getMessage() }
 }
+
+/**
+ * Holds for extraction information keys that should be skipped from telemetry reports.
+ * This predicate can be extended by other packs to filter out specific telemetry keys.
+ */
+extensible predicate extractorInformationSkipKey(string key);

java/ql/lib/semmle/code/java/Generics.qll

@@ -521,7 +521,13 @@ private predicate unificationTargets(RefType t1, Type t2) {
     t2 = a2.getComponentType()
   )
   or
-  exists(ParameterizedType pt1, ParameterizedType pt2, int pos |
+  unificationTargetsParameterized(_, _, t1, t2)
+}
+
+private predicate unificationTargetsParameterized(
+  ParameterizedType pt1, ParameterizedType pt2, RefType t1, RefType t2
+) {
+  exists(int pos |
     unificationTargets(pt1, pt2) and
     t1 = pt1.getTypeArgument(pos) and
     t2 = pt2.getTypeArgument(pos)
@@ -565,10 +571,12 @@ private predicate hasParameterSubstitution(
   GenericType g1, ParameterizedType pt1, GenericType g2, ParameterizedType pt2, TypeVariable v,
   RefType subst
 ) {
-  unificationTargets(pt1, pt2) and
-  exists(int pos | hasSubstitution(pt1.getTypeArgument(pos), pt2.getTypeArgument(pos), v, subst)) and
-  g1 = pt1.getGenericType() and
-  g2 = pt2.getGenericType()
+  exists(RefType t1, RefType t2 |
+    unificationTargetsParameterized(pt1, pt2, t1, t2) and
+    hasSubstitution(t1, t2, v, subst) and
+    g1 = pt1.getGenericType() and
+    g2 = pt2.getGenericType()
+  )
 }
 
 /**

java/ql/lib/semmle/code/java/Member.qll

@@ -256,7 +256,15 @@ class Callable extends StmtParent, Member, @callable {
   Exception getAnException() { exceptions(result, _, this) }
 
   /** Gets an exception type that occurs in the `throws` clause of this callable. */
-  RefType getAThrownExceptionType() { result = this.getAnException().getType() }
+  RefType getAThrownExceptionType() {
+    result = this.getAnException().getType()
+    or
+    exists(Annotation a |
+      this.getAnAnnotation() = a and
+      a.getType().hasQualifiedName("kotlin.jvm", "Throws") and
+      a.getATypeArrayValue(_) = result
+    )
+  }
 
   /** Gets a call site that references this callable. */
   Call getAReference() { result.getCallee() = this }

java/ql/lib/semmle/code/java/Type.qll

@@ -1261,14 +1261,21 @@ private Type erase(Type t) {
  *
  * For the definition of the notion of *erasure* see JLS v8, section 4.6 (Type Erasure).
  */
+bindingset[t1, t2]
 overlay[caller?]
-pragma[inline]
+pragma[inline_late]
 predicate haveIntersection(RefType t1, RefType t2) {
   exists(RefType e1, RefType e2 | e1 = erase(t1) and e2 = erase(t2) |
-    erasedHaveIntersection(e1, e2)
+    erasedHaveIntersectionFilter(e1, e2)
   )
 }
 
+bindingset[t1, t2]
+pragma[inline_late]
+private predicate erasedHaveIntersectionFilter(RefType t1, RefType t2) {
+  erasedHaveIntersection(t1, t2)
+}
+
 /**
  * Holds if there is no common (reflexive, transitive) subtype of the erasures
  * of types `t1` and `t2`.

java/ql/lib/semmle/code/java/controlflow/BasicBlocks.qll

@@ -57,7 +57,7 @@ private module Input implements BB::InputSig<Location> {
    * Holds if `node` represents an exit node to be used when calculating
    * post dominance.
    */
-  predicate nodeIsPostDominanceExit(Node node) { node instanceof ControlFlow::ExitNode }
+  predicate nodeIsPostDominanceExit(Node node) { node instanceof ControlFlow::NormalExitNode }
 }
 
 private module BbImpl = BB::Make<Location, Input>;

java/ql/lib/semmle/code/java/controlflow/Guards.qll

@@ -141,11 +141,14 @@ private predicate isNonFallThroughPredecessor(SwitchCase sc, ControlFlowNode pre
 
 private module GuardsInput implements SharedGuards::InputSig<Location> {
   private import java as J
+  private import semmle.code.java.dataflow.internal.BaseSSA
   private import semmle.code.java.dataflow.NullGuards as NullGuards
   import SuccessorType
 
   class ControlFlowNode = J::ControlFlowNode;
 
+  class NormalExitNode = ControlFlow::NormalExitNode;
+
   class BasicBlock = J::BasicBlock;
 
   predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2) { J::dominatingEdge(bb1, bb2) }
@@ -214,6 +217,12 @@ private module GuardsInput implements SharedGuards::InputSig<Location> {
         f.isFinal() and
         f.getInitializer() = NullGuards::baseNotNullExpr()
       )
+      or
+      exists(CatchClause cc, LocalVariableDeclExpr decl, BaseSsaUpdate v |
+        decl = cc.getVariable() and
+        decl = v.getDefiningExpr() and
+        this = v.getAUse()
+      )
     }
   }
 
@@ -322,6 +331,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 +398,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 +433,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 +464,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 +483,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>;
 
@@ -494,12 +497,6 @@ module Guards_v2 = GuardsImpl::Logic<LogicInput_v2>;
 /** INTERNAL: Don't use. */
 module Guards_v3 = GuardsImpl::Logic<LogicInput_v3>;
 
-/** 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

java/ql/lib/semmle/code/java/dataflow/Nullness.qll

@@ -653,7 +653,7 @@ private Expr trackingVarGuard(
       result = integerGuard(trackvar.getAnAccess(), branch, k, isA)
       or
       exists(int k2 |
-        result = integerGuard(trackvar.getAnAccess(), branch.booleanNot(), k2, true) and
+        result = integerGuard(trackvar.getAnAccess(), branch, k2, true) and
         isA = false and
         k2 != k
       )

java/ql/lib/semmle/code/java/dataflow/internal/DataFlowPrivate.qll

@@ -348,6 +348,16 @@ predicate expectsContent(Node n, ContentSet c) {
   FlowSummaryImpl::Private::Steps::summaryExpectsContent(n.(FlowSummaryNode).getSummaryNode(), c)
 }
 
+pragma[nomagic]
+private predicate numericRepresentative(RefType t) {
+  t.(BoxedType).getPrimitiveType().getName() = "double"
+}
+
+pragma[nomagic]
+private predicate booleanRepresentative(RefType t) {
+  t.(BoxedType).getPrimitiveType().getName() = "boolean"
+}
+
 /**
  * Gets a representative (boxed) type for `t` for the purpose of pruning
  * possible flow. A single type is used for all numeric types to account for
@@ -356,10 +366,10 @@ predicate expectsContent(Node n, ContentSet c) {
 RefType getErasedRepr(Type t) {
   exists(Type e | e = t.getErasure() |
     if e instanceof NumericOrCharType
-    then result.(BoxedType).getPrimitiveType().getName() = "double"
+    then numericRepresentative(result)
     else
       if e instanceof BooleanType
-      then result.(BoxedType).getPrimitiveType().getName() = "boolean"
+      then booleanRepresentative(result)
       else result = e
   )
   or

java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll

@@ -562,14 +562,20 @@ private module Cached {
 
     cached // nothing is actually cached
     module BarrierGuard<guardChecksSig/3 guardChecks> {
-      private predicate guardChecksAdjTypes(
-        DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e, boolean branch
-      ) {
+      private predicate guardChecksAdjTypes(Guards::Guards_v3::Guard g, Expr e, boolean branch) {
         guardChecks(g, e, branch)
       }
 
+      private predicate guardChecksWithWrappers(
+        DataFlowIntegrationInput::Guard g, Definition def, Guards::GuardValue val, Unit state
+      ) {
+        Guards::Guards_v3::ValidationWrapper<guardChecksAdjTypes/3>::guardChecksDef(g, def, val) and
+        exists(state)
+      }
+
       private Node getABarrierNodeImpl() {
-        result = DataFlowIntegrationImpl::BarrierGuard<guardChecksAdjTypes/3>::getABarrierNode()
+        result =
+          DataFlowIntegrationImpl::BarrierGuardDefWithState<Unit, guardChecksWithWrappers/4>::getABarrierNode(_)
       }
 
       predicate getABarrierNode = getABarrierNodeImpl/0;
@@ -657,16 +663,18 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
     def instanceof SsaUncertainImplicitUpdate
   }
 
+  class GuardValue = Guards::GuardValue;
+
   class Guard = Guards::Guard;
 
-  /** Holds if the guard `guard` directly controls block `bb` upon evaluating to `branch`. */
-  predicate guardDirectlyControlsBlock(Guard guard, BasicBlock bb, boolean branch) {
-    guard.directlyControls(bb, branch)
+  /** Holds if the guard `guard` directly controls block `bb` upon evaluating to `val`. */
+  predicate guardDirectlyControlsBlock(Guard guard, BasicBlock bb, GuardValue val) {
+    guard.directlyValueControls(bb, val)
   }
 
-  /** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */
-  predicate guardControlsBlock(Guard guard, BasicBlock bb, boolean branch) {
-    guard.controls(bb, branch)
+  /** Holds if the guard `guard` controls block `bb` upon evaluating to `val`. */
+  predicate guardControlsBlock(Guard guard, BasicBlock bb, GuardValue val) {
+    guard.valueControls(bb, val)
   }
 
   predicate includeWriteDefsInFlowStep() { none() }

java/ql/lib/semmle/code/java/dispatch/ObjFlow.qll

@@ -214,24 +214,35 @@ private predicate relevantNode(ObjNode n) {
   exists(ObjNode mid | relevantNode(mid) and objStep(mid, n) and relevantNodeBack(n))
 }
 
-pragma[noinline]
-private predicate objStepPruned(ObjNode n1, ObjNode n2) {
-  objStep(n1, n2) and relevantNode(n1) and relevantNode(n2)
+private newtype TObjFlowNode =
+  TObjNode(ObjNode n) { relevantNode(n) } or
+  TObjType(RefType t) { source(t, _) }
+
+private predicate objStepPruned(TObjFlowNode node1, TObjFlowNode node2) {
+  exists(ObjNode n1, ObjNode n2 |
+    node1 = TObjNode(n1) and
+    node2 = TObjNode(n2) and
+    objStep(n1, n2)
+  )
+  or
+  exists(RefType t, ObjNode n |
+    node1 = TObjType(t) and
+    node2 = TObjNode(n) and
+    source(t, n)
+  )
 }
 
-private predicate stepPlus(Node n1, Node n2) = fastTC(objStepPruned/2)(n1, n2)
+private predicate flowSrc(TObjFlowNode src) { src instanceof TObjType }
+
+private predicate flowSink(TObjFlowNode sink) { exists(ObjNode n | sink = TObjNode(n) and sink(n)) }
+
+private predicate stepPlus(TObjFlowNode n1, TObjFlowNode n2) =
+  doublyBoundedFastTC(objStepPruned/2, flowSrc/1, flowSink/1)(n1, n2)
 
 /**
  * Holds if the qualifier `n` of an `Object.toString()` call might have type `t`.
  */
-pragma[noopt]
-private predicate objType(ObjNode n, RefType t) {
-  exists(ObjNode n2 |
-    sink(n) and
-    (stepPlus(n2, n) or n2 = n) and
-    source(t, n2)
-  )
-}
+private predicate objType(ObjNode n, RefType t) { stepPlus(TObjType(t), TObjNode(n)) }
 
 private VirtualMethodCall objectToString(ObjNode n) {
   result.getQualifier() = n.asExpr() and sink(n)

java/ql/lib/semmle/code/java/security/AndroidSensitiveCommunicationQuery.qll

@@ -149,6 +149,8 @@ module SensitiveCommunicationConfig implements DataFlow::ConfigSig {
   predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
     isSink(node) and exists(c)
   }
+
+  predicate observeDiffInformedIncrementalMode() { any() }
 }
 
 /**

java/ql/lib/semmle/code/java/security/ArithmeticCommon.qll

@@ -20,16 +20,16 @@ predicate narrowerThanOrEqualTo(ArithExpr exp, NumType numType) {
   exists(CastingExpr cast | cast.getAChildExpr() = exp | numType.widerThanOrEqualTo(cast.getType()))
 }
 
-private Guard sizeGuard(SsaVariable v, boolean branch, boolean upper) {
+private Guard sizeGuard(Expr e, boolean branch, boolean upper) {
   exists(ComparisonExpr comp | comp = result |
-    comp.getLesserOperand() = ssaRead(v, 0) and
+    comp.getLesserOperand() = e and
     (
       branch = true and upper = true
       or
       branch = false and upper = false
     )
     or
-    comp.getGreaterOperand() = ssaRead(v, 0) and
+    comp.getGreaterOperand() = e and
     (
       branch = true and upper = false
       or
@@ -38,7 +38,7 @@ private Guard sizeGuard(SsaVariable v, boolean branch, boolean upper) {
     or
     exists(MethodCall ma |
       ma.getMethod() instanceof MethodAbs and
-      ma.getArgument(0) = ssaRead(v, 0) and
+      ma.getArgument(0) = e and
       (
         comp.getLesserOperand() = ma and branch = true
         or
@@ -49,7 +49,7 @@ private Guard sizeGuard(SsaVariable v, boolean branch, boolean upper) {
     or
     // overflow test
     exists(AddExpr add, VarRead use, Expr pos |
-      use = ssaRead(v, 0) and
+      use = e and
       add.hasOperands(use, pos) and
       positive(use) and
       positive(pos) and
@@ -65,70 +65,38 @@ private Guard sizeGuard(SsaVariable v, boolean branch, boolean upper) {
     )
   )
   or
-  result.isEquality(ssaRead(v, 0), _, branch) and
+  result.isEquality(e, _, branch) and
   (upper = true or upper = false)
-  or
-  exists(MethodCall call, Method m, int ix |
-    call = result and
-    call.getArgument(ix) = ssaRead(v, 0) and
-    call.getMethod().getSourceDeclaration() = m and
-    m = customSizeGuard(ix, branch, upper)
-  )
 }
 
-private Guard derivedSizeGuard(SsaVariable v, boolean branch, boolean upper) {
-  result = sizeGuard(v, branch, upper) or
-  exists(boolean branch0 | implies_v3(result, branch, derivedSizeGuard(v, branch0, upper), branch0))
+private predicate sizeGuardLessThan(Guard g, Expr e, boolean branch) {
+  g = sizeGuard(e, branch, true)
 }
 
-private Method customSizeGuard(int index, boolean retval, boolean upper) {
-  exists(Parameter p, SsaImplicitInit v |
-    result.getReturnType().(PrimitiveType).hasName("boolean") and
-    not result.isOverridable() and
-    p.getCallable() = result and
-    not p.isVarargs() and
-    p.getType() instanceof NumericOrCharType and
-    p.getPosition() = index and
-    v.isParameterDefinition(p) and
-    forex(ReturnStmt ret |
-      ret.getEnclosingCallable() = result and
-      exists(Expr res | res = ret.getResult() |
-        not res.(BooleanLiteral).getBooleanValue() = retval.booleanNot()
-      )
-    |
-      ret.getResult() = derivedSizeGuard(v, retval, upper)
-    )
-  )
+private predicate sizeGuardGreaterThan(Guard g, Expr e, boolean branch) {
+  g = sizeGuard(e, branch, false)
 }
 
 /**
- * Holds if `e` is bounded in a way that is likely to prevent overflow.
+ * Holds if `n` is bounded in a way that is likely to prevent overflow.
  */
-predicate guardedLessThanSomething(Expr e) {
-  exists(SsaVariable v, Guard guard, boolean branch |
-    e = v.getAUse() and
-    guard = sizeGuard(v.getAPhiInputOrPriorDef*(), branch, true) and
-    guard.controls(e.getBasicBlock(), branch)
-  )
+predicate guardedLessThanSomething(DataFlow::Node n) {
+  DataFlow::BarrierGuard<sizeGuardLessThan/3>::getABarrierNode() = n
   or
-  negative(e)
+  negative(n.asExpr())
   or
-  e.(MethodCall).getMethod() instanceof MethodMathMin
+  n.asExpr().(MethodCall).getMethod() instanceof MethodMathMin
 }
 
 /**
  * Holds if `e` is bounded in a way that is likely to prevent underflow.
  */
-predicate guardedGreaterThanSomething(Expr e) {
-  exists(SsaVariable v, Guard guard, boolean branch |
-    e = v.getAUse() and
-    guard = sizeGuard(v.getAPhiInputOrPriorDef*(), branch, false) and
-    guard.controls(e.getBasicBlock(), branch)
-  )
+predicate guardedGreaterThanSomething(DataFlow::Node n) {
+  DataFlow::BarrierGuard<sizeGuardGreaterThan/3>::getABarrierNode() = n
   or
-  positive(e)
+  positive(n.asExpr())
   or
-  e.(MethodCall).getMethod() instanceof MethodMathMax
+  n.asExpr().(MethodCall).getMethod() instanceof MethodMathMax
 }
 
 /** Holds if `e` occurs in a context where it will be upcast to a wider type. */
@@ -182,7 +150,7 @@ private predicate unlikelyNode(DataFlow::Node n) {
 /** Holds if `n` is likely guarded against overflow. */
 predicate overflowBarrier(DataFlow::Node n) {
   n.getType() instanceof BooleanType or
-  guardedLessThanSomething(n.asExpr()) or
+  guardedLessThanSomething(n) or
   unlikelyNode(n) or
   upcastToWiderType(n.asExpr()) or
   overflowIrrelevant(n.asExpr())
@@ -191,7 +159,7 @@ predicate overflowBarrier(DataFlow::Node n) {
 /** Holds if `n` is likely guarded against underflow. */
 predicate underflowBarrier(DataFlow::Node n) {
   n.getType() instanceof BooleanType or
-  guardedGreaterThanSomething(n.asExpr()) or
+  guardedGreaterThanSomething(n) or
   unlikelyNode(n) or
   upcastToWiderType(n.asExpr()) or
   overflowIrrelevant(n.asExpr())
@@ -210,7 +178,6 @@ predicate overflowSink(ArithExpr exp, VarAccess use) {
     exp instanceof PostIncExpr or
     exp instanceof MulExpr
   ) and
-  not guardedLessThanSomething(use) and
   // Exclude widening conversions of tainted values due to binary numeric promotion (JLS 5.6.2)
   // unless there is an enclosing cast down to a narrower type.
   narrowerThanOrEqualTo(exp, use.getType()) and
@@ -230,7 +197,6 @@ predicate underflowSink(ArithExpr exp, VarAccess use) {
     exp instanceof PostDecExpr or
     exp instanceof MulExpr
   ) and
-  not guardedGreaterThanSomething(use) and
   // Exclude widening conversions of tainted values due to binary numeric promotion (JLS 5.6.2)
   // unless there is an enclosing cast down to a narrower type.
   narrowerThanOrEqualTo(exp, use.getType()) and

java/ql/lib/semmle/code/java/security/ArithmeticTaintedQuery.qll

@@ -13,6 +13,14 @@ module ArithmeticOverflowConfig implements DataFlow::ConfigSig {
   predicate isBarrier(DataFlow::Node n) { overflowBarrier(n) }
 
   predicate isBarrierIn(DataFlow::Node node) { isSource(node) }
+
+  predicate observeDiffInformedIncrementalMode() {
+    any() // merged with ArithmeticUnderflow in ArithmeticTainted.ql
+  }
+
+  Location getASelectedSinkLocation(DataFlow::Node sink) {
+    exists(ArithExpr exp | result = exp.getLocation() | overflowSink(exp, sink.asExpr()))
+  }
 }
 
 /**
@@ -29,6 +37,14 @@ module ArithmeticUnderflowConfig implements DataFlow::ConfigSig {
   predicate isBarrier(DataFlow::Node n) { underflowBarrier(n) }
 
   predicate isBarrierIn(DataFlow::Node node) { isSource(node) }
+
+  predicate observeDiffInformedIncrementalMode() {
+    any() // merged with ArithmeticOverflow in ArithmeticTainted.ql
+  }
+
+  Location getASelectedSinkLocation(DataFlow::Node sink) {
+    exists(ArithExpr exp | result = exp.getLocation() | underflowSink(exp, sink.asExpr()))
+  }
 }
 
 /**

java/ql/lib/semmle/code/java/security/ArithmeticUncontrolledQuery.qll

@@ -19,6 +19,14 @@ module ArithmeticUncontrolledOverflowConfig implements DataFlow::ConfigSig {
   predicate isSink(DataFlow::Node sink) { overflowSink(_, sink.asExpr()) }
 
   predicate isBarrier(DataFlow::Node n) { overflowBarrier(n) }
+
+  predicate observeDiffInformedIncrementalMode() {
+    any() // merged with ArithmeticUncontrolledUnderflow in ArithmeticUncontrolled.ql
+  }
+
+  Location getASelectedSinkLocation(DataFlow::Node sink) {
+    exists(ArithExpr exp | result = exp.getLocation() | overflowSink(exp, sink.asExpr()))
+  }
 }
 
 /** Taint-tracking flow to reason about overflow from arithmetic with uncontrolled values. */
@@ -32,6 +40,14 @@ module ArithmeticUncontrolledUnderflowConfig implements DataFlow::ConfigSig {
   predicate isSink(DataFlow::Node sink) { underflowSink(_, sink.asExpr()) }
 
   predicate isBarrier(DataFlow::Node n) { underflowBarrier(n) }
+
+  predicate observeDiffInformedIncrementalMode() {
+    any() // merged with ArithmeticUncontrolledOverflow in ArithmeticUncontrolled.ql
+  }
+
+  Location getASelectedSinkLocation(DataFlow::Node sink) {
+    exists(ArithExpr exp | result = exp.getLocation() | underflowSink(exp, sink.asExpr()))
+  }
 }
 
 /** Taint-tracking flow to reason about underflow from arithmetic with uncontrolled values. */

java/ql/lib/semmle/code/java/security/ConditionalBypassQuery.qll

@@ -47,6 +47,15 @@ module ConditionalBypassFlowConfig implements DataFlow::ConfigSig {
   predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
     endsWithStep(node1, node2)
   }
+
+  predicate observeDiffInformedIncrementalMode() { any() }
+
+  Location getASelectedSinkLocation(DataFlow::Node sink) {
+    exists(MethodCall m, Expr e | result = [m, e].getLocation() |
+      conditionControlsMethod(m, e) and
+      sink.asExpr() = e
+    )
+  }
 }
 
 /**

java/ql/lib/semmle/code/java/security/CsrfUnprotectedRequestTypeQuery.qll

@@ -237,12 +237,35 @@ private predicate sink(CallPathNode sinkMethodCall) {
   )
 }
 
+private predicate fwdFlow(CallPathNode n) {
+  source(n)
+  or
+  exists(CallPathNode mid | fwdFlow(mid) and CallGraph::edges(mid, n))
+}
+
+private predicate revFlow(CallPathNode n) {
+  fwdFlow(n) and
+  (
+    sink(n)
+    or
+    exists(CallPathNode mid | revFlow(mid) and CallGraph::edges(n, mid))
+  )
+}
+
+/**
+ * Holds if `pred` has a successor node `succ` and this edge is in an
+ * `unprotectedStateChange` path.
+ */
+predicate relevantEdge(CallPathNode pred, CallPathNode succ) {
+  CallGraph::edges(pred, succ) and revFlow(pred) and revFlow(succ)
+}
+
 /**
  * Holds if `sourceMethod` is an unprotected request handler that reaches a
  * `sinkMethodCall` that updates a database.
  */
 private predicate unprotectedDatabaseUpdate(CallPathNode sourceMethod, CallPathNode sinkMethodCall) =
-  doublyBoundedFastTC(CallGraph::edges/2, source/1, sink/1)(sourceMethod, sinkMethodCall)
+  doublyBoundedFastTC(relevantEdge/2, source/1, sink/1)(sourceMethod, sinkMethodCall)
 
 /**
  * Holds if `sourceMethod` is an unprotected request handler that appears to

java/ql/lib/semmle/code/java/security/ExternalAPIs.qll

@@ -101,6 +101,10 @@ module UntrustedDataToExternalApiConfig implements DataFlow::ConfigSig {
   predicate isSource(DataFlow::Node source) { source instanceof ActiveThreatModelSource }
 
   predicate isSink(DataFlow::Node sink) { sink instanceof ExternalApiDataNode }
+
+  predicate observeDiffInformedIncrementalMode() {
+    any() // Simple use in UntrustedDataToExternalAPI.ql; also used through ExternalApiUsedWithUntrustedData in ExternalAPIsUsedWithUntrustedData.ql
+  }
 }
 
 /**

java/ql/lib/semmle/code/java/security/ImproperValidationOfArrayConstructionCodeSpecifiedQuery.qll

@@ -17,6 +17,15 @@ module BoundedFlowSourceConfig implements DataFlow::ConfigSig {
   predicate isSink(DataFlow::Node sink) {
     any(CheckableArrayAccess caa).canThrowOutOfBoundsDueToEmptyArray(sink.asExpr(), _)
   }
+
+  predicate observeDiffInformedIncrementalMode() { any() }
+
+  Location getASelectedSinkLocation(DataFlow::Node sink) {
+    exists(ArrayCreationExpr arrayCreation, CheckableArrayAccess arrayAccess |
+      result = [arrayCreation, arrayAccess.getIndexExpr()].getLocation() and
+      arrayAccess.canThrowOutOfBoundsDueToEmptyArray(sink.asExpr(), arrayCreation)
+    )
+  }
 }
 
 /**

java/ql/lib/semmle/code/java/security/ImproperValidationOfArrayConstructionQuery.qll

@@ -14,6 +14,15 @@ module ImproperValidationOfArrayConstructionConfig implements DataFlow::ConfigSi
   predicate isSink(DataFlow::Node sink) {
     any(CheckableArrayAccess caa).canThrowOutOfBoundsDueToEmptyArray(sink.asExpr(), _)
   }
+
+  predicate observeDiffInformedIncrementalMode() { any() }
+
+  Location getASelectedSinkLocation(DataFlow::Node sink) {
+    exists(ArrayCreationExpr arrayCreation, CheckableArrayAccess arrayAccess |
+      result = [arrayCreation, arrayAccess.getIndexExpr()].getLocation() and
+      arrayAccess.canThrowOutOfBoundsDueToEmptyArray(sink.asExpr(), arrayCreation)
+    )
+  }
 }
 
 /**

java/ql/lib/semmle/code/java/security/ImproperValidationOfArrayIndexCodeSpecifiedQuery.qll

@@ -14,6 +14,8 @@ module BoundedFlowSourceConfig implements DataFlow::ConfigSig {
   predicate isSink(DataFlow::Node sink) {
     exists(CheckableArrayAccess arrayAccess | arrayAccess.canThrowOutOfBounds(sink.asExpr()))
   }
+
+  predicate observeDiffInformedIncrementalMode() { any() }
 }
 
 /**

java/ql/lib/semmle/code/java/security/ImproperValidationOfArrayIndexQuery.qll

@@ -18,6 +18,8 @@ module ImproperValidationOfArrayIndexConfig implements DataFlow::ConfigSig {
   predicate isBarrier(DataFlow::Node node) { node.getType() instanceof BooleanType }
 
   predicate isBarrierIn(DataFlow::Node node) { isSource(node) }
+
+  predicate observeDiffInformedIncrementalMode() { any() }
 }
 
 /**

java/ql/lib/semmle/code/java/security/InsecureCookieQuery.qll

@@ -35,6 +35,10 @@ module SecureCookieConfig implements DataFlow::ConfigSig {
     sink.asExpr() =
       any(MethodCall add | add.getMethod() instanceof ResponseAddCookieMethod).getArgument(0)
   }
+
+  predicate observeDiffInformedIncrementalMode() {
+    none() // only used negatively in InsecureCookie.ql
+  }
 }
 
 /** Data flow to reason about the failure to use secure cookies. */

java/ql/lib/semmle/code/java/security/InsecureLdapAuthQuery.qll

@@ -40,6 +40,10 @@ private module BasicAuthConfig implements DataFlow::ConfigSig {
   }
 
   predicate isSink(DataFlow::Node sink) { sink instanceof InsecureLdapUrlSink }
+
+  predicate observeDiffInformedIncrementalMode() {
+    none() // used as secondary flow to InsecureLdapUrlFlow in InsecureLdapAuth.ql
+  }
 }
 
 module BasicAuthFlow = DataFlow::Global<BasicAuthConfig>;
@@ -56,6 +60,10 @@ private module RequiresSslConfig implements DataFlow::ConfigSig {
   }
 
   predicate isSink(DataFlow::Node sink) { sink instanceof InsecureLdapUrlSink }
+
+  predicate observeDiffInformedIncrementalMode() {
+    none() // only used negatively in InsecureLdapAuth.ql
+  }
 }
 
 module RequiresSslFlow = DataFlow::Global<RequiresSslConfig>;

java/ql/lib/semmle/code/java/security/LogInjectionQuery.qll

@@ -19,6 +19,10 @@ module LogInjectionConfig implements DataFlow::ConfigSig {
   }
 
   predicate isBarrierIn(DataFlow::Node node) { isSource(node) }
+
+  predicate observeDiffInformedIncrementalMode() {
+    none() // straightforward case; but the large test source is causing OOMs under `--check-diff-informed`.
+  }
 }
 
 /**

java/ql/lib/semmle/code/java/security/MaybeBrokenCryptoAlgorithmQuery.qll

@@ -77,6 +77,12 @@ module InsecureCryptoConfig implements DataFlow::ConfigSig {
     objectToString(n.asExpr()) or
     n.getType().getErasure() instanceof TypeObject
   }
+
+  predicate observeDiffInformedIncrementalMode() { any() }
+
+  Location getASelectedSinkLocation(DataFlow::Node sink) {
+    exists(CryptoAlgoSpec c | result = c.getLocation() | sink.asExpr() = c.getAlgoSpec())
+  }
 }
 
 /**

java/ql/lib/semmle/code/java/security/PathSanitizer.qll

@@ -13,33 +13,6 @@ private import semmle.code.java.dataflow.Nullness
 /** A sanitizer that protects against path injection vulnerabilities. */
 abstract class PathInjectionSanitizer extends DataFlow::Node { }
 
-/**
- * Provides a set of nodes validated by a method that uses a validation guard.
- */
-private module ValidationMethod<DataFlow::guardChecksSig/3 validationGuard> {
-  /** Gets a node that is safely guarded by a method that uses the given guard check. */
-  DataFlow::Node getAValidatedNode() {
-    exists(MethodCall ma, int pos, VarRead rv |
-      validationMethod(ma.getMethod(), pos) and
-      ma.getArgument(pos) = rv and
-      adjacentUseUseSameVar(rv, result.asExpr()) and
-      ma.getBasicBlock().dominates(result.asExpr().getBasicBlock())
-    )
-  }
-
-  /**
-   * Holds if `m` validates its `arg`th parameter by using `validationGuard`.
-   */
-  private predicate validationMethod(Method m, int arg) {
-    exists(Guard g, SsaImplicitInit var, ControlFlow::NormalExitNode normexit, boolean branch |
-      validationGuard(g, var.getAUse(), branch) and
-      var.isParameterDefinition(m.getParameter(arg)) and
-      normexit.getEnclosingCallable() = m and
-      g.controls(normexit.getBasicBlock(), branch)
-    )
-  }
-}
-
 /**
  * Holds if `g` is guard that compares a path to a trusted value.
  */
@@ -68,8 +41,6 @@ private predicate exactPathMatchGuard(Guard g, Expr e, boolean branch) {
 class ExactPathMatchSanitizer extends PathInjectionSanitizer {
   ExactPathMatchSanitizer() {
     this = DataFlow::BarrierGuard<exactPathMatchGuard/3>::getABarrierNode()
-    or
-    this = ValidationMethod<exactPathMatchGuard/3>::getAValidatedNode()
   }
 }
 
@@ -120,8 +91,7 @@ private predicate allowedPrefixGuard(Guard g, Expr e, boolean branch) {
 
 private class AllowedPrefixSanitizer extends PathInjectionSanitizer {
   AllowedPrefixSanitizer() {
-    this = DataFlow::BarrierGuard<allowedPrefixGuard/3>::getABarrierNode() or
-    this = ValidationMethod<allowedPrefixGuard/3>::getAValidatedNode()
+    this = DataFlow::BarrierGuard<allowedPrefixGuard/3>::getABarrierNode()
   }
 }
 
@@ -139,10 +109,7 @@ private predicate dotDotCheckGuard(Guard g, Expr e, boolean branch) {
 }
 
 private class DotDotCheckSanitizer extends PathInjectionSanitizer {
-  DotDotCheckSanitizer() {
-    this = DataFlow::BarrierGuard<dotDotCheckGuard/3>::getABarrierNode() or
-    this = ValidationMethod<dotDotCheckGuard/3>::getAValidatedNode()
-  }
+  DotDotCheckSanitizer() { this = DataFlow::BarrierGuard<dotDotCheckGuard/3>::getABarrierNode() }
 }
 
 private class BlockListGuard extends PathGuard instanceof MethodCall {
@@ -179,10 +146,7 @@ private predicate blockListGuard(Guard g, Expr e, boolean branch) {
 }
 
 private class BlockListSanitizer extends PathInjectionSanitizer {
-  BlockListSanitizer() {
-    this = DataFlow::BarrierGuard<blockListGuard/3>::getABarrierNode() or
-    this = ValidationMethod<blockListGuard/3>::getAValidatedNode()
-  }
+  BlockListSanitizer() { this = DataFlow::BarrierGuard<blockListGuard/3>::getABarrierNode() }
 }
 
 private class ConstantOrRegex extends Expr {
@@ -368,7 +332,6 @@ private class FileConstructorChildArgumentStep extends AdditionalTaintStep {
       n2.asExpr() = constrCall
     |
       not n1 = DataFlow::BarrierGuard<pathTraversalGuard/3>::getABarrierNode() and
-      not n1 = ValidationMethod<pathTraversalGuard/3>::getAValidatedNode() and
       not TaintTracking::localExprTaint(any(PathNormalizeSanitizer p), n1.asExpr())
       or
       DataFlow::localExprFlow(nullExpr(), constrCall.getArgument(0))
@@ -546,7 +509,6 @@ private predicate directoryCharactersGuard(Guard g, Expr e, boolean branch) {
 private class DirectoryCharactersSanitizer extends PathInjectionSanitizer {
   DirectoryCharactersSanitizer() {
     this.asExpr() instanceof ReplaceDirectoryCharactersSanitizer or
-    this = DataFlow::BarrierGuard<directoryCharactersGuard/3>::getABarrierNode() or
-    this = ValidationMethod<directoryCharactersGuard/3>::getAValidatedNode()
+    this = DataFlow::BarrierGuard<directoryCharactersGuard/3>::getABarrierNode()
   }
 }

java/ql/lib/semmle/code/java/security/SensitiveLoggingQuery.qll

@@ -53,6 +53,8 @@ module SensitiveLoggerConfig implements DataFlow::ConfigSig {
   }
 
   predicate isBarrierIn(DataFlow::Node node) { isSource(node) }
+
+  predicate observeDiffInformedIncrementalMode() { any() }
 }
 
 module SensitiveLoggerFlow = TaintTracking::Global<SensitiveLoggerConfig>;

java/ql/lib/semmle/code/java/security/SqlConcatenatedQuery.qll

@@ -24,6 +24,15 @@ module UncontrolledStringBuilderSourceFlowConfig implements DataFlow::ConfigSig
   predicate isSink(DataFlow::Node sink) { sink instanceof QueryInjectionSink }
 
   predicate isBarrier(DataFlow::Node node) { node instanceof SimpleTypeSanitizer }
+
+  predicate observeDiffInformedIncrementalMode() { any() }
+
+  Location getASelectedSourceLocation(DataFlow::Node source) {
+    exists(Expr uncontrolled, StringBuilderVar sbv | result = uncontrolled.getLocation() |
+      uncontrolledStringBuilderQuery(sbv, uncontrolled) and
+      source = DataFlow::exprNode(sbv.getToStringCall())
+    )
+  }
 }
 
 /**

java/ql/lib/semmle/code/java/security/TaintedEnvironmentVariableQuery.qll

@@ -38,6 +38,10 @@ module ExecTaintedEnvironmentConfig implements DataFlow::ConfigSig {
       ProcessBuilderEnvironmentFlow::flowToExpr(mm.getQualifier())
     )
   }
+
+  predicate observeDiffInformedIncrementalMode() { any() }
+
+  Location getASelectedSourceLocation(DataFlow::Node source) { none() }
 }
 
 /**

java/ql/lib/semmle/code/java/security/TempDirLocalInformationDisclosureQuery.qll

@@ -145,6 +145,10 @@ module TempDirSystemGetPropertyToCreateConfig implements DataFlow::ConfigSig {
     or
     sanitizer instanceof WindowsOsSanitizer
   }
+
+  predicate observeDiffInformedIncrementalMode() { any() }
+
+  Location getASelectedSinkLocation(DataFlow::Node sink) { none() }
 }
 
 /**

java/ql/lib/semmle/code/java/security/TrustBoundaryViolationQuery.qll

@@ -62,6 +62,8 @@ module TrustBoundaryConfig implements DataFlow::ConfigSig {
   }
 
   predicate isSink(DataFlow::Node sink) { sink instanceof TrustBoundaryViolationSink }
+
+  predicate observeDiffInformedIncrementalMode() { any() }
 }
 
 /**

java/ql/lib/semmle/code/java/security/UnsafeCertTrustQuery.qll

@@ -14,6 +14,10 @@ module SslEndpointIdentificationFlowConfig implements DataFlow::ConfigSig {
   predicate isSink(DataFlow::Node sink) { sink instanceof SslConnectionCreation }
 
   predicate isBarrier(DataFlow::Node sanitizer) { sanitizer instanceof SslUnsafeCertTrustSanitizer }
+
+  predicate observeDiffInformedIncrementalMode() { any() }
+
+  Location getASelectedSourceLocation(DataFlow::Node source) { none() }
 }
 
 /**