Shared: Generalize typeConstraintBaseTypeMatch

Author: hvitved

rust/ql/test/library-tests/type-inference/main.rs

@@ -469,7 +469,7 @@ mod method_non_parametric_trait_impl {
         let i = thing.convert_to(); // $ type=i:S1 target=T::convert_to
         let j = convert_to(thing); // $ target=convert_to $ MISSING: type=j:S1 -- the blanket implementation `impl<T: MyTrait<S1>> ConvertTo<S1> for T` is currently not included in the constraint analysis
 
-        let x = call_trait_m1_trait2_m3(MyThing { a: S2 }); // $ target=call_trait_m1_trait2_m3 $ MISSING: type=x:S1
+        let x = call_trait_m1_trait2_m3(MyThing { a: S2 }); // $ target=call_trait_m1_trait2_m3 type=x:S1
     }
 }
 

rust/ql/test/library-tests/type-inference/type-inference.expected

@@ -8371,6 +8371,8 @@ inferType
 | main.rs:469:17:469:34 | thing.convert_to() |  | main.rs:249:5:250:14 | S1 |
 | main.rs:470:28:470:32 | thing |  | main.rs:238:5:241:5 | MyThing |
 | main.rs:470:28:470:32 | thing | A | main.rs:249:5:250:14 | S1 |
+| main.rs:472:13:472:13 | x |  | main.rs:249:5:250:14 | S1 |
+| main.rs:472:17:472:58 | call_trait_m1_trait2_m3(...) |  | main.rs:249:5:250:14 | S1 |
 | main.rs:472:41:472:57 | MyThing {...} |  | main.rs:238:5:241:5 | MyThing |
 | main.rs:472:41:472:57 | MyThing {...} | A | main.rs:251:5:252:14 | S2 |
 | main.rs:472:54:472:55 | S2 |  | main.rs:251:5:252:14 | S2 |

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

@@ -1346,6 +1346,14 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
     module MatchingWithEnvironment<MatchingWithEnvironmentInputSig Input> {
       private import Input
 
+      pragma[nomagic]
+      private TypeParameter getDeclTypeParameter(Declaration decl, TypeArgumentPosition tapos) {
+        exists(TypeParameterPosition tppos |
+          result = decl.getTypeParameter(tppos) and
+          typeArgumentParameterPositionMatch(tapos, tppos)
+        )
+      }
+
       /**
        * Gets the type of the type argument at `path` in `a` that corresponds to
        * the type parameter `tp` in `target`, if any.
@@ -1356,11 +1364,11 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
        */
       bindingset[a, target]
       pragma[inline_late]
-      private Type getTypeArgument(Access a, Declaration target, TypeParameter tp, TypePath path) {
-        exists(TypeArgumentPosition tapos, TypeParameterPosition tppos |
+      Type getTypeArgument(Access a, Declaration target, TypeParameter tp, TypePath path) {
+        exists(TypeArgumentPosition tapos |
           result = a.getTypeArgument(tapos, path) and
-          tp = target.getTypeParameter(tppos) and
-          typeArgumentParameterPositionMatch(tapos, tppos)
+          tp = getDeclTypeParameter(target, tapos) and
+          not isPseudoType(result)
         )
       }
 
@@ -1526,42 +1534,35 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
 
       private module AccessConstraint {
         private predicate relevantAccessConstraint(
-          Access a, AccessEnvironment e, Declaration target, AccessPosition apos, TypePath path,
+          Access a, AccessEnvironment e, Declaration target, TypeParameter constrainedTp,
           TypeMention constraint
         ) {
           target = a.getTarget(e) and
-          typeParameterHasConstraint(target, apos, _, path, constraint)
+          typeParameterHasConstraint(target, constrainedTp, constraint)
         }
 
         private newtype TRelevantAccess =
-          MkRelevantAccess(Access a, AccessPosition apos, AccessEnvironment e, TypePath path) {
-            relevantAccessConstraint(a, e, _, apos, path, _)
+          MkRelevantAccess(Access a, AccessEnvironment e, TypeParameter constrainedTp) {
+            relevantAccessConstraint(a, e, _, constrainedTp, _)
           }
 
-        /**
-         * If the access `a` for `apos`, environment `e`, and `path` has an inferred type
-         * which type inference requires to satisfy some constraint.
-         */
         private class RelevantAccess extends MkRelevantAccess {
           Access a;
-          AccessPosition apos;
           AccessEnvironment e;
-          TypePath path;
+          TypeParameter constrainedTp;
 
-          RelevantAccess() { this = MkRelevantAccess(a, apos, e, path) }
+          RelevantAccess() { this = MkRelevantAccess(a, e, constrainedTp) }
 
           pragma[nomagic]
-          Type getTypeAt(TypePath suffix) {
-            result = a.getInferredType(e, apos, path.appendInverse(suffix))
-          }
+          Type getTypeAt(TypePath path) { typeMatch(a, e, _, path, result, constrainedTp) }
 
           /** Gets the constraint that this relevant access should satisfy. */
           TypeMention getConstraint(Declaration target) {
-            relevantAccessConstraint(a, e, target, apos, path, result)
+            relevantAccessConstraint(a, e, target, constrainedTp, result)
           }
 
           string toString() {
-            result = a.toString() + ", " + apos.toString() + ", " + path.toString()
+            result = a.toString() + ", " + e.toString() + ", " + constrainedTp.toString()
           }
 
           Location getLocation() { result = a.getLocation() }
@@ -1577,7 +1578,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
           class TypeMatchingContext = Access;
 
           TypeMatchingContext getTypeMatchingContext(RelevantAccess at) {
-            at = MkRelevantAccess(result, _, _, _)
+            at = MkRelevantAccess(result, _, _)
           }
 
           pragma[nomagic]
@@ -1591,41 +1592,32 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
             SatisfiesTypeParameterConstraintInput>;
 
         pragma[nomagic]
-        predicate satisfiesConstraintAtTypeParameter(
+        predicate argSatisfiesConstraintAtTypeParameter(
           Access a, AccessEnvironment e, Declaration target, AccessPosition apos, TypePath prefix,
           TypeMention constraint, TypePath pathToTypeParamInConstraint,
           TypePath pathToTypeParamInSub
         ) {
-          exists(RelevantAccess ra |
-            ra = MkRelevantAccess(a, apos, e, prefix) and
+          exists(RelevantAccess ra, TypeParameter constrainedTp |
+            ra = MkRelevantAccess(a, e, constrainedTp) and
+            relevantAccessConstraint(a, e, target, constrainedTp, constraint) and
             SatisfiesTypeParameterConstraint::satisfiesConstraintAtTypeParameter(ra, constraint,
               pathToTypeParamInConstraint, pathToTypeParamInSub) and
-            constraint = ra.getConstraint(target)
+            exists(DeclarationPosition dpos |
+              accessDeclarationPositionMatch(apos, dpos) and
+              constrainedTp = target.getDeclaredType(dpos, prefix)
+            )
           )
         }
 
         pragma[nomagic]
         predicate satisfiesConstraint(
-          Access a, AccessEnvironment e, Declaration target, AccessPosition apos, TypePath prefix,
+          Access a, AccessEnvironment e, Declaration target, TypeParameter constrainedTp,
           TypeMention constraint, TypePath path, Type t
         ) {
           exists(RelevantAccess ra |
-            ra = MkRelevantAccess(a, apos, e, prefix) and
-            SatisfiesTypeParameterConstraint::satisfiesConstraint(ra, constraint, path, t) and
-            constraint = ra.getConstraint(target)
-          )
-        }
-
-        pragma[nomagic]
-        predicate satisfiesConstraintThrough(
-          Access a, AccessEnvironment e, Declaration target, AccessPosition apos, TypePath prefix,
-          TypeAbstraction abs, TypeMention constraint, TypePath path, Type t
-        ) {
-          exists(RelevantAccess ra |
-            ra = MkRelevantAccess(a, apos, e, prefix) and
-            SatisfiesTypeParameterConstraint::satisfiesConstraintThrough(ra, abs, constraint, path,
-              t) and
-            constraint = ra.getConstraint(target)
+            ra = MkRelevantAccess(a, e, constrainedTp) and
+            relevantAccessConstraint(a, e, target, constrainedTp, constraint) and
+            SatisfiesTypeParameterConstraint::satisfiesConstraint(ra, constraint, path, t)
           )
         }
       }
@@ -1650,55 +1642,48 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
        */
       pragma[nomagic]
       private predicate typeParameterHasConstraint(
-        Declaration target, AccessPosition apos, TypeParameter constrainedTp,
-        TypePath pathToConstrained, TypeMention constraint
+        Declaration target, TypeParameter constrainedTp, TypeMention constraint
       ) {
-        exists(DeclarationPosition dpos |
-          accessDeclarationPositionMatch(apos, dpos) and
-          constrainedTp = target.getTypeParameter(_) and
-          constrainedTp = target.getDeclaredType(dpos, pathToConstrained) and
-          constraint = getATypeParameterConstraint(constrainedTp, target)
-        )
+        constrainedTp = target.getTypeParameter(_) and
+        constraint = getATypeParameterConstraint(constrainedTp, target)
       }
 
       /**
-       * 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`.
+       * Holds if the declared type of `target` contains type parameter `constrainedTp`
+       * that must satisfy `constraint` and `tp` occurs at `pathToTp` in `constraint`.
        *
        * 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 with `apos`
-       * corresponding to `item`, we have the following
-       * - `pathToConstrained = ""`,
-       * - `tp = T1`,
+       *
+       * with the method declaration being the target, we have the following
+       * - `constrainedTp = T2`,
        * - `constraint = IFoo`,
+       * - `tp = T1`, and
        * - `pathToTp = "A"`.
        */
       pragma[nomagic]
       private predicate typeParameterConstraintHasTypeParameter(
-        Declaration target, AccessPosition apos, TypePath pathToConstrained, TypeMention constraint,
-        TypePath pathToTp, TypeParameter tp
+        Declaration target, TypeParameter constrainedTp, TypeMention constraint, TypePath pathToTp,
+        TypeParameter tp
       ) {
-        exists(TypeParameter constrainedTp |
-          typeParameterHasConstraint(target, apos, constrainedTp, pathToConstrained, constraint) and
-          tp = target.getTypeParameter(_) and
-          tp = constraint.getTypeAt(pathToTp) and
-          constrainedTp != tp
-        )
+        typeParameterHasConstraint(target, constrainedTp, constraint) and
+        tp = target.getTypeParameter(_) and
+        tp = constraint.getTypeAt(pathToTp) and
+        constrainedTp != tp
       }
 
       pragma[nomagic]
       private predicate typeConstraintBaseTypeMatch(
         Access a, AccessEnvironment e, Declaration target, TypePath path, Type t, TypeParameter tp
       ) {
         not exists(getTypeArgument(a, target, tp, _)) and
-        exists(TypeMention constraint, AccessPosition apos, TypePath pathToTp, TypePath pathToTp2 |
-          typeParameterConstraintHasTypeParameter(target, apos, pathToTp2, constraint, pathToTp, tp) and
-          AccessConstraint::satisfiesConstraint(a, e, target, apos, pathToTp2, constraint,
+        exists(TypeMention constraint, TypeParameter constrainedTp, TypePath pathToTp |
+          typeParameterConstraintHasTypeParameter(target, constrainedTp, constraint, pathToTp, tp) and
+          AccessConstraint::satisfiesConstraint(a, e, target, constrainedTp, constraint,
             pathToTp.appendInverse(path), t)
         )
       }
@@ -1781,7 +1766,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
           Declaration target, TypePath prefix, TypeMention constraint,
           TypePath pathToTypeParamInConstraint, TypePath pathToTypeParamInSub
         |
-          AccessConstraint::satisfiesConstraintAtTypeParameter(a, e, target, apos, prefix,
+          AccessConstraint::argSatisfiesConstraintAtTypeParameter(a, e, target, apos, prefix,
             constraint, pathToTypeParamInConstraint, pathToTypeParamInSub)
         |
           exists(TypePath suffix |
@@ -1847,7 +1832,12 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
              */
 
             typeMatch(a, e, target, suffix, result, tp) and
-            typeParameterConstraintHasTypeParameter(target, apos, _, constraint, pathToTp, tp) and
+            exists(TypeParameter constrainedTp, DeclarationPosition dpos |
+              typeParameterConstraintHasTypeParameter(target, constrainedTp, constraint, pathToTp,
+                tp) and
+              accessDeclarationPositionMatch(apos, dpos) and
+              constrainedTp = target.getDeclaredType(dpos, _)
+            ) and
             pathToTp = pathToTypeParamInConstraint.appendInverse(mid) and
             path = prefix.append(pathToTypeParamInSub.append(mid).append(suffix))
           )