From 65ca8849f2f2554a56cc05182f4d2a501dbb0c06 Mon Sep 17 00:00:00 2001 From: Tom Hvitved Date: 2026年1月12日 14:25:36 +0100 Subject: [PATCH] Type inference: Disable universal conditions --- .../typeinference/BlanketImplementation.qll | 2 - .../internal/typeinference/TypeInference.qll | 8 ---- .../test/library-tests/type-inference/main.rs | 2 +- .../type-inference/type-inference.expected | 2 - .../typeinference/internal/TypeInference.qll | 46 ++++++++----------- 5 files changed, 20 insertions(+), 40 deletions(-) diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll b/rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll index 1d2eda61ddb4..fee912dc8bc3 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll +++ b/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 = diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll b/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll index 9ad964854cf5..c4a76ad68025 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll +++ b/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll @@ -2193,8 +2193,6 @@ private module MethodResolution { exists(mc) and constraint.(TraitType).getTrait() instanceof DerefTrait } - - predicate useUniversalConditions() { none() } } private module MethodCallSatisfiesDerefConstraint = @@ -3566,8 +3564,6 @@ private module AwaitSatisfiesConstraintInput implements SatisfiesConstraintInput exists(term) and constraint.(TraitType).getTrait() instanceof FutureTrait } - - predicate useUniversalConditions() { none() } } pragma[nomagic] @@ -3764,8 +3760,6 @@ private module ForIterableSatisfiesConstraintInput implements t instanceof IntoIteratorTrait ) } - - predicate useUniversalConditions() { none() } } pragma[nomagic] @@ -3817,8 +3811,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`. */ diff --git a/rust/ql/test/library-tests/type-inference/main.rs b/rust/ql/test/library-tests/type-inference/main.rs index a7efa447647a..5134b26b04eb 100644 --- a/rust/ql/test/library-tests/type-inference/main.rs +++ b/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 - let j = convert_to(thing); // $ type=j:S1 + let j = convert_to(thing); // $ $ MISSING: type=j:S1 -- the blanket implementation `impl> ConvertTo for T` is currently not included in the constraint analysis } } diff --git a/rust/ql/test/library-tests/type-inference/type-inference.expected b/rust/ql/test/library-tests/type-inference/type-inference.expected index 197ce9ae47fb..c5f797efd2f1 100644 --- a/rust/ql/test/library-tests/type-inference/type-inference.expected +++ b/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] | diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll index 05a8d31ef879..5295048623e1 100644 --- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll +++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll @@ -841,15 +841,6 @@ module Make1 Input1> { signature module SatisfiesConstraintInputSig { /** 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 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 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

AltStyle によって変換されたページ (->オリジナル) /