First stab at implementing negative type-test logic for pattern-case

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

@@ -1512,5 +1512,5 @@ class ConditionNode extends ControlFlowNode {
   ControlFlowNode getAFalseSuccessor() { result = this.getABranchSuccessor(false) }
 
   /** Gets the condition of this `ConditionNode`. This is equal to the node itself. */
-  Expr getCondition() { result = this }
+  ExprParent getCondition() { result = this }
 }

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

@@ -18,7 +18,7 @@ class ConditionBlock extends BasicBlock {
   ConditionNode getConditionNode() { result = this.getLastNode() }
 
   /** Gets the condition of the last node of this basic block. */
-  Expr getCondition() { result = this.getConditionNode().getCondition() }
+  ExprParent getCondition() { result = this.getConditionNode().getCondition() }
 
   /** Gets a `true`- or `false`-successor of the last node of this basic block. */
   BasicBlock getTestSuccessor(boolean testIsTrue) {
@@ -174,6 +174,30 @@ class Guard extends ExprParent {
   }
 }
 
+/**
+ * A `Guard` that tests an expression's type -- that is, an `instanceof T` or a
+ * `case T varname` pattern case.
+ */
+class TypeTestGuard extends Guard {
+  Expr testedExpr;
+  Type testedType;
+
+  TypeTestGuard() {
+    exists(InstanceOfExpr ioe | this = ioe |
+      testedExpr = ioe.getExpr() and
+      testedType = ioe.getCheckedType()
+    )
+    or
+    exists(PatternCase pc | this = pc |
+      pc.getSelectorExpr() = testedExpr and
+      testedType = pc.getPattern().getType()
+    )
+  }
+
+  /** Holds if this guard tests whether `e` has type `t`. */
+  predicate appliesTypeTest(Expr e, Type t) { e = testedExpr and t = testedType }
+}
+
 private predicate switchCaseControls(SwitchCase sc, BasicBlock bb) {
   exists(BasicBlock caseblock, Expr selector |
     selector = sc.getSelectorExpr() and

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

@@ -413,26 +413,12 @@ private predicate downcastSuccessor(VarAccess va, RefType t) {
   )
 }
 
-private predicate isTypeTestGuard(Guard test, Expr tested, Type t) {
-  exists(InstanceOfExpr ioe |
-    test = ioe and
-    ioe.getExpr() = tested and
-    t = ioe.getCheckedType()
-  )
-  or
-  exists(PatternCase pc |
-    test = pc and
-    pc.getSelectorExpr() = tested and
-    t = pc.getPattern().getType()
-  )
-}
-
 /**
  * Holds if `va` is an access to a value that is guarded by `instanceof t` or `case e t`.
  */
 private predicate typeTestGuarded(VarAccess va, RefType t) {
-  exists(Guard typeTest, BaseSsaVariable v |
-    isTypeTestGuard(typeTest, v.getAUse(), t) and
+  exists(TypeTestGuard typeTest, BaseSsaVariable v |
+    typeTest.appliesTypeTest(v.getAUse(), t) and
     va = v.getAUse() and
     guardControls_v1(typeTest, va.getBasicBlock(), true)
   )
@@ -442,8 +428,8 @@ private predicate typeTestGuarded(VarAccess va, RefType t) {
  * Holds if `aa` is an access to a value that is guarded by `instanceof t` or `case e t`.
  */
 predicate arrayTypeTestGuarded(ArrayAccess aa, RefType t) {
-  exists(Guard typeTest, BaseSsaVariable v1, BaseSsaVariable v2, ArrayAccess aa1 |
-    isTypeTestGuard(typeTest, aa1, t) and
+  exists(TypeTestGuard typeTest, BaseSsaVariable v1, BaseSsaVariable v2, ArrayAccess aa1 |
+    typeTest.appliesTypeTest(aa1, t) and
     aa1.getArray() = v1.getAUse() and
     aa1.getIndexExpr() = v2.getAUse() and
     aa.getArray() = v1.getAUse() and

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

@@ -194,13 +194,12 @@ private module Dispatch {
    */
   private predicate impossibleDispatchTarget(MethodCall source, Method tgt) {
     tgt = viableImpl_v1_cand(source) and
-    exists(InstanceOfExpr ioe, BaseSsaVariable v, Expr q, RefType t |
+    exists(TypeTestGuard typeTest, BaseSsaVariable v, Expr q, RefType t |
       source.getQualifier() = q and
       v.getAUse() = q and
-      guardControls_v1(ioe, q.getBasicBlock(), false) and
-      ioe.getExpr() = v.getAUse() and
-      ioe.getCheckedType().getErasure() = t and
-      tgt.getDeclaringType().getSourceDeclaration().getASourceSupertype*() = t
+      typeTest.appliesTypeTest(v.getAUse(), t) and
+      guardControls_v1(typeTest, q.getBasicBlock(), false) and
+      tgt.getDeclaringType().getSourceDeclaration().getASourceSupertype*() = t.getErasure()
     )
   }
 

java/ql/test/library-tests/switch-default-impossible-dispatch/Test.java

@@ -0,0 +1,31 @@
+public class Test {
+
+  public static int source() { return 0; }
+  public static void sink(int x) { }
+
+  interface I { void take(int x); }
+  static class C1 implements I { public void take(int x) { sink(x); } }
+  static class C2 implements I { public void take(int x) { sink(x); } }
+
+  public static void test(boolean unknown, int alsoUnknown) {
+
+    I c1or2 = unknown ? new C1() : new C2();
+
+    switch(c1or2) {
+      case C1 c1 when alsoUnknown == 1 -> { }
+      default -> c1or2.take(source()); // Could call either implementation
+    }
+
+    switch(c1or2) {
+      case C1 c1 -> { }
+      default -> c1or2.take(source()); // Can't call C1.take
+    }
+
+    switch(c1or2) {
+      case C1 c1 -> { }
+      case null, default -> c1or2.take(source()); // Can't call C1.take
+    }
+
+  }
+
+}

java/ql/test/library-tests/switch-default-impossible-dispatch/options

@@ -0,0 +1 @@
+//semmle-extractor-options: --javac-args --release 21

java/ql/test/library-tests/switch-default-impossible-dispatch/test.expected

@@ -0,0 +1,4 @@
+| Test.java:16:29:16:36 | source(...) | Test.java:7:65:7:65 | x |
+| Test.java:16:29:16:36 | source(...) | Test.java:8:65:8:65 | x |
+| Test.java:21:29:21:36 | source(...) | Test.java:8:65:8:65 | x |
+| Test.java:26:40:26:47 | source(...) | Test.java:8:65:8:65 | x |

java/ql/test/library-tests/switch-default-impossible-dispatch/test.ql

@@ -0,0 +1,18 @@
+import java
+import semmle.code.java.dataflow.DataFlow
+
+module TestConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node source) {
+    source.asExpr() = any(MethodCall mc | mc.getMethod().getName() = "source")
+  }
+
+  predicate isSink(DataFlow::Node sink) {
+    sink.asExpr() = any(MethodCall mc | mc.getMethod().getName() = "sink").getAnArgument()
+  }
+}
+
+module Flow = DataFlow::Global<TestConfig>;
+
+from DataFlow::Node source, DataFlow::Node sink
+where Flow::flow(source, sink)
+select source, sink