Skip to content

Conversation

@ssyram
Copy link
Contributor

@ssyram ssyram commented Oct 8, 2025

Following #814 , this PR is further split from #762, which includes the part of vtable support for the correct dispatch of virtual methods. Now, calling methods of &dyn Trait will be translated to finding the corresponding function pointer from the vtable (fetched by ptr_metadata operation) and then call the function pointer.

Specifically, calling virtual methods is turned from <dyn Trait as Trait>::method(receiver, args...) to something like:

let vtable = receiver.ptr_metadata;
let method_fn_ptr = vtable.method_index;
method_fn_ptr(receiver, args...)

This is reached by adding a new pass: normalize::transform_dyn_trait_calls.

@ssyram ssyram force-pushed the dyn-method-dispatch branch 2 times, most recently from 3917c3e to 5c500f6 Compare October 8, 2025 08:53
@Nadrieril Nadrieril force-pushed the dyn-method-dispatch branch from 6a7e238 to 81edea2 Compare October 8, 2025 14:41
@Nadrieril Nadrieril enabled auto-merge October 8, 2025 14:41
@Nadrieril Nadrieril added this pull request to the merge queue Oct 8, 2025
Merged via the queue into AeneasVerif:main with commit c66a520 Oct 8, 2025
7 checks passed
@ssyram ssyram deleted the dyn-method-dispatch branch October 8, 2025 16:02
@ssyram ssyram mentioned this pull request Oct 9, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants