Skip to content

Commit f9915e6

Browse files
hvitvedhvitved
committed
Rust: Fix bad join in satisfiesConcreteTypesFromIndex
Before ``` Pipeline standard for TypeInference::M2::IsInstantiationOf<TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess,TypeInference::CallExprBaseMatching::AccessConstraint::IsInstantiationOfInput>::satisfiesConcreteTypesFromIndex/4#716280b9@061312x0 was evaluated in 367 iterations totaling 3484ms (delta sizes total: 563408). 66609 ~0% {3} r1 = SCAN `TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess.getTypeAt/1#dispred#3a89868c#prev_delta` OUTPUT In.1, In.2, In.0 867138261 ~1% {4} | JOIN WITH `TypeMention::TypeMention.resolveTypeAt/1#dispred#a125c821#bff#reorder_0_2_1_210#join_rhs` ON FIRST 2 OUTPUT Lhs.2, Rhs.2, Lhs.0, Lhs.1 29320 ~0% {5} | JOIN WITH `TypeInference::CallExprBaseMatching::AccessConstraint::IsInstantiationOfInput::potentialInstantiationOf/3#1239e45f#reorder_0_2_1#prev` ON FIRST 2 OUTPUT Rhs.2, Lhs.3, Lhs.0, Lhs.2, Lhs.1 {5} | AND NOT `Type::TypeAbstraction.getATypeParameter/0#dispred#030257a0`(FIRST 2) 29320 ~1% {4} | SCAN OUTPUT In.4, In.3, In.2, In.0 29320 ~0% {5} r2 = JOIN r1 WITH `TypeInference::M2::IsInstantiationOf<TypeInference::AwaitExprMatching::AccessConstraint::RelevantAccess,TypeInference::AwaitExprMatching::AccessConstraint::IsInstantiationOfInput>::getNthPath/2#8b978a80_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 29320 ~0% {5} | SCAN OUTPUT In.0, In.2, In.1, _, In.3 29320 ~0% {5} | REWRITE WITH Tmp.3 := 1, Out.3 := (InOut.4 - Tmp.3) 29296 ~1% {4} | JOIN WITH `TypeInference::M2::IsInstantiationOf<TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess,TypeInference::CallExprBaseMatching::AccessConstraint::IsInstantiationOfInput>::satisfiesConcreteTypesFromIndex/4#716280b9#prev` ON FIRST 4 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.4 29320 ~0% {6} r3 = JOIN r1 WITH `TypeInference::M2::IsInstantiationOf<TypeInference::AwaitExprMatching::AccessConstraint::RelevantAccess,TypeInference::AwaitExprMatching::AccessConstraint::IsInstantiationOfInput>::getNthPath/2#8b978a80_021#join_rhs` ON FIRST 2 OUTPUT Lhs.2, Lhs.1, Lhs.0, Lhs.3, Rhs.2, _ {5} | REWRITE WITH Tmp.5 := 0, TEST InOut.4 = Tmp.5 KEEPING 5 0 ~0% {5} | SCAN OUTPUT In.2, _, In.1, In.0, In.3 0 ~0% {5} | REWRITE WITH Out.1 := 0 0 ~0% {4} | JOIN WITH `TypeInference::M2::IsInstantiationOf<TypeInference::AwaitExprMatching::AccessConstraint::RelevantAccess,TypeInference::AwaitExprMatching::AccessConstraint::IsInstantiationOfInput>::getNthPath/2#8b978a80` ON FIRST 3 OUTPUT Lhs.3, Lhs.4, Lhs.0, _ 0 ~0% {4} | REWRITE WITH Out.3 := 0 563353 ~1% {4} r4 = SCAN `TypeInference::M2::IsInstantiationOf<TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess,TypeInference::CallExprBaseMatching::AccessConstraint::IsInstantiationOfInput>::satisfiesConcreteTypesFromIndex/4#716280b9#prev_delta` OUTPUT In.0, In.2, In.1, In.3 563353 ~1% {6} | JOIN WITH `TypeInference::CallExprBaseMatching::AccessConstraint::IsInstantiationOfInput::potentialInstantiationOf/3#1239e45f#reorder_0_2_1#prev` ON FIRST 3 OUTPUT Lhs.0, Lhs.2, Lhs.1, _, Lhs.3, _ {4} | REWRITE WITH Tmp.3 := 1, Out.3 := (Tmp.3 + In.4), Tmp.5 := 0, TEST Out.3 != Tmp.5 KEEPING 4 563353 ~0% {4} | SCAN OUTPUT In.2, In.3, In.0, In.1 258647 ~1% {5} r5 = JOIN r4 WITH `TypeInference::M2::IsInstantiationOf<TypeInference::AwaitExprMatching::AccessConstraint::RelevantAccess,TypeInference::AwaitExprMatching::AccessConstraint::IsInstantiationOfInput>::getNthPath/2#8b978a80` ON FIRST 2 OUTPUT Lhs.3, Lhs.2, Lhs.0, Lhs.1, Rhs.2 102998 ~1% {6} | JOIN WITH `Type::TypeAbstraction.getATypeParameter/0#dispred#030257a0` ON FIRST 1 OUTPUT Lhs.2, Rhs.1, Lhs.4, Lhs.1, Lhs.0, Lhs.3 52485 ~1% {6} | JOIN WITH `TypeMention::TypeMention.resolveTypeAt/1#dispred#a125c821#bff#reorder_0_2_1` ON FIRST 3 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.3, Lhs.4, Lhs.5 258647 ~0% {5} r6 = JOIN r4 WITH `TypeInference::M2::IsInstantiationOf<TypeInference::AwaitExprMatching::AccessConstraint::RelevantAccess,TypeInference::AwaitExprMatching::AccessConstraint::IsInstantiationOfInput>::getNthPath/2#8b978a80` ON FIRST 2 OUTPUT Lhs.0, Rhs.2, Lhs.2, Lhs.3, Lhs.1 259340 ~1% {6} | JOIN WITH `TypeMention::TypeMention.resolveTypeAt/1#dispred#a125c821#bff#reorder_0_2_1_021#join_rhs` ON FIRST 2 OUTPUT Lhs.2, Lhs.1, Rhs.2, Lhs.3, Lhs.0, Lhs.4 16033 ~0% {6} | JOIN WITH `TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess.getTypeAt/1#dispred#3a89868c#prev` ON FIRST 3 OUTPUT Lhs.3, Lhs.2, Lhs.0, Lhs.4, Lhs.5, Lhs.1 {6} | AND NOT `Type::TypeAbstraction.getATypeParameter/0#dispred#030257a0`(FIRST 2) 15992 ~1% {6} | SCAN OUTPUT In.3, In.1, In.5, In.2, In.0, In.4 68477 ~1% {6} r7 = r5 UNION r6 68477 ~0% {4} | JOIN WITH `TypeMention::TypeMention.resolveTypeAt/1#dispred#a125c821#bff#reorder_0_2_1` ON FIRST 3 OUTPUT Lhs.3, Lhs.4, Lhs.0, Lhs.5 465635 ~0% {3} r8 = SCAN `TypeInference::CallExprBaseMatching::AccessConstraint::IsInstantiationOfInput::potentialInstantiationOf/3#1239e45f#reorder_0_2_1#prev_delta` OUTPUT In.1, In.0, In.2 465635 ~0% {5} r9 = JOIN r8 WITH `_TypeInference::M2::IsInstantiationOf<TypeInference::AwaitExprMatching::AccessConstraint::RelevantAc__#join_rhs` ON FIRST 1 OUTPUT Lhs.0, _, Rhs.2, Lhs.1, Lhs.2 465635 ~1% {5} | REWRITE WITH Out.1 := 0 465635 ~1% {5} r10 = JOIN r9 WITH `TypeInference::M2::IsInstantiationOf<TypeInference::AwaitExprMatching::AccessConstraint::RelevantAccess,TypeInference::AwaitExprMatching::AccessConstraint::IsInstantiationOfInput>::getNthPath/2#8b978a80` ON FIRST 3 OUTPUT Lhs.4, Lhs.0, _, Lhs.2, Lhs.3 465635 ~1% {5} | REWRITE WITH Out.2 := 0 275069 ~0% {5} r11 = JOIN r8 WITH `_TypeInference::M2::IsInstantiationOf<TypeInference::AwaitExprMatching::AccessConstraint::RelevantAc__#join_rhs#1` ON FIRST 1 OUTPUT Lhs.1, Lhs.2, Lhs.0, Rhs.1, Rhs.2 0 ~0% {7} | JOIN WITH `TypeInference::M2::IsInstantiationOf<TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess,TypeInference::CallExprBaseMatching::AccessConstraint::IsInstantiationOfInput>::satisfiesConcreteTypesFromIndex/4#716280b9#prev` ON FIRST 3 OUTPUT Lhs.2, Lhs.3, Lhs.4, Lhs.0, Lhs.1, Rhs.3, _ 0 ~0% {7} | REWRITE WITH Tmp.6 := 1, Out.6 := (InOut.1 - Tmp.6), TEST Out.6 = InOut.5 0 ~0% {5} r12 = SCAN r11 OUTPUT In.4, In.0, In.1, In.2, In.3 465635 ~1% {5} r13 = r10 UNION r12 94444 ~1% {6} | JOIN WITH `Type::TypeAbstraction.getATypeParameter/0#dispred#030257a0` ON FIRST 1 OUTPUT Lhs.1, Rhs.1, Lhs.3, Lhs.2, Lhs.4, Lhs.0 6 ~20% {6} | JOIN WITH `TypeMention::TypeMention.resolveTypeAt/1#dispred#a125c821#bff#reorder_0_2_1` ON FIRST 3 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.3, Lhs.4, Lhs.5 465635 ~0% {5} r14 = JOIN r9 WITH `TypeInference::M2::IsInstantiationOf<TypeInference::AwaitExprMatching::AccessConstraint::RelevantAccess,TypeInference::AwaitExprMatching::AccessConstraint::IsInstantiationOfInput>::getNthPath/2#8b978a80` ON FIRST 3 OUTPUT Lhs.0, Lhs.2, _, Lhs.3, Lhs.4 465635 ~1% {5} | REWRITE WITH Out.2 := 0 0 ~0% {5} r15 = SCAN r11 OUTPUT In.0, In.2, In.1, In.3, In.4 465635 ~1% {5} r16 = r14 UNION r15 465635 ~0% {6} | JOIN WITH `TypeMention::TypeMention.resolveTypeAt/1#dispred#a125c821#bff#reorder_0_2_1_021#join_rhs` ON FIRST 2 OUTPUT Lhs.3, Lhs.1, Rhs.2, Lhs.0, Lhs.2, Lhs.4 465635 ~0% {6} | JOIN WITH `TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess.getTypeAt/1#dispred#3a89868c#prev` ON FIRST 3 OUTPUT Lhs.5, Lhs.2, Lhs.3, Lhs.4, Lhs.1, Lhs.0 {6} | AND NOT `Type::TypeAbstraction.getATypeParameter/0#dispred#030257a0`(FIRST 2) 465629 ~1% {6} | SCAN OUTPUT In.2, In.1, In.4, In.3, In.5, In.0 465635 ~1% {6} r17 = r13 UNION r16 465635 ~1% {4} | JOIN WITH `TypeMention::TypeMention.resolveTypeAt/1#dispred#a125c821#bff#reorder_0_2_1` ON FIRST 3 OUTPUT Lhs.4, Lhs.5, Lhs.0, Lhs.3 563408 ~1% {4} r18 = r2 UNION r3 UNION r7 UNION r17 563408 ~1% {4} | AND NOT `TypeInference::M2::IsInstantiationOf<TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess,TypeInference::CallExprBaseMatching::AccessConstraint::IsInstantiationOfInput>::satisfiesConcreteTypesFromIndex/4#716280b9#prev`(FIRST 4) return r18 ``` After ``` Pipeline standard for TypeInference::M2::IsInstantiationOf<TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess,TypeInference::CallExprBaseMatching::AccessConstraint::IsInstantiationOfInput>::satisfiesConcreteTypesFromIndex/4#716280b9@e8671bx7 was evaluated in 376 iterations totaling 245ms (delta sizes total: 563353). 563353 ~1% {6} r1 = SCAN `TypeInference::M2::IsInstantiationOf<TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess,TypeInference::CallExprBaseMatching::AccessConstraint::IsInstantiationOfInput>::satisfiesConcreteTypesFromIndex/4#716280b9#prev_delta` OUTPUT In.0, In.1, In.2, _, In.3, _ 563353 ~1% {4} | REWRITE WITH Tmp.3 := 1, Out.3 := (Tmp.3 + In.4), Tmp.5 := 0, TEST Out.3 != Tmp.5 KEEPING 4 259340 ~1% {5} r2 = JOIN r1 WITH `TypeInference::M2::IsInstantiationOf<TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess,TypeInference::CallExprBaseMatching::AccessConstraint::IsInstantiationOfInput>::resolveTypeAt/5#77e2181d#prev` ON FIRST 4 OUTPUT Lhs.1, Rhs.5, Lhs.0, Lhs.2, Lhs.3 52485 ~0% {4} | JOIN WITH `Type::TypeAbstraction.getATypeParameter/0#dispred#030257a0` ON FIRST 2 OUTPUT Lhs.2, Lhs.0, Lhs.3, Lhs.4 259340 ~1% {6} r3 = JOIN r1 WITH `TypeInference::M2::IsInstantiationOf<TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess,TypeInference::CallExprBaseMatching::AccessConstraint::IsInstantiationOfInput>::resolveTypeAt/5#77e2181d#prev` ON FIRST 4 OUTPUT Lhs.0, Rhs.4, Rhs.5, Lhs.1, Lhs.2, Lhs.3 16033 ~0% {5} | JOIN WITH `TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess.getTypeAt/1#dispred#3a89868c#prev` ON FIRST 3 OUTPUT Lhs.3, Lhs.2, Lhs.0, Lhs.4, Lhs.5 {5} | AND NOT `Type::TypeAbstraction.getATypeParameter/0#dispred#030257a0`(FIRST 2) 15992 ~0% {4} | SCAN OUTPUT In.2, In.0, In.3, In.4 741397 ~1% {7} r4 = SCAN `TypeInference::M2::IsInstantiationOf<TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess,TypeInference::CallExprBaseMatching::AccessConstraint::IsInstantiationOfInput>::resolveTypeAt/5#77e2181d#prev_delta` OUTPUT In.0, In.1, In.2, In.3, In.4, In.5, _ 465635 ~1% {6} | REWRITE WITH Tmp.6 := 0, TEST InOut.3 = Tmp.6 KEEPING 6 465635 ~1% {5} r5 = SCAN r4 OUTPUT In.1, In.5, In.0, In.2, _ 465635 ~0% {5} | REWRITE WITH Out.4 := 0 741397 ~1% {7} r6 = SCAN `TypeInference::M2::IsInstantiationOf<TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess,TypeInference::CallExprBaseMatching::AccessConstraint::IsInstantiationOfInput>::resolveTypeAt/5#77e2181d#prev_delta` OUTPUT In.0, In.1, In.2, In.3, In.4, In.5, _ 275762 ~1% {6} | REWRITE WITH Tmp.6 := 0, TEST InOut.3 != Tmp.6 KEEPING 6 0 ~0% {7} r7 = JOIN r6 WITH `TypeInference::M2::IsInstantiationOf<TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess,TypeInference::CallExprBaseMatching::AccessConstraint::IsInstantiationOfInput>::satisfiesConcreteTypesFromIndex/4#716280b9#prev` ON FIRST 3 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.3, Lhs.5, Rhs.3, _ {7} | REWRITE WITH Tmp.6 := 1, Out.6 := (InOut.3 - Tmp.6), TEST Out.6 = InOut.5 0 ~0% {5} | SCAN OUTPUT In.1, In.4, In.0, In.2, In.3 465635 ~0% {5} r8 = r5 UNION r7 6 ~0% {4} | JOIN WITH `Type::TypeAbstraction.getATypeParameter/0#dispred#030257a0` ON FIRST 2 OUTPUT Lhs.2, Lhs.0, Lhs.3, Lhs.4 29310 ~0% {5} r9 = JOIN `TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess.getTypeAt/1#dispred#3a89868c#prev_delta` WITH `TypeInference::M2::IsInstantiationOf<TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess,TypeInference::CallExprBaseMatching::AccessConstraint::IsInstantiationOfInput>::resolveTypeAt/5#77e2181d#reorder_0_4_5_1_2_3#prev` ON FIRST 3 OUTPUT Lhs.0, Lhs.2, Rhs.3, Rhs.4, Rhs.5 29310 ~0% {6} r10 = SCAN r9 OUTPUT In.0, In.1, In.2, In.3, In.4, _ {5} | REWRITE WITH Tmp.5 := 0, TEST InOut.4 = Tmp.5 KEEPING 5 0 ~0% {5} | SCAN OUTPUT In.2, In.1, In.0, In.3, _ 0 ~0% {5} | REWRITE WITH Out.4 := 0 29310 ~0% {6} r11 = SCAN r9 OUTPUT In.0, In.1, In.2, In.3, In.4, _ {5} | REWRITE WITH Tmp.5 := 0, TEST InOut.4 != Tmp.5 KEEPING 5 29310 ~1% {6} | SCAN OUTPUT In.0, In.2, In.3, _, In.1, In.4 29310 ~1% {6} | REWRITE WITH Tmp.3 := 1, Out.3 := (InOut.5 - Tmp.3) 29241 ~0% {5} | JOIN WITH `TypeInference::M2::IsInstantiationOf<TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess,TypeInference::CallExprBaseMatching::AccessConstraint::IsInstantiationOfInput>::satisfiesConcreteTypesFromIndex/4#716280b9#prev` ON FIRST 4 OUTPUT Lhs.1, Lhs.4, Lhs.0, Lhs.2, Lhs.5 29241 ~0% {5} r12 = r10 UNION r11 {5} | AND NOT `Type::TypeAbstraction.getATypeParameter/0#dispred#030257a0`(FIRST 2) 29241 ~1% {4} | SCAN OUTPUT In.2, In.0, In.3, In.4 465635 ~0% {6} r13 = SCAN r4 OUTPUT In.0, In.4, In.5, In.1, In.2, _ 465635 ~1% {6} | REWRITE WITH Out.5 := 0 0 ~0% {8} r14 = JOIN r6 WITH `TypeInference::M2::IsInstantiationOf<TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess,TypeInference::CallExprBaseMatching::AccessConstraint::IsInstantiationOfInput>::satisfiesConcreteTypesFromIndex/4#716280b9#prev` ON FIRST 3 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.3, Lhs.4, Lhs.5, Rhs.3, _ {8} | REWRITE WITH Tmp.7 := 1, Out.7 := (InOut.3 - Tmp.7), TEST Out.7 = InOut.6 0 ~0% {6} | SCAN OUTPUT In.0, In.4, In.5, In.1, In.2, In.3 465635 ~1% {6} r15 = r13 UNION r14 465635 ~0% {5} | JOIN WITH `TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess.getTypeAt/1#dispred#3a89868c#prev` ON FIRST 3 OUTPUT Lhs.3, Lhs.2, Lhs.0, Lhs.4, Lhs.5 {5} | AND NOT `Type::TypeAbstraction.getATypeParameter/0#dispred#030257a0`(FIRST 2) 465629 ~1% {4} | SCAN OUTPUT In.2, In.0, In.3, In.4 563353 ~1% {4} r16 = r2 UNION r3 UNION r8 UNION r12 UNION r15 563353 ~1% {4} | AND NOT `TypeInference::M2::IsInstantiationOf<TypeInference::CallExprBaseMatching::AccessConstraint::RelevantAccess,TypeInference::CallExprBaseMatching::AccessConstraint::IsInstantiationOfInput>::satisfiesConcreteTypesFromIndex/4#716280b9#prev`(FIRST 4) return r16 ```
1 parent bc60d03 commit f9915e6

File tree

1 file changed

+10
-14
lines changed

1 file changed

+10
-14
lines changed

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

Lines changed: 10 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -423,27 +423,23 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
423423
)
424424
}
425425

426-
/**
427-
* Holds if `app` is a possible instantiation of `tm` at `path`. That is
428-
* the type at `path` in `tm` is either a type parameter or equal to the
429-
* type at the same path in `app`.
430-
*/
431-
bindingset[app, abs, tm, path]
432-
private predicate satisfiesConcreteTypeAt(
433-
App app, TypeAbstraction abs, TypeMention tm, TypePath path
426+
pragma[nomagic]
427+
private Type resolveNthTypeAt(
428+
App app, TypeAbstraction abs, TypeMention tm, int i, TypePath path
434429
) {
435-
exists(Type t |
436-
tm.resolveTypeAt(path) = t and
437-
if t = abs.getATypeParameter() then any() else app.getTypeAt(path) = t
438-
)
430+
potentialInstantiationOf(app, abs, tm) and
431+
path = getNthPath(tm, i) and
432+
result = tm.resolveTypeAt(path)
439433
}
440434

441435
pragma[nomagic]
442436
private predicate satisfiesConcreteTypesFromIndex(
443437
App app, TypeAbstraction abs, TypeMention tm, int i
444438
) {
445-
potentialInstantiationOf(app, abs, tm) and
446-
satisfiesConcreteTypeAt(app, abs, tm, getNthPath(tm, i)) and
439+
exists(Type t, TypePath path |
440+
t = resolveNthTypeAt(app, abs, tm, i, path) and
441+
if t = abs.getATypeParameter() then any() else app.getTypeAt(path) = t
442+
) and
447443
// Recurse unless we are at the first path
448444
if i = 0 then any() else satisfiesConcreteTypesFromIndex(app, abs, tm, i - 1)
449445
}

0 commit comments

Comments
 (0)