Restrict getCheckedType to unrestricted records, introduce getSyntacticCheckedType and use that where appropriate

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

@@ -78,6 +78,8 @@ predicate depends(RefType t, RefType dep) {
     // the type accessed in an `instanceof` expression in `t`.
     exists(InstanceOfExpr ioe | t = ioe.getEnclosingCallable().getDeclaringType() |
       usesType(ioe.getCheckedType(), dep)
+      or
+      usesType(ioe.getPattern().getAChildExpr*().getType(), dep)
     )
     or
     // A type accessed in a pattern-switch case statement in `t`.

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

@@ -101,6 +101,8 @@ predicate numDepends(RefType t, RefType dep, int value) {
         t = ioe.getEnclosingCallable().getDeclaringType()
       |
         usesType(ioe.getCheckedType(), dep)
+        or
+        usesType(ioe.getPattern().getAChildExpr*().getType(), dep)
       )
       or
       // the type accessed in a pattern-switch case statement in `t`.

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

@@ -1592,9 +1592,27 @@ class InstanceOfExpr extends Expr, @instanceofexpr {
   /**
    * Gets the type this `instanceof` expression checks for.
    *
-   * For a match against a record pattern, this is the type of the outermost record type.
+   * For a match against a record pattern, this is the type of the outermost record type, and only holds if
+   * the record pattern matches that type unconditionally, i.e. it does not restrict field types more tightly
+   * than the fields' declared types and therefore match a subset of `rpe.getType()`.
    */
   RefType getCheckedType() {
+    result = this.getTypeName().getType()
+    or
+    exists(RecordPatternExpr rpe | rpe = this.getPattern().asRecordPattern() |
+      result = rpe.getType() and rpe.isUnrestricted()
+    )
+  }
+
+  /**
+   * Gets the type this `instanceof` expression checks for.
+   *
+   * For a match against a record pattern, this is the type of the outermost record type. Note that because
+   * the record match might additionally constrain field or sub-record fields to have a more specific type,
+   * and so while if the `instanceof` test passes we know that `this.getExpr()` has this type, if it fails
+   * we do not know that it doesn't.
+   */
+  RefType getSyntacticCheckedType() {
     result = this.getTypeName().getType()
     or
     result = this.getPattern().asRecordPattern().getType()

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

@@ -204,7 +204,7 @@ class TypeTestGuard extends Guard {
   TypeTestGuard() {
     exists(InstanceOfExpr ioe | this = ioe |
       testedExpr = ioe.getExpr() and
-      testedType = ioe.getCheckedType()
+      testedType = ioe.getSyntacticCheckedType()
     )
     or
     exists(PatternCase pc | this = pc |

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

@@ -627,7 +627,7 @@ private predicate instanceofDisjunctionGuarded(TypeFlowNode n, RefType t) {
     bb.bbDominates(va.getBasicBlock()) and
     va = v.getAUse() and
     instanceofDisjunct(ioe, bb, v) and
-    t = ioe.getCheckedType() and
+    t = ioe.getSyntacticCheckedType() and
     n.asExpr() = va
   )
 }

java/ql/src/Language Abuse/DubiousTypeTestOfThis.ql

@@ -17,7 +17,7 @@ from InstanceOfExpr ioe, RefType t, RefType ct
 where
   ioe.getExpr() instanceof ThisAccess and
   t = ioe.getExpr().getType() and
-  ct = ioe.getCheckedType() and
+  ct = ioe.getSyntacticCheckedType() and
   ct.getAnAncestor() = t
 select ioe,
   "Testing whether 'this' is an instance of $@ in $@ introduces a dependency cycle between the two types.",

java/ql/src/Likely Bugs/Comparison/EqualsUsesInstanceOf.ql

@@ -18,7 +18,7 @@ predicate instanceofInEquals(EqualsMethod m, InstanceOfExpr e) {
   e.getEnclosingCallable() = m and
   e.getExpr().(VarAccess).getVariable() = m.getParameter() and
   exists(RefType instanceofType |
-    instanceofType = e.getCheckedType() and
+    instanceofType = e.getSyntacticCheckedType() and
     not instanceofType.isFinal()
   )
 }