Ensure that contract closures are FnOnce

[vonaka]

Rust believes that Kani's contract closures are FnMut. This prevents us from writing contracts for functions that return mutable references to their input arguments (#3764).

To ensure Rust correctly infers these closures as FnOnce, they need to be wrapped in a dummy function that explicitly requires an FnOnce. This wrapping must be done at the point of closure definition, as doing it later, when calling the function, doesn't seem to have any effect.

Resolves #3764

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

[carolynzech]

Thanks! Before we review the code, can you write test(s)? You can put the one from the linked issue in the kani folder (which just checks that Kani exits successfully), and perhaps then add some more complex tests to the expected folder that ensure that the printed output contains successful assertions for the postconditions.

You can take a look at the existing contracts tests for inspiration. To run a test, run cargo build-dev && cargo run -p compiletest -- --suite [SUITE] --mode [MODE] <test name>. You can look at scripts/kani-regression.sh for the relevant suites and modes (or run cargo run -p compiletest -- --help).

[vonaka]

@carolynzech I added some basic tests. Regarding PR itself, defining force_fn_once to later replace it with literarily the same function feels suboptimal. Maybe at the very least, the body of force_fn_once should be unreachable!, just like kani_register_contract. Speaking of which, I wonder if this function is still needed considering this PR

[carolynzech]

Regarding PR itself, defining force_fn_once to later replace it with literarily the same function feels suboptimal. Maybe at the very least, the body of force_fn_once should be unreachable!, just like kani_register_contract. Speaking of which, I wonder if this function is still needed considering this PR

Yeah, so I can think of a couple of things you can try here:

1. Make the body of the functions in kani_macros unreachable!, just like kani_register_contract does, or
2. Remove the compiler & kani_core changes entirely and just do the transformations entirely in the macro expansion logic. I would think you could just change the macro logic to have an extra () that calls these const functions, so that then the closures are just there. You'd have to try it, though.

I don't know if we'll need kani_register_contract anymore. I would try removing it and seeing if we can still write contracts instead const functions, since that's why we needed it in the first place.

[carolynzech]

Can you add a comment describing what this tests and why it fails?

[carolynzech]

Add a comment describing what this tests, linking to the Github issue that this closes

[carolynzech]

Also can you add a test for the Github issue test case specifically? I did it locally and confirmed it works; it's just nice to have the sanity check that we did in fact solve that particular issue.

[carolynzech]

Can you expand this comment to describe why this is important?
(Perhaps link to the issue here again)

[vonaka]

Thanks, I've added some comments.

[tautschnig]

I'd suggest also including a particular "assertion ..." line(s).

[vonaka]

I added a few lines, although the test is really elementary and doesn't have any interesting assertion.

[vonaka]

Remove the compiler & kani_core changes entirely and just do the transformations entirely in the macro expansion logic. I would think you could just change the macro logic to have an extra () that calls these const functions, so that then the closures are just there. You'd have to try it, though.

Right, so I simply reverted all the changes to the core and the compiler. I assume this is enough? The only problem I see is that if the file Kani tries to verify has its own kani_force_fn_once, Kani will fail to compile. But this is also the case for kani_register_contract, so at least I'm being consistent with the existing code. In general, I'm not sure how to fix this elegantly (and I'm not sure if it's worth fixing).