Function Contracts: remove instances of _renamed

[pi314mm]

The current method for creating the modifies wrapper requires changing the ensures clause to have _renamed variables which are unsafe copies of the original function arguments. This causes issues with regards to some possible tests as in #3239.

This change removes the _renamed variables and instead simply changes the modifies clauses within the replace to unsafely dereference the pointer to modify the contents of it unsafely, condensing all instances of unsafe Rust into a single location.

Resolves #3239
Resolves #3026
May affect #3027. In my attempt to run this example with slight modification to fit the current implementation, I got the error CBMC appears to have run out of memory. You may want to rerun your proof in an environment with additional memory or use stubbing to reduce the size of the code the verifier reasons about. This suggests that the compilation is working appropriately but the test case is just too large for CBMC.

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

[feliperodri]

Why would this change affect #3027? Add the response to the PR description.

[celinval]

That's a nice cleanup. Thanks

[celinval]

Why are you changing this?

[pi314mm]

The test originally did not make sense as the S struct gets consumed by the modify function and so you cannot refer to the contents of it within the ensures. The test originally passed unsafely as it ignored the fact that it referred to a potentially deallocated memory address. Changing it to a pass by reference is better than deleting the test.

[celinval]

Did the test break with your changes? I still believe we need tests to capture what the behavior would be here. Broken tests should trigger an error, not deleted since a user could make the same mistake

[pi314mm]

The test broke, but error cannot be represented within the current expected test framework because valid rust code is not produced after the macro expansion, so the kani compilation fails. In other words, it broke before we could check if it breaks. To include this failing test case, the harness for expected needs to be changed.

Basically, the test case expands to something like

modify(s, prior); // s is consumed here
kani::assert(*s.target == prior + 1, "*s.target == prior + 1"); // s is used here after it is consumed

which is definitely not valid Rust code, and kani is unable to compile it, and the expected test fails even with the error message being included into the .expected file.

A better test case that is now fixed by this code change was mentioned in the issue #3239

#[derive(Clone,Copy)]
struct Five;

impl Five {
    fn five(self : &Five) -> u32{
        5
    }
}

#[kani::ensures(|result : &Five| x.five() == result.five())]
fn id(x : Five) -> Five {
    x
}

#[kani::proof_for_contract(id)]
fn eat_harness() {
    let x = Five;
    id(x);
}

If you leave the copy/clone line, the test works (did not work before this change). If you delete the copy/clone line, you get the following error

error[E0382]: borrow of moved value: `x`
  --> ../test.rs:9:17
   |
9  | #[kani::ensures(|result : &Five| x.five() == result.five())]
   |                 ^^^^^^^^^^^^^^^^ - borrow occurs due to use in closure
   |                 |
   |                 value borrowed here after move
10 | fn id(x : Five) -> Five {
   |       -
   |       |
   |       value moved here
   |       move occurs because `x` has type `Five`, which does not implement the `Copy` trait
   |
note: consider changing this parameter type in function `id_wrapper_8110d0` to borrow instead if owning the value isn't necessary
  --> ../test.rs:10:11
   |
9  | #[kani::ensures(|result : &Five| x.five() == result.five())]
   | ------------------------------------------------------------ in this function
10 | fn id(x : Five) -> Five {
   |           ^^^^ this parameter takes ownership of the value
note: if `Five` implemented `Clone`, you could clone the value
  --> ../test.rs:1:1
   |
1  | struct Five;
   | ^^^^^^^^^^^ consider implementing `Clone` for this type
...
10 | fn id(x : Five) -> Five {
   |       - you could clone this value

[celinval]

We usually use the ui suite to ensure compilation errors are user friendly. In this case, I would recommend to move the broken test there. Thanks