diff --git a/java/ql/lib/semmle/code/java/controlflow/BasicBlocks.qll b/java/ql/lib/semmle/code/java/controlflow/BasicBlocks.qll
index 284ee1dad0ce..7c9e58b20ce1 100644
--- a/java/ql/lib/semmle/code/java/controlflow/BasicBlocks.qll
+++ b/java/ql/lib/semmle/code/java/controlflow/BasicBlocks.qll
@@ -85,6 +85,17 @@ class BasicBlock extends BbImpl::BasicBlock {
    */
   predicate dominates(BasicBlock bb) { super.dominates(bb) }
 
+  /**
+   * Holds if this basic block strictly dominates basic block `bb`.
+   *
+   * That is, all paths reaching `bb` from the entry point basic block must
+   * go through this basic block and this basic block is different from `bb`.
+   */
+  predicate strictlyDominates(BasicBlock bb) { super.strictlyDominates(bb) }
+
+  /** Gets an immediate successor of this basic block of a given type, if any. */
+  BasicBlock getASuccessor(Input::SuccessorType t) { result = super.getASuccessor(t) }
+
   /**
    * DEPRECATED: Use `getASuccessor` instead.
    *
diff --git a/java/ql/lib/semmle/code/java/controlflow/Guards.qll b/java/ql/lib/semmle/code/java/controlflow/Guards.qll
index 4042e7b29624..be023939b8c0 100644
--- a/java/ql/lib/semmle/code/java/controlflow/Guards.qll
+++ b/java/ql/lib/semmle/code/java/controlflow/Guards.qll
@@ -5,9 +5,9 @@
 
 import java
 private import semmle.code.java.controlflow.Dominance
-private import semmle.code.java.controlflow.internal.GuardsLogic
 private import semmle.code.java.controlflow.internal.Preconditions
 private import semmle.code.java.controlflow.internal.SwitchCases
+private import codeql.controlflow.Guards as SharedGuards
 
 /**
  * A basic block that terminates in a condition, splitting the subsequent control flow.
@@ -137,67 +137,381 @@ private predicate isNonFallThroughPredecessor(SwitchCase sc, ControlFlowNode pre
   )
 }
 
-/**
- * A condition that can be evaluated to either true or false. This can either
- * be an `Expr` of boolean type that isn't a boolean literal, or a case of a
- * switch statement, or a method access that acts as a precondition check.
- *
- * Evaluating a switch case to true corresponds to taking that switch case, and
- * evaluating it to false corresponds to taking some other branch.
- */
-final class Guard extends ExprParent {
-  Guard() {
-    this.(Expr).getType() instanceof BooleanType and not this instanceof BooleanLiteral
-    or
-    this instanceof SwitchCase
-    or
-    conditionCheckArgument(this, _, _)
+private module GuardsInput implements SharedGuards::InputSig<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())
+    }
   }
 
-  /** Gets the immediately enclosing callable whose body contains this guard. */
-  Callable getEnclosingCallable() {
-    result = this.(Expr).getEnclosingCallable() or
-    result = this.(SwitchCase).getEnclosingCallable()
+  abstract class ConstantExpr extends Expr {
+    predicate isNull() { none() }
+
+    boolean asBooleanValue() { none() }
+
+    int asIntegerValue() { none() }
+
+    ConstantValue asConstantValue() { none() }
   }
 
-  /** Gets the statement containing this guard. */
-  Stmt getEnclosingStmt() {
-    result = this.(Expr).getEnclosingStmt() or
-    result = this.(SwitchCase).getSwitch() or
-    result = this.(SwitchCase).getSwitchExpr().getEnclosingStmt()
+  private class NullConstant extends ConstantExpr instanceof J::NullLiteral {
+    override predicate isNull() { any() }
   }
 
-  /**
-   * Gets the basic block containing this guard or the basic block that tests the
-   * applicability of this switch case -- for a pattern case this is the case statement
-   * itself; for a non-pattern case this is the most recent pattern case or the top of
-   * the switch block if there is none.
-   */
-  BasicBlock getBasicBlock() {
-    // Not a switch case
-    result = this.(Expr).getBasicBlock()
-    or
-    // Return the closest pattern case statement before this one, including this one.
-    result = getClosestPrecedingPatternCase(this).getBasicBlock()
-    or
-    // Not a pattern case and no preceding pattern case -- return the top of the switch block.
-    not exists(getClosestPrecedingPatternCase(this)) and
-    result = this.(SwitchCase).getSelectorExpr().getBasicBlock()
+  private class BooleanConstant extends ConstantExpr instanceof J::BooleanLiteral {
+    override boolean asBooleanValue() { result = super.getBooleanValue() }
   }
 
-  /**
-   * Holds if this guard is an equality test between `e1` and `e2`. The test
-   * can be either `==`, `!=`, `.equals`, or a switch case. If the test is
-   * negated, that is `!=`, then `polarity` is false, otherwise `polarity` is
-   * true.
-   */
-  predicate isEquality(Expr e1, Expr e2, boolean polarity) {
-    exists(Expr exp1, Expr exp2 | equalityGuard(this, exp1, exp2, polarity) |
-      e1 = exp1 and e2 = exp2
+  private class IntegerConstant extends ConstantExpr instanceof J::CompileTimeConstantExpr {
+    override int asIntegerValue() { result = super.getIntValue() }
+  }
+
+  private class CharConstant extends ConstantExpr instanceof J::CharacterLiteral {
+    override ConstantValue asConstantValue() { result = TCharValue(super.getValue()) }
+  }
+
+  private class StringConstant extends ConstantExpr instanceof J::CompileTimeConstantExpr {
+    override ConstantValue asConstantValue() { result = TStringValue(super.getStringValue()) }
+  }
+
+  private class EnumConstantExpr extends ConstantExpr instanceof J::VarAccess {
+    override ConstantValue asConstantValue() {
+      exists(EnumConstant c | this = c.getAnAccess() and result = TEnumValue(c))
+    }
+  }
+
+  class NonNullExpr extends Expr {
+    NonNullExpr() {
+      this = NullGuards::baseNotNullExpr()
+      or
+      exists(Field f |
+        this = f.getAnAccess() and
+        f.isFinal() and
+        f.getInitializer() = NullGuards::baseNotNullExpr()
+      )
+    }
+  }
+
+  class Case extends ExprParent instanceof J::SwitchCase {
+    Expr getSwitchExpr() { result = super.getSelectorExpr() }
+
+    predicate isDefaultCase() { this instanceof DefaultCase }
+
+    ConstantExpr asConstantCase() {
+      exists(ConstCase cc | this = cc |
+        cc.getValue() = result and
+        strictcount(cc.getValue(_)) = 1
+      )
+    }
+
+    private predicate hasPatternCaseMatchEdge(BasicBlock bb1, BasicBlock bb2, boolean isMatch) {
+      exists(ConditionNode patterncase |
+        this instanceof PatternCase and
+        patterncase = super.getControlFlowNode() and
+        bb1.getLastNode() = patterncase and
+        bb2.getFirstNode() = patterncase.getABranchSuccessor(isMatch)
+      )
+    }
+
+    predicate matchEdge(BasicBlock bb1, BasicBlock bb2) {
+      exists(ControlFlowNode pred |
+        // Pattern cases are handled as ConditionBlocks.
+        not this instanceof PatternCase and
+        bb2.getFirstNode() = super.getControlFlowNode() and
+        isNonFallThroughPredecessor(this, pred) and
+        bb1 = pred.getBasicBlock()
+      )
+      or
+      this.hasPatternCaseMatchEdge(bb1, bb2, true)
+    }
+
+    predicate nonMatchEdge(BasicBlock bb1, BasicBlock bb2) {
+      this.hasPatternCaseMatchEdge(bb1, bb2, false)
+    }
+  }
+
+  abstract private class BinExpr extends Expr {
+    Expr getAnOperand() {
+      result = this.(BinaryExpr).getAnOperand() or result = this.(AssignOp).getSource()
+    }
+  }
+
+  class AndExpr extends BinExpr {
+    AndExpr() {
+      this instanceof AndBitwiseExpr or
+      this instanceof AndLogicalExpr or
+      this instanceof AssignAndExpr
+    }
+  }
+
+  class OrExpr extends BinExpr {
+    OrExpr() {
+      this instanceof OrBitwiseExpr or
+      this instanceof OrLogicalExpr or
+      this instanceof AssignOrExpr
+    }
+  }
+
+  class NotExpr extends Expr instanceof J::LogNotExpr {
+    Expr getOperand() { result = this.(J::LogNotExpr).getExpr() }
+  }
+
+  class IdExpr extends Expr {
+    IdExpr() { this instanceof AssignExpr or this instanceof CastExpr }
+
+    Expr getEqualChildExpr() {
+      result = this.(AssignExpr).getSource()
+      or
+      result = this.(CastExpr).getExpr()
+    }
+  }
+
+  private predicate objectsEquals(Method equals) {
+    equals.hasQualifiedName("java.util", "Objects", "equals") and
+    equals.getNumberOfParameters() = 2
+  }
+
+  class EqualityTest extends Expr {
+    EqualityTest() {
+      this instanceof J::EqualityTest or
+      this.(MethodCall).getMethod() instanceof EqualsMethod or
+      objectsEquals(this.(MethodCall).getMethod())
+    }
+
+    Expr getAnOperand() {
+      result = this.(J::EqualityTest).getAnOperand()
+      or
+      result = this.(MethodCall).getAnArgument()
+      or
+      this.(MethodCall).getMethod() instanceof EqualsMethod and
+      result = this.(MethodCall).getQualifier()
+    }
+
+    boolean polarity() {
+      result = this.(J::EqualityTest).polarity()
       or
-      e2 = exp1 and e1 = exp2
+      result = true and not this instanceof J::EqualityTest
+    }
+  }
+
+  class ConditionalExpr extends Expr instanceof J::ConditionalExpr {
+    Expr getCondition() { result = super.getCondition() }
+
+    Expr getThen() { result = super.getTrueExpr() }
+
+    Expr getElse() { result = super.getFalseExpr() }
+  }
+}
+
+private module GuardsImpl = SharedGuards::Make<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()
+  }
 
   /**
    * Holds if this guard tests whether `testedExpr` has type `testedType`.
@@ -231,211 +545,14 @@ final class Guard extends ExprParent {
       else restricted = false
     )
   }
-
-  /**
-   * Holds if the evaluation of this guard to `branch` corresponds to the edge
-   * from `bb1` to `bb2`.
-   */
-  predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) {
-    exists(ConditionBlock cb |
-      cb = bb1 and
-      cb.getCondition() = this and
-      bb2 = cb.getTestSuccessor(branch)
-    )
-    or
-    exists(SwitchCase sc, ControlFlowNode pred |
-      sc = this and
-      // Pattern cases are handled as ConditionBlocks above.
-      not sc instanceof PatternCase and
-      branch = true and
-      bb2.getFirstNode() = sc.getControlFlowNode() and
-      isNonFallThroughPredecessor(sc, pred) and
-      bb1 = pred.getBasicBlock()
-    )
-    or
-    preconditionBranchEdge(this, bb1, bb2, branch)
-  }
-
-  /**
-   * Holds if this guard evaluating to `branch` directly controls the block
-   * `controlled`. That is, the `true`- or `false`-successor of this guard (as
-   * given by `branch`) dominates `controlled`.
-   */
-  predicate directlyControls(BasicBlock controlled, boolean branch) {
-    exists(ConditionBlock cb |
-      cb.getCondition() = this and
-      cb.controls(controlled, branch)
-    )
-    or
-    switchCaseControls(this, controlled) and branch = true
-    or
-    preconditionControls(this, controlled, branch)
-  }
-
-  /**
-   * Holds if this guard evaluating to `branch` controls the control-flow
-   * branch edge from `bb1` to `bb2`. That is, following the edge from
-   * `bb1` to `bb2` implies that this guard evaluated to `branch`.
-   */
-  predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) {
-    guardControlsBranchEdge_v3(this, bb1, bb2, branch)
-  }
-
-  /**
-   * Holds if this guard evaluating to `branch` directly or indirectly controls
-   * the block `controlled`. That is, the evaluation of `controlled` is
-   * dominated by this guard evaluating to `branch`.
-   */
-  predicate controls(BasicBlock controlled, boolean branch) {
-    guardControls_v3(this, controlled, branch)
-  }
-}
-
-private predicate switchCaseControls(SwitchCase sc, BasicBlock bb) {
-  exists(BasicBlock caseblock |
-    // Pattern cases are handled as condition blocks
-    not sc instanceof PatternCase and
-    caseblock.getFirstNode() = sc.getControlFlowNode() and
-    caseblock.dominates(bb) and
-    // Check we can't fall through from a previous block:
-    forall(ControlFlowNode pred | pred = sc.getControlFlowNode().getAPredecessor() |
-      isNonFallThroughPredecessor(sc, pred)
-    )
-  )
-}
-
-private predicate preconditionBranchEdge(
-  MethodCall ma, BasicBlock bb1, BasicBlock bb2, boolean branch
-) {
-  conditionCheckArgument(ma, _, branch) and
-  bb1.getLastNode() = ma.getControlFlowNode() and
-  bb2.getFirstNode() = bb1.getLastNode().getANormalSuccessor()
-}
-
-private predicate preconditionControls(MethodCall ma, BasicBlock controlled, boolean branch) {
-  exists(BasicBlock check, BasicBlock succ |
-    preconditionBranchEdge(ma, check, succ, branch) and
-    dominatingEdge(check, succ) and
-    succ.dominates(controlled)
-  )
 }
 
 /**
- * INTERNAL: Use `Guards.controls` instead.
+ * INTERNAL: Use `Guard.controls` instead.
  *
  * Holds if `guard.controls(controlled, branch)`, except this only relies on
  * BaseSSA-based reasoning.
  */
-predicate guardControls_v1(Guard guard, BasicBlock controlled, boolean branch) {
-  guard.directlyControls(controlled, branch)
-  or
-  exists(Guard g, boolean b |
-    guardControls_v1(g, controlled, b) and
-    implies_v1(g, b, guard, branch)
-  )
-}
-
-/**
- * INTERNAL: Use `Guards.controls` instead.
- *
- * Holds if `guard.controls(controlled, branch)`, except this doesn't rely on
- * RangeAnalysis.
- */
-predicate guardControls_v2(Guard guard, BasicBlock controlled, boolean branch) {
-  guard.directlyControls(controlled, branch)
-  or
-  exists(Guard g, boolean b |
-    guardControls_v2(g, controlled, b) and
-    implies_v2(g, b, guard, branch)
-  )
-}
-
-pragma[nomagic]
-private predicate guardControls_v3(Guard guard, BasicBlock controlled, boolean branch) {
-  guard.directlyControls(controlled, branch)
-  or
-  exists(Guard g, boolean b |
-    guardControls_v3(g, controlled, b) and
-    implies_v3(g, b, guard, branch)
-  )
-}
-
-pragma[nomagic]
-private predicate guardControlsBranchEdge_v2(
-  Guard guard, BasicBlock bb1, BasicBlock bb2, boolean branch
-) {
-  guard.hasBranchEdge(bb1, bb2, branch)
-  or
-  exists(Guard g, boolean b |
-    guardControlsBranchEdge_v2(g, bb1, bb2, b) and
-    implies_v2(g, b, guard, branch)
-  )
-}
-
-pragma[nomagic]
-private predicate guardControlsBranchEdge_v3(
-  Guard guard, BasicBlock bb1, BasicBlock bb2, boolean branch
-) {
-  guard.hasBranchEdge(bb1, bb2, branch)
-  or
-  exists(Guard g, boolean b |
-    guardControlsBranchEdge_v3(g, bb1, bb2, b) and
-    implies_v3(g, b, guard, branch)
-  )
-}
-
-/** INTERNAL: Use `Guard` instead. */
-final class Guard_v2 extends Guard {
-  /**
-   * Holds if this guard evaluating to `branch` controls the control-flow
-   * branch edge from `bb1` to `bb2`. That is, following the edge from
-   * `bb1` to `bb2` implies that this guard evaluated to `branch`.
-   */
-  predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) {
-    guardControlsBranchEdge_v2(this, bb1, bb2, branch)
-  }
-
-  /**
-   * Holds if this guard evaluating to `branch` directly or indirectly controls
-   * the block `controlled`. That is, the evaluation of `controlled` is
-   * dominated by this guard evaluating to `branch`.
-   */
-  predicate controls(BasicBlock controlled, boolean branch) {
-    guardControls_v2(this, controlled, branch)
-  }
-}
-
-private predicate equalityGuard(Guard g, Expr e1, Expr e2, boolean polarity) {
-  exists(EqualityTest eqtest |
-    eqtest = g and
-    polarity = eqtest.polarity() and
-    eqtest.hasOperands(e1, e2)
-  )
-  or
-  exists(MethodCall ma |
-    ma = g and
-    ma.getMethod() instanceof EqualsMethod and
-    polarity = true and
-    ma.getAnArgument() = e1 and
-    ma.getQualifier() = e2
-  )
-  or
-  exists(MethodCall ma, Method equals |
-    ma = g and
-    ma.getMethod() = equals and
-    polarity = true and
-    equals.hasName("equals") and
-    equals.getNumberOfParameters() = 2 and
-    equals.getDeclaringType().hasQualifiedName("java.util", "Objects") and
-    ma.getArgument(0) = e1 and
-    ma.getArgument(1) = e2
-  )
-  or
-  exists(ConstCase cc |
-    cc = g and
-    polarity = true and
-    cc.getSelectorExpr() = e1 and
-    cc.getValue() = e2 and
-    strictcount(cc.getValue(_)) = 1
-  )
+predicate guardControls_v1(Guards_v1::Guard guard, BasicBlock controlled, boolean branch) {
+  guard.controls(controlled, branch)
 }
diff --git a/java/ql/lib/semmle/code/java/controlflow/internal/GuardsLogic.qll b/java/ql/lib/semmle/code/java/controlflow/internal/GuardsLogic.qll
deleted file mode 100644
index 4cb3bc74f97f..000000000000
--- a/java/ql/lib/semmle/code/java/controlflow/internal/GuardsLogic.qll
+++ /dev/null
@@ -1,396 +0,0 @@
-/**
- * Provides predicates for working with the internal logic of the `Guards`
- * library.
- */
-
-import java
-import semmle.code.java.controlflow.Guards
-private import Preconditions
-private import semmle.code.java.dataflow.SSA
-private import semmle.code.java.dataflow.internal.BaseSSA
-private import semmle.code.java.dataflow.NullGuards
-private import semmle.code.java.dataflow.IntegerGuards
-
-/**
- * Holds if the assumption that `g1` has been evaluated to `b1` implies that
- * `g2` has been evaluated to `b2`, that is, the evaluation of `g2` to `b2`
- * dominates the evaluation of `g1` to `b1`.
- *
- * Restricted to BaseSSA-based reasoning.
- */
-predicate implies_v1(Guard g1, boolean b1, Guard g2, boolean b2) {
-  g1.(AndBitwiseExpr).getAnOperand() = g2 and b1 = true and b2 = true
-  or
-  g1.(OrBitwiseExpr).getAnOperand() = g2 and b1 = false and b2 = false
-  or
-  g1.(AssignAndExpr).getSource() = g2 and b1 = true and b2 = true
-  or
-  g1.(AssignOrExpr).getSource() = g2 and b1 = false and b2 = false
-  or
-  g1.(AndLogicalExpr).getAnOperand() = g2 and b1 = true and b2 = true
-  or
-  g1.(OrLogicalExpr).getAnOperand() = g2 and b1 = false and b2 = false
-  or
-  g1.(LogNotExpr).getExpr() = g2 and
-  b1 = b2.booleanNot() and
-  b1 = [true, false]
-  or
-  exists(EqualityTest eqtest, boolean polarity, BooleanLiteral boollit |
-    eqtest = g1 and
-    eqtest.hasOperands(g2, boollit) and
-    eqtest.polarity() = polarity and
-    b1 = [true, false] and
-    b2 = b1.booleanXor(polarity).booleanXor(boollit.getBooleanValue())
-  )
-  or
-  exists(ConditionalExpr cond, boolean branch, BooleanLiteral boollit, boolean boolval |
-    cond.getBranchExpr(branch) = boollit and
-    cond = g1 and
-    boolval = boollit.getBooleanValue() and
-    b1 = boolval.booleanNot() and
-    (
-      g2 = cond.getCondition() and b2 = branch.booleanNot()
-      or
-      g2 = cond.getABranchExpr() and b2 = b1
-    )
-  )
-  or
-  g1.(DefaultCase).getSwitch().getAConstCase() = g2 and b1 = true and b2 = false
-  or
-  g1.(DefaultCase).getSwitchExpr().getAConstCase() = g2 and b1 = true and b2 = false
-  or
-  exists(MethodCall check, int argIndex | check = g1 |
-    conditionCheckArgument(check, argIndex, _) and
-    g2 = check.getArgument(argIndex) and
-    b1 = [true, false] and
-    b2 = b1
-  )
-  or
-  exists(BaseSsaUpdate vbool |
-    vbool.getDefiningExpr().(VariableAssign).getSource() = g2 or
-    vbool.getDefiningExpr().(AssignOp) = g2
-  |
-    vbool.getAUse() = g1 and
-    b1 = [true, false] and
-    b2 = b1
-  )
-  or
-  g1.(AssignExpr).getSource() = g2 and b2 = b1 and b1 = [true, false]
-}
-
-/**
- * Holds if the assumption that `g1` has been evaluated to `b1` implies that
- * `g2` has been evaluated to `b2`, that is, the evaluation of `g2` to `b2`
- * dominates the evaluation of `g1` to `b1`.
- *
- * Allows full use of SSA but is restricted to pre-RangeAnalysis reasoning.
- */
-predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) {
-  implies_v1(g1, b1, g2, b2)
-  or
-  exists(SsaExplicitUpdate vbool |
-    vbool.getDefiningExpr().(VariableAssign).getSource() = g2 or
-    vbool.getDefiningExpr().(AssignOp) = g2
-  |
-    vbool.getAUse() = g1 and
-    b1 = [true, false] and
-    b2 = b1
-  )
-  or
-  exists(SsaVariable v, AbstractValue k |
-    // If `v = g2 ? k : ...` or `v = g2 ? ... : k` then a guard
-    // proving `v != k` ensures that `g2` evaluates to `b2`.
-    conditionalAssignVal(v, g2, b2.booleanNot(), k) and
-    guardImpliesNotEqual1(g1, b1, v, k)
-  )
-  or
-  exists(SsaVariable v, Expr e, AbstractValue k |
-    // If `v = g2 ? k : ...` and all other assignments to `v` are different from
-    // `k` then a guard proving `v == k` ensures that `g2` evaluates to `b2`.
-    uniqueValue(v, e, k) and
-    guardImpliesEqual(g1, b1, v, k) and
-    g2.directlyControls(e.getBasicBlock(), b2) and
-    not g2.directlyControls(g1.getBasicBlock(), b2)
-  )
-}
-
-/**
- * Holds if the assumption that `g1` has been evaluated to `b1` implies that
- * `g2` has been evaluated to `b2`, that is, the evaluation of `g2` to `b2`
- * dominates the evaluation of `g1` to `b1`.
- */
-cached
-predicate implies_v3(Guard g1, boolean b1, Guard g2, boolean b2) {
-  implies_v2(g1, b1, g2, b2)
-  or
-  exists(SsaVariable v, AbstractValue k |
-    // If `v = g2 ? k : ...` or `v = g2 ? ... : k` then a guard
-    // proving `v != k` ensures that `g2` evaluates to `b2`.
-    conditionalAssignVal(v, g2, b2.booleanNot(), k) and
-    guardImpliesNotEqual2(g1, b1, v, k)
-  )
-  or
-  exists(SsaVariable v |
-    conditionalAssign(v, g2, b2.booleanNot(), clearlyNotNullExpr()) and
-    guardImpliesEqual(g1, b1, v, TAbsValNull())
-  )
-}
-
-private newtype TAbstractValue =
-  TAbsValNull() or
-  TAbsValInt(int i) { exists(CompileTimeConstantExpr c | c.getIntValue() = i) } or
-  TAbsValChar(string c) { exists(CharacterLiteral lit | lit.getValue() = c) } or
-  TAbsValString(string s) { exists(StringLiteral lit | lit.getValue() = s) } or
-  TAbsValEnum(EnumConstant c)
-
-/** The value of a constant expression. */
-abstract private class AbstractValue extends TAbstractValue {
-  abstract string toString();
-
-  /** Gets an expression whose value is this abstract value. */
-  abstract Expr getExpr();
-}
-
-private class AbsValNull extends AbstractValue, TAbsValNull {
-  override string toString() { result = "null" }
-
-  override Expr getExpr() { result = alwaysNullExpr() }
-}
-
-private class AbsValInt extends AbstractValue, TAbsValInt {
-  int i;
-
-  AbsValInt() { this = TAbsValInt(i) }
-
-  override string toString() { result = i.toString() }
-
-  override Expr getExpr() { result.(CompileTimeConstantExpr).getIntValue() = i }
-}
-
-private class AbsValChar extends AbstractValue, TAbsValChar {
-  string c;
-
-  AbsValChar() { this = TAbsValChar(c) }
-
-  override string toString() { result = c }
-
-  override Expr getExpr() { result.(CharacterLiteral).getValue() = c }
-}
-
-private class AbsValString extends AbstractValue, TAbsValString {
-  string s;
-
-  AbsValString() { this = TAbsValString(s) }
-
-  override string toString() { result = s }
-
-  override Expr getExpr() { result.(CompileTimeConstantExpr).getStringValue() = s }
-}
-
-private class AbsValEnum extends AbstractValue, TAbsValEnum {
-  EnumConstant c;
-
-  AbsValEnum() { this = TAbsValEnum(c) }
-
-  override string toString() { result = c.toString() }
-
-  override Expr getExpr() { result = c.getAnAccess() }
-}
-
-/**
- * Holds if `v` can have a value that is not representable as an `AbstractValue`.
- */
-private predicate hasPossibleUnknownValue(SsaVariable v) {
-  exists(SsaVariable def | v.getAnUltimateDefinition() = def |
-    def instanceof SsaImplicitUpdate
-    or
-    def instanceof SsaImplicitInit
-    or
-    exists(VariableUpdate upd | upd = def.(SsaExplicitUpdate).getDefiningExpr() |
-      not exists(upd.(VariableAssign).getSource())
-    )
-    or
-    exists(VariableAssign a, Expr e |
-      a = def.(SsaExplicitUpdate).getDefiningExpr() and
-      e = possibleValue(a.getSource()) and
-      not exists(AbstractValue val | val.getExpr() = e)
-    )
-  )
-}
-
-/**
- * Gets a sub-expression of `e` whose value can flow to `e` through
- * `ConditionalExpr`s.
- */
-private Expr possibleValue(Expr e) {
-  result = possibleValue(e.(ConditionalExpr).getABranchExpr())
-  or
-  result = e and not e instanceof ConditionalExpr
-}
-
-/**
- * Gets an ultimate definition of `v` that is not itself a phi node. The
- * boolean `fromBackEdge` indicates whether the flow from `result` to `v` goes
- * through a back edge.
- */
-SsaVariable getADefinition(SsaVariable v, boolean fromBackEdge) {
-  result = v and not v instanceof SsaPhiNode and fromBackEdge = false
-  or
-  exists(SsaVariable inp, BasicBlock bb, boolean fbe |
-    v.(SsaPhiNode).hasInputFromBlock(inp, bb) and
-    result = getADefinition(inp, fbe) and
-    (if v.getBasicBlock().dominates(bb) then fromBackEdge = true else fromBackEdge = fbe)
-  )
-}
-
-/**
- * Holds if `e` equals `k` and may be assigned to `v`. The boolean
- * `fromBackEdge` indicates whether the flow from `e` to `v` goes through a
- * back edge.
- */
-private predicate possibleValue(SsaVariable v, boolean fromBackEdge, Expr e, AbstractValue k) {
-  not hasPossibleUnknownValue(v) and
-  exists(SsaExplicitUpdate def |
-    def = getADefinition(v, fromBackEdge) and
-    e = possibleValue(def.getDefiningExpr().(VariableAssign).getSource()) and
-    k.getExpr() = e
-  )
-}
-
-/**
- * Holds if `e` equals `k` and may be assigned to `v` without going through
- * back edges, and all other possible ultimate definitions of `v` are different
- * from `k`. The trivial case where `v` is an `SsaExplicitUpdate` with `e` as
- * the only possible value is excluded.
- */
-private predicate uniqueValue(SsaVariable v, Expr e, AbstractValue k) {
-  possibleValue(v, false, e, k) and
-  forex(Expr other, AbstractValue otherval | possibleValue(v, _, other, otherval) and other != e |
-    otherval != k
-  )
-}
-
-/**
- * Holds if `v1` and `v2` have the same value in `bb`.
- */
-private predicate equalVarsInBlock(BasicBlock bb, SsaVariable v1, SsaVariable v2) {
-  exists(Guard guard, boolean branch |
-    guard.isEquality(v1.getAUse(), v2.getAUse(), branch) and
-    guardControls_v1(guard, bb, branch)
-  )
-}
-
-/**
- * Holds if `guard` evaluating to `branch` implies that `v` equals `k`.
- */
-private predicate guardImpliesEqual(Guard guard, boolean branch, SsaVariable v, AbstractValue k) {
-  exists(SsaVariable v0 |
-    guard.isEquality(v0.getAUse(), k.getExpr(), branch) and
-    (v = v0 or equalVarsInBlock(guard.getBasicBlock(), v0, v))
-  )
-}
-
-private BasicBlock getAGuardBranchSuccessor(Guard g, boolean branch) {
-  result.getFirstNode() = g.(Expr).getControlFlowNode().(ConditionNode).getABranchSuccessor(branch)
-  or
-  result.getFirstNode() = g.(SwitchCase).getControlFlowNode() and branch = true
-}
-
-/**
- * Holds if `guard` dominates `phi` and `guard` evaluating to `branch` controls the definition
- * `upd = e` where `upd` is a possible input to `phi`.
- */
-private predicate guardControlsPhiBranch(
-  SsaExplicitUpdate upd, SsaPhiNode phi, Guard guard, boolean branch, Expr e
-) {
-  guard.directlyControls(upd.getBasicBlock(), branch) and
-  upd.getDefiningExpr().(VariableAssign).getSource() = e and
-  upd = phi.getAPhiInput() and
-  guard.getBasicBlock().strictlyDominates(phi.getBasicBlock())
-}
-
-/**
- * Holds if `v` is conditionally assigned `e` under the condition that `guard` evaluates to `branch`.
- *
- * The evaluation of `guard` dominates the definition of `v` and `guard` evaluating to `branch`
- * implies that `e` is assigned to `v`. In particular, this allows us to conclude that if `v` has
- * a value different from `e` then `guard` must have evaluated to `branch.booleanNot()`.
- */
-private predicate conditionalAssign(SsaVariable v, Guard guard, boolean branch, Expr e) {
-  exists(ConditionalExpr c |
-    v.(SsaExplicitUpdate).getDefiningExpr().(VariableAssign).getSource() = c and
-    guard = c.getCondition()
-  |
-    e = c.getBranchExpr(branch)
-  )
-  or
-  exists(SsaExplicitUpdate upd, SsaPhiNode phi |
-    phi = v and
-    guardControlsPhiBranch(upd, phi, guard, branch, e) and
-    not guard.directlyControls(phi.getBasicBlock(), branch) and
-    forall(SsaVariable other | other != upd and other = phi.getAPhiInput() |
-      guard.directlyControls(other.getBasicBlock(), branch.booleanNot())
-      or
-      other.getBasicBlock().dominates(guard.getBasicBlock()) and
-      not other.isLiveAtEndOfBlock(getAGuardBranchSuccessor(guard, branch))
-    )
-  )
-}
-
-/**
- * Holds if `v` is conditionally assigned `val` under the condition that `guard` evaluates to `branch`.
- */
-private predicate conditionalAssignVal(SsaVariable v, Guard guard, boolean branch, AbstractValue val) {
-  conditionalAssign(v, guard, branch, val.getExpr())
-}
-
-private predicate relevantEq(SsaVariable v, AbstractValue val) {
-  conditionalAssignVal(v, _, _, val)
-  or
-  exists(SsaVariable v0 |
-    conditionalAssignVal(v0, _, _, val) and
-    equalVarsInBlock(_, v0, v)
-  )
-}
-
-/**
- * Holds if the evaluation of `guard` to `branch` implies that `v` does not have the value `val`.
- */
-private predicate guardImpliesNotEqual1(
-  Guard guard, boolean branch, SsaVariable v, AbstractValue val
-) {
-  exists(SsaVariable v0 |
-    relevantEq(v0, val) and
-    (
-      guard.isEquality(v0.getAUse(), val.getExpr(), branch.booleanNot())
-      or
-      exists(AbstractValue val2 |
-        guard.isEquality(v0.getAUse(), val2.getExpr(), branch) and
-        val != val2
-      )
-      or
-      guard.(InstanceOfExpr).getExpr() = sameValue(v0, _) and branch = true and val = TAbsValNull()
-    ) and
-    (v = v0 or equalVarsInBlock(guard.getBasicBlock(), v0, v))
-  )
-}
-
-/**
- * Holds if the evaluation of `guard` to `branch` implies that `v` does not have the value `val`.
- */
-private predicate guardImpliesNotEqual2(
-  Guard guard, boolean branch, SsaVariable v, AbstractValue val
-) {
-  exists(SsaVariable v0 |
-    relevantEq(v0, val) and
-    (
-      guard = directNullGuard(v0, branch, false) and val = TAbsValNull()
-      or
-      exists(int k |
-        guard = integerGuard(v0.getAUse(), branch, k, false) and
-        val = TAbsValInt(k)
-      )
-    ) and
-    (v = v0 or equalVarsInBlock(guard.getBasicBlock(), v0, v))
-  )
-}
diff --git a/java/ql/lib/semmle/code/java/dataflow/FlowSteps.qll b/java/ql/lib/semmle/code/java/dataflow/FlowSteps.qll
index d081a6289ecd..fb491e91e097 100644
--- a/java/ql/lib/semmle/code/java/dataflow/FlowSteps.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/FlowSteps.qll
@@ -160,7 +160,7 @@ private class NumberTaintPreservingCallable extends TaintPreservingCallable {
   int argument;
 
   NumberTaintPreservingCallable() {
-    this.getDeclaringType().getAnAncestor().hasQualifiedName("java.lang", "Number") and
+    this.getDeclaringType().getASourceSupertype*().hasQualifiedName("java.lang", "Number") and
     (
       this instanceof Constructor and
       argument = 0
diff --git a/java/ql/lib/semmle/code/java/dataflow/IntegerGuards.qll b/java/ql/lib/semmle/code/java/dataflow/IntegerGuards.qll
index 58d77b649788..a91dbced456a 100644
--- a/java/ql/lib/semmle/code/java/dataflow/IntegerGuards.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/IntegerGuards.qll
@@ -32,6 +32,58 @@ class IntComparableExpr extends Expr {
   }
 }
 
+/**
+ * Holds if `comp` evaluating to `branch` ensures that `e1` is less than `e2`.
+ * When `strict` is true, `e1` is strictly less than `e2`, otherwise it is less
+ * than or equal to `e2`.
+ */
+private predicate comparison(ComparisonExpr comp, boolean branch, Expr e1, Expr e2, boolean strict) {
+  branch = true and
+  e1 = comp.getLesserOperand() and
+  e2 = comp.getGreaterOperand() and
+  (if comp.isStrict() then strict = true else strict = false)
+  or
+  branch = false and
+  e1 = comp.getGreaterOperand() and
+  e2 = comp.getLesserOperand() and
+  (if comp.isStrict() then strict = false else strict = true)
+}
+
+/**
+ * Holds if `guard` evaluating to `branch` ensures that:
+ * `e <= k` when `upper = true`
+ * `e >= k` when `upper = false`
+ */
+pragma[nomagic]
+predicate rangeGuard(Expr guard, boolean branch, Expr e, int k, boolean upper) {
+  exists(EqualityTest eqtest, Expr c |
+    eqtest = guard and
+    eqtest.hasOperands(e, c) and
+    bounded(c, any(ZeroBound zb), k, upper, _) and
+    branch = eqtest.polarity()
+  )
+  or
+  exists(Expr c, int val, boolean strict, int d |
+    bounded(c, any(ZeroBound zb), val, upper, _) and
+    (
+      upper = true and
+      comparison(guard, branch, e, c, strict) and
+      d = -1
+      or
+      upper = false and
+      comparison(guard, branch, c, e, strict) and
+      d = 1
+    ) and
+    (
+      strict = false and k = val
+      or
+      // e < c <= val ==> e <= c - 1 <= val - 1
+      // e > c >= val ==> e >= c + 1 >= val + 1
+      strict = true and k = val + d
+    )
+  )
+}
+
 /**
  * An expression that directly tests whether a given expression is equal to `k` or not.
  * The set of `k`s is restricted to those that are relevant for the expression or
@@ -53,75 +105,14 @@ Expr integerGuard(IntComparableExpr e, boolean branch, int k, boolean is_k) {
     )
   )
   or
-  exists(EqualityTest eqtest, int val, Expr c, boolean upper |
-    k = e.relevantInt() and
-    eqtest = result and
-    eqtest.hasOperands(e, c) and
-    bounded(c, any(ZeroBound zb), val, upper, _) and
-    is_k = false and
-    (
-      upper = true and val < k
-      or
-      upper = false and val > k
-    ) and
-    branch = eqtest.polarity()
-  )
-  or
-  exists(ComparisonExpr comp, Expr c, int val, boolean upper |
+  exists(int val, boolean upper |
+    rangeGuard(result, branch, e, val, upper) and
     k = e.relevantInt() and
-    comp = result and
-    comp.hasOperands(e, c) and
-    bounded(c, any(ZeroBound zb), val, upper, _) and
     is_k = false
   |
-    // k <= val <= c < e, so e != k
-    comp.getLesserOperand() = c and
-    comp.isStrict() and
-    branch = true and
-    val >= k and
-    upper = false
-    or
-    comp.getLesserOperand() = c and
-    comp.isStrict() and
-    branch = false and
-    val < k and
-    upper = true
-    or
-    comp.getLesserOperand() = c and
-    not comp.isStrict() and
-    branch = true and
-    val > k and
-    upper = false
+    upper = true and val < k // e <= val < k  ==>  e != k
     or
-    comp.getLesserOperand() = c and
-    not comp.isStrict() and
-    branch = false and
-    val <= k and
-    upper = true
-    or
-    comp.getGreaterOperand() = c and
-    comp.isStrict() and
-    branch = true and
-    val <= k and
-    upper = true
-    or
-    comp.getGreaterOperand() = c and
-    comp.isStrict() and
-    branch = false and
-    val > k and
-    upper = false
-    or
-    comp.getGreaterOperand() = c and
-    not comp.isStrict() and
-    branch = true and
-    val < k and
-    upper = true
-    or
-    comp.getGreaterOperand() = c and
-    not comp.isStrict() and
-    branch = false and
-    val >= k and
-    upper = false
+    upper = false and val > k // e >= val > k  ==>  e != k
   )
 }
 
diff --git a/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll b/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll
index 2dd72d78a2ea..d28a2e0e30cb 100644
--- a/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll
@@ -4,7 +4,7 @@
 
 import java
 import SSA
-private import semmle.code.java.controlflow.internal.GuardsLogic
+private import semmle.code.java.controlflow.Guards
 private import semmle.code.java.frameworks.apache.Collections
 private import IntegerGuards
 
@@ -41,33 +41,44 @@ EqualityTest varEqualityTestExpr(SsaVariable v1, SsaVariable v2, boolean isEqual
 }
 
 /** Gets an expression that is provably not `null`. */
-Expr clearlyNotNullExpr(Expr reason) {
-  result instanceof ClassInstanceExpr and reason = result
+Expr baseNotNullExpr() {
+  result instanceof ClassInstanceExpr
   or
-  result instanceof ArrayCreationExpr and reason = result
+  result instanceof ArrayCreationExpr
   or
-  result instanceof TypeLiteral and reason = result
+  result instanceof TypeLiteral
   or
-  result instanceof ThisAccess and reason = result
+  result instanceof ThisAccess
   or
-  result instanceof StringLiteral and reason = result
+  result instanceof StringLiteral
   or
-  result instanceof AddExpr and result.getType() instanceof TypeString and reason = result
+  result instanceof AddExpr and result.getType() instanceof TypeString
   or
   exists(Field f |
     result = f.getAnAccess() and
     (f.hasName("TRUE") or f.hasName("FALSE")) and
-    f.getDeclaringType().hasQualifiedName("java.lang", "Boolean") and
-    reason = result
+    f.getDeclaringType().hasQualifiedName("java.lang", "Boolean")
   )
   or
-  result.(CastExpr).getExpr() = clearlyNotNullExpr(reason)
+  result = any(EnumConstant c).getAnAccess()
   or
-  result.(ImplicitCastExpr).getExpr() = clearlyNotNullExpr(reason)
+  result instanceof ImplicitNotNullExpr
   or
-  result instanceof ImplicitNotNullExpr and reason = result
+  result instanceof ImplicitCoercionToUnitExpr
   or
-  result instanceof ImplicitCoercionToUnitExpr and reason = result
+  result
+      .(MethodCall)
+      .getMethod()
+      .hasQualifiedName("com.google.common.base", "Strings", "nullToEmpty")
+}
+
+/** Gets an expression that is provably not `null`. */
+Expr clearlyNotNullExpr(Expr reason) {
+  result = baseNotNullExpr() and reason = result
+  or
+  result.(CastExpr).getExpr() = clearlyNotNullExpr(reason)
+  or
+  result.(ImplicitCastExpr).getExpr() = clearlyNotNullExpr(reason)
   or
   result.(AssignExpr).getSource() = clearlyNotNullExpr(reason)
   or
@@ -83,14 +94,14 @@ Expr clearlyNotNullExpr(Expr reason) {
     guard.controls(rval.getBasicBlock(), branch) and
     reason = guard and
     rval = v.getAUse() and
-    result = rval
+    result = rval and
+    not result = baseNotNullExpr()
   )
   or
-  exists(SsaVariable v | clearlyNotNull(v, reason) and result = v.getAUse())
-  or
-  exists(Method m | m = result.(MethodCall).getMethod() and reason = result |
-    m.getDeclaringType().hasQualifiedName("com.google.common.base", "Strings") and
-    m.hasName("nullToEmpty")
+  exists(SsaVariable v |
+    clearlyNotNull(v, reason) and
+    result = v.getAUse() and
+    not result = baseNotNullExpr()
   )
 }
 
@@ -173,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)
-  )
 }
 
 /**
@@ -226,80 +206,61 @@ 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)
+/**
+ * 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.
+ */
+predicate nullGuardControls(SsaVariable v, boolean isnull, BasicBlock bb) {
+  exists(GuardValue gv |
+    Guards_v3::ssaControls(v, bb, gv) and
+    gv.isNullness(isnull)
   )
 }
 
-pragma[nomagic]
-private Method returnStmtGetEnclosingCallable(ReturnStmt ret) {
-  ret.getEnclosingCallable() = result
-}
-
 /**
- * Gets a non-overridable method with a boolean return value that performs a null-check
- * on the `index`th parameter. A return value equal to `retval` allows us to conclude
- * that the argument either is null or non-null as specified by `isnull`.
+ * Holds if `guard` is a guard expression that suggests that `e` might be null.
  */
-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 guardSuggestsExprMaybeNull(Expr guard, Expr e) {
+  guard.(EqualityTest).hasOperands(e, any(NullLiteral n))
+  or
+  exists(MethodCall call |
+    call = guard and
+    call.getAnArgument() = e and
+    nullCheckMethod(call.getMethod(), _, true)
   )
 }
 
 /**
- * `guard` is a guard expression that suggests that `v` might be null.
- *
- * This is equivalent to `guard = basicNullGuard(sameValue(v, _), _, true)`.
+ * Holds if `guard` is a guard expression that suggests that `v` might be null.
  */
 predicate guardSuggestsVarMaybeNull(Expr guard, SsaVariable v) {
-  guard = basicNullGuard(sameValue(v, _), _, true)
+  guardSuggestsExprMaybeNull(guard, sameValue(v, _))
 }
diff --git a/java/ql/lib/semmle/code/java/dataflow/Nullness.qll b/java/ql/lib/semmle/code/java/dataflow/Nullness.qll
index 786207d34865..dec79adff852 100644
--- a/java/ql/lib/semmle/code/java/dataflow/Nullness.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/Nullness.qll
@@ -141,11 +141,11 @@ private ControlFlowNode varDereference(SsaVariable v, VarAccess va) {
 private ControlFlowNode ensureNotNull(SsaVariable v) {
   result = varDereference(v, _)
   or
-  result.asStmt().(AssertStmt).getExpr() = nullGuard(v, true, false)
+  result.asStmt().(AssertStmt).getExpr() = directNullGuard(v, true, false)
   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
@@ -341,7 +341,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
@@ -478,6 +478,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
@@ -493,10 +498,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
@@ -622,7 +625,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
@@ -833,15 +836,13 @@ predicate alwaysNullDeref(SsaSourceVariable v, VarAccess va) {
       def.(SsaExplicitUpdate).getDefiningExpr().(VariableAssign).getSource() = alwaysNullExpr()
     )
     or
-    exists(boolean branch |
-      nullGuard(ssa, branch, true).directlyControls(bb, branch) and
-      not clearlyNotNull(ssa)
-    )
+    nullGuardControls(ssa, true, bb) and
+    not clearlyNotNull(ssa)
   |
     // Exclude fields as they might not have an accurate ssa representation.
     not v.getVariable() instanceof Field and
     firstVarDereferenceInBlock(bb, ssa, va) and
     ssa.getSourceVariable() = v and
-    not exists(boolean branch | nullGuard(ssa, branch, false).directlyControls(bb, branch))
+    not nullGuardControls(ssa, false, bb)
   )
 }
diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
index 64f68b9c075a..4bbac387c896 100644
--- a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
@@ -66,7 +66,6 @@
 import java
 private import SSA
 private import RangeUtils
-private import semmle.code.java.controlflow.internal.GuardsLogic
 private import semmle.code.java.security.RandomDataSource
 private import SignAnalysis
 private import semmle.code.java.Reflection
@@ -79,7 +78,7 @@ module Sem implements Semantic<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 444fec8f8659..a9b8abf90b63 100644
--- a/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll
@@ -4,7 +4,7 @@
 
 import java
 private import SSA
-private import semmle.code.java.controlflow.internal.GuardsLogic
+private import semmle.code.java.controlflow.Guards
 private import semmle.code.java.Constants
 private import semmle.code.java.dataflow.RangeAnalysis
 private import codeql.rangeanalysis.internal.RangeUtils
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll b/java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll
index 874aca871832..ec56822d5852 100644
--- a/java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll
@@ -372,5 +372,10 @@ class BaseSsaImplicitInit extends BaseSsaVariable instanceof Impl::WriteDefiniti
 /** An SSA phi node. */
 class BaseSsaPhiNode extends BaseSsaVariable instanceof Impl::PhiNode {
   /** Gets an input to the phi node defining the SSA variable. */
-  BaseSsaVariable getAPhiInput() { phiHasInputFromBlock(this, result, _) }
+  BaseSsaVariable getAPhiInput() { this.hasInputFromBlock(result, _) }
+
+  /** Holds if `inp` is an input to the phi node along the edge originating in `bb`. */
+  predicate hasInputFromBlock(BaseSsaVariable inp, BasicBlock bb) {
+    phiHasInputFromBlock(this, inp, bb)
+  }
 }
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll
index 7778f6ebc353..0a4e6c8d062a 100644
--- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll
@@ -60,8 +60,6 @@ module SsaFlow {
 
 cached
 private module Cached {
-  private import semmle.code.java.controlflow.internal.GuardsLogic as GuardsLogic
-
   cached
   newtype TNode =
     TExprNode(Expr e) {
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll
index b639947793b5..8aebfc672861 100644
--- a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll
@@ -14,7 +14,7 @@ module Private {
 
   class Expr = J::Expr;
 
-  class Guard = G::Guard_v2;
+  class Guard = G::Guards_v2::Guard;
 
   class ConstantIntegerExpr = RU::ConstantIntegerExpr;
 
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll
index 04e896b26011..72dd345d69e2 100644
--- a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll
@@ -12,7 +12,7 @@ module Private {
 
   class ConstantIntegerExpr = RU::ConstantIntegerExpr;
 
-  class Guard = G::Guard_v2;
+  class Guard = G::Guards_v2::Guard;
 
   class SsaVariable = Ssa::SsaVariable;
 
diff --git a/java/ql/lib/semmle/code/java/security/ArithmeticCommon.qll b/java/ql/lib/semmle/code/java/security/ArithmeticCommon.qll
index 785dce3da7ed..2628ae7ba4d0 100644
--- a/java/ql/lib/semmle/code/java/security/ArithmeticCommon.qll
+++ b/java/ql/lib/semmle/code/java/security/ArithmeticCommon.qll
@@ -7,7 +7,6 @@ private import semmle.code.java.dataflow.DataFlow
 private import semmle.code.java.dataflow.RangeAnalysis
 private import semmle.code.java.dataflow.RangeUtils
 private import semmle.code.java.dataflow.SignAnalysis
-private import semmle.code.java.controlflow.internal.GuardsLogic
 
 /**
  * Holds if the type of `exp` is narrower than or equal to `numType`,
diff --git a/java/ql/src/Language Abuse/UselessNullCheck.ql b/java/ql/src/Language Abuse/UselessNullCheck.ql
index 93e5a92c3070..9a9fccbd5e01 100644
--- a/java/ql/src/Language Abuse/UselessNullCheck.ql	
+++ b/java/ql/src/Language Abuse/UselessNullCheck.ql	
@@ -17,10 +17,10 @@ import semmle.code.java.controlflow.Guards
 
 from Expr guard, Expr e, Expr reason, string msg
 where
-  guard = basicNullGuard(e, _, true) and
+  guardSuggestsExprMaybeNull(guard, e) and
   e = clearlyNotNullExpr(reason) and
   (
-    if reason instanceof Guard
+    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
new file mode 100644
index 000000000000..91363176e2c0
--- /dev/null
+++ b/java/ql/test/library-tests/guards/Guards.java
@@ -0,0 +1,130 @@
+public class Guards {
+  static void chk() { }
+
+  static boolean g(Object lbl) { return lbl.hashCode() > 10; }
+
+  static void checkTrue(boolean b, String msg) {
+    if (!b) throw new Error(msg);
+  }
+
+  static void checkFalse(boolean b, String msg) {
+    checkTrue(!b, msg);
+  }
+
+  void t1(int[] a, String s) {
+    if (g("A")) {
+      chk(); // $ guarded=g(A):true
+    } else {
+      chk(); // $ guarded=g(A):false
+    }
+
+    boolean b = g(1) ? g(2) : true;
+    if (b != false) {
+      chk(); // $ guarded=...?...:...:true guarded='b != false:true' guarded=b:true
+    } else {
+      chk(); // $ guarded=...?...:...:false guarded='b != false:false' guarded=b:false guarded=g(1):true guarded=g(2):false
+    }
+    int sz = a != null ? a.length : 0;
+    for (int i = 0; i < sz; i++) {
+      chk(); // $ guarded='a != null:true' guarded='i < sz:true' guarded='sz:not 0' guarded='...?...:...:not 0' guarded='a.length:not 0' guarded='a:not null'
+      int e = a[i];
+      if (e > 2) break;
+    }
+    chk(); // nothing guards here
+
+    if (g(3))
+      s = "bar";
+    switch (s) {
+      case "bar":
+        chk(); // $ guarded='s:match "bar"' guarded='s:bar'
+        break;
+      case "foo":
+        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: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='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(...):no exception' guarded=g(1):true guarded='checkFalse(...):no exception' guarded=g(2):false
+  }
+
+  void t3() {
+    boolean b = g(1) && (g(2) || g(3));
+    if (b) {
+      chk(); // $ guarded=b:true guarded='g(...) && ... \|\| ...:true' guarded=g(1):true guarded='g(...) \|\| g(...):true'
+    } else {
+      chk(); // $ guarded=b:false guarded='g(...) && ... \|\| ...:false'
+    }
+    b = g(4) || !g(5);
+    if (b) {
+      chk(); // $ guarded=b:true guarded='g(...) \|\| !...:true'
+    } else {
+      chk(); // $ guarded=b:false guarded='g(...) \|\| !...:false' guarded=g(4):false guarded=!...:false guarded=g(5):true
+    }
+  }
+
+  enum Val {
+    E1,
+    E2,
+    E3
+  }
+
+  void t4() {
+    Val x = null; // unique value
+    if (g(1)) x = Val.E1; // unique value
+    if (g(2)) x = Val.E2;
+    if (g("Alt2")) x = Val.E2;
+    if (g(3)) x = Val.E3; // unique value
+    if (x == null)
+      chk(); // $ guarded='x == null:true' guarded='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='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='x:E2' guarded=g(3):false
+        break;
+      case E3:
+        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='o:null' guarded='...?...:...:null' guarded=g(4):false
+    } else {
+      chk(); // $ guarded='o == null:false' guarded='o:not null' guarded='...?...:...:not null' guarded=g(4):true
+    }
+  }
+
+  void t5(String foo) {
+    String base = foo;
+    if (base == null) {
+      base = "/user";
+    }
+    if (base.equals("/"))
+      chk(); // $ guarded=equals(/):true guarded='base:/' guarded='base:not null' guarded='base == null:false' guarded='foo:/' guarded='foo:not null'
+  }
+
+  void t6() {
+    Object o = null;
+    if (g(1)) {
+      o = new Object();
+      if (g(2)) { }
+    }
+    if (o != null) {
+      chk(); // $ guarded='o != null:true' guarded='o:not null' guarded=g(1):true
+    } else {
+      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
new file mode 100644
index 000000000000..71abf007eeb5
--- /dev/null
+++ b/java/ql/test/library-tests/guards/GuardsInline.expected
@@ -0,0 +1,87 @@
+| Guards.java:16:7:16:11 | chk(...) | g(A):true |
+| Guards.java:18:7:18:11 | chk(...) | g(A):false |
+| Guards.java:23:7:23:11 | chk(...) | 'b != false:true' |
+| Guards.java:23:7:23:11 | chk(...) | ...?...:...:true |
+| Guards.java:23:7:23:11 | chk(...) | b:true |
+| Guards.java:25:7:25:11 | chk(...) | 'b != false:false' |
+| Guards.java:25:7:25:11 | chk(...) | ...?...:...:false |
+| Guards.java:25:7:25:11 | chk(...) | b:false |
+| Guards.java:25:7:25:11 | chk(...) | g(1):true |
+| Guards.java:25:7:25:11 | chk(...) | g(2):false |
+| Guards.java:29:7:29:11 | chk(...) | '...?...:...: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(...):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' |
+| Guards.java:64:7:64:11 | chk(...) | 'g(...) \|\| g(...):true' |
+| Guards.java:64:7:64:11 | chk(...) | b:true |
+| Guards.java:64:7:64:11 | chk(...) | g(1):true |
+| Guards.java:66:7:66:11 | chk(...) | 'g(...) && ... \|\| ...:false' |
+| Guards.java:66:7:66:11 | chk(...) | b:false |
+| Guards.java:70:7:70:11 | chk(...) | 'g(...) \|\| !...:true' |
+| Guards.java:70:7:70:11 | chk(...) | b:true |
+| Guards.java:72:7:72:11 | chk(...) | !...:false |
+| Guards.java:72:7:72:11 | chk(...) | 'g(...) \|\| !...:false' |
+| Guards.java:72:7:72:11 | chk(...) | b:false |
+| Guards.java:72:7:72:11 | chk(...) | g(4):false |
+| Guards.java:72:7:72:11 | chk(...) | g(5):true |
+| Guards.java:89:7:89:11 | chk(...) | 'x == null:true' |
+| Guards.java:89:7:89:11 | chk(...) | '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 |
diff --git a/java/ql/test/library-tests/guards/GuardsInline.ql b/java/ql/test/library-tests/guards/GuardsInline.ql
new file mode 100644
index 000000000000..1b854659d87b
--- /dev/null
+++ b/java/ql/test/library-tests/guards/GuardsInline.ql
@@ -0,0 +1,51 @@
+import java
+import semmle.code.java.controlflow.Guards
+import codeql.util.Boolean
+
+string ppGuard(Guard g, Boolean branch) {
+  exists(MethodCall mc, Literal s |
+    mc = g and
+    mc.getAnArgument() = s and
+    result = mc.getMethod().getName() + "(" + s.getValue() + ")" + ":" + branch
+  )
+  or
+  exists(BinaryExpr bin |
+    bin = g and
+    result = "'" + bin.getLeftOperand() + bin.getOp() + bin.getRightOperand() + ":" + branch + "'"
+  )
+  or
+  exists(SwitchCase cc, Expr s, string match, string value |
+    cc = g and
+    cc.getSelectorExpr() = s and
+    (
+      cc.(ConstCase).getValue().toString() = value
+      or
+      cc instanceof DefaultCase and value = "default"
+    ) and
+    if branch = true then match = ":match " else match = ":non-match "
+  |
+    result = "'" + s.toString() + match + value + "'"
+  )
+}
+
+query predicate guarded(MethodCall mc, string guard) {
+  mc.getMethod().hasName("chk") and
+  exists(Guard g, BasicBlock bb, boolean branch |
+    g.controls(bb, branch) and
+    mc.getBasicBlock() = bb
+  |
+    guard = ppGuard(g, branch)
+    or
+    not exists(ppGuard(g, branch)) and
+    guard = g.toString() + ":" + branch
+  )
+  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/guards/GuardsInline.qlref b/java/ql/test/library-tests/guards/GuardsInline.qlref
new file mode 100644
index 000000000000..a9492ac8f238
--- /dev/null
+++ b/java/ql/test/library-tests/guards/GuardsInline.qlref
@@ -0,0 +1,2 @@
+query: GuardsInline.ql
+postprocess: utils/test/InlineExpectationsTestQuery.ql
diff --git a/java/ql/test/library-tests/guards/guardslogic.expected b/java/ql/test/library-tests/guards/guardslogic.expected
index 6536ad3b69fa..29c11ccd153d 100644
--- a/java/ql/test/library-tests/guards/guardslogic.expected
+++ b/java/ql/test/library-tests/guards/guardslogic.expected
@@ -30,33 +30,33 @@
 | Logic.java:29:16:29:19 | g(...) | false | Logic.java:30:30:31:5 | { ... } |
 | Logic.java:29:16:29:19 | g(...) | true | Logic.java:29:23:29:26 | null |
 | Logic.java:30:9:30:27 | ...instanceof... | true | Logic.java:30:30:31:5 | { ... } |
-| Logic.java:35:5:35:29 | checkTrue(...) | true | Logic.java:36:5:36:28 | <Expr>; |
-| Logic.java:35:5:35:29 | checkTrue(...) | true | Logic.java:37:5:37:15 | if (...) |
-| Logic.java:35:5:35:29 | checkTrue(...) | true | Logic.java:37:17:39:5 | { ... } |
-| Logic.java:35:5:35:29 | checkTrue(...) | true | Logic.java:40:5:40:18 | var ...; |
+| Logic.java:35:5:35:29 | checkTrue(...) | no exception | Logic.java:36:5:36:28 | <Expr>; |
+| Logic.java:35:5:35:29 | checkTrue(...) | no exception | Logic.java:37:5:37:15 | if (...) |
+| Logic.java:35:5:35:29 | checkTrue(...) | no exception | Logic.java:37:17:39:5 | { ... } |
+| Logic.java:35:5:35:29 | checkTrue(...) | no exception | Logic.java:40:5:40:18 | var ...; |
 | Logic.java:35:15:35:19 | ... > ... | true | Logic.java:36:5:36:28 | <Expr>; |
 | Logic.java:35:15:35:19 | ... > ... | true | Logic.java:37:5:37:15 | if (...) |
 | Logic.java:35:15:35:19 | ... > ... | true | Logic.java:37:17:39:5 | { ... } |
 | Logic.java:35:15:35:19 | ... > ... | true | Logic.java:40:5:40:18 | var ...; |
-| Logic.java:36:5:36:27 | checkFalse(...) | false | Logic.java:37:5:37:15 | if (...) |
-| Logic.java:36:5:36:27 | checkFalse(...) | false | Logic.java:37:17:39:5 | { ... } |
-| Logic.java:36:5:36:27 | checkFalse(...) | false | Logic.java:40:5:40:18 | var ...; |
+| Logic.java:36:5:36:27 | checkFalse(...) | no exception | Logic.java:37:5:37:15 | if (...) |
+| Logic.java:36:5:36:27 | checkFalse(...) | no exception | Logic.java:37:17:39:5 | { ... } |
+| Logic.java:36:5:36:27 | checkFalse(...) | no exception | Logic.java:40:5:40:18 | var ...; |
 | Logic.java:36:16:36:21 | g(...) | false | Logic.java:37:5:37:15 | if (...) |
 | Logic.java:36:16:36:21 | g(...) | false | Logic.java:37:17:39:5 | { ... } |
 | Logic.java:36:16:36:21 | g(...) | false | Logic.java:40:5:40:18 | var ...; |
 | Logic.java:37:9:37:14 | ... > ... | true | Logic.java:37:17:39:5 | { ... } |
 | Logic.java:44:10:44:10 | b | false | Logic.java:44:33:44:35 | msg |
-| Logic.java:52:5:52:29 | checkTrue(...) | true | Logic.java:53:5:53:28 | <Expr>; |
-| Logic.java:52:5:52:29 | checkTrue(...) | true | Logic.java:54:5:54:15 | if (...) |
-| Logic.java:52:5:52:29 | checkTrue(...) | true | Logic.java:54:17:56:5 | { ... } |
-| Logic.java:52:5:52:29 | checkTrue(...) | true | Logic.java:57:5:57:18 | var ...; |
+| Logic.java:52:5:52:29 | checkTrue(...) | no exception | Logic.java:53:5:53:28 | <Expr>; |
+| Logic.java:52:5:52:29 | checkTrue(...) | no exception | Logic.java:54:5:54:15 | if (...) |
+| Logic.java:52:5:52:29 | checkTrue(...) | no exception | Logic.java:54:17:56:5 | { ... } |
+| Logic.java:52:5:52:29 | checkTrue(...) | no exception | Logic.java:57:5:57:18 | var ...; |
 | Logic.java:52:24:52:28 | ... > ... | true | Logic.java:53:5:53:28 | <Expr>; |
 | Logic.java:52:24:52:28 | ... > ... | true | Logic.java:54:5:54:15 | if (...) |
 | Logic.java:52:24:52:28 | ... > ... | true | Logic.java:54:17:56:5 | { ... } |
 | Logic.java:52:24:52:28 | ... > ... | true | Logic.java:57:5:57:18 | var ...; |
-| Logic.java:53:5:53:27 | checkFalse(...) | false | Logic.java:54:5:54:15 | if (...) |
-| Logic.java:53:5:53:27 | checkFalse(...) | false | Logic.java:54:17:56:5 | { ... } |
-| Logic.java:53:5:53:27 | checkFalse(...) | false | Logic.java:57:5:57:18 | var ...; |
+| Logic.java:53:5:53:27 | checkFalse(...) | no exception | Logic.java:54:5:54:15 | if (...) |
+| Logic.java:53:5:53:27 | checkFalse(...) | no exception | Logic.java:54:17:56:5 | { ... } |
+| Logic.java:53:5:53:27 | checkFalse(...) | no exception | Logic.java:57:5:57:18 | var ...; |
 | Logic.java:53:21:53:26 | g(...) | false | Logic.java:54:5:54:15 | if (...) |
 | Logic.java:53:21:53:26 | g(...) | false | Logic.java:54:17:56:5 | { ... } |
 | Logic.java:53:21:53:26 | g(...) | false | Logic.java:57:5:57:18 | var ...; |
diff --git a/java/ql/test/library-tests/guards/guardslogic.ql b/java/ql/test/library-tests/guards/guardslogic.ql
index afbb313d6645..f2ce9fdaa365 100644
--- a/java/ql/test/library-tests/guards/guardslogic.ql
+++ b/java/ql/test/library-tests/guards/guardslogic.ql
@@ -1,8 +1,9 @@
 import java
 import semmle.code.java.controlflow.Guards
 
-from Guard g, BasicBlock bb, boolean branch
+from Guard g, BasicBlock bb, GuardValue gv
 where
-  g.controls(bb, branch) and
-  g.getEnclosingCallable().getDeclaringType().hasName("Logic")
-select g, branch, bb
+  g.valueControls(bb, gv) and
+  g.getEnclosingCallable().getDeclaringType().hasName("Logic") and
+  (exists(gv.asBooleanValue()) or gv.isThrowsException() or gv.getDualValue().isThrowsException())
+select g, gv, bb
diff --git a/java/ql/test/library-tests/guards/guardspreconditions.expected b/java/ql/test/library-tests/guards/guardspreconditions.expected
index 9c0136c8e6e9..41080a5dab6e 100644
--- a/java/ql/test/library-tests/guards/guardspreconditions.expected
+++ b/java/ql/test/library-tests/guards/guardspreconditions.expected
@@ -1,20 +1,20 @@
-| Preconditions.java:8:9:8:31 | assertTrue(...) | true | Preconditions.java:9:9:9:18 | <Expr>; |
-| Preconditions.java:13:9:13:32 | assertTrue(...) | true | Preconditions.java:14:9:14:18 | <Expr>; |
-| Preconditions.java:18:9:18:33 | assertFalse(...) | false | Preconditions.java:19:9:19:18 | <Expr>; |
-| Preconditions.java:23:9:23:32 | assertFalse(...) | false | Preconditions.java:24:9:24:18 | <Expr>; |
-| Preconditions.java:28:9:28:41 | assertTrue(...) | true | Preconditions.java:29:9:29:18 | <Expr>; |
-| Preconditions.java:33:9:33:42 | assertTrue(...) | true | Preconditions.java:34:9:34:18 | <Expr>; |
-| Preconditions.java:38:9:38:43 | assertFalse(...) | false | Preconditions.java:39:9:39:18 | <Expr>; |
-| Preconditions.java:43:9:43:42 | assertFalse(...) | false | Preconditions.java:44:9:44:18 | <Expr>; |
-| Preconditions.java:48:9:48:35 | assertTrue(...) | true | Preconditions.java:49:9:49:18 | <Expr>; |
-| Preconditions.java:53:9:53:36 | assertTrue(...) | true | Preconditions.java:54:9:54:18 | <Expr>; |
-| Preconditions.java:58:9:58:37 | assertFalse(...) | false | Preconditions.java:59:9:59:18 | <Expr>; |
-| Preconditions.java:63:9:63:36 | assertFalse(...) | false | Preconditions.java:64:9:64:18 | <Expr>; |
-| Preconditions.java:68:9:68:45 | assertTrue(...) | true | Preconditions.java:69:9:69:18 | <Expr>; |
-| Preconditions.java:73:9:73:46 | assertTrue(...) | true | Preconditions.java:74:9:74:18 | <Expr>; |
-| Preconditions.java:78:9:78:47 | assertFalse(...) | false | Preconditions.java:79:9:79:18 | <Expr>; |
-| Preconditions.java:83:9:83:46 | assertFalse(...) | false | Preconditions.java:84:9:84:18 | <Expr>; |
-| Preconditions.java:88:9:88:15 | t(...) | true | Preconditions.java:89:9:89:18 | <Expr>; |
-| Preconditions.java:93:9:93:16 | t(...) | true | Preconditions.java:94:9:94:18 | <Expr>; |
-| Preconditions.java:98:9:98:16 | f(...) | false | Preconditions.java:99:9:99:18 | <Expr>; |
-| Preconditions.java:103:9:103:15 | f(...) | false | Preconditions.java:104:9:104:18 | <Expr>; |
+| Preconditions.java:8:9:8:31 | assertTrue(...) | no exception | Preconditions.java:9:9:9:18 | <Expr>; |
+| Preconditions.java:13:9:13:32 | assertTrue(...) | no exception | Preconditions.java:14:9:14:18 | <Expr>; |
+| Preconditions.java:18:9:18:33 | assertFalse(...) | no exception | Preconditions.java:19:9:19:18 | <Expr>; |
+| Preconditions.java:23:9:23:32 | assertFalse(...) | no exception | Preconditions.java:24:9:24:18 | <Expr>; |
+| Preconditions.java:28:9:28:41 | assertTrue(...) | no exception | Preconditions.java:29:9:29:18 | <Expr>; |
+| Preconditions.java:33:9:33:42 | assertTrue(...) | no exception | Preconditions.java:34:9:34:18 | <Expr>; |
+| Preconditions.java:38:9:38:43 | assertFalse(...) | no exception | Preconditions.java:39:9:39:18 | <Expr>; |
+| Preconditions.java:43:9:43:42 | assertFalse(...) | no exception | Preconditions.java:44:9:44:18 | <Expr>; |
+| Preconditions.java:48:9:48:35 | assertTrue(...) | no exception | Preconditions.java:49:9:49:18 | <Expr>; |
+| Preconditions.java:53:9:53:36 | assertTrue(...) | no exception | Preconditions.java:54:9:54:18 | <Expr>; |
+| Preconditions.java:58:9:58:37 | assertFalse(...) | no exception | Preconditions.java:59:9:59:18 | <Expr>; |
+| Preconditions.java:63:9:63:36 | assertFalse(...) | no exception | Preconditions.java:64:9:64:18 | <Expr>; |
+| Preconditions.java:68:9:68:45 | assertTrue(...) | no exception | Preconditions.java:69:9:69:18 | <Expr>; |
+| Preconditions.java:73:9:73:46 | assertTrue(...) | no exception | Preconditions.java:74:9:74:18 | <Expr>; |
+| Preconditions.java:78:9:78:47 | assertFalse(...) | no exception | Preconditions.java:79:9:79:18 | <Expr>; |
+| Preconditions.java:83:9:83:46 | assertFalse(...) | no exception | Preconditions.java:84:9:84:18 | <Expr>; |
+| Preconditions.java:88:9:88:15 | t(...) | no exception | Preconditions.java:89:9:89:18 | <Expr>; |
+| Preconditions.java:93:9:93:16 | t(...) | no exception | Preconditions.java:94:9:94:18 | <Expr>; |
+| Preconditions.java:98:9:98:16 | f(...) | no exception | Preconditions.java:99:9:99:18 | <Expr>; |
+| Preconditions.java:103:9:103:15 | f(...) | no exception | Preconditions.java:104:9:104:18 | <Expr>; |
diff --git a/java/ql/test/library-tests/guards/guardspreconditions.ql b/java/ql/test/library-tests/guards/guardspreconditions.ql
index 12c823e9638c..77e4a4e48c08 100644
--- a/java/ql/test/library-tests/guards/guardspreconditions.ql
+++ b/java/ql/test/library-tests/guards/guardspreconditions.ql
@@ -1,8 +1,9 @@
 import java
 import semmle.code.java.controlflow.Guards
 
-from Guard g, BasicBlock bb, boolean branch
+from Guard g, BasicBlock bb, GuardValue gv
 where
-  g.controls(bb, branch) and
-  g.getEnclosingCallable().getDeclaringType().hasName("Preconditions")
-select g, branch, bb
+  g.valueControls(bb, gv) and
+  g.getEnclosingCallable().getDeclaringType().hasName("Preconditions") and
+  (gv.isThrowsException() or gv.getDualValue().isThrowsException())
+select g, gv, bb
diff --git a/java/ql/test/library-tests/guards12/guard.expected b/java/ql/test/library-tests/guards12/guard.expected
index 0980e891d84a..fade9fd4e8fc 100644
--- a/java/ql/test/library-tests/guards12/guard.expected
+++ b/java/ql/test/library-tests/guards12/guard.expected
@@ -51,13 +51,5 @@ hasBranchEdge
 | Test.java:12:7:12:17 | case ... | Test.java:9:13:9:13 | s | Test.java:12:12:12:14 | "d" | true | false | Test.java:13:7:13:16 | default |
 | Test.java:12:7:12:17 | case ... | Test.java:9:13:9:13 | s | Test.java:12:12:12:14 | "d" | true | true | Test.java:12:7:12:17 | case ... |
 | Test.java:17:26:17:33 | ... == ... | Test.java:17:26:17:28 | len | Test.java:17:33:17:33 | 4 | true | true | Test.java:17:38:17:40 | { ... } |
-| Test.java:18:7:18:17 | case ... | Test.java:16:13:16:13 | s | Test.java:18:12:18:14 | "e" | true | false | Test.java:19:7:19:16 | default |
-| Test.java:18:7:18:17 | case ... | Test.java:16:13:16:13 | s | Test.java:18:12:18:14 | "e" | true | true | Test.java:18:7:18:17 | case ... |
-| Test.java:22:7:22:17 | case ... | Test.java:21:13:21:41 | ...?...:... | Test.java:22:12:22:14 | "f" | true | false | Test.java:25:7:25:16 | default |
-| Test.java:22:7:22:17 | case ... | Test.java:21:13:21:41 | ...?...:... | Test.java:22:12:22:14 | "f" | true | true | Test.java:22:7:22:17 | case ... |
 | Test.java:23:27:23:34 | ... == ... | Test.java:23:27:23:29 | len | Test.java:23:34:23:34 | 4 | true | true | Test.java:23:39:23:41 | { ... } |
-| Test.java:24:7:24:17 | case ... | Test.java:21:13:21:41 | ...?...:... | Test.java:24:12:24:14 | "g" | true | false | Test.java:25:7:25:16 | default |
-| Test.java:24:7:24:17 | case ... | Test.java:21:13:21:41 | ...?...:... | Test.java:24:12:24:14 | "g" | true | true | Test.java:24:7:24:17 | case ... |
-| Test.java:28:7:28:15 | case ... | Test.java:27:13:27:13 | s | Test.java:28:12:28:14 | "h" | true | false | Test.java:33:7:33:14 | default |
 | Test.java:28:7:28:15 | case ... | Test.java:27:13:27:13 | s | Test.java:28:12:28:14 | "h" | true | true | Test.java:28:7:28:15 | case ... |
-| Test.java:30:7:30:15 | case ... | Test.java:27:13:27:13 | s | Test.java:30:12:30:14 | "i" | true | false | Test.java:33:7:33:14 | default |
diff --git a/java/ql/test/library-tests/guards12/guard.ql b/java/ql/test/library-tests/guards12/guard.ql
index cff2845ad9f8..d53dfdbc7135 100644
--- a/java/ql/test/library-tests/guards12/guard.ql
+++ b/java/ql/test/library-tests/guards12/guard.ql
@@ -1,8 +1,8 @@
 import java
 import semmle.code.java.controlflow.Guards
 
-query predicate hasBranchEdge(Guard g, BasicBlock bb1, BasicBlock bb2, boolean branch) {
-  g.hasBranchEdge(bb1, bb2, branch)
+query predicate hasBranchEdge(Guard g, BasicBlock bb1, BasicBlock bb2, GuardValue branch) {
+  g.hasValueBranchEdge(bb1, bb2, branch)
 }
 
 from Guard g, BasicBlock bb, boolean branch, Expr e1, Expr e2, boolean pol
diff --git a/java/ql/test/query-tests/Nullness/C.java b/java/ql/test/query-tests/Nullness/C.java
index ac6a5f291da2..317569e64c1d 100644
--- a/java/ql/test/query-tests/Nullness/C.java
+++ b/java/ql/test/query-tests/Nullness/C.java
@@ -60,7 +60,7 @@ public void ex5(boolean hasArr, int[] arr) {
       arrLen = arr == null ? 0 : arr.length;
     }
     if (arrLen > 0) {
-      arr[0] = 0; // NPE - false positive
+      arr[0] = 0; // OK
     }
   }
 
diff --git a/java/ql/test/query-tests/Nullness/NullMaybe.expected b/java/ql/test/query-tests/Nullness/NullMaybe.expected
index 80cf8f00f8d5..a19fae57e74e 100644
--- a/java/ql/test/query-tests/Nullness/NullMaybe.expected
+++ b/java/ql/test/query-tests/Nullness/NullMaybe.expected
@@ -24,7 +24,6 @@
 | C.java:10:17:10:18 | a3 | Variable $@ may be null at this access because of $@ assignment. | C.java:8:5:8:21 | long[] a3 | a3 | C.java:8:12:8:20 | a3 | this |
 | C.java:21:7:21:8 | s1 | Variable $@ may be null at this access because of $@ assignment. | C.java:14:5:14:30 | String s1 | s1 | C.java:17:7:17:24 | ...=... | this |
 | C.java:51:7:51:11 | slice | Variable $@ may be null at this access because of $@ assignment. | C.java:43:5:43:30 | List<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 |
diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll
new file mode 100644
index 000000000000..bbaea7b87ad0
--- /dev/null
+++ b/shared/controlflow/codeql/controlflow/Guards.qll
@@ -0,0 +1,1088 @@
+/**
+ * Provides classes and predicates for determining "guard-controls"
+ * relationships.
+ *
+ * In their most general form, these relate a guard expression, a value, and a
+ * basic block, and state that execution of the basic block implies that
+ * control flow must have passed through the guard in order to reach the basic
+ * block, and when it did, the guard evaluated to the given value.
+ *
+ * For example, in `if (x == 0) { A }`, the guard `x == 0` evaluating to `true`
+ * controls the basic block `A`, in this case because the true branch dominates
+ * `A`, but more elaborate controls-relationships may also hold.
+ * For example, in
+ * ```
+ * int sz = a != null ? a.length : 0;
+ * if (sz != 0) {
+ *   // this block is controlled by:
+ *   // sz != 0   evaluating to true
+ *   // sz        evaluating to not 0
+ *   // a.length  evaluating to not 0
+ *   // a != null evaluating to true
+ *   // a         evaluating to not null
+ * }
+ * ```
+ *
+ * The provided predicates are separated into general "controls" predicates and
+ * "directly controls" predicates. The former use all possible implication
+ * logic as described above, whereas the latter only use control flow dominance
+ * of the corresponding conditional successor edges.
+ *
+ * In some cases, a guard may have a successor edge that can be relevant for
+ * controlling the input to an SSA phi node, but does not dominate the
+ * preceding block. To support this, the `hasBranchEdge` and
+ * `controlsBranchEdge` predicates are provided, where the former only uses the
+ * control flow graph similar to the `directlyControls` predicate, and the
+ * latter uses the full implication logic.
+ *
+ * All of these predicates are also available in the more general form that refers
+ * to `GuardValue`s instead of `boolean`s.
+ *
+ * The implementation is nested in two parameterized modules intended to
+ * facilitate multiple instantiations of the nested module with different
+ * precision levels. For example, more implications are available if the result
+ * of Range Analysis is available, but Range Analysis depends on Guards. This
+ * allows an initial instantiation of the `Logic` module without Range Analysis
+ * that can be used as input to Range Analysis, and a second instantiation
+ * using the result of Range Analysis to provide a final and more complete
+ * controls relation.
+ */
+
+private import codeql.util.Boolean
+private import codeql.util.Location
+
+signature module InputSig<LocationSig Location> {
+  class SuccessorType {
+    /** Gets a textual representation of this successor type. */
+    string toString();
+  }
+
+  class ExceptionSuccessor extends SuccessorType;
+
+  class ConditionalSuccessor extends SuccessorType {
+    /** Gets the Boolean value of this successor. */
+    boolean getValue();
+  }
+
+  class BooleanSuccessor extends ConditionalSuccessor;
+
+  class NullnessSuccessor extends ConditionalSuccessor;
+
+  /** A control flow node. */
+  class ControlFlowNode {
+    /** Gets a textual representation of this control flow node. */
+    string toString();
+
+    /** Gets the location of this control flow node. */
+    Location getLocation();
+  }
+
+  /**
+   * A basic block, that is, a maximal straight-line sequence of control flow nodes
+   * without branches or joins.
+   */
+  class BasicBlock {
+    /** Gets a textual representation of this basic block. */
+    string toString();
+
+    /** Gets the `i`th node in this basic block. */
+    ControlFlowNode getNode(int i);
+
+    /** Gets the last control flow node in this basic block. */
+    ControlFlowNode getLastNode();
+
+    /** Gets the length of this basic block. */
+    int length();
+
+    /** Gets the location of this basic block. */
+    Location getLocation();
+
+    BasicBlock getASuccessor(SuccessorType t);
+
+    predicate dominates(BasicBlock bb);
+
+    predicate strictlyDominates(BasicBlock bb);
+  }
+
+  predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2);
+
+  class AstNode {
+    /** Gets a textual representation of this AST node. */
+    string toString();
+
+    /** Gets the location of this AST node. */
+    Location getLocation();
+  }
+
+  class Expr extends AstNode {
+    /** Gets the associated control flow node. */
+    ControlFlowNode getControlFlowNode();
+
+    /** Gets the basic block containing this expression. */
+    BasicBlock getBasicBlock();
+  }
+
+  class ConstantValue {
+    /** Gets a textual representation of this constant value. */
+    string toString();
+  }
+
+  class ConstantExpr extends Expr {
+    predicate isNull();
+
+    boolean asBooleanValue();
+
+    int asIntegerValue();
+
+    ConstantValue asConstantValue();
+  }
+
+  class NonNullExpr extends Expr;
+
+  class Case extends AstNode {
+    Expr getSwitchExpr();
+
+    predicate isDefaultCase();
+
+    ConstantExpr asConstantCase();
+
+    predicate matchEdge(BasicBlock bb1, BasicBlock bb2);
+
+    predicate nonMatchEdge(BasicBlock bb1, BasicBlock bb2);
+  }
+
+  class AndExpr extends Expr {
+    /** Gets an operand of this expression. */
+    Expr getAnOperand();
+  }
+
+  class OrExpr extends Expr {
+    /** Gets an operand of this expression. */
+    Expr getAnOperand();
+  }
+
+  class NotExpr extends Expr {
+    /** Gets the operand of this expression. */
+    Expr getOperand();
+  }
+
+  /**
+   * An expression that has the same value as a specific sub-expression.
+   *
+   * For example, in Java, the assignment `x = rhs` has the same value as `rhs`.
+   */
+  class IdExpr extends Expr {
+    Expr getEqualChildExpr();
+  }
+
+  class EqualityTest extends Expr {
+    /** Gets an operand of this expression. */
+    Expr getAnOperand();
+
+    /** Gets a boolean indicating whether this test is equality (true) or inequality (false). */
+    boolean polarity();
+  }
+
+  class ConditionalExpr extends Expr {
+    /** Gets the condition of this expression. */
+    Expr getCondition();
+
+    /** Gets the true branch of this expression. */
+    Expr getThen();
+
+    /** Gets the false branch of this expression. */
+    Expr getElse();
+  }
+}
+
+/** Provides guards-related predicates and classes. */
+module Make<LocationSig Location, InputSig<Location> Input> {
+  private import Input
+
+  private newtype TAbstractSingleValue =
+    TValueNull() or
+    TValueTrue() or
+    TValueInt(int i) { exists(ConstantExpr c | c.asIntegerValue() = i) or i = 0 } or
+    TValueConstant(ConstantValue c) { exists(ConstantExpr ce | ce.asConstantValue() = c) }
+
+  private newtype TGuardValue =
+    TValue(TAbstractSingleValue val, Boolean isVal) or
+    TException(Boolean throws)
+
+  private class AbstractSingleValue extends TAbstractSingleValue {
+    /** Gets a textual representation of this value. */
+    string toString() {
+      result = "null" and this instanceof TValueNull
+      or
+      result = "true" and this instanceof TValueTrue
+      or
+      exists(int i | result = i.toString() and this = TValueInt(i))
+      or
+      exists(ConstantValue c | result = c.toString() and this = TValueConstant(c))
+    }
+  }
+
+  /** An abstract value that a `Guard` may evaluate to. */
+  class GuardValue extends TGuardValue {
+    /**
+     * Gets the dual value. Examples of dual values include:
+     * - null vs. not null
+     * - true vs. false
+     * - evaluating to a specific value vs. evaluating to any other value
+     * - throwing an exception vs. not throwing an exception
+     */
+    GuardValue getDualValue() {
+      exists(AbstractSingleValue val, boolean isVal |
+        this = TValue(val, isVal) and
+        result = TValue(val, isVal.booleanNot())
+      )
+      or
+      exists(boolean throws |
+        this = TException(throws) and
+        result = TException(throws.booleanNot())
+      )
+    }
+
+    /** Holds if this value represents `null`. */
+    predicate isNullValue() { this.isNullness(true) }
+
+    /** Holds if this value represents non-`null`. */
+    predicate isNonNullValue() { this.isNullness(false) }
+
+    /** Holds if this value represents `null` or non-`null` as indicated by `isNull`. */
+    predicate isNullness(boolean isNull) { this = TValue(TValueNull(), isNull) }
+
+    /** Gets the integer that this value represents, if any. */
+    int asIntValue() { this = TValue(TValueInt(result), true) }
+
+    /** Gets the boolean that this value represents, if any. */
+    boolean asBooleanValue() { this = TValue(TValueTrue(), result) }
+
+    /** Gets the constant that this value represents, if any. */
+    ConstantValue asConstantValue() { this = TValue(TValueConstant(result), true) }
+
+    /** Holds if this value represents throwing an exception. */
+    predicate isThrowsException() { this = TException(true) }
+
+    /** Gets a textual representation of this value. */
+    string toString() {
+      result = this.asBooleanValue().toString()
+      or
+      exists(AbstractSingleValue val | not val instanceof TValueTrue |
+        this = TValue(val, true) and result = val.toString()
+        or
+        this = TValue(val, false) and result = "not " + val.toString()
+      )
+      or
+      exists(boolean throws | this = TException(throws) |
+        throws = true and result = "exception"
+        or
+        throws = false and result = "no exception"
+      )
+    }
+  }
+
+  bindingset[a, b]
+  pragma[inline_late]
+  private predicate disjointValues(GuardValue a, GuardValue b) {
+    a = b.getDualValue()
+    or
+    exists(AbstractSingleValue a1, AbstractSingleValue b1 |
+      a = TValue(a1, true) and
+      b = TValue(b1, true) and
+      a1 != b1
+    )
+  }
+
+  private predicate constantHasValue(ConstantExpr c, GuardValue v) {
+    c.isNull() and v.isNullValue()
+    or
+    v.asBooleanValue() = c.asBooleanValue()
+    or
+    v.asIntValue() = c.asIntegerValue()
+    or
+    v.asConstantValue() = c.asConstantValue()
+  }
+
+  private predicate exceptionBranchPoint(BasicBlock bb1, BasicBlock normalSucc, BasicBlock excSucc) {
+    exists(SuccessorType norm, ExceptionSuccessor exc |
+      bb1.getASuccessor(norm) = normalSucc and
+      bb1.getASuccessor(exc) = excSucc and
+      normalSucc != excSucc and
+      not norm instanceof ExceptionSuccessor
+    )
+  }
+
+  private predicate branchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue v) {
+    exists(ConditionalSuccessor s |
+      bb1.getASuccessor(s) = bb2 and
+      exists(AbstractSingleValue val |
+        s instanceof NullnessSuccessor and val = TValueNull()
+        or
+        s instanceof BooleanSuccessor and val = TValueTrue()
+      |
+        v = TValue(val, s.getValue())
+      )
+    )
+    or
+    exceptionBranchPoint(bb1, bb2, _) and v = TException(false)
+    or
+    exceptionBranchPoint(bb1, _, bb2) and v = TException(true)
+  }
+
+  private predicate caseBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue v, Case c) {
+    v.asBooleanValue() = true and
+    c.matchEdge(bb1, bb2)
+    or
+    v.asBooleanValue() = false and
+    c.nonMatchEdge(bb1, bb2)
+  }
+
+  pragma[nomagic]
+  private predicate eqtestHasOperands(EqualityTest eqtest, Expr e1, Expr e2, boolean polarity) {
+    eqtest.getAnOperand() = e1 and
+    eqtest.getAnOperand() = e2 and
+    e1 != e2 and
+    eqtest.polarity() = polarity
+  }
+
+  private predicate constcaseEquality(PreGuard g, Expr e1, ConstantExpr e2) {
+    exists(Case c |
+      g = c and
+      e1 = c.getSwitchExpr() and
+      e2 = c.asConstantCase()
+    )
+  }
+
+  final private class FinalAstNode = AstNode;
+
+  /**
+   * 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 PreGuard extends FinalAstNode {
+    /**
+     * Holds if this guard evaluating to `v` corresponds to taking the edge
+     * from `bb1` to `bb2`. For ordinary conditional branching this guard is
+     * the last node in `bb1`, but for switch case matching it is the switch
+     * expression, which may either be in `bb1` or an earlier basic block.
+     */
+    predicate hasValueBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue v) {
+      bb1.getLastNode() = this.(Expr).getControlFlowNode() and
+      branchEdge(bb1, bb2, v)
+      or
+      caseBranchEdge(bb1, bb2, v, this)
+    }
+
+    /**
+     * Holds if this guard evaluating to `v` directly controls the basic block `bb`.
+     *
+     * That is, `bb` is dominated by the `v`-successor edge of this guard.
+     */
+    predicate directlyValueControls(BasicBlock bb, GuardValue v) {
+      exists(BasicBlock guard, BasicBlock succ |
+        this.hasValueBranchEdge(guard, succ, v) and
+        dominatingEdge(guard, succ) and
+        succ.dominates(bb)
+      )
+    }
+
+    /**
+     * Holds if this guard is the last node in `bb1` and that its successor is
+     * `bb2` exactly when evaluating to `branch`.
+     */
+    predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) {
+      this.hasValueBranchEdge(bb1, bb2, any(GuardValue gv | gv.asBooleanValue() = branch))
+    }
+
+    /**
+     * Holds if this guard evaluating to `branch` directly controls the basic
+     * block `bb`.
+     *
+     * That is, `bb` is dominated by the `branch`-successor edge of this guard.
+     */
+    predicate directlyControls(BasicBlock bb, boolean branch) {
+      this.directlyValueControls(bb, any(GuardValue gv | gv.asBooleanValue() = branch))
+    }
+
+    /**
+     * Holds if this guard tests equality between `e1` and `e2` upon evaluating
+     * to `eqval`.
+     */
+    predicate isEquality(Expr e1, Expr e2, boolean eqval) {
+      eqtestHasOperands(this, e1, e2, eqval)
+      or
+      constcaseEquality(this, e1, e2) and eqval = true
+      or
+      constcaseEquality(this, e2, e1) and eqval = true
+    }
+
+    /**
+     * Gets the basic block of this guard. For expressions, this is the basic
+     * block of the expression itself, and for switch cases, this is the basic
+     * block of the expression being compared against the cases.
+     */
+    BasicBlock getBasicBlock() {
+      result = this.(Expr).getBasicBlock()
+      or
+      result = this.(Case).getSwitchExpr().getBasicBlock()
+    }
+  }
+
+  private Expr getBranchExpr(ConditionalExpr cond, boolean branch) {
+    branch = true and result = cond.getThen()
+    or
+    branch = false and result = cond.getElse()
+  }
+
+  private predicate baseImpliesStep(PreGuard g1, GuardValue v1, PreGuard g2, GuardValue v2) {
+    g1.(AndExpr).getAnOperand() = g2 and v1.asBooleanValue() = true and v2 = v1
+    or
+    g1.(OrExpr).getAnOperand() = g2 and v1.asBooleanValue() = false and v2 = v1
+    or
+    g1.(NotExpr).getOperand() = g2 and v1.asBooleanValue().booleanNot() = v2.asBooleanValue()
+    or
+    exists(GuardValue eqval, ConstantExpr constant, GuardValue cv |
+      g1.isEquality(g2, constant, eqval.asBooleanValue()) and
+      constantHasValue(constant, cv)
+    |
+      v1 = eqval and v2 = cv
+      or
+      v1 = eqval.getDualValue() and v2 = cv.getDualValue()
+    )
+    or
+    exists(NonNullExpr nonnull |
+      eqtestHasOperands(g1, g2, nonnull, v1.asBooleanValue()) and
+      v2.isNonNullValue()
+    )
+    or
+    exists(Case c1, Expr switchExpr |
+      g1 = c1 and
+      c1.isDefaultCase() and
+      c1.getSwitchExpr() = switchExpr and
+      v1.asBooleanValue() = true and
+      g2.(Case).getSwitchExpr() = switchExpr and
+      v2.asBooleanValue() = false and
+      g1 != g2
+    )
+  }
+
+  signature module LogicInputSig {
+    class SsaDefinition {
+      /** Gets the basic block to which this SSA definition belongs. */
+      BasicBlock getBasicBlock();
+
+      Expr getARead();
+
+      /** Gets a textual representation of this SSA definition. */
+      string toString();
+
+      /** Gets the location of this SSA definition. */
+      Location getLocation();
+    }
+
+    class SsaWriteDefinition extends SsaDefinition {
+      Expr getDefinition();
+    }
+
+    class SsaPhiNode extends SsaDefinition {
+      /** Holds if `inp` is an input to the phi node along the edge originating in `bb`. */
+      predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb);
+    }
+
+    /**
+     * Holds if `guard` evaluating to `val` ensures that:
+     * `e <= k` when `upper = true`
+     * `e >= k` when `upper = false`
+     */
+    default predicate rangeGuard(PreGuard guard, GuardValue val, Expr e, int k, boolean upper) {
+      none()
+    }
+
+    /**
+     * Holds if `guard` evaluating to `val` ensures that:
+     * `e == null` when `isNull = true`
+     * `e != null` when `isNull = false`
+     */
+    default predicate additionalNullCheck(PreGuard guard, GuardValue val, Expr e, boolean isNull) {
+      none()
+    }
+
+    /**
+     * Holds if the assumption that `g1` has been evaluated to `v1` implies that
+     * `g2` has been evaluated to `v2`, that is, the evaluation of `g2` to `v2`
+     * dominates the evaluation of `g1` to `v1`.
+     *
+     * This predicate can be instantiated with `CustomGuard<..>::additionalImpliesStep`.
+     */
+    default predicate additionalImpliesStep(PreGuard g1, GuardValue v1, PreGuard g2, GuardValue v2) {
+      none()
+    }
+  }
+
+  /**
+   * Provides the `Guard` class with suitable 'controls' predicates augmented
+   * with logical implications based on SSA.
+   */
+  module Logic<LogicInputSig LogicInput> {
+    private import LogicInput
+
+    private predicate guardControlsPhiBranch(
+      Guard guard, GuardValue v, SsaPhiNode phi, SsaDefinition inp
+    ) {
+      exists(BasicBlock bbPhi |
+        phi.hasInputFromBlock(inp, _) and
+        phi.getBasicBlock() = bbPhi and
+        guard.getBasicBlock().strictlyDominates(bbPhi) and
+        not guard.directlyValueControls(bbPhi, _) and
+        forex(BasicBlock bbInput | phi.hasInputFromBlock(inp, bbInput) |
+          guard.directlyValueControls(bbInput, v) or
+          guard.hasValueBranchEdge(bbInput, bbPhi, v)
+        )
+      )
+    }
+
+    /**
+     * Holds if `phi` takes `input` exactly when `guard` is `v`. That is,
+     * `guard == v` directly controls `input` and `guard == v.getDualValue()`
+     * directly controls all other inputs to `phi`.
+     *
+     * This makes `phi` similar to the conditional `phi = guard==v ? input : ...`.
+     */
+    private predicate guardDeterminesPhiInput(Guard guard, GuardValue v, SsaPhiNode phi, Expr input) {
+      exists(GuardValue dv, SsaWriteDefinition inp |
+        guardControlsPhiBranch(guard, v, phi, inp) and
+        inp.getDefinition() = input and
+        dv = v.getDualValue() and
+        forall(SsaDefinition other | phi.hasInputFromBlock(other, _) and other != inp |
+          guardControlsPhiBranch(guard, dv, phi, other)
+        )
+      )
+    }
+
+    pragma[nomagic]
+    private predicate guardChecksEqualVars(
+      Guard guard, SsaDefinition v1, SsaDefinition v2, boolean branch
+    ) {
+      eqtestHasOperands(guard, v1.getARead(), v2.getARead(), branch)
+    }
+
+    private predicate guardReadsSsaVar(Guard guard, SsaDefinition def) {
+      def.getARead() = guard
+      or
+      exists(Guard eqtest, SsaDefinition other, boolean branch |
+        guardChecksEqualVars(eqtest, def, other, branch) and
+        other.getARead() = guard and
+        eqtest.directlyControls(guard.getBasicBlock(), branch)
+      )
+      or
+      // An expression `x = ...` can be considered as a read of `x`.
+      guard.(IdExpr).getEqualChildExpr() = def.(SsaWriteDefinition).getDefinition()
+    }
+
+    private predicate valueStep(Expr e1, Expr e2) {
+      e2.(ConditionalExpr).getThen() = e1 or
+      e2.(ConditionalExpr).getElse() = e1 or
+      e2.(IdExpr).getEqualChildExpr() = e1
+    }
+
+    /**
+     * Gets a sub-expression of `e` whose value can flow to `e` through
+     * `valueStep`s
+     */
+    private Expr possibleValue(Expr e) {
+      result = possibleValue(any(Expr e1 | valueStep(e1, e)))
+      or
+      result = e and not valueStep(_, e)
+    }
+
+    /**
+     * Gets an ultimate definition of `v` that is not itself a phi node. The
+     * boolean `fromBackEdge` indicates whether the flow from `result` to `v` goes
+     * through a back edge.
+     */
+    private SsaDefinition getADefinition(SsaDefinition v, boolean fromBackEdge) {
+      result = v and not v instanceof SsaPhiNode and fromBackEdge = false
+      or
+      exists(SsaDefinition inp, BasicBlock bb, boolean fbe |
+        v.(SsaPhiNode).hasInputFromBlock(inp, bb) and
+        result = getADefinition(inp, fbe) and
+        (if v.getBasicBlock().dominates(bb) then fromBackEdge = true else fromBackEdge = fbe)
+      )
+    }
+
+    /**
+     * Holds if `v` can have a value that is not representable as an `GuardValue`.
+     */
+    private predicate hasPossibleUnknownValue(SsaDefinition v) {
+      exists(SsaDefinition def | def = getADefinition(v, _) |
+        not exists(def.(SsaWriteDefinition).getDefinition())
+        or
+        exists(Expr e | e = possibleValue(def.(SsaWriteDefinition).getDefinition()) |
+          not constantHasValue(e, _)
+        )
+      )
+    }
+
+    /**
+     * Holds if `e` equals `k` and may be assigned to `v`. The boolean
+     * `fromBackEdge` indicates whether the flow from `e` to `v` goes through a
+     * back edge.
+     */
+    private predicate possibleValue(SsaDefinition v, boolean fromBackEdge, Expr e, GuardValue k) {
+      not hasPossibleUnknownValue(v) and
+      exists(SsaWriteDefinition def |
+        def = getADefinition(v, fromBackEdge) and
+        e = possibleValue(def.getDefinition()) and
+        constantHasValue(e, k)
+      )
+    }
+
+    /**
+     * Holds if `e` equals `k` and may be assigned to `v` without going through
+     * back edges, and all other possible ultimate definitions of `v` are different
+     * from `k`. The trivial case where `v` is an `SsaWriteDefinition` with `e` as
+     * the only possible value is excluded.
+     */
+    private predicate uniqueValue(SsaDefinition v, Expr e, GuardValue k) {
+      possibleValue(v, false, e, k) and
+      forex(Expr other, GuardValue otherval | possibleValue(v, _, other, otherval) and other != e |
+        disjointValues(otherval, k)
+      )
+    }
+
+    /**
+     * Holds if `phi` has exactly two inputs, `def1` and `e2`, and that `def1`
+     * does not come from a back-edge into `phi`.
+     */
+    private predicate phiWithTwoInputs(SsaPhiNode phi, SsaDefinition def1, Expr e2) {
+      exists(SsaWriteDefinition def2, BasicBlock bb1 |
+        2 = strictcount(SsaDefinition inp, BasicBlock bb | phi.hasInputFromBlock(inp, bb)) and
+        phi.hasInputFromBlock(def1, bb1) and
+        phi.hasInputFromBlock(def2, _) and
+        def1 != def2 and
+        not phi.getBasicBlock().dominates(bb1) and
+        def2.getDefinition() = e2
+      )
+    }
+
+    /** Holds if `e` may take the value `k` */
+    private predicate relevantInt(Expr e, int k) {
+      e.(ConstantExpr).asIntegerValue() = k
+      or
+      relevantInt(any(Expr e1 | valueStep(e1, e)), k)
+      or
+      exists(SsaDefinition def |
+        guardReadsSsaVar(e, def) and
+        relevantInt(getADefinition(def, _).(SsaWriteDefinition).getDefinition(), k)
+      )
+    }
+
+    private predicate impliesStep1(Guard g1, GuardValue v1, Guard g2, GuardValue v2) {
+      baseImpliesStep(g1, v1, g2, v2)
+      or
+      exists(SsaDefinition def, Expr e |
+        // If `def = g2 ? v1 : ...` and all other assignments to `def` are different from
+        // `v1` then a guard proving `def == v1` ensures that `g2` evaluates to `v2`.
+        uniqueValue(def, e, v1) and
+        guardReadsSsaVar(g1, def) and
+        g2.directlyValueControls(e.getBasicBlock(), v2) and
+        not g2.directlyValueControls(g1.getBasicBlock(), v2)
+      )
+      or
+      exists(int k1, int k2, boolean upper |
+        rangeGuard(g1, v1, g2, k1, upper) and
+        relevantInt(g2, k2) and
+        v2 = TValue(TValueInt(k2), false)
+      |
+        upper = true and k1 < k2 // g2 <= k1 < k2  ==>  g2 != k2
+        or
+        upper = false and k1 > k2 // g2 >= k1 > k2  ==>  g2 != k2
+      )
+      or
+      exists(boolean isNull |
+        additionalNullCheck(g1, v1, g2, isNull) and
+        v2.isNullness(isNull) and
+        not (g2 instanceof NonNullExpr and isNull = false) // disregard trivial guard
+      )
+    }
+
+    /**
+     * Holds if `g` evaluating to `v` implies that `def` evaluates to `ssaVal`.
+     * The included set of implications is somewhat restricted to avoid a
+     * recursive dependency on `exprHasValue`.
+     */
+    private predicate baseSsaValueCheck(SsaDefinition def, GuardValue ssaVal, Guard g, GuardValue v) {
+      exists(Guard g0, GuardValue v0 |
+        guardReadsSsaVar(g0, def) and v0 = ssaVal
+        or
+        baseSsaValueCheck(def, ssaVal, g0, v0)
+      |
+        impliesStep1(g, v, g0, v0)
+      )
+    }
+
+    private predicate exprHasValue(Expr e, GuardValue v) {
+      constantHasValue(e, v)
+      or
+      e instanceof NonNullExpr and v.isNonNullValue()
+      or
+      exprHasValue(e.(IdExpr).getEqualChildExpr(), v)
+      or
+      exists(SsaDefinition def, Guard g, GuardValue gv |
+        e = def.getARead() and
+        g.directlyValueControls(e.getBasicBlock(), gv) and
+        baseSsaValueCheck(def, v, g, gv)
+      )
+      or
+      exists(SsaWriteDefinition def |
+        exprHasValue(def.getDefinition(), v) and
+        e = def.getARead()
+      )
+    }
+
+    private predicate impliesStep2(Guard g1, GuardValue v1, Guard g2, GuardValue v2) {
+      impliesStep1(g1, v1, g2, v2)
+      or
+      exists(Expr nonnull |
+        exprHasValue(nonnull, v2) and
+        eqtestHasOperands(g1, g2, nonnull, v1.asBooleanValue()) and
+        v2.isNonNullValue()
+      )
+    }
+
+    bindingset[g1, v1]
+    pragma[inline_late]
+    private predicate unboundImpliesStep(Guard g1, GuardValue v1, Guard g2, GuardValue v2) {
+      g1.(IdExpr).getEqualChildExpr() = g2 and v1 = v2 and not v1 instanceof TException
+      or
+      exists(ConditionalExpr cond, boolean branch, Expr e, GuardValue ev |
+        cond = g1 and
+        e = getBranchExpr(cond, branch) and
+        exprHasValue(e, ev) and
+        disjointValues(v1, ev)
+      |
+        // g1 === g2 ? e : ...;
+        // g1 === g2 ? ... : e;
+        g2 = cond.getCondition() and
+        v2.asBooleanValue() = branch.booleanNot()
+        or
+        // g1 === ... ? g2 : e
+        // g1 === ... ? e : g2
+        g2 = getBranchExpr(cond, branch.booleanNot()) and
+        v2 = v1 and
+        not exprHasValue(g2, v2) // disregard trivial guard
+      )
+    }
+
+    bindingset[def1, v1]
+    pragma[inline_late]
+    private predicate impliesStepSsaGuard(SsaDefinition def1, GuardValue v1, Guard g2, GuardValue v2) {
+      def1.(SsaWriteDefinition).getDefinition() = g2 and
+      v1 = v2 and
+      not exprHasValue(g2, v2) // disregard trivial guard
+      or
+      exists(Expr e, GuardValue ev |
+        guardDeterminesPhiInput(g2, v2.getDualValue(), def1, e) and
+        exprHasValue(e, ev) and
+        disjointValues(v1, ev)
+      )
+    }
+
+    bindingset[def1, v]
+    pragma[inline_late]
+    private predicate impliesStepSsa(SsaDefinition def1, GuardValue v, SsaDefinition def2) {
+      exists(Expr e, GuardValue ev |
+        phiWithTwoInputs(def1, def2, e) and
+        exprHasValue(e, ev) and
+        disjointValues(v, ev)
+      )
+    }
+
+    private signature predicate baseGuardValueSig(Guard guard, GuardValue v);
+
+    /**
+     * Calculates the transitive closure of all the guard implication steps
+     * starting from a given set of base cases.
+     */
+    module ImpliesTC<baseGuardValueSig/2 baseGuardValue> {
+      /**
+       * Holds if `tgtGuard` evaluating to `tgtVal` implies that `guard`
+       * evaluates to `v`.
+       */
+      pragma[nomagic]
+      predicate guardControls(Guard guard, GuardValue v, Guard tgtGuard, GuardValue tgtVal) {
+        baseGuardValue(tgtGuard, tgtVal) and
+        guard = tgtGuard and
+        v = tgtVal
+        or
+        exists(Guard g0, GuardValue v0 |
+          guardControls(g0, v0, tgtGuard, tgtVal) and
+          impliesStep2(g0, v0, guard, v)
+        )
+        or
+        exists(Guard g0, GuardValue v0 |
+          guardControls(g0, v0, tgtGuard, tgtVal) and
+          unboundImpliesStep(g0, v0, guard, v)
+        )
+        or
+        exists(SsaDefinition def0, GuardValue v0 |
+          ssaControls(def0, v0, tgtGuard, tgtVal) and
+          impliesStepSsaGuard(def0, v0, guard, v)
+        )
+        or
+        exists(Guard g0, GuardValue v0 |
+          guardControls(g0, v0, tgtGuard, tgtVal) and
+          additionalImpliesStep(g0, v0, guard, v)
+        )
+      }
+
+      /**
+       * Holds if `tgtGuard` evaluating to `tgtVal` implies that `def`
+       * evaluates to `v`.
+       */
+      pragma[nomagic]
+      predicate ssaControls(SsaDefinition def, GuardValue v, Guard tgtGuard, GuardValue tgtVal) {
+        exists(Guard g0 |
+          guardControls(g0, v, tgtGuard, tgtVal) and
+          guardReadsSsaVar(g0, def)
+        )
+        or
+        exists(SsaDefinition def0 |
+          ssaControls(def0, v, tgtGuard, tgtVal) and
+          impliesStepSsa(def0, v, def)
+        )
+      }
+    }
+
+    private predicate booleanGuard(Guard guard, GuardValue val) {
+      exists(guard) and exists(val.asBooleanValue())
+    }
+
+    private module BooleanImplies = ImpliesTC<booleanGuard/2>;
+
+    /** INTERNAL: Don't use. */
+    predicate boolImplies(Guard g1, GuardValue v1, Guard g2, GuardValue v2) {
+      BooleanImplies::guardControls(g2, v2, g1, v1) and
+      g2 != g1
+    }
+
+    /**
+     * Holds if `guard` evaluating to `v` implies that `e` is guaranteed to be
+     * null if `isNull` is true, and non-null if `isNull` is false.
+     */
+    predicate nullGuard(Guard guard, GuardValue v, Expr e, boolean isNull) {
+      impliesStep2(guard, v, e, any(GuardValue gv | gv.isNullness(isNull))) or
+      additionalImpliesStep(guard, v, e, any(GuardValue gv | gv.isNullness(isNull)))
+    }
+
+    private predicate hasAValueBranchEdge(Guard guard, GuardValue v) {
+      guard.hasValueBranchEdge(_, _, v)
+    }
+
+    private module BranchImplies = ImpliesTC<hasAValueBranchEdge/2>;
+
+    private predicate guardControlsBranchEdge(
+      Guard guard, BasicBlock bb1, BasicBlock bb2, GuardValue v
+    ) {
+      exists(Guard g0, GuardValue v0 |
+        g0.hasValueBranchEdge(bb1, bb2, v0) and
+        BranchImplies::guardControls(guard, v, g0, v0)
+      )
+    }
+
+    /**
+     * Holds if `def` evaluating to `v` controls the control-flow branch
+     * edge from `bb1` to `bb2`. That is, following the edge from `bb1` to
+     * `bb2` implies that `def` evaluated to `v`.
+     */
+    predicate ssaControlsBranchEdge(SsaDefinition def, BasicBlock bb1, BasicBlock bb2, GuardValue v) {
+      exists(Guard g0, GuardValue v0 |
+        g0.hasValueBranchEdge(bb1, bb2, v0) and
+        BranchImplies::ssaControls(def, v, g0, v0)
+      )
+    }
+
+    /**
+     * Holds if `def` evaluating to `v` controls the basic block `bb`.
+     * That is, execution of `bb` implies that `def` evaluated to `v`.
+     */
+    predicate ssaControls(SsaDefinition def, BasicBlock bb, GuardValue v) {
+      exists(BasicBlock guard, BasicBlock succ |
+        ssaControlsBranchEdge(def, guard, succ, v) and
+        dominatingEdge(guard, succ) and
+        succ.dominates(bb)
+      )
+    }
+
+    signature module CustomGuardInputSig {
+      class ParameterPosition {
+        /** Gets a textual representation of this element. */
+        bindingset[this]
+        string toString();
+      }
+
+      class ArgumentPosition {
+        /** Gets a textual representation of this element. */
+        bindingset[this]
+        string toString();
+      }
+
+      /**
+       * Holds if the parameter position `ppos` matches the argument position
+       * `apos`.
+       */
+      predicate parameterMatch(ParameterPosition ppos, ArgumentPosition apos);
+
+      /** A non-overridable method with a boolean return value. */
+      class BooleanMethod {
+        SsaDefinition getParameter(ParameterPosition ppos);
+
+        Expr getAReturnExpr();
+      }
+
+      class BooleanMethodCall extends Expr {
+        BooleanMethod getMethod();
+
+        Expr getArgument(ArgumentPosition apos);
+      }
+    }
+
+    /**
+     * Provides an implementation of guard implication logic for custom
+     * wrappers. This can be used to instantiate the `additionalImpliesStep`
+     * predicate.
+     */
+    module CustomGuard<CustomGuardInputSig CustomGuardInput> {
+      private import CustomGuardInput
+
+      final private class FinalExpr = Expr;
+
+      private class ReturnExpr extends FinalExpr {
+        ReturnExpr() { any(BooleanMethod m).getAReturnExpr() = this }
+
+        pragma[nomagic]
+        BasicBlock getBasicBlock() { result = super.getBasicBlock() }
+      }
+
+      private predicate booleanReturnGuard(Guard guard, GuardValue val) {
+        guard instanceof ReturnExpr and exists(val.asBooleanValue())
+      }
+
+      private module ReturnImplies = ImpliesTC<booleanReturnGuard/2>;
+
+      /**
+       * Holds if `ret` is a return expression in a non-overridable method that
+       * on a return value of `retval` allows the conclusion that the `ppos`th
+       * parameter has the value `val`.
+       */
+      private predicate validReturnInCustomGuard(
+        ReturnExpr ret, ParameterPosition ppos, boolean retval, GuardValue val
+      ) {
+        exists(BooleanMethod m, SsaDefinition param |
+          m.getAReturnExpr() = ret and
+          m.getParameter(ppos) = param
+        |
+          exists(Guard g0, GuardValue v0 |
+            g0.directlyValueControls(ret.getBasicBlock(), v0) and
+            BranchImplies::ssaControls(param, val, g0, v0) and
+            retval = [true, false]
+          )
+          or
+          ReturnImplies::ssaControls(param, val, ret,
+            any(GuardValue r | r.asBooleanValue() = retval))
+        )
+      }
+
+      /**
+       * Gets a non-overridable method with a boolean return value that performs a check
+       * on the `ppos`th parameter. A return value equal to `retval` allows us to conclude
+       * that the argument has the value `val`.
+       */
+      private BooleanMethod customGuard(ParameterPosition ppos, boolean retval, GuardValue val) {
+        forex(ReturnExpr ret |
+          result.getAReturnExpr() = ret and
+          not ret.(ConstantExpr).asBooleanValue() = retval.booleanNot()
+        |
+          validReturnInCustomGuard(ret, ppos, retval, val)
+        )
+      }
+
+      /**
+       * Holds if the assumption that `g1` has been evaluated to `v1` implies that
+       * `g2` has been evaluated to `v2`, that is, the evaluation of `g2` to `v2`
+       * dominates the evaluation of `g1` to `v1`.
+       *
+       * This predicate covers the implication steps that arise from calls to
+       * custom guard wrappers.
+       */
+      predicate additionalImpliesStep(PreGuard g1, GuardValue v1, PreGuard g2, GuardValue v2) {
+        exists(BooleanMethodCall call, ParameterPosition ppos, ArgumentPosition apos |
+          g1 = call and
+          call.getMethod() = customGuard(ppos, v1.asBooleanValue(), v2) and
+          call.getArgument(apos) = g2 and
+          parameterMatch(pragma[only_bind_out](ppos), pragma[only_bind_out](apos))
+        )
+      }
+    }
+
+    /**
+     * 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 PreGuard {
+      /**
+       * Holds if this guard evaluating to `v` controls the control-flow branch
+       * edge from `bb1` to `bb2`. That is, following the edge from `bb1` to
+       * `bb2` implies that this guard evaluated to `v`.
+       *
+       * Note that this goes beyond mere control-flow graph dominance, as it
+       * also considers additional logical reasoning.
+       */
+      predicate valueControlsBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue v) {
+        guardControlsBranchEdge(this, bb1, bb2, v)
+      }
+
+      /**
+       * Holds if this guard evaluating to `v` controls the basic block `bb`.
+       * That is, execution of `bb` implies that this guard evaluated to `v`.
+       *
+       * Note that this goes beyond mere control-flow graph dominance, as it
+       * also considers additional logical reasoning.
+       */
+      predicate valueControls(BasicBlock bb, GuardValue v) {
+        exists(BasicBlock guard, BasicBlock succ |
+          this.valueControlsBranchEdge(guard, succ, v) and
+          dominatingEdge(guard, succ) and
+          succ.dominates(bb)
+        )
+      }
+
+      /**
+       * Holds if this guard evaluating to `branch` controls the control-flow
+       * branch edge from `bb1` to `bb2`. That is, following the edge from
+       * `bb1` to `bb2` implies that this guard evaluated to `branch`.
+       *
+       * Note that this goes beyond mere control-flow graph dominance, as it
+       * also considers additional logical reasoning.
+       */
+      predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) {
+        this.valueControlsBranchEdge(bb1, bb2, any(GuardValue gv | gv.asBooleanValue() = branch))
+      }
+
+      /**
+       * Holds if this guard evaluating to `branch` controls the basic block
+       * `bb`. That is, execution of `bb` implies that this guard evaluated to
+       * `branch`.
+       *
+       * Note that this goes beyond mere control-flow graph dominance, as it
+       * also considers additional logical reasoning.
+       */
+      predicate controls(BasicBlock bb, boolean branch) {
+        this.valueControls(bb, any(GuardValue gv | gv.asBooleanValue() = branch))
+      }
+    }
+  }
+}