Rust: Apply inherent method prioritization inside type inference loop

This commit is contained in:
Tom Hvitved
2025-06-27 11:46:27 +02:00
parent e5f0ef6ae8
commit e88d7baa7d
6 changed files with 84 additions and 254 deletions

View File

@@ -699,7 +699,7 @@ private module CallExprBaseMatchingInput implements MatchingInputSig {
}
Declaration getTarget() {
result = inferMethodCallTarget(this) // mutual recursion; resolving method calls requires resolving types and vice versa
result = resolveMethodCallTarget(this) // mutual recursion; resolving method calls requires resolving types and vice versa
or
result = CallExprImpl::getResolvedFunction(this)
}
@@ -1178,14 +1178,14 @@ private predicate methodCandidateTrait(Type type, Trait trait, string name, int
methodCandidate(type, name, arity, impl)
}
private module IsInstantiationOfInput implements IsInstantiationOfInputSig<MethodCall> {
pragma[nomagic]
private predicate isMethodCall(MethodCall mc, Type rootType, string name, int arity) {
rootType = mc.getTypeAt(TypePath::nil()) and
name = mc.getMethodName() and
arity = mc.getNumberOfArguments()
}
pragma[nomagic]
private predicate isMethodCall(MethodCall mc, Type rootType, string name, int arity) {
rootType = mc.getTypeAt(TypePath::nil()) and
name = mc.getMethodName() and
arity = mc.getNumberOfArguments()
}
private module IsInstantiationOfInput implements IsInstantiationOfInputSig<MethodCall> {
pragma[nomagic]
predicate potentialInstantiationOf(MethodCall mc, TypeAbstraction impl, TypeMention constraint) {
exists(Type rootType, string name, int arity |
@@ -1334,17 +1334,46 @@ private predicate methodResolutionDependsOnArgument(
)
}
/**
* Holds if the method call `mc` has no inherent target, i.e., it does not
* resolve to a method in an `impl` block for the type of the receiver.
*/
pragma[nomagic]
private predicate methodCallHasNoInherentTarget(MethodCall mc) {
exists(Type rootType, string name, int arity |
isMethodCall(mc, rootType, name, arity) and
forall(Impl impl |
methodCandidate(rootType, name, arity, impl) and
not impl.hasTrait()
|
IsInstantiationOf<MethodCall, IsInstantiationOfInput>::isNotInstantiationOf(mc, impl, _)
)
)
}
pragma[nomagic]
private predicate methodCallHasImplCandidate(MethodCall mc, Impl impl) {
IsInstantiationOf<MethodCall, IsInstantiationOfInput>::isInstantiationOf(mc, impl, _) and
if impl.hasTrait() and not exists(mc.getTrait())
then
// inherent methods take precedence over trait methods, so only allow
// trait methods when there are no matching inherent methods
methodCallHasNoInherentTarget(mc)
else any()
}
/** Gets a method from an `impl` block that matches the method call `mc`. */
pragma[nomagic]
private Function getMethodFromImpl(MethodCall mc) {
exists(Impl impl |
IsInstantiationOf<MethodCall, IsInstantiationOfInput>::isInstantiationOf(mc, impl, _) and
result = getMethodSuccessor(impl, mc.getMethodName())
exists(Impl impl, string name |
methodCallHasImplCandidate(mc, impl) and
name = mc.getMethodName() and
result = getMethodSuccessor(impl, name)
|
not methodResolutionDependsOnArgument(impl, _, _, _, _, _) and
result = getMethodSuccessor(impl, mc.getMethodName())
not methodResolutionDependsOnArgument(impl, _, _, _, _, _)
or
exists(int pos, TypePath path, Type type |
methodResolutionDependsOnArgument(impl, mc.getMethodName(), result, pos, path, type) and
methodResolutionDependsOnArgument(impl, name, result, pos, path, type) and
inferType(mc.getPositionalArgument(pos), path) = type
)
)
@@ -1356,22 +1385,6 @@ private Function getTraitMethod(ImplTraitReturnType trait, string name) {
result = getMethodSuccessor(trait.getImplTraitTypeRepr(), name)
}
/**
* Gets a method that the method call `mc` resolves to based on type inference,
* if any.
*/
private Function inferMethodCallTarget(MethodCall mc) {
// The method comes from an `impl` block targeting the type of the receiver.
result = getMethodFromImpl(mc)
or
// The type of the receiver is a type parameter and the method comes from a
// trait bound on the type parameter.
result = getTypeParameterMethod(mc.getTypeAt(TypePath::nil()), mc.getMethodName())
or
// The type of the receiver is an `impl Trait` type.
result = getTraitMethod(mc.getTypeAt(TypePath::nil()), mc.getMethodName())
}
cached
private module Cached {
private import codeql.rust.internal.CachedStages
@@ -1400,47 +1413,18 @@ private module Cached {
)
}
private predicate isInherentImplFunction(Function f) {
f = any(Impl impl | not impl.hasTrait()).(ImplItemNode).getAnAssocItem()
}
private predicate isTraitImplFunction(Function f) {
f = any(Impl impl | impl.hasTrait()).(ImplItemNode).getAnAssocItem()
}
private Function resolveMethodCallTargetFrom(MethodCall mc, boolean fromSource) {
result = inferMethodCallTarget(mc) and
(if result.fromSource() then fromSource = true else fromSource = false) and
(
// prioritize inherent implementation methods first
isInherentImplFunction(result)
or
not isInherentImplFunction(inferMethodCallTarget(mc)) and
(
// then trait implementation methods
isTraitImplFunction(result)
or
not isTraitImplFunction(inferMethodCallTarget(mc)) and
(
// then trait methods with default implementations
result.hasBody()
or
// and finally trait methods without default implementations
not inferMethodCallTarget(mc).hasBody()
)
)
)
}
/** Gets a method that the method call `mc` resolves to, if any. */
cached
Function resolveMethodCallTarget(MethodCall mc) {
// Functions in source code also gets extracted as library code, due to
// this duplication we prioritize functions from source code.
result = resolveMethodCallTargetFrom(mc, true)
// The method comes from an `impl` block targeting the type of the receiver.
result = getMethodFromImpl(mc)
or
not exists(resolveMethodCallTargetFrom(mc, true)) and
result = resolveMethodCallTargetFrom(mc, false)
// The type of the receiver is a type parameter and the method comes from a
// trait bound on the type parameter.
result = getTypeParameterMethod(mc.getTypeAt(TypePath::nil()), mc.getMethodName())
or
// The type of the receiver is an `impl Trait` type.
result = getTraitMethod(mc.getTypeAt(TypePath::nil()), mc.getMethodName())
}
pragma[inline]

View File

@@ -10,6 +10,9 @@ multipleCallTargets
| test.rs:168:26:168:111 | ...::_print(...) |
| test.rs:178:30:178:68 | ...::_print(...) |
| test.rs:187:26:187:105 | ...::_print(...) |
| test.rs:228:22:228:72 | ... .read_to_string(...) |
| test.rs:482:22:482:50 | file.read_to_end(...) |
| test.rs:488:22:488:53 | file.read_to_string(...) |
| test.rs:609:18:609:38 | ...::_print(...) |
| test.rs:614:18:614:45 | ...::_print(...) |
| test.rs:618:25:618:49 | address.to_socket_addrs() |

View File

@@ -1,9 +1,9 @@
multipleCallTargets
| dereference.rs:61:15:61:24 | e1.deref() |
| main.rs:1963:13:1963:31 | ...::from(...) |
| main.rs:1964:13:1964:31 | ...::from(...) |
| main.rs:1965:13:1965:31 | ...::from(...) |
| main.rs:1970:13:1970:31 | ...::from(...) |
| main.rs:1971:13:1971:31 | ...::from(...) |
| main.rs:1972:13:1972:31 | ...::from(...) |
| main.rs:2006:21:2006:43 | ...::from(...) |
| main.rs:2032:13:2032:31 | ...::from(...) |
| main.rs:2033:13:2033:31 | ...::from(...) |
| main.rs:2034:13:2034:31 | ...::from(...) |
| main.rs:2040:13:2040:31 | ...::from(...) |
| main.rs:2041:13:2041:31 | ...::from(...) |
| main.rs:2042:13:2042:31 | ...::from(...) |
| main.rs:2078:21:2078:43 | ...::from(...) |

View File

@@ -736,89 +736,13 @@ inferType
| main.rs:485:13:485:16 | self | | file://:0:0:0:0 | & |
| main.rs:485:13:485:16 | self | &T | main.rs:468:5:469:22 | S3 |
| main.rs:485:13:485:16 | self | &T.T3 | main.rs:482:10:482:10 | T |
| main.rs:490:13:490:13 | x | | file://:0:0:0:0 | & |
| main.rs:490:13:490:13 | x | | main.rs:397:5:398:14 | S1 |
| main.rs:490:13:490:13 | x | &T | file://:0:0:0:0 | & |
| main.rs:490:13:490:13 | x | &T | main.rs:397:5:398:14 | S1 |
| main.rs:490:13:490:13 | x | &T.&T | file://:0:0:0:0 | & |
| main.rs:490:13:490:13 | x | &T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:490:13:490:13 | x | &T.&T.&T | file://:0:0:0:0 | & |
| main.rs:490:13:490:13 | x | &T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:490:13:490:13 | x | &T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:490:13:490:13 | x | &T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:490:13:490:13 | x | &T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:490:13:490:13 | x | &T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:490:13:490:13 | x | &T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:490:13:490:13 | x | &T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:490:13:490:13 | x | &T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:490:13:490:13 | x | &T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:490:13:490:13 | x | &T.&T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:490:13:490:13 | x | &T.&T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:490:13:490:13 | x | &T.&T.&T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:490:13:490:13 | x | &T.&T.&T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:490:17:490:18 | S1 | | file://:0:0:0:0 | & |
| main.rs:490:17:490:18 | S1 | | main.rs:397:5:398:14 | S1 |
| main.rs:490:17:490:18 | S1 | &T | file://:0:0:0:0 | & |
| main.rs:490:17:490:18 | S1 | &T | main.rs:397:5:398:14 | S1 |
| main.rs:490:17:490:18 | S1 | &T.&T | file://:0:0:0:0 | & |
| main.rs:490:17:490:18 | S1 | &T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:490:17:490:18 | S1 | &T.&T.&T | file://:0:0:0:0 | & |
| main.rs:490:17:490:18 | S1 | &T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:490:17:490:18 | S1 | &T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:490:17:490:18 | S1 | &T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:490:17:490:18 | S1 | &T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:490:17:490:18 | S1 | &T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:490:17:490:18 | S1 | &T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:490:17:490:18 | S1 | &T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:490:17:490:18 | S1 | &T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:490:17:490:18 | S1 | &T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:490:17:490:18 | S1 | &T.&T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:490:17:490:18 | S1 | &T.&T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:490:17:490:18 | S1 | &T.&T.&T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:490:17:490:18 | S1 | &T.&T.&T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:491:18:491:23 | "{:?}\\n" | | {EXTERNAL LOCATION} | str |
| main.rs:491:26:491:26 | x | | file://:0:0:0:0 | & |
| main.rs:491:26:491:26 | x | | main.rs:397:5:398:14 | S1 |
| main.rs:491:26:491:26 | x | &T | file://:0:0:0:0 | & |
| main.rs:491:26:491:26 | x | &T | main.rs:397:5:398:14 | S1 |
| main.rs:491:26:491:26 | x | &T.&T | file://:0:0:0:0 | & |
| main.rs:491:26:491:26 | x | &T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:491:26:491:26 | x | &T.&T.&T | file://:0:0:0:0 | & |
| main.rs:491:26:491:26 | x | &T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:491:26:491:26 | x | &T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:491:26:491:26 | x | &T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:491:26:491:26 | x | &T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:491:26:491:26 | x | &T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:491:26:491:26 | x | &T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:491:26:491:26 | x | &T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:491:26:491:26 | x | &T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:491:26:491:26 | x | &T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:491:26:491:26 | x | &T.&T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:491:26:491:26 | x | &T.&T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:491:26:491:26 | x | &T.&T.&T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:491:26:491:26 | x | &T.&T.&T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:491:26:491:42 | x.common_method() | | main.rs:397:5:398:14 | S1 |
| main.rs:492:18:492:23 | "{:?}\\n" | | {EXTERNAL LOCATION} | str |
| main.rs:492:26:492:26 | x | | file://:0:0:0:0 | & |
| main.rs:492:26:492:26 | x | | main.rs:397:5:398:14 | S1 |
| main.rs:492:26:492:26 | x | &T | file://:0:0:0:0 | & |
| main.rs:492:26:492:26 | x | &T | main.rs:397:5:398:14 | S1 |
| main.rs:492:26:492:26 | x | &T.&T | file://:0:0:0:0 | & |
| main.rs:492:26:492:26 | x | &T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:492:26:492:26 | x | &T.&T.&T | file://:0:0:0:0 | & |
| main.rs:492:26:492:26 | x | &T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:492:26:492:26 | x | &T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:492:26:492:26 | x | &T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:492:26:492:26 | x | &T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:492:26:492:26 | x | &T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:492:26:492:26 | x | &T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:492:26:492:26 | x | &T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:492:26:492:26 | x | &T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:492:26:492:26 | x | &T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:492:26:492:26 | x | &T.&T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:492:26:492:26 | x | &T.&T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:492:26:492:26 | x | &T.&T.&T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:492:26:492:26 | x | &T.&T.&T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:492:26:492:44 | x.common_method_2() | | main.rs:397:5:398:14 | S1 |
| main.rs:494:13:494:13 | y | | main.rs:430:5:430:22 | S2 |
| main.rs:494:13:494:13 | y | T2 | main.rs:397:5:398:14 | S1 |
@@ -839,121 +763,17 @@ inferType
| main.rs:498:26:498:26 | z | T2 | {EXTERNAL LOCATION} | i32 |
| main.rs:498:26:498:42 | z.common_method() | | main.rs:397:5:398:14 | S1 |
| main.rs:500:13:500:13 | w | | main.rs:468:5:469:22 | S3 |
| main.rs:500:13:500:13 | w | T3 | file://:0:0:0:0 | & |
| main.rs:500:13:500:13 | w | T3 | main.rs:397:5:398:14 | S1 |
| main.rs:500:13:500:13 | w | T3.&T | file://:0:0:0:0 | & |
| main.rs:500:13:500:13 | w | T3.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:13:500:13 | w | T3.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:13:500:13 | w | T3.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:13:500:13 | w | T3.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:13:500:13 | w | T3.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:13:500:13 | w | T3.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:13:500:13 | w | T3.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:13:500:13 | w | T3.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:13:500:13 | w | T3.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:13:500:13 | w | T3.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:13:500:13 | w | T3.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:13:500:13 | w | T3.&T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:13:500:13 | w | T3.&T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:13:500:13 | w | T3.&T.&T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:13:500:13 | w | T3.&T.&T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:17:500:22 | S3(...) | | main.rs:468:5:469:22 | S3 |
| main.rs:500:17:500:22 | S3(...) | T3 | file://:0:0:0:0 | & |
| main.rs:500:17:500:22 | S3(...) | T3 | main.rs:397:5:398:14 | S1 |
| main.rs:500:17:500:22 | S3(...) | T3.&T | file://:0:0:0:0 | & |
| main.rs:500:17:500:22 | S3(...) | T3.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:17:500:22 | S3(...) | T3.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:17:500:22 | S3(...) | T3.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:17:500:22 | S3(...) | T3.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:17:500:22 | S3(...) | T3.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:17:500:22 | S3(...) | T3.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:17:500:22 | S3(...) | T3.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:17:500:22 | S3(...) | T3.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:17:500:22 | S3(...) | T3.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:17:500:22 | S3(...) | T3.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:17:500:22 | S3(...) | T3.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:17:500:22 | S3(...) | T3.&T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:17:500:22 | S3(...) | T3.&T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:17:500:22 | S3(...) | T3.&T.&T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:17:500:22 | S3(...) | T3.&T.&T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:20:500:21 | S1 | | file://:0:0:0:0 | & |
| main.rs:500:20:500:21 | S1 | | main.rs:397:5:398:14 | S1 |
| main.rs:500:20:500:21 | S1 | &T | file://:0:0:0:0 | & |
| main.rs:500:20:500:21 | S1 | &T | main.rs:397:5:398:14 | S1 |
| main.rs:500:20:500:21 | S1 | &T.&T | file://:0:0:0:0 | & |
| main.rs:500:20:500:21 | S1 | &T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:20:500:21 | S1 | &T.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:20:500:21 | S1 | &T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:20:500:21 | S1 | &T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:20:500:21 | S1 | &T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:20:500:21 | S1 | &T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:20:500:21 | S1 | &T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:20:500:21 | S1 | &T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:20:500:21 | S1 | &T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:20:500:21 | S1 | &T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:20:500:21 | S1 | &T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:500:20:500:21 | S1 | &T.&T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:500:20:500:21 | S1 | &T.&T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:18:501:23 | "{:?}\\n" | | {EXTERNAL LOCATION} | str |
| main.rs:501:26:501:26 | w | | main.rs:468:5:469:22 | S3 |
| main.rs:501:26:501:26 | w | T3 | file://:0:0:0:0 | & |
| main.rs:501:26:501:26 | w | T3 | main.rs:397:5:398:14 | S1 |
| main.rs:501:26:501:26 | w | T3.&T | file://:0:0:0:0 | & |
| main.rs:501:26:501:26 | w | T3.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:26:501:26 | w | T3.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:26:501:26 | w | T3.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:26:501:26 | w | T3.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:26:501:26 | w | T3.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:26:501:26 | w | T3.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:26:501:26 | w | T3.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:26:501:26 | w | T3.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:26:501:26 | w | T3.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:26:501:26 | w | T3.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:26:501:26 | w | T3.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:26:501:26 | w | T3.&T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:26:501:26 | w | T3.&T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:26:501:26 | w | T3.&T.&T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:26:501:26 | w | T3.&T.&T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:26:501:31 | w.m(...) | | file://:0:0:0:0 | & |
| main.rs:501:26:501:31 | w.m(...) | &T | main.rs:468:5:469:22 | S3 |
| main.rs:501:26:501:31 | w.m(...) | &T.T3 | file://:0:0:0:0 | & |
| main.rs:501:26:501:31 | w.m(...) | &T.T3 | main.rs:397:5:398:14 | S1 |
| main.rs:501:26:501:31 | w.m(...) | &T.T3.&T | file://:0:0:0:0 | & |
| main.rs:501:26:501:31 | w.m(...) | &T.T3.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:26:501:31 | w.m(...) | &T.T3.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:26:501:31 | w.m(...) | &T.T3.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:26:501:31 | w.m(...) | &T.T3.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:26:501:31 | w.m(...) | &T.T3.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:26:501:31 | w.m(...) | &T.T3.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:26:501:31 | w.m(...) | &T.T3.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:26:501:31 | w.m(...) | &T.T3.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:26:501:31 | w.m(...) | &T.T3.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:26:501:31 | w.m(...) | &T.T3.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:26:501:31 | w.m(...) | &T.T3.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:26:501:31 | w.m(...) | &T.T3.&T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:26:501:31 | w.m(...) | &T.T3.&T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:26:501:31 | w.m(...) | &T.T3.&T.&T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:26:501:31 | w.m(...) | &T.T3.&T.&T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:30:501:30 | x | | file://:0:0:0:0 | & |
| main.rs:501:30:501:30 | x | | main.rs:397:5:398:14 | S1 |
| main.rs:501:30:501:30 | x | &T | file://:0:0:0:0 | & |
| main.rs:501:30:501:30 | x | &T | main.rs:397:5:398:14 | S1 |
| main.rs:501:30:501:30 | x | &T.&T | file://:0:0:0:0 | & |
| main.rs:501:30:501:30 | x | &T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:30:501:30 | x | &T.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:30:501:30 | x | &T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:30:501:30 | x | &T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:30:501:30 | x | &T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:30:501:30 | x | &T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:30:501:30 | x | &T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:30:501:30 | x | &T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:30:501:30 | x | &T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:30:501:30 | x | &T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:30:501:30 | x | &T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:30:501:30 | x | &T.&T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:30:501:30 | x | &T.&T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:501:30:501:30 | x | &T.&T.&T.&T.&T.&T.&T.&T.&T | file://:0:0:0:0 | & |
| main.rs:501:30:501:30 | x | &T.&T.&T.&T.&T.&T.&T.&T.&T | main.rs:397:5:398:14 | S1 |
| main.rs:518:19:518:22 | SelfParam | | main.rs:516:5:519:5 | Self [trait FirstTrait] |
| main.rs:523:19:523:22 | SelfParam | | main.rs:521:5:524:5 | Self [trait SecondTrait] |
| main.rs:526:64:526:64 | x | | main.rs:526:45:526:61 | T |

View File

@@ -2,3 +2,4 @@ multipleCallTargets
| test_logging.rs:77:20:77:36 | password.as_str() |
| test_logging.rs:78:22:78:38 | password.as_str() |
| test_logging.rs:88:18:88:34 | password.as_str() |
| test_logging.rs:243:5:245:66 | ... .write_all(...) |

View File

@@ -649,6 +649,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
* - `Pair<int, bool>` is _not_ an instantiation of `Pair<A, A>`
* - `Pair<int, string>` is _not_ an instantiation of `Pair<string, string>`
*/
pragma[nomagic]
predicate isInstantiationOf(App app, TypeAbstraction abs, TypeMention tm) {
// We only need to check equality if the concrete types are satisfied.
satisfiesConcreteTypes(app, abs, tm) and
@@ -666,6 +667,27 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
)
)
}
/**
* Holds if `app` is _not_ a possible instantiation of `tm`.
*/
pragma[nomagic]
predicate isNotInstantiationOf(App app, TypeAbstraction abs, TypeMention tm) {
// `app` and `tm` differ on a concrete type
exists(Type t, TypePath path |
t = resolveNthTypeAt(app, abs, tm, _, path) and
not t = abs.getATypeParameter() and
not path.isEmpty() and
app.getTypeAt(path) != t
)
or
// `app` uses inconsistent type parameter instantiations
exists(TypeParameter tp |
potentialInstantiationOf(app, abs, tm) and
app.getTypeAt(getNthTypeParameterPath(tm, tp, _)) !=
app.getTypeAt(getNthTypeParameterPath(tm, tp, _))
)
}
}
/** Provides logic related to base types. */