Single use of `type_map`

[tedinski]

There is exactly one use of type_map:

https://github.com/model-checking/kani/blob/89c1269fd163f4aa38b1ae475ce2b780bd229d43/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs#L120-L124

I believe this code (the function virtual_call_with_restricted_fn_ptr) could have its arguments changed to take the MIR type instead of the cprover_bindings Type, and so it wouldn't have to reverse this lookup in the first place.

There are exactly two callsites for virtual_call_with_restricted_fn_ptr:

• codegen_virtual_funcall of course
• codegen_drop in the virtual case

I think, but haven't dug into it enough yet, that each of these sites already "knows" the trait, which is what is needed here.

[tedinski]

After experimenting, I think I'm partially right that the callers have the MIR type. Just not in exactly the right form, unfortunately.

@celinval Can you help me understand a bit of this code? I think in codegen_virtual_funcall we almost have the MIR Ty we want, but sometimes self_ty is something like Box<dyn Trait>. The self.extract_ptr seems to construct the CBMC Expr for getting the vtable pointer, and I think something similar should be adaptable to also give me the resulting MIR type too, but I'm taking a bit too long to understand this code.

Is there a simple way to get the trait Ty here?

[celinval]

Yes, you should be able to use receiver_data_path which is used by self.extract_ptr. Something similar to this code except that you can just use iter::last() instead of iter::map() to get the fat pointer's Ty: https://github.com/model-checking/kani/blob/89c1269fd163f4aa38b1ae475ce2b780bd229d43/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs#L1416-L1420

[celinval]

BTW, you should be aware of this issue with drop: https://github.com/model-checking/kani/issues/1072