From 5c0dcd980d2eb474863e49d4d9f17749ff7995f9 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Thu, 15 May 2025 16:23:21 +0200
Subject: [PATCH] Java: Switch to the shared Guards library.

---
 .../code/java/controlflow/BasicBlocks.qll     |  11 +
 .../semmle/code/java/controlflow/Guards.qll   | 627 +++++++++++-------
 .../java/controlflow/internal/GuardsLogic.qll | 396 -----------
 .../semmle/code/java/dataflow/NullGuards.qll  | 110 +--
 .../semmle/code/java/dataflow/Nullness.qll    |  27 +-
 .../code/java/dataflow/RangeAnalysis.qll      |   5 +-
 .../semmle/code/java/dataflow/RangeUtils.qll  |   2 +-
 .../java/dataflow/internal/DataFlowNodes.qll  |   2 -
 .../rangeanalysis/ModulusAnalysisSpecific.qll |   2 +-
 .../rangeanalysis/SignAnalysisSpecific.qll    |   2 +-
 .../code/java/security/ArithmeticCommon.qll   |   1 -
 .../ql/src/Language Abuse/UselessNullCheck.ql |   2 +-
 java/ql/test/library-tests/guards/Guards.java |  30 +-
 .../guards/GuardsInline.expected              |  35 +-
 .../test/library-tests/guards/GuardsInline.ql |   9 +
 .../library-tests/guards12/guard.expected     |   8 -
 java/ql/test/library-tests/guards12/guard.ql  |   4 +-
 java/ql/test/query-tests/Nullness/C.java      |   2 +-
 .../query-tests/Nullness/NullMaybe.expected   |   1 -
 19 files changed, 488 insertions(+), 788 deletions(-)
 delete mode 100644 java/ql/lib/semmle/code/java/controlflow/internal/GuardsLogic.qll

diff --git a/java/ql/lib/semmle/code/java/controlflow/BasicBlocks.qll b/java/ql/lib/semmle/code/java/controlflow/BasicBlocks.qll
index 284ee1dad0c..7c9e58b20ce 100644
--- a/java/ql/lib/semmle/code/java/controlflow/BasicBlocks.qll
+++ b/java/ql/lib/semmle/code/java/controlflow/BasicBlocks.qll
@@ -85,6 +85,17 @@ class BasicBlock extends BbImpl::BasicBlock {
    */
   predicate dominates(BasicBlock bb) { super.dominates(bb) }
 
+  /**
+   * Holds if this basic block strictly dominates basic block `bb`.
+   *
+   * That is, all paths reaching `bb` from the entry point basic block must
+   * go through this basic block and this basic block is different from `bb`.
+   */
+  predicate strictlyDominates(BasicBlock bb) { super.strictlyDominates(bb) }
+
+  /** Gets an immediate successor of this basic block of a given type, if any. */
+  BasicBlock getASuccessor(Input::SuccessorType t) { result = super.getASuccessor(t) }
+
   /**
    * DEPRECATED: Use `getASuccessor` instead.
    *
diff --git a/java/ql/lib/semmle/code/java/controlflow/Guards.qll b/java/ql/lib/semmle/code/java/controlflow/Guards.qll
index 4042e7b2962..be023939b8c 100644
--- a/java/ql/lib/semmle/code/java/controlflow/Guards.qll
+++ b/java/ql/lib/semmle/code/java/controlflow/Guards.qll
@@ -5,9 +5,9 @@
 
 import java
 private import semmle.code.java.controlflow.Dominance
-private import semmle.code.java.controlflow.internal.GuardsLogic
 private import semmle.code.java.controlflow.internal.Preconditions
 private import semmle.code.java.controlflow.internal.SwitchCases
+private import codeql.controlflow.Guards as SharedGuards
 
 /**
  * A basic block that terminates in a condition, splitting the subsequent control flow.
@@ -137,68 +137,382 @@ private predicate isNonFallThroughPredecessor(SwitchCase sc, ControlFlowNode pre
   )
 }
 
-/**
- * A condition that can be evaluated to either true or false. This can either
- * be an `Expr` of boolean type that isn't a boolean literal, or a case of a
- * switch statement, or a method access that acts as a precondition check.
- *
- * Evaluating a switch case to true corresponds to taking that switch case, and
- * evaluating it to false corresponds to taking some other branch.
- */
-final class Guard extends ExprParent {
-  Guard() {
-    this.(Expr).getType() instanceof BooleanType and not this instanceof BooleanLiteral
-    or
-    this instanceof SwitchCase
-    or
-    conditionCheckArgument(this, _, _)
+private module GuardsInput implements SharedGuards::InputSig<Location> {
+  private import java as J
+  private import semmle.code.java.dataflow.NullGuards as NullGuards
+  import SuccessorType
+
+  class ControlFlowNode = J::ControlFlowNode;
+
+  class BasicBlock = J::BasicBlock;
+
+  predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2) { J::dominatingEdge(bb1, bb2) }
+
+  class AstNode = ExprParent;
+
+  class Expr = J::Expr;
+
+  private newtype TConstantValue =
+    TCharValue(string c) { any(CharacterLiteral lit).getValue() = c } or
+    TStringValue(string value) { any(CompileTimeConstantExpr c).getStringValue() = value } or
+    TEnumValue(EnumConstant c)
+
+  class ConstantValue extends TConstantValue {
+    string toString() {
+      this = TCharValue(result)
+      or
+      this = TStringValue(result)
+      or
+      exists(EnumConstant c | this = TEnumValue(c) and result = c.toString())
+    }
   }
 
+  abstract class ConstantExpr extends Expr {
+    predicate isNull() { none() }
+
+    boolean asBooleanValue() { none() }
+
+    int asIntegerValue() { none() }
+
+    ConstantValue asConstantValue() { none() }
+  }
+
+  private class NullConstant extends ConstantExpr instanceof J::NullLiteral {
+    override predicate isNull() { any() }
+  }
+
+  private class BooleanConstant extends ConstantExpr instanceof J::BooleanLiteral {
+    override boolean asBooleanValue() { result = super.getBooleanValue() }
+  }
+
+  private class IntegerConstant extends ConstantExpr instanceof J::CompileTimeConstantExpr {
+    override int asIntegerValue() { result = super.getIntValue() }
+  }
+
+  private class CharConstant extends ConstantExpr instanceof J::CharacterLiteral {
+    override ConstantValue asConstantValue() { result = TCharValue(super.getValue()) }
+  }
+
+  private class StringConstant extends ConstantExpr instanceof J::CompileTimeConstantExpr {
+    override ConstantValue asConstantValue() { result = TStringValue(super.getStringValue()) }
+  }
+
+  private class EnumConstantExpr extends ConstantExpr instanceof J::VarAccess {
+    override ConstantValue asConstantValue() {
+      exists(EnumConstant c | this = c.getAnAccess() and result = TEnumValue(c))
+    }
+  }
+
+  class NonNullExpr extends Expr {
+    NonNullExpr() {
+      this = NullGuards::baseNotNullExpr()
+      or
+      exists(Field f |
+        this = f.getAnAccess() and
+        f.isFinal() and
+        f.getInitializer() = NullGuards::baseNotNullExpr()
+      )
+    }
+  }
+
+  class Case extends ExprParent instanceof J::SwitchCase {
+    Expr getSwitchExpr() { result = super.getSelectorExpr() }
+
+    predicate isDefaultCase() { this instanceof DefaultCase }
+
+    ConstantExpr asConstantCase() {
+      exists(ConstCase cc | this = cc |
+        cc.getValue() = result and
+        strictcount(cc.getValue(_)) = 1
+      )
+    }
+
+    private predicate hasPatternCaseMatchEdge(BasicBlock bb1, BasicBlock bb2, boolean isMatch) {
+      exists(ConditionNode patterncase |
+        this instanceof PatternCase and
+        patterncase = super.getControlFlowNode() and
+        bb1.getLastNode() = patterncase and
+        bb2.getFirstNode() = patterncase.getABranchSuccessor(isMatch)
+      )
+    }
+
+    predicate matchEdge(BasicBlock bb1, BasicBlock bb2) {
+      exists(ControlFlowNode pred |
+        // Pattern cases are handled as ConditionBlocks.
+        not this instanceof PatternCase and
+        bb2.getFirstNode() = super.getControlFlowNode() and
+        isNonFallThroughPredecessor(this, pred) and
+        bb1 = pred.getBasicBlock()
+      )
+      or
+      this.hasPatternCaseMatchEdge(bb1, bb2, true)
+    }
+
+    predicate nonMatchEdge(BasicBlock bb1, BasicBlock bb2) {
+      this.hasPatternCaseMatchEdge(bb1, bb2, false)
+    }
+  }
+
+  abstract private class BinExpr extends Expr {
+    Expr getAnOperand() {
+      result = this.(BinaryExpr).getAnOperand() or result = this.(AssignOp).getSource()
+    }
+  }
+
+  class AndExpr extends BinExpr {
+    AndExpr() {
+      this instanceof AndBitwiseExpr or
+      this instanceof AndLogicalExpr or
+      this instanceof AssignAndExpr
+    }
+  }
+
+  class OrExpr extends BinExpr {
+    OrExpr() {
+      this instanceof OrBitwiseExpr or
+      this instanceof OrLogicalExpr or
+      this instanceof AssignOrExpr
+    }
+  }
+
+  class NotExpr extends Expr instanceof J::LogNotExpr {
+    Expr getOperand() { result = this.(J::LogNotExpr).getExpr() }
+  }
+
+  class IdExpr extends Expr {
+    IdExpr() { this instanceof AssignExpr or this instanceof CastExpr }
+
+    Expr getEqualChildExpr() {
+      result = this.(AssignExpr).getSource()
+      or
+      result = this.(CastExpr).getExpr()
+    }
+  }
+
+  private predicate objectsEquals(Method equals) {
+    equals.hasQualifiedName("java.util", "Objects", "equals") and
+    equals.getNumberOfParameters() = 2
+  }
+
+  class EqualityTest extends Expr {
+    EqualityTest() {
+      this instanceof J::EqualityTest or
+      this.(MethodCall).getMethod() instanceof EqualsMethod or
+      objectsEquals(this.(MethodCall).getMethod())
+    }
+
+    Expr getAnOperand() {
+      result = this.(J::EqualityTest).getAnOperand()
+      or
+      result = this.(MethodCall).getAnArgument()
+      or
+      this.(MethodCall).getMethod() instanceof EqualsMethod and
+      result = this.(MethodCall).getQualifier()
+    }
+
+    boolean polarity() {
+      result = this.(J::EqualityTest).polarity()
+      or
+      result = true and not this instanceof J::EqualityTest
+    }
+  }
+
+  class ConditionalExpr extends Expr instanceof J::ConditionalExpr {
+    Expr getCondition() { result = super.getCondition() }
+
+    Expr getThen() { result = super.getTrueExpr() }
+
+    Expr getElse() { result = super.getFalseExpr() }
+  }
+}
+
+private module GuardsImpl = SharedGuards::Make<Location, GuardsInput>;
+
+private module LogicInputCommon {
+  private import semmle.code.java.dataflow.NullGuards as NullGuards
+
+  predicate additionalNullCheck(
+    GuardsImpl::PreGuard guard, GuardValue val, GuardsInput::Expr e, boolean isNull
+  ) {
+    guard.(InstanceOfExpr).getExpr() = e and val.asBooleanValue() = true and isNull = false
+    or
+    exists(MethodCall call |
+      call = guard and
+      call.getAnArgument() = e and
+      NullGuards::nullCheckMethod(call.getMethod(), val.asBooleanValue(), isNull)
+    )
+  }
+}
+
+private module LogicInput_v1 implements GuardsImpl::LogicInputSig {
+  private import semmle.code.java.dataflow.internal.BaseSSA
+
+  final private class FinalBaseSsaVariable = BaseSsaVariable;
+
+  class SsaDefinition extends FinalBaseSsaVariable {
+    GuardsInput::Expr getARead() { result = this.getAUse() }
+  }
+
+  class SsaWriteDefinition extends SsaDefinition instanceof BaseSsaUpdate {
+    GuardsInput::Expr getDefinition() {
+      super.getDefiningExpr().(VariableAssign).getSource() = result or
+      super.getDefiningExpr().(AssignOp) = result
+    }
+  }
+
+  class SsaPhiNode extends SsaDefinition instanceof BaseSsaPhiNode {
+    predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb) {
+      super.hasInputFromBlock(inp, bb)
+    }
+  }
+
+  predicate additionalNullCheck = LogicInputCommon::additionalNullCheck/4;
+
+  predicate additionalImpliesStep(
+    GuardsImpl::PreGuard g1, GuardValue v1, GuardsImpl::PreGuard g2, GuardValue v2
+  ) {
+    exists(MethodCall check, int argIndex |
+      g1 = check and
+      v1.getDualValue().isThrowsException() and
+      conditionCheckArgument(check, argIndex, v2.asBooleanValue()) and
+      g2 = check.getArgument(argIndex)
+    )
+  }
+}
+
+private module LogicInput_v2 implements GuardsImpl::LogicInputSig {
+  private import semmle.code.java.dataflow.SSA as SSA
+
+  final private class FinalSsaVariable = SSA::SsaVariable;
+
+  class SsaDefinition extends FinalSsaVariable {
+    GuardsInput::Expr getARead() { result = this.getAUse() }
+  }
+
+  class SsaWriteDefinition extends SsaDefinition instanceof SSA::SsaExplicitUpdate {
+    GuardsInput::Expr getDefinition() {
+      super.getDefiningExpr().(VariableAssign).getSource() = result or
+      super.getDefiningExpr().(AssignOp) = result
+    }
+  }
+
+  class SsaPhiNode extends SsaDefinition instanceof SSA::SsaPhiNode {
+    predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb) {
+      super.hasInputFromBlock(inp, bb)
+    }
+  }
+
+  predicate additionalNullCheck = LogicInputCommon::additionalNullCheck/4;
+
+  predicate additionalImpliesStep(
+    GuardsImpl::PreGuard g1, GuardValue v1, GuardsImpl::PreGuard g2, GuardValue v2
+  ) {
+    LogicInput_v1::additionalImpliesStep(g1, v1, g2, v2)
+    or
+    CustomGuard::additionalImpliesStep(g1, v1, g2, v2)
+  }
+}
+
+private module LogicInput_v3 implements GuardsImpl::LogicInputSig {
+  private import semmle.code.java.dataflow.IntegerGuards as IntegerGuards
+  import LogicInput_v2
+
+  predicate rangeGuard(GuardsImpl::PreGuard guard, GuardValue val, Expr e, int k, boolean upper) {
+    IntegerGuards::rangeGuard(guard, val.asBooleanValue(), e, k, upper)
+  }
+
+  predicate additionalNullCheck = LogicInputCommon::additionalNullCheck/4;
+
+  predicate additionalImpliesStep = LogicInput_v2::additionalImpliesStep/4;
+}
+
+private module CustomGuardInput implements Guards_v2::CustomGuardInputSig {
+  private import semmle.code.java.dataflow.SSA
+
+  private int parameterPosition() { result in [-1, any(Parameter p).getPosition()] }
+
+  /** A parameter position represented by an integer. */
+  class ParameterPosition extends int {
+    ParameterPosition() { this = parameterPosition() }
+  }
+
+  /** An argument position represented by an integer. */
+  class ArgumentPosition extends int {
+    ArgumentPosition() { this = parameterPosition() }
+  }
+
+  /** Holds if arguments at position `apos` match parameters at position `ppos`. */
+  pragma[inline]
+  predicate parameterMatch(ParameterPosition ppos, ArgumentPosition apos) { ppos = apos }
+
+  final private class FinalMethod = Method;
+
+  class BooleanMethod extends FinalMethod {
+    BooleanMethod() {
+      super.getReturnType().(PrimitiveType).hasName("boolean") and
+      not super.isOverridable()
+    }
+
+    LogicInput_v2::SsaDefinition getParameter(ParameterPosition ppos) {
+      exists(Parameter p |
+        super.getParameter(ppos) = p and
+        not p.isVarargs() and
+        result.(SsaImplicitInit).isParameterDefinition(p)
+      )
+    }
+
+    GuardsInput::Expr getAReturnExpr() {
+      exists(ReturnStmt ret |
+        this = ret.getEnclosingCallable() and
+        ret.getResult() = result
+      )
+    }
+  }
+
+  private predicate booleanMethodCall(MethodCall call, BooleanMethod m) {
+    call.getMethod().getSourceDeclaration() = m
+  }
+
+  class BooleanMethodCall extends GuardsInput::Expr instanceof MethodCall {
+    BooleanMethodCall() { booleanMethodCall(this, _) }
+
+    BooleanMethod getMethod() { booleanMethodCall(this, result) }
+
+    GuardsInput::Expr getArgument(ArgumentPosition apos) { result = super.getArgument(apos) }
+  }
+}
+
+class GuardValue = GuardsImpl::GuardValue;
+
+private module CustomGuard = Guards_v2::CustomGuard<CustomGuardInput>;
+
+/** INTERNAL: Don't use. */
+module Guards_v1 = GuardsImpl::Logic<LogicInput_v1>;
+
+/** INTERNAL: Don't use. */
+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
+ * to evaluate to either true or false depending on whether the case matches.
+ */
+final class Guard extends Guards_v3::Guard {
   /** Gets the immediately enclosing callable whose body contains this guard. */
   Callable getEnclosingCallable() {
     result = this.(Expr).getEnclosingCallable() or
     result = this.(SwitchCase).getEnclosingCallable()
   }
 
-  /** Gets the statement containing this guard. */
-  Stmt getEnclosingStmt() {
-    result = this.(Expr).getEnclosingStmt() or
-    result = this.(SwitchCase).getSwitch() or
-    result = this.(SwitchCase).getSwitchExpr().getEnclosingStmt()
-  }
-
-  /**
-   * Gets the basic block containing this guard or the basic block that tests the
-   * applicability of this switch case -- for a pattern case this is the case statement
-   * itself; for a non-pattern case this is the most recent pattern case or the top of
-   * the switch block if there is none.
-   */
-  BasicBlock getBasicBlock() {
-    // Not a switch case
-    result = this.(Expr).getBasicBlock()
-    or
-    // Return the closest pattern case statement before this one, including this one.
-    result = getClosestPrecedingPatternCase(this).getBasicBlock()
-    or
-    // Not a pattern case and no preceding pattern case -- return the top of the switch block.
-    not exists(getClosestPrecedingPatternCase(this)) and
-    result = this.(SwitchCase).getSelectorExpr().getBasicBlock()
-  }
-
-  /**
-   * Holds if this guard is an equality test between `e1` and `e2`. The test
-   * can be either `==`, `!=`, `.equals`, or a switch case. If the test is
-   * negated, that is `!=`, then `polarity` is false, otherwise `polarity` is
-   * true.
-   */
-  predicate isEquality(Expr e1, Expr e2, boolean polarity) {
-    exists(Expr exp1, Expr exp2 | equalityGuard(this, exp1, exp2, polarity) |
-      e1 = exp1 and e2 = exp2
-      or
-      e2 = exp1 and e1 = exp2
-    )
-  }
-
   /**
    * Holds if this guard tests whether `testedExpr` has type `testedType`.
    *
@@ -231,211 +545,14 @@ final class Guard extends ExprParent {
       else restricted = false
     )
   }
-
-  /**
-   * Holds if the evaluation of this guard to `branch` corresponds to the edge
-   * from `bb1` to `bb2`.
-   */
-  predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) {
-    exists(ConditionBlock cb |
-      cb = bb1 and
-      cb.getCondition() = this and
-      bb2 = cb.getTestSuccessor(branch)
-    )
-    or
-    exists(SwitchCase sc, ControlFlowNode pred |
-      sc = this and
-      // Pattern cases are handled as ConditionBlocks above.
-      not sc instanceof PatternCase and
-      branch = true and
-      bb2.getFirstNode() = sc.getControlFlowNode() and
-      isNonFallThroughPredecessor(sc, pred) and
-      bb1 = pred.getBasicBlock()
-    )
-    or
-    preconditionBranchEdge(this, bb1, bb2, branch)
-  }
-
-  /**
-   * Holds if this guard evaluating to `branch` directly controls the block
-   * `controlled`. That is, the `true`- or `false`-successor of this guard (as
-   * given by `branch`) dominates `controlled`.
-   */
-  predicate directlyControls(BasicBlock controlled, boolean branch) {
-    exists(ConditionBlock cb |
-      cb.getCondition() = this and
-      cb.controls(controlled, branch)
-    )
-    or
-    switchCaseControls(this, controlled) and branch = true
-    or
-    preconditionControls(this, controlled, branch)
-  }
-
-  /**
-   * Holds if this guard evaluating to `branch` controls the control-flow
-   * branch edge from `bb1` to `bb2`. That is, following the edge from
-   * `bb1` to `bb2` implies that this guard evaluated to `branch`.
-   */
-  predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) {
-    guardControlsBranchEdge_v3(this, bb1, bb2, branch)
-  }
-
-  /**
-   * Holds if this guard evaluating to `branch` directly or indirectly controls
-   * the block `controlled`. That is, the evaluation of `controlled` is
-   * dominated by this guard evaluating to `branch`.
-   */
-  predicate controls(BasicBlock controlled, boolean branch) {
-    guardControls_v3(this, controlled, branch)
-  }
-}
-
-private predicate switchCaseControls(SwitchCase sc, BasicBlock bb) {
-  exists(BasicBlock caseblock |
-    // Pattern cases are handled as condition blocks
-    not sc instanceof PatternCase and
-    caseblock.getFirstNode() = sc.getControlFlowNode() and
-    caseblock.dominates(bb) and
-    // Check we can't fall through from a previous block:
-    forall(ControlFlowNode pred | pred = sc.getControlFlowNode().getAPredecessor() |
-      isNonFallThroughPredecessor(sc, pred)
-    )
-  )
-}
-
-private predicate preconditionBranchEdge(
-  MethodCall ma, BasicBlock bb1, BasicBlock bb2, boolean branch
-) {
-  conditionCheckArgument(ma, _, branch) and
-  bb1.getLastNode() = ma.getControlFlowNode() and
-  bb2.getFirstNode() = bb1.getLastNode().getANormalSuccessor()
-}
-
-private predicate preconditionControls(MethodCall ma, BasicBlock controlled, boolean branch) {
-  exists(BasicBlock check, BasicBlock succ |
-    preconditionBranchEdge(ma, check, succ, branch) and
-    dominatingEdge(check, succ) and
-    succ.dominates(controlled)
-  )
 }
 
 /**
- * INTERNAL: Use `Guards.controls` instead.
+ * INTERNAL: Use `Guard.controls` instead.
  *
  * Holds if `guard.controls(controlled, branch)`, except this only relies on
  * BaseSSA-based reasoning.
  */
-predicate guardControls_v1(Guard guard, BasicBlock controlled, boolean branch) {
-  guard.directlyControls(controlled, branch)
-  or
-  exists(Guard g, boolean b |
-    guardControls_v1(g, controlled, b) and
-    implies_v1(g, b, guard, branch)
-  )
-}
-
-/**
- * INTERNAL: Use `Guards.controls` instead.
- *
- * Holds if `guard.controls(controlled, branch)`, except this doesn't rely on
- * RangeAnalysis.
- */
-predicate guardControls_v2(Guard guard, BasicBlock controlled, boolean branch) {
-  guard.directlyControls(controlled, branch)
-  or
-  exists(Guard g, boolean b |
-    guardControls_v2(g, controlled, b) and
-    implies_v2(g, b, guard, branch)
-  )
-}
-
-pragma[nomagic]
-private predicate guardControls_v3(Guard guard, BasicBlock controlled, boolean branch) {
-  guard.directlyControls(controlled, branch)
-  or
-  exists(Guard g, boolean b |
-    guardControls_v3(g, controlled, b) and
-    implies_v3(g, b, guard, branch)
-  )
-}
-
-pragma[nomagic]
-private predicate guardControlsBranchEdge_v2(
-  Guard guard, BasicBlock bb1, BasicBlock bb2, boolean branch
-) {
-  guard.hasBranchEdge(bb1, bb2, branch)
-  or
-  exists(Guard g, boolean b |
-    guardControlsBranchEdge_v2(g, bb1, bb2, b) and
-    implies_v2(g, b, guard, branch)
-  )
-}
-
-pragma[nomagic]
-private predicate guardControlsBranchEdge_v3(
-  Guard guard, BasicBlock bb1, BasicBlock bb2, boolean branch
-) {
-  guard.hasBranchEdge(bb1, bb2, branch)
-  or
-  exists(Guard g, boolean b |
-    guardControlsBranchEdge_v3(g, bb1, bb2, b) and
-    implies_v3(g, b, guard, branch)
-  )
-}
-
-/** INTERNAL: Use `Guard` instead. */
-final class Guard_v2 extends Guard {
-  /**
-   * Holds if this guard evaluating to `branch` controls the control-flow
-   * branch edge from `bb1` to `bb2`. That is, following the edge from
-   * `bb1` to `bb2` implies that this guard evaluated to `branch`.
-   */
-  predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) {
-    guardControlsBranchEdge_v2(this, bb1, bb2, branch)
-  }
-
-  /**
-   * Holds if this guard evaluating to `branch` directly or indirectly controls
-   * the block `controlled`. That is, the evaluation of `controlled` is
-   * dominated by this guard evaluating to `branch`.
-   */
-  predicate controls(BasicBlock controlled, boolean branch) {
-    guardControls_v2(this, controlled, branch)
-  }
-}
-
-private predicate equalityGuard(Guard g, Expr e1, Expr e2, boolean polarity) {
-  exists(EqualityTest eqtest |
-    eqtest = g and
-    polarity = eqtest.polarity() and
-    eqtest.hasOperands(e1, e2)
-  )
-  or
-  exists(MethodCall ma |
-    ma = g and
-    ma.getMethod() instanceof EqualsMethod and
-    polarity = true and
-    ma.getAnArgument() = e1 and
-    ma.getQualifier() = e2
-  )
-  or
-  exists(MethodCall ma, Method equals |
-    ma = g and
-    ma.getMethod() = equals and
-    polarity = true and
-    equals.hasName("equals") and
-    equals.getNumberOfParameters() = 2 and
-    equals.getDeclaringType().hasQualifiedName("java.util", "Objects") and
-    ma.getArgument(0) = e1 and
-    ma.getArgument(1) = e2
-  )
-  or
-  exists(ConstCase cc |
-    cc = g and
-    polarity = true and
-    cc.getSelectorExpr() = e1 and
-    cc.getValue() = e2 and
-    strictcount(cc.getValue(_)) = 1
-  )
+predicate guardControls_v1(Guards_v1::Guard guard, BasicBlock controlled, boolean branch) {
+  guard.controls(controlled, branch)
 }
diff --git a/java/ql/lib/semmle/code/java/controlflow/internal/GuardsLogic.qll b/java/ql/lib/semmle/code/java/controlflow/internal/GuardsLogic.qll
deleted file mode 100644
index 4cb3bc74f97..00000000000
--- a/java/ql/lib/semmle/code/java/controlflow/internal/GuardsLogic.qll
+++ /dev/null
@@ -1,396 +0,0 @@
-/**
- * Provides predicates for working with the internal logic of the `Guards`
- * library.
- */
-
-import java
-import semmle.code.java.controlflow.Guards
-private import Preconditions
-private import semmle.code.java.dataflow.SSA
-private import semmle.code.java.dataflow.internal.BaseSSA
-private import semmle.code.java.dataflow.NullGuards
-private import semmle.code.java.dataflow.IntegerGuards
-
-/**
- * Holds if the assumption that `g1` has been evaluated to `b1` implies that
- * `g2` has been evaluated to `b2`, that is, the evaluation of `g2` to `b2`
- * dominates the evaluation of `g1` to `b1`.
- *
- * Restricted to BaseSSA-based reasoning.
- */
-predicate implies_v1(Guard g1, boolean b1, Guard g2, boolean b2) {
-  g1.(AndBitwiseExpr).getAnOperand() = g2 and b1 = true and b2 = true
-  or
-  g1.(OrBitwiseExpr).getAnOperand() = g2 and b1 = false and b2 = false
-  or
-  g1.(AssignAndExpr).getSource() = g2 and b1 = true and b2 = true
-  or
-  g1.(AssignOrExpr).getSource() = g2 and b1 = false and b2 = false
-  or
-  g1.(AndLogicalExpr).getAnOperand() = g2 and b1 = true and b2 = true
-  or
-  g1.(OrLogicalExpr).getAnOperand() = g2 and b1 = false and b2 = false
-  or
-  g1.(LogNotExpr).getExpr() = g2 and
-  b1 = b2.booleanNot() and
-  b1 = [true, false]
-  or
-  exists(EqualityTest eqtest, boolean polarity, BooleanLiteral boollit |
-    eqtest = g1 and
-    eqtest.hasOperands(g2, boollit) and
-    eqtest.polarity() = polarity and
-    b1 = [true, false] and
-    b2 = b1.booleanXor(polarity).booleanXor(boollit.getBooleanValue())
-  )
-  or
-  exists(ConditionalExpr cond, boolean branch, BooleanLiteral boollit, boolean boolval |
-    cond.getBranchExpr(branch) = boollit and
-    cond = g1 and
-    boolval = boollit.getBooleanValue() and
-    b1 = boolval.booleanNot() and
-    (
-      g2 = cond.getCondition() and b2 = branch.booleanNot()
-      or
-      g2 = cond.getABranchExpr() and b2 = b1
-    )
-  )
-  or
-  g1.(DefaultCase).getSwitch().getAConstCase() = g2 and b1 = true and b2 = false
-  or
-  g1.(DefaultCase).getSwitchExpr().getAConstCase() = g2 and b1 = true and b2 = false
-  or
-  exists(MethodCall check, int argIndex | check = g1 |
-    conditionCheckArgument(check, argIndex, _) and
-    g2 = check.getArgument(argIndex) and
-    b1 = [true, false] and
-    b2 = b1
-  )
-  or
-  exists(BaseSsaUpdate vbool |
-    vbool.getDefiningExpr().(VariableAssign).getSource() = g2 or
-    vbool.getDefiningExpr().(AssignOp) = g2
-  |
-    vbool.getAUse() = g1 and
-    b1 = [true, false] and
-    b2 = b1
-  )
-  or
-  g1.(AssignExpr).getSource() = g2 and b2 = b1 and b1 = [true, false]
-}
-
-/**
- * Holds if the assumption that `g1` has been evaluated to `b1` implies that
- * `g2` has been evaluated to `b2`, that is, the evaluation of `g2` to `b2`
- * dominates the evaluation of `g1` to `b1`.
- *
- * Allows full use of SSA but is restricted to pre-RangeAnalysis reasoning.
- */
-predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) {
-  implies_v1(g1, b1, g2, b2)
-  or
-  exists(SsaExplicitUpdate vbool |
-    vbool.getDefiningExpr().(VariableAssign).getSource() = g2 or
-    vbool.getDefiningExpr().(AssignOp) = g2
-  |
-    vbool.getAUse() = g1 and
-    b1 = [true, false] and
-    b2 = b1
-  )
-  or
-  exists(SsaVariable v, AbstractValue k |
-    // If `v = g2 ? k : ...` or `v = g2 ? ... : k` then a guard
-    // proving `v != k` ensures that `g2` evaluates to `b2`.
-    conditionalAssignVal(v, g2, b2.booleanNot(), k) and
-    guardImpliesNotEqual1(g1, b1, v, k)
-  )
-  or
-  exists(SsaVariable v, Expr e, AbstractValue k |
-    // If `v = g2 ? k : ...` and all other assignments to `v` are different from
-    // `k` then a guard proving `v == k` ensures that `g2` evaluates to `b2`.
-    uniqueValue(v, e, k) and
-    guardImpliesEqual(g1, b1, v, k) and
-    g2.directlyControls(e.getBasicBlock(), b2) and
-    not g2.directlyControls(g1.getBasicBlock(), b2)
-  )
-}
-
-/**
- * Holds if the assumption that `g1` has been evaluated to `b1` implies that
- * `g2` has been evaluated to `b2`, that is, the evaluation of `g2` to `b2`
- * dominates the evaluation of `g1` to `b1`.
- */
-cached
-predicate implies_v3(Guard g1, boolean b1, Guard g2, boolean b2) {
-  implies_v2(g1, b1, g2, b2)
-  or
-  exists(SsaVariable v, AbstractValue k |
-    // If `v = g2 ? k : ...` or `v = g2 ? ... : k` then a guard
-    // proving `v != k` ensures that `g2` evaluates to `b2`.
-    conditionalAssignVal(v, g2, b2.booleanNot(), k) and
-    guardImpliesNotEqual2(g1, b1, v, k)
-  )
-  or
-  exists(SsaVariable v |
-    conditionalAssign(v, g2, b2.booleanNot(), clearlyNotNullExpr()) and
-    guardImpliesEqual(g1, b1, v, TAbsValNull())
-  )
-}
-
-private newtype TAbstractValue =
-  TAbsValNull() or
-  TAbsValInt(int i) { exists(CompileTimeConstantExpr c | c.getIntValue() = i) } or
-  TAbsValChar(string c) { exists(CharacterLiteral lit | lit.getValue() = c) } or
-  TAbsValString(string s) { exists(StringLiteral lit | lit.getValue() = s) } or
-  TAbsValEnum(EnumConstant c)
-
-/** The value of a constant expression. */
-abstract private class AbstractValue extends TAbstractValue {
-  abstract string toString();
-
-  /** Gets an expression whose value is this abstract value. */
-  abstract Expr getExpr();
-}
-
-private class AbsValNull extends AbstractValue, TAbsValNull {
-  override string toString() { result = "null" }
-
-  override Expr getExpr() { result = alwaysNullExpr() }
-}
-
-private class AbsValInt extends AbstractValue, TAbsValInt {
-  int i;
-
-  AbsValInt() { this = TAbsValInt(i) }
-
-  override string toString() { result = i.toString() }
-
-  override Expr getExpr() { result.(CompileTimeConstantExpr).getIntValue() = i }
-}
-
-private class AbsValChar extends AbstractValue, TAbsValChar {
-  string c;
-
-  AbsValChar() { this = TAbsValChar(c) }
-
-  override string toString() { result = c }
-
-  override Expr getExpr() { result.(CharacterLiteral).getValue() = c }
-}
-
-private class AbsValString extends AbstractValue, TAbsValString {
-  string s;
-
-  AbsValString() { this = TAbsValString(s) }
-
-  override string toString() { result = s }
-
-  override Expr getExpr() { result.(CompileTimeConstantExpr).getStringValue() = s }
-}
-
-private class AbsValEnum extends AbstractValue, TAbsValEnum {
-  EnumConstant c;
-
-  AbsValEnum() { this = TAbsValEnum(c) }
-
-  override string toString() { result = c.toString() }
-
-  override Expr getExpr() { result = c.getAnAccess() }
-}
-
-/**
- * Holds if `v` can have a value that is not representable as an `AbstractValue`.
- */
-private predicate hasPossibleUnknownValue(SsaVariable v) {
-  exists(SsaVariable def | v.getAnUltimateDefinition() = def |
-    def instanceof SsaImplicitUpdate
-    or
-    def instanceof SsaImplicitInit
-    or
-    exists(VariableUpdate upd | upd = def.(SsaExplicitUpdate).getDefiningExpr() |
-      not exists(upd.(VariableAssign).getSource())
-    )
-    or
-    exists(VariableAssign a, Expr e |
-      a = def.(SsaExplicitUpdate).getDefiningExpr() and
-      e = possibleValue(a.getSource()) and
-      not exists(AbstractValue val | val.getExpr() = e)
-    )
-  )
-}
-
-/**
- * Gets a sub-expression of `e` whose value can flow to `e` through
- * `ConditionalExpr`s.
- */
-private Expr possibleValue(Expr e) {
-  result = possibleValue(e.(ConditionalExpr).getABranchExpr())
-  or
-  result = e and not e instanceof ConditionalExpr
-}
-
-/**
- * Gets an ultimate definition of `v` that is not itself a phi node. The
- * boolean `fromBackEdge` indicates whether the flow from `result` to `v` goes
- * through a back edge.
- */
-SsaVariable getADefinition(SsaVariable v, boolean fromBackEdge) {
-  result = v and not v instanceof SsaPhiNode and fromBackEdge = false
-  or
-  exists(SsaVariable inp, BasicBlock bb, boolean fbe |
-    v.(SsaPhiNode).hasInputFromBlock(inp, bb) and
-    result = getADefinition(inp, fbe) and
-    (if v.getBasicBlock().dominates(bb) then fromBackEdge = true else fromBackEdge = fbe)
-  )
-}
-
-/**
- * Holds if `e` equals `k` and may be assigned to `v`. The boolean
- * `fromBackEdge` indicates whether the flow from `e` to `v` goes through a
- * back edge.
- */
-private predicate possibleValue(SsaVariable v, boolean fromBackEdge, Expr e, AbstractValue k) {
-  not hasPossibleUnknownValue(v) and
-  exists(SsaExplicitUpdate def |
-    def = getADefinition(v, fromBackEdge) and
-    e = possibleValue(def.getDefiningExpr().(VariableAssign).getSource()) and
-    k.getExpr() = e
-  )
-}
-
-/**
- * Holds if `e` equals `k` and may be assigned to `v` without going through
- * back edges, and all other possible ultimate definitions of `v` are different
- * from `k`. The trivial case where `v` is an `SsaExplicitUpdate` with `e` as
- * the only possible value is excluded.
- */
-private predicate uniqueValue(SsaVariable v, Expr e, AbstractValue k) {
-  possibleValue(v, false, e, k) and
-  forex(Expr other, AbstractValue otherval | possibleValue(v, _, other, otherval) and other != e |
-    otherval != k
-  )
-}
-
-/**
- * Holds if `v1` and `v2` have the same value in `bb`.
- */
-private predicate equalVarsInBlock(BasicBlock bb, SsaVariable v1, SsaVariable v2) {
-  exists(Guard guard, boolean branch |
-    guard.isEquality(v1.getAUse(), v2.getAUse(), branch) and
-    guardControls_v1(guard, bb, branch)
-  )
-}
-
-/**
- * Holds if `guard` evaluating to `branch` implies that `v` equals `k`.
- */
-private predicate guardImpliesEqual(Guard guard, boolean branch, SsaVariable v, AbstractValue k) {
-  exists(SsaVariable v0 |
-    guard.isEquality(v0.getAUse(), k.getExpr(), branch) and
-    (v = v0 or equalVarsInBlock(guard.getBasicBlock(), v0, v))
-  )
-}
-
-private BasicBlock getAGuardBranchSuccessor(Guard g, boolean branch) {
-  result.getFirstNode() = g.(Expr).getControlFlowNode().(ConditionNode).getABranchSuccessor(branch)
-  or
-  result.getFirstNode() = g.(SwitchCase).getControlFlowNode() and branch = true
-}
-
-/**
- * Holds if `guard` dominates `phi` and `guard` evaluating to `branch` controls the definition
- * `upd = e` where `upd` is a possible input to `phi`.
- */
-private predicate guardControlsPhiBranch(
-  SsaExplicitUpdate upd, SsaPhiNode phi, Guard guard, boolean branch, Expr e
-) {
-  guard.directlyControls(upd.getBasicBlock(), branch) and
-  upd.getDefiningExpr().(VariableAssign).getSource() = e and
-  upd = phi.getAPhiInput() and
-  guard.getBasicBlock().strictlyDominates(phi.getBasicBlock())
-}
-
-/**
- * Holds if `v` is conditionally assigned `e` under the condition that `guard` evaluates to `branch`.
- *
- * The evaluation of `guard` dominates the definition of `v` and `guard` evaluating to `branch`
- * implies that `e` is assigned to `v`. In particular, this allows us to conclude that if `v` has
- * a value different from `e` then `guard` must have evaluated to `branch.booleanNot()`.
- */
-private predicate conditionalAssign(SsaVariable v, Guard guard, boolean branch, Expr e) {
-  exists(ConditionalExpr c |
-    v.(SsaExplicitUpdate).getDefiningExpr().(VariableAssign).getSource() = c and
-    guard = c.getCondition()
-  |
-    e = c.getBranchExpr(branch)
-  )
-  or
-  exists(SsaExplicitUpdate upd, SsaPhiNode phi |
-    phi = v and
-    guardControlsPhiBranch(upd, phi, guard, branch, e) and
-    not guard.directlyControls(phi.getBasicBlock(), branch) and
-    forall(SsaVariable other | other != upd and other = phi.getAPhiInput() |
-      guard.directlyControls(other.getBasicBlock(), branch.booleanNot())
-      or
-      other.getBasicBlock().dominates(guard.getBasicBlock()) and
-      not other.isLiveAtEndOfBlock(getAGuardBranchSuccessor(guard, branch))
-    )
-  )
-}
-
-/**
- * Holds if `v` is conditionally assigned `val` under the condition that `guard` evaluates to `branch`.
- */
-private predicate conditionalAssignVal(SsaVariable v, Guard guard, boolean branch, AbstractValue val) {
-  conditionalAssign(v, guard, branch, val.getExpr())
-}
-
-private predicate relevantEq(SsaVariable v, AbstractValue val) {
-  conditionalAssignVal(v, _, _, val)
-  or
-  exists(SsaVariable v0 |
-    conditionalAssignVal(v0, _, _, val) and
-    equalVarsInBlock(_, v0, v)
-  )
-}
-
-/**
- * Holds if the evaluation of `guard` to `branch` implies that `v` does not have the value `val`.
- */
-private predicate guardImpliesNotEqual1(
-  Guard guard, boolean branch, SsaVariable v, AbstractValue val
-) {
-  exists(SsaVariable v0 |
-    relevantEq(v0, val) and
-    (
-      guard.isEquality(v0.getAUse(), val.getExpr(), branch.booleanNot())
-      or
-      exists(AbstractValue val2 |
-        guard.isEquality(v0.getAUse(), val2.getExpr(), branch) and
-        val != val2
-      )
-      or
-      guard.(InstanceOfExpr).getExpr() = sameValue(v0, _) and branch = true and val = TAbsValNull()
-    ) and
-    (v = v0 or equalVarsInBlock(guard.getBasicBlock(), v0, v))
-  )
-}
-
-/**
- * Holds if the evaluation of `guard` to `branch` implies that `v` does not have the value `val`.
- */
-private predicate guardImpliesNotEqual2(
-  Guard guard, boolean branch, SsaVariable v, AbstractValue val
-) {
-  exists(SsaVariable v0 |
-    relevantEq(v0, val) and
-    (
-      guard = directNullGuard(v0, branch, false) and val = TAbsValNull()
-      or
-      exists(int k |
-        guard = integerGuard(v0.getAUse(), branch, k, false) and
-        val = TAbsValInt(k)
-      )
-    ) and
-    (v = v0 or equalVarsInBlock(guard.getBasicBlock(), v0, v))
-  )
-}
diff --git a/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll b/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll
index 5fde238a4b6..d28a2e0e30c 100644
--- a/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll
@@ -4,7 +4,7 @@
 
 import java
 import SSA
-private import semmle.code.java.controlflow.internal.GuardsLogic
+private import semmle.code.java.controlflow.Guards
 private import semmle.code.java.frameworks.apache.Collections
 private import IntegerGuards
 
@@ -40,6 +40,7 @@ EqualityTest varEqualityTestExpr(SsaVariable v1, SsaVariable v2, boolean isEqual
   isEqualExpr = result.polarity()
 }
 
+/** Gets an expression that is provably not `null`. */
 Expr baseNotNullExpr() {
   result instanceof ClassInstanceExpr
   or
@@ -183,50 +184,19 @@ predicate nullCheckMethod(Method m, boolean branch, boolean isnull) {
  * is true, and non-null if `isnull` is false.
  */
 Expr basicNullGuard(Expr e, boolean branch, boolean isnull) {
-  exists(EqualityTest eqtest, boolean polarity |
-    eqtest = result and
-    eqtest.hasOperands(e, any(NullLiteral n)) and
-    polarity = eqtest.polarity() and
-    (
-      branch = true and isnull = polarity
-      or
-      branch = false and isnull = polarity.booleanNot()
-    )
-  )
-  or
-  result.(InstanceOfExpr).getExpr() = e and branch = true and isnull = false
-  or
-  exists(MethodCall call |
-    call = result and
-    call.getAnArgument() = e and
-    nullCheckMethod(call.getMethod(), branch, isnull)
-  )
-  or
-  exists(EqualityTest eqtest |
-    eqtest = result and
-    eqtest.hasOperands(e, clearlyNotNullExpr()) and
-    isnull = false and
-    branch = eqtest.polarity()
-  )
-  or
-  result = enumConstEquality(e, branch, _) and isnull = false
+  Guards_v3::nullGuard(result, any(GuardValue v | v.asBooleanValue() = branch), e, isnull)
 }
 
 /**
+ * DEPRECATED: Use `basicNullGuard` instead.
+ *
  * Gets an expression that directly tests whether a given expression, `e`, is null or not.
  *
  * If `result` evaluates to `branch`, then `e` is guaranteed to be null if `isnull`
  * is true, and non-null if `isnull` is false.
  */
-Expr basicOrCustomNullGuard(Expr e, boolean branch, boolean isnull) {
+deprecated Expr basicOrCustomNullGuard(Expr e, boolean branch, boolean isnull) {
   result = basicNullGuard(e, branch, isnull)
-  or
-  exists(MethodCall call, Method m, int ix |
-    call = result and
-    call.getArgument(ix) = e and
-    call.getMethod().getSourceDeclaration() = m and
-    m = customNullGuard(ix, branch, isnull)
-  )
 }
 
 /**
@@ -236,72 +206,42 @@ Expr basicOrCustomNullGuard(Expr e, boolean branch, boolean isnull) {
  * is true, and non-null if `isnull` is false.
  */
 Expr directNullGuard(SsaVariable v, boolean branch, boolean isnull) {
-  result = basicOrCustomNullGuard(sameValue(v, _), branch, isnull)
+  result = basicNullGuard(sameValue(v, _), branch, isnull)
 }
 
 /**
+ * DEPRECATED: Use `nullGuardControls`/`nullGuardControlsBranchEdge` instead.
+ *
  * Gets a `Guard` that tests (possibly indirectly) whether a given SSA variable is null or not.
  *
  * If `result` evaluates to `branch`, then `v` is guaranteed to be null if `isnull`
  * is true, and non-null if `isnull` is false.
  */
-Guard nullGuard(SsaVariable v, boolean branch, boolean isnull) {
-  result = directNullGuard(v, branch, isnull) or
-  exists(boolean branch0 | implies_v3(result, branch, nullGuard(v, branch0, isnull), branch0))
+deprecated Guard nullGuard(SsaVariable v, boolean branch, boolean isnull) {
+  result = directNullGuard(v, branch, isnull)
 }
 
 /**
- * A return statement in a non-overridable method that on a return value of
- * `retval` allows the conclusion that the parameter `p` either is null or
- * non-null as specified by `isnull`.
+ * Holds if there exists a null check on `v`, such that taking the branch edge
+ * from `bb1` to `bb2` implies that `v` is guaranteed to be null if `isnull` is
+ * true, and non-null if `isnull` is false.
  */
-private predicate validReturnInCustomNullGuard(
-  ReturnStmt ret, Parameter p, boolean retval, boolean isnull
-) {
-  exists(Method m |
-    ret.getEnclosingCallable() = m and
-    p.getCallable() = m and
-    m.getReturnType().(PrimitiveType).hasName("boolean") and
-    not p.isVarargs() and
-    p.getType() instanceof RefType and
-    not m.isOverridable()
-  ) and
-  exists(SsaImplicitInit ssa | ssa.isParameterDefinition(p) |
-    nullGuardedReturn(ret, ssa, isnull) and
-    (retval = true or retval = false)
-    or
-    exists(Expr res | res = ret.getResult() | res = nullGuard(ssa, retval, isnull))
+predicate nullGuardControlsBranchEdge(SsaVariable v, boolean isnull, BasicBlock bb1, BasicBlock bb2) {
+  exists(GuardValue gv |
+    Guards_v3::ssaControlsBranchEdge(v, bb1, bb2, gv) and
+    gv.isNullness(isnull)
   )
 }
 
-private predicate nullGuardedReturn(ReturnStmt ret, SsaImplicitInit ssa, boolean isnull) {
-  exists(boolean branch |
-    nullGuard(ssa, branch, isnull).directlyControls(ret.getBasicBlock(), branch)
-  )
-}
-
-pragma[nomagic]
-private Method returnStmtGetEnclosingCallable(ReturnStmt ret) {
-  ret.getEnclosingCallable() = result
-}
-
 /**
- * Gets a non-overridable method with a boolean return value that performs a null-check
- * on the `index`th parameter. A return value equal to `retval` allows us to conclude
- * that the argument either is null or non-null as specified by `isnull`.
+ * Holds if there exists a null check on `v` that controls `bb`, such that in
+ * `bb` `v` is guaranteed to be null if `isnull` is true, and non-null if
+ * `isnull` is false.
  */
-private Method customNullGuard(int index, boolean retval, boolean isnull) {
-  exists(Parameter p |
-    p.getCallable() = result and
-    p.getPosition() = index and
-    forex(ReturnStmt ret |
-      returnStmtGetEnclosingCallable(ret) = result and
-      exists(Expr res | res = ret.getResult() |
-        not res.(BooleanLiteral).getBooleanValue() = retval.booleanNot()
-      )
-    |
-      validReturnInCustomNullGuard(ret, p, retval, isnull)
-    )
+predicate nullGuardControls(SsaVariable v, boolean isnull, BasicBlock bb) {
+  exists(GuardValue gv |
+    Guards_v3::ssaControls(v, bb, gv) and
+    gv.isNullness(isnull)
   )
 }
 
diff --git a/java/ql/lib/semmle/code/java/dataflow/Nullness.qll b/java/ql/lib/semmle/code/java/dataflow/Nullness.qll
index 36ad96c497f..a4b007e1b13 100644
--- a/java/ql/lib/semmle/code/java/dataflow/Nullness.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/Nullness.qll
@@ -141,9 +141,9 @@ private ControlFlowNode varDereference(SsaVariable v, VarAccess va) {
 private ControlFlowNode ensureNotNull(SsaVariable v) {
   result = varDereference(v, _)
   or
-  exists(AssertTrueMethod m | result.asCall() = m.getACheck(nullGuard(v, true, false)))
+  exists(AssertTrueMethod m | result.asCall() = m.getACheck(directNullGuard(v, true, false)))
   or
-  exists(AssertFalseMethod m | result.asCall() = m.getACheck(nullGuard(v, false, false)))
+  exists(AssertFalseMethod m | result.asCall() = m.getACheck(directNullGuard(v, false, false)))
   or
   exists(AssertNotNullMethod m | result.asCall() = m.getACheck(v.getAUse()))
   or
@@ -339,7 +339,7 @@ private predicate nullVarStep(
   not assertFail(mid, _) and
   bb = mid.getASuccessor() and
   not impossibleEdge(mid, bb) and
-  not exists(boolean branch | nullGuard(midssa, branch, false).hasBranchEdge(mid, bb, branch)) and
+  not nullGuardControlsBranchEdge(midssa, false, mid, bb) and
   not (leavingFinally(mid, bb, true) and midstoredcompletion = true) and
   if bb.getFirstNode().asStmt() = any(TryStmt try | | try.getFinally())
   then
@@ -476,6 +476,11 @@ private ConditionBlock ssaEnumConstEquality(SsaVariable v, boolean polarity, Enu
   result.getCondition() = enumConstEquality(v.getAUse(), polarity, c)
 }
 
+private predicate conditionChecksNull(ConditionBlock cond, SsaVariable v, boolean branchIsNull) {
+  nullGuardControlsBranchEdge(v, true, cond, cond.getTestSuccessor(branchIsNull)) and
+  nullGuardControlsBranchEdge(v, false, cond, cond.getTestSuccessor(branchIsNull.booleanNot()))
+}
+
 /** A pair of correlated conditions for a given NPE candidate. */
 private predicate correlatedConditions(
   SsaSourceVariable npecand, ConditionBlock cond1, ConditionBlock cond2, boolean inverted
@@ -491,10 +496,8 @@ private predicate correlatedConditions(
     )
     or
     exists(SsaVariable v, boolean branch1, boolean branch2 |
-      cond1.getCondition() = nullGuard(v, branch1, true) and
-      cond1.getCondition() = nullGuard(v, branch1.booleanNot(), false) and
-      cond2.getCondition() = nullGuard(v, branch2, true) and
-      cond2.getCondition() = nullGuard(v, branch2.booleanNot(), false) and
+      conditionChecksNull(cond1, v, branch1) and
+      conditionChecksNull(cond2, v, branch2) and
       inverted = branch1.booleanXor(branch2)
     )
     or
@@ -620,7 +623,7 @@ private Expr trackingVarGuard(
   SsaVariable trackssa, SsaSourceVariable trackvar, TrackVarKind kind, boolean branch, boolean isA
 ) {
   exists(Expr init | trackingVar(_, trackssa, trackvar, kind, init) |
-    result = basicOrCustomNullGuard(trackvar.getAnAccess(), branch, isA) and
+    result = basicNullGuard(trackvar.getAnAccess(), branch, isA) and
     kind = TrackVarKindNull()
     or
     result = trackvar.getAnAccess() and
@@ -831,15 +834,13 @@ predicate alwaysNullDeref(SsaSourceVariable v, VarAccess va) {
       def.(SsaExplicitUpdate).getDefiningExpr().(VariableAssign).getSource() = alwaysNullExpr()
     )
     or
-    exists(boolean branch |
-      nullGuard(ssa, branch, true).directlyControls(bb, branch) and
-      not clearlyNotNull(ssa)
-    )
+    nullGuardControls(ssa, true, bb) and
+    not clearlyNotNull(ssa)
   |
     // Exclude fields as they might not have an accurate ssa representation.
     not v.getVariable() instanceof Field and
     firstVarDereferenceInBlock(bb, ssa, va) and
     ssa.getSourceVariable() = v and
-    not exists(boolean branch | nullGuard(ssa, branch, false).directlyControls(bb, branch))
+    not nullGuardControls(ssa, false, bb)
   )
 }
diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
index 64f68b9c075..4bbac387c89 100644
--- a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
@@ -66,7 +66,6 @@
 import java
 private import SSA
 private import RangeUtils
-private import semmle.code.java.controlflow.internal.GuardsLogic
 private import semmle.code.java.security.RandomDataSource
 private import SignAnalysis
 private import semmle.code.java.Reflection
@@ -79,7 +78,7 @@ module Sem implements Semantic<Location> {
   private import java as J
   private import SSA as SSA
   private import RangeUtils as RU
-  private import semmle.code.java.controlflow.internal.GuardsLogic as GL
+  private import semmle.code.java.controlflow.Guards as G
 
   class Expr = J::Expr;
 
@@ -219,7 +218,7 @@ module Sem implements Semantic<Location> {
 
   int getBlockId1(BasicBlock bb) { idOf(bb, result) }
 
-  class Guard extends GL::Guard_v2 {
+  class Guard extends G::Guards_v2::Guard {
     Expr asExpr() { result = this }
   }
 
diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll b/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll
index 444fec8f865..a9b8abf90b6 100644
--- a/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll
@@ -4,7 +4,7 @@
 
 import java
 private import SSA
-private import semmle.code.java.controlflow.internal.GuardsLogic
+private import semmle.code.java.controlflow.Guards
 private import semmle.code.java.Constants
 private import semmle.code.java.dataflow.RangeAnalysis
 private import codeql.rangeanalysis.internal.RangeUtils
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll
index 7778f6ebc35..0a4e6c8d062 100644
--- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll
@@ -60,8 +60,6 @@ module SsaFlow {
 
 cached
 private module Cached {
-  private import semmle.code.java.controlflow.internal.GuardsLogic as GuardsLogic
-
   cached
   newtype TNode =
     TExprNode(Expr e) {
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll
index b639947793b..8aebfc67286 100644
--- a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll
@@ -14,7 +14,7 @@ module Private {
 
   class Expr = J::Expr;
 
-  class Guard = G::Guard_v2;
+  class Guard = G::Guards_v2::Guard;
 
   class ConstantIntegerExpr = RU::ConstantIntegerExpr;
 
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll
index 04e896b2601..72dd345d69e 100644
--- a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll
@@ -12,7 +12,7 @@ module Private {
 
   class ConstantIntegerExpr = RU::ConstantIntegerExpr;
 
-  class Guard = G::Guard_v2;
+  class Guard = G::Guards_v2::Guard;
 
   class SsaVariable = Ssa::SsaVariable;
 
diff --git a/java/ql/lib/semmle/code/java/security/ArithmeticCommon.qll b/java/ql/lib/semmle/code/java/security/ArithmeticCommon.qll
index 785dce3da7e..2628ae7ba4d 100644
--- a/java/ql/lib/semmle/code/java/security/ArithmeticCommon.qll
+++ b/java/ql/lib/semmle/code/java/security/ArithmeticCommon.qll
@@ -7,7 +7,6 @@ private import semmle.code.java.dataflow.DataFlow
 private import semmle.code.java.dataflow.RangeAnalysis
 private import semmle.code.java.dataflow.RangeUtils
 private import semmle.code.java.dataflow.SignAnalysis
-private import semmle.code.java.controlflow.internal.GuardsLogic
 
 /**
  * Holds if the type of `exp` is narrower than or equal to `numType`,
diff --git a/java/ql/src/Language Abuse/UselessNullCheck.ql b/java/ql/src/Language Abuse/UselessNullCheck.ql
index d95b528c4c4..92041ca9e4a 100644
--- a/java/ql/src/Language Abuse/UselessNullCheck.ql	
+++ b/java/ql/src/Language Abuse/UselessNullCheck.ql	
@@ -21,7 +21,7 @@ where
   guardSuggestsExprMaybeNull(guard, e) and
   e = clearlyNotNullExpr(reason) and
   (
-    if reason instanceof Guard
+    if reason = directNullGuard(_, _, _)
     then msg = "This check is useless. $@ cannot be null at this check, since it is guarded by $@."
     else
       if reason != e
diff --git a/java/ql/test/library-tests/guards/Guards.java b/java/ql/test/library-tests/guards/Guards.java
index 877c1827166..b75e549d166 100644
--- a/java/ql/test/library-tests/guards/Guards.java
+++ b/java/ql/test/library-tests/guards/Guards.java
@@ -26,7 +26,7 @@ public class Guards {
     }
     int sz = a != null ? a.length : 0;
     for (int i = 0; i < sz; i++) {
-      chk(); // $ guarded='a != null:true' guarded='i < sz:true'
+      chk(); // $ guarded='a != null:true' guarded='i < sz:true' guarded='sz:not 0' guarded='...?...:...:not 0' guarded='a.length:not 0' guarded='a:not null'
       int e = a[i];
       if (e > 2) break;
     }
@@ -36,26 +36,26 @@ public class Guards {
       s = "bar";
     switch (s) {
       case "bar":
-        chk(); // $ guarded='s:match "bar"'
+        chk(); // $ guarded='s:match "bar"' guarded='s:bar'
         break;
       case "foo":
-        chk(); // $ guarded='s:match "foo"' guarded=g(3):false
+        chk(); // $ guarded='s:match "foo"' guarded='s:foo' guarded=g(3):false
         break;
       default:
-        chk(); // $ guarded='s:non-match "bar"' guarded='s:non-match "foo"' guarded='s:match default' guarded=g(3):false
+        chk(); // $ guarded='s:non-match "bar"' guarded='s:non-match "foo"' guarded='s:not bar' guarded='s:not foo' guarded='s:match default' guarded=g(3):false
         break;
     }
 
     Object o = g(4) ? null : s;
     if (o instanceof String) {
-      chk(); // $ guarded=...instanceof...:true guarded=g(4):false
+      chk(); // $ guarded=...instanceof...:true guarded='o:not null' guarded='...?...:...:not null' guarded=g(4):false guarded='s:not null'
     }
   }
 
   void t2() {
     checkTrue(g(1), "A");
     checkFalse(g(2), "B");
-    chk(); // $ guarded=checkTrue(A):true guarded=g(1):true guarded=checkFalse(B):false guarded=g(2):false
+    chk(); // $ guarded='checkTrue(...):no exception' guarded=g(1):true guarded='checkFalse(...):no exception' guarded=g(2):false
   }
 
   void t3() {
@@ -86,23 +86,23 @@ public class Guards {
     if (g("Alt2")) x = Val.E2;
     if (g(3)) x = Val.E3; // unique value
     if (x == null)
-      chk(); // $ guarded='x == null:true' guarded=g(3):false
+      chk(); // $ guarded='x == null:true' guarded='x:null' guarded=g(1):false guarded=g(2):false guarded=g(Alt2):false guarded=g(3):false
     switch (x) {
       case E1:
-        chk(); // $ guarded='x:match E1' guarded=g(1):true guarded=g(3):false
+        chk(); // $ guarded='x:match E1' guarded='x:E1' guarded=g(1):true guarded=g(2):false guarded=g(Alt2):false guarded=g(3):false
         break;
       case E2:
-        chk(); // $ guarded='x:match E2' guarded=g(3):false
+        chk(); // $ guarded='x:match E2' guarded='x:E2' guarded=g(3):false
         break;
       case E3:
-        chk(); // $ guarded='x:match E3' guarded=g(3):true
+        chk(); // $ guarded='x:match E3' guarded='x:E3' guarded=g(3):true
         break;
     }
     Object o = g(4) ? new Object() : null;
     if (o == null) {
-      chk(); // $ guarded='o == null:true' guarded=g(4):false
+      chk(); // $ guarded='o == null:true' guarded='o:null' guarded='...?...:...:null' guarded=g(4):false
     } else {
-      chk(); // $ guarded='o == null:false' guarded=g(4):true
+      chk(); // $ guarded='o == null:false' guarded='o:not null' guarded='...?...:...:not null' guarded=g(4):true
     }
   }
 
@@ -112,7 +112,7 @@ public class Guards {
       base = "/user";
     }
     if (base.equals("/"))
-      chk(); // $ guarded=equals(/):true guarded='base == null:false'
+      chk(); // $ guarded=equals(/):true guarded='base:/' guarded='base:not null' guarded='base == null:false' guarded='foo:/' guarded='foo:not null'
   }
 
   void t6() {
@@ -122,9 +122,9 @@ public class Guards {
       if (g(2)) { }
     }
     if (o != null) {
-      chk(); // $ guarded='o != null:true'
+      chk(); // $ guarded='o != null:true' guarded='o:not null' guarded=g(1):true
     } else {
-      chk(); // $ guarded='o != null:false' guarded=g(1):false
+      chk(); // $ guarded='o != null:false' guarded='o:null' guarded=g(1):false
     }
   }
 
diff --git a/java/ql/test/library-tests/guards/GuardsInline.expected b/java/ql/test/library-tests/guards/GuardsInline.expected
index 1aaf791acab..c45d536b7e9 100644
--- a/java/ql/test/library-tests/guards/GuardsInline.expected
+++ b/java/ql/test/library-tests/guards/GuardsInline.expected
@@ -8,19 +8,30 @@
 | Guards.java:25:7:25:11 | chk(...) | b:false |
 | Guards.java:25:7:25:11 | chk(...) | g(1):true |
 | Guards.java:25:7:25:11 | chk(...) | g(2):false |
+| Guards.java:29:7:29:11 | chk(...) | '...?...:...:not 0' |
 | Guards.java:29:7:29:11 | chk(...) | 'a != null:true' |
+| Guards.java:29:7:29:11 | chk(...) | 'a.length:not 0' |
+| Guards.java:29:7:29:11 | chk(...) | 'a:not null' |
 | Guards.java:29:7:29:11 | chk(...) | 'i < sz:true' |
+| Guards.java:29:7:29:11 | chk(...) | 'sz:not 0' |
+| Guards.java:39:9:39:13 | chk(...) | 's:bar' |
 | Guards.java:39:9:39:13 | chk(...) | 's:match "bar"' |
+| Guards.java:42:9:42:13 | chk(...) | 's:foo' |
 | Guards.java:42:9:42:13 | chk(...) | 's:match "foo"' |
 | Guards.java:42:9:42:13 | chk(...) | g(3):false |
 | Guards.java:45:9:45:13 | chk(...) | 's:match default' |
 | Guards.java:45:9:45:13 | chk(...) | 's:non-match "bar"' |
 | Guards.java:45:9:45:13 | chk(...) | 's:non-match "foo"' |
+| Guards.java:45:9:45:13 | chk(...) | 's:not bar' |
+| Guards.java:45:9:45:13 | chk(...) | 's:not foo' |
 | Guards.java:45:9:45:13 | chk(...) | g(3):false |
+| Guards.java:51:7:51:11 | chk(...) | '...?...:...:not null' |
+| Guards.java:51:7:51:11 | chk(...) | 'o:not null' |
+| Guards.java:51:7:51:11 | chk(...) | 's:not null' |
 | Guards.java:51:7:51:11 | chk(...) | ...instanceof...:true |
 | Guards.java:51:7:51:11 | chk(...) | g(4):false |
-| Guards.java:58:5:58:9 | chk(...) | checkFalse(B):false |
-| Guards.java:58:5:58:9 | chk(...) | checkTrue(A):true |
+| Guards.java:58:5:58:9 | chk(...) | 'checkFalse(...):no exception' |
+| Guards.java:58:5:58:9 | chk(...) | 'checkTrue(...):no exception' |
 | Guards.java:58:5:58:9 | chk(...) | g(1):true |
 | Guards.java:58:5:58:9 | chk(...) | g(2):false |
 | Guards.java:64:7:64:11 | chk(...) | 'g(...) && ... \|\| ...:true' |
@@ -37,22 +48,42 @@
 | Guards.java:72:7:72:11 | chk(...) | g(4):false |
 | Guards.java:72:7:72:11 | chk(...) | g(5):true |
 | Guards.java:89:7:89:11 | chk(...) | 'x == null:true' |
+| Guards.java:89:7:89:11 | chk(...) | 'x:null' |
+| Guards.java:89:7:89:11 | chk(...) | g(1):false |
+| Guards.java:89:7:89:11 | chk(...) | g(2):false |
 | Guards.java:89:7:89:11 | chk(...) | g(3):false |
+| Guards.java:89:7:89:11 | chk(...) | g(Alt2):false |
+| Guards.java:92:9:92:13 | chk(...) | 'x:E1' |
 | Guards.java:92:9:92:13 | chk(...) | 'x:match E1' |
 | Guards.java:92:9:92:13 | chk(...) | g(1):true |
+| Guards.java:92:9:92:13 | chk(...) | g(2):false |
 | Guards.java:92:9:92:13 | chk(...) | g(3):false |
+| Guards.java:92:9:92:13 | chk(...) | g(Alt2):false |
+| Guards.java:95:9:95:13 | chk(...) | 'x:E2' |
 | Guards.java:95:9:95:13 | chk(...) | 'x:match E2' |
 | Guards.java:95:9:95:13 | chk(...) | g(3):false |
+| Guards.java:98:9:98:13 | chk(...) | 'x:E3' |
 | Guards.java:98:9:98:13 | chk(...) | 'x:match E3' |
 | Guards.java:98:9:98:13 | chk(...) | g(3):true |
+| Guards.java:103:7:103:11 | chk(...) | '...?...:...:null' |
 | Guards.java:103:7:103:11 | chk(...) | 'o == null:true' |
+| Guards.java:103:7:103:11 | chk(...) | 'o:null' |
 | Guards.java:103:7:103:11 | chk(...) | g(4):false |
+| Guards.java:105:7:105:11 | chk(...) | '...?...:...:not null' |
 | Guards.java:105:7:105:11 | chk(...) | 'o == null:false' |
+| Guards.java:105:7:105:11 | chk(...) | 'o:not null' |
 | Guards.java:105:7:105:11 | chk(...) | g(4):true |
 | Guards.java:115:7:115:11 | chk(...) | 'base == null:false' |
+| Guards.java:115:7:115:11 | chk(...) | 'base:/' |
+| Guards.java:115:7:115:11 | chk(...) | 'base:not null' |
+| Guards.java:115:7:115:11 | chk(...) | 'foo:/' |
+| Guards.java:115:7:115:11 | chk(...) | 'foo:not null' |
 | Guards.java:115:7:115:11 | chk(...) | equals(/):true |
 | Guards.java:125:7:125:11 | chk(...) | 'o != null:true' |
+| Guards.java:125:7:125:11 | chk(...) | 'o:not null' |
+| Guards.java:125:7:125:11 | chk(...) | g(1):true |
 | Guards.java:127:7:127:11 | chk(...) | 'o != null:false' |
+| Guards.java:127:7:127:11 | chk(...) | 'o:null' |
 | Guards.java:127:7:127:11 | chk(...) | g(1):false |
 | Guards.java:139:9:139:13 | chk(...) | 'i < a.length:true' |
 | Guards.java:139:9:139:13 | chk(...) | found:true |
diff --git a/java/ql/test/library-tests/guards/GuardsInline.ql b/java/ql/test/library-tests/guards/GuardsInline.ql
index 54386f9777a..1b854659d87 100644
--- a/java/ql/test/library-tests/guards/GuardsInline.ql
+++ b/java/ql/test/library-tests/guards/GuardsInline.ql
@@ -39,4 +39,13 @@ query predicate guarded(MethodCall mc, string guard) {
     not exists(ppGuard(g, branch)) and
     guard = g.toString() + ":" + branch
   )
+  or
+  mc.getMethod().hasName("chk") and
+  exists(Guard g, BasicBlock bb, GuardValue val |
+    g.valueControls(bb, val) and
+    not exists(val.asBooleanValue()) and
+    mc.getBasicBlock() = bb
+  |
+    guard = "'" + g.toString() + ":" + val + "'"
+  )
 }
diff --git a/java/ql/test/library-tests/guards12/guard.expected b/java/ql/test/library-tests/guards12/guard.expected
index 0980e891d84..fade9fd4e8f 100644
--- a/java/ql/test/library-tests/guards12/guard.expected
+++ b/java/ql/test/library-tests/guards12/guard.expected
@@ -51,13 +51,5 @@ hasBranchEdge
 | Test.java:12:7:12:17 | case ... | Test.java:9:13:9:13 | s | Test.java:12:12:12:14 | "d" | true | false | Test.java:13:7:13:16 | default |
 | Test.java:12:7:12:17 | case ... | Test.java:9:13:9:13 | s | Test.java:12:12:12:14 | "d" | true | true | Test.java:12:7:12:17 | case ... |
 | Test.java:17:26:17:33 | ... == ... | Test.java:17:26:17:28 | len | Test.java:17:33:17:33 | 4 | true | true | Test.java:17:38:17:40 | { ... } |
-| Test.java:18:7:18:17 | case ... | Test.java:16:13:16:13 | s | Test.java:18:12:18:14 | "e" | true | false | Test.java:19:7:19:16 | default |
-| Test.java:18:7:18:17 | case ... | Test.java:16:13:16:13 | s | Test.java:18:12:18:14 | "e" | true | true | Test.java:18:7:18:17 | case ... |
-| Test.java:22:7:22:17 | case ... | Test.java:21:13:21:41 | ...?...:... | Test.java:22:12:22:14 | "f" | true | false | Test.java:25:7:25:16 | default |
-| Test.java:22:7:22:17 | case ... | Test.java:21:13:21:41 | ...?...:... | Test.java:22:12:22:14 | "f" | true | true | Test.java:22:7:22:17 | case ... |
 | Test.java:23:27:23:34 | ... == ... | Test.java:23:27:23:29 | len | Test.java:23:34:23:34 | 4 | true | true | Test.java:23:39:23:41 | { ... } |
-| Test.java:24:7:24:17 | case ... | Test.java:21:13:21:41 | ...?...:... | Test.java:24:12:24:14 | "g" | true | false | Test.java:25:7:25:16 | default |
-| Test.java:24:7:24:17 | case ... | Test.java:21:13:21:41 | ...?...:... | Test.java:24:12:24:14 | "g" | true | true | Test.java:24:7:24:17 | case ... |
-| Test.java:28:7:28:15 | case ... | Test.java:27:13:27:13 | s | Test.java:28:12:28:14 | "h" | true | false | Test.java:33:7:33:14 | default |
 | Test.java:28:7:28:15 | case ... | Test.java:27:13:27:13 | s | Test.java:28:12:28:14 | "h" | true | true | Test.java:28:7:28:15 | case ... |
-| Test.java:30:7:30:15 | case ... | Test.java:27:13:27:13 | s | Test.java:30:12:30:14 | "i" | true | false | Test.java:33:7:33:14 | default |
diff --git a/java/ql/test/library-tests/guards12/guard.ql b/java/ql/test/library-tests/guards12/guard.ql
index cff2845ad9f..d53dfdbc713 100644
--- a/java/ql/test/library-tests/guards12/guard.ql
+++ b/java/ql/test/library-tests/guards12/guard.ql
@@ -1,8 +1,8 @@
 import java
 import semmle.code.java.controlflow.Guards
 
-query predicate hasBranchEdge(Guard g, BasicBlock bb1, BasicBlock bb2, boolean branch) {
-  g.hasBranchEdge(bb1, bb2, branch)
+query predicate hasBranchEdge(Guard g, BasicBlock bb1, BasicBlock bb2, GuardValue branch) {
+  g.hasValueBranchEdge(bb1, bb2, branch)
 }
 
 from Guard g, BasicBlock bb, boolean branch, Expr e1, Expr e2, boolean pol
diff --git a/java/ql/test/query-tests/Nullness/C.java b/java/ql/test/query-tests/Nullness/C.java
index ac6a5f291da..317569e64c1 100644
--- a/java/ql/test/query-tests/Nullness/C.java
+++ b/java/ql/test/query-tests/Nullness/C.java
@@ -60,7 +60,7 @@ public class C {
       arrLen = arr == null ? 0 : arr.length;
     }
     if (arrLen > 0) {
-      arr[0] = 0; // NPE - false positive
+      arr[0] = 0; // OK
     }
   }
 
diff --git a/java/ql/test/query-tests/Nullness/NullMaybe.expected b/java/ql/test/query-tests/Nullness/NullMaybe.expected
index 80cf8f00f8d..a19fae57e74 100644
--- a/java/ql/test/query-tests/Nullness/NullMaybe.expected
+++ b/java/ql/test/query-tests/Nullness/NullMaybe.expected
@@ -24,7 +24,6 @@
 | C.java:10:17:10:18 | a3 | Variable $@ may be null at this access because of $@ assignment. | C.java:8:5:8:21 | long[] a3 | a3 | C.java:8:12:8:20 | a3 | this |
 | C.java:21:7:21:8 | s1 | Variable $@ may be null at this access because of $@ assignment. | C.java:14:5:14:30 | String s1 | s1 | C.java:17:7:17:24 | ...=... | this |
 | C.java:51:7:51:11 | slice | Variable $@ may be null at this access because of $@ assignment. | C.java:43:5:43:30 | List<String> slice | slice | C.java:43:18:43:29 | slice | this |
-| C.java:63:7:63:9 | arr | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:57:35:57:43 | arr | arr | C.java:60:16:60:26 | ... == ... | this |
 | C.java:100:7:100:10 | arr2 | Variable $@ may be null at this access because of $@ assignment. | C.java:95:5:95:22 | int[] arr2 | arr2 | C.java:95:11:95:21 | arr2 | this |
 | C.java:110:25:110:27 | obj | Variable $@ may be null at this access because of $@ assignment. | C.java:106:5:106:30 | Object obj | obj | C.java:118:13:118:22 | ...=... | this |
 | C.java:137:7:137:10 | obj2 | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:131:5:131:23 | Object obj2 | obj2 | C.java:132:9:132:20 | ... != ... | this |