Rust: Rework call resolution and type inference for calls

[hvitved]

Overview

This PR rewrites how we do call resolution and type inference for calls, to make it more faithful to what actually happens in the compiler.

Impact

The changes to expected test output shows that this PR resolves many shortcomings, as well as removes a lot of inconsistencies.

DCA is excellent: On some projects we achieve a whopping ~90 % reduction in analysis time, which follows the decrease in Nodes With Type At Length Limit for those projects. On coreutils, rendiation, peace, ruff, and gluon, however, we see increases in both analysis time and Nodes With Type At Length Limit.

I also did a QA run, which confirms the overall reduction in analysis time:

Top 50 largest absolute deltas

Project	Analysis time before	Analysis time after	Diff
parbo/advent-of-code	3:43:52	0:10:09	-03:33:43
lambdaclass/sp1_poc_forger	3:14:07	0:30:51	-02:43:17
julianandrews/adventofcode	1:51:16	0:08:48	-01:42:28
uiua-lang/uiua	1:44:58	0:13:50	-01:31:09
renegade-fi/renegade	1:48:36	0:21:16	-01:27:21
mdsumner/zr	1:58:16	0:48:45	-01:09:32
to-omer/competitive-library	1:09:36	0:06:06	-01:03:30
dimforge/rapier	1:16:05	0:17:15	-00:58:51
rojo-rbx/rbx-dom	0:59:33	0:05:43	-00:53:50
nyx-space/nyx	0:55:50	0:09:36	-00:46:14
astral-sh/ruff	0:18:20	1:01:36	0:43:16
kjnapier/spacerocks	0:53:19	0:10:45	-00:42:35
lz520520/rust-1.75-ollvm	2:04:56	2:46:28	0:41:32
gluon-lang/gluon	0:09:06	0:38:28	0:29:21
azriel91/peace	0:14:06	0:41:52	0:27:46
sseemayer/aoc	0:28:06	0:06:45	-00:21:21
mpyle101/aoc	0:41:43	0:21:54	-00:19:49
tokio-rs/toasty	0:08:40	0:24:03	0:15:22
ferrocene/ferrocene	1:24:48	1:39:23	0:14:35
GraphiteEditor/Graphite	0:24:43	0:38:57	0:14:13
szbergeron/DaPaMIR-rustc	1:15:44	1:28:41	0:12:56
clear-crab/clear-crab	1:09:51	1:21:52	0:12:01
sigurd4/signal_processing	0:22:47	0:34:22	0:11:35
rust-lang/bors-kindergarten	1:13:03	1:24:09	0:11:06
RustVis/zu	0:56:20	0:45:16	-00:11:05
finos/perspective	0:26:00	0:36:31	0:10:30
misttech/mist-os	1:41:12	1:51:15	0:10:03
rust-lang/rust	1:15:01	1:24:31	0:09:30
mhogrefe/malachite	0:25:07	0:15:57	-00:09:11
mikialex/rendiation	0:55:48	0:47:29	-00:08:19
use-ink/ink	2:18:01	2:26:17	0:08:16
apache/datafusion	1:02:58	0:55:00	-00:07:58
dfinity/ic	2:47:07	2:54:52	0:07:44
tracel-ai/burn	0:45:35	0:37:59	-00:07:36
splashprotocol/splash-offchain-multiplatform	0:28:02	0:20:40	-00:07:22
ROCm/ROCK-Kernel-Driver	1:50:10	1:57:00	0:06:50
PyO3/pyo3	0:09:47	0:16:28	0:06:40
kolonialno/adventofcode	0:26:00	0:19:49	-00:06:12
Axnjr/snn_be_pro	0:44:35	0:38:26	-00:06:09
misttech/fuchsia	1:41:16	1:47:18	0:06:01
subcoin-project/subcoin	0:28:36	0:34:32	0:05:56
MDGSF/RustPractice	2:18:52	2:24:43	0:05:51
rustwasm/wasm-bindgen	0:21:24	0:26:41	0:05:17
Kalapaja/kampela-firmware	0:18:12	0:13:00	-00:05:13
oxidecomputer/third-party-api-clients	0:37:44	0:32:36	-00:05:08
zeitgeistpm/zeitgeist	2:30:08	2:25:33	-00:04:35
nazar-pc/abundance	0:37:50	0:33:18	-00:04:33
galacticcouncil/Basilisk-node	1:04:21	0:59:59	-00:04:23
microsoft/azure-devops-rust-api	0:21:15	0:17:01	-00:04:14
rivet-gg/rivet	1:22:04	1:17:52	-00:04:13

The QA run also showed that we have resolved analysis timeouts/failures for 29 projects:

Projects timeout/failure before

williamlion218/rust-sgx-sdk
zkMIPS/zkMIPS
zama-ai/tfhe-rs
veloren/veloren
kentakom1213/kyopro
TimTheBig/geo-3d
Univa/rumcake
10XGenomics/cellranger
ricosjp/truck
okaponta/atcoder-rust
jblindsay/whitebox-tools
futureversecom/trn-seed
mycroft/challenges
galacticcouncil/hydration-node
ChristopherBiscardi/advent-of-code
gasp-xyz/gasp-monorepo
dimforge/nalgebra
Apollo-Lab-Yale/apollo-rust
awsdocs/aws-doc-sdk-examples
rickyota/genoboost
SparkyPotato/radiance
strawlab/strand-braid
10XGenomics/spaceranger
sarah-quinones/faer-rs
hackmad/pbrt-v3-rs
attack68/rateslib
wingrew/thcore
Gleb-Zaslavsky/RustedSciThe
feos-org/feos

However, timeouts/failures have been introduced for 7 new projects

Projects timeout/failure after

golemfactory/yagna
carthage-software/mago
MaterializeInc/materialize
stencila/stencila
typedb/typedb
Feodor2/Mypal68
mattwparas/steel

In summary, both DCA and QA indicate overall performans wins, which is not necessarily expected (and certainly not the case for many earlier iterations of this PR), as this PR extends on the kinds of calls we are able to resolve.

For the reviewer

Note for review: As usual, commit-by-commit review is encouraged. As for the changes to TypeInference.qll, I very much recommend using split diff view.

Method call resolution

According to the spec, when resolving a method call x.m():

The first step is to build a list of candidate receiver types. Obtain these by repeatedly dereferencing the receiver expression’s type, adding each type encountered to the list, then finally attempting an unsized coercion at the end, and adding the result type if that is successful.

Then, for each candidate T, add &T and &mut T to the list immediately after T.

For instance, if the receiver has type Box<[i32;2]>, then the candidate types will be Box<[i32;2]>, &Box<[i32;2]>, &mut Box<[i32;2]>, [i32; 2] (by dereferencing), &[i32; 2], &mut [i32; 2], [i32] (by unsized coercion), &[i32], and finally &mut [i32].

Before this PR, we handled the above in a very ad hoc way, where we did attempt to model implicit dereferencing and borrowing, but we did not model the construction of candidate receiver types and prioritized lookup order. In particular, if x had type &Foo, we would only lookup the method in Foo.

With this PR, we model prioritized method lookup in the list of candidate receiver types in the module MethodResolution, but instead of constructing the full list of candidate receiver types, we recursively compute a set of candidates, only adding a new candidate receiver type to the set when we can rule out that the method cannot be found for the current candidate:

forall method:
  not current_candidate matches method

Care must be taken to ensure that the not current_candidate matches method check is monotonic, which we achieve using the monotonic isNotInstantiationOf predicate from the shared type inference library.

Method lookup

For a given candidate receiver type C, we need to match that type against the type of the self parameters of all potential call targets, taking into account that self parameters can have both explicit types and use shorthand syntax. Further care must be taken for methods that are inherited (either a trait method with a default implementation inherited by an impl block or a trait method inherited by a sub trait), so it only makes sense to talk about the type of a self parameter in the context of a given impl block or trait where that method is available (either directly or inherited). We model this using the class AssocFunctionType in the newly introduced FunctionType.qll library.

As before this PR, we use the IsInstantiationOf library for matching C against a given AssocFunctionType type S, now distinguishing between the following three cases:

1. The method is defined in a blanket implementation: In this case, we additionally check that the part of C that matches the blanket type parameter also satisfies the blanket constraint. This means that blanket implementations are now also taken into account in the context of auto-dereferencing/borrowing.
2. S represents the type of a self parameter for a method in a trait: In case C is e.g. dyn Trait, then we want C to match S, but only if the traits match up as well. We achieve this by substituting in the trait in both S and C before performing the IsInstantiationOf check.
3. Not case 1 and 2: Simply perform the IsInstantiationOf check.

Method call type inference

When we have identified a valid call target for x.m() with a given candidate receiver type C, we need to use that type as well when doing type inference. Before this PR, we used the Matching module from the shared type inference library, but now we instead use MatchingWithEnvironment, where we record C in the environment via the sequence of auto-dereferences and borrows that happened to obtain C. This means we replace the ad hoc handling mentioned earlier, because we now have explicit knowledge about dereferencing/borrowing. The implementation is in the new MethodCallMatchingInput module.

Non-method call resolution

Resolution of non-method calls is much easier, since there is no such thing as auto-dereferencing and borrowing, even if the target is a method (Foo::m(&x) vs x.m()). However, as for method call resolution, we still need to take three cases into account:

1. The function is defined in a blanket implementation: As before, we check that the blanket constraint is satisfied, but this time for an argument or the call context, when it provides information about the return type.
2. The function is in a trait: As before, we substitute in the traits before performing the IsInstantiationOf check.
3. Not case 1 and 2: As before, simply perform the IsInstantiationOf check, using an argument or the call context, when it provides information about the return type.

The implementation is in the module NonMethodResolution for calls that target non-methods, and in the MethodResolution module for calls that target methods.

Non-method call type inference

When the call is an operator call, we need to take into account that implicit borrowing may happen. For example, x == y is syntactic sugar for PartialEq::eq(&x, &y), so in order for the types to properly match up, we adjust the types of the operator, by stripping away the &s. This is done in the new OperationMatchingInput module.

When the call is not an operator call, we can match types directly, which happens in the NonMethodCallMatchingInput module for calls that target non-methods, and in the MethodCallMatchingInput module for calls that target methods.

Future work

• As before this PR, we do not handle the Deref trait when performing auto-dereferencing and unsized coercions. With this PR, however, it should be much easier to support that.
• Investigate the slowdowns/failures reported by DCA/QA.
• When we rule out a given candidate receiver type in order to progress to the next candidate, we do not currently take blanket implementations into account. This means that even if a blanket implementation matches for a given candidate receiver type C_i, we will still lookup in C_(i+1) as well. Supporting this is not straightforward, since we need a monotonic way of checking blanket constraint non-satisfaction.