Merge remote-tracking branch 'origin/main' into smowton/admin/merge-rc319-into-main

shared/controlflow/codeql/controlflow/Guards.qll

@@ -873,77 +873,85 @@ module Make<LocationSig Location, InputSig<Location> Input> {
 
     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.
-     */
     cached
-    private module ImpliesTC<baseGuardValueSig/2 baseGuardValue> {
+    private module Cached {
       /**
-       * Holds if `tgtGuard` evaluating to `tgtVal` implies that `guard`
-       * evaluates to `v`.
+       * Calculates the transitive closure of all the guard implication steps
+       * starting from a given set of base cases.
        */
-      pragma[nomagic]
       cached
-      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
-          WrapperGuard::wrapperImpliesStep(g0, v0, guard, v)
-        )
-        or
-        exists(Guard g0, GuardValue v0 |
-          guardControls(g0, v0, tgtGuard, tgtVal) and
-          additionalImpliesStep(g0, v0, guard, v)
-        )
+      module ImpliesTC<baseGuardValueSig/2 baseGuardValue> {
+        /**
+         * Holds if `tgtGuard` evaluating to `tgtVal` implies that `guard`
+         * evaluates to `v`.
+         */
+        pragma[nomagic]
+        cached
+        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
+            WrapperGuard::wrapperImpliesStep(g0, 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]
+        cached
+        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)
+          )
+        }
       }
 
       /**
-       * Holds if `tgtGuard` evaluating to `tgtVal` implies that `def`
-       * evaluates to `v`.
+       * 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.
        */
-      pragma[nomagic]
       cached
-      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)
-        )
+      predicate nullGuard(Guard guard, GuardValue v, Expr e, boolean isNull) {
+        impliesStep2(guard, v, e, any(GuardValue gv | gv.isNullness(isNull))) or
+        WrapperGuard::wrapperImpliesStep(guard, v, e, any(GuardValue gv | gv.isNullness(isNull))) or
+        additionalImpliesStep(guard, v, e, any(GuardValue gv | gv.isNullness(isNull)))
       }
     }
 
-    /**
-     * 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
-      WrapperGuard::wrapperImpliesStep(guard, v, e, any(GuardValue gv | gv.isNullness(isNull))) or
-      additionalImpliesStep(guard, v, e, any(GuardValue gv | gv.isNullness(isNull)))
-    }
+    private import Cached
+
+    predicate nullGuard = Cached::nullGuard/4;
 
     private predicate hasAValueBranchEdge(Guard guard, GuardValue v) {
       guard.hasValueBranchEdge(_, _, v)

shared/typeinference/codeql/typeinference/internal/TypeInference.qll

@@ -731,20 +731,24 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
         IsInstantiationOfInputSig<TypeMentionTypeTree>
       {
         pragma[nomagic]
-        private predicate typeCondition(Type type, TypeAbstraction abs, TypeMentionTypeTree lhs) {
-          conditionSatisfiesConstraint(abs, lhs, _) and type = resolveTypeMentionRoot(lhs)
+        private predicate typeCondition(
+          Type type, TypeAbstraction abs, TypeMentionTypeTree condition
+        ) {
+          conditionSatisfiesConstraint(abs, condition, _) and
+          type = resolveTypeMentionRoot(condition)
         }
 
         pragma[nomagic]
-        private predicate typeConstraint(Type type, TypeMentionTypeTree rhs) {
-          conditionSatisfiesConstraint(_, _, rhs) and type = resolveTypeMentionRoot(rhs)
+        private predicate typeConstraint(Type type, TypeMentionTypeTree constraint) {
+          conditionSatisfiesConstraint(_, _, constraint) and
+          type = resolveTypeMentionRoot(constraint)
         }
 
         predicate potentialInstantiationOf(
-          TypeMentionTypeTree condition, TypeAbstraction abs, TypeMention constraint
+          TypeMentionTypeTree constraint, TypeAbstraction abs, TypeMention condition
         ) {
           exists(Type type |
-            typeConstraint(type, condition) and typeCondition(type, abs, constraint)
+            typeConstraint(type, constraint) and typeCondition(type, abs, condition)
           )
         }
       }
@@ -761,20 +765,20 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
         constraint.resolveTypeAt(path) = t
         or
         // recursive case
-        exists(TypeAbstraction midAbs, TypeMention midSup, TypeMention midSub |
-          conditionSatisfiesConstraint(abs, condition, midSup) and
-          // NOTE: `midAbs` describe the free type variables in `midSub`, hence
+        exists(TypeAbstraction midAbs, TypeMention midConstraint, TypeMention midCondition |
+          conditionSatisfiesConstraint(abs, condition, midConstraint) and
+          // NOTE: `midAbs` describe the free type variables in `midCondition`, hence
           // we use that for instantiation check.
-          IsInstantiationOf<TypeMentionTypeTree, IsInstantiationOfInput>::isInstantiationOf(midSup,
-            midAbs, midSub)
+          IsInstantiationOf<TypeMentionTypeTree, IsInstantiationOfInput>::isInstantiationOf(midConstraint,
+            midAbs, midCondition)
         |
-          conditionSatisfiesConstraintTypeAt(midAbs, midSub, constraint, path, t) and
+          conditionSatisfiesConstraintTypeAt(midAbs, midCondition, constraint, path, t) and
           not t = midAbs.getATypeParameter()
           or
           exists(TypePath prefix, TypePath suffix, TypeParameter tp |
             tp = midAbs.getATypeParameter() and
-            conditionSatisfiesConstraintTypeAt(midAbs, midSub, constraint, prefix, tp) and
-            instantiatesWith(midSup, midSub, tp, suffix, t) and
+            conditionSatisfiesConstraintTypeAt(midAbs, midCondition, constraint, prefix, tp) and
+            instantiatesWith(midConstraint, midCondition, tp, suffix, t) and
             path = prefix.append(suffix)
           )
         )
@@ -949,23 +953,24 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
        */
       pragma[nomagic]
       private predicate hasConstraintMention(
-        HasTypeTree tt, TypeAbstraction abs, TypeMention sub, Type constraint,
+        HasTypeTree tt, TypeAbstraction abs, TypeMention condition, Type constraint,
         TypeMention constraintMention
       ) {
         exists(Type type | hasTypeConstraint(tt, type, constraint) |
           not exists(countConstraintImplementations(type, constraint)) and
-          conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, _, _) and
-          resolveTypeMentionRoot(sub) = abs.getATypeParameter() and
+          conditionSatisfiesConstraintTypeAt(abs, condition, constraintMention, _, _) and
+          resolveTypeMentionRoot(condition) = abs.getATypeParameter() and
           constraint = resolveTypeMentionRoot(constraintMention)
           or
           countConstraintImplementations(type, constraint) > 0 and
-          rootTypesSatisfaction(type, constraint, abs, sub, constraintMention) and
+          rootTypesSatisfaction(type, constraint, abs, condition, constraintMention) and
           // When there are multiple ways the type could implement the
           // constraint we need to find the right implementation, which is the
           // one where the type instantiates the precondition.
           if multipleConstraintImplementations(type, constraint)
           then
-            IsInstantiationOf<HasTypeTree, IsInstantiationOfInput>::isInstantiationOf(tt, abs, sub)
+            IsInstantiationOf<HasTypeTree, IsInstantiationOfInput>::isInstantiationOf(tt, abs,
+              condition)
           else any()
         )
       }