Represent FnDefs as zero-sized structs instead of Code

[fzaiser]

Description of changes:

Before this change, Kani compiled functions (FnDefs) to Code in GotoC, i.e. C function types. This causes problems because functions in C are not first-class, e.g. they cannot be stored in a struct. In Rust, this is possible: functions are just zero-sized objects of a unique anonymous type. To allow the same behavior in GotoC, we need to actually represent FnDefs as zero-sized objects.

For this reason, we create for each function instance f in Rust an empty dummy type f::FnDefStruct and a global variable f::FnDefSingleton. We need to do this for each instance to ensure that function pointer equality behaves as expected. This is done by the codegen_fun_expr_zst.

In some contexts, e.g. when calling a function or casting a function to a function pointer, we need to convert the dummy struct back to an actual function. This is done by calling codegen_func_expr instead.

This change also allows us to enable type checking of fields (cf. #1243).

Resolved issues:

Resolves #1243

Call-outs:

Also, we no longer ignore FnDef parameters of functions. I believe this is desirable because it makes the code more consistent, but I can undo the change if you want.

Testing:

• How is this change tested? Additional tests in tests/kani/FunctionSymbols, plus the existing regression tests exercising this code as well.

• Is this a refactor change? No.

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[tautschnig]

Just curious: do you actually need to put those elements in the struct at all? I can see how that might make sense at the Rust level for perhaps it introduces scopes or convenient names, but maybe this just doesn't need to be carried over?

[danielsn]

And document what this returns

[fzaiser]

Fixed in the next commit.

[danielsn]

Might be cleaner to just return the symbol, which would have the name and type included

[fzaiser]

Good point, done.

[fzaiser]

Actually, that does not work. Because at least for the function memcmp, the signature generated by codegen_function_sig is different from the type that's already in the symbol table. If I add an assertion to check that the two results are the same

let funct = self.codegen_function_sig(self.fn_sig_of_instance(instance).unwrap());
let sym = self.ensure(&func, |ctx, _| {
    Symbol::function(
        &func,
        funct.clone(),
        None,
        Some(ctx.readable_instance_name(instance)),
        Location::none(),
    )
    .with_is_extern(true)
});
dbg!(instance);
assert_eq!(funct, sym.typ.clone());

Then I get the following error:

$ kani tests/kani/Whitespace/main.rs
[...]
[kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:637] instance = Instance {
    def: Item(
        WithOptConstParam {
            did: DefId(3:10534 ~ core[916d]::slice::cmp::{extern#0}::memcmp),
            const_param_did: None,
        },
    ),
    substs: [],
}
thread 'rustc' panicked at 'assertion failed: `(left == right)`
  left: `Code { parameters: [Parameter { typ: Pointer { typ: Unsignedbv { width: 8 } }, identifier: None, base_name: None }, Parameter { typ: Pointer { typ: Unsignedbv { width: 8 } }, identifier: None, base_name: None }, Parameter { typ: CInteger(SizeT), identifier: None, base_name: None }], return_type: Signedbv { width: 32 } }`,
 right: `Code { parameters: [Parameter { typ: Pointer { typ: Empty }, identifier: None, base_name: None }, Parameter { typ: Pointer { typ: Empty }, identifier: None, base_name: None }, Parameter { typ: CInteger(SizeT), identifier: None, base_name: None }], return_type: CInteger(Int) }`'

I guess the type that's stored for memcmp is different because it's built-in? How should I proceed?

[fzaiser]

I did not want to spend too much time on this, so I decided to just return the symbol and the type for now. I filed #1350 to track this problem and added a fixme in the code.

[fzaiser]

@tautschnig I think we could filter out struct fields, parameters and local variables of FnDef type and not generate code for them. But staying closer to the MIR has the advantage of less special casing in the GotoC generation. Kani has also introduced some type checking (which is where #1243 was discovered in the first place) where the GotoC type is compared with the MIR type. This would also require more special casing if we just erase FnDefs. Do you think there's a performance penalty with the current approach?

[tautschnig]

@tautschnig I think we could filter out struct fields, parameters and local variables of FnDef type and not generate code for them. But staying closer to the MIR has the advantage of less special casing in the GotoC generation. Kani has also introduced some type checking (which is where #1243 was discovered in the first place) where the GotoC type is compared with the MIR type. This would also require more special casing if we just erase FnDefs. Do you think there's a performance penalty with the current approach?

No, I'm not really sure there is much of a performance cost. I was just wondering whether getting rid of those struct members would be easier to implement. But you seem to have a working solution already, so all is well.

[fzaiser]

I just added some explanations and a link to this PR in the comments to provide context. i also updated the PR description.

[danielsn]

Might be cleaner to just return the symbol, which would have the name and type included

[celinval]

That's a clever approach. The function names are a bit confusing to me though. I would suggest moving the "ensure*" functions to typ.rs and rename them to codegen_*_type. I also suggest renaming codegen_func_expr_zst to something like codegen_fn_item.

[celinval]

This comment is duplicated

[fzaiser]

I've shortened it. But I don't want to remove it completely because it adds important context in my opinion. Same for the comment in rvalue.rs. I agree that the comment in typ.rs is redundant though (it just copied the function doc), so I've removed that one.

[celinval]

You could also add the definition from the rust reference: https://doc.rust-lang.org/reference/types/function-item.html

[fzaiser]

@celinval I've renamed the fndef_zst function and moved it to typ.rs as you suggested. But I left the function ensure_func where it is because it just ensures that the function symbol is in the symbol table, which is not really about types, right? I've renamed it to codegen_func_symbol though. I also followed your other renaming suggestions. Finally, I added the link to the rust reference. I'm not sure what you mean by "add the definition".