From 3419c00bc0f398e439665c9a384483ee2b226254 Mon Sep 17 00:00:00 2001 From: Tom Hvitved Date: Mon, 17 Nov 2025 12:27:53 +0100 Subject: [PATCH] Rust: Use `ToIndex` instead of `FromIndex` in ranked `forex` predicates `ToIndex` makes more sense, since we start the recursion from `0`. --- .../internal/typeinference/FunctionType.qll | 10 ++++----- .../typeinference/internal/TypeInference.qll | 22 +++++++++---------- 2 files changed, 16 insertions(+), 16 deletions(-) diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionType.qll b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionType.qll index 727c99fa8105..e8b44336e76f 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionType.qll +++ b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionType.qll @@ -351,7 +351,7 @@ module ArgsAreInstantiationsOf { | rnk = 0 or - argsAreInstantiationsOfFromIndex(call, abs, f, rnk - 1) + argsAreInstantiationsOfToIndex(call, abs, f, rnk - 1) ) } @@ -360,15 +360,15 @@ module ArgsAreInstantiationsOf { } } - private module ArgIsInstantiationOfFromIndex = + private module ArgIsInstantiationOfToIndex = ArgIsInstantiationOf; pragma[nomagic] - private predicate argsAreInstantiationsOfFromIndex( + private predicate argsAreInstantiationsOfToIndex( Input::Call call, ImplOrTraitItemNode i, Function f, int rnk ) { exists(FunctionPosition pos | - ArgIsInstantiationOfFromIndex::argIsInstantiationOf(MkCallAndPos(call, pos), i, _) and + ArgIsInstantiationOfToIndex::argIsInstantiationOf(MkCallAndPos(call, pos), i, _) and call.hasTargetCand(i, f) and toCheckRanked(i, f, pos, rnk) ) @@ -381,7 +381,7 @@ module ArgsAreInstantiationsOf { pragma[nomagic] predicate argsAreInstantiationsOf(Input::Call call, ImplOrTraitItemNode i, Function f) { exists(int rnk | - argsAreInstantiationsOfFromIndex(call, i, f, rnk) and + argsAreInstantiationsOfToIndex(call, i, f, rnk) and rnk = max(int r | toCheckRanked(i, f, _, r)) ) } diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll index a827ef3cd792..47b80b9dc189 100644 --- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll +++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll @@ -578,7 +578,7 @@ module Make1 Input1> { } pragma[nomagic] - private predicate satisfiesConcreteTypesFromIndex( + private predicate satisfiesConcreteTypesToIndex( App app, TypeAbstraction abs, Constraint constraint, int i ) { exists(Type t, TypePath path | @@ -586,13 +586,13 @@ module Make1 Input1> { if t = abs.getATypeParameter() then any() else app.getTypeAt(path) = t ) and // Recurse unless we are at the first path - if i = 0 then any() else satisfiesConcreteTypesFromIndex(app, abs, constraint, i - 1) + if i = 0 then any() else satisfiesConcreteTypesToIndex(app, abs, constraint, i - 1) } /** Holds if all the concrete types in `constraint` also occur in `app`. */ pragma[nomagic] private predicate satisfiesConcreteTypes(App app, TypeAbstraction abs, Constraint constraint) { - satisfiesConcreteTypesFromIndex(app, abs, constraint, + satisfiesConcreteTypesToIndex(app, abs, constraint, max(int i | exists(getNthPath(constraint, i)))) } @@ -620,7 +620,7 @@ module Make1 Input1> { } pragma[nomagic] - private predicate typeParametersEqualFromIndexBase( + private predicate typeParametersEqualToIndexBase( App app, TypeAbstraction abs, Constraint constraint, TypeParameter tp, TypePath path ) { path = getNthTypeParameterPath(constraint, tp, 0) and @@ -630,15 +630,15 @@ module Make1 Input1> { } pragma[nomagic] - private predicate typeParametersEqualFromIndex( + private predicate typeParametersEqualToIndex( App app, TypeAbstraction abs, Constraint constraint, TypeParameter tp, Type t, int i ) { exists(TypePath path | t = app.getTypeAt(path) and if i = 0 - then typeParametersEqualFromIndexBase(app, abs, constraint, tp, path) + then typeParametersEqualToIndexBase(app, abs, constraint, tp, path) else ( - typeParametersEqualFromIndex(app, abs, constraint, tp, t, i - 1) and + typeParametersEqualToIndex(app, abs, constraint, tp, t, i - 1) and path = getNthTypeParameterPath(constraint, tp, i) ) ) @@ -655,19 +655,19 @@ module Make1 Input1> { exists(int n | n = max(int i | exists(getNthTypeParameterPath(constraint, tp, i))) | // If the largest index is 0, then there are no equalities to check as // the type parameter only occurs once. - if n = 0 then any() else typeParametersEqualFromIndex(app, abs, constraint, tp, _, n) + if n = 0 then any() else typeParametersEqualToIndex(app, abs, constraint, tp, _, n) ) ) } - private predicate typeParametersHaveEqualInstantiationFromIndex( + private predicate typeParametersHaveEqualInstantiationToIndex( App app, TypeAbstraction abs, Constraint constraint, int i ) { exists(TypeParameter tp | tp = getNthTypeParameter(abs, i) | typeParametersEqual(app, abs, constraint, tp) and if i = 0 then any() - else typeParametersHaveEqualInstantiationFromIndex(app, abs, constraint, i - 1) + else typeParametersHaveEqualInstantiationToIndex(app, abs, constraint, i - 1) ) } @@ -697,7 +697,7 @@ module Make1 Input1> { not exists(getNthTypeParameter(abs, _)) or exists(int n | n = max(int i | exists(getNthTypeParameter(abs, i))) | - typeParametersHaveEqualInstantiationFromIndex(app, abs, constraint, n) + typeParametersHaveEqualInstantiationToIndex(app, abs, constraint, n) ) ) }