Skip to content

Commit 0db62b2

Browse files
hvitvedhvitved
committed
Type inference: Fix bad join
Before ``` Pipeline standard for TypeInference::M2::SatisfiesConstraintWithTypeMatching<TypeInference::FunctionCallMatching::AccessConstraint::RelevantAccess,TypeMention::TypeMention,TypeInference::FunctionCallMatching::AccessConstraint::SatisfiesTypeParameterConstraintInput>::TermIsInstantiationOfCondition::typeParametersHaveEqualInstantiationToIndex/4#dde26112@d5eb7x9q was evaluated in 471 iterations totaling 24306ms (delta sizes total: 42097188). 5676156578 ~1% {7} r1 = JOIN `TypeInference::M2::SatisfiesConstraintWithTypeMatching<TypeInference::FunctionCallMatching::AccessConstraint::RelevantAccess,TypeMention::TypeMention,TypeInference::FunctionCallMatching::AccessConstraint::SatisfiesTypeParameterConstraintInput>::TermIsInstantiationOfCondition::typeParametersHaveEqualInstantiationToIndex/4#dde26112#prev_delta` WITH `TypeInference::M2::SatisfiesConstraintWithTypeMatching<TypeInference::FunctionCallMatching::AccessConstraint::RelevantAccess,TypeMention::TypeMention,TypeInference::FunctionCallMatching::AccessConstraint::SatisfiesTypeParameterConstraintInput>::TermIsInstantiationOfCondition::typeParametersEqual/4#a276e5d4#prev` ON FIRST 3 OUTPUT Lhs.0, Lhs.1, Lhs.2, Rhs.3, _, Lhs.3, _ {5} | REWRITE WITH Tmp.4 := 1, Out.4 := (Tmp.4 + In.5), Tmp.6 := 0, TEST Out.4 != Tmp.6 KEEPING 5 5676156578 ~1% {5} | SCAN OUTPUT In.1, In.4, In.3, In.0, In.2 41691564 ~1% {4} | JOIN WITH `TypeInference::M2::SatisfiesConstraintWithTypeMatching<TypeInference::AssocFunctionResolution::ArgSatisfiesBlanketLikeConstraint::ArgumentTypeAndBlanketOffset,TypeMention::TypeMention,TypeInference::AssocFunctionResolution::ArgSatisfiesBlanketLikeConstraint::SatisfiesBlanketConstraint::Inp>::TermIsInstantiationOfCondition::getNthTypeParameter/2#40c66343` ON FIRST 3 OUTPUT Lhs.3, Lhs.0, Lhs.4, Lhs.1 42097188 ~2% {4} r2 = SCAN `TypeInference::M2::SatisfiesConstraintWithTypeMatching<TypeInference::FunctionCallMatching::AccessConstraint::RelevantAccess,TypeMention::TypeMention,TypeInference::FunctionCallMatching::AccessConstraint::SatisfiesTypeParameterConstraintInput>::TermIsInstantiationOfCondition::typeParametersEqual/4#a276e5d4#prev_delta` OUTPUT In.1, In.3, In.0, In.2 42097188 ~1% {5} r3 = JOIN r2 WITH `TypeInference::M2::SatisfiesConstraintWithTypeMatching<TypeInference::AssocFunctionResolution::ArgSatisfiesBlanketLikeConstraint::ArgumentTypeAndBlanketOffset,TypeMention::TypeMention,TypeInference::AssocFunctionResolution::ArgSatisfiesBlanketLikeConstraint::SatisfiesBlanketConstraint::Inp>::TermIsInstantiationOfCondition::getNthTypeParameter/2#40c66343_021#join_rhs` ON FIRST 2 OUTPUT Lhs.2, Lhs.0, Lhs.3, Rhs.2, _ {4} | REWRITE WITH Tmp.4 := 0, TEST InOut.3 != Tmp.4 KEEPING 4 41691564 ~1% {5} | SCAN OUTPUT In.0, In.1, In.2, _, In.3 41691564 ~1% {5} | REWRITE WITH Tmp.3 := 1, Out.3 := (InOut.4 - Tmp.3) 0 ~0% {4} | JOIN WITH `TypeInference::M2::SatisfiesConstraintWithTypeMatching<TypeInference::FunctionCallMatching::AccessConstraint::RelevantAccess,TypeMention::TypeMention,TypeInference::FunctionCallMatching::AccessConstraint::SatisfiesTypeParameterConstraintInput>::TermIsInstantiationOfCondition::typeParametersHaveEqualInstantiationToIndex/4#dde26112#prev` ON FIRST 4 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.4 42097188 ~0% {6} r4 = JOIN r2 WITH `TypeInference::M2::SatisfiesConstraintWithTypeMatching<TypeInference::AssocFunctionResolution::ArgSatisfiesBlanketLikeConstraint::ArgumentTypeAndBlanketOffset,TypeMention::TypeMention,TypeInference::AssocFunctionResolution::ArgSatisfiesBlanketLikeConstraint::SatisfiesBlanketConstraint::Inp>::TermIsInstantiationOfCondition::getNthTypeParameter/2#40c66343_021#join_rhs` ON FIRST 2 OUTPUT Lhs.2, Lhs.0, Lhs.3, Lhs.1, Rhs.2, _ {5} | REWRITE WITH Tmp.5 := 0, TEST InOut.4 = Tmp.5 KEEPING 5 405624 ~1% {5} | SCAN OUTPUT In.1, _, In.3, In.0, In.2 405624 ~1% {5} | REWRITE WITH Out.1 := 0 405624 ~0% {4} | JOIN WITH `TypeInference::M2::SatisfiesConstraintWithTypeMatching<TypeInference::AssocFunctionResolution::ArgSatisfiesBlanketLikeConstraint::ArgumentTypeAndBlanketOffset,TypeMention::TypeMention,TypeInference::AssocFunctionResolution::ArgSatisfiesBlanketLikeConstraint::SatisfiesBlanketConstraint::Inp>::TermIsInstantiationOfCondition::getNthTypeParameter/2#40c66343` ON FIRST 3 OUTPUT Lhs.3, Lhs.0, Lhs.4, _ 405624 ~1% {4} | REWRITE WITH Out.3 := 0 42097188 ~1% {4} r5 = r1 UNION r3 UNION r4 42097188 ~1% {4} | AND NOT `TypeInference::M2::SatisfiesConstraintWithTypeMatching<TypeInference::FunctionCallMatching::AccessConstraint::RelevantAccess,TypeMention::TypeMention,TypeInference::FunctionCallMatching::AccessConstraint::SatisfiesTypeParameterConstraintInput>::TermIsInstantiationOfCondition::typeParametersHaveEqualInstantiationToIndex/4#dde26112#prev`(FIRST 4) return r5 ``` After ``` Pipeline standard for TypeInference::M2::SatisfiesConstraintWithTypeMatching<TypeInference::FunctionCallMatching::AccessConstraint::RelevantAccess,TypeMention::TypeMention,TypeInference::FunctionCallMatching::AccessConstraint::SatisfiesTypeParameterConstraintInput>::TermIsInstantiationOfCondition::typeParametersHaveEqualInstantiationToIndex/4#dde26112@96df1x2u was evaluated in 471 iterations totaling 4058ms (delta sizes total: 42097188). 42097188 ~0% {4} r1 = SCAN `TypeInference::M2::SatisfiesConstraintWithTypeMatching<TypeInference::FunctionCallMatching::AccessConstraint::RelevantAccess,TypeMention::TypeMention,TypeInference::FunctionCallMatching::AccessConstraint::SatisfiesTypeParameterConstraintInput>::TermIsInstantiationOfCondition::typeParametersEqual/5#ddfcf430#prev_delta` OUTPUT In.3, In.0, In.1, In.2 405624 ~0% {4} | JOIN WITH const_0 ON FIRST 1 OUTPUT Lhs.1, Lhs.2, Lhs.3, _ 405624 ~1% {4} | REWRITE WITH Out.3 := 0 42097188 ~1% {6} r2 = SCAN `TypeInference::M2::SatisfiesConstraintWithTypeMatching<TypeInference::FunctionCallMatching::AccessConstraint::RelevantAccess,TypeMention::TypeMention,TypeInference::FunctionCallMatching::AccessConstraint::SatisfiesTypeParameterConstraintInput>::TermIsInstantiationOfCondition::typeParametersHaveEqualInstantiationToIndex/4#dde26112#prev_delta` OUTPUT In.0, In.1, In.2, _, In.3, _ 42097188 ~1% {4} | REWRITE WITH Tmp.3 := 1, Out.3 := (Tmp.3 + In.4), Tmp.5 := 0, TEST Out.3 != Tmp.5 KEEPING 4 41691564 ~1% {4} | JOIN WITH `TypeInference::M2::SatisfiesConstraintWithTypeMatching<TypeInference::FunctionCallMatching::AccessConstraint::RelevantAccess,TypeMention::TypeMention,TypeInference::FunctionCallMatching::AccessConstraint::SatisfiesTypeParameterConstraintInput>::TermIsInstantiationOfCondition::typeParametersEqual/5#ddfcf430#prev` ON FIRST 4 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.3 42097188 ~1% {6} r3 = SCAN `TypeInference::M2::SatisfiesConstraintWithTypeMatching<TypeInference::FunctionCallMatching::AccessConstraint::RelevantAccess,TypeMention::TypeMention,TypeInference::FunctionCallMatching::AccessConstraint::SatisfiesTypeParameterConstraintInput>::TermIsInstantiationOfCondition::typeParametersEqual/5#ddfcf430#prev_delta` OUTPUT In.0, In.1, In.2, In.3, In.4, _ {5} | REWRITE WITH Tmp.5 := 0, TEST InOut.3 != Tmp.5 KEEPING 5 41691564 ~1% {5} | SCAN OUTPUT In.0, In.1, In.2, _, In.3 41691564 ~1% {5} | REWRITE WITH Tmp.3 := 1, Out.3 := (InOut.4 - Tmp.3) 0 ~0% {4} | JOIN WITH `TypeInference::M2::SatisfiesConstraintWithTypeMatching<TypeInference::FunctionCallMatching::AccessConstraint::RelevantAccess,TypeMention::TypeMention,TypeInference::FunctionCallMatching::AccessConstraint::SatisfiesTypeParameterConstraintInput>::TermIsInstantiationOfCondition::typeParametersHaveEqualInstantiationToIndex/4#dde26112#prev` ON FIRST 4 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.4 42097188 ~1% {4} r4 = r1 UNION r2 UNION r3 42097188 ~1% {4} | AND NOT `TypeInference::M2::SatisfiesConstraintWithTypeMatching<TypeInference::FunctionCallMatching::AccessConstraint::RelevantAccess,TypeMention::TypeMention,TypeInference::FunctionCallMatching::AccessConstraint::SatisfiesTypeParameterConstraintInput>::TermIsInstantiationOfCondition::typeParametersHaveEqualInstantiationToIndex/4#dde26112#prev`(FIRST 4) return r4 ```
1 parent 33cc887 commit 0db62b2

File tree

1 file changed

+11
-11
lines changed

1 file changed

+11
-11
lines changed

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

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -566,15 +566,17 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
566566
)
567567
}
568568

569+
pragma[nomagic]
569570
private predicate typeParametersEqual(
570-
App app, TypeAbstraction abs, Constraint constraint, TypeParameter tp
571+
App app, TypeAbstraction abs, Constraint constraint, int i
571572
) {
572-
satisfiesConcreteTypes(app, abs, constraint) and
573-
tp = getNthTypeParameter(abs, _) and
574-
(
573+
exists(TypeParameter tp |
574+
satisfiesConcreteTypes(app, abs, constraint) and
575+
tp = getNthTypeParameter(abs, i)
576+
|
575577
not exists(getNthTypeParameterPath(constraint, tp, _))
576578
or
577-
exists(int n | n = max(int i | exists(getNthTypeParameterPath(constraint, tp, i))) |
579+
exists(int n | n = max(int j | exists(getNthTypeParameterPath(constraint, tp, j))) |
578580
// If the largest index is 0, then there are no equalities to check as
579581
// the type parameter only occurs once.
580582
if n = 0 then any() else typeParametersEqualToIndex(app, abs, constraint, tp, _, n)
@@ -585,12 +587,10 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
585587
private predicate typeParametersHaveEqualInstantiationToIndex(
586588
App app, TypeAbstraction abs, Constraint constraint, int i
587589
) {
588-
exists(TypeParameter tp | tp = getNthTypeParameter(abs, i) |
589-
typeParametersEqual(app, abs, constraint, tp) and
590-
if i = 0
591-
then any()
592-
else typeParametersHaveEqualInstantiationToIndex(app, abs, constraint, i - 1)
593-
)
590+
typeParametersEqual(app, abs, constraint, i) and
591+
if i = 0
592+
then any()
593+
else typeParametersHaveEqualInstantiationToIndex(app, abs, constraint, i - 1)
594594
}
595595

596596
/**

0 commit comments

Comments
 (0)