model-checking
Ensure that contract closures are FnOnce
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 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
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).
Thanks! Before merging, can you check if we can indeed get rid of
kani_register_contract?
We can't, we still need this workaround to call closures from const functions.