Merge pull request github#21151 from hvitved/rust/disable-universal-conds-by-default

Type inference: Disable universal conditions by default

Author: hvitved

rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll

@@ -117,8 +117,6 @@ module SatisfiesBlanketConstraint<
     predicate relevantConstraint(ArgumentTypeAndBlanketOffset ato, Type constraint) {
       relevantConstraint(ato, _, constraint.(TraitType).getTrait())
     }
-
-    predicate useUniversalConditions() { none() }
   }
 
   private module SatisfiesBlanketConstraint =

rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll

@@ -2200,8 +2200,6 @@ private module MethodResolution {
         exists(mc) and
         constraint.(TraitType).getTrait() instanceof DerefTrait
       }
-
-      predicate useUniversalConditions() { none() }
     }
 
     private module MethodCallSatisfiesDerefConstraint =
@@ -3613,8 +3611,6 @@ private module AwaitSatisfiesConstraintInput implements SatisfiesConstraintInput
     exists(term) and
     constraint.(TraitType).getTrait() instanceof FutureTrait
   }
-
-  predicate useUniversalConditions() { none() }
 }
 
 pragma[nomagic]
@@ -3811,8 +3807,6 @@ private module ForIterableSatisfiesConstraintInput implements
       t instanceof IntoIteratorTrait
     )
   }
-
-  predicate useUniversalConditions() { none() }
 }
 
 pragma[nomagic]
@@ -3864,8 +3858,6 @@ private module InvokedClosureSatisfiesConstraintInput implements
     exists(term) and
     constraint.(TraitType).getTrait() instanceof FnOnceTrait
   }
-
-  predicate useUniversalConditions() { none() }
 }
 
 /** Gets the type of `ce` when viewed as an implementation of `FnOnce`. */

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

@@ -438,7 +438,7 @@ mod method_non_parametric_trait_impl {
 
         let thing = MyThing { a: S1 };
         let i = thing.convert_to(); // $ type=i:S1 target=T::convert_to
-        let j = convert_to(thing); // $ type=j:S1 target=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
     }
 }
 

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

@@ -7151,8 +7151,6 @@ inferType
 | main.rs:440:17:440:21 | thing |  | main.rs:224:5:227:5 | MyThing |
 | main.rs:440:17:440:21 | thing | A | main.rs:235:5:236:14 | S1 |
 | main.rs:440:17:440:34 | thing.convert_to() |  | main.rs:235:5:236:14 | S1 |
-| main.rs:441:13:441:13 | j |  | main.rs:235:5:236:14 | S1 |
-| main.rs:441:17:441:33 | convert_to(...) |  | main.rs:235:5:236:14 | S1 |
 | main.rs:441:28:441:32 | thing |  | main.rs:224:5:227:5 | MyThing |
 | main.rs:441:28:441:32 | thing | A | main.rs:235:5:236:14 | S1 |
 | main.rs:450:26:450:29 | SelfParam |  | main.rs:449:5:453:5 | Self [trait OverlappingTrait] |

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

@@ -841,15 +841,6 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
     signature module SatisfiesConstraintInputSig<HasTypeTreeSig HasTypeTree> {
       /** Holds if it is relevant to know if `term` satisfies `constraint`. */
       predicate relevantConstraint(HasTypeTree term, Type constraint);
-
-      /**
-       * Holds if constraints that are satisfied through conditions that are
-       * universally quantified type parameters should be used. Such type
-       * parameters might have type parameter constraints, and these are _not_
-       * checked. Hence using these represent a trade-off between too many
-       * constraints and too few constraints being satisfied.
-       */
-      default predicate useUniversalConditions() { any() }
     }
 
     module SatisfiesConstraint<
@@ -901,12 +892,14 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
         TypeMention constraintMention
       ) {
         exists(Type type | hasTypeConstraint(tt, type, constraint) |
-          useUniversalConditions() and // todo: remove, and instead check constraints
-          not exists(countConstraintImplementations(type, constraint)) and
-          conditionSatisfiesConstraintTypeAt(abs, condition, constraintMention, _, _) and
-          resolveTypeMentionRoot(condition) = abs.getATypeParameter() and
-          constraint = resolveTypeMentionRoot(constraintMention)
-          or
+          // TODO: Handle universal conditions properly, which means checking type parameter constraints
+          // Also remember to update logic in `hasNotConstraintMention`
+          //
+          // not exists(countConstraintImplementations(type, constraint)) and
+          // conditionSatisfiesConstraintTypeAt(abs, condition, constraintMention, _, _) and
+          // resolveTypeMentionRoot(condition) = abs.getATypeParameter() and
+          // constraint = resolveTypeMentionRoot(constraintMention)
+          // or
           countConstraintImplementations(type, constraint) > 0 and
           rootTypesSatisfaction(type, constraint, abs, condition, constraintMention) and
           // When there are multiple ways the type could implement the
@@ -936,18 +929,17 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
       pragma[nomagic]
       private predicate hasNotConstraintMention(HasTypeTree tt, Type constraint) {
         exists(Type type | hasTypeConstraint(tt, type, constraint) |
-          (
-            not useUniversalConditions()
-            or
-            exists(countConstraintImplementations(type, constraint))
-            or
-            forall(TypeAbstraction abs, TypeMention condition, TypeMention constraintMention |
-              conditionSatisfiesConstraintTypeAt(abs, condition, constraintMention, _, _) and
-              resolveTypeMentionRoot(condition) = abs.getATypeParameter()
-            |
-              not constraint = resolveTypeMentionRoot(constraintMention)
-            )
-          ) and
+          // TODO: Handle universal conditions properly, which means taking type parameter constraints into account
+          // (
+          //   exists(countConstraintImplementations(type, constraint))
+          //   or
+          //   forall(TypeAbstraction abs, TypeMention condition, TypeMention constraintMention |
+          //     conditionSatisfiesConstraintTypeAt(abs, condition, constraintMention, _, _) and
+          //     resolveTypeMentionRoot(condition) = abs.getATypeParameter()
+          //   |
+          //     not constraint = resolveTypeMentionRoot(constraintMention)
+          //   )
+          // ) and
           (
             countConstraintImplementations(type, constraint) = 0
             or