[miguelcorderopamphile]

Refs #3738 (this does not close the issue: cross-crate metadata is not covered yet).

What this changes

Kani now fails verification when the vtable pointer used by a virtual call is equal to a vtable that it generated for a different principal trait. This detects invalid wide pointer metadata like the reproducer in #3738:

let meta_b = ptr::metadata(&s as &dyn B);
let meta_a: DynMetadata<dyn A> = unsafe { std::mem::transmute(meta_b) };
let fat: *const dyn A = ptr::from_raw_parts(data, meta_a);
let _ = (*fat).f(); // UB; previously verified successfully

Context

ptr::from_raw_parts goes through normal MIR, and nothing validated the metadata. Vtables are already generated as Kani::CommonVTable globals with a size sanity check (check_vtable_size), so this check reuses that machinery: VtableCtx records each generated vtable with its principal trait, and codegen_virtual_funcall adds one SafetyCheck assertion per call site (a single conjunction over the mismatching vtables).

The principal comparison matches what codegen already uses to reuse vtables for dyn-to-dyn casts, so auto trait differences (e.g. dyn T + Send to dyn T) do not trigger the check.

Known limitations

• Only vtables generated in the same crate are checked. Wrong-trait metadata that points to a vtable from another crate is not caught yet; that requires the per-call-site data that --restrict-vtable aggregates after linking (left as the design question in Check vtable validity when explicitly creating wide pointer #3738).
• The set of vtables seen grows during codegen, so checks use the vtables recorded up to that point.

Testing

• New regression test tests/expected/dyn-vtable-wrong-trait/wrong_trait_vtable.rs, plus the reproducer above.
• tests/kani: 618 passed (3 pre-existing, unrelated failures in Quantifiers on this machine because z3 is unavailable), tests/ui: 153 passed, tests/expected: 499 passed (remaining failures are pre-existing on this CBMC build), DynTrait suite: 30/30, covering upcasting, dyn Fn and cross-crate trait objects.

AI assistance was used to develop this change.