Audit function signature codegen

[fzaiser]

The code of closure_sig is copy-pasted from fn_sig_for_fn_abi in compiler/rustc_middle/src/ty/layout.rs. We may have to do something similar for generators (#416), so it would be good if we could use the rustc function fn_abi_of_instance directly (as the comment on fn_sig_for_fn_abi suggests. This would prevent problems with keeping in sync with rustc.

[fzaiser]

The relevant function fn_sig_for_fn_abi is here. It has a comment saying:

    // NOTE(eddyb) this is private to avoid using it from outside of
    // `fn_abi_of_instance` - any other uses are either too high-level
    // for `Instance` (e.g. typeck would use `Ty::fn_sig` instead),
    // or should go through `FnAbi` instead, to avoid losing any
    // adjustments `fn_abi_of_instance` might be performing.

So the question is whether we should use Ty::fn_sig or fn_abi_of_instance. To find out, I looked at the cranelift backend. They use this function to obtain the signature of a function/closure/generator. I presume we should do something similar.

Note that the fn_abi_of_instance function makes some adjustments to the signature returned by the private function fn_sig_for_fn_abi: they happen in the call to fn_abi_new_uncached here, in that function they call fn_abi_adjust_for_abi here, which is defined just below.

[fzaiser]

@celinval The adjustments to the signature could be related to #1350. These adjustments don't currently happen in the Kani code, but they probably should.

[celinval]

Totally! We should investigate if using fn_abi_of_instance would simplify how we handle functions today. I believe this is also related to the issue we were having with closure to function pointer casting: #274

For the ZST parameters, the parameter "mode" is set to Ignore.

[celinval]

@celinval The adjustments to the signature could be related to #1350. These adjustments don't currently happen in the Kani code, but they probably should.

I don't think this would actually fix #1350 though. I believe we add those functions to the symbol table and their signature matches CBMC ones.

FYI, we declare these functions and their signatures here: https://github.com/model-checking/kani/blob/main/cprover_bindings/src/goto_program/builtin.rs

[celinval]

Note that the function ABI will include the tracker location when required, so #374 and this issue are somewhat related.