Merge pull request #20076 from paldepind/rust/type-inference-cleanup-join

Rust: Type inference refactor and improve join orders

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

@@ -796,6 +796,14 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
           )
       }
 
+      /**
+       * Holds if there is multiple ways in which a type with `conditionRoot` at
+       * the root can satisfy a constraint with `constraintRoot` at the root.
+       */
+      predicate multipleConstraintImplementations(Type conditionRoot, Type constraintRoot) {
+        countConstraintImplementations(conditionRoot, constraintRoot) > 1
+      }
+
       /**
        * Holds if `baseMention` is a (transitive) base type mention of `sub`,
        * and `t` is mentioned (implicitly) at `path` inside `baseMention`. For
@@ -902,14 +910,20 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
     {
       private import Input
 
+      /** Holds if the type tree has the type `type` and should satisfy `constraint`. */
+      pragma[nomagic]
+      private predicate hasTypeConstraint(HasTypeTree term, Type type, Type constraint) {
+        type = term.getTypeAt(TypePath::nil()) and
+        relevantConstraint(term, constraint)
+      }
+
       private module IsInstantiationOfInput implements IsInstantiationOfInputSig<HasTypeTree> {
         predicate potentialInstantiationOf(HasTypeTree tt, TypeAbstraction abs, TypeMention cond) {
           exists(Type constraint, Type type |
-            type = tt.getTypeAt(TypePath::nil()) and
-            relevantConstraint(tt, constraint) and
+            hasTypeConstraint(tt, type, constraint) and
             rootTypesSatisfaction(type, constraint, abs, cond, _) and
             // We only need to check instantiations where there are multiple candidates.
-            countConstraintImplementations(type, constraint) > 1
+            multipleConstraintImplementations(type, constraint)
           )
         }
 
@@ -918,13 +932,6 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
         }
       }
 
-      /** Holds if the type tree has the type `type` and should satisfy `constraint`. */
-      pragma[nomagic]
-      private predicate hasTypeConstraint(HasTypeTree term, Type type, Type constraint) {
-        type = term.getTypeAt(TypePath::nil()) and
-        relevantConstraint(term, constraint)
-      }
-
       /**
        * Holds if `tt` satisfies `constraint` through `abs`, `sub`, and `constraintMention`.
        */
@@ -944,7 +951,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
           // 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 countConstraintImplementations(type, constraint) > 1
+          if multipleConstraintImplementations(type, constraint)
           then
             IsInstantiationOf<HasTypeTree, IsInstantiationOfInput>::isInstantiationOf(tt, abs, sub)
           else any()
@@ -989,7 +996,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
           path = prefix0.append(suffix)
         )
         or
-        tt.getTypeAt(TypePath::nil()) = constraint and
+        hasTypeConstraint(tt, constraint, constraint) and
         t = tt.getTypeAt(path)
       }
     }
@@ -1229,11 +1236,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
         predicate relevantAccessConstraint(
           Access a, Declaration target, AccessPosition apos, TypePath path, Type constraint
         ) {
-          exists(DeclarationPosition dpos |
-            accessDeclarationPositionMatch(apos, dpos) and
-            target = a.getTarget() and
-            typeParameterConstraintHasTypeParameter(target, dpos, path, _, constraint, _, _)
-          )
+          target = a.getTarget() and
+          typeParameterConstraintHasTypeParameter(target, apos, path, constraint, _, _)
         }
 
         private newtype TRelevantAccess =
@@ -1276,12 +1280,11 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
         }
 
         predicate satisfiesConstraintType(
-          Access a, AccessPosition apos, TypePath prefix, Type constraint, TypePath path, Type t
+          Access a, Declaration target, AccessPosition apos, TypePath prefix, Type constraint,
+          TypePath path, Type t
         ) {
-          exists(RelevantAccess at | at = MkRelevantAccess(a, _, apos, prefix) |
-            SatisfiesConstraint<RelevantAccess, SatisfiesConstraintInput>::satisfiesConstraintType(at,
-              constraint, path, t)
-          )
+          SatisfiesConstraint<RelevantAccess, SatisfiesConstraintInput>::satisfiesConstraintType(MkRelevantAccess(a,
+              target, apos, prefix), constraint, path, t)
         }
       }
 
@@ -1370,37 +1373,38 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
       }
 
       /**
-       * Holds if `tp1` and `tp2` are distinct type parameters of `target`, the
-       * declared type at `dpos` mentions `tp1` at `path1`, `tp1` has a base
-       * type mention of type `constraint` that mentions `tp2` at the path
-       * `path2`.
+       * Holds if the declared type of `target` contains a type parameter at
+       * `apos` and `pathToConstrained` that must satisfy `constraint` and `tp`
+       * occurs at `pathToTp` in `constraint`.
        *
-       * For this example
+       * For example, in
        * ```csharp
        * interface IFoo<A> { }
        * T1 M<T1, T2>(T2 item) where T2 : IFoo<T1> { }
        * ```
-       * with the method declaration being the target and the for the first
-       * parameter position, we have the following
-       * - `path1 = ""`,
-       * - `tp1 = T2`,
+       * with the method declaration being the target and with `apos`
+       * corresponding to `item`, we have the following
+       * - `pathToConstrained = ""`,
+       * - `tp = T1`,
        * - `constraint = IFoo`,
-       * - `path2 = "A"`, and
-       * - `tp2 = T1`.
+       * - `pathToTp = "A"`.
        */
       pragma[nomagic]
       private predicate typeParameterConstraintHasTypeParameter(
-        Declaration target, DeclarationPosition dpos, TypePath path1, TypeParameter tp1,
-        Type constraint, TypePath path2, TypeParameter tp2
+        Declaration target, AccessPosition apos, TypePath pathToConstrained, Type constraint,
+        TypePath pathToTp, TypeParameter tp
       ) {
-        tp1 = target.getTypeParameter(_) and
-        tp2 = target.getTypeParameter(_) and
-        tp1 != tp2 and
-        tp1 = target.getDeclaredType(dpos, path1) and
-        exists(TypeMention tm |
-          tm = getATypeParameterConstraint(tp1) and
-          tm.resolveTypeAt(path2) = tp2 and
-          constraint = resolveTypeMentionRoot(tm)
+        exists(DeclarationPosition dpos, TypeParameter constrainedTp |
+          accessDeclarationPositionMatch(apos, dpos) and
+          constrainedTp = target.getTypeParameter(_) and
+          tp = target.getTypeParameter(_) and
+          constrainedTp != tp and
+          constrainedTp = target.getDeclaredType(dpos, pathToConstrained) and
+          exists(TypeMention tm |
+            tm = getATypeParameterConstraint(constrainedTp) and
+            tm.resolveTypeAt(pathToTp) = tp and
+            constraint = resolveTypeMentionRoot(tm)
+          )
         )
       }
 
@@ -1409,15 +1413,9 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
         Access a, Declaration target, TypePath path, Type t, TypeParameter tp
       ) {
         not exists(getTypeArgument(a, target, tp, _)) and
-        target = a.getTarget() and
-        exists(
-          Type constraint, AccessPosition apos, DeclarationPosition dpos, TypePath pathToTp,
-          TypePath pathToTp2
-        |
-          accessDeclarationPositionMatch(apos, dpos) and
-          typeParameterConstraintHasTypeParameter(target, dpos, pathToTp2, _, constraint, pathToTp,
-            tp) and
-          AccessConstraint::satisfiesConstraintType(a, apos, pathToTp2, constraint,
+        exists(Type constraint, AccessPosition apos, TypePath pathToTp, TypePath pathToTp2 |
+          typeParameterConstraintHasTypeParameter(target, apos, pathToTp2, constraint, pathToTp, tp) and
+          AccessConstraint::satisfiesConstraintType(a, target, apos, pathToTp2, constraint,
             pathToTp.appendInverse(path), t)
         )
       }